OAI/NumberTheory/DukePrimeDegree/Geometry/RealLeafDensity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Linear lower bounds at typical centers of real leaf measures

Differentiation of Lebesgue measure relative to an arbitrary locally finite real measure bounds their small-ball ratio at almost every center. This supplies the dimension-one bound for actual root information.

  1. theorem OAI.DukePrimeDegree.ae_real_ball_linear_lower_bound line 22

    Source documentation

    A locally finite measure has at least linear mass in small balls around almost every one of its own typical points.

    theorem ae_real_ball_linear_lower_bound (ν : Measure ℝ) [IsLocallyFiniteMeasure ν] :
    ∀ᵐ x ∂ν, ∃ C : ℝ≥0∞, C ≠ ∞ ∧
      ∀ᶠ r : ℝ in 𝓝[>] 0, ENNReal.ofReal r ≤ C * ν (ball x r) := by
…