StationaryApproximation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Compact-uniform stationary coboundary approximations

The Cornulier–Tessera reduced-cohomology theorem gives compact-uniform coboundary approximation vectors for the zero-mean Hilbert representation.

theorem OAI.PolycyclicRecognition.stationary_coboundary_approximation line 23

Source documentation

The centered stationary cocycle admits actual ambient L² approximation vectors, with its mean homomorphism subtracted explicitly.

theorem stationary_coboundary_approximation
    {G X W : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [R1Space X]
    [MulAction G X] [ContinuousSMul G X]
    [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W]
    [SecondCountableTopology W]
    (μ : Measure X) [IsProbabilityMeasure μ] [ErgodicSMul G X μ]
    [μ.InnerRegularCompactLTTop]
    (hvan : ReducedCohomologyInput G (ZeroMeanL2 (W := W) μ))
…

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

theorem OAI.PolycyclicRecognition.coboundary_approximation_sequence line 55

Source documentation

On a proper metric group, compact-uniform approximations can be chosen as one sequence using the integer-radius compact exhaustion.

theorem coboundary_approximation_sequence
    {G E : Type*} [Group G] [MetricSpace G] [ProperSpace G]
    [NormedAddCommGroup E] [DistribMulAction G E]
    (b : G → E)
    (happrox : ∀ Q : Set G, IsCompact Q → ∀ ε : ℝ, 0 < ε →
      ∃ φ : E, ∀ q ∈ Q, ‖b q + q • φ - φ‖ ≤ ε) :
    ∃ φ : ℕ → E, ∀ Q : Set G, IsCompact Q → ∀ ε : ℝ, 0 < ε →
      ∀ᶠ n in Filter.atTop, ∀ q ∈ Q, ‖b q + q • φ n - φ n‖ ≤ ε := by
…

theorem OAI.PolycyclicRecognition.stationary_coboundary_approximation_sequence line 78

Source documentation

One sequence of ambient approximation vectors works on every compact set for the stationary cocycle and its actual mean slope.

theorem stationary_coboundary_approximation_sequence
    {G X W : Type*} [Group G] [MetricSpace G] [ProperSpace G] [IsTopologicalGroup G]
    [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [R1Space X]
    [MulAction G X] [ContinuousSMul G X]
    [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W]
    [SecondCountableTopology W]
    (μ : Measure X) [IsProbabilityMeasure μ] [ErgodicSMul G X μ]
    [μ.InnerRegularCompactLTTop]
    (hvan : ReducedCohomologyInput G (ZeroMeanL2 (W := W) μ))
…

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

theorem OAI.PolycyclicRecognition.lintegral_enorm_sq_L2 line 111

Source documentation

The squared extended norm integral of an L² vector is its squared norm.

theorem lintegral_enorm_sq_L2 {X W : Type*} [MeasurableSpace X]
    [NormedAddCommGroup W] (μ : Measure X) (f : Lp W 2 μ) :
    ∫⁻ x, ‖f x‖ₑ ^ 2 ∂μ = ENNReal.ofReal ‖f‖ ^ 2 := by
…