FlowMaximal.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Maximal occupation control for long flow intervals

The discrete Hopf inequality, applied to one-unit occupation, controls every real interval of length at least one. This is sufficient for the large logarithmic time windows in EKL (2006), Lemmas 4.5 and 4.6.

theorem OAI.DukePrimeDegree.exists_flow_average_good_set line 19
lemma OAI.DukePrimeDegree.flow_occupation_eq_time_measure line 51

theorem OAI.DukePrimeDegree.exists_flow_return_good_set line 70

Source documentation

Every long interval has a uniformly small fraction of bad visits outside one set with the explicit maximal-inequality bound.

theorem exists_flow_return_good_set
    {Y : Type*} [MeasurableSpace Y] (μ : Measure Y) [IsFiniteMeasure μ]
    {Φ : ℝ → Y → Y} (hΦ : Measurable (fun p : Y × ℝ => Φ p.2 p.1))
    (hzero : ∀ x, Φ 0 x = x) (hadd : ∀ s t x, Φ (s + t) x = Φ s (Φ t x))
    (hpres : ∀ t, MeasurePreserving (Φ t) μ μ)
    {E : Set Y} (hE : MeasurableSet E) (c : ℝ) (hc : 0 < c) :
    ∃ G : Set Y, MeasurableSet G ∧ μ Gᶜ ≤ ENNReal.ofReal (2 * μ.real E / c) ∧
      ∀ x ∈ G, ∀ T : ℝ, 1 ≤ T →
        volume.real (Ioc 0 T ∩ {t | Φ t x ∈ E}) ≤ c * T := by
…