LeafMaximal.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A covering estimate for leafwise bad sets

The relative maximal estimate used in EKL (2006), Section 4.3, rests on the one-dimensional Besicovitch covering theorem. We first prove the estimate for an arbitrary bounded family of witnessing radii. The measure on the line is arbitrary; no doubling property is used.

theorem OAI.DukePrimeDegree.real_ball_covering_estimate line 21

theorem OAI.DukePrimeDegree.exists_real_relative_maximal_constant line 77

Source documentation

A single finite constant controls every bounded-radius relative maximal set on a real leaf, uniformly in the leaf measure.

theorem exists_real_relative_maximal_constant :
    ∃ N : ℕ, ∀ (ν : Measure ℝ) (E : Set ℝ), MeasurableSet E →
      ∀ (c : ℝ≥0∞) (R : ℝ),
      c * ν {x | ∃ r : ℝ, 0 < r ∧ r ≤ R ∧
        c * ν (closedBall x r) ≤ ν (E ∩ closedBall x r)} ≤ (N : ℝ≥0∞) * ν E := by
…

theorem OAI.DukePrimeDegree.exists_real_relative_maximal_constant_all_radii line 94

Source documentation

The same constant controls all radii. Continuity from below holds for arbitrary increasing sets, so no measurability of the supremum over the radius parameter has to be assumed.

theorem exists_real_relative_maximal_constant_all_radii :
    ∃ N : ℕ, ∀ (ν : Measure ℝ) (E : Set ℝ), MeasurableSet E →
      ∀ c : ℝ≥0∞,
      c * ν {x | ∃ r : ℝ, 0 < r ∧
        c * ν (closedBall x r) ≤ ν (E ∩ closedBall x r)} ≤ (N : ℝ≥0∞) * ν E := by
…