StationarySlope.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Averaging the stationary height cocycle

The normalized pair space carries a measure-preserving action. Its height evaluation is a cocycle for inverse pullback. We construct that action on the actual space L², and show that integration gives an additive slope. No reduced-cohomology assertion is assumed in this construction.

def OAI.PolycyclicRecognition.stationaryPullback line 32
Source documentation
Inverse pullback is the left representation associated to a left action.
```
def stationaryPullback (g : G) : Lp W 2 μ →+ Lp W 2 μ :=
…
```
theorem OAI.PolycyclicRecognition.stationaryPullback_one line 35
theorem OAI.PolycyclicRecognition.stationaryPullback_mul line 41
def OAI.PolycyclicRecognition.stationaryL2Action line 50
Source documentation
The isometric additive action on the genuine L² space.
```
def stationaryL2Action : DistribMulAction G (Lp W 2 μ) where
…
```
theorem OAI.PolycyclicRecognition.stationaryPullback_const_finite line 61
Source documentation
Constants are invariant for a finite invariant measure, without a probability normalization.
```
theorem stationaryPullback_const_finite [IsFiniteMeasure μ] (g : G) (w : W) :
    stationaryPullback μ g (Lp.const 2 μ w) = Lp.const 2 μ w := by
…
```
Mentions: OAI.PolycyclicRecognition.stationaryPullback
instance OAI.PolycyclicRecognition.stationaryL2Isometric line 69
theorem OAI.PolycyclicRecognition.continuous_stationaryPullback line 82
Source documentation
Strong continuity follows from the actual continuous action on the underlying measure space and density of simple functions in L².
```
theorem continuous_stationaryPullback :
    Continuous (fun z : G × Lp W 2 μ => stationaryPullback μ z.1 z.2) := by
…
```
Mentions: OAI.PolycyclicRecognition.stationaryPullback
theorem OAI.PolycyclicRecognition.isCocycle_toL2 line 96
Source documentation
Pointwise measurable height cocycles give L² cocycles without selecting pointwise representatives of the resulting equivalence classes.
```
theorem isCocycle_toL2 (b : G → X → W) (hb : ∀ g, MemLp (b g) 2 μ)
    (hc : ∀ g h x, b (g * h) x = b g x + b h (g⁻¹ • x)) :
    IsCocycle (fun g => (hb g).toLp (b g)) := by
…
```
Mentions: OAI.PolycyclicRecognition.IsCocycle
instance OAI.PolycyclicRecognition.stationaryL2SMulComm line 113
theorem OAI.PolycyclicRecognition.norm_integral_le_l2 line 119
Source documentation
The averaging operator is bounded by one on a probability space.
```
theorem norm_integral_le_l2 [IsProbabilityMeasure μ] (v : Lp W 2 μ) :
    ‖∫ x, v x ∂μ‖ ≤ ‖v‖ := by
…
```
def OAI.PolycyclicRecognition.stationaryL2Mean line 132
Source documentation
Averaging as an actual bounded linear operator on L².
```
def stationaryL2Mean [IsProbabilityMeasure μ] : Lp W 2 μ →L[ℝ] W :=
…
```
theorem OAI.PolycyclicRecognition.stationaryL2Mean_pullback line 148
Source documentation
The mean is invariant under the pullback representation.
```
theorem stationaryL2Mean_pullback [IsProbabilityMeasure μ] (g : G) (v : Lp W 2 μ) :
    stationaryL2Mean μ (stationaryPullback μ g v) = stationaryL2Mean μ v := by
…
```
Mentions: OAI.PolycyclicRecognition.stationaryL2Mean, OAI.PolycyclicRecognition.stationaryPullback
def OAI.PolycyclicRecognition.stationaryMean line 159
Source documentation
The average is a genuine homomorphism; invariance removes the translated second summand in the cocycle equation.
```
def stationaryMean (b : G → X → W) (hb : ∀ g, Integrable (b g) μ)
    (hc : ∀ g h x, b (g * h) x = b g x + b h (g⁻¹ • x)) :
    G →* Multiplicative W where
…
```

theorem OAI.PolycyclicRecognition.integral_centered_stationaryMean line 180

Source documentation

On a probability space the centered pointwise cocycle has zero mean.

theorem integral_centered_stationaryMean [IsProbabilityMeasure μ]
    (b : G → X → W) (hb : ∀ g, Integrable (b g) μ)
    (hc : ∀ g h x, b (g * h) x = b g x + b h (g⁻¹ • x)) (g : G) :
    (∫ x, b g x - (stationaryMean μ b hb hc g).toAdd ∂μ) = 0 := by
…

Mentions: OAI.PolycyclicRecognition.stationaryMean

theorem OAI.PolycyclicRecognition.stationary_fixed_eq_const line 189

Source documentation

Ergodicity of the action, rather than an assumption about its Hilbert representation, identifies all invariant L² vectors with constants.

theorem stationary_fixed_eq_const
    {G X W : Type*} [Group G] [MeasurableSpace X] [MulAction G X]
    [MeasurableConstSMul G X] [NormedAddCommGroup W] [SecondCountableTopology W]
    (μ : Measure X) [IsProbabilityMeasure μ] [ErgodicSMul G X μ] (v : Lp W 2 μ)
    (hfix : ∀ g : G, stationaryPullback μ g v = v) :
    ∃ c : W, v = Lp.const 2 μ c := by
…

Mentions: OAI.PolycyclicRecognition.stationaryPullback