Good sets for Mattila's Lemma 14.7

This file constructs sets on which ball measures are uniformly comparable and proves the approximation results used in Lemma 14.7.

Points with uniformly comparable ball measures

def goodSet {n : ℕ} (s p q : ℝ) (m : ℕ) (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) : Set (EuclideanSpace ℝ (Fin n))

goodSet s p q m μ is the set of points z such that p ρ ^ s ≤ μ (B (z, ρ)) ≤ q ρ ^ s for every radius 0 < ρ < 1 / (m + 1).

Equations

• One or more equations did not get rendered due to their size.

theorem goodSet_subset {n : ℕ} {s p q p' q' : ℝ} {m : ℕ} {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))} (hp : p' ≤ p) (hq : q ≤ q') : goodSet s p q m μ ⊆ goodSet s p' q' m μ

Enlarging the admissible range [p, q] enlarges goodSet.

theorem goodSet_mono_nat {n : ℕ} {s p q : ℝ} {m m' : ℕ} {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))} (hm : m ≤ m') : goodSet s p q m μ ⊆ goodSet s p q m' μ

Passing to a smaller range of radii enlarges goodSet.

theorem isClosed_goodSet {n : ℕ} (s p q : ℝ) (m : ℕ) (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) : IsClosed (goodSet s p q m μ)

The sets goodSet s p q m μ are closed, hence Borel.

theorem exists_goodSet_mem {n : ℕ} {s : ℝ} {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))} {a : EuclideanSpace ℝ (Fin n)} (ha : a ∈ positiveFiniteDensitySet s μ) {θ : ℝ} (hθ0 : 0 < θ) (hθ : ENNReal.ofReal θ < RatioOfDensities s μ a) : ∃ (p : ℚ) (q : ℚ) (m : ℕ), 0 < ↑p ∧ 0 < ↑q ∧ θ * ↑q ≤ ↑p ∧ dimensionalUpperDensity μ.toOuterMeasure s a * ENNReal.ofReal (2 ^ s) < ENNReal.ofReal ↑q ∧ a ∈ goodSet s (↑p) (↑q) m μ

Every point of A at which the density ratio exceeds θ lies in one of the sets goodSet s p q m μ with θ q ≤ p.

Points all of whose small balls are controlled

def goodBallSet {n : ℕ} (s q : ℝ) (m : ℕ) (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) : Set (EuclideanSpace ℝ (Fin n))

goodBallSet s q m μ is the set of points z such that every closed ball of radius 0 < w < 1 / (m + 1) containing z has measure at most q w ^ s.

Equations

• One or more equations did not get rendered due to their size.

theorem goodBallSet_subset {n : ℕ} {s q q' : ℝ} {m : ℕ} {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))} (hq : q ≤ q') : goodBallSet s q m μ ⊆ goodBallSet s q' m μ

theorem goodBallSet_mono_nat {n : ℕ} {s q : ℝ} {m m' : ℕ} {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))} (hm : m ≤ m') : goodBallSet s q m μ ⊆ goodBallSet s q m' μ

theorem isClosed_goodBallSet {n : ℕ} (s q : ℝ) (m : ℕ) (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) : IsClosed (goodBallSet s q m μ)

theorem exists_goodBallSet_mem {n : ℕ} {s q : ℝ} {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))} {a : EuclideanSpace ℝ (Fin n)} (hq : 0 < q) (hball : upperBallSDensity s μ a ≤ dimensionalUpperDensity μ.toOuterMeasure s a) (hqsup : dimensionalUpperDensity μ.toOuterMeasure s a * ENNReal.ofReal (2 ^ s) < ENNReal.ofReal q) : ∃ (m : ℕ), a ∈ goodBallSet s q m μ

Under the ball-density hypothesis of Lemma 14.7 (2), a point whose upper density is small compared with q lies in one of the sets goodBallSet s q m μ.

The density theorem in the form required by the reduction step

theorem exists_null_of_not_density_point {n : ℕ} (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) (hμ : μ.Regular) {B : Set (EuclideanSpace ℝ (Fin n))} (hB : MeasurableSet B) : ∃ (N : Set (EuclideanSpace ℝ (Fin n))), μ N = 0 ∧ ∀ a ∈ B \ N, ∀ (γ : ENNReal), 0 < γ → ∀ᶠ (ρ : ℝ) in nhdsWithin 0 (Set.Ioi 0), μ (Metric.closedBall a ρ \ B) ≤ γ * μ (Metric.closedBall a ρ)

Besicovitch density theorem for a Radon measure, in the form used in Mattila's proof of Lemma 14.7 (1): outside a μ-null set, every point of a Borel set B is a density point of B, in the sense that the portion of a small ball around it which misses B is an arbitrarily small fraction of the ball.

Passing to the limit in the constants

