Elementary lower-density consequences

Strictly exceeding a lower-density level gives the corresponding ball-mass estimate at every sufficiently small positive radius.

theorem LeanPool.Besicovitch.restrict_hausdorffMeasure_ball {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] (s : Set X) (x : X) (r : ℝ) : ((MeasureTheory.Measure.hausdorffMeasure 1).restrict s) (Metric.ball x r) = (MeasureTheory.Measure.hausdorffMeasure 1) (s ∩ Metric.ball x r)

Hausdorff measure restricted to a set evaluates balls by intersection with that set.

theorem LeanPool.Besicovitch.lowerOneDensity_eventually_ball_measure_gt {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] {s : Set X} {x : X} {β : ℝ} (hβ : 0 ≤ β) (h : ENNReal.ofReal β < lowerOneDensity s x) : ∃ (scale : ℝ), 0 < scale ∧ ∀ (r : ℝ), 0 < r → r < scale → ENNReal.ofReal (2 * β * r) < (MeasureTheory.Measure.hausdorffMeasure 1) (s ∩ Metric.ball x r)

A strict lower-density bound holds as a mass bound on every sufficiently small ball.