Localizing lower density to a straight subset #
At almost every point of a measurable subset, the complementary restriction is negligible relative to the restricted measure. Straightness turns this relative differentiation statement into preservation of every strictly smaller lower-density bound.
theorem
LeanPool.Besicovitch.le_lowerOneDensity_of_eventually_ball_measure_ge
{s : Set (EuclideanSpace ℝ (Fin 2))}
{x : EuclideanSpace ℝ (Fin 2)}
{beta scale : ℝ}
(hbeta : 0 ≤ beta)
(hscale : 0 < scale)
(hmass :
∀ (r : ℝ),
0 < r →
r < scale → ENNReal.ofReal (2 * beta * r) ≤ (MeasureTheory.Measure.hausdorffMeasure 1) (s ∩ Metric.ball x r))
:
An eventual lower ball-mass bound gives the corresponding lower-density bound.
theorem
LeanPool.Besicovitch.ae_lt_lowerOneDensity_of_subset_of_straight
{e a : Set (EuclideanSpace ℝ (Fin 2))}
(ha : MeasurableSet a)
(hae : a ⊆ e)
(he_fin : (MeasureTheory.Measure.hausdorffMeasure 1) e < ⊤)
(ha_straight : IsStraightMeasure ((MeasureTheory.Measure.hausdorffMeasure 1).restrict a))
{beta gamma : ℝ}
(hbeta : 0 ≤ beta)
(hbeta_gamma : beta < gamma)
(hdensity :
∀ᵐ (x : EuclideanSpace ℝ (Fin 2)) ∂(MeasureTheory.Measure.hausdorffMeasure 1).restrict a, ENNReal.ofReal gamma ≤ lowerOneDensity e x)
:
∀ᵐ (x : EuclideanSpace ℝ (Fin 2)) ∂(MeasureTheory.Measure.hausdorffMeasure 1).restrict a, ENNReal.ofReal beta < lowerOneDensity a x
A straight measurable subset inherits every strictly smaller lower-density threshold almost everywhere from a finite measurable ambient set.