Consequences of Mattila's condition 14.3

This file derives doubling and compactness consequences from the small-scale hypothesis in Mattila's condition 14.3.

Consequences of the doubling assumption 14.3 (1)

theorem exists_doubling_constant {n : ℕ} {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))} (hμ : μ.Regular) {a : EuclideanSpace ℝ (Fin n)} (ha : a ∈ μ.support) (hdoub : Filter.limsup (fun (ρ : ℝ) => μ (Metric.ball a (2 * ρ)) / μ (Metric.ball a ρ)) (nhdsWithin 0 (Set.Ioi 0)) < ⊤) : ∃ (C : ENNReal), 1 ≤ C ∧ C ≠ ⊤ ∧ ∃ (r₀ : ℝ), 0 < r₀ ∧ ∀ (ρ : ℝ), 0 < ρ → ρ < r₀ → μ (Metric.ball a (2 * ρ)) ≤ C * μ (Metric.ball a ρ)

Assumption 14.3 (1) gives a genuine doubling inequality at small scales.

theorem measure_ball_two_pow_le {n : ℕ} {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))} {a : EuclideanSpace ℝ (Fin n)} {C : ENNReal} {r₀ : ℝ} (hC : ∀ (ρ : ℝ), 0 < ρ → ρ < r₀ → μ (Metric.ball a (2 * ρ)) ≤ C * μ (Metric.ball a ρ)) (k : ℕ) (ρ : ℝ) : 0 < ρ → 2 ^ k * ρ < r₀ → μ (Metric.ball a (2 ^ k * ρ)) ≤ C ^ k * μ (Metric.ball a ρ)

Iterating the doubling inequality.

theorem exists_measure_ball_le_measure_ball {n : ℕ} {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))} (hμ : μ.Regular) {a : EuclideanSpace ℝ (Fin n)} (ha : a ∈ μ.support) (hdoub : Filter.limsup (fun (ρ : ℝ) => μ (Metric.ball a (2 * ρ)) / μ (Metric.ball a ρ)) (nhdsWithin 0 (Set.Ioi 0)) < ⊤) (t : ℝ) : ∃ (D : ENNReal), 1 ≤ D ∧ D ≠ ⊤ ∧ ∃ (ρ₀ : ℝ), 0 < ρ₀ ∧ ∀ (ρ : ℝ), 0 < ρ → ρ < ρ₀ → μ (Metric.ball a (t * ρ)) ≤ D * μ (Metric.ball a ρ)

Under assumption 14.3 (1), balls of comparable radii have comparable measures, uniformly at small scales.

The normalizing constants of a tangent measure

theorem limsup_normalizing_le {n : ℕ} {μ ν : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))} (hμ : μ.Regular) (hν : ν.Regular) {a : EuclideanSpace ℝ (Fin n)} {r : ℕ → ℝ} {c : ℕ → ENNReal} (hr : ∀ (i : ℕ), 0 < r i) (hc : ∀ (i : ℕ), c i ≠ ⊤) (hconv : MeasureTheory.Measure.WeaklyConverges (fun (i : ℕ) => c i • MeasureTheory.Measure.map (blowUpMap a (r i)) μ) ν) : Filter.limsup (fun (i : ℕ) => c i * μ (Metric.closedBall a (r i))) Filter.atTop ≤ ν (Metric.closedBall 0 1)

Upper bound for the normalizing constants: the numbers c i * μ (B (a, r i)) are bounded above.

theorem exists_le_normalizing {n : ℕ} {μ ν : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))} (hμ : μ.Regular) (hν : ν.Regular) {a : EuclideanSpace ℝ (Fin n)} (ha : a ∈ μ.support) (hdoub : Filter.limsup (fun (ρ : ℝ) => μ (Metric.ball a (2 * ρ)) / μ (Metric.ball a ρ)) (nhdsWithin 0 (Set.Ioi 0)) < ⊤) {r : ℕ → ℝ} {c : ℕ → ENNReal} (hr : ∀ (i : ℕ), 0 < r i) (hc : ∀ (i : ℕ), c i ≠ ⊤) (hr0 : Filter.Tendsto r Filter.atTop (nhds 0)) (hν0 : ν ≠ 0) (hconv : MeasureTheory.Measure.WeaklyConverges (fun (i : ℕ) => c i • MeasureTheory.Measure.map (blowUpMap a (r i)) μ) ν) : ∃ (δ : ENNReal), 0 < δ ∧ ∀ᶠ (i : ℕ) in Filter.atTop, δ ≤ c i * μ (Metric.ball a (r i))

