OAI/NumberTheory/DukePrimeDegree/Dynamics/ErgodicAverageMean.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Identifying the constant ergodic average

The constant obtained from the L2 mean ergodic theorem is the integral of the original observable. Integration is represented by pairing with the constant-one vector, so passage to the limit is continuous in L2.

  1. def OAI.DukePrimeDegree.constantL2 line 22

    Source documentation

    Constant observables as actual L2 vectors.

    def constantL2 (μ : Measure X) [IsFiniteMeasure μ] (c : ℝ) : Lp ℝ 2 μ :=
…
  2. lemma OAI.DukePrimeDegree.constantL2_ae line 25
  3. def OAI.DukePrimeDegree.meanL2 line 30

    Source documentation

    Integration is the continuous L2 pairing with the constant one.

    def meanL2 (μ : Measure X) [IsFiniteMeasure μ] : Lp ℝ 2 μ →L[ℝ] ℝ :=
…
  4. lemma OAI.DukePrimeDegree.meanL2_apply line 33
  5. lemma OAI.DukePrimeDegree.meanL2_constant line 41
  6. lemma OAI.DukePrimeDegree.meanL2_koopman line 46
  7. lemma OAI.DukePrimeDegree.meanL2_iterate line 61
  8. lemma OAI.DukePrimeDegree.meanL2_birkhoffAverage line 69
  9. theorem OAI.DukePrimeDegree.L2_orbit_average_tendsto_integral line 80

    Source documentation

    The L2 limit is the original integral, with no generic-point hypothesis.

    theorem L2_orbit_average_tendsto_integral
    (μ : Measure X) [IsProbabilityMeasure μ]
    (T : X → X) (hT : Ergodic T μ) (f : Lp ℝ 2 μ) :
    Tendsto (fun N => birkhoffAverage ℝ (Lp.compMeasurePreserving T hT.toMeasurePreserving)
      id N f) atTop (𝓝 (constantL2 μ (∫ x, f x ∂μ))) := by
…

    Mentions: OAI.DukePrimeDegree.constantL2