UnitFlowSmoothing.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Bounded observable smoothing for an ergodic real flow

Unit smoothing is measurable, bounded, and preserves the integral. Its discrete averages have an actual L1 limit under flow ergodicity. Together with the maximal estimate this gives fixed large-measure sets that control every sufficiently long integer flow window.

lemma OAI.DukePrimeDegree.continuous_flow_observable line 26
lemma OAI.DukePrimeDegree.measurable_unitFlowSmooth line 31
lemma OAI.DukePrimeDegree.unitFlowSmooth_abs_le line 40
lemma OAI.DukePrimeDegree.memLp_unitFlowSmooth line 47
lemma OAI.DukePrimeDegree.unitFlowSmooth_integral_eq line 52

theorem OAI.DukePrimeDegree.L1_integer_flow_windows_tendsto_integral line 78

Source documentation

The genuine continuous-flow windows converge in L1 at integer lengths. Full-flow ergodicity is the only ergodicity hypothesis.

theorem L1_integer_flow_windows_tendsto_integral
    (μ : Measure X) [IsProbabilityMeasure μ] [ErgodicSMul (Multiplicative ℝ) X μ]
    (f : X →ᵇ ℝ) :
    Tendsto (fun N : ℕ => ∫ x,
      |(N : ℝ)⁻¹ * (∫ t in (0 : ℝ)..(N : ℝ), f (realActionTime t x)) -
        ∫ y, f y ∂μ| ∂μ) atTop (𝓝 0) := by
…

Mentions: OAI.DukePrimeDegree.realActionTime

theorem OAI.DukePrimeDegree.exists_uniform_integer_flow_generic_set line 114

Source documentation

A fixed large-measure set works for all sufficiently large integer flow windows, including a window length selected from a pair of points.

theorem exists_uniform_integer_flow_generic_set
    (μ : Measure X) [IsProbabilityMeasure μ] [ErgodicSMul (Multiplicative ℝ) X μ]
    (f : X →ᵇ ℝ) (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ) :
    ∃ G : Set X, MeasurableSet G ∧ μ Gᶜ ≤ ENNReal.ofReal δ ∧
      ∃ N₀ : ℕ, ∀ x ∈ G, ∀ N ≥ N₀,
        |(N : ℝ)⁻¹ * (∫ t in (0 : ℝ)..(N : ℝ), f (realActionTime t x)) -
          ∫ y, f y ∂μ| ≤ ε := by
…

Mentions: OAI.DukePrimeDegree.realActionTime