theorem exists_uniform_constant_of_tendsto {n : ℕ} {s θ₀ : ℝ} {t : ENNReal} {θ : ℕ → ℝ} {ν : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))} (hν : ν.Regular) (hν0 : ν ≠ 0) (hθ₀ : 0 < θ₀) (hθlb : ∀ (k : ℕ), θ₀ ≤ θ k) (hθ : Filter.Tendsto (fun (k : ℕ) => ENNReal.ofReal (θ k)) Filter.atTop (nhds t)) (h : ∀ (k : ℕ), ∃ (c : ENNReal), 0 < c ∧ c ≠ ⊤ ∧ ∀ x ∈ ν.support, ∀ (ρ : ℝ), 0 < ρ → ENNReal.ofReal (θ k) * c * ENNReal.ofReal (ρ ^ s) ≤ ν (Metric.closedBall x ρ) ∧ ν (Metric.closedBall x ρ) ≤ c * ENNReal.ofReal (ρ ^ s)) : ∃ (c : ENNReal), 0 < c ∧ c ≠ ⊤ ∧ ∀ x ∈ ν.support, ∀ (ρ : ℝ), 0 < ρ → t * c * ENNReal.ofReal (ρ ^ s) ≤ ν (Metric.closedBall x ρ) ∧ ν (Metric.closedBall x ρ) ≤ c * ENNReal.ofReal (ρ ^ s)

If the two-sided ball estimate holds with constants θ k tending to t, then it holds with the constant t itself.

theorem exists_uniform_constant_of_tendsto_ball {n : ℕ} {s θ₀ : ℝ} {t : ENNReal} {θ : ℕ → ℝ} {ν : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))} (hν : ν.Regular) (hν0 : ν ≠ 0) (hθ₀ : 0 < θ₀) (hθlb : ∀ (k : ℕ), θ₀ ≤ θ k) (hθ : Filter.Tendsto (fun (k : ℕ) => ENNReal.ofReal (θ k)) Filter.atTop (nhds t)) (h : ∀ (k : ℕ), ∃ (c : ENNReal), 0 < c ∧ c ≠ ⊤ ∧ (∀ x ∈ ν.support, ∀ (ρ : ℝ), 0 < ρ → ENNReal.ofReal (θ k) * c * ENNReal.ofReal (ρ ^ s) ≤ ν (Metric.closedBall x ρ)) ∧ ∀ (x : EuclideanSpace ℝ (Fin n)) (ρ : ℝ), 0 < ρ → ν (Metric.closedBall x ρ) ≤ c * ENNReal.ofReal (ρ ^ s)) : ∃ (c : ENNReal), 0 < c ∧ c ≠ ⊤ ∧ (∀ x ∈ ν.support, ∀ (ρ : ℝ), 0 < ρ → t * c * ENNReal.ofReal (ρ ^ s) ≤ ν (Metric.closedBall x ρ)) ∧ ∀ (x : EuclideanSpace ℝ (Fin n)) (ρ : ℝ), 0 < ρ → ν (Metric.closedBall x ρ) ≤ c * ENNReal.ofReal (ρ ^ s)

The analogue of exists_uniform_constant_of_tendsto for the situation of Lemma 14.7 (2), where the upper bound holds for balls with arbitrary centres.

def farFromTouching {n : ℕ} (F : Set (EuclideanSpace ℝ (Fin n))) (ε d₀ : ℝ) : Set (EuclideanSpace ℝ (Fin n))

The set of points a ∈ F which stay at distance at least ε d from every touching point of a hole of F of size d ≤ d₀.

Equations

• One or more equations did not get rendered due to their size.

theorem isClosed_farFromTouching {n : ℕ} {F : Set (EuclideanSpace ℝ (Fin n))} (hF : IsClosed F) (ε d₀ : ℝ) : IsClosed (farFromTouching F ε d₀)

theorem measure_farFromTouching_eq_zero {n : ℕ} {s p q r₀ ε d₀ : ℝ} (hsn : s < ↑n) (hp : 0 < p) (hq : 0 < q) (hr₀ : 0 < r₀) (hε : 0 < ε) (hε1 : ε ≤ 1) (hd₀ : 0 < d₀) (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) (hμ : μ.Regular) {F : Set (EuclideanSpace ℝ (Fin n))} (hFclosed : IsClosed F) (hupper : ∀ y ∈ F, ∀ (ρ : ℝ), 0 < ρ → ρ < r₀ → μ (Metric.closedBall y ρ) ≤ ENNReal.ofReal (q * ρ ^ s)) (hlower : ∀ y ∈ F, ∀ (ρ : ℝ), 0 < ρ → ρ < r₀ → ENNReal.ofReal (p * ρ ^ s) ≤ μ (Metric.closedBall y ρ)) : μ (farFromTouching F ε d₀) = 0

Almost no point of F is uniformly far from all touching points.

theorem exists_touching_points_ae {n : ℕ} {s p q r₀ : ℝ} (hsn : s < ↑n) (hp : 0 < p) (hq : 0 < q) (hr₀ : 0 < r₀) (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) (hμ : μ.Regular) {F : Set (EuclideanSpace ℝ (Fin n))} (hFclosed : IsClosed F) (hupper : ∀ y ∈ F, ∀ (ρ : ℝ), 0 < ρ → ρ < r₀ → μ (Metric.closedBall y ρ) ≤ ENNReal.ofReal (q * ρ ^ s)) (hlower : ∀ y ∈ F, ∀ (ρ : ℝ), 0 < ρ → ρ < r₀ → ENNReal.ofReal (p * ρ ^ s) ≤ μ (Metric.closedBall y ρ)) : ∃ (N : Set (EuclideanSpace ℝ (Fin n))), μ N = 0 ∧ ∀ a ∈ F \ N, ∀ (ε d₀ : ℝ), 0 < ε → 0 < d₀ → ∃ (y : EuclideanSpace ℝ (Fin n)) (z : EuclideanSpace ℝ (Fin n)), y ∈ F ∧ dist z y = Metric.infDist z F ∧ 0 < Metric.infDist z F ∧ Metric.infDist z F ≤ d₀ ∧ dist y a < ε * Metric.infDist z F

At almost every point of F there are touching points of relatively large holes. If the balls centred on the closed set F have measure comparable to ρ ^ s with s < n, then outside a μ-null set every a ∈ F has, for every ε > 0 and every d₀ > 0, a touching point y ∈ F of a hole B (z, d) with 0 < d ≤ d₀ and dist y a < ε d.

theorem mem_support_of_ball_lower_bound {n : ℕ} {s p r₀ : ℝ} (hp : 0 < p) (hr₀ : 0 < r₀) {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))} {a : EuclideanSpace ℝ (Fin n)} (hlower : ∀ (ρ : ℝ), 0 < ρ → ρ < r₀ → ENNReal.ofReal (p * ρ ^ s) ≤ μ (Metric.closedBall a ρ)) : a ∈ μ.support

A point whose balls have positive measure lies in the support.

theorem limsup_ball_ratio_lt_top_of_ball_bounds_at {n : ℕ} {s p q r₀ : ℝ} (hp : 0 < p) (hq : 0 < q) (hr₀ : 0 < r₀) {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))} {a : EuclideanSpace ℝ (Fin n)} (hupper : ∀ (ρ : ℝ), 0 < ρ → ρ < r₀ → μ (Metric.closedBall a ρ) ≤ ENNReal.ofReal (q * ρ ^ s)) (hlower : ∀ (ρ : ℝ), 0 < ρ → ρ < r₀ → ENNReal.ofReal (p * ρ ^ s) ≤ μ (Metric.closedBall a ρ)) : Filter.limsup (fun (ρ : ℝ) => μ (Metric.ball a (2 * ρ)) / μ (Metric.ball a ρ)) (nhdsWithin 0 (Set.Ioi 0)) < ⊤

Two-sided ball bounds at a single point a already give Mattila's assumption 14.3 (1) at a.

theorem exists_halfSpace_tangentMeasure_of_touching {n : ℕ} {s p q r₀ : ℝ} (hp : 0 < p) (hq : 0 < q) (hr₀ : 0 < r₀) (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) (hμ : μ.Regular) {F : Set (EuclideanSpace ℝ (Fin n))} {a : EuclideanSpace ℝ (Fin n)} (haF : a ∈ F) (hupper : ∀ y ∈ F, ∀ (ρ : ℝ), 0 < ρ → ρ < r₀ → μ (Metric.closedBall y ρ) ≤ ENNReal.ofReal (q * ρ ^ s)) (hlower : ∀ y ∈ F, ∀ (ρ : ℝ), 0 < ρ → ρ < r₀ → ENNReal.ofReal (p * ρ ^ s) ≤ μ (Metric.closedBall y ρ)) (hdens : ∀ (γ : ENNReal), 0 < γ → ∀ᶠ (ρ : ℝ) in nhdsWithin 0 (Set.Ioi 0), μ (Metric.closedBall a ρ \ F) ≤ γ * μ (Metric.closedBall a ρ)) (htouch : ∀ (ε d₀ : ℝ), 0 < ε → 0 < d₀ → ∃ (y : EuclideanSpace ℝ (Fin n)) (z : EuclideanSpace ℝ (Fin n)), y ∈ F ∧ dist z y = Metric.infDist z F ∧ 0 < Metric.infDist z F ∧ Metric.infDist z F ≤ d₀ ∧ dist y a < ε * Metric.infDist z F) : ∃ (e : EuclideanSpace ℝ (Fin n)) (ν : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))), ‖e‖ = 1 ∧ IsTangentMeasure μ ν a ∧ ν.support ⊆ {x : EuclideanSpace ℝ (Fin n) | 0 ≤ inner ℝ x e}

Half-space tangent measures at asymptotic touching points. If a ∈ F is a density point of F, the balls centred on F carry measure comparable to ρ ^ s, and a is an asymptotic touching point of holes of F, then μ has a tangent measure at a whose support lies in a closed half-space.