Behavior of the Lebesgue integral under maps #
theorem
MeasureTheory.lintegral_map
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : Measure α}
{f : β → ENNReal}
{g : α → β}
(hf : Measurable f)
(hg : Measurable g)
:
theorem
MeasureTheory.lintegral_map'
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : Measure α}
{f : β → ENNReal}
{g : α → β}
(hf : AEMeasurable f (Measure.map g μ))
(hg : AEMeasurable g μ)
:
theorem
MeasureTheory.lintegral_map_le
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : Measure α}
(f : β → ENNReal)
(g : α → β)
:
theorem
MeasureTheory.lintegral_comp
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : Measure α}
{f : β → ENNReal}
{g : α → β}
(hf : Measurable f)
(hg : Measurable g)
:
theorem
MeasureTheory.setLIntegral_map
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : Measure α}
{f : β → ENNReal}
{g : α → β}
{s : Set β}
(hs : MeasurableSet s)
(hf : Measurable f)
(hg : Measurable g)
:
theorem
MeasureTheory.lintegral_indicator_const_comp
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : Measure α}
{f : α → β}
{s : Set β}
(hf : Measurable f)
(hs : MeasurableSet s)
(c : ENNReal)
:
theorem
MeasurableEmbedding.lintegral_map
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{g : α → β}
(hg : MeasurableEmbedding g)
(f : β → ENNReal)
:
If g : α → β is a measurable embedding and f : β → ℝ≥0∞ is any function (not necessarily
measurable), then ∫⁻ a, f a ∂(map g μ) = ∫⁻ a, f (g a) ∂μ. Compare with lintegral_map which
applies to any measurable g : α → β but requires that f is measurable as well.
theorem
MeasureTheory.lintegral_map_equiv
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : Measure α}
(f : β → ENNReal)
(g : α ≃ᵐ β)
:
The lintegral transforms appropriately under a measurable equivalence g : α ≃ᵐ β.
(Compare lintegral_map, which applies to a wider class of functions g : α → β, but requires
measurability of the function being integrated.)
theorem
MeasureTheory.lintegral_subtype_comap
{α : Type u_1}
[MeasurableSpace α]
{μ : Measure α}
{s : Set α}
(hs : MeasurableSet s)
(f : α → ENNReal)
:
theorem
MeasureTheory.setLIntegral_subtype
{α : Type u_1}
[MeasurableSpace α]
{μ : Measure α}
{s : Set α}
(hs : MeasurableSet s)
(t : Set ↑s)
(f : α → ENNReal)
:
theorem
MeasureTheory.MeasurePreserving.lintegral_map_equiv
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : Measure α}
{ν : Measure β}
(f : β → ENNReal)
(g : α ≃ᵐ β)
(hg : MeasurePreserving (⇑g) μ ν)
:
theorem
MeasureTheory.MeasurePreserving.lintegral_comp
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : Measure α}
{ν : Measure β}
{g : α → β}
(hg : MeasurePreserving g μ ν)
{f : β → ENNReal}
(hf : Measurable f)
:
theorem
MeasureTheory.MeasurePreserving.lintegral_comp_emb
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : Measure α}
{ν : Measure β}
{g : α → β}
(hg : MeasurePreserving g μ ν)
(hge : MeasurableEmbedding g)
(f : β → ENNReal)
:
theorem
MeasureTheory.MeasurePreserving.setLIntegral_comp_preimage
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : Measure α}
{ν : Measure β}
{g : α → β}
(hg : MeasurePreserving g μ ν)
{s : Set β}
(hs : MeasurableSet s)
{f : β → ENNReal}
(hf : Measurable f)
:
theorem
MeasureTheory.MeasurePreserving.setLIntegral_comp_preimage_emb
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : Measure α}
{ν : Measure β}
{g : α → β}
(hg : MeasurePreserving g μ ν)
(hge : MeasurableEmbedding g)
(f : β → ENNReal)
(s : Set β)
:
theorem
MeasureTheory.MeasurePreserving.setLIntegral_comp_emb
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : Measure α}
{ν : Measure β}
{g : α → β}
(hg : MeasurePreserving g μ ν)
(hge : MeasurableEmbedding g)
(f : β → ENNReal)
(s : Set α)
: