LineCounting.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The measurable line-counting lemma used for simultaneous separated directions.

theorem OAI.LipschitzHilbert.line_counting line 20

Source documentation

A single jointly measurable count dominates every finite collection of popular bins, and its tail is exponentially small on every bounded interval. Only finite partial sums of the countable bin family are needed as data.

theorem line_counting {X B : Type*} [MeasurableSpace X] [Countable B]
    (f : B → X × ℝ → ℝ) (hf : ∀ b, Measurable (f b))
    (hbound : ∀ b p, 0 ≤ f b p ∧ f b p ≤ 1)
    {C H θ : ℝ} (hC : 0 < C) (hH : 0 < H) (hθ : 0 < θ)
    (hsum : ∀ s : Finset B, ∀ p, (∑ b ∈ s, f b p) ≤ C) :
    ∃ N : X × ℝ → ℝ≥0∞, Measurable N ∧
      (∀ (p : X × ℝ) (bins : Finset B), (∀ b ∈ bins, ∃ a c : ℝ, a < c ∧ c - a ≤ H ∧ p.2 ∈ Icc a c ∧
        θ * (c - a) ≤ ∫ x in Icc a c, f b (p.1, x)) → (bins.card : ℝ≥0∞) ≤ N p) ∧
      ∀ (p : X) (a b : ℝ), a ≤ b → ∀ lambda : ℝ, 0 ≤ lambda →
        volume.real ({x | ENNReal.ofReal lambda < N (p, x)} ∩ Icc a b) ≤
          96 * (b - a + H) * Real.exp (-θ * lambda / (24 * C)) := by
…