# Documentation

Mathlib.MeasureTheory.Measure.Haar.Disintegration

# 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)][fremlin_vol4]

theorem LinearMap.exists_map_addHaar_eq_smul_addHaar' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] [] [] (L : E →ₗ[𝕜] F) (μ : ) (ν : ) (h : ) :
∃ (c : ENNReal), 0 < c c < = (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} [] [] [] [] [] [] [] (L : E →ₗ[𝕜] F) (μ : ) (ν : ) (h : ) :
∃ (c : ENNReal), 0 < c = 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} [] [] [] [] [] [] [] (L : E →ₗ[𝕜] F) (μ : ) (ν : ) (h : ) {s : Set F} (hs : ) :
(∀ᵐ (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} [] [] [] [] [] [] [] (L : E →ₗ[𝕜] F) (μ : ) (ν : ) {s : Set F} (hs : ) :
(∀ᵐ (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} [] [] [] [] [] [] [] (L : E →ₗ[𝕜] F) (μ : ) (ν : ) {s : Set F} (hs : ) (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.