# Relationship between the Haar and Lebesgue measures #

We prove that the Haar measure and Lebesgue measure are equal on `ℝ` and on `ℝ^ι`, in `MeasureTheory.addHaarMeasure_eq_volume` and `MeasureTheory.addHaarMeasure_eq_volume_pi`.

We deduce basic properties of any Haar measure on a finite-dimensional real vector space:

- `map_linearMap_addHaar_eq_smul_addHaar`: a linear map rescales the Haar measure by the absolute value of its determinant.
- `addHaar_preimage_linearMap` : when `f` is a linear map with nonzero determinant, the measure of `f ⁻¹' s` is the measure of `s` multiplied by the absolute value of the inverse of the determinant of `f`.
- `addHaar_image_linearMap` : when `f` is a linear map, the measure of `f '' s` is the measure of `s` multiplied by the absolute value of the determinant of `f`.
- `addHaar_submodule` : a strict submodule has measure `0`.
- `addHaar_smul` : the measure of `r • s` is `|r| ^ dim * μ s`.
- `addHaar_ball`: the measure of `ball x r` is `r ^ dim * μ (ball 0 1)`.
- `addHaar_closedBall`: the measure of `closedBall x r` is `r ^ dim * μ (ball 0 1)`.
- `addHaar_sphere`: spheres have zero measure.

This makes it possible to associate a Lebesgue measure to an `n`-alternating map in dimension `n`. This measure is called `AlternatingMap.measure`. Its main property is `ω.measure_parallelepiped v`, stating that the associated measure of the parallelepiped spanned by vectors `v₁, ..., vₙ` is given by `|ω v|`.

We also show that a Lebesgue density point `x` of a set `s` (with respect to closed balls) has density one for the rescaled copies `{x} + r • t` of a given set `t` with positive measure, in `tendsto_addHaar_inter_smul_one_of_density_one`. In particular, `s` intersects `{x} + r • t` for small `r`, see `eventually_nonempty_inter_smul_of_density_one`.

Statements on integrals of functions with respect to an additive Haar measure can be found in `MeasureTheory.Measure.Haar.NormedSpace`.

source
def TopologicalSpace.PositiveCompacts.Icc01 :
PositiveCompacts ℝ

The interval `[0,1]` as a compact set with non-empty interior.

Equations

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

Instances For

source
def TopologicalSpace.PositiveCompacts.piIcc01 (ι : Type u_1) [Finite ι] :
PositiveCompacts (ι → ℝ)

The set `[0,1]^ι` as a compact set with non-empty interior.

Equations

- TopologicalSpace.PositiveCompacts.piIcc01 ι = { carrier := Set.univ.pi fun (x : ι) => Set.Icc 0 1, isCompact' := ⋯, interior_nonempty' := ⋯ }

Instances For

source
theorem Module.Basis.parallelepiped_basisFun (ι : Type u_1) [Fintype ι] :
(Pi.basisFun ℝ ι).parallelepiped = TopologicalSpace.PositiveCompacts.piIcc01 ι

The parallelepiped formed from the standard basis for `ι → ℝ` is `[0,1]^ι`

source
theorem Module.Basis.parallelepiped_eq_map {ι : Type u_1} {E : Type u_2} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] (b : Basis ι ℝ E) :
b.parallelepiped = TopologicalSpace.PositiveCompacts.map ⇑b.equivFun.symm ⋯ ⋯ (TopologicalSpace.PositiveCompacts.piIcc01 ι)

A parallelepiped can be expressed on the standard basis.

source
theorem Module.Basis.map_addHaar {ι : Type u_1} {E : Type u_2} {F : Type u_3} [Fintype ι] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] [MeasurableSpace E] [MeasurableSpace F] [BorelSpace E] [BorelSpace F] [SecondCountableTopology F] [SigmaCompactSpace F] (b : Basis ι ℝ E) (f : E ≃L[ℝ] F) :
MeasureTheory.Measure.map (⇑f) b.addHaar = (b.map f.toLinearEquiv).addHaar

### The Lebesgue measure is a Haar measure on `ℝ` and on `ℝ^ι`. #

source
theorem MeasureTheory.addHaarMeasure_eq_volume :
Measure.addHaarMeasure TopologicalSpace.PositiveCompacts.Icc01 = volume

The Haar measure equals the Lebesgue measure on `ℝ`.

