# Behavior of the Lebesgue integral under maps #

source
theorem MeasureTheory.lintegral_map {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {f : β → ENNReal} {g : α → β} (hf : Measurable f) (hg : Measurable g) :
∫⁻ (a : β), f a ∂Measure.map g μ = ∫⁻ (a : α), f (g a) ∂μ
source
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 μ) :
∫⁻ (a : β), f a ∂Measure.map g μ = ∫⁻ (a : α), f (g a) ∂μ
source
theorem MeasureTheory.lintegral_map_le {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} (f : β → ENNReal) (g : α → β) :
∫⁻ (a : β), f a ∂Measure.map g μ ≤ ∫⁻ (a : α), f (g a) ∂μ
source
theorem MeasureTheory.lintegral_comp {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {f : β → ENNReal} {g : α → β} (hf : Measurable f) (hg : Measurable g) :
lintegral μ (f ∘ g) = ∫⁻ (a : β), f a ∂Measure.map g μ
source
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) :
∫⁻ (y : β) in s, f y ∂Measure.map g μ = ∫⁻ (x : α) in g ⁻¹' s, f (g x) ∂μ
source
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) :
∫⁻ (a : α), s.indicator (fun (x : β) => c) (f a) ∂μ = c * μ (f ⁻¹' s)
source
theorem MeasurableEmbedding.lintegral_map {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {g : α → β} (hg : MeasurableEmbedding g) (f : β → ENNReal) :
∫⁻ (a : β), f a ∂MeasureTheory.Measure.map g μ = ∫⁻ (a : α), f (g a) ∂μ

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.

source
theorem MeasureTheory.lintegral_map_equiv {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} (f : β → ENNReal) (g : α ≃ᵐ β) :
∫⁻ (a : β), f a ∂Measure.map (⇑g) μ = ∫⁻ (a : α), f (g a) ∂μ

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.)

source
theorem MeasureTheory.lintegral_subtype_comap {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {s : Set α} (hs : MeasurableSet s) (f : α → ENNReal) :
∫⁻ (x : ↑s), f ↑x ∂Measure.comap Subtype.val μ = ∫⁻ (x : α) in s, f x ∂μ
source
theorem MeasureTheory.setLIntegral_subtype {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {s : Set α} (hs : MeasurableSet s) (t : Set ↑s) (f : α → ENNReal) :
∫⁻ (x : ↑s) in t, f ↑x ∂Measure.comap Subtype.val μ = ∫⁻ (x : α) in Subtype.val '' t, f x ∂μ
source
theorem MeasureTheory.MeasurePreserving.lintegral_map_equiv {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} (f : β → ENNReal) (g : α ≃ᵐ β) (hg : MeasurePreserving (⇑g) μ ν) :
∫⁻ (a : β), f a ∂ν = ∫⁻ (a : α), f (g a) ∂μ
source
theorem MeasureTheory.MeasurePreserving.lintegral_comp {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} {g : α → β} (hg : MeasurePreserving g μ ν) {f : β → ENNReal} (hf : Measurable f) :
∫⁻ (a : α), f (g a) ∂μ = ∫⁻ (b : β), f b ∂ν
source
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) :
∫⁻ (a : α), f (g a) ∂μ = ∫⁻ (b : β), f b ∂ν
source
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) :
∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂ν
source
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 β) :
∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂ν
source
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 α) :
∫⁻ (a : α) in s, f (g a) ∂μ = ∫⁻ (b : β) in g '' s, f b ∂ν