Mattila's Lemma 14.7

This file assembles the ball-bound and good-set machinery into the three statements of Mattila's Lemma 14.7.

Mattila, Lemma 14.7 (1), (2) and (3)

The three statements below are the almost-everywhere statements of Lemma 14.7; A is the set positiveFiniteDensitySet s μ of points where 0 < Θ^s_*(μ, a) ≤ Θ^{*s}(μ, a) < ∞, and "μ almost all points a ∈ A" is expressed by exhibiting a μ-null exceptional set E.

theorem mattila_14_7_1 {n : ℕ} {s : ℝ} (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) (hμ : μ.Regular) : ∃ (E : Set (EuclideanSpace ℝ (Fin n))), μ E = 0 ∧ ∀ a ∈ positiveFiniteDensitySet s μ \ E, ∀ (ν : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))), IsTangentMeasure μ ν a → ∃ (c : ENNReal), 0 < c ∧ c ≠ ⊤ ∧ ∀ x ∈ ν.support, ∀ (r : ℝ), 0 < r → RatioOfDensities s μ a * c * ENNReal.ofReal (r ^ s) ≤ ν (Metric.closedBall x r) ∧ ν (Metric.closedBall x r) ≤ c * ENNReal.ofReal (r ^ s)

Mattila, Lemma 14.7 (1). At μ almost all points a of A = {a | 0 < Θ^s_*(μ, a) ≤ Θ^{*s}(μ, a) < ∞}: for every tangent measure ν ∈ Tan (μ, a) there is a positive (finite) number c such that t c r ^ s ≤ ν (B (x, r)) ≤ c r ^ s for x ∈ spt ν and 0 < r < ∞, where t = t (a) = Θ^s_*(μ, a) / Θ^{*s}(μ, a). The proof needs no sign assumption on the exponent s.

theorem mattila_14_7_2 {n : ℕ} {s : ℝ} (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) (hμ : μ.Regular) (hball : ∃ (E₀ : Set (EuclideanSpace ℝ (Fin n))), μ E₀ = 0 ∧ ∀ z ∈ positiveFiniteDensitySet s μ \ E₀, upperBallSDensity s μ z ≤ dimensionalUpperDensity μ.toOuterMeasure s z) : ∃ (E : Set (EuclideanSpace ℝ (Fin n))), μ E = 0 ∧ ∀ a ∈ positiveFiniteDensitySet s μ \ E, ∀ (ν : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))), IsTangentMeasure μ ν a → ∃ (c : ENNReal), 0 < c ∧ c ≠ ⊤ ∧ (∀ x ∈ ν.support, ∀ (r : ℝ), 0 < r → RatioOfDensities s μ a * c * ENNReal.ofReal (r ^ s) ≤ ν (Metric.closedBall x r) ∧ ν (Metric.closedBall x r) ≤ c * ENNReal.ofReal (r ^ s)) ∧ ∀ (x : EuclideanSpace ℝ (Fin n)) (r : ℝ), 0 < r → ν (Metric.closedBall x r) ≤ c * ENNReal.ofReal (r ^ s)

Mattila, Lemma 14.7 (2). If, in addition, at μ almost all z ∈ A the upper bound limsup_{δ ↓ 0} sup {d (B) ^ (-s) μ (B) : B a closed ball with z ∈ B, d (B) < δ} ≤ Θ^{*s}(μ, z) holds, then at μ almost all a ∈ A every tangent measure ν ∈ Tan (μ, a) satisfies ν (B (x, r)) ≤ c r ^ s for all x ∈ ℝⁿ and r > 0, with the same constant c as in Lemma 14.7 (1).

theorem mattila_14_7_3 {n : ℕ} {s : ℝ} (hsn : s < ↑n) (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) (hμ : μ.Regular) : ∃ (E : Set (EuclideanSpace ℝ (Fin n))), μ E = 0 ∧ ∀ a ∈ positiveFiniteDensitySet s μ \ E, ∃ (e : EuclideanSpace ℝ (Fin n)) (ν : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))), ‖e‖ = 1 ∧ IsTangentMeasure μ ν a ∧ ν.support ⊆ {x : EuclideanSpace ℝ (Fin n) | 0 ≤ inner ℝ x e}

Mattila, Lemma 14.7 (3). If s < n, then at μ almost all a ∈ A there are a unit vector e and a tangent measure ν ∈ Tan (μ, a) whose support is contained in the half-space {x | 0 ≤ x ⬝ e}. The proof runs as follows. Almost every a ∈ A lies in one of the closed sets F = goodSet s p q m μ, on which the measures of all small balls are comparable to ρ ^ s, and is a μ-density point of F. Since s < n, a Fubini argument shows that a definite proportion of every ball centred on F is a hole of F (exists_hole_of_ball_bounds), and a density argument then shows that almost every point of F is an asymptotic touching point: there are points y ∈ F touching holes B (z, d) with d → 0 and dist y a negligible compared with d (exists_touching_points_ae). Blowing μ up at a at scales r with dist y a ≪ r ≪ d turns these holes into balls of radius tending to infinity whose boundaries pass arbitrarily close to the origin; in the limit they exhaust an open half-space, so the resulting tangent measure is supported in the complementary closed half-space (exists_halfSpace_tangentMeasure_of_touching). The proof turned out not to need any positivity assumption on the exponent s, so the hypothesis 0 < s was dropped from the statement, as in parts (1) and (2).

Mattila, Lemma 14.7 (4)

theorem mattila_14_7_4 {n : ℕ} {s d t r₀ : ℝ} (hd : 0 < d) (ht : 0 < t) (hr₀ : 0 < r₀) (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) (hμ : μ.Regular) (hbounds : ∀ y ∈ μ.support, ∀ (ρ : ℝ), 0 < ρ → ρ < r₀ → ENNReal.ofReal (t * d * ρ ^ s) ≤ μ (Metric.closedBall y ρ) ∧ μ (Metric.closedBall y ρ) ≤ ENNReal.ofReal (d * ρ ^ s)) (a : EuclideanSpace ℝ (Fin n)) (ha : a ∈ μ.support) : (∃ (ν : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))), IsTangentMeasure μ ν a) ∧ ∀ (ν : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))), IsTangentMeasure μ ν a → ∃ (c : ENNReal), 0 < c ∧ c ≠ ⊤ ∧ ∀ x ∈ ν.support, ∀ (ρ : ℝ), 0 < ρ → ENNReal.ofReal t * c * ENNReal.ofReal (ρ ^ s) ≤ ν (Metric.closedBall x ρ) ∧ ν (Metric.closedBall x ρ) ≤ c * ENNReal.ofReal (ρ ^ s)

Mattila, Lemma 14.7 (4). If there exist positive numbers d, t and r₀ such that t d r ^ s ≤ μ (B (a, r)) ≤ d r ^ s for all a ∈ spt μ and 0 < r < r₀, then at every point a ∈ spt μ the set Tan (μ, a) of tangent measures is nonempty, and every tangent measure ν ∈ Tan (μ, a) satisfies the conclusion of Lemma 14.7 (1): there is a positive finite constant c with t c r ^ s ≤ ν (B (x, r)) ≤ c r ^ s for all x ∈ spt ν and 0 < r < ∞.