Haar measure under dilations and affine maps

The dimension root of outer volume scales by the absolute value of a real dilation in a positive-dimensional real inner product space. The identity applies to arbitrary sets and infinite outer volumes, and supplies the scaling law for volume inequalities.

An affine map of a finite-dimensional real normed space multiplies every additive Haar measure by the absolute value of the determinant of its linear part (MeasureTheory.Measure.addHaar_image_affineMap, and MeasureTheory.Measure.addHaar_image_affineEquiv for affine equivalences), the affine form of Mathlib's MeasureTheory.Measure.addHaar_image_linearMap. The affine dilation y ↦ x + r • y, r ≠ 0, is quasi-measure-preserving for every additive Haar measure (MeasureTheory.Measure.quasiMeasurePreserving_add_smul), and it scales measures by the inverse dimension power of |r| (MeasureTheory.Measure.addHaar_preimage_add_smul), in particular the measure of the part of a set in a ball or closed ball (MeasureTheory.Measure.addHaar_preimage_add_smul_inter_ball, MeasureTheory.Measure.addHaar_preimage_add_smul_inter_closedBall).

A linear map into a finite-dimensional real normed space that is not surjective has almost every fibre empty for every additive Haar measure on the codomain (LinearMap.ae_preimage_singleton_eq_empty), since its range is a strict subspace.

For an invertible real square matrix A and nonnegative bounds a i, the region {x | ∀ i, |(A *ᵥ x) i| ≤ a i} cut out by the linear forms of A has volume 2 ^ n * (∏ i, a i) / |det A|, where n is the size of A (Matrix.volume_setOf_forall_abs_mulVec_le). It is the preimage of a coordinate box under A; this is the volume computation behind Minkowski's linear forms theorem.

We also bound the additive Haar measure of the closure of a set in a finite-dimensional real normed space by the measure of the unit ball times the dimension power of its diameter. This is the elementary estimate converting coverings by sets of small diameter into measure bounds. Combined with the diameter bound for Lipschitz images, it bounds the measure of the closure of the image of a set under a Lipschitz map.

An element of finite order acting linearly on a finite-dimensional real space preserves every additive Haar measure, because its determinant has finite order and so absolute value one (MeasureTheory.Measure.addHaar_preimage_smul_of_isOfFinOrder). Hence a finite group acting linearly preserves every additive Haar measure (MeasureTheory.Measure.smulInvariantMeasure_addHaar).

theorem TauCeti.volume_smul_rpow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {A : Set E} (hn : Module.finrank ℝ E ≠ 0) (c : ℝ) : MeasureTheory.volume (c • A) ^ (↑(Module.finrank ℝ E))⁻¹ = ENNReal.ofReal |c| * MeasureTheory.volume A ^ (↑(Module.finrank ℝ E))⁻¹

Dimension-root volume scales linearly under every real dilation, including zero. This identity holds for arbitrary sets and infinite outer volumes.

theorem MeasureTheory.Measure.addHaar_image_affineMap {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] (μ : Measure F) [μ.IsAddHaarMeasure] (f : F →ᵃ[ℝ] F) (s : Set F) : μ (⇑f '' s) = ENNReal.ofReal |LinearMap.det f.linear| * μ s

The image of a set under an affine map has Haar measure equal to the absolute value of the determinant of the linear part times the measure of the set.

theorem MeasureTheory.Measure.addHaar_image_affineEquiv {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] (μ : Measure F) [μ.IsAddHaarMeasure] (f : F ≃ᵃ[ℝ] F) (s : Set F) : μ (⇑f '' s) = ENNReal.ofReal |LinearMap.det ↑f.linear| * μ s

The image of a set under an affine equivalence has Haar measure equal to the absolute value of the determinant of the linear part times the measure of the set.

theorem MeasureTheory.Measure.quasiMeasurePreserving_add_smul {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] (μ : Measure F) [μ.IsAddHaarMeasure] (x : F) {r : ℝ} (hr : r ≠ 0) : QuasiMeasurePreserving (fun (y : F) => x + r • y) μ μ

The affine dilation y ↦ x + r • y with r ≠ 0 is quasi-measure-preserving for an additive Haar measure, so preimages under it of null-measurable sets are null-measurable.