source
theorem MeasureTheory.addHaarMeasure_eq_volume_pi (ι : Type u_1) [Fintype ι] :
Measure.addHaarMeasure (TopologicalSpace.PositiveCompacts.piIcc01 ι) = volume

The Haar measure equals the Lebesgue measure on `ℝ^ι`.

source
theorem MeasureTheory.isAddHaarMeasure_volume_pi (ι : Type u_1) [Fintype ι] :
volume.IsAddHaarMeasure

### Strict subspaces have zero measure #

source
theorem MeasureTheory.Measure.addHaar_eq_zero_of_disjoint_translates_aux {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] {s : Set E} (u : ℕ → E) (sb : Bornology.IsBounded s) (hu : Bornology.IsBounded (Set.range u)) (hs : Pairwise (Function.onFun Disjoint fun (n : ℕ) => {u n} + s)) (h's : MeasurableSet s) :
μ s = 0

If a set is disjoint of its translates by infinitely many bounded vectors, then it has measure zero. This auxiliary lemma proves this assuming additionally that the set is bounded.

source
theorem MeasureTheory.Measure.addHaar_eq_zero_of_disjoint_translates {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] {s : Set E} (u : ℕ → E) (hu : Bornology.IsBounded (Set.range u)) (hs : Pairwise (Function.onFun Disjoint fun (n : ℕ) => {u n} + s)) (h's : MeasurableSet s) :
μ s = 0

If a set is disjoint of its translates by infinitely many bounded vectors, then it has measure zero.

source
theorem MeasureTheory.Measure.addHaar_submodule {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (s : Submodule ℝ E) (hs : s ≠ ⊤) :
μ ↑s = 0

A strict vector subspace has measure zero.

source
theorem MeasureTheory.Measure.addHaar_affineSubspace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (s : AffineSubspace ℝ E) (hs : s ≠ ⊤) :
μ ↑s = 0

A strict affine subspace has measure zero.

### Applying a linear map rescales Haar measure by the determinant #

We first prove this on `ι → ℝ`, using that this is already known for the product Lebesgue measure (thanks to matrices computations). Then, we extend this to any finite-dimensional real vector space by using a linear equiv with a space of the form `ι → ℝ`, and arguing that such a linear equiv maps Haar measure to Haar measure.

source
theorem MeasureTheory.Measure.map_linearMap_addHaar_pi_eq_smul_addHaar {ι : Type u_1} [Finite ι] {f : (ι → ℝ) →ₗ[ℝ] ι → ℝ} (hf : LinearMap.det f ≠ 0) (μ : Measure (ι → ℝ)) [μ.IsAddHaarMeasure] :
map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ
source
theorem MeasureTheory.Measure.map_linearMap_addHaar_eq_smul_addHaar {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] {f : E →ₗ[ℝ] E} (hf : LinearMap.det f ≠ 0) :
map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ
source
@[simp]
theorem MeasureTheory.Measure.addHaar_preimage_linearMap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] {f : E →ₗ[ℝ] E} (hf : LinearMap.det f ≠ 0) (s : Set E) :
μ (⇑f ⁻¹' s) = ENNReal.ofReal |(LinearMap.det f)⁻¹| * μ s

The preimage of a set `s` under a linear map `f` with nonzero determinant has measure equal to `μ s` times the absolute value of the inverse of the determinant of `f`.

source
@[simp]
theorem MeasureTheory.Measure.addHaar_preimage_continuousLinearMap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] {f : E →L[ℝ] E} (hf : LinearMap.det ↑f ≠ 0) (s : Set E) :
μ (⇑f ⁻¹' s) = ENNReal.ofReal |(LinearMap.det ↑f)⁻¹| * μ s

The preimage of a set `s` under a continuous linear map `f` with nonzero determinant has measure equal to `μ s` times the absolute value of the inverse of the determinant of `f`.

source
@[simp]
theorem MeasureTheory.Measure.addHaar_preimage_linearEquiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (f : E ≃ₗ[ℝ] E) (s : Set E) :
μ (⇑f ⁻¹' s) = ENNReal.ofReal |LinearMap.det ↑f.symm| * μ s

The preimage of a set `s` under a linear equiv `f` has measure equal to `μ s` times the absolute value of the inverse of the determinant of `f`.

source
@[simp]
theorem MeasureTheory.Measure.addHaar_preimage_continuousLinearEquiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (f : E ≃L[ℝ] E) (s : Set E) :
μ (⇑f ⁻¹' s) = ENNReal.ofReal |LinearMap.det ↑↑f.symm| * μ s

The preimage of a set `s` under a continuous linear equiv `f` has measure equal to `μ s` times the absolute value of the inverse of the determinant of `f`.

source
@[simp]
theorem MeasureTheory.Measure.addHaar_image_linearMap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (f : E →ₗ[ℝ] E) (s : Set E) :
μ (⇑f '' s) = ENNReal.ofReal |LinearMap.det f| * μ s

The image of a set `s` under a linear map `f` has measure equal to `μ s` times the absolute value of the determinant of `f`.

source
@[simp]
theorem MeasureTheory.Measure.addHaar_image_continuousLinearMap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (f : E →L[ℝ] E) (s : Set E) :
μ (⇑f '' s) = ENNReal.ofReal |LinearMap.det ↑f| * μ s

The image of a set `s` under a continuous linear map `f` has measure equal to `μ s` times the absolute value of the determinant of `f`.

source
@[simp]
theorem MeasureTheory.Measure.addHaar_image_continuousLinearEquiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (f : E ≃L[ℝ] E) (s : Set E) :
μ (⇑f '' s) = ENNReal.ofReal |LinearMap.det ↑↑f| * μ s

The image of a set `s` under a continuous linear equiv `f` has measure equal to `μ s` times the absolute value of the determinant of `f`.

source
theorem MeasureTheory.Measure.LinearMap.quasiMeasurePreserving {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (f : E →ₗ[ℝ] E) (hf : LinearMap.det f ≠ 0) :
QuasiMeasurePreserving (⇑f) μ μ
source
theorem MeasureTheory.Measure.ContinuousLinearMap.quasiMeasurePreserving {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (f : E →L[ℝ] E) (hf : f.det ≠ 0) :
QuasiMeasurePreserving (⇑f) μ μ

### Basic properties of Haar measures on real vector spaces #

source
theorem MeasureTheory.Measure.map_addHaar_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] {r : ℝ} (hr : r ≠ 0) :
map (fun (x : E) => r • x) μ = ENNReal.ofReal |(r ^ Module.finrank ℝ E)⁻¹| • μ
source
theorem MeasureTheory.Measure.quasiMeasurePreserving_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] {r : ℝ} (hr : r ≠ 0) :
QuasiMeasurePreserving (fun (x : E) => r • x) μ μ
source
@[simp]
theorem MeasureTheory.Measure.addHaar_preimage_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] {r : ℝ} (hr : r ≠ 0) (s : Set E) :
μ ((fun (x : E) => r • x) ⁻¹' s) = ENNReal.ofReal |(r ^ Module.finrank ℝ E)⁻¹| * μ s
source
@[simp]
theorem MeasureTheory.Measure.addHaar_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (r : ℝ) (s : Set E) :
μ (r • s) = ENNReal.ofReal |r ^ Module.finrank ℝ E| * μ s

Rescaling a set by a factor `r` multiplies its measure by `abs (r ^ dim)`.

source
theorem MeasureTheory.Measure.addHaar_smul_of_nonneg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] {r : ℝ} (hr : 0 ≤ r) (s : Set E) :
μ (r • s) = ENNReal.ofReal (r ^ Module.finrank ℝ E) * μ s
source
theorem MeasureTheory.Measure.NullMeasurableSet.const_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] {μ : Measure E} [μ.IsAddHaarMeasure] {s : Set E} (hs : NullMeasurableSet s μ) (r : ℝ) :
NullMeasurableSet (r • s) μ
source
@[simp]
theorem MeasureTheory.Measure.addHaar_image_homothety {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (x : E) (r : ℝ) (s : Set E) :
μ (⇑(AffineMap.homothety x r) '' s) = ENNReal.ofReal |r ^ Module.finrank ℝ E| * μ s

We don't need to state `map_addHaar_neg` here, because it has already been proved for general Haar measures on general commutative groups.

### Measure of balls #

source
theorem MeasureTheory.Measure.addHaar_ball_center {E : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (x : E) (r : ℝ) :
μ (Metric.ball x r) = μ (Metric.ball 0 r)
source
theorem MeasureTheory.Measure.addHaar_real_ball_center {E : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (x : E) (r : ℝ) :
μ.real (Metric.ball x r) = μ.real (Metric.ball 0 r)
source
theorem MeasureTheory.Measure.addHaar_closedBall_center {E : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (x : E) (r : ℝ) :
μ (Metric.closedBall x r) = μ (Metric.closedBall 0 r)
source
theorem MeasureTheory.Measure.addHaar_real_closedBall_center {E : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (x : E) (r : ℝ) :
μ.real (Metric.closedBall x r) = μ.real (Metric.closedBall 0 r)
source
theorem MeasureTheory.Measure.addHaar_ball_mul_of_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (x : E) {r : ℝ} (hr : 0 < r) (s : ℝ) :
μ (Metric.ball x (r * s)) = ENNReal.ofReal (r ^ Module.finrank ℝ E) * μ (Metric.ball 0 s)
source
theorem MeasureTheory.Measure.addHaar_ball_of_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (x : E) {r : ℝ} (hr : 0 < r) :
μ (Metric.ball x r) = ENNReal.ofReal (r ^ Module.finrank ℝ E) * μ (Metric.ball 0 1)
source
theorem MeasureTheory.Measure.addHaar_ball_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] [Nontrivial E] (x : E) {r : ℝ} (hr : 0 ≤ r) (s : ℝ) :
μ (Metric.ball x (r * s)) = ENNReal.ofReal (r ^ Module.finrank ℝ E) * μ (Metric.ball 0 s)
source
theorem MeasureTheory.Measure.addHaar_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] [Nontrivial E] (x : E) {r : ℝ} (hr : 0 ≤ r) :
μ (Metric.ball x r) = ENNReal.ofReal (r ^ Module.finrank ℝ E) * μ (Metric.ball 0 1)
source
theorem MeasureTheory.Measure.addHaar_closedBall_mul_of_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (x : E) {r : ℝ} (hr : 0 < r) (s : ℝ) :
μ (Metric.closedBall x (r * s)) = ENNReal.ofReal (r ^ Module.finrank ℝ E) * μ (Metric.closedBall 0 s)
source
theorem MeasureTheory.Measure.addHaar_closedBall_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (x : E) {r : ℝ} (hr : 0 ≤ r) {s : ℝ} (hs : 0 ≤ s) :
μ (Metric.closedBall x (r * s)) = ENNReal.ofReal (r ^ Module.finrank ℝ E) * μ (Metric.closedBall 0 s)
source
theorem MeasureTheory.Measure.addHaar_closedBall' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (x : E) {r : ℝ} (hr : 0 ≤ r) :
μ (Metric.closedBall x r) = ENNReal.ofReal (r ^ Module.finrank ℝ E) * μ (Metric.closedBall 0 1)

The measure of a closed ball can be expressed in terms of the measure of the closed unit ball. Use instead `addHaar_closedBall`, which uses the measure of the open unit ball as a standard form.

source
theorem MeasureTheory.Measure.addHaar_real_closedBall' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (x : E) {r : ℝ} (hr : 0 ≤ r) :
μ.real (Metric.closedBall x r) = r ^ Module.finrank ℝ E * μ.real (Metric.closedBall 0 1)
source
theorem MeasureTheory.Measure.addHaar_unitClosedBall_eq_addHaar_unitBall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] :
μ (Metric.closedBall 0 1) = μ (Metric.ball 0 1)
source
theorem MeasureTheory.Measure.addHaar_closedBall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (x : E) {r : ℝ} (hr : 0 ≤ r) :
μ (Metric.closedBall x r) = ENNReal.ofReal (r ^ Module.finrank ℝ E) * μ (Metric.ball 0 1)
source
theorem MeasureTheory.Measure.addHaar_real_closedBall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (x : E) {r : ℝ} (hr : 0 ≤ r) :
μ.real (Metric.closedBall x r) = r ^ Module.finrank ℝ E * μ.real (Metric.ball 0 1)
source
theorem MeasureTheory.Measure.addHaar_closedBall_eq_addHaar_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] [Nontrivial E] (x : E) (r : ℝ) :
μ (Metric.closedBall x r) = μ (Metric.ball x r)
source
theorem MeasureTheory.Measure.addHaar_real_closedBall_eq_addHaar_real_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] [Nontrivial E] (x : E) (r : ℝ) :
μ.real (Metric.closedBall x r) = μ.real (Metric.ball x r)
source
theorem MeasureTheory.Measure.addHaar_sphere_of_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (x : E) {r : ℝ} (hr : r ≠ 0) :
μ (Metric.sphere x r) = 0
source
theorem MeasureTheory.Measure.addHaar_sphere {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] [Nontrivial E] (x : E) (r : ℝ) :
μ (Metric.sphere x r) = 0
source
theorem MeasureTheory.Measure.addHaar_singleton_add_smul_div_singleton_add_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] {r : ℝ} (hr : r ≠ 0) (x y : E) (s t : Set E) :
μ ({x} + r • s) / μ ({y} + r • t) = μ s / μ t
source
@[instance 100]
instance MeasureTheory.Measure.isUnifLocDoublingMeasureOfIsAddHaarMeasure {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] :
IsUnifLocDoublingMeasure μ

### The Lebesgue measure associated to an alternating map #

source
theorem MeasureTheory.Measure.addHaar_parallelepiped {ι : Type u_2} {G : Type u_3} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup G] [NormedSpace ℝ G] [MeasurableSpace G] [BorelSpace G] (b : Module.Basis ι ℝ G) (v : ι → G) :
b.addHaar (parallelepiped v) = ENNReal.ofReal |b.det v|
source
theorem AlternatingMap.measure_def {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] [MeasurableSpace G] [BorelSpace G] [FiniteDimensional ℝ G] {n : ℕ} [_i : Fact (Module.finrank ℝ G = n)] (ω : G [⋀^Fin n]→ₗ[ℝ] ℝ) :
ω.measure = ‖ω ⇑(Module.finBasisOfFinrankEq ℝ G ⋯)‖₊ • (Module.finBasisOfFinrankEq ℝ G ⋯).addHaar
source
@[irreducible]
noncomputable def AlternatingMap.measure {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] [MeasurableSpace G] [BorelSpace G] [FiniteDimensional ℝ G] {n : ℕ} [_i : Fact (Module.finrank ℝ G = n)] (ω : G [⋀^Fin n]→ₗ[ℝ] ℝ) :
MeasureTheory.Measure G

The Lebesgue measure associated to an alternating map. It gives measure `|ω v|` to the parallelepiped spanned by the vectors `v₁, ..., vₙ`. Note that it is not always a Haar measure, as it can be zero, but it is always locally finite and translation invariant.

Equations

- ω.measure = ‖ω ⇑(Module.finBasisOfFinrankEq ℝ G ⋯)‖₊ • (Module.finBasisOfFinrankEq ℝ G ⋯).addHaar

Instances For

source
theorem AlternatingMap.measure_parallelepiped {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] [MeasurableSpace G] [BorelSpace G] [FiniteDimensional ℝ G] {n : ℕ} [_i : Fact (Module.finrank ℝ G = n)] (ω : G [⋀^Fin n]→ₗ[ℝ] ℝ) (v : Fin n → G) :
ω.measure (parallelepiped v) = ENNReal.ofReal |ω v|
source
instance MeasureTheory.Measure.instIsAddLeftInvariantMeasure {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] [MeasurableSpace G] [BorelSpace G] [FiniteDimensional ℝ G] {n : ℕ} [_i : Fact (Module.finrank ℝ G = n)] (ω : G [⋀^Fin n]→ₗ[ℝ] ℝ) :
ω.measure.IsAddLeftInvariant
source
instance MeasureTheory.Measure.instIsLocallyFiniteMeasureMeasure {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] [MeasurableSpace G] [BorelSpace G] [FiniteDimensional ℝ G] {n : ℕ} [_i : Fact (Module.finrank ℝ G = n)] (ω : G [⋀^Fin n]→ₗ[ℝ] ℝ) :
IsLocallyFiniteMeasure ω.measure

### Density points #

Besicovitch covering theorem ensures that, for any locally finite measure on a finite-dimensional real vector space, almost every point of a set `s` is a density point, i.e., `μ (s ∩ closedBall x r) / μ (closedBall x r)` tends to `1` as `r` tends to `0` (see `Besicovitch.ae_tendsto_measure_inter_div`). When `μ` is a Haar measure, one can deduce the same property for any rescaling sequence of sets, of the form `{x} + r • t` where `t` is a set with positive finite measure, instead of the sequence of closed balls.

We argue first for the dual property, i.e., if `s` has density `0` at `x`, then `μ (s ∩ ({x} + r • t)) / μ ({x} + r • t)` tends to `0`. First when `t` is contained in the ball of radius `1`, in `tendsto_addHaar_inter_smul_zero_of_density_zero_aux1`, (by arguing by inclusion). Then when `t` is bounded, reducing to the previous one by rescaling, in `tendsto_addHaar_inter_smul_zero_of_density_zero_aux2`. Then for a general set `t`, by cutting it into a bounded part and a part with small measure, in `tendsto_addHaar_inter_smul_zero_of_density_zero`. Going to the complement, one obtains the desired property at points of density `1`, first when `s` is measurable in `tendsto_addHaar_inter_smul_one_of_density_one_aux`, and then without this assumption in `tendsto_addHaar_inter_smul_one_of_density_one` by applying the previous lemma to the measurable hull `toMeasurable μ s`

source
theorem MeasureTheory.Measure.tendsto_addHaar_inter_smul_zero_of_density_zero_aux1 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (s : Set E) (x : E) (h : Filter.Tendsto (fun (r : ℝ) => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) (t u : Set E) (h'u : μ u ≠ 0) (t_bound : t ⊆ Metric.closedBall 0 1) :
Filter.Tendsto (fun (r : ℝ) => μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
source
theorem MeasureTheory.Measure.tendsto_addHaar_inter_smul_zero_of_density_zero_aux2 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (s : Set E) (x : E) (h : Filter.Tendsto (fun (r : ℝ) => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) (t u : Set E) (h'u : μ u ≠ 0) (R : ℝ) (Rpos : 0 < R) (t_bound : t ⊆ Metric.closedBall 0 R) :
Filter.Tendsto (fun (r : ℝ) => μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
source
theorem MeasureTheory.Measure.tendsto_addHaar_inter_smul_zero_of_density_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (s : Set E) (x : E) (h : Filter.Tendsto (fun (r : ℝ) => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) (t : Set E) (ht : MeasurableSet t) (h''t : μ t ≠ ⊤) :
Filter.Tendsto (fun (r : ℝ) => μ (s ∩ ({x} + r • t)) / μ ({x} + r • t)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Consider a point `x` at which a set `s` has density zero, with respect to closed balls. Then it also has density zero with respect to any measurable set `t`: the proportion of points in `s` belonging to a rescaled copy `{x} + r • t` of `t` tends to zero as `r` tends to zero.

source
theorem MeasureTheory.Measure.tendsto_addHaar_inter_smul_one_of_density_one_aux {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (s : Set E) (hs : MeasurableSet s) (x : E) (h : Filter.Tendsto (fun (r : ℝ) => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)) (t : Set E) (ht : MeasurableSet t) (h't : μ t ≠ 0) (h''t : μ t ≠ ⊤) :
Filter.Tendsto (fun (r : ℝ) => μ (s ∩ ({x} + r • t)) / μ ({x} + r • t)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)
source
theorem MeasureTheory.Measure.tendsto_addHaar_inter_smul_one_of_density_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (s : Set E) (x : E) (h : Filter.Tendsto (fun (r : ℝ) => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)) (t : Set E) (ht : MeasurableSet t) (h't : μ t ≠ 0) (h''t : μ t ≠ ⊤) :
Filter.Tendsto (fun (r : ℝ) => μ (s ∩ ({x} + r • t)) / μ ({x} + r • t)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)

Consider a point `x` at which a set `s` has density one, with respect to closed balls (i.e., a Lebesgue density point of `s`). Then `s` has also density one at `x` with respect to any measurable set `t`: the proportion of points in `s` belonging to a rescaled copy `{x} + r • t` of `t` tends to one as `r` tends to zero.

source
theorem MeasureTheory.Measure.eventually_nonempty_inter_smul_of_density_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (s : Set E) (x : E) (h : Filter.Tendsto (fun (r : ℝ) => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)) (t : Set E) (ht : MeasurableSet t) (h't : μ t ≠ 0) :
∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), (s ∩ ({x} + r • t)).Nonempty

Consider a point `x` at which a set `s` has density one, with respect to closed balls (i.e., a Lebesgue density point of `s`). Then `s` intersects the rescaled copies `{x} + r • t` of a given set `t` with positive measure, for any small enough `r`.