Documentation

TauCeti.Probability.Ergodic.FixedSpace

Fixed points of a measure-preserving transformation on Lᵖ #

This file relates membership in Mathlib's fixed submodule for the Lᵖ composition isometry to almost-everywhere invariance of representatives. This is the closed subspace onto which the mean ergodic projection in the Koopman route to de Finetti's theorem will project.

It also records the simp lemma coe_compMeasurePreservingₗᵢ, which identifies the map underlying the composition isometry with Mathlib's composition operator MeasureTheory.Lp.compMeasurePreserving, so that statements phrased with the isometry can be rewritten into the form the lemmas about representatives use.

source
def TauCeti.Probability.fixedSpace {Ω : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [MeasurableSpace Ω] [NormedRing 𝕜] [NormedAddCommGroup E] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] {p : ENNReal} {μ : MeasureTheory.Measure Ω} (T : Ω → Ω) (hT : MeasureTheory.MeasurePreserving T μ μ) :
Submodule 𝕜 ↥(MeasureTheory.Lp E p μ)

The submodule of Lᵖ observables fixed by composition with a measure-preserving transformation.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Probability.mem_fixedSpace_iff {Ω : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [MeasurableSpace Ω] [NormedRing 𝕜] [NormedAddCommGroup E] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] {p : ENNReal} {μ : MeasureTheory.Measure Ω} {T : Ω → Ω} (hT : MeasureTheory.MeasurePreserving T μ μ) (g : ↥(MeasureTheory.Lp E p μ)) :
    g ∈ fixedSpace T hT ↔ (MeasureTheory.Lp.compMeasurePreserving T hT) g = g

    Membership in the fixed space means being fixed by the composition operator.

    source
    @[simp]
    theorem TauCeti.Probability.compMeasurePreserving_eq_self_iff {Ω : Type u_1} {E : Type u_3} [MeasurableSpace Ω] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure Ω} {T : Ω → Ω} (hT : MeasureTheory.MeasurePreserving T μ μ) (g : ↥(MeasureTheory.Lp E p μ)) :
    (MeasureTheory.Lp.compMeasurePreserving T hT) g = g ↔ ↑↑g ∘ T =ᵐ[μ] ↑↑g

    Characterization of fixed points of the Lᵖ composition isometry using representatives.

    source
    @[simp]
    theorem TauCeti.Probability.fixedSpace_id {Ω : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [MeasurableSpace Ω] [NormedRing 𝕜] [NormedAddCommGroup E] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] {p : ENNReal} {μ : MeasureTheory.Measure Ω} :
    fixedSpace id ⋯ = ⊤

    The fixed space of the identity transformation is all of Lᵖ.

    source
    theorem TauCeti.Probability.mem_fixedSpace_iterate {Ω : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [MeasurableSpace Ω] [NormedRing 𝕜] [NormedAddCommGroup E] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] {p : ENNReal} {μ : MeasureTheory.Measure Ω} {T : Ω → Ω} (hT : MeasureTheory.MeasurePreserving T μ μ) {g : ↥(MeasureTheory.Lp E p μ)} (hg : g ∈ fixedSpace T hT) (n : ℕ) :
    g ∈ fixedSpace T^[n] ⋯

    Every observable fixed by T is fixed by every iterate of T.

    source
    @[simp]
    theorem TauCeti.Probability.coe_compMeasurePreservingₗᵢ {Ω : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [MeasurableSpace Ω] [NormedRing 𝕜] [NormedAddCommGroup E] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] {p : ENNReal} [Fact (1 ≤ p)] {μ : MeasureTheory.Measure Ω} (T : Ω → Ω) (hT : MeasureTheory.MeasurePreserving T μ μ) :
    ⇑(MeasureTheory.Lp.compMeasurePreservingₗᵢ 𝕜 T hT) = ⇑(MeasureTheory.Lp.compMeasurePreserving T hT)

    The map underlying Mathlib's Lᵖ composition isometry is Mathlib's composition operator MeasureTheory.Lp.compMeasurePreserving. This is the bridge between the statements phrased with the isometry, such as the mean ergodic theorem, and the lemmas about representatives, which are phrased with MeasureTheory.Lp.compMeasurePreserving. Together with Mathlib's simp lemma LinearIsometry.coe_toContinuousLinearMap it also normalizes the continuous linear map the isometry induces.

    source
    theorem TauCeti.Probability.fixedSpace_eq_eqLocus {Ω : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [MeasurableSpace Ω] [NormedRing 𝕜] [NormedAddCommGroup E] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] {p : ENNReal} [Fact (1 ≤ p)] {μ : MeasureTheory.Measure Ω} (T : Ω → Ω) (hT : MeasureTheory.MeasurePreserving T μ μ) :
    fixedSpace T hT = (↑(MeasureTheory.Lp.compMeasurePreservingₗᵢ 𝕜 T hT).toContinuousLinearMap).eqLocus ↑1

    The fixed space is the equalizer of the continuous Lᵖ composition operator and the identity.

    source
    theorem TauCeti.Probability.isClosed_fixedSpace {Ω : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [MeasurableSpace Ω] [NormedRing 𝕜] [NormedAddCommGroup E] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] {p : ENNReal} [Fact (1 ≤ p)] {μ : MeasureTheory.Measure Ω} (T : Ω → Ω) (hT : MeasureTheory.MeasurePreserving T μ μ) :
    IsClosed ↑(fixedSpace T hT)

    The fixed space is closed in Lᵖ.

    source
    instance TauCeti.Probability.fixedSpace.completeSpace {Ω : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [MeasurableSpace Ω] [NormedRing 𝕜] [NormedAddCommGroup E] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] {p : ENNReal} [Fact (1 ≤ p)] {μ : MeasureTheory.Measure Ω} [CompleteSpace ↥(MeasureTheory.Lp E p μ)] (T : Ω → Ω) (hT : MeasureTheory.MeasurePreserving T μ μ) :
    CompleteSpace ↥(fixedSpace T hT)