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)

instance instBorelSpaceSubtypeMemSubmodule {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [NormedSpace ๐•œ E] (T : Submodule ๐•œ E) :
BorelSpace โ†ฅT
Equations
  • โ‹ฏ = โ‹ฏ
instance instOpensMeasurableSpaceSubtypeMemSubmodule {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [NormedSpace ๐•œ E] (T : Submodule ๐•œ E) :
Equations
  • โ‹ฏ = โ‹ฏ
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.