FlowWindowAverages.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Unit smoothing and continuous orbit windows

Discrete averages of a unit-smoothed observable are exactly continuous flow averages at integer lengths. Shifting the initial point changes only two boundary intervals; their contribution is uniformly bounded. Neither statement assumes that a time-one map is ergodic.

def OAI.DukePrimeDegree.unitFlowSmooth line 23
lemma OAI.DukePrimeDegree.flow_nat_iterate line 26
Distinct definitions of this name: OAI/NumberTheory/DukePrimeDegree/Dynamics/FlowOccupation.lean:102 (different declaration text). Qualify references as OAI.DukePrimeDegree.flow_nat_iterate@path.
lemma OAI.DukePrimeDegree.unitFlowSmooth_nat line 36

theorem OAI.DukePrimeDegree.birkhoffAverage_unitFlowSmooth line 47

Source documentation

Integer discrete averages of the smoothed observable are literal continuous-time averages of the original observable.

theorem birkhoffAverage_unitFlowSmooth
    (U : ℝ → X → X) (f : X → ℝ)
    (hzero : ∀ x, U 0 x = x)
    (hadd : ∀ s t x, U (s + t) x = U s (U t x))
    (hint : ∀ x a b, IntervalIntegrable (fun t => f (U t x)) volume a b)
    (N : ℕ) (x : X) :
    birkhoffAverage ℝ (U 1) (unitFlowSmooth U f) N x =
      (N : ℝ)⁻¹ * ∫ t in (0 : ℝ)..(N : ℝ), f (U t x) := by
…

Mentions: OAI.DukePrimeDegree.unitFlowSmooth

theorem OAI.DukePrimeDegree.integral_window_shift_bound line 66

Source documentation

A translated window differs by two boundary intervals of the translation length, regardless of the total window length.

theorem integral_window_shift_bound (F : ℝ → ℝ)
    (hint : ∀ a b, IntervalIntegrable F volume a b)
    (C : ℝ) (hC : ∀ t, |F t| ≤ C) (s L : ℝ) :
    |(∫ t in s..s + L, F t) - ∫ t in (0 : ℝ)..L, F t| ≤ 2 * C * |s| := by
…

theorem OAI.DukePrimeDegree.birkhoffAverage_unitFlowSmooth_shift_bound line 89

Source documentation

Invariance of the eventual average is under every real flow time, not just under its integer subgroup.

theorem birkhoffAverage_unitFlowSmooth_shift_bound
    (U : ℝ → X → X) (f : X → ℝ)
    (hzero : ∀ x, U 0 x = x)
    (hadd : ∀ s t x, U (s + t) x = U s (U t x))
    (hint : ∀ x a b, IntervalIntegrable (fun t => f (U t x)) volume a b)
    (C : ℝ) (hC : ∀ x, |f x| ≤ C) (N : ℕ) (s : ℝ) (x : X) :
    |birkhoffAverage ℝ (U 1) (unitFlowSmooth U f) N (U s x) -
        birkhoffAverage ℝ (U 1) (unitFlowSmooth U f) N x| ≤
      (N : ℝ)⁻¹ * (2 * C * |s|) := by
…

Mentions: OAI.DukePrimeDegree.unitFlowSmooth