OAI/NumberTheory/DukePrimeDegree/Dynamics/FlowSmoothedL2.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Mean convergence for a real flow without time-one ergodicity

Unit smoothing removes the possible nonconstant time-one invariant vectors. The boundary estimate makes the Hilbert-space limit invariant under every real time, and ergodicity of the entire flow then makes it constant. This is the averaging statement needed on actual ergodic components of a root flow.

  1. def OAI.DukePrimeDegree.realActionTime line 25
  2. lemma OAI.DukePrimeDegree.realActionTime_zero line 27
  3. lemma OAI.DukePrimeDegree.realActionTime_add line 30
  4. theorem OAI.DukePrimeDegree.L2_unit_smoothed_real_action_tendsto_integral line 37

    Source documentation

    Flow ergodicity, with no ergodicity assumption on its time-one map.

    theorem L2_unit_smoothed_real_action_tendsto_integral
    (μ : Measure X) [IsProbabilityMeasure μ] [ErgodicSMul (Multiplicative ℝ) X μ]
    (f : X → ℝ) (C : ℝ) (hC0 : 0 ≤ C) (hC : ∀ x, |f x| ≤ C)
    (hint : ∀ x a b, IntervalIntegrable
      (fun t => f (realActionTime t x)) volume a b)
    (hg : MemLp (unitFlowSmooth realActionTime f) 2 μ) :
    Tendsto (fun N => birkhoffAverage ℝ
      (Lp.compMeasurePreserving (realActionTime 1)
        (measurePreserving_smul (Multiplicative.ofAdd 1) μ)) id N
      (hg.toLp (unitFlowSmooth realActionTime f))) atTop
      (𝓝 (constantL2 μ (∫ x, unitFlowSmooth realActionTime f x ∂μ))) := by
…

    Mentions: OAI.DukePrimeDegree.realActionTime, OAI.DukePrimeDegree.unitFlowSmooth, OAI.DukePrimeDegree.constantL2