Pushforward of a measure #
In this file we define the pushforward MeasureTheory.Measure.map f μ
of a measure μ along an almost everywhere measurable map f.
If f is not a.e. measurable, then we define map f μ to be zero.
Main definitions #
MeasureTheory.Measure.map f μ: map of the measureμalong the mapf.
Main statements #
noncomputable def
MeasureTheory.Measure.liftLinear
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
[MeasurableSpace β]
(f : OuterMeasure α →ₗ[ENNReal] OuterMeasure β)
(hf : ∀ (μ : Measure α), inst✝ ≤ (f μ.toOuterMeasure).caratheodory)
:
Lift a linear map between OuterMeasure spaces such that for each measure μ every measurable
set is caratheodory-measurable w.r.t. f μ to a linear map between Measure spaces.
Equations
- MeasureTheory.Measure.liftLinear f hf = { toFun := fun (μ : MeasureTheory.Measure α) => (f μ.toOuterMeasure).toMeasure ⋯, map_add' := ⋯, map_smul' := ⋯ }
Instances For
theorem
MeasureTheory.Measure.liftLinear_apply₀
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{f : OuterMeasure α →ₗ[ENNReal] OuterMeasure β}
(hf : ∀ (μ : Measure α), mβ ≤ (f μ.toOuterMeasure).caratheodory)
{s : Set β}
(hs : NullMeasurableSet s ((liftLinear f hf) μ))
:
@[simp]
theorem
MeasureTheory.Measure.liftLinear_apply
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{f : OuterMeasure α →ₗ[ENNReal] OuterMeasure β}
(hf : ∀ (μ : Measure α), mβ ≤ (f μ.toOuterMeasure).caratheodory)
{s : Set β}
(hs : MeasurableSet s)
:
theorem
MeasureTheory.Measure.le_liftLinear_apply
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{f : OuterMeasure α →ₗ[ENNReal] OuterMeasure β}
(hf : ∀ (μ : Measure α), mβ ≤ (f μ.toOuterMeasure).caratheodory)
(s : Set β)
:
noncomputable def
MeasureTheory.Measure.mapₗ
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(f : α → β)
:
The pushforward of a measure as a linear map. It is defined to be 0 if f is not
a measurable function.
Equations
- MeasureTheory.Measure.mapₗ f = if hf : Measurable f then MeasureTheory.Measure.liftLinear (MeasureTheory.OuterMeasure.map f) ⋯ else 0
Instances For
theorem
MeasureTheory.Measure.mapₗ_congr
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{f g : α → β}
(hf : Measurable f)
(hg : Measurable g)
(h : f =ᶠ[ae μ] g)
:
theorem
MeasureTheory.Measure.map_def
{α : Type u_4}
{β : Type u_5}
[MeasurableSpace α]
[MeasurableSpace β]
(f : α → β)
(μ : Measure α)
:
@[irreducible]
noncomputable def
MeasureTheory.Measure.map
{α : Type u_4}
{β : Type u_5}
[MeasurableSpace α]
[MeasurableSpace β]
(f : α → β)
(μ : Measure α)
:
Measure β
The pushforward of a measure. It is defined to be 0 if f is not an almost everywhere
measurable function.
Equations
- MeasureTheory.Measure.map f μ = if hf : AEMeasurable f μ then (MeasureTheory.Measure.mapₗ (AEMeasurable.mk f hf)) μ else 0
Instances For
theorem
MeasureTheory.Measure.mapₗ_mk_apply_of_aemeasurable
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
:
theorem
MeasureTheory.Measure.mapₗ_apply_of_measurable
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : α → β}
(hf : Measurable f)
(μ : Measure α)
:
@[simp]
theorem
MeasureTheory.Measure.map_add
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ ν : Measure α)
{f : α → β}
(hf : Measurable f)
:
@[simp]
theorem
MeasureTheory.Measure.map_zero
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(f : α → β)
:
@[simp]
theorem
MeasureTheory.Measure.map_of_not_aemeasurable
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : α → β}
{μ : Measure α}
(hf : ¬AEMeasurable f μ)
:
theorem
AEMeasurable.of_map_ne_zero
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : α → β}
{μ : MeasureTheory.Measure α}
(hf : MeasureTheory.Measure.map f μ ≠ 0)
:
AEMeasurable f μ
theorem
MeasureTheory.Measure.map_congr
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{f g : α → β}
(h : f =ᶠ[ae μ] g)
:
@[simp]
theorem
MeasureTheory.Measure.map_smul
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{R : Type u_4}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
(c : R)
(μ : Measure α)
(f : α → β)
:
theorem
MeasureTheory.Measure.map_apply₀
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
{s : Set β}
(hs : NullMeasurableSet s (map f μ))
:
@[simp]
theorem
MeasureTheory.Measure.map_apply_of_aemeasurable
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
{s : Set β}
(hs : MeasurableSet s)
:
We can evaluate the pushforward on measurable sets. For non-measurable sets, see
MeasureTheory.Measure.le_map_apply and MeasurableEquiv.map_apply.
@[simp]
theorem
MeasureTheory.Measure.map_apply
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{f : α → β}
(hf : Measurable f)
{s : Set β}
(hs : MeasurableSet s)
:
theorem
MeasureTheory.Measure.map_toOuterMeasure
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
:
@[simp]
theorem
MeasureTheory.Measure.map_eq_zero_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
:
@[simp]
theorem
MeasureTheory.Measure.mapₗ_eq_zero_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{f : α → β}
(hf : Measurable f)
:
theorem
MeasureTheory.Measure.measure_preimage_of_map_eq_self
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f : α → α}
(hf : map f μ = μ)
{s : Set α}
(hs : NullMeasurableSet s μ)
:
If map f μ = μ, then the measure of the preimage of any null measurable set s
is equal to the measure of s.
Note that this lemma does not assume (a.e.) measurability of f.
theorem
MeasureTheory.Measure.map_ne_zero_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
:
theorem
MeasureTheory.Measure.mapₗ_ne_zero_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{f : α → β}
(hf : Measurable f)
:
@[simp]
@[simp]
theorem
MeasureTheory.Measure.map_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{μ : Measure α}
{g : β → γ}
{f : α → β}
(hg : Measurable g)
(hf : Measurable f)
:
Mapping a measure twice is the same as mapping the measure with the composition. This version is
for measurable functions. See map_map_of_aemeasurable when they are just ae measurable.
theorem
MeasureTheory.Measure.map_mono
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ ν : Measure α}
{f : α → β}
(h : μ ≤ ν)
(hf : Measurable f)
:
theorem
MeasureTheory.Measure.le_map_apply
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
(s : Set β)
:
Even if s is not measurable, we can bound map f μ s from below.
See also MeasurableEquiv.map_apply.
theorem
MeasureTheory.Measure.le_map_apply_image
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
(s : Set α)
:
theorem
MeasureTheory.Measure.preimage_null_of_map_null
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
{s : Set β}
(hs : (map f μ) s = 0)
:
Even if s is not measurable, map f μ s = 0 implies that μ (f ⁻¹' s) = 0.
theorem
MeasureTheory.Measure.tendsto_ae_map
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
:
Filter.Tendsto f (ae μ) (ae (map f μ))
theorem
MeasureTheory.mem_ae_map_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
{s : Set β}
(hs : MeasurableSet s)
:
theorem
MeasureTheory.mem_ae_of_mem_ae_map
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
{s : Set β}
(hs : s ∈ ae (Measure.map f μ))
:
theorem
MeasureTheory.ae_map_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
{p : β → Prop}
(hp : MeasurableSet {x : β | p x})
:
theorem
MeasureTheory.ae_of_ae_map
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
{p : β → Prop}
(h : ∀ᵐ (y : β) ∂Measure.map f μ, p y)
:
theorem
MeasureTheory.ae_map_mem_range
{α : Type u_1}
{β : Type u_2}
{mβ : MeasurableSpace β}
{m0 : MeasurableSpace α}
(f : α → β)
(hf : MeasurableSet (Set.range f))
(μ : Measure α)
:
theorem
MeasurableEmbedding.map_apply
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{m1 : MeasurableSpace β}
{f : α → β}
(hf : MeasurableEmbedding f)
(μ : MeasureTheory.Measure α)
(s : Set β)
:
Interactions of measurable equivalences and measures
theorem
MeasurableEquiv.map_apply
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
(f : α ≃ᵐ β)
(s : Set β)
:
If we map a measure along a measurable equivalence, we can compute the measure on all sets (not just the measurable ones).
@[simp]
theorem
MeasurableEquiv.map_symm_map
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
(e : α ≃ᵐ β)
:
@[simp]
theorem
MeasurableEquiv.map_map_symm
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[MeasurableSpace β]
{ν : MeasureTheory.Measure β}
(e : α ≃ᵐ β)
:
theorem
MeasurableEquiv.map_measurableEquiv_injective
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[MeasurableSpace β]
(e : α ≃ᵐ β)
:
theorem
MeasurableEquiv.map_apply_eq_iff_map_symm_apply_eq
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
(e : α ≃ᵐ β)
:
theorem
MeasurableEquiv.map_ae
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[MeasurableSpace β]
(f : α ≃ᵐ β)
(μ : MeasureTheory.Measure α)
: