PairSublinear.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Sublinear height errors from the coupled transfers

The finite invariant measure on the inverse section need not be ergodic. The transfers already constructed there suffice for the same word estimate.

theorem OAI.PolycyclicRecognition.isCocycle_pairHeight_sub_hom line 31
Source documentation
Subtracting any continuous height homomorphism preserves the cocycle identity, independently of any ergodicity or averaging assertion.
```
theorem isCocycle_pairHeight_sub_hom
    (π l : G →* Multiplicative W) (hπ : Continuous fun g => (π g).toAdd) :
    IsCocycle (fun g => pairHeightL2 μ π hπ g - Lp.const 2 μ (l g).toAdd) := by
…
```
Mentions: OAI.PolycyclicRecognition.IsCocycle, OAI.PolycyclicRecognition.pairHeightL2

theorem OAI.PolycyclicRecognition.pairHeight_coboundary_of_squared_errors line 47

Source documentation

A compact-uniform squared-error estimate gives an actual small coboundary in the Hilbert space, for a finite invariant measure.

theorem pairHeight_coboundary_of_squared_errors
    (π l : G →* Multiplicative W) (hπ : Continuous fun g => (π g).toAdd)
    (φ : ℕ → NormalizedPair G Λ → W) (hφ : ∀ n, MemLp (φ n) 2 μ)
    (Q : Set G)
    (happrox : Filter.Tendsto (fun n => ⨆ t ∈ Q,
      ∫⁻ p, ‖pairTransferDefect π l (φ n) t p‖ₑ ^ 2 ∂μ) Filter.atTop (nhds 0)) :
    ∀ ε : ℝ, 0 < ε → ∃ v : Lp W 2 μ, ∀ q ∈ Q,
      ‖(pairHeightL2 μ π hπ q - Lp.const 2 μ (l q).toAdd) + q • v - v‖ ≤ ε := by
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairTransferDefect, OAI.PolycyclicRecognition.pairHeightL2

theorem OAI.PolycyclicRecognition.pairHeight_sublinear_of_squared_errors line 85

Source documentation

Compact-uniform transfer errors imply the global sublinear word bound. This applies directly to the finite measure constructed by inverse coupling.

theorem pairHeight_sublinear_of_squared_errors
    (π l : G →* Multiplicative W) (hπ : Continuous fun g => (π g).toAdd)
    (φ : ℕ → NormalizedPair G Λ → W) (hφ : ∀ n, MemLp (φ n) 2 μ)
    (Q : Set G) (length : G → ℝ) (hlen : ∀ g, 0 ≤ length g)
    {a : ℝ} (ha : 0 ≤ a)
    (hword : ∀ g, ∃ w : List G, (∀ q ∈ w, q ∈ Q) ∧ w.prod = g ∧
      (w.length : ℝ) ≤ a * length g + a)
    (happrox : Filter.Tendsto (fun n => ⨆ t ∈ Q,
      ∫⁻ p, ‖pairTransferDefect π l (φ n) t p‖ₑ ^ 2 ∂μ) Filter.atTop (nhds 0)) :
    ∀ ε : ℝ, 0 < ε → ∃ B : ℝ, 0 ≤ B ∧ ∀ g,
      ‖pairHeightL2 μ π hπ g - Lp.const 2 μ (l g).toAdd‖ ≤ ε * length g + B := by
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairTransferDefect, OAI.PolycyclicRecognition.pairHeightL2

theorem OAI.PolycyclicRecognition.pairHeight_sublinear_of_minimizing_paths line 101

Source documentation

For a proper group with minimizing paths, compact-uniform transfer approximation alone supplies metric sublinearity.

theorem pairHeight_sublinear_of_minimizing_paths
    (π l : G →* Multiplicative W) (hπ : Continuous fun g => (π g).toAdd)
    (φ : ℕ → NormalizedPair G Λ → W) (hφ : ∀ n, MemLp (φ n) 2 μ)
    (happrox : ∀ Q : Set G, IsCompact Q →
      Filter.Tendsto (fun n => ⨆ t ∈ Q,
        ∫⁻ p, ‖pairTransferDefect π l (φ n) t p‖ₑ ^ 2 ∂μ) Filter.atTop (nhds 0))
    (hpath : ∀ g : G, ∃ γ : ℝ → G, γ 0 = 1 ∧ γ 1 = g ∧
      ∀ t ∈ Set.Icc (0 : ℝ) 1, ∀ u ∈ Set.Icc (0 : ℝ) 1,
        dist (γ t) (γ u) ≤ dist 1 g * |t - u|) :
    ∀ ε : ℝ, 0 < ε → ∃ B : ℝ, 0 ≤ B ∧ ∀ g,
      ‖pairHeightL2 μ π hπ g - Lp.const 2 μ (l g).toAdd‖ ≤ ε * dist 1 g + B := by
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairTransferDefect, OAI.PolycyclicRecognition.pairHeightL2

theorem OAI.PolycyclicRecognition.inverseCoupling_sublinear line 120

Source documentation

The actual inverse coupling supplies a sublinear inverse height error with exactly the inverse coefficient. No ergodicity of its finite measure and no second reduced-cohomology hypothesis are required.

theorem inverseCoupling_sublinear
    {G W : Type*} [Group G] [MetricSpace G] [ProperSpace G]
    [SecondCountableTopology G] [IsTopologicalGroup G] [IsIsometricSMul G G]
    {Λ : ℝ≥0} [MeasurableSpace G] [BorelSpace G]
    [MeasurableSpace (NormalizedPair G Λ)] [BorelSpace (NormalizedPair G Λ)]
    [NormedAddCommGroup W] [NormedSpace ℝ W] [CompleteSpace W] [SecondCountableTopology W]
    [MeasurableSpace W] [BorelSpace W]
    (m : Measure G) [m.IsHaarMeasure] [m.IsMulRightInvariant]
    (μ : Measure (NormalizedPair G Λ)) [IsProbabilityMeasure μ]
    [SMulInvariantMeasure G (NormalizedPair G Λ) μ]
    (A : W ≃L[ℝ] W) (π l : G →* Multiplicative W)
    (hπ : Continuous fun g => (π g).toAdd) (hl : Continuous fun g => (l g).toAdd)
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair