UniformDynkinProducts.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform convergence in exponential coordinates

Compact coordinate balls give a uniform modulus for right multiplication by a small exponential. Combining it with the common BCH tail estimate gives uniform convergence of families of contracting products. No invariance of the coordinate metric is asserted or used.

theorem OAI.PolycyclicRecognition.exists_coordinate_mul_modulus line 24

Source documentation

Right multiplication by a point tending to the identity approaches the identity map uniformly on each bounded coordinate ball.

theorem exists_coordinate_mul_modulus
    {V G : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V]
    [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (e : V ≃ₜ G) (he : e 0 = 1) (R : ℝ) {ε : ℝ} (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ x : V, ‖x‖ ≤ R → ∀ y : V, ‖y‖ < δ →
      dist (e.symm (e x * e y)) x < ε := by
…

theorem OAI.PolycyclicRecognition.tendstoUniformly_of_uniform_forward_cauchy line 47

Source documentation

Pointwise limits of a uniformly Cauchy family of sequences are uniform limits. The tail estimate is only needed in the forward direction.

theorem tendstoUniformly_of_uniform_forward_cauchy
    {P V : Type*} [PseudoMetricSpace V] (f : P → ℕ → V) (b : P → V)
    (hlim : ∀ p, Tendsto (f p) atTop (𝓝 (b p)))
    (hc : ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ p n, N ≤ n → ∀ m, n ≤ m →
      dist (f p n) (f p m) < ε) :
    TendstoUniformly (fun n p => f p n) b atTop := by
…

theorem OAI.PolycyclicRecognition.exists_uniform_limit_of_summable_log_products line 72

Source documentation

A common summable logarithmic increment bound gives uniform convergence in any fixed global exponential coordinates. This applies simultaneously to the normalized trajectories for an entire quasi-isometry family.

theorem exists_uniform_limit_of_summable_log_products
    (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 : P → ℕ → GroupLieAlgebra (𝓘(ℝ, E)) G) (d : ℕ → ℝ) (hd : Summable d)
    (hX : ∀ p n, ‖b.equivFun (X p n)‖ ≤ d n) :
    ∃ g : P → G,
      (∀ p, Tendsto (exponentialPartialProduct Exp (X p)) atTop (𝓝 (g p))) ∧
…

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