PolynomialTranslationLimits.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Small translations in a compact family of polynomial group laws

Normalized brackets can vary with the box. Their compactness and the exact unit identity still make a vanishing right translation uniformly small on each fixed coordinate compact set.

theorem OAI.PolycyclicRecognition.dynkin_translations_tendstoUniformlyOn line 27

Source documentation

Uniformity in the normalized bracket is essential: the sequence of laws need not converge. Only the translation vector tends to zero.

theorem dynkin_translations_tendstoUniformlyOn
    {c : ℕ} (a : DynkinCoefficients c 2)
    (P : Set (V →L[ℝ] V →L[ℝ] V)) (hP : IsCompact P)
    (hunit : ∀ B ∈ P, ∀ x, dynkinProduct a B x 0 = x)
    {l : Filter ι} (B : ι → V →L[ℝ] V →L[ℝ] V) (hB : ∀ i, B i ∈ P)
    (q : ι → V) (hq : Tendsto q l (𝓝 0))
    (K : Set V) (hK : IsCompact K) :
    TendstoUniformlyOn (fun i x => dynkinProduct a (B i) x (q i)) id l K := by
…

Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.dynkinProduct

theorem OAI.PolycyclicRecognition.dynkin_translation_maps_tendsto line 61

Source documentation

The coordinate translation converges in the compact-open topology.

theorem dynkin_translation_maps_tendsto
    {c : ℕ} (a : DynkinCoefficients c 2)
    (P : Set (V →L[ℝ] V →L[ℝ] V)) (hP : IsCompact P)
    (hunit : ∀ B ∈ P, ∀ x, dynkinProduct a B x 0 = x)
    {l : Filter ι} (B : ι → V →L[ℝ] V →L[ℝ] V) (hB : ∀ i, B i ∈ P)
    (q : ι → V) (hq : Tendsto q l (𝓝 0)) :
    Tendsto (fun i => (⟨fun x => dynkinProduct a (B i) x (q i),
      continuous_dynkinProduct a _ _ _ continuous_const continuous_id continuous_const⟩ : C(V, V)))
      l (𝓝 (ContinuousMap.id V)) := by
…

Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.dynkinProduct, OAI.PolycyclicRecognition.continuous_dynkinProduct

theorem OAI.PolycyclicRecognition.measure_dynkin_translation_symmDiff_tendsto_zero line 76

Source documentation

For a normalized Haar measure, small polynomial translations preserve a fixed finite cell up to a symmetric difference of vanishing measure.

theorem measure_dynkin_translation_symmDiff_tendsto_zero
    [MeasurableSpace V] [BorelSpace V]
    (μ : Measure V) [μ.InnerRegularCompactLTTop] [IsLocallyFiniteMeasure μ]
    {c : ℕ} (a : DynkinCoefficients c 2)
    (P : Set (V →L[ℝ] V →L[ℝ] V)) (hP : IsCompact P)
    (hunit : ∀ B ∈ P, ∀ x, dynkinProduct a B x 0 = x)
    {l : Filter ι} (B : ι → V →L[ℝ] V →L[ℝ] V) (hB : ∀ i, B i ∈ P)
    (q : ι → V) (hq : Tendsto q l (𝓝 0))
    (hpres : ∀ i, MeasurePreserving (fun x => dynkinProduct a (B i) x (q i)) μ μ)
    {S : Set V} (hS : MeasurableSet S) (hfin : μ S ≠ ⊤) :
    Tendsto (fun i => μ (((fun x => dynkinProduct a (B i) x (q i)) ⁻¹' S) ∆ S))
      l (𝓝 0) := by
…

Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.dynkinProduct