RealFlowWindows.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Real stopping times for bounded flow averages

An arbitrary real window differs from its integer part by a boundary interval of length at most one. The estimate is uniform in the initial point, so the same good set works for stopping times selected from a pair.

lemma OAI.DukePrimeDegree.normalized_integral_nearby_length_bound line 20

lemma OAI.DukePrimeDegree.normalized_integral_floor_bound line 70

Source documentation

Any real-time average has uniformly small distance from its integer part once that integer part is positive.

lemma normalized_integral_floor_bound
    (F : ℝ → ℝ) (hint : ∀ a b, IntervalIntegrable F volume a b)
    (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ t, |F t| ≤ C)
    (T : ℝ) (hT : 1 ≤ T) :
    |T⁻¹ * (∫ t in (0 : ℝ)..T, F t) -
        (⌊T⌋₊ : ℝ)⁻¹ * (∫ t in (0 : ℝ)..(⌊T⌋₊ : ℝ), F t)| ≤
      2 * C / (⌊T⌋₊ : ℝ) := by
…

theorem OAI.DukePrimeDegree.real_window_control_of_integer_mean_control line 85

Source documentation

Integer good-set control extends to all sufficiently large real window lengths, retaining the same measurable set.

theorem real_window_control_of_integer_mean_control
    {Y : Type*} (U : ℝ → Y → Y) (f : Y → ℝ)
    (hint : ∀ x a b, IntervalIntegrable (fun t => f (U t x)) volume a b)
    (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ x, |f x| ≤ C)
    (G : Set Y) (q : Y → ℝ) (ε : ℝ) (hε : 0 < ε) (N₀ : ℕ)
    (hgood : ∀ x ∈ G, ∀ N ≥ N₀,
      |(N : ℝ)⁻¹ * (∫ t in (0 : ℝ)..(N : ℝ), f (U t x)) - q x| ≤ ε / 2) :
    ∃ R : ℝ, 1 ≤ R ∧ ∀ x ∈ G, ∀ T ≥ R,
      |T⁻¹ * (∫ t in (0 : ℝ)..T, f (U t x)) - q x| ≤ ε := by
…

theorem OAI.DukePrimeDegree.real_window_control_of_integer_control line 123

Source documentation

The constant-mean specialization retains the original generic-set API.

theorem real_window_control_of_integer_control
    {Y : Type*} (U : ℝ → Y → Y) (f : Y → ℝ)
    (hint : ∀ x a b, IntervalIntegrable (fun t => f (U t x)) volume a b)
    (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ x, |f x| ≤ C)
    (G : Set Y) (c ε : ℝ) (hε : 0 < ε) (N₀ : ℕ)
    (hgood : ∀ x ∈ G, ∀ N ≥ N₀,
      |(N : ℝ)⁻¹ * (∫ t in (0 : ℝ)..(N : ℝ), f (U t x)) - c| ≤ ε / 2) :
    ∃ R : ℝ, 1 ≤ R ∧ ∀ x ∈ G, ∀ T ≥ R,
      |T⁻¹ * (∫ t in (0 : ℝ)..T, f (U t x)) - c| ≤ ε :=
…

theorem OAI.DukePrimeDegree.exists_uniform_real_flow_generic_set line 135