PairApproximation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Measurable approximation of the actual pair-height cocycle

theorem OAI.PolycyclicRecognition.pairTransferDefect_ae_L2 line 26
Source documentation
A representative of an L² transfer gives exactly the pointwise defect of the height cocycle, up to the unavoidable null set for a fixed group element.
```
theorem pairTransferDefect_ae_L2
    (π l : G →* Multiplicative W) (hπ : Continuous fun g => (π g).toAdd)
    (v : Lp W 2 μ) (φ : NormalizedPair G Λ → W) (hv : v =ᵐ[μ] φ) (g : G) :
    (pairHeightL2 μ π hπ g + stationaryPullback μ g v - v -
      Lp.const 2 μ (l g).toAdd : Lp W 2 μ) =ᵐ[μ] pairTransferDefect π l φ g := by
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairHeightL2, OAI.PolycyclicRecognition.stationaryPullback, OAI.PolycyclicRecognition.pairTransferDefect

theorem OAI.PolycyclicRecognition.uniform_ofReal_sq_tendsto line 49

Source documentation

Uniformly small nonnegative real errors have uniformly vanishing squared extended-real errors. This handles the supremum over an entire compact set.

theorem uniform_ofReal_sq_tendsto {T : Type*} (f : ℕ → T → ℝ) (Q : Set T)
    (hsmall : ∀ ε : ℝ, 0 < ε →
      ∀ᶠ n in Filter.atTop, ∀ q ∈ Q, f n q ≤ ε) :
    Filter.Tendsto (fun n => ⨆ q ∈ Q, ENNReal.ofReal (f n q) ^ 2)
      Filter.atTop (nhds 0) := by
…

theorem OAI.PolycyclicRecognition.normalizedPair_coboundary_approximation line 68

Source documentation

The precise published reduced-cohomology input produces measurable square-integrable transfers for the actual pair-height cocycle. Their squared defects vanish uniformly on every compact subset of the group.

theorem normalizedPair_coboundary_approximation
    {G W : Type*} [Group G] [MetricSpace G] [ProperSpace G]
    [IsTopologicalGroup G] [IsIsometricSMul G G]
    [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W]
    [SecondCountableTopology W] [MeasurableSpace W] [BorelSpace W] {Λ : ℝ≥0}
    [MeasurableSpace (NormalizedPair G Λ)] [BorelSpace (NormalizedPair G Λ)]
    (μ : Measure (NormalizedPair G Λ)) [IsProbabilityMeasure μ]
    [ErgodicSMul G (NormalizedPair G Λ) μ] [μ.InnerRegularCompactLTTop]
    (hvan : ReducedCohomologyInput G (ZeroMeanL2 (W := W) μ))
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.ReducedCohomologyInput, OAI.PolycyclicRecognition.ZeroMeanL2