CoarseNegativeQuotient.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Quotient asymptotics of actual negative-height chains

Sublinear height error preserves a linear negative margin on a linear ball. Polynomial metric factor bounds and compact unit increments then give asymptotic equality of the projected endpoints.

theorem OAI.PolycyclicRecognition.scalar_sublinear_error line 22

Source documentation

A continuous linear functional preserves a global sublinear error. The constant is chosen before the scale, including for the zero functional.

theorem scalar_sublinear_error
    {X W : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W]
    (length : X → ℝ) (hlen : ∀ x, 0 ≤ length x)
    (u v : X → W) (α : W →L[ℝ] ℝ)
    (hsub : ∀ ε : ℝ, 0 < ε → ∃ B : ℝ, 0 ≤ B ∧ ∀ x,
      ‖u x - v x‖ ≤ ε * length x + B) :
    ∀ ε : ℝ, 0 < ε → ∃ B : ℝ, 0 ≤ B ∧ ∀ x,
      |α (u x) - α (v x)| ≤ ε * length x + B := by
…

theorem OAI.PolycyclicRecognition.coarse_negative_chain_quotient_difference_tendsto_one line 57

Source documentation

A coarse map preserves enough negative height for every polynomial chain in a linear ball. The factors are selected from the actual metric factorization theorem, and the quotient increments are those of the map.

theorem coarse_negative_chain_quotient_difference_tendsto_one
    (ι : N →* G) (κ : D →* G) (π : N →* Q)
    (α : D →* MulAut Q) (act : G →* Equiv.Perm Q)
    (hact : ∀ u d q, act (ι u * κ d) q = π u * α d q)
    (dynkin : NilpotentDynkinExpansionInput E Q)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) Q → Q) (hExp : IsGroupExponential Exp)
    (chart : GroupLieAlgebra (𝓘(ℝ, E)) Q ≃ₜ Q) (hchart : ∀ v, chart v = Exp v)
    {c : ℕ} (hc : lowerCentralSeries ℝ (GroupLieAlgebra (𝓘(ℝ, E)) Q)
      (GroupLieAlgebra (𝓘(ℝ, E)) Q) c = ⊥)
    (b : Basis J ℝ (GroupLieAlgebra (𝓘(ℝ, E)) Q))
    (size height : D → ℝ) (sourceHeight : S → ℝ) (targetHeight : G → ℝ)
    (f : S → G) {L error : ℝ} (hL : 0 ≤ L)
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput

theorem OAI.PolycyclicRecognition.coarse_negative_chain_quotient_difference_of_compact_contraction line 141

Source documentation

Compact-set contraction in the quotient, independent of a choice of basis.

theorem coarse_negative_chain_quotient_difference_of_compact_contraction
    (ι : N →* G) (κ : D →* G) (π : N →* Q)
    (α : D →* MulAut Q) (act : G →* Equiv.Perm Q)
    (hact : ∀ u d q, act (ι u * κ d) q = π u * α d q)
    (dynkin : NilpotentDynkinExpansionInput E Q)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) Q → Q) (hExp : IsGroupExponential Exp)
    (chart : GroupLieAlgebra (𝓘(ℝ, E)) Q ≃ₜ Q) (hchart : ∀ v, chart v = Exp v)
    (hnil : LieRing.IsNilpotent (GroupLieAlgebra (𝓘(ℝ, E)) Q))
    (size height : D → ℝ) (sourceHeight : S → ℝ) (targetHeight : G → ℝ)
    (f : S → G) {L error : ℝ} (hL : 0 ≤ L)
    (hf : ∀ x y, dist (f x) (f y) ≤ L * dist x y + error)
    (hsub : ∀ ε : ℝ, 0 < ε → ∃ B : ℝ, 0 ≤ B ∧ ∀ x,
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput