Basic definitions for tangent measures

This file defines blow-up maps, rescaled measures, tangent measures, and the basic facts used by the Chapter 14 results.

noncomputable def blowUpMap {n : ℕ} (a : EuclideanSpace ℝ (Fin n)) (r : ℝ) (x : EuclideanSpace ℝ (Fin n)) : EuclideanSpace ℝ (Fin n)

The blow-up map T_{a,r}(x) = (x - a) / r on Euclidean space ℝⁿ.

Equations

• blowUpMap a r x = r⁻¹ • (x - a)

theorem continuous_blowUpMap {n : ℕ} (a : EuclideanSpace ℝ (Fin n)) (r : ℝ) : Continuous (blowUpMap a r)

theorem measurable_blowUpMap {n : ℕ} (a : EuclideanSpace ℝ (Fin n)) (r : ℝ) : Measurable (blowUpMap a r)

def IsTangentMeasure {n : ℕ} (μ ν : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) (a : EuclideanSpace ℝ (Fin n)) : Prop

IsTangentMeasure μ ν a asserts that ν is a tangent measure of μ at the point a: ν is a nonzero Radon measure which is the weak limit of a sequence of rescaled blow-ups of μ at a along radii tending to 0.

Equations

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

Elementary facts about weak convergence

theorem MeasureTheory.Measure.WeaklyConverges.comp {n : ℕ} {μ : ℕ → Measure (EuclideanSpace ℝ (Fin n))} {ν : Measure (EuclideanSpace ℝ (Fin n))} (h : WeaklyConverges μ ν) {φ : ℕ → ℕ} (hφ : Filter.Tendsto φ Filter.atTop Filter.atTop) : WeaklyConverges (fun (j : ℕ) => μ (φ j)) ν

Weak convergence is inherited by subsequences (more generally, by any reindexing along a map tending to infinity).

theorem MeasureTheory.Measure.WeaklyConverges.smul_of_tendsto_one {n : ℕ} {μ : ℕ → Measure (EuclideanSpace ℝ (Fin n))} {ν : Measure (EuclideanSpace ℝ (Fin n))} (h : WeaklyConverges μ ν) {e : ℕ → ENNReal} (he1 : Filter.Tendsto (fun (i : ℕ) => (e i).toReal) Filter.atTop (nhds 1)) : WeaklyConverges (fun (i : ℕ) => e i • μ i) ν

Rescaling a weakly convergent sequence by constants tending to 1 does not change the weak limit.

theorem MeasureTheory.Measure.WeaklyConverges.congr_seq {n : ℕ} {F G : ℕ → Measure (EuclideanSpace ℝ (Fin n))} {ν : Measure (EuclideanSpace ℝ (Fin n))} (hFG : ∀ (i : ℕ), F i = G i) (h : WeaklyConverges G ν) : WeaklyConverges F ν

Weak convergence only depends on the underlying sequence of measures.

Extracting a strictly decreasing sequence of radii

theorem exists_strictMono_strictAnti_subseq {r : ℕ → ℝ} (hpos : ∀ (i : ℕ), 0 < r i) (hr : Filter.Tendsto r Filter.atTop (nhds 0)) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ StrictAnti fun (j : ℕ) => r (φ j)

A positive sequence tending to 0 has a strictly decreasing subsequence.

Basic properties of the blow-up maps

theorem blowUpMap_preimage_ball {n : ℕ} (a : EuclideanSpace ℝ (Fin n)) {r : ℝ} (hr : 0 < r) (ρ : ℝ) : blowUpMap a r ⁻¹' Metric.ball 0 ρ = Metric.ball a (r * ρ)

theorem blowUpMap_preimage_closedBall {n : ℕ} (a : EuclideanSpace ℝ (Fin n)) {r : ℝ} (hr : 0 < r) (ρ : ℝ) : blowUpMap a r ⁻¹' Metric.closedBall 0 ρ = Metric.closedBall a (r * ρ)

noncomputable def blowUpHomeomorph {n : ℕ} (a : EuclideanSpace ℝ (Fin n)) {r : ℝ} (hr : r ≠ 0) : EuclideanSpace ℝ (Fin n) ≃ₜ EuclideanSpace ℝ (Fin n)

The blow-up map as a homeomorphism of Euclidean space.

Equations

• blowUpHomeomorph a hr = (Homeomorph.subRight a).trans (Homeomorph.smulOfNeZero r⁻¹ ⋯)

theorem regular_map_blowUp {n : ℕ} {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))} (hμ : μ.Regular) (a : EuclideanSpace ℝ (Fin n)) {r : ℝ} (hr : r ≠ 0) : (MeasureTheory.Measure.map (blowUpMap a r) μ).Regular

The push-forward of a Radon measure under a blow-up map is a Radon measure.

theorem regular_smul_map_blowUp {n : ℕ} {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))} (hμ : μ.Regular) (a : EuclideanSpace ℝ (Fin n)) {r : ℝ} (hr : r ≠ 0) {c : ENNReal} (hc : c ≠ ⊤) : (c • MeasureTheory.Measure.map (blowUpMap a r) μ).Regular

A finite rescaling of the push-forward of a Radon measure under a blow-up map is again a Radon measure.

theorem map_blowUp_apply_ball {n : ℕ} (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) (a : EuclideanSpace ℝ (Fin n)) {r : ℝ} (hr : 0 < r) (ρ : ℝ) : (MeasureTheory.Measure.map (blowUpMap a r) μ) (Metric.ball 0 ρ) = μ (Metric.ball a (r * ρ))

theorem map_blowUp_apply_closedBall {n : ℕ} (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))) (a : EuclideanSpace ℝ (Fin n)) {r : ℝ} (hr : 0 < r) (ρ : ℝ) : (MeasureTheory.Measure.map (blowUpMap a r) μ) (Metric.closedBall 0 ρ) = μ (Metric.closedBall a (r * ρ))

Balls of positive and finite measure

theorem measure_ball_pos_of_mem_support {n : ℕ} {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))} {a : EuclideanSpace ℝ (Fin n)} (ha : a ∈ μ.support) {ρ : ℝ} (hρ : 0 < ρ) : 0 < μ (Metric.ball a ρ)

theorem regular_measure_closedBall_lt_top {n : ℕ} {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))} (hμ : μ.Regular) (a : EuclideanSpace ℝ (Fin n)) (ρ : ℝ) : μ (Metric.closedBall a ρ) < ⊤

theorem regular_measure_ball_lt_top {n : ℕ} {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))} (hμ : μ.Regular) (a : EuclideanSpace ℝ (Fin n)) (ρ : ℝ) : μ (Metric.ball a ρ) < ⊤