GenericMeanOscillation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Comparing the nonconstant means of nearby generic points

A single finite continuous average approximates the invariant mean on the entire good set. Nearby good points therefore have nearby means. This supplies exactly the continuity comparison needed after bounded simultaneous corrections; no continuity of the invariant mean is assumed.

lemma OAI.DukePrimeDegree.continuous_fixed_flow_average line 22
lemma OAI.DukePrimeDegree.invariant_mean_pair_bound line 39

theorem OAI.DukePrimeDegree.eventually_invariant_means_close line 58

Source documentation

Close pairs may vary inside one common generic set. A fixed continuous finite approximation suffices to compare their invariant means, even when those means are not constant.

theorem eventually_invariant_means_close
    {Y I : Type*} [TopologicalSpace Y] {l : Filter I}
    (q F : Y → ℝ) (G : Set Y) (ε η : ℝ) (hη : 0 < η)
    (happrox : ∀ x ∈ G, |q x - F x| ≤ ε)
    (a b : I → Y) (x : Y) (hF : ContinuousAt F x)
    (ha : Tendsto a l (𝓝 x)) (hb : Tendsto b l (𝓝 x))
    (hG : ∀ᶠ i in l, a i ∈ G ∧ b i ∈ G) :
    ∀ᶠ i in l, |q (a i) - q (b i)| ≤ 2 * ε + η := by
…

theorem OAI.DukePrimeDegree.eventually_flow_invariant_means_close line 74

Source documentation

A common integer averaging time supplies the finite continuous approximation used above for genuine flow windows.

theorem eventually_flow_invariant_means_close
    {Y I : Type*} [TopologicalSpace Y] [FirstCountableTopology Y]
    [MeasurableSpace Y] [BorelSpace Y]
    [MulAction (Multiplicative ℝ) Y] [ContinuousSMul (Multiplicative ℝ) Y]
    {l : Filter I} (f : Y →ᵇ ℝ) (q : Y → ℝ) (G : Set Y)
    (ε η : ℝ) (hη : 0 < η) (N₀ : ℕ)
    (hgood : ∀ x ∈ G, ∀ N ≥ N₀,
      |(N : ℝ)⁻¹ * (∫ t in (0 : ℝ)..(N : ℝ), f (realActionTime t x)) - q x| ≤ ε)
    (a b : I → Y) (x : Y) (ha : Tendsto a l (𝓝 x)) (hb : Tendsto b l (𝓝 x))
    (hG : ∀ᶠ i in l, a i ∈ G ∧ b i ∈ G) :
    ∀ᶠ i in l, |q (a i) - q (b i)| ≤ 2 * ε + η := by
…

Mentions: OAI.DukePrimeDegree.realActionTime