MeasureTheory.ae_mem_of_ae_add_linearMap_mem
theorem MeasureTheory.ae_mem_of_ae_add_linearMap_mem :
โ {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField ๐] [inst_1 : CompleteSpace ๐]
[inst_2 : NormedAddCommGroup E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [inst_5 : NormedSpace ๐ E]
[inst_6 : NormedAddCommGroup F] [inst_7 : MeasurableSpace F] [inst_8 : BorelSpace F] [inst_9 : NormedSpace ๐ F]
(L : E โโ[๐] F) (ฮผ : MeasureTheory.Measure E) (ฮฝ : MeasureTheory.Measure F) [inst_10 : ฮผ.IsAddHaarMeasure]
[inst_11 : ฮฝ.IsAddHaarMeasure] [inst_12 : LocallyCompactSpace E] [inst_13 : LocallyCompactSpace F] {s : Set F},
MeasurableSet s โ (โ (y : F), โแต (x : E) โฮผ, y + L x โ s) โ โแต (y : F) โฮฝ, y โ s
This theorem, "MeasureTheory.ae_mem_of_ae_add_linearMap_mem", states that to verify a property holds almost everywhere (almost all places) with respect to an additive Haar measure, it is sufficient to check the property almost everywhere along all translates of a specific vector subspace. In more detail, given a linear map `L` from a normed additive commutative group `E` to another such group `F`, and measures `ฮผ` and `ฮฝ` over these spaces, all under the additional conditions that `ฮผ` and `ฮฝ` are additive Haar measures and `E` and `F` are locally compact spaces, if a set `s` in `F` is measurable, and for every element `y` in `F`, almost every `x` in `E` satisfies that `y + Lx` is in `s` with respect to measure `ฮผ`, then almost every `y` in `F` is in `s` with respect to measure `ฮฝ`. This theorem is an instance of a disintegration argument for additive Haar measures.
More concisely: If a property holds almost everywhere with respect to an additive Haar measure for translates of a linear map's images in one locally compact space, then it also holds almost everywhere in the target space with respect to the additive Haar measure.
|
MeasureTheory.ae_ae_add_linearMap_mem_iff
theorem MeasureTheory.ae_ae_add_linearMap_mem_iff :
โ {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField ๐] [inst_1 : CompleteSpace ๐]
[inst_2 : NormedAddCommGroup E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [inst_5 : NormedSpace ๐ E]
[inst_6 : NormedAddCommGroup F] [inst_7 : MeasurableSpace F] [inst_8 : BorelSpace F] [inst_9 : NormedSpace ๐ F]
(L : E โโ[๐] F) (ฮผ : MeasureTheory.Measure E) (ฮฝ : MeasureTheory.Measure F) [inst_10 : ฮผ.IsAddHaarMeasure]
[inst_11 : ฮฝ.IsAddHaarMeasure] [inst_12 : LocallyCompactSpace E] [inst_13 : LocallyCompactSpace F] {s : Set F},
MeasurableSet s โ ((โแต (y : F) โฮฝ, โแต (x : E) โฮผ, y + L x โ s) โ โแต (y : F) โฮฝ, y โ s)
The theorem `MeasureTheory.ae_ae_add_linearMap_mem_iff` states that for any given linear map `L` from a normed additively commutative group `E` to another such group `F`, with both `E` and `F` being locally compact spaces, and given any measurable set `s` in `F`, a property holds almost everywhere in `F` if and only if, almost everywhere in `F`, the property holds almost everywhere along the subspace spanned by the image of `L`. This theorem is applied for additive Haar measures `ฮผ` on `E` and `ฮฝ` on `F`. The term 'almost everywhere' (notated as 'โแต') refers to the property being true except on a set of measure zero.
More concisely: For any locally compact, normed additively commutative groups E and F, measurable set s in F, and linear map L from E to F with respect to additive Haar measures ฮผ on E and ฮฝ on F, the property ฯ holds almost everywhere in F if and only if almost everywhere in F, the property ฯ holds almost everywhere along the subspace spanned by the image of L.
|
MeasureTheory.ae_comp_linearMap_mem_iff
theorem MeasureTheory.ae_comp_linearMap_mem_iff :
โ {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField ๐] [inst_1 : CompleteSpace ๐]
[inst_2 : NormedAddCommGroup E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [inst_5 : NormedSpace ๐ E]
[inst_6 : NormedAddCommGroup F] [inst_7 : MeasurableSpace F] [inst_8 : BorelSpace F] [inst_9 : NormedSpace ๐ F]
(L : E โโ[๐] F) (ฮผ : MeasureTheory.Measure E) (ฮฝ : MeasureTheory.Measure F) [inst_10 : ฮผ.IsAddHaarMeasure]
[inst_11 : ฮฝ.IsAddHaarMeasure] [inst_12 : LocallyCompactSpace E],
Function.Surjective โL โ โ {s : Set F}, MeasurableSet s โ ((โแต (x : E) โฮผ, L x โ s) โ โแต (y : F) โฮฝ, y โ s)
This theorem states that for a given surjective linear map `L` from a space `E` to another space `F` (both being normed additive commutative groups and with certain topological and measure-theoretic properties), then a statement holds almost everywhere in `E` with respect to a measure `ฮผ` (being an additive Haar measure) if and only if the same statement holds almost everywhere in `F` with respect to a measure `ฮฝ` (also being an additive Haar measure). Here, the statement being considered is the property of a point being in a measurable subset `s` of `F`. "Almost everywhere" means that the set of points where the statement doesn't hold has measure zero.
More concisely: For a surjective linear map between two normed additive commutative groups with compatible Haar measures, a point is in a measurable subset almost everywhere in the domain if and only if its image is in the subset almost everywhere in the codomain.
|
LinearMap.exists_map_addHaar_eq_smul_addHaar
theorem LinearMap.exists_map_addHaar_eq_smul_addHaar :
โ {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField ๐] [inst_1 : CompleteSpace ๐]
[inst_2 : NormedAddCommGroup E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [inst_5 : NormedSpace ๐ E]
[inst_6 : NormedAddCommGroup F] [inst_7 : MeasurableSpace F] [inst_8 : BorelSpace F] [inst_9 : NormedSpace ๐ F]
(L : E โโ[๐] F) (ฮผ : MeasureTheory.Measure E) (ฮฝ : MeasureTheory.Measure F) [inst_10 : ฮผ.IsAddHaarMeasure]
[inst_11 : ฮฝ.IsAddHaarMeasure] [inst_12 : LocallyCompactSpace E],
Function.Surjective โL โ โ c, 0 < c โง MeasureTheory.Measure.map (โL) ฮผ = c โข ฮฝ
The theorem `LinearMap.exists_map_addHaar_eq_smul_addHaar` states that for any surjective linear map `L` from a normed add commutative group `E` to another normed add commutative group `F` over a non-trivially normed field `๐`, if `E` is a locally compact space and both `E` and `F` are equipped with additive Haar measures `ฮผ` and `ฮฝ` respectively, then the image of the measure `ฮผ` under the map `L` is proportional to the measure `ฮฝ`. The proportionality factor is a positive scalar `c`, which might be infinite.
More concisely: For any surjective linear map between locally compact normed add commutative groups over a non-trivially normed field, if the domains are equipped with additive Haar measures, then the image measure is proportional to the target measure, up to a positive scalar (which may be infinite).
|