DynkinProductTails.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Convergence of products with summable logarithmic increments

Finite BCH gives a common bound on every tail product in terms of the sum of its logarithmic increments. The global exponential chart then gives convergence, without identifying its coordinate metric with a left invariant metric.

def OAI.PolycyclicRecognition.exponentialPartialProduct line 29

Source documentation

The ordered product of the first m exponential increments.

def exponentialPartialProduct
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G)
    (X : ℕ → GroupLieAlgebra (𝓘(ℝ, E)) G) (m : ℕ) : G :=
…

theorem OAI.PolycyclicRecognition.exponentialPartialProduct_add line 35

theorem OAI.PolycyclicRecognition.exists_tail_product_log_bound line 46

Source documentation

Summability controls the logarithm of every finite tail product, uniformly in the number of tail factors.

theorem exists_tail_product_log_bound
    (dynkin : NilpotentDynkinExpansionInput E G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    {c : ℕ} (hc : lowerCentralSeries ℝ (GroupLieAlgebra (𝓘(ℝ, E)) G)
      (GroupLieAlgebra (𝓘(ℝ, E)) G) c = ⊥)
    (b : Basis J ℝ (GroupLieAlgebra (𝓘(ℝ, E)) G))
    {C : ℝ} (hC : 0 ≤ C) (hbracket : ∀ i j k, |b.repr ⁅b i, b j⁆ k| ≤ C)
    (X : ℕ → GroupLieAlgebra (𝓘(ℝ, E)) G) (d : ℕ → ℝ) (hd : Summable d)
    (hX : ∀ n, ‖b.equivFun (X n)‖ ≤ d n) (n m : ℕ) :
    ∃ z, exponentialPartialProduct Exp (fun k => X (n + k)) m = Exp z ∧
      ‖b.equivFun z‖ ≤
        (c : ℝ) * 2 ^ c * (1 + (Fintype.card J : ℝ) ^ 2 * C) ^ c *
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.exponentialPartialProduct

theorem OAI.PolycyclicRecognition.dynkin_tail_bound_tendsto_zero line 76

Source documentation

The common bound for all finite tail products tends to zero.

theorem dynkin_tail_bound_tendsto_zero
    (A : ℝ) (c : ℕ) (d : ℕ → ℝ) :
    Tendsto (fun n => A * (∑' k, d (n + k)) * (1 + ∑' k, d (n + k)) ^ c)
      atTop (𝓝 0) := by
…

theorem OAI.PolycyclicRecognition.exponentialPartialProduct_tendsto_of_summable line 87

Source documentation

Actual ordered products with summable logarithmic increments converge in the global exponential chart. The proof uses the common finite-tail bound and compactness in coordinates, not a metric invariance assumption.

theorem exponentialPartialProduct_tendsto_of_summable
    (dynkin : NilpotentDynkinExpansionInput E G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (chart : GroupLieAlgebra (𝓘(ℝ, E)) G ≃ₜ G) (hchart : ∀ v, chart v = Exp v)
    {c : ℕ} (hc : lowerCentralSeries ℝ (GroupLieAlgebra (𝓘(ℝ, E)) G)
      (GroupLieAlgebra (𝓘(ℝ, E)) G) c = ⊥)
    (b : Basis J ℝ (GroupLieAlgebra (𝓘(ℝ, E)) G))
    {C : ℝ} (hC : 0 ≤ C) (hbracket : ∀ i j k, |b.repr ⁅b i, b j⁆ k| ≤ C)
    (X : ℕ → GroupLieAlgebra (𝓘(ℝ, E)) G) (d : ℕ → ℝ) (hd : Summable d)
    (hX : ∀ n, ‖b.equivFun (X n)‖ ≤ d n) :
    ∃ g : G, Tendsto (exponentialPartialProduct Exp X) atTop (𝓝 g) := by
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.exponentialPartialProduct

theorem OAI.PolycyclicRecognition.trajectory_tendsto_of_summable_log_increments line 141

Source documentation

The same conclusion for an actual trajectory specified by its successive exponential increments.

theorem trajectory_tendsto_of_summable_log_increments
    (dynkin : NilpotentDynkinExpansionInput E G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (chart : GroupLieAlgebra (𝓘(ℝ, E)) G ≃ₜ G) (hchart : ∀ v, chart v = Exp v)
    {c : ℕ} (hc : lowerCentralSeries ℝ (GroupLieAlgebra (𝓘(ℝ, E)) G)
      (GroupLieAlgebra (𝓘(ℝ, E)) G) c = ⊥)
    (b : Basis J ℝ (GroupLieAlgebra (𝓘(ℝ, E)) G))
    {C : ℝ} (hC : 0 ≤ C) (hbracket : ∀ i j k, |b.repr ⁅b i, b j⁆ k| ≤ C)
    (X : ℕ → GroupLieAlgebra (𝓘(ℝ, E)) G) (d : ℕ → ℝ) (hd : Summable d)
    (hX : ∀ n, ‖b.equivFun (X n)‖ ≤ d n)
    (f : ℕ → G) (hstep : ∀ n, f (n + 1) = f n * Exp (X n)) :
    ∃ g : G, Tendsto f atTop (𝓝 g) := by
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput

theorem OAI.PolycyclicRecognition.finite_exp_products_tendsto_one line 169

Source documentation

Finite chains whose total logarithmic increment size tends to zero have endpoint product tending to the identity, even if their lengths grow.

theorem finite_exp_products_tendsto_one
    (dynkin : NilpotentDynkinExpansionInput E G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (hcontinuous : Continuous Exp)
    {c : ℕ} (hc : lowerCentralSeries ℝ (GroupLieAlgebra (𝓘(ℝ, E)) G)
      (GroupLieAlgebra (𝓘(ℝ, E)) G) c = ⊥)
    (b : Basis J ℝ (GroupLieAlgebra (𝓘(ℝ, E)) G))
    {C : ℝ} (hC : 0 ≤ C) (hbracket : ∀ i j k, |b.repr ⁅b i, b j⁆ k| ≤ C)
    (m : ℕ → ℕ) (X : (n : ℕ) → Fin (m n) → GroupLieAlgebra (𝓘(ℝ, E)) G)
    (hsmall : Tendsto (fun n => ∑ i, ‖b.equivFun (X n i)‖) atTop (𝓝 0)) :
    Tendsto (fun n => (List.ofFn (fun i => Exp (X n i))).prod) atTop (𝓝 (1 : G)) := by
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput

theorem OAI.PolycyclicRecognition.sum_norm_tendsto_zero_of_polynomial_count_exp_steps line 198

Source documentation

Polynomially many exponentially small increments have vanishing total size. This is the endpoint estimate for the representative-independence paths in boundary.tex.

theorem sum_norm_tendsto_zero_of_polynomial_count_exp_steps
    (b : Basis J ℝ (GroupLieAlgebra (𝓘(ℝ, E)) G))
    (m : ℕ → ℕ) (X : (n : ℕ) → Fin (m n) → GroupLieAlgebra (𝓘(ℝ, E)) G)
    (A K c : ℝ) (p q : ℕ) (hA : 0 ≤ A) (hc : 0 < c)
    (hcount : ∀ n, (m n : ℝ) ≤ K * (1 + (n : ℝ)) ^ q)
    (hstep : ∀ n i, ‖b.equivFun (X n i)‖ ≤
      A * (1 + (n : ℝ)) ^ p * Real.exp (-c * n)) :
    Tendsto (fun n => ∑ i, ‖b.equivFun (X n i)‖) atTop (𝓝 0) := by
…