Exact source: Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
Pinned GitHub source · Raw UTF-8 source
Back to The recovered contraction maps one unit ball onto the other
1/-2Copyright (c) 2021 Floris van Doorn. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Floris van Doorn, Sébastien Gouëzel5-/6module78public import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas9public import Mathlib.MeasureTheory.Constructions.BorelSpace.Metric10public import Mathlib.MeasureTheory.Group.Pointwise11public import Mathlib.MeasureTheory.Measure.Doubling12public import Mathlib.MeasureTheory.Measure.Haar.Basic13public import Mathlib.MeasureTheory.Measure.Lebesgue.Basic1415/-!16# Relationship between the Haar and Lebesgue measures1718We prove that the Haar measure and Lebesgue measure are equal on `ℝ` and on `ℝ^ι`, in19`MeasureTheory.addHaarMeasure_eq_volume` and `MeasureTheory.addHaarMeasure_eq_volume_pi`.2021We deduce basic properties of any Haar measure on a finite-dimensional real vector space:22* `map_linearMap_addHaar_eq_smul_addHaar`: a linear map rescales the Haar measure by the23 absolute value of its determinant.24* `addHaar_preimage_linearMap` : when `f` is a linear map with nonzero determinant, the measure25 of `f ⁻¹' s` is the measure of `s` multiplied by the absolute value of the inverse of the26 determinant of `f`.27* `addHaar_image_linearMap` : when `f` is a linear map, the measure of `f '' s` is the28 measure of `s` multiplied by the absolute value of the determinant of `f`.29* `addHaar_submodule` : a strict submodule has measure `0`.30* `addHaar_smul` : the measure of `r • s` is `|r| ^ dim * μ s`.31* `addHaar_ball`: the measure of `ball x r` is `r ^ dim * μ (ball 0 1)`.32* `addHaar_closedBall`: the measure of `closedBall x r` is `r ^ dim * μ (ball 0 1)`.33* `addHaar_sphere`: spheres have zero measure.3435This makes it possible to associate a Lebesgue measure to an `n`-alternating map in dimension `n`.36This measure is called `AlternatingMap.measure`. Its main property is37`ω.measure_parallelepiped v`, stating that the associated measure of the parallelepiped spanned38by vectors `v₁, ..., vₙ` is given by `|ω v|`.3940We also show that a Lebesgue density point `x` of a set `s` (with respect to closed balls) has41density one for the rescaled copies `{x} + r • t` of a given set `t` with positive measure, in42`tendsto_addHaar_inter_smul_one_of_density_one`. In particular, `s` intersects `{x} + r • t` for43small `r`, see `eventually_nonempty_inter_smul_of_density_one`.4445Statements on integrals of functions with respect to an additive Haar measure can be found in46`MeasureTheory.Measure.Haar.NormedSpace`.47-/4849@[expose] public section5051assert_not_exists MeasureTheory.integral5253open TopologicalSpace Set Filter Metric Bornology5455open scoped ENNReal Pointwise Topology NNReal5657/-- The interval `[0,1]` as a compact set with non-empty interior. -/58def TopologicalSpace.PositiveCompacts.Icc01 : PositiveCompacts ℝ where59 carrier := Icc 0 160 isCompact' := isCompact_Icc61 interior_nonempty' := by simp_rw [interior_Icc, nonempty_Ioo, zero_lt_one]6263universe u6465/-- The set `[0,1]^ι` as a compact set with non-empty interior. -/66def TopologicalSpace.PositiveCompacts.piIcc01 (ι : Type*) [Finite ι] :67 PositiveCompacts (ι → ℝ) where68 carrier := pi univ fun _ => Icc 0 169 isCompact' := isCompact_univ_pi fun _ => isCompact_Icc70 interior_nonempty' := by71 simp only [interior_pi_set, Set.toFinite, interior_Icc, univ_pi_nonempty_iff, nonempty_Ioo,72 imp_true_iff, zero_lt_one]7374namespace Module.Basis7576/-- The parallelepiped formed from the standard basis for `ι → ℝ` is `[0,1]^ι` -/77theorem parallelepiped_basisFun (ι : Type*) [Fintype ι] :78 (Pi.basisFun ℝ ι).parallelepiped = TopologicalSpace.PositiveCompacts.piIcc01 ι :=79 SetLike.coe_injective <| by80 refine Eq.trans ?_ ((uIcc_of_le ?_).trans (Set.pi_univ_Icc _ _).symm)81 · classical convert! parallelepiped_single (ι := ι) 182 · exact zero_le_one8384/-- A parallelepiped can be expressed on the standard basis. -/85theorem parallelepiped_eq_map {ι E : Type*} [Fintype ι] [NormedAddCommGroup E]86 [NormedSpace ℝ E] (b : Basis ι ℝ E) :87 b.parallelepiped = (PositiveCompacts.piIcc01 ι).map b.equivFun.symm88 b.equivFunL.symm.continuous b.equivFunL.symm.isOpenMap := by89 classical90 rw [← Basis.parallelepiped_basisFun, ← Basis.parallelepiped_map]91 congr with x92 simp [Pi.single_apply]9394open MeasureTheory MeasureTheory.Measure9596theorem map_addHaar {ι E F : Type*} [Fintype ι] [NormedAddCommGroup E] [NormedAddCommGroup F]97 [NormedSpace ℝ E] [NormedSpace ℝ F] [MeasurableSpace E] [MeasurableSpace F] [BorelSpace E]98 [BorelSpace F] [SecondCountableTopology F] [SigmaCompactSpace F]99 (b : Basis ι ℝ E) (f : E ≃L[ℝ] F) :100 map f b.addHaar = (b.map f.toLinearEquiv).addHaar := by101 rw [eq_comm, Basis.addHaar_eq_iff, Measure.map_apply f.continuous.measurable102 (PositiveCompacts.isCompact _).measurableSet, Basis.coe_parallelepiped, Basis.coe_map]103 erw [← image_parallelepiped, f.toEquiv.preimage_image, addHaar_self]104105end Module.Basis106107namespace MeasureTheory108109open Measure TopologicalSpace.PositiveCompacts Module110111/-!112### The Lebesgue measure is a Haar measure on `ℝ` and on `ℝ^ι`.113-/114115/-- The Haar measure equals the Lebesgue measure on `ℝ`. -/116theorem addHaarMeasure_eq_volume : addHaarMeasure Icc01 = volume := by117 convert! (addHaarMeasure_unique volume Icc01).symm; simp [Icc01]118119/-- The Haar measure equals the Lebesgue measure on `ℝ^ι`. -/120theorem addHaarMeasure_eq_volume_pi (ι : Type*) [Fintype ι] :121 addHaarMeasure (piIcc01 ι) = volume := by122 convert! (addHaarMeasure_unique volume (piIcc01 ι)).symm123 simp only [piIcc01, volume_pi_pi fun _ => Icc (0 : ℝ) 1, PositiveCompacts.coe_mk,124 Compacts.coe_mk, Finset.prod_const_one, ENNReal.ofReal_one, Real.volume_Icc, one_smul, sub_zero]125126theorem isAddHaarMeasure_volume_pi (ι : Type*) [Fintype ι] :127 IsAddHaarMeasure (volume : Measure (ι → ℝ)) :=128 inferInstance129130namespace Measure131132/-!133### Strict subspaces have zero measure134-/135136open scoped Function -- required for scoped `on` notation137138/-- If a set is disjoint from its translates by infinitely many bounded vectors, then it has measure139zero. This auxiliary lemma proves this assuming additionally that the set is bounded. -/140theorem addHaar_eq_zero_of_disjoint_translates_aux {E : Type*} [NormedAddCommGroup E]141 [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E)142 [IsAddHaarMeasure μ] {s : Set E} (u : ℕ → E) (sb : IsBounded s) (hu : IsBounded (range u))143 (hs : Pairwise (Disjoint on fun n => {u n} + s)) (h's : MeasurableSet s) : μ s = 0 := by144 by_contra h145 apply lt_irrefl ∞146 calc147 ∞ = ∑' _ : ℕ, μ s := (ENNReal.tsum_const_eq_top_of_ne_zero h).symm148 _ = ∑' n : ℕ, μ ({u n} + s) := by149 congr 1; ext1 n; simp only [image_add_left, measure_preimage_add, singleton_add]150 _ = μ (⋃ n, {u n} + s) := Eq.symm <| measure_iUnion hs fun n => by151 simpa only [image_add_left, singleton_add] using! measurable_id.const_add _ h's152 _ = μ (range u + s) := by rw [← iUnion_add, iUnion_singleton_eq_range]153 _ < ∞ := (hu.add sb).measure_lt_top154155/-- If a set is disjoint from its translates by infinitely many bounded vectors, then it has measure156zero. -/157theorem addHaar_eq_zero_of_disjoint_translates {E : Type*} [NormedAddCommGroup E]158 [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E)159 [IsAddHaarMeasure μ] {s : Set E} (u : ℕ → E) (hu : IsBounded (range u))160 (hs : Pairwise (Disjoint on fun n => {u n} + s)) (h's : MeasurableSet s) : μ s = 0 := by161 suffices H : ∀ R, μ (s ∩ closedBall 0 R) = 0 by162 rw [← nonpos_iff_eq_zero]163 calc164 μ s ≤ ∑' n : ℕ, μ (s ∩ closedBall 0 n) := by165 conv_lhs => rw [← iUnion_inter_closedBall_nat s 0]166 exact measure_iUnion_le _167 _ = 0 := by simp only [H, tsum_zero]168 intro R169 apply addHaar_eq_zero_of_disjoint_translates_aux μ u170 (isBounded_closedBall.subset inter_subset_right) hu _ (h's.inter measurableSet_closedBall)171 refine pairwise_disjoint_mono hs fun n => ?_172 exact add_subset_add Subset.rfl inter_subset_left173174/-- A strict vector subspace has measure zero. -/175theorem addHaar_submodule {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E]176 [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [IsAddHaarMeasure μ] (s : Submodule ℝ E)177 (hs : s ≠ ⊤) : μ s = 0 := by178 obtain ⟨x, hx⟩ : ∃ x, x ∉ s := by179 simpa only [Submodule.eq_top_iff', not_exists, Ne, not_forall] using hs180 obtain ⟨c, cpos, cone⟩ : ∃ c : ℝ, 0 < c ∧ c < 1 := ⟨1 / 2, by simp, by norm_num⟩181 have A : IsBounded (range fun n : ℕ => c ^ n • x) :=182 have : Tendsto (fun n : ℕ => c ^ n • x) atTop (𝓝 ((0 : ℝ) • x)) :=183 (tendsto_pow_atTop_nhds_zero_of_lt_one cpos.le cone).smul_const x184 isBounded_range_of_tendsto _ this185 apply addHaar_eq_zero_of_disjoint_translates μ _ A _186 (Submodule.closed_of_finiteDimensional s).measurableSet187 intro m n hmn188 simp only [Function.onFun, image_add_left, singleton_add, disjoint_left, mem_preimage,189 SetLike.mem_coe]190 intro y hym hyn191 have A : (c ^ n - c ^ m) • x ∈ s := by192 convert! s.sub_mem hym hyn using 1193 simp only [sub_smul, neg_sub_neg, add_sub_add_right_eq_sub]194 have H : c ^ n - c ^ m ≠ 0 := by195 simpa only [sub_eq_zero, Ne] using (pow_right_strictAnti₀ cpos cone).injective.ne hmn.symm196 have : x ∈ s := by197 convert! s.smul_mem (c ^ n - c ^ m)⁻¹ A198 rw [smul_smul, inv_mul_cancel₀ H, one_smul]199 exact hx this200201/-- A strict affine subspace has measure zero. -/202theorem addHaar_affineSubspace {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]203 [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [IsAddHaarMeasure μ]204 (s : AffineSubspace ℝ E) (hs : s ≠ ⊤) : μ s = 0 := by205 rcases s.eq_bot_or_nonempty with (rfl | hne)206 · rw [AffineSubspace.bot_coe, measure_empty]207 rw [Ne, ← AffineSubspace.direction_eq_top_iff_of_nonempty hne] at hs208 rcases hne with ⟨x, hx : x ∈ s⟩209 simpa only [AffineSubspace.coe_direction_eq_vsub_set_right hx, vsub_eq_sub, sub_eq_add_neg,210 image_add_right, neg_neg, measure_preimage_add_right] using addHaar_submodule μ s.direction hs211212/-!213### Applying a linear map rescales Haar measure by the determinant214215We first prove this on `ι → ℝ`, using that this is already known for the product Lebesgue216measure (thanks to matrices computations). Then, we extend this to any finite-dimensional real217vector space by using a linear equiv with a space of the form `ι → ℝ`, and arguing that such a218linear equiv maps Haar measure to Haar measure.219-/220221theorem map_linearMap_addHaar_pi_eq_smul_addHaar {ι : Type*} [Finite ι] {f : (ι → ℝ) →ₗ[ℝ] ι → ℝ}222 (hf : LinearMap.det f ≠ 0) (μ : Measure (ι → ℝ)) [IsAddHaarMeasure μ] :223 Measure.map f μ = ENNReal.ofReal (abs (LinearMap.det f)⁻¹) • μ := by224 cases nonempty_fintype ι225 /- We have already proved the result for the Lebesgue product measure, using matrices.226 We deduce it for any Haar measure by uniqueness (up to scalar multiplication). -/227 have := addHaarMeasure_unique μ (piIcc01 ι)228 rw [this, addHaarMeasure_eq_volume_pi, Measure.map_smul,229 Real.map_linearMap_volume_pi_eq_smul_volume_pi hf, smul_comm]230231variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E]232 [FiniteDimensional ℝ E] (μ : Measure E) [IsAddHaarMeasure μ]233234theorem map_linearMap_addHaar_eq_smul_addHaar {f : E →ₗ[ℝ] E} (hf : LinearMap.det f ≠ 0) :235 Measure.map f μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ := by236 -- we reduce to the case of `E = ι → ℝ`, for which we have already proved the result using237 -- matrices in `map_linearMap_addHaar_pi_eq_smul_addHaar`.238 let ι := Fin (finrank ℝ E)239 haveI : FiniteDimensional ℝ (ι → ℝ) := by infer_instance240 have : finrank ℝ E = finrank ℝ (ι → ℝ) := by simp [ι]241 have e : E ≃ₗ[ℝ] ι → ℝ := LinearEquiv.ofFinrankEq E (ι → ℝ) this242 -- next line is to avoid `g` getting reduced by `simp`.243 obtain ⟨g, hg⟩ : ∃ g, g = (e : E →ₗ[ℝ] ι → ℝ).comp (f.comp (e.symm : (ι → ℝ) →ₗ[ℝ] E)) := ⟨_, rfl⟩244 have gdet : LinearMap.det g = LinearMap.det f := by rw [hg]; exact LinearMap.det_conj f e245 rw [← gdet] at hf ⊢246 have fg : f = (e.symm : (ι → ℝ) →ₗ[ℝ] E).comp (g.comp (e : E →ₗ[ℝ] ι → ℝ)) := by247 ext x248 simp only [LinearEquiv.coe_coe, Function.comp_apply, LinearMap.coe_comp,249 LinearEquiv.symm_apply_apply, hg]250 simp only [fg, LinearEquiv.coe_coe, LinearMap.coe_comp]251 have Ce : Continuous e := (e : E →ₗ[ℝ] ι → ℝ).continuous_of_finiteDimensional252 have Cg : Continuous g := LinearMap.continuous_of_finiteDimensional g253 have Cesymm : Continuous e.symm := (e.symm : (ι → ℝ) →ₗ[ℝ] E).continuous_of_finiteDimensional254 rw [← map_map Cesymm.measurable (Cg.comp Ce).measurable, ← map_map Cg.measurable Ce.measurable]255 haveI : IsAddHaarMeasure (map e μ) := (e : E ≃+ (ι → ℝ)).isAddHaarMeasure_map μ Ce Cesymm256 have ecomp : e.symm ∘ e = id := by257 ext x; simp only [id, Function.comp_apply, LinearEquiv.symm_apply_apply]258 rw [map_linearMap_addHaar_pi_eq_smul_addHaar hf (map e μ), Measure.map_smul,259 map_map Cesymm.measurable Ce.measurable, ecomp, Measure.map_id]260261/-- The preimage of a set `s` under a linear map `f` with nonzero determinant has measure262equal to `μ s` times the absolute value of the inverse of the determinant of `f`. -/263@[simp]264theorem addHaar_preimage_linearMap {f : E →ₗ[ℝ] E} (hf : LinearMap.det f ≠ 0) (s : Set E) :265 μ (f ⁻¹' s) = ENNReal.ofReal |(LinearMap.det f)⁻¹| * μ s :=266 calc267 μ (f ⁻¹' s) = Measure.map f μ s :=268 ((f.equivOfDetNeZero hf).toContinuousLinearEquiv.toHomeomorph.toMeasurableEquiv.map_apply269 s).symm270 _ = ENNReal.ofReal |(LinearMap.det f)⁻¹| * μ s := by271 rw [map_linearMap_addHaar_eq_smul_addHaar μ hf]; rfl272273/-- The preimage of a set `s` under a continuous linear map `f` with nonzero determinant has measure274equal to `μ s` times the absolute value of the inverse of the determinant of `f`. -/275@[simp]276theorem addHaar_preimage_continuousLinearMap {f : E →L[ℝ] E}277 (hf : LinearMap.det (f : E →ₗ[ℝ] E) ≠ 0) (s : Set E) :278 μ (f ⁻¹' s) = ENNReal.ofReal (abs (LinearMap.det (f : E →ₗ[ℝ] E))⁻¹) * μ s :=279 addHaar_preimage_linearMap μ hf s280281/-- The preimage of a set `s` under a linear equiv `f` has measure282equal to `μ s` times the absolute value of the inverse of the determinant of `f`. -/283@[simp]284theorem addHaar_preimage_linearEquiv (f : E ≃ₗ[ℝ] E) (s : Set E) :285 μ (f ⁻¹' s) = ENNReal.ofReal |LinearMap.det (f.symm : E →ₗ[ℝ] E)| * μ s := by286 have A : LinearMap.det (f : E →ₗ[ℝ] E) ≠ 0 := (LinearEquiv.isUnit_det' f).ne_zero287 convert! addHaar_preimage_linearMap μ A s288 simp only [LinearEquiv.det_coe_symm]289290/-- The preimage of a set `s` under a continuous linear equiv `f` has measure291equal to `μ s` times the absolute value of the inverse of the determinant of `f`. -/292@[simp]293theorem addHaar_preimage_continuousLinearEquiv (f : E ≃L[ℝ] E) (s : Set E) :294 μ (f ⁻¹' s) = ENNReal.ofReal |LinearMap.det (f.symm : E →ₗ[ℝ] E)| * μ s :=295 addHaar_preimage_linearEquiv μ _ s296297/-- The image of a set `s` under a linear map `f` has measure298equal to `μ s` times the absolute value of the determinant of `f`. -/299@[simp]300theorem addHaar_image_linearMap (f : E →ₗ[ℝ] E) (s : Set E) :301 μ (f '' s) = ENNReal.ofReal |LinearMap.det f| * μ s := by302 rcases ne_or_eq (LinearMap.det f) 0 with (hf | hf)303 · let g := (f.equivOfDetNeZero hf).toContinuousLinearEquiv304 change μ (g '' s) = _305 rw [ContinuousLinearEquiv.image_eq_preimage_symm g s, addHaar_preimage_continuousLinearEquiv]306 congr307 · simpa [hf] using (measure_mono (image_subset_range _ _)).trans_eq <|308 addHaar_submodule μ _ (LinearMap.range_lt_top_of_det_eq_zero hf).ne309310/-- The image of a set `s` under a continuous linear map `f` has measure311equal to `μ s` times the absolute value of the determinant of `f`. -/312@[simp]313theorem addHaar_image_continuousLinearMap (f : E →L[ℝ] E) (s : Set E) :314 μ (f '' s) = ENNReal.ofReal |LinearMap.det (f : E →ₗ[ℝ] E)| * μ s :=315 addHaar_image_linearMap μ _ s316317/-- The image of a set `s` under a continuous linear equiv `f` has measure318equal to `μ s` times the absolute value of the determinant of `f`. -/319@[simp]320theorem addHaar_image_continuousLinearEquiv (f : E ≃L[ℝ] E) (s : Set E) :321 μ (f '' s) = ENNReal.ofReal |LinearMap.det (f : E →ₗ[ℝ] E)| * μ s :=322 μ.addHaar_image_linearMap (f : E →ₗ[ℝ] E) s323324theorem LinearMap.quasiMeasurePreserving (f : E →ₗ[ℝ] E) (hf : LinearMap.det f ≠ 0) :325 QuasiMeasurePreserving f μ μ := by326 refine ⟨f.continuous_of_finiteDimensional.measurable, ?_⟩327 rw [map_linearMap_addHaar_eq_smul_addHaar μ hf]328 exact smul_absolutelyContinuous329330theorem ContinuousLinearMap.quasiMeasurePreserving (f : E →L[ℝ] E) (hf : f.det ≠ 0) :331 QuasiMeasurePreserving f μ μ :=332 LinearMap.quasiMeasurePreserving μ (f : E →ₗ[ℝ] E) hf333334/-!335### Basic properties of Haar measures on real vector spaces336-/337338339theorem map_addHaar_smul {r : ℝ} (hr : r ≠ 0) :340 Measure.map (r • ·) μ = ENNReal.ofReal (abs (r ^ finrank ℝ E)⁻¹) • μ := by341 let f : E →ₗ[ℝ] E := r • (1 : E →ₗ[ℝ] E)342 change Measure.map f μ = _343 have hf : LinearMap.det f ≠ 0 := by344 simp only [f, mul_one, LinearMap.det_smul, Ne, map_one]345 exact pow_ne_zero _ hr346 simp only [f, map_linearMap_addHaar_eq_smul_addHaar μ hf, mul_one, LinearMap.det_smul, map_one]347348theorem quasiMeasurePreserving_smul {r : ℝ} (hr : r ≠ 0) :349 QuasiMeasurePreserving (r • ·) μ μ := by350 refine ⟨measurable_const_smul r, ?_⟩351 rw [map_addHaar_smul μ hr]352 exact smul_absolutelyContinuous353354@[simp]355theorem addHaar_preimage_smul {r : ℝ} (hr : r ≠ 0) (s : Set E) :356 μ ((r • ·) ⁻¹' s) = ENNReal.ofReal (abs (r ^ finrank ℝ E)⁻¹) * μ s :=357 calc358 μ ((r • ·) ⁻¹' s) = Measure.map (r • ·) μ s :=359 ((Homeomorph.smul (isUnit_iff_ne_zero.2 hr).unit).toMeasurableEquiv.map_apply s).symm360 _ = ENNReal.ofReal (abs (r ^ finrank ℝ E)⁻¹) * μ s := by361 rw [map_addHaar_smul μ hr, coe_smul, Pi.smul_apply, smul_eq_mul]362363/-- Rescaling a set by a factor `r` multiplies its measure by `abs (r ^ dim)`. -/364@[simp]365theorem addHaar_smul (r : ℝ) (s : Set E) :366 μ (r • s) = ENNReal.ofReal (abs (r ^ finrank ℝ E)) * μ s := by367 rcases ne_or_eq r 0 with (h | rfl)368 · rw [← preimage_smul_inv₀ h, addHaar_preimage_smul μ (inv_ne_zero h), inv_pow, inv_inv]369 rcases eq_empty_or_nonempty s with (rfl | hs)370 · simp only [measure_empty, mul_zero, smul_set_empty]371 rw [zero_smul_set hs, ← singleton_zero]372 by_cases h : finrank ℝ E = 0373 · haveI : Subsingleton E := finrank_zero_iff.1 h374 simp only [h, one_mul, ENNReal.ofReal_one, abs_one, Subsingleton.eq_univ_of_nonempty hs,375 pow_zero, Subsingleton.eq_univ_of_nonempty (singleton_nonempty (0 : E))]376 · haveI : Nontrivial E := nontrivial_of_finrank_pos (bot_lt_iff_ne_bot.2 h)377 simp only [h, zero_mul, ENNReal.ofReal_zero, abs_zero, Ne, not_false_iff,378 zero_pow, measure_singleton]379380theorem addHaar_smul_of_nonneg {r : ℝ} (hr : 0 ≤ r) (s : Set E) :381 μ (r • s) = ENNReal.ofReal (r ^ finrank ℝ E) * μ s := by382 rw [addHaar_smul, abs_pow, abs_of_nonneg hr]383384@[simp]385theorem addHaar_nnreal_smul (r : ℝ≥0) (s : Set E) :386 μ (r • s) = r ^ Module.finrank ℝ E * μ s := by387 simp [NNReal.smul_def]388389variable {μ} {s : Set E}390391-- Note: We might want to rename this once we acquire the lemma corresponding to392-- `MeasurableSet.const_smul`393theorem NullMeasurableSet.const_smul (hs : NullMeasurableSet s μ) (r : ℝ) :394 NullMeasurableSet (r • s) μ := by395 obtain rfl | hs' := s.eq_empty_or_nonempty396 · simp397 obtain rfl | hr := eq_or_ne r 0398 · simpa [zero_smul_set hs'] using! nullMeasurableSet_singleton _399 obtain ⟨t, ht, hst⟩ := hs400 refine ⟨_, ht.const_smul_of_ne_zero hr, ?_⟩401 rw [← measure_symmDiff_eq_zero_iff] at hst ⊢402 rw [← smul_set_symmDiff₀ hr, addHaar_smul μ, hst, mul_zero]403404variable (μ)405406@[simp]407theorem addHaar_image_homothety (x : E) (r : ℝ) (s : Set E) :408 μ (AffineMap.homothety x r '' s) = ENNReal.ofReal (abs (r ^ finrank ℝ E)) * μ s :=409 calc410 μ (AffineMap.homothety x r '' s) = μ ((fun y => y + x) '' (r • (fun y => y + -x) '' s)) := by411 simp only [← image_smul, image_image, ← sub_eq_add_neg]; rfl412 _ = ENNReal.ofReal (abs (r ^ finrank ℝ E)) * μ s := by413 simp only [image_add_right, measure_preimage_add_right, addHaar_smul]414415/-! We don't need to state `map_addHaar_neg` here, because it has already been proved for416general Haar measures on general commutative groups. -/417418419/-! ### Measure of balls -/420421theorem addHaar_ball_center {E : Type*} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E]422 (μ : Measure E) [IsAddHaarMeasure μ] (x : E) (r : ℝ) : μ (ball x r) = μ (ball (0 : E) r) := by423 have : ball (0 : E) r = (x + ·) ⁻¹' ball x r := by simp [preimage_add_ball]424 rw [this, measure_preimage_add]425426theorem addHaar_real_ball_center {E : Type*} [NormedAddCommGroup E] [MeasurableSpace E]427 [BorelSpace E] (μ : Measure E) [IsAddHaarMeasure μ] (x : E) (r : ℝ) :428 μ.real (ball x r) = μ.real (ball (0 : E) r) := by429 simp [measureReal_def, addHaar_ball_center]430431theorem addHaar_closedBall_center {E : Type*} [NormedAddCommGroup E] [MeasurableSpace E]432 [BorelSpace E] (μ : Measure E) [IsAddHaarMeasure μ] (x : E) (r : ℝ) :433 μ (closedBall x r) = μ (closedBall (0 : E) r) := by434 have : closedBall (0 : E) r = (x + ·) ⁻¹' closedBall x r := by simp [preimage_add_closedBall]435 rw [this, measure_preimage_add]436437theorem addHaar_real_closedBall_center {E : Type*} [NormedAddCommGroup E] [MeasurableSpace E]438 [BorelSpace E] (μ : Measure E) [IsAddHaarMeasure μ] (x : E) (r : ℝ) :439 μ.real (closedBall x r) = μ.real (closedBall (0 : E) r) := by440 simp [measureReal_def, addHaar_closedBall_center]441442theorem addHaar_ball_mul_of_pos (x : E) {r : ℝ} (hr : 0 < r) (s : ℝ) :443 μ (ball x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 s) := by444 have : ball (0 : E) (r * s) = r • ball (0 : E) s := by445 simp only [_root_.smul_ball hr.ne' (0 : E) s, Real.norm_eq_abs, abs_of_nonneg hr.le, smul_zero]446 simp only [this, addHaar_smul, abs_of_nonneg hr.le, addHaar_ball_center, abs_pow]447448theorem addHaar_ball_of_pos (x : E) {r : ℝ} (hr : 0 < r) :449 μ (ball x r) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 1) := by450 rw [← addHaar_ball_mul_of_pos μ x hr, mul_one]451452theorem addHaar_ball_mul [Nontrivial E] (x : E) {r : ℝ} (hr : 0 ≤ r) (s : ℝ) :453 μ (ball x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 s) := by454 rcases hr.eq_or_lt with (rfl | h)455 · simp only [zero_pow (finrank_pos (R := ℝ) (M := E)).ne', measure_empty, zero_mul,456 ENNReal.ofReal_zero, ball_zero]457 · exact addHaar_ball_mul_of_pos μ x h s458459theorem addHaar_ball [Nontrivial E] (x : E) {r : ℝ} (hr : 0 ≤ r) :460 μ (ball x r) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 1) := by461 rw [← addHaar_ball_mul μ x hr, mul_one]462463theorem addHaar_closedBall_mul_of_pos (x : E) {r : ℝ} (hr : 0 < r) (s : ℝ) :464 μ (closedBall x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 s) := by465 have : closedBall (0 : E) (r * s) = r • closedBall (0 : E) s := by466 simp [smul_closedBall' hr.ne' (0 : E), abs_of_nonneg hr.le]467 simp only [this, addHaar_smul, abs_of_nonneg hr.le, addHaar_closedBall_center, abs_pow]468469theorem addHaar_closedBall_mul (x : E) {r : ℝ} (hr : 0 ≤ r) {s : ℝ} (hs : 0 ≤ s) :470 μ (closedBall x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 s) := by471 have : closedBall (0 : E) (r * s) = r • closedBall (0 : E) s := by472 simp [smul_closedBall r (0 : E) hs, abs_of_nonneg hr]473 simp only [this, addHaar_smul, abs_of_nonneg hr, addHaar_closedBall_center, abs_pow]474475/-- The measure of a closed ball can be expressed in terms of the measure of the closed unit ball.476Use instead `addHaar_closedBall`, which uses the measure of the open unit ball as a standard477form. -/478theorem addHaar_closedBall' (x : E) {r : ℝ} (hr : 0 ≤ r) :479 μ (closedBall x r) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 1) := by480 rw [← addHaar_closedBall_mul μ x hr zero_le_one, mul_one]481482theorem addHaar_real_closedBall' (x : E) {r : ℝ} (hr : 0 ≤ r) :483 μ.real (closedBall x r) = r ^ finrank ℝ E * μ.real (closedBall 0 1) := by484 simp only [measureReal_def, addHaar_closedBall' μ x hr, ENNReal.toReal_mul, mul_eq_mul_right_iff,485 ENNReal.toReal_ofReal_eq_iff]486 left487 positivity488489theorem addHaar_unitClosedBall_eq_addHaar_unitBall :490 μ (closedBall (0 : E) 1) = μ (ball 0 1) := by491 apply le_antisymm _ (measure_mono ball_subset_closedBall)492 have A : Tendsto493 (fun r : ℝ => ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall (0 : E) 1)) (𝓝[<] 1)494 (𝓝 (ENNReal.ofReal ((1 : ℝ) ^ finrank ℝ E) * μ (closedBall (0 : E) 1))) := by495 refine ENNReal.Tendsto.mul ?_ (by simp) tendsto_const_nhds (by simp)496 exact ENNReal.tendsto_ofReal ((tendsto_id'.2 nhdsWithin_le_nhds).pow _)497 simp only [one_pow, one_mul, ENNReal.ofReal_one] at A498 refine le_of_tendsto A ?_499 filter_upwards [Ioo_mem_nhdsLT zero_lt_one] with r hr500 rw [← addHaar_closedBall' μ (0 : E) hr.1.le]501 exact measure_mono (closedBall_subset_ball hr.2)502503theorem addHaar_closedBall (x : E) {r : ℝ} (hr : 0 ≤ r) :504 μ (closedBall x r) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 1) := by505 rw [addHaar_closedBall' μ x hr, addHaar_unitClosedBall_eq_addHaar_unitBall]506507theorem addHaar_real_closedBall (x : E) {r : ℝ} (hr : 0 ≤ r) :508 μ.real (closedBall x r) = r ^ finrank ℝ E * μ.real (ball 0 1) := by509 simp [addHaar_real_closedBall' μ x hr, measureReal_def,510 addHaar_unitClosedBall_eq_addHaar_unitBall]511512theorem addHaar_closedBall_eq_addHaar_ball [Nontrivial E] (x : E) (r : ℝ) :513 μ (closedBall x r) = μ (ball x r) := by514 by_cases! h : r < 0515 · rw [Metric.closedBall_eq_empty.mpr h, Metric.ball_eq_empty.mpr h.le]516 rw [addHaar_closedBall μ x h, addHaar_ball μ x h]517518theorem addHaar_real_closedBall_eq_addHaar_real_ball [Nontrivial E] (x : E) (r : ℝ) :519 μ.real (closedBall x r) = μ.real (ball x r) := by520 simp [measureReal_def, addHaar_closedBall_eq_addHaar_ball μ x r]521522theorem addHaar_sphere_of_ne_zero (x : E) {r : ℝ} (hr : r ≠ 0) : μ (sphere x r) = 0 := by523 rcases hr.lt_or_gt with (h | h)524 · simp only [empty_sdiff, measure_empty, ← closedBall_sdiff_ball, closedBall_eq_empty.2 h]525 · rw [← closedBall_sdiff_ball,526 measure_sdiff ball_subset_closedBall measurableSet_ball.nullMeasurableSet527 measure_ball_lt_top.ne,528 addHaar_ball_of_pos μ _ h, addHaar_closedBall μ _ h.le, tsub_self]529530theorem addHaar_sphere [Nontrivial E] (x : E) (r : ℝ) : μ (sphere x r) = 0 := by531 rcases eq_or_ne r 0 with (rfl | h)532 · rw [sphere_zero, measure_singleton]533 · exact addHaar_sphere_of_ne_zero μ x h534535theorem addHaar_singleton_add_smul_div_singleton_add_smul {r : ℝ} (hr : r ≠ 0) (x y : E)536 (s t : Set E) : μ ({x} + r • s) / μ ({y} + r • t) = μ s / μ t :=537 calc538 μ ({x} + r • s) / μ ({y} + r • t) = ENNReal.ofReal (|r| ^ finrank ℝ E) * μ s *539 (ENNReal.ofReal (|r| ^ finrank ℝ E) * μ t)⁻¹ := by540 simp only [div_eq_mul_inv, addHaar_smul, image_add_left, measure_preimage_add, abs_pow,541 singleton_add]542 _ = ENNReal.ofReal (|r| ^ finrank ℝ E) * (ENNReal.ofReal (|r| ^ finrank ℝ E))⁻¹ *543 (μ s * (μ t)⁻¹) := by544 rw [ENNReal.mul_inv]545 · ring546 · simp only [pow_pos (abs_pos.mpr hr), ENNReal.ofReal_eq_zero, not_le, Ne, true_or]547 · simp only [ENNReal.ofReal_ne_top, true_or, Ne, not_false_iff]548 _ = μ s / μ t := by549 rw [ENNReal.mul_inv_cancel, one_mul, div_eq_mul_inv]550 · simp only [pow_pos (abs_pos.mpr hr), ENNReal.ofReal_eq_zero, not_le, Ne]551 · simp only [ENNReal.ofReal_ne_top, Ne, not_false_iff]552553instance (priority := 100) isUnifLocDoublingMeasureOfIsAddHaarMeasure :554 IsUnifLocDoublingMeasure μ := by555 refine ⟨⟨(2 : ℝ≥0) ^ finrank ℝ E, ?_⟩⟩556 filter_upwards [self_mem_nhdsWithin] with r hr x557 rw [addHaar_closedBall_mul μ x zero_le_two (le_of_lt hr), addHaar_closedBall_center μ x,558 ENNReal.ofReal, Real.toNNReal_pow zero_le_two]559 simp only [Real.toNNReal_ofNat, le_refl]560561section562563/-!564### The Lebesgue measure associated to an alternating map565-/566567variable {ι G : Type*} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup G] [NormedSpace ℝ G]568 [MeasurableSpace G] [BorelSpace G]569570theorem addHaar_parallelepiped (b : Basis ι ℝ G) (v : ι → G) :571 b.addHaar (parallelepiped v) = ENNReal.ofReal |b.det v| := by572 have : FiniteDimensional ℝ G := b.finiteDimensional_of_finite573 have A : parallelepiped v = b.constr ℕ v '' parallelepiped b := by574 rw [image_parallelepiped]575 exact congr_arg _ <| funext fun i ↦ (b.constr_basis ℕ v i).symm576 rw [A, addHaar_image_linearMap, b.addHaar_self, mul_one, ← LinearMap.det_toMatrix b,577 ← Basis.toMatrix_eq_toMatrix_constr, Basis.det_apply]578579variable [FiniteDimensional ℝ G] {n : ℕ} [_i : Fact (finrank ℝ G = n)]580581/-- The Lebesgue measure associated to an alternating map. It gives measure `|ω v|` to the582parallelepiped spanned by the vectors `v₁, ..., vₙ`. Note that it is not always a Haar measure,583as it can be zero, but it is always locally finite and translation invariant. -/584noncomputable irreducible_def _root_.AlternatingMap.measure (ω : G [⋀^Fin n]→ₗ[ℝ] ℝ) :585 Measure G :=586 ‖ω (finBasisOfFinrankEq ℝ G _i.out)‖₊ • (finBasisOfFinrankEq ℝ G _i.out).addHaar587588theorem _root_.AlternatingMap.measure_parallelepiped (ω : G [⋀^Fin n]→ₗ[ℝ] ℝ)589 (v : Fin n → G) : ω.measure (parallelepiped v) = ENNReal.ofReal |ω v| := by590 conv_rhs => rw [ω.eq_smul_basis_det (finBasisOfFinrankEq ℝ G _i.out)]591 simp only [addHaar_parallelepiped, AlternatingMap.measure, coe_nnreal_smul_apply,592 AlternatingMap.smul_apply, smul_eq_mul, abs_mul, ENNReal.ofReal_mul (abs_nonneg _),593 ← Real.enorm_eq_ofReal_abs, enorm]594595instance (ω : G [⋀^Fin n]→ₗ[ℝ] ℝ) : IsAddLeftInvariant ω.measure := by596 rw [AlternatingMap.measure]; infer_instance597598instance (ω : G [⋀^Fin n]→ₗ[ℝ] ℝ) : IsLocallyFiniteMeasure ω.measure := by599 rw [AlternatingMap.measure]; infer_instance600601end602603/-!604### Density points605606Besicovitch covering theorem ensures that, for any locally finite measure on a finite-dimensional607real vector space, almost every point of a set `s` is a density point, i.e.,608`μ (s ∩ closedBall x r) / μ (closedBall x r)` tends to `1` as `r` tends to `0`609(see `Besicovitch.ae_tendsto_measure_inter_div`).610When `μ` is a Haar measure, one can deduce the same property for any rescaling sequence of sets,611of the form `{x} + r • t` where `t` is a set with positive finite measure, instead of the sequence612of closed balls.613614We argue first for the dual property, i.e., if `s` has density `0` at `x`, then615`μ (s ∩ ({x} + r • t)) / μ ({x} + r • t)` tends to `0`. First when `t` is contained in the ball616of radius `1`, in `tendsto_addHaar_inter_smul_zero_of_density_zero_aux1`,617(by arguing by inclusion). Then when `t` is bounded, reducing to the previous one by rescaling, in618`tendsto_addHaar_inter_smul_zero_of_density_zero_aux2`.619Then for a general set `t`, by cutting it into a bounded part and a part with small measure, in620`tendsto_addHaar_inter_smul_zero_of_density_zero`.621Going to the complement, one obtains the desired property at points of density `1`, first when622`s` is measurable in `tendsto_addHaar_inter_smul_one_of_density_one_aux`, and then without this623assumption in `tendsto_addHaar_inter_smul_one_of_density_one` by applying the previous lemma to624the measurable hull `toMeasurable μ s`625-/626627theorem tendsto_addHaar_inter_smul_zero_of_density_zero_aux1 (s : Set E) (x : E)628 (h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)) (t : Set E)629 (u : Set E) (h'u : μ u ≠ 0) (t_bound : t ⊆ closedBall 0 1) :630 Tendsto (fun r : ℝ => μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)) (𝓝[>] 0) (𝓝 0) := by631 have A : Tendsto (fun r : ℝ => μ (s ∩ ({x} + r • t)) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0) := by632 apply633 tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds h634 (Eventually.of_forall fun b => zero_le)635 filter_upwards [self_mem_nhdsWithin]636 rintro r (rpos : 0 < r)637 grw [t_bound]638 rw [← vadd_eq_add, singleton_vadd, affinity_unitClosedBall rpos.le]639 have B :640 Tendsto (fun r : ℝ => μ (closedBall x r) / μ ({x} + r • u)) (𝓝[>] 0)641 (𝓝 (μ (closedBall x 1) / μ ({x} + u))) := by642 apply tendsto_const_nhds.congr' _643 filter_upwards [self_mem_nhdsWithin]644 rintro r (rpos : 0 < r)645 have : closedBall x r = {x} + r • closedBall (0 : E) 1 := by646 simp only [_root_.smul_closedBall, Real.norm_of_nonneg rpos.le, zero_le_one, add_zero,647 mul_one, singleton_add_closedBall, smul_zero]648 simp only [this, addHaar_singleton_add_smul_div_singleton_add_smul μ rpos.ne']649 simp only [addHaar_closedBall_center, image_add_left, measure_preimage_add, singleton_add]650 have C : Tendsto (fun r : ℝ =>651 μ (s ∩ ({x} + r • t)) / μ (closedBall x r) * (μ (closedBall x r) / μ ({x} + r • u)))652 (𝓝[>] 0) (𝓝 (0 * (μ (closedBall x 1) / μ ({x} + u)))) := by653 apply ENNReal.Tendsto.mul A _ B (Or.inr ENNReal.zero_ne_top)654 simp [ENNReal.div_eq_top, h'u, measure_closedBall_lt_top.ne]655 simp only [zero_mul] at C656 apply C.congr' _657 filter_upwards [self_mem_nhdsWithin]658 rintro r (rpos : 0 < r)659 calc μ (s ∩ ({x} + r • t)) / μ (closedBall x r) * (μ (closedBall x r) / μ ({x} + r • u))660 _ = μ (closedBall x r) * (μ (closedBall x r))⁻¹ *661 (μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)) := by simp only [div_eq_mul_inv]; ring662 _ = μ (s ∩ ({x} + r • t)) / μ ({x} + r • u) := by663 rw [ENNReal.mul_inv_cancel (measure_closedBall_pos μ x rpos).ne'664 measure_closedBall_lt_top.ne,665 one_mul]666667theorem tendsto_addHaar_inter_smul_zero_of_density_zero_aux2 (s : Set E) (x : E)668 (h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)) (t : Set E)669 (u : Set E) (h'u : μ u ≠ 0) (R : ℝ) (Rpos : 0 < R) (t_bound : t ⊆ closedBall 0 R) :670 Tendsto (fun r : ℝ => μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)) (𝓝[>] 0) (𝓝 0) := by671 set t' := R⁻¹ • t with ht'672 set u' := R⁻¹ • u with hu'673 have A : Tendsto (fun r : ℝ => μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) (𝓝[>] 0) (𝓝 0) := by674 apply tendsto_addHaar_inter_smul_zero_of_density_zero_aux1 μ s x h t' u'675 · simp only [u', h'u, (pow_pos Rpos _).ne', abs_nonpos_iff, addHaar_smul, not_false_iff,676 ENNReal.ofReal_eq_zero, inv_eq_zero, inv_pow, Ne, or_self_iff, mul_eq_zero]677 · refine (smul_set_mono t_bound).trans_eq ?_678 rw [smul_closedBall _ _ Rpos.le, smul_zero, Real.norm_of_nonneg (inv_nonneg.2 Rpos.le),679 inv_mul_cancel₀ Rpos.ne']680 have B : Tendsto (fun r : ℝ => R * r) (𝓝[>] 0) (𝓝[>] (R * 0)) := by681 apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within682 · exact (tendsto_const_nhds.mul tendsto_id).mono_left nhdsWithin_le_nhds683 · filter_upwards [self_mem_nhdsWithin]684 intro r rpos685 rw [mul_zero]686 exact mul_pos Rpos rpos687 rw [mul_zero] at B688 apply (A.comp B).congr' _689 filter_upwards [self_mem_nhdsWithin]690 rintro r -691 have T : (R * r) • t' = r • t := by692 rw [mul_comm, ht', smul_smul, mul_assoc, mul_inv_cancel₀ Rpos.ne', mul_one]693 have U : (R * r) • u' = r • u := by694 rw [mul_comm, hu', smul_smul, mul_assoc, mul_inv_cancel₀ Rpos.ne', mul_one]695 dsimp696 rw [T, U]697698/-- Consider a point `x` at which a set `s` has density zero, with respect to closed balls. Then it699also has density zero with respect to any measurable set `t`: the proportion of points in `s`700belonging to a rescaled copy `{x} + r • t` of `t` tends to zero as `r` tends to zero. -/701theorem tendsto_addHaar_inter_smul_zero_of_density_zero (s : Set E) (x : E)702 (h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)) (t : Set E)703 (ht : MeasurableSet t) (h''t : μ t ≠ ∞) :704 Tendsto (fun r : ℝ => μ (s ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0) := by705 refine tendsto_order.2 ⟨fun a' ha' => (ENNReal.not_lt_zero ha').elim, fun ε (εpos : 0 < ε) => ?_⟩706 rcases eq_or_ne (μ t) 0 with (h't | h't)707 · filter_upwards with r708 suffices H : μ (s ∩ ({x} + r • t)) = 0 by709 rw [H]; simpa only [ENNReal.zero_div] using εpos710 rw [← nonpos_iff_eq_zero]711 calc712 μ (s ∩ ({x} + r • t)) ≤ μ ({x} + r • t) := measure_mono inter_subset_right713 _ = 0 := by714 simp only [h't, addHaar_smul, image_add_left, measure_preimage_add, singleton_add,715 mul_zero]716 obtain ⟨n, npos, hn⟩ : ∃ n : ℕ, 0 < n ∧ μ (t \ closedBall 0 n) < ε / 2 * μ t := by717 have A :718 Tendsto (fun n : ℕ => μ (t \ closedBall 0 n)) atTop719 (𝓝 (μ (⋂ n : ℕ, t \ closedBall 0 n))) := by720 have N : ∃ n : ℕ, μ (t \ closedBall 0 n) ≠ ∞ :=721 ⟨0, ((measure_mono sdiff_subset).trans_lt h''t.lt_top).ne⟩722 refine tendsto_measure_iInter_atTop723 (fun n ↦ (ht.diff measurableSet_closedBall).nullMeasurableSet) (fun m n hmn ↦ ?_) N724 exact sdiff_subset_sdiff Subset.rfl (by gcongr)725 have : ⋂ n : ℕ, t \ closedBall 0 n = ∅ := by726 simp_rw [sdiff_eq, ← inter_iInter, iInter_eq_compl_iUnion_compl, compl_compl,727 iUnion_closedBall_nat, compl_univ, inter_empty]728 simp only [this, measure_empty] at A729 have I : 0 < ε / 2 * μ t := ENNReal.mul_pos (ENNReal.half_pos εpos.ne').ne' h't730 exact (Eventually.and (Ioi_mem_atTop 0) ((tendsto_order.1 A).2 _ I)).exists731 have L :732 Tendsto (fun r : ℝ => μ (s ∩ ({x} + r • (t ∩ closedBall 0 n))) / μ ({x} + r • t)) (𝓝[>] 0)733 (𝓝 0) :=734 tendsto_addHaar_inter_smul_zero_of_density_zero_aux2 μ s x h _ t h't n (Nat.cast_pos.2 npos)735 inter_subset_right736 filter_upwards [(tendsto_order.1 L).2 _ (ENNReal.half_pos εpos.ne'), self_mem_nhdsWithin]737 rintro r hr (rpos : 0 < r)738 have I :739 μ (s ∩ ({x} + r • t)) ≤740 μ (s ∩ ({x} + r • (t ∩ closedBall 0 n))) + μ ({x} + r • (t \ closedBall 0 n)) :=741 calc742 μ (s ∩ ({x} + r • t)) =743 μ (s ∩ ({x} + r • (t ∩ closedBall 0 n)) ∪ s ∩ ({x} + r • (t \ closedBall 0 n))) := by744 rw [← inter_union_distrib_left, ← add_union, ← smul_set_union, inter_union_sdiff]745 _ ≤ μ (s ∩ ({x} + r • (t ∩ closedBall 0 n))) + μ (s ∩ ({x} + r • (t \ closedBall 0 n))) :=746 measure_union_le _ _747 _ ≤ μ (s ∩ ({x} + r • (t ∩ closedBall 0 n))) + μ ({x} + r • (t \ closedBall 0 n)) := by748 gcongr; apply inter_subset_right749 calc750 μ (s ∩ ({x} + r • t)) / μ ({x} + r • t) ≤751 (μ (s ∩ ({x} + r • (t ∩ closedBall 0 n))) + μ ({x} + r • (t \ closedBall 0 n))) /752 μ ({x} + r • t) := by gcongr753 _ < ε / 2 + ε / 2 := by754 rw [ENNReal.add_div]755 apply ENNReal.add_lt_add hr _756 rwa [addHaar_singleton_add_smul_div_singleton_add_smul μ rpos.ne',757 ENNReal.div_lt_iff (Or.inl h't) (Or.inl h''t)]758 _ = ε := ENNReal.add_halves _759760theorem tendsto_addHaar_inter_smul_one_of_density_one_aux (s : Set E) (hs : MeasurableSet s)761 (x : E) (h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1))762 (t : Set E) (ht : MeasurableSet t) (h't : μ t ≠ 0) (h''t : μ t ≠ ∞) :763 Tendsto (fun r : ℝ => μ (s ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 1) := by764 have I : ∀ u v, μ u ≠ 0 → μ u ≠ ∞ → MeasurableSet v →765 μ u / μ u - μ (vᶜ ∩ u) / μ u = μ (v ∩ u) / μ u := by766 intro u v uzero utop vmeas767 simp_rw [div_eq_mul_inv]768 rw [← ENNReal.sub_mul]; swap769 · simp only [uzero, ENNReal.inv_eq_top, imp_true_iff, Ne, not_false_iff]770 congr 1771 rw [inter_comm _ u, inter_comm _ u, eq_comm]772 exact ENNReal.eq_sub_of_add_eq' utop (measure_inter_add_sdiff u vmeas)773 have L : Tendsto (fun r => μ (sᶜ ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0) := by774 have A : Tendsto (fun r => μ (closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1) := by775 apply tendsto_const_nhds.congr' _776 filter_upwards [self_mem_nhdsWithin]777 intro r hr778 rw [div_eq_mul_inv, ENNReal.mul_inv_cancel]779 · exact (measure_closedBall_pos μ _ hr).ne'780 · exact measure_closedBall_lt_top.ne781 have B := ENNReal.Tendsto.sub A h (Or.inl ENNReal.one_ne_top)782 simp only [tsub_self] at B783 apply B.congr' _784 filter_upwards [self_mem_nhdsWithin]785 rintro r (rpos : 0 < r)786 convert!787 I (closedBall x r) sᶜ (measure_closedBall_pos μ _ rpos).ne' measure_closedBall_lt_top.ne788 hs.compl789 rw [compl_compl]790 have L' : Tendsto (fun r : ℝ => μ (sᶜ ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0) :=791 tendsto_addHaar_inter_smul_zero_of_density_zero μ sᶜ x L t ht h''t792 have L'' : Tendsto (fun r : ℝ => μ ({x} + r • t) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 1) := by793 apply tendsto_const_nhds.congr' _794 filter_upwards [self_mem_nhdsWithin]795 rintro r (rpos : 0 < r)796 rw [addHaar_singleton_add_smul_div_singleton_add_smul μ rpos.ne', ENNReal.div_self h't h''t]797 have := ENNReal.Tendsto.sub L'' L' (Or.inl ENNReal.one_ne_top)798 simp only [tsub_zero] at this799 apply this.congr' _800 filter_upwards [self_mem_nhdsWithin]801 rintro r (rpos : 0 < r)802 refine I ({x} + r • t) s ?_ ?_ hs803 · simp only [h't, abs_of_nonneg rpos.le, pow_pos rpos, addHaar_smul, image_add_left,804 ENNReal.ofReal_eq_zero, not_le, or_false, Ne, measure_preimage_add, abs_pow,805 singleton_add, mul_eq_zero]806 · simp [h''t, ENNReal.ofReal_ne_top, addHaar_smul, image_add_left, ENNReal.mul_eq_top,807 Ne, measure_preimage_add, singleton_add]808809/-- Consider a point `x` at which a set `s` has density one, with respect to closed balls (i.e.,810a Lebesgue density point of `s`). Then `s` has also density one at `x` with respect to any811measurable set `t`: the proportion of points in `s` belonging to a rescaled copy `{x} + r • t`812of `t` tends to one as `r` tends to zero. -/813theorem tendsto_addHaar_inter_smul_one_of_density_one (s : Set E) (x : E)814 (h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)) (t : Set E)815 (ht : MeasurableSet t) (h't : μ t ≠ 0) (h''t : μ t ≠ ∞) :816 Tendsto (fun r : ℝ => μ (s ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 1) := by817 have : Tendsto (fun r : ℝ => μ (toMeasurable μ s ∩ ({x} + r • t)) / μ ({x} + r • t))818 (𝓝[>] 0) (𝓝 1) := by819 apply820 tendsto_addHaar_inter_smul_one_of_density_one_aux μ _ (measurableSet_toMeasurable _ _) _ _821 t ht h't h''t822 apply tendsto_of_tendsto_of_tendsto_of_le_of_le' h tendsto_const_nhds823 · refine Eventually.of_forall fun r ↦ ?_824 gcongr825 apply subset_toMeasurable826 · filter_upwards [self_mem_nhdsWithin]827 rintro r -828 apply ENNReal.div_le_of_le_mul829 rw [one_mul]830 exact measure_mono inter_subset_right831 refine this.congr fun r => ?_832 congr 1833 apply measure_toMeasurable_inter_of_sFinite834 simp only [image_add_left, singleton_add]835 apply (continuous_const_add (-x)).measurable (ht.const_smul₀ r)836837/-- Consider a point `x` at which a set `s` has density one, with respect to closed balls (i.e.,838a Lebesgue density point of `s`). Then `s` intersects the rescaled copies `{x} + r • t` of a given839set `t` with positive measure, for any small enough `r`. -/840theorem eventually_nonempty_inter_smul_of_density_one (s : Set E) (x : E)841 (h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)) (t : Set E)842 (ht : MeasurableSet t) (h't : μ t ≠ 0) :843 ∀ᶠ r in 𝓝[>] (0 : ℝ), (s ∩ ({x} + r • t)).Nonempty := by844 obtain ⟨t', t'_meas, t't, t'pos, t'top⟩ : ∃ t', MeasurableSet t' ∧ t' ⊆ t ∧ 0 < μ t' ∧ μ t' < ⊤ :=845 exists_subset_measure_lt_top ht h't.bot_lt846 filter_upwards [(tendsto_order.1847 (tendsto_addHaar_inter_smul_one_of_density_one μ s x h t' t'_meas t'pos.ne' t'top.ne)).1848 0 zero_lt_one]849 intro r hr850 have : μ (s ∩ ({x} + r • t')) ≠ 0 := fun h' => by851 simp only [ENNReal.not_lt_zero, ENNReal.zero_div, h'] at hr852 have : (s ∩ ({x} + r • t')).Nonempty := nonempty_of_measure_ne_zero this853 apply this.mono (inter_subset_inter Subset.rfl _)854 exact add_subset_add Subset.rfl (smul_set_mono t't)855856end Measure857858end MeasureTheory