theorem MeasureTheory.Measure.addHaar_preimage_add_smul {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] (μ : Measure F) [μ.IsAddHaarMeasure] (x : F) {r : ℝ} (hr : r ≠ 0) (s : Set F) : μ ((fun (y : F) => x + r • y) ⁻¹' s) = ENNReal.ofReal |(r ^ Module.finrank ℝ F)⁻¹| * μ s

The volume of a blow-up. For r ≠ 0, the preimage of s under the affine dilation y ↦ x + r • y has measure |r| ^ (-n) μ s, where n = dim F.

theorem MeasureTheory.Measure.addHaar_preimage_add_smul_inter_ball {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] (μ : Measure F) [μ.IsAddHaarMeasure] (x : F) {r : ℝ} (hr : r ≠ 0) (s : Set F) (ρ : ℝ) : μ ((fun (y : F) => x + r • y) ⁻¹' s ∩ Metric.ball 0 ρ) = ENNReal.ofReal |(r ^ Module.finrank ℝ F)⁻¹| * μ (s ∩ Metric.ball x (|r| * ρ))

The volume of a blow-up in a ball. For r ≠ 0, the preimage of s under the affine dilation y ↦ x + r • y satisfies μ(s_{x,r} ∩ ball 0 ρ) = |r| ^ (-n) μ(s ∩ ball x (|r| * ρ)), where n = dim F.

theorem MeasureTheory.Measure.addHaar_preimage_add_smul_inter_closedBall {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] (μ : Measure F) [μ.IsAddHaarMeasure] (x : F) {r : ℝ} (hr : r ≠ 0) (s : Set F) (ρ : ℝ) : μ ((fun (y : F) => x + r • y) ⁻¹' s ∩ Metric.closedBall 0 ρ) = ENNReal.ofReal |(r ^ Module.finrank ℝ F)⁻¹| * μ (s ∩ Metric.closedBall x (|r| * ρ))

The volume of a blow-up in a closed ball. For r ≠ 0, the preimage of s under the affine dilation y ↦ x + r • y satisfies μ(s_{x,r} ∩ closedBall 0 ρ) = |r| ^ (-n) μ(s ∩ closedBall x (|r| * ρ)), where n = dim F.

theorem MeasureTheory.Measure.addHaar_closure_le_mul_ediam_pow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (s : Set E) : μ (closure s) ≤ μ (Metric.ball 0 1) * Metric.ediam s ^ Module.finrank ℝ E

The closure of a set of diameter d in an n-dimensional real normed space has additive Haar measure at most μ (ball 0 1) * d ^ n, since it lies in a closed ball of radius d. This holds for every set, including empty and unbounded ones.

theorem MeasureTheory.Measure.addHaar_preimage_smul_of_isOfFinOrder {G : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] [Monoid G] [DistribMulAction G E] [SMulCommClass G ℝ E] {g : G} (hg : IsOfFinOrder g) (s : Set E) : μ ((fun (x : E) => g • x) ⁻¹' s) = μ s

An element of finite order acting linearly on a finite-dimensional real space preserves every additive Haar measure. Its determinant has finite order in ℝ, hence absolute value one.

theorem MeasureTheory.Measure.smulInvariantMeasure_addHaar {G : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] [Group G] [Finite G] [DistribMulAction G E] [SMulCommClass G ℝ E] : SMulInvariantMeasure G E μ

A finite group acting linearly on a finite-dimensional real space preserves every additive Haar measure.

theorem LinearMap.ae_preimage_singleton_eq_empty {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] (μ : MeasureTheory.Measure F) [μ.IsAddHaarMeasure] (L : E →ₗ[ℝ] F) (hL : ¬Function.Surjective ⇑L) : ∀ᵐ (y : F) ∂μ, ⇑L ⁻¹' {y} = ∅

A linear map that is not surjective has almost every fibre empty, for every additive Haar measure on its finite-dimensional codomain.

theorem Matrix.volume_setOf_forall_abs_mulVec_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι ℝ) (hA : A.det ≠ 0) {a : ι → ℝ} (ha : 0 ≤ a) : MeasureTheory.volume {x : ι → ℝ | ∀ (i : ι), |A.mulVec x i| ≤ a i} = ENNReal.ofReal ((2 ^ Fintype.card ι * ∏ i : ι, a i) / |A.det|)

The region cut out by the linear forms of an invertible real square matrix A: for nonnegative bounds a i, the set of x : ι → ℝ with |(A *ᵥ x) i| ≤ a i for every i has volume 2 ^ n * (∏ i, a i) / |det A|, where n is the cardinality of ι. This includes the case of an empty ι, where both sides are 1.

theorem LipschitzOnWith.addHaar_closure_image_le_mul_ediam_pow {X : Type u_1} {E : Type u_2} [PseudoEMetricSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {K : NNReal} {f : X → E} {A : Set X} (hf : LipschitzOnWith K f A) : μ (closure (f '' A)) ≤ μ (Metric.ball 0 1) * ↑K ^ Module.finrank ℝ E * Metric.ediam A ^ Module.finrank ℝ E

The closure of the image of a set A under a K-Lipschitz map into an n-dimensional real normed space has additive Haar measure at most μ (ball 0 1) * K ^ n * ediam A ^ n.