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) : ∫⁻ (a : β), f a ∂Measure.map g μ = ∫⁻ (a : α), f (g a) ∂μ

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) ∂μ

theorem MeasureTheory.lintegral_map_le {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} (f : β → ENNReal) {g : α → β} (hg : AEMeasurable g μ) : ∫⁻ (a : β), f a ∂Measure.map g μ ≤ ∫⁻ (a : α), f (g a) ∂μ

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 μ

theorem MeasureTheory.lintegral_comp' {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {f : β → ENNReal} {g : α → β} (hf : AEMeasurable f (Measure.map g μ)) (hg : AEMeasurable g μ) : lintegral μ (f ∘ g) = ∫⁻ (a : β), f a ∂Measure.map g μ

Generalization of lintegral_comp to ae-measurable functions.

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) ∂μ

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)

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.

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

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 ∂μ

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 ∂μ

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) ∂μ

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 ∂ν

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 ∂ν

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 ∂ν

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 ∂ν

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 ∂ν