Pushing a Haar measure by a linear map

We show that the push-forward of an additive Haar measure in a vector space under a surjective linear map is proportional to the Haar measure on the target space, in LinearMap.exists_map_addHaar_eq_smul_addHaar.

We deduce disintegration properties of the Haar measure: to check that a property is true ae, it suffices to check that it is true ae along all translates of a given vector subspace. See MeasureTheory.ae_mem_of_ae_add_linearMap_mem.

TODO: this holds more generally in any locally compact group, see Fremlin, Measure Theory (volume 4, 443Q)

instance instBorelSpaceSubtypeMemSubmodule {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [NormedSpace 𝕜 E] (T : Submodule 𝕜 E) : BorelSpace ↥T

instance instOpensMeasurableSpaceSubtypeMemSubmodule {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [NormedSpace 𝕜 E] (T : Submodule 𝕜 E) : OpensMeasurableSpace ↥T

theorem LinearMap.exists_map_addHaar_eq_smul_addHaar' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [MeasurableSpace F] [BorelSpace F] [NormedSpace 𝕜 F] (L : E →ₗ[𝕜] F) (μ : MeasureTheory.Measure E) (ν : MeasureTheory.Measure F) [μ.IsAddHaarMeasure] [ν.IsAddHaarMeasure] [LocallyCompactSpace E] (h : Function.Surjective ⇑L) : ∃ (c : ENNReal), 0 < c ∧ c < ⊤ ∧ MeasureTheory.Measure.map (⇑L) μ = (c * MeasureTheory.Measure.addHaar Set.univ) • ν

The image of an additive Haar measure under a surjective linear map is proportional to a given additive Haar measure. The proportionality factor will be infinite if the linear map has a nontrivial kernel.

theorem LinearMap.exists_map_addHaar_eq_smul_addHaar {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [MeasurableSpace F] [BorelSpace F] [NormedSpace 𝕜 F] (L : E →ₗ[𝕜] F) (μ : MeasureTheory.Measure E) (ν : MeasureTheory.Measure F) [μ.IsAddHaarMeasure] [ν.IsAddHaarMeasure] [LocallyCompactSpace E] (h : Function.Surjective ⇑L) : ∃ (c : ENNReal), 0 < c ∧ MeasureTheory.Measure.map (⇑L) μ = c • ν

The image of an additive Haar measure under a surjective linear map is proportional to a given additive Haar measure, with a positive (but maybe infinite) factor.

theorem MeasureTheory.ae_comp_linearMap_mem_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [MeasurableSpace F] [BorelSpace F] [NormedSpace 𝕜 F] (L : E →ₗ[𝕜] F) (μ : MeasureTheory.Measure E) (ν : MeasureTheory.Measure F) [μ.IsAddHaarMeasure] [ν.IsAddHaarMeasure] [LocallyCompactSpace E] (h : Function.Surjective ⇑L) {s : Set F} (hs : MeasurableSet s) : (∀ᵐ (x : E) ∂μ, L x ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s

Given a surjective linear map L, it is equivalent to require a property almost everywhere in the source or the target spaces of L, with respect to additive Haar measures there.

theorem MeasureTheory.ae_ae_add_linearMap_mem_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [MeasurableSpace F] [BorelSpace F] [NormedSpace 𝕜 F] (L : E →ₗ[𝕜] F) (μ : MeasureTheory.Measure E) (ν : MeasureTheory.Measure F) [μ.IsAddHaarMeasure] [ν.IsAddHaarMeasure] [LocallyCompactSpace E] [LocallyCompactSpace F] {s : Set F} (hs : MeasurableSet s) : (∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, y + L x ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s

Given a linear map L : E → F, a property holds almost everywhere in F if and only if, almost everywhere in F, it holds almost everywhere along the subspace spanned by the image of L. This is an instance of a disintegration argument for additive Haar measures.

theorem MeasureTheory.ae_mem_of_ae_add_linearMap_mem {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [MeasurableSpace F] [BorelSpace F] [NormedSpace 𝕜 F] (L : E →ₗ[𝕜] F) (μ : MeasureTheory.Measure E) (ν : MeasureTheory.Measure F) [μ.IsAddHaarMeasure] [ν.IsAddHaarMeasure] [LocallyCompactSpace E] [LocallyCompactSpace F] {s : Set F} (hs : MeasurableSet s) (h : ∀ (y : F), ∀ᵐ (x : E) ∂μ, y + L x ∈ s) : ∀ᵐ (y : F) ∂ν, y ∈ s

To check that a property holds almost everywhere with respect to an additive Haar measure, it suffices to check it almost everywhere along all translates of a given vector subspace. This is an instance of a disintegration argument for additive Haar measures.