Uniform lower-density sets #
The set uniformDensitySet μ A γ m consists of the points of A where the lower ball-mass
bound at level γ holds at every positive rational radius below 1 / (m + 1).
theorem
LeanPool.Besicovitch.measurable_measure_ball
(mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2)))
[MeasureTheory.SFinite mu]
(r : ℝ)
:
Measurable fun (x : EuclideanSpace ℝ (Fin 2)) => mu (Metric.ball x r)
Ball mass is a measurable function of the center for an s-finite measure on the plane.
def
LeanPool.Besicovitch.uniformDensitySet
(mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2)))
(A : Set (EuclideanSpace ℝ (Fin 2)))
(γ : ℝ)
(m : ℕ)
:
Set (EuclideanSpace ℝ (Fin 2))
Points with a uniform rational-radius lower mass bound.
Equations
Instances For
theorem
LeanPool.Besicovitch.measurableSet_uniformDensitySet
(mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2)))
[MeasureTheory.SFinite mu]
{A : Set (EuclideanSpace ℝ (Fin 2))}
(hA : MeasurableSet A)
(γ : ℝ)
(m : ℕ)
:
MeasurableSet (uniformDensitySet mu A γ m)
Uniform density sets are measurable.
theorem
LeanPool.Besicovitch.exists_mem_uniformDensitySet_of_lt_lowerOneDensity
{A : Set (EuclideanSpace ℝ (Fin 2))}
{x : EuclideanSpace ℝ (Fin 2)}
{γ : ℝ}
(hx : x ∈ A)
(hγ : 0 ≤ γ)
(hdensity : ENNReal.ofReal γ < lowerOneDensity A x)
:
∃ (m : ℕ), x ∈ uniformDensitySet ((MeasureTheory.Measure.hausdorffMeasure 1).restrict A) A γ m
A strict lower-density bound places a point in some uniform density set.
theorem
LeanPool.Besicovitch.uniformDensitySet_ball_measure_gt
{mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))}
{A : Set (EuclideanSpace ℝ (Fin 2))}
{β γ : ℝ}
{m : ℕ}
{x : EuclideanSpace ℝ (Fin 2)}
(hβ : 0 ≤ β)
(hβγ : β < γ)
(hx : x ∈ uniformDensitySet mu A γ m)
{r : ℝ}
(hr : 0 < r)
(hr_small : r < 1 / (↑m + 1))
:
Membership at level γ gives strict ball bounds at every lower nonnegative level.