# 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} [] [CompleteSpace ๐] [] [] [NormedSpace ๐ E] [] [] [NormedSpace ๐ F] (L : E โโ[๐] F) (ฮผ : ) (ฮฝ : ) [ฮผ.IsAddHaarMeasure] [ฮฝ.IsAddHaarMeasure] (h : ) :
โ (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} [] [CompleteSpace ๐] [] [] [NormedSpace ๐ E] [] [] [NormedSpace ๐ F] (L : E โโ[๐] F) (ฮผ : ) (ฮฝ : ) [ฮผ.IsAddHaarMeasure] [ฮฝ.IsAddHaarMeasure] (h : ) :
โ (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} [] [CompleteSpace ๐] [] [] [NormedSpace ๐ E] [] [] [NormedSpace ๐ F] (L : E โโ[๐] F) (ฮผ : ) (ฮฝ : ) [ฮผ.IsAddHaarMeasure] [ฮฝ.IsAddHaarMeasure] (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} [] [CompleteSpace ๐] [] [] [NormedSpace ๐ E] [] [] [NormedSpace ๐ F] (L : E โโ[๐] F) (ฮผ : ) (ฮฝ : ) [ฮผ.IsAddHaarMeasure] [ฮฝ.IsAddHaarMeasure] {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} [] [CompleteSpace ๐] [] [] [NormedSpace ๐ E] [] [] [NormedSpace ๐ F] (L : E โโ[๐] F) (ฮผ : ) (ฮฝ : ) [ฮผ.IsAddHaarMeasure] [ฮฝ.IsAddHaarMeasure] {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.