ChainProducts.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Polynomial coordinates for nilpotent chains

Every bounded-step chain is an actual product of its group increments. Compactness bounds the increment logarithms in a global exponential chart. The finite Dynkin identity then bounds all endpoint coordinates polynomially in the number of steps. No geometric growth estimate is assumed.

theorem OAI.PolycyclicRecognition.BoundedHeightChain.exists_increment_list line 27
Source documentation
The increments telescope to the relative endpoint, with their actual lengths controlled by the chain steps.
```
theorem BoundedHeightChain.exists_increment_list {π : G → W} {L M : ℝ}
    {m : ℕ} {x y : G} (h : BoundedHeightChain π L M m x y) :
    ∃ l : List G, l.length = m ∧ (∀ g ∈ l, dist (1 : G) g ≤ L) ∧ l.prod = x⁻¹ * y := by
…
```
Mentions: OAI.PolycyclicRecognition.BoundedHeightChain
theorem OAI.PolycyclicRecognition.BoundedHeightChain.mono_step line 44
Source documentation
Increase the permitted step length without changing the chain.
```
theorem BoundedHeightChain.mono_step {π : G → W} {L L' M : ℝ}
    {m : ℕ} {x y : G} (h : BoundedHeightChain π L M m x y) (hL : L ≤ L') :
    BoundedHeightChain π L' M m x y := by
…
```
Mentions: OAI.PolycyclicRecognition.BoundedHeightChain

theorem OAI.PolycyclicRecognition.BoundedHeightChain.snoc line 53

Source documentation

Append one final bounded step.

theorem BoundedHeightChain.snoc {π : G → W} {L M : ℝ}
    {m : ℕ} {x y z : G} (h : BoundedHeightChain π L M m x y)
    (hz : ‖π z‖ ≤ M) (hyz : dist y z ≤ L) :
    BoundedHeightChain π L M (m + 1) x z := by
…

Mentions: OAI.PolycyclicRecognition.BoundedHeightChain

theorem OAI.PolycyclicRecognition.exists_bound_increment_log line 68

Source documentation

Compact metric balls have bounded logarithms in any fixed exponential coordinate basis.

theorem exists_bound_increment_log
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G)
    (chart : GroupLieAlgebra (𝓘(ℝ, E)) G ≃ₜ G) (hchart : ∀ x, chart x = Exp x)
    {J : Type*} [Fintype J] (b : Basis J ℝ (GroupLieAlgebra (𝓘(ℝ, E)) G))
    (L : ℝ) : ∃ R : ℝ, 0 ≤ R ∧ ∀ g, dist (1 : G) g ≤ L →
      ∃ x, Exp x = g ∧ ‖b.equivFun x‖ ≤ R := by
…

theorem OAI.PolycyclicRecognition.exists_basis_structureConstant_bound line 86

Source documentation

The finite list of basis brackets always has a common bound.

theorem exists_basis_structureConstant_bound {L : Type*} [LieRing L] [LieAlgebra ℝ L]
    {J : Type*} [Fintype J] (b : Basis J ℝ L) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ i j l, |b.repr ⁅b i, b j⁆ l| ≤ C := by
…

theorem OAI.PolycyclicRecognition.exists_polynomial_chain_coordinate_bound line 96

Source documentation

Bounded-step chains in the nilpotent group have polynomial logarithmic coordinate size. The height function imposes no extra restriction here.

theorem exists_polynomial_chain_coordinate_bound
    (dynkin : NilpotentDynkinExpansionInput E G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (chart : GroupLieAlgebra (𝓘(ℝ, E)) G ≃ₜ G) (hchart : ∀ x, chart x = Exp x)
    {c : ℕ} (hzero : lowerCentralSeries ℝ (GroupLieAlgebra (𝓘(ℝ, E)) G)
      (GroupLieAlgebra (𝓘(ℝ, E)) G) c = ⊥)
    {J : Type*} [Fintype J] (b : Basis J ℝ (GroupLieAlgebra (𝓘(ℝ, E)) G))
    (L : ℝ) :
    ∃ A : ℝ, 0 ≤ A ∧ ∀ (π : G → W) (M : ℝ) (m : ℕ) (x y : G),
      BoundedHeightChain π L M m x y →
      ∃ z, Exp z = x⁻¹ * y ∧ ‖b.equivFun z‖ ≤ A * (1 + (m : ℝ)) ^ c := by
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.BoundedHeightChain