Module

Valued_exists_mulVec_add_eq_of_v_det_eq_one.lean

Nyll.AlgebraicCurves.Valuations.Valued_exists_mulVec_add_eq_of_v_det_eq_one

9 declarations indexed from sourceView source ↗

Module documentation

Valued exists mul Vec add eq of v det eq one

Imports19

Mathlib.Algebra.BigOperators.Group.Finset.Defs
Mathlib.Algebra.GroupWithZero.Range
Mathlib.Algebra.GroupWithZero.Units.Basic
Mathlib.Algebra.Order.BigOperators.Group.Finset
Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Mathlib.Algebra.Ring.Int.Units
Mathlib.Data.Finset.Lattice.Fold
Mathlib.Data.Matrix.Mul
Mathlib.LinearAlgebra.Matrix.Adjugate
Mathlib.LinearAlgebra.Matrix.Defs
Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Mathlib.LinearAlgebra.Matrix.RowCol
Mathlib.RingTheory.Valuation.Basic
Mathlib.Topology.Algebra.Valued.ValuationTopology
Mathlib.Topology.UniformSpace.Cauchy
Mathlib.Tactic.Choose
Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.SplitIfs

Imported by1

Nyll.AlgebraicCurves.Valuations.All

theorem

v_sum_le

L47 ↗

AlgebraicCurves.Valuations.Proofs.Valued_exists_mulVec_add_eq_of_v_det_eq_one.NewtonNA.v_sum_le

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.Valued_exists_mulVec_add_eq_of_v_det_eq_one
namespace NewtonNA
open Matrix
variable {K : Type} [Field K] {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀]

Lean source · statement

theorem v_sum_le {ι : Type} (s : Finset ι) (f : ι → K) (g : Γ₀) (h : ∀ i ∈ s, Valued.v (f i) ≤ g) :
    Valued.v (∑ i ∈ s, f i) ≤ g

theorem

v_det_le_one

L51 ↗

AlgebraicCurves.Valuations.Proofs.Valued_exists_mulVec_add_eq_of_v_det_eq_one.NewtonNA.v_det_le_one

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.Valued_exists_mulVec_add_eq_of_v_det_eq_one
namespace NewtonNA
open Matrix
variable {K : Type} [Field K] {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀]

Lean source · statement

theorem v_det_le_one {n : ℕ} (M : Matrix (Fin n) (Fin n) K) (hM : ∀ i j, Valued.v (M i j) ≤ 1) :
    Valued.v M.det ≤ 1

theorem

v_adjugate_le_one

L63 ↗

AlgebraicCurves.Valuations.Proofs.Valued_exists_mulVec_add_eq_of_v_det_eq_one.NewtonNA.v_adjugate_le_one

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.Valued_exists_mulVec_add_eq_of_v_det_eq_one
namespace NewtonNA
open Matrix
variable {K : Type} [Field K] {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀]

Lean source · statement

theorem v_adjugate_le_one {n : ℕ} (M : Matrix (Fin n) (Fin n) K) (hM : ∀ i j, Valued.v (M i j) ≤ 1)
  (i j : Fin n) :
    Valued.v (M.adjugate i j) ≤ 1

theorem

v_inv_le_one

L74 ↗

AlgebraicCurves.Valuations.Proofs.Valued_exists_mulVec_add_eq_of_v_det_eq_one.NewtonNA.v_inv_le_one

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.Valued_exists_mulVec_add_eq_of_v_det_eq_one
namespace NewtonNA
open Matrix
variable {K : Type} [Field K] {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀]

Lean source · statement

theorem v_inv_le_one {n : ℕ} (M : Matrix (Fin n) (Fin n) K) (hM : ∀ i j, Valued.v (M i j) ≤ 1)
    (hdet : Valued.v M.det = 1) (i j : Fin n) : Valued.v (M⁻¹ i j) ≤ 1

theorem

v_mulVec_le

L80 ↗

AlgebraicCurves.Valuations.Proofs.Valued_exists_mulVec_add_eq_of_v_det_eq_one.NewtonNA.v_mulVec_le

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.Valued_exists_mulVec_add_eq_of_v_det_eq_one
namespace NewtonNA
open Matrix
variable {K : Type} [Field K] {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀]

Lean source · statement

theorem v_mulVec_le {n : ℕ} (M : Matrix (Fin n) (Fin n) K) (hM : ∀ i j, Valued.v (M i j) ≤ 1)
    (w : Fin n → K) (τ : Γ₀) (hw : ∀ j, Valued.v (w j) ≤ τ) (i : Fin n) :
    Valued.v ((M *ᵥ w) i) ≤ τ

theorem

exists_eq_restrict

L94 ↗

AlgebraicCurves.Valuations.Proofs.Valued_exists_mulVec_add_eq_of_v_det_eq_one.NewtonNA.exists_eq_restrict

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.Valued_exists_mulVec_add_eq_of_v_det_eq_one
namespace NewtonNA
variable {K : Type} [Field K] {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀]

Lean source · statement

theorem exists_eq_restrict (γ : (MonoidWithZeroHom.ValueGroup₀ (MonoidWithZeroHom.ofClass (Valued.v
  : Valuation K Γ₀)))ˣ) :
    ∃ w : K, w ≠ 0 ∧ (Valued.v : Valuation K Γ₀).restrict w = (γ : MonoidWithZeroHom.ValueGroup₀
      (MonoidWithZeroHom.ofClass (Valued.v : Valuation K Γ₀)))

theorem

eventually_lt_of_tendsto

L105 ↗

AlgebraicCurves.Valuations.Proofs.Valued_exists_mulVec_add_eq_of_v_det_eq_one.NewtonNA.eventually_lt_of_tendsto

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.Valued_exists_mulVec_add_eq_of_v_det_eq_one
namespace NewtonNA
variable {K : Type} [Field K] {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀]

Lean source · statement

theorem eventually_lt_of_tendsto {f : ℕ → K} {a : K} (h : Filter.Tendsto f Filter.atTop (nhds a))
    (w : K) (hw : w ≠ 0) : ∃ N : ℕ, ∀ k, N ≤ k → Valued.v (f k - a) < Valued.v w

theorem

exists_tendsto_of_v_sub_le_pow

L122 ↗

AlgebraicCurves.Valuations.Proofs.Valued_exists_mulVec_add_eq_of_v_det_eq_one.NewtonNA.exists_tendsto_of_v_sub_le_pow

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.Valued_exists_mulVec_add_eq_of_v_det_eq_one
namespace NewtonNA
variable {K : Type} [Field K] {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀]

Lean source · statement

theorem exists_tendsto_of_v_sub_le_pow [CompleteSpace K]
    (hrk : ∀ x y : K, Valued.v x < 1 → y ≠ 0 → ∃ m : ℕ, Valued.v x ^ m ≤ Valued.v y)
    (x₀ : K) (hx₀0 : Valued.v x₀ ≠ 0) (hx₀ : Valued.v x₀ < 1) (f : ℕ → K)
    (hf : ∀ a b : ℕ, a ≤ b → Valued.v (f b - f a) ≤ Valued.v x₀ ^ (a + 1)) :
    ∃ a : K, Filter.Tendsto f Filter.atTop (nhds a)

theorem

exists_mulVec_add_eq_of_v_det_eq_one

L153 ↗

Valued.exists_mulVec_add_eq_of_v_det_eq_one

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.Valued_exists_mulVec_add_eq_of_v_det_eq_one
open Matrix NewtonNA in

Lean source · statement

theorem _root_.Valued.exists_mulVec_add_eq_of_v_det_eq_one
    {K : Type} [Field K] {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀]
      [CompleteSpace K]
    (hrk : ∀ x y : K, Valued.v x < 1 → y ≠ 0 → ∃ m : ℕ, Valued.v x ^ m ≤ Valued.v y)
    {n : ℕ} (A : Matrix (Fin n) (Fin n) K) (hA : ∀ i j : Fin n, Valued.v (A i j) ≤ 1)
    (hdet : Valued.v A.det = 1)
    (R : (Fin n → K) → (Fin n → K)) (hR0 : R 0 = 0)
    (hR : ∀ (ε ε' : Fin n → K) (s t : Γ₀), s < 1 → (∀ j, Valued.v (ε j) ≤ s) → (∀ j, Valued.v (ε'
      j) ≤ s) →
      (∀ j, Valued.v (ε j - ε' j) ≤ t) → ∀ i, Valued.v (R ε i - R ε' i) ≤ t * s)
    (y : Fin n → K) (s : Γ₀) (hs : s < 1) (hy : ∀ i, Valued.v (y i) ≤ s) :
    ∃ ε : Fin n → K, (∀ i, Valued.v (ε i) ≤ s) ∧ A.mulVec ε + R ε = y

Module documentation

Valued exists mul Vec add eq of v det eq one

Declarations