BoundaryFromLogProducts.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Boundary limits from contracting logarithmic increments

The actual finite BCH estimate constructs uniform normalized limits in a common compact set. Continuous trajectories then define a continuous boundary map on an actual quotient whenever trajectories in a common fiber are asymptotic. Only that geometric fiber condition remains an input here; no boundary map or compact shadow is assumed.

theorem OAI.PolycyclicRecognition.exists_compact_uniform_log_product_limit line 28

Source documentation

The normalized product limits of a whole contracting family lie in one compact set, while convergence is uniform in exponential coordinates.

theorem exists_compact_uniform_log_product_limit
    (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) (K : Set G), IsCompact K ∧ (∀ p, g p ∈ K) ∧
      (∀ p, Tendsto (exponentialPartialProduct Exp (X p)) atTop (𝓝 (g p))) ∧
…

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

theorem OAI.PolycyclicRecognition.exists_quotient_boundary_of_summable_log_increments line 71

Source documentation

Contracting logarithmic increments and geometric asymptotic equality on fibers construct the continuous boundary map and a fixed compact normalized shadow.

theorem exists_quotient_boundary_of_summable_log_increments
    {Q : Type*} [TopologicalSpace P] [TopologicalSpace Q]
    (q : P → Q) (hq : Topology.IsQuotientMap q)
    (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)
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput