StationaryCentered.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The zero-mean Hilbert representation and stationary sublinearity

The closed kernel of integration is invariant under inverse pullback. Ergodicity removes its invariant vectors. This constructs the representation to which the published reduced-cohomology input is applied; the conclusion is the manuscript's averaged sublinear estimate for a fixed measure.

abbrev OAI.PolycyclicRecognition.ZeroMeanL2 line 30
Source documentation
The actual closed zero-mean subspace of L².
```
abbrev ZeroMeanL2 : Submodule ℝ (Lp W 2 μ) := (stationaryL2Mean (W := W) μ).ker
```
Mentions: OAI.PolycyclicRecognition.stationaryL2Mean
theorem OAI.PolycyclicRecognition.stationaryL2Mean_const line 33
Source documentation
Constants have their stated mean on a probability space.
```
theorem stationaryL2Mean_const (w : W) : stationaryL2Mean μ (Lp.const 2 μ w) = w := by
…
```
Mentions: OAI.PolycyclicRecognition.stationaryL2Mean
theorem OAI.PolycyclicRecognition.stationaryPullback_const line 40
Source documentation
Constant functions are fixed by inverse pullback.
```
theorem stationaryPullback_const (g : G) (w : W) :
    stationaryPullback μ g (Lp.const 2 μ w) = Lp.const 2 μ w := by
…
```
Mentions: OAI.PolycyclicRecognition.stationaryPullback
def OAI.PolycyclicRecognition.zeroMeanL2Action line 50
Source documentation
Restrict the pullback representation to the kernel of integration.
```
def zeroMeanL2Action : DistribMulAction G (ZeroMeanL2 (W := W) μ) where
…
```
Mentions: OAI.PolycyclicRecognition.ZeroMeanL2
instance OAI.PolycyclicRecognition.zeroMeanL2Isometric line 62
instance OAI.PolycyclicRecognition.zeroMeanL2SMulComm line 67

theorem OAI.PolycyclicRecognition.zeroMeanL2_no_fixed line 71

Source documentation

Ergodicity removes every invariant vector from the zero-mean subspace.

theorem zeroMeanL2_no_fixed
    {G X W : Type*} [Group G] [MeasurableSpace X] [MulAction G X]
    [MeasurableConstSMul G X] [NormedAddCommGroup W] [NormedSpace ℝ W]
    [CompleteSpace W] [SecondCountableTopology W]
    (μ : Measure X) [IsProbabilityMeasure μ] [ErgodicSMul G X μ]
    (v : ZeroMeanL2 (W := W) μ) (hfix : ∀ g : G, g • v = v) : v = 0 := by
…

Mentions: OAI.PolycyclicRecognition.ZeroMeanL2

def OAI.PolycyclicRecognition.l2MeanSlope line 86
Source documentation
Averaging any L² cocycle gives a genuine height homomorphism.
```
def l2MeanSlope (b : G → Lp W 2 μ) (hb : IsCocycle b) : G →* Multiplicative W where
…
```
Mentions: OAI.PolycyclicRecognition.IsCocycle
def OAI.PolycyclicRecognition.centeredL2Cocycle line 97
Source documentation
Subtracting the actual averaged slope produces a zero-mean cocycle.
```
def centeredL2Cocycle (b : G → Lp W 2 μ) (g : G) : ZeroMeanL2 (W := W) μ :=
…
```
Mentions: OAI.PolycyclicRecognition.ZeroMeanL2
theorem OAI.PolycyclicRecognition.isCocycle_centeredL2 line 102
theorem OAI.PolycyclicRecognition.continuous_centeredL2 line 116

theorem OAI.PolycyclicRecognition.stationary_sublinear line 124

Source documentation

The fixed-measure stationary sublinear estimate, conditional only on the precise reduced-cohomology input for the constructed zero-mean representation. The analytic and algebraic hypotheses are verified on that representation.

theorem stationary_sublinear
    {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