Lower bound for the normalizing constants: under assumption 14.3 (1) the numbers c i * μ (B (a, r i)) are eventually bounded away from 0.

Consequence (2): the origin belongs to the support of every tangent measure

theorem zero_mem_support_of_isTangentMeasure {n : ℕ} (μ ν : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) (hμ : μ.Regular) (a : EuclideanSpace ℝ (Fin n)) (ha : a ∈ μ.support) (hdoub : Filter.limsup (fun (ρ : ℝ) => μ (Metric.ball a (2 * ρ)) / μ (Metric.ball a ρ)) (nhdsWithin 0 (Set.Ioi 0)) < ⊤) (htan : IsTangentMeasure μ ν a) : 0 ∈ ν.support

Mattila, Chapter 14, consequence (2) of assumption 14.3 (1). If μ is a Radon measure on ℝⁿ, a ∈ spt μ satisfies limsup_{ρ ↓ 0} μ (B (a, 2ρ)) / μ (B (a, ρ)) < ∞, then 0 ∈ spt ν for every tangent measure ν ∈ Tan (μ, a).

Consequence (3): tangent measures arise from the canonical normalizations

theorem exists_normalized_blowUp_weaklyConverges_of_isTangentMeasure {n : ℕ} (μ ν : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) (hμ : μ.Regular) (a : EuclideanSpace ℝ (Fin n)) (ha : a ∈ μ.support) (hdoub : Filter.limsup (fun (ρ : ℝ) => μ (Metric.ball a (2 * ρ)) / μ (Metric.ball a ρ)) (nhdsWithin 0 (Set.Ioi 0)) < ⊤) (htan : IsTangentMeasure μ ν a) : ∃ (r : ℕ → ℝ) (c : ENNReal), (∀ (i : ℕ), 0 < r i) ∧ StrictAnti r ∧ Filter.Tendsto r Filter.atTop (nhds 0) ∧ 0 < c ∧ c ≠ ⊤ ∧ MeasureTheory.Measure.WeaklyConverges (fun (i : ℕ) => c • (μ (Metric.ball a (r i)))⁻¹ • MeasureTheory.Measure.map (blowUpMap a (r i)) μ) ν

Mattila, Chapter 14, consequence (3) of assumption 14.3 (1). If μ is a Radon measure on ℝⁿ and a ∈ spt μ satisfies limsup_{ρ ↓ 0} μ (B (a, 2ρ)) / μ (B (a, ρ)) < ∞, then every tangent measure ν ∈ Tan (μ, a) can be written as ν = c · lim_i μ (B (a, r i))⁻¹ • T_{a, r i #} μ for a strictly decreasing sequence of radii r i ↓ 0 and a positive finite constant c.

Theorem 14.3: existence of tangent measures

theorem exists_subseq_blowUp_weaklyConverges_tangentMeasure {n : ℕ} (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) (hμ : μ.Regular) (a : EuclideanSpace ℝ (Fin n)) (ha : a ∈ μ.support) (hc : Filter.limsup (fun (ρ : ℝ) => μ (Metric.ball a (2 * ρ)) / μ (Metric.ball a ρ)) (nhdsWithin 0 (Set.Ioi 0)) < ⊤) (r : ℕ → ℝ) (hr_pos : ∀ (i : ℕ), 0 < r i) (hr : Filter.Tendsto r Filter.atTop (nhds 0)) : ∃ (φ : ℕ → ℕ) (ν : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))), StrictMono φ ∧ IsTangentMeasure μ ν a ∧ MeasureTheory.Measure.WeaklyConverges (fun (j : ℕ) => (μ (Metric.ball a (r (φ j))))⁻¹ • MeasureTheory.Measure.map (blowUpMap a (r (φ j))) μ) ν

Mattila, Theorem 14.3. Let μ be a Radon measure on ℝⁿ and let a ∈ spt μ satisfy assumption (1), limsup_{ρ ↓ 0} μ (B (a, 2ρ)) / μ (B (a, ρ)) < ∞. Then every sequence of radii r i ↓ 0 has a subsequence along which the normalized blow-ups μ (B (a, r i))⁻¹ T_{a, r i #} μ converge weakly to a tangent measure of μ at a.