Mattila's Lemmas 14.5 and 14.6

This file proves the compactness and normalization results for tangent measures appearing in Mattila's Lemmas 14.5 and 14.6.

Auxiliary material for Lemmas 14.5 and 14.6

theorem tendsto_nhdsGT_zero_of_pos {u : ℕ → ℝ} (hpos : ∀ (i : ℕ), 0 < u i) (h0 : Filter.Tendsto u Filter.atTop (nhds 0)) : Filter.Tendsto u Filter.atTop (nhdsWithin 0 (Set.Ioi 0))

A positive sequence converging to 0 converges to 0 from the right.

theorem norm_integral_cc_le {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] (M : MeasureTheory.Measure X) (f : CompactlySupportedContinuousMap X ℝ) {K : Set X} (hK : tsupport ⇑f ⊆ K) (hfin : M K < ⊤) : ‖∫ (x : X), f x ∂M‖ ≤ ‖f.toBoundedContinuousFunction‖ * (M K).toReal

The integral of a compactly supported continuous function against a measure which is finite on the support is bounded by the supremum norm times the measure of the support.

theorem weaklyConverges_of_tendsto_integral_sub {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {F G : ℕ → MeasureTheory.Measure X} {ν : MeasureTheory.Measure X} (h : MeasureTheory.Measure.WeaklyConverges F ν) (hd : ∀ (f : CompactlySupportedContinuousMap X ℝ), Filter.Tendsto (fun (i : ℕ) => ∫ (x : X), f x ∂G i - ∫ (x : X), f x ∂F i) Filter.atTop (nhds 0)) : MeasureTheory.Measure.WeaklyConverges G ν

If two sequences of Radon measures have asymptotically the same integrals against compactly supported continuous functions, then they have the same weak limits.

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

Weak convergence of the blow-ups gives a uniform bound for the mass of balls.

theorem tendsto_mul_measure_diff_zero {n : ℕ} {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))} (hμ : μ.Regular) {a : EuclideanSpace ℝ (Fin n)} (ha : a ∈ μ.support) {B : Set (EuclideanSpace ℝ (Fin n))} (hdens : Filter.Tendsto (fun (s : ℝ) => μ (Metric.ball a s \ B) / μ (Metric.ball a s)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) {r : ℕ → ℝ} (hr : ∀ (i : ℕ), 0 < r i) (hr0 : Filter.Tendsto r Filter.atTop (nhds 0)) {c : ℕ → ENNReal} {t : ℝ} (ht : 0 < t) {M : ENNReal} (hM : M ≠ ⊤) (hbd : ∀ᶠ (i : ℕ) in Filter.atTop, c i * μ (Metric.closedBall a (2 * (r i * t))) ≤ M) : Filter.Tendsto (fun (i : ℕ) => c i * μ (Metric.closedBall a (r i * t) \ B)) Filter.atTop (nhds 0)

If B has density one at a and the normalized masses of the balls stay bounded, then the normalized masses of the sets B̄ (a, r i t) \ B tend to 0.

theorem eventually_measure_ball_le_two_mul_inter {n : ℕ} {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))} (hμ : μ.Regular) {a : EuclideanSpace ℝ (Fin n)} (ha : a ∈ μ.support) {B : Set (EuclideanSpace ℝ (Fin n))} (hB : MeasurableSet B) (hdens : Filter.Tendsto (fun (s : ℝ) => μ (Metric.ball a s \ B) / μ (Metric.ball a s)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) : ∀ᶠ (s : ℝ) in nhdsWithin 0 (Set.Ioi 0), μ (Metric.ball a s) ≤ 2 * μ (Metric.ball a s ∩ B)

If B has density one at a, then at small scales the measure of a ball is at most twice the measure of its intersection with B.

theorem tendsto_integral_sub_restrict {n : ℕ} (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) (hμ : μ.Regular) {B : Set (EuclideanSpace ℝ (Fin n))} (hB : MeasurableSet B) (a : EuclideanSpace ℝ (Fin n)) {r : ℕ → ℝ} (hr : ∀ (i : ℕ), 0 < r i) {c : ℕ → ENNReal} (hcfin : ∀ (i : ℕ), c i ≠ ⊤) (hF : ∀ (i : ℕ), (c i • MeasureTheory.Measure.map (blowUpMap a (r i)) μ).Regular) (hdiff : ∀ (t : ℝ), 0 < t → Filter.Tendsto (fun (i : ℕ) => c i * μ (Metric.closedBall a (r i * t) \ B)) Filter.atTop (nhds 0)) (f : CompactlySupportedContinuousMap (EuclideanSpace ℝ (Fin n)) ℝ) : Filter.Tendsto (fun (i : ℕ) => ∫ (x : EuclideanSpace ℝ (Fin n)), f x ∂c i • MeasureTheory.Measure.map (blowUpMap a (r i)) (μ.restrict B) - ∫ (x : EuclideanSpace ℝ (Fin n)), f x ∂c i • MeasureTheory.Measure.map (blowUpMap a (r i)) μ) Filter.atTop (nhds 0)

The key estimate behind Mattila's Lemma 14.5: if the normalized masses outside B tend to 0, then the blow-ups of μ and of μ.restrict B have asymptotically equal integrals.

theorem isTangentMeasure_restrict_iff {n : ℕ} (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) (hμ : μ.Regular) (B : Set (EuclideanSpace ℝ (Fin n))) (hB : MeasurableSet B) (hμB : (μ.restrict B).Regular) (a : EuclideanSpace ℝ (Fin n)) (ha : a ∈ μ.support) (hdens : Filter.Tendsto (fun (r : ℝ) => μ (Metric.ball a r \ B) / μ (Metric.ball a r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) (ν : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) : IsTangentMeasure μ ν a ↔ IsTangentMeasure (μ.restrict B) ν a

Mattila, Lemma 14.5. If B has density one with respect to μ at a, then restricting μ to B does not change the tangent measures at a.

Auxiliary material for Lemma 14.6

theorem measure_ext_of_bounded {n : ℕ} {m₁ m₂ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))} (h : ∀ (B : Set (EuclideanSpace ℝ (Fin n))), MeasurableSet B → Bornology.IsBounded B → m₁ B = m₂ B) : m₁ = m₂

Two measures agreeing on bounded measurable sets are equal.

theorem measure_eq_withDensity {n : ℕ} (μ L : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) (φ : EuclideanSpace ℝ (Fin n) → ℝ) (hφ_nonneg : ∀ (x : EuclideanSpace ℝ (Fin n)), 0 ≤ φ x) (hφ_loc : MeasureTheory.LocallyIntegrable φ μ) (hL_eq : ∀ (B : Set (EuclideanSpace ℝ (Fin n))), MeasurableSet B → Bornology.IsBounded B → L B = ENNReal.ofReal (∫ (x : EuclideanSpace ℝ (Fin n)) in B, φ x ∂μ)) : L = μ.withDensity fun (x : EuclideanSpace ℝ (Fin n)) => ENNReal.ofReal (φ x)

A measure specified as φ μ on bounded measurable sets is μ.withDensity φ.

theorem ae_tendsto_setAverage_norm_sub {n : ℕ} (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) (hμ : μ.Regular) (φ : EuclideanSpace ℝ (Fin n) → ℝ) (hφ_loc : MeasureTheory.LocallyIntegrable φ μ) : ∀ᵐ (a : EuclideanSpace ℝ (Fin n)) ∂μ, Filter.Tendsto (fun (s : ℝ) => ⨍ (y : EuclideanSpace ℝ (Fin n)) in Metric.closedBall a s, ‖φ y - φ a‖ ∂μ) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Lebesgue differentiation theorem for a Radon measure on Euclidean space.

theorem integral_blowUp_smul {n : ℕ} (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) (a : EuclideanSpace ℝ (Fin n)) (r : ℝ) (c : ENNReal) (f : CompactlySupportedContinuousMap (EuclideanSpace ℝ (Fin n)) ℝ) : ∫ (x : EuclideanSpace ℝ (Fin n)), f x ∂c • MeasureTheory.Measure.map (blowUpMap a r) μ = c.toReal * ∫ (x : EuclideanSpace ℝ (Fin n)), f (blowUpMap a r x) ∂μ

The integral of a compactly supported continuous function against a scaled blow-up.

theorem integral_withDensity_real {n : ℕ} (m : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) {φ : EuclideanSpace ℝ (Fin n) → ℝ} (hφ_meas : Measurable φ) (hφ_nonneg : ∀ (x : EuclideanSpace ℝ (Fin n)), 0 ≤ φ x) (g : EuclideanSpace ℝ (Fin n) → ℝ) : (∫ (x : EuclideanSpace ℝ (Fin n)), g x ∂m.withDensity fun (x : EuclideanSpace ℝ (Fin n)) => ENNReal.ofReal (φ x)) = ∫ (x : EuclideanSpace ℝ (Fin n)), φ x * g x ∂m

theorem norm_integral_blowUp_density_sub_le {n : ℕ} (μ L : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) (hμ : μ.Regular) (φ : EuclideanSpace ℝ (Fin n) → ℝ) (hφ_meas : Measurable φ) (hφ_nonneg : ∀ (x : EuclideanSpace ℝ (Fin n)), 0 ≤ φ x) (hφ_loc : MeasureTheory.LocallyIntegrable φ μ) (hLm : L = μ.withDensity fun (x : EuclideanSpace ℝ (Fin n)) => ENNReal.ofReal (φ x)) (a : EuclideanSpace ℝ (Fin n)) (hφa : 0 < φ a) {r : ℝ} (hr : 0 < r) {c : ENNReal} (f : CompactlySupportedContinuousMap (EuclideanSpace ℝ (Fin n)) ℝ) {t : ℝ} (htsup : tsupport ⇑f ⊆ Metric.closedBall 0 t) : ‖∫ (x : EuclideanSpace ℝ (Fin n)), f x ∂(c / ENNReal.ofReal (φ a)) • MeasureTheory.Measure.map (blowUpMap a r) L - ∫ (x : EuclideanSpace ℝ (Fin n)), f x ∂c • MeasureTheory.Measure.map (blowUpMap a r) μ‖ ≤ c.toReal / φ a * ‖f.toBoundedContinuousFunction‖ * ∫ (y : EuclideanSpace ℝ (Fin n)) in Metric.closedBall a (r * t), ‖φ y - φ a‖ ∂μ

The key per-scale estimate behind Mattila's Lemma 14.6.

theorem tendsto_mul_setIntegral_norm_sub_zero {n : ℕ} (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) (hμ : μ.Regular) (a : EuclideanSpace ℝ (Fin n)) (ha : a ∈ μ.support) (φ : EuclideanSpace ℝ (Fin n) → ℝ) (hleb : Filter.Tendsto (fun (s : ℝ) => ⨍ (y : EuclideanSpace ℝ (Fin n)) in Metric.closedBall a s, ‖φ y - φ a‖ ∂μ) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) {r : ℕ → ℝ} (hr : ∀ (i : ℕ), 0 < r i) (hr0 : Filter.Tendsto r Filter.atTop (nhds 0)) {t : ℝ} (ht : 0 < t) {c : ℕ → ENNReal} {M : ENNReal} (hM : M ≠ ⊤) (hbdd : ∀ᶠ (i : ℕ) in Filter.atTop, c i * μ (Metric.closedBall a (r i * t)) ≤ M) : Filter.Tendsto (fun (i : ℕ) => (c i).toReal * ∫ (y : EuclideanSpace ℝ (Fin n)) in Metric.closedBall a (r i * t), ‖φ y - φ a‖ ∂μ) Filter.atTop (nhds 0)

theorem eventually_ofReal_mul_measure_closedBall_le {n : ℕ} (μ L : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) (hμ : μ.Regular) (φ : EuclideanSpace ℝ (Fin n) → ℝ) (hφ_loc : MeasureTheory.LocallyIntegrable φ μ) (hL_eq : ∀ (B : Set (EuclideanSpace ℝ (Fin n))), MeasurableSet B → Bornology.IsBounded B → L B = ENNReal.ofReal (∫ (x : EuclideanSpace ℝ (Fin n)) in B, φ x ∂μ)) (a : EuclideanSpace ℝ (Fin n)) (ha : a ∈ μ.support) (hφa : 0 < φ a) (hleb : Filter.Tendsto (fun (s : ℝ) => ⨍ (y : EuclideanSpace ℝ (Fin n)) in Metric.closedBall a s, ‖φ y - φ a‖ ∂μ) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) : ∀ᶠ (s : ℝ) in nhdsWithin 0 (Set.Ioi 0), ENNReal.ofReal (φ a / 2) * μ (Metric.closedBall a s) ≤ L (Metric.closedBall a s)

At a Lebesgue point a of φ with φ a > 0, the measure L = φ μ of a small ball is at least φ a / 2 times the μ-measure of that ball.

theorem tendsto_integral_sub_density {n : ℕ} (μ L : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) (hμ : μ.Regular) (φ : EuclideanSpace ℝ (Fin n) → ℝ) (hφ_meas : Measurable φ) (hφ_nonneg : ∀ (x : EuclideanSpace ℝ (Fin n)), 0 ≤ φ x) (hφ_loc : MeasureTheory.LocallyIntegrable φ μ) (hLm : L = μ.withDensity fun (x : EuclideanSpace ℝ (Fin n)) => ENNReal.ofReal (φ x)) (a : EuclideanSpace ℝ (Fin n)) (hφa : 0 < φ a) (ha : a ∈ μ.support) (hleb : Filter.Tendsto (fun (s : ℝ) => ⨍ (y : EuclideanSpace ℝ (Fin n)) in Metric.closedBall a s, ‖φ y - φ a‖ ∂μ) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) {r : ℕ → ℝ} (hr : ∀ (i : ℕ), 0 < r i) (hr0 : Filter.Tendsto r Filter.atTop (nhds 0)) {c : ℕ → ENNReal} (hbdd : ∀ (t : ℝ), 0 < t → ∃ (M : ENNReal), M ≠ ⊤ ∧ ∀ᶠ (i : ℕ) in Filter.atTop, c i * μ (Metric.closedBall a (r i * t)) ≤ M) (f : CompactlySupportedContinuousMap (EuclideanSpace ℝ (Fin n)) ℝ) : Filter.Tendsto (fun (i : ℕ) => ∫ (x : EuclideanSpace ℝ (Fin n)), f x ∂(c i / ENNReal.ofReal (φ a)) • MeasureTheory.Measure.map (blowUpMap a (r i)) L - ∫ (x : EuclideanSpace ℝ (Fin n)), f x ∂c i • MeasureTheory.Measure.map (blowUpMap a (r i)) μ) Filter.atTop (nhds 0)

At a positive Lebesgue point of φ, appropriately normalized blow-ups of μ and φ μ have asymptotically equal integrals.

theorem isTangentMeasure_iff_of_lebesgue_point {n : ℕ} (μ L : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) (hμ : μ.Regular) (hL : L.Regular) (φ : EuclideanSpace ℝ (Fin n) → ℝ) (hφ_meas : Measurable φ) (hφ_nonneg : ∀ (x : EuclideanSpace ℝ (Fin n)), 0 ≤ φ x) (hφ_loc : MeasureTheory.LocallyIntegrable φ μ) (hL_eq : ∀ (B : Set (EuclideanSpace ℝ (Fin n))), MeasurableSet B → Bornology.IsBounded B → L B = ENNReal.ofReal (∫ (x : EuclideanSpace ℝ (Fin n)) in B, φ x ∂μ)) (hLm : L = μ.withDensity fun (x : EuclideanSpace ℝ (Fin n)) => ENNReal.ofReal (φ x)) (a : EuclideanSpace ℝ (Fin n)) (hφa : 0 < φ a) (ha : a ∈ μ.support) (hleb : Filter.Tendsto (fun (s : ℝ) => ⨍ (y : EuclideanSpace ℝ (Fin n)) in Metric.closedBall a s, ‖φ y - φ a‖ ∂μ) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) (ν : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) : IsTangentMeasure μ ν a ↔ IsTangentMeasure L ν a

Mattila, Lemma 14.6, at a fixed Lebesgue point of the density.

theorem isTangentMeasure_iff_ae_of_density {n : ℕ} (μ «λ» : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) (hμ : μ.Regular) («hλ» : «λ».Regular) (φ : EuclideanSpace ℝ (Fin n) → ℝ) (hφ_nonneg : ∀ (x : EuclideanSpace ℝ (Fin n)), 0 ≤ φ x) (hφ_loc : MeasureTheory.LocallyIntegrable φ μ) («hλ_eq» : ∀ (B : Set (EuclideanSpace ℝ (Fin n))), MeasurableSet B → Bornology.IsBounded B → «λ» B = ENNReal.ofReal (∫ (x : EuclideanSpace ℝ (Fin n)) in B, φ x ∂μ)) : ∀ᵐ (a : EuclideanSpace ℝ (Fin n)) ∂«λ», ∀ (ν : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))), IsTangentMeasure μ ν a ↔ IsTangentMeasure «λ» ν a

Mattila, Lemma 14.6. If λ = φ μ with φ ≥ 0 locally μ-integrable, then μ and λ have the same tangent measures at λ-almost every point.