Documentation

TauCeti.Probability.Ergodic.MeanErgodic

Mean ergodic projection for measure-preserving maps #

This file defines the orthogonal projection from vector-valued L² onto the fixed space of the composition operator associated to a measure-preserving endomorphism. It characterizes the projection by membership, fixed points, its range, and the orthogonal error.

The main theorem, birkhoffAverage_tendsto_metProjection, says that the Birkhoff averages of the composition operator converge in L² to this projection. It specializes Mathlib's von Neumann mean ergodic theorem ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection to the L² composition isometry.

source
noncomputable def TauCeti.Probability.metProjection {Ω : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [MeasurableSpace Ω] [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {μ : MeasureTheory.Measure Ω} (T : Ω → Ω) (hT : MeasureTheory.MeasurePreserving T μ μ) :
↥(MeasureTheory.Lp E 2 μ) →L[𝕜] ↥(MeasureTheory.Lp E 2 μ)

The mean-ergodic projection onto the L² observables fixed by composition with T.

Equations
Instances For
    source
    theorem TauCeti.Probability.metProjection_mem_fixedSpace {Ω : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [MeasurableSpace Ω] [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {μ : MeasureTheory.Measure Ω} (T : Ω → Ω) (hT : MeasureTheory.MeasurePreserving T μ μ) (g : ↥(MeasureTheory.Lp E 2 μ)) :
    (metProjection T hT) g ∈ fixedSpace T hT

    The mean-ergodic projection takes values in the fixed space.

    source
    @[simp]
    theorem TauCeti.Probability.metProjection_eq_self_iff {Ω : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [MeasurableSpace Ω] [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {μ : MeasureTheory.Measure Ω} (T : Ω → Ω) (hT : MeasureTheory.MeasurePreserving T μ μ) (g : ↥(MeasureTheory.Lp E 2 μ)) :
    (metProjection T hT) g = g ↔ g ∈ fixedSpace T hT

    The mean-ergodic projection fixes exactly the invariant L² observables.

    source
    @[simp]
    theorem TauCeti.Probability.range_metProjection {Ω : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [MeasurableSpace Ω] [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {μ : MeasureTheory.Measure Ω} (T : Ω → Ω) (hT : MeasureTheory.MeasurePreserving T μ μ) :
    (↑(metProjection T hT)).range = fixedSpace T hT

    The range of the mean-ergodic projection is the fixed space.

    source
    @[simp]
    theorem TauCeti.Probability.sub_metProjection_mem_orthogonal {Ω : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [MeasurableSpace Ω] [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {μ : MeasureTheory.Measure Ω} (T : Ω → Ω) (hT : MeasureTheory.MeasurePreserving T μ μ) (g : ↥(MeasureTheory.Lp E 2 μ)) :
    g - (metProjection T hT) g ∈ (fixedSpace T hT)ᗮ

    The error after mean-ergodic projection is orthogonal to the fixed space.

    source
    @[simp]
    theorem TauCeti.Probability.metProjection_id {Ω : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [MeasurableSpace Ω] [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {μ : MeasureTheory.Measure Ω} :
    metProjection id ⋯ = ContinuousLinearMap.id 𝕜 ↥(MeasureTheory.Lp E 2 μ)

    The mean-ergodic projection for the identity transformation is the identity operator.

    source
    theorem TauCeti.Probability.birkhoffAverage_tendsto_metProjection {Ω : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [MeasurableSpace Ω] [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {μ : MeasureTheory.Measure Ω} (T : Ω → Ω) (hT : MeasureTheory.MeasurePreserving T μ μ) (g : ↥(MeasureTheory.Lp E 2 μ)) :
    Filter.Tendsto (fun (x : ℕ) => birkhoffAverage 𝕜 (⇑(MeasureTheory.Lp.compMeasurePreservingₗᵢ 𝕜 T hT).toContinuousLinearMap) id x g) Filter.atTop (nhds ((metProjection T hT) g))

    The Birkhoff averages of the L² composition operator converge to the mean-ergodic projection onto its fixed space.