Some tools for measure theory computations

A collection of small lemmas to help with integral manipulations.

theorem MeasureTheory.measure_preserving_shift {a : ℝ} : MeasurePreserving (fun (x : ℝ) => a + x) volume volume

theorem MeasureTheory.measureable_embedding_shift {a : ℝ} : MeasurableEmbedding fun (x : ℝ) => a + x

theorem MeasureTheory.measure_preserving_scaling {a : ℝ} (ha : a ≠ 0) : MeasurePreserving (fun (x : ℝ) => a * x) volume (ENNReal.ofReal |a⁻¹| • volume)

theorem MeasureTheory.lintegral_shift (f : ℝ → ENNReal) {a : ℝ} : ∫⁻ (x : ℝ), f (x + a) = ∫⁻ (x : ℝ), f x

theorem MeasureTheory.lintegral_shift' (f : ℝ → ENNReal) {a : ℝ} {s : Set ℝ} : ∫⁻ (x : ℝ) in (fun (z : ℝ) => z + a) ⁻¹' s, f (x + a) = ∫⁻ (x : ℝ) in s, f x

theorem MeasureTheory.lintegral_add_right_Ioi (f : ℝ → ENNReal) {a b : ℝ} : ∫⁻ (x : ℝ) in Set.Ioi (b - a), f (x + a) = ∫⁻ (x : ℝ) in Set.Ioi b, f x

theorem MeasureTheory.lintegral_scale_constant (f : ℝ → ENNReal) {a : ℝ} (h : a ≠ 0) : ∫⁻ (x : ℝ), f (a * x) = ENNReal.ofReal |a⁻¹| * ∫⁻ (x : ℝ), f x

theorem MeasureTheory.lintegral_scale_constant_preimage (f : ℝ → ENNReal) {a : ℝ} (h : a ≠ 0) {s : Set ℝ} : ∫⁻ (x : ℝ) in (fun (z : ℝ) => a * z) ⁻¹' s, f (a * x) = ENNReal.ofReal |a⁻¹| * ∫⁻ (x : ℝ) in s, f x

theorem MeasureTheory.lintegral_scale_constant_halfspace (f : ℝ → ENNReal) {a : ℝ} (h : 0 < a) : ∫⁻ (x : ℝ) in Set.Ioi 0, f (a * x) = ENNReal.ofReal |a⁻¹| * ∫⁻ (x : ℝ) in Set.Ioi 0, f x

theorem MeasureTheory.lintegral_scale_constant_halfspace' {f : ℝ → ENNReal} {a : ℝ} (h : 0 < a) : ENNReal.ofReal |a| * ∫⁻ (x : ℝ) in Set.Ioi 0, f (a * x) = ∫⁻ (x : ℝ) in Set.Ioi 0, f x

theorem MeasureTheory.lintegral_scale_constant' {f : ℝ → ENNReal} {a : ℝ} (h : a ≠ 0) : ENNReal.ofReal |a| * ∫⁻ (x : ℝ), f (a * x) = ∫⁻ (x : ℝ), f x

theorem MeasureTheory.lintegral_eq_iSup_eapprox_lintegral' {α : Type u_3} {m : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) : ∫⁻ (a : α), f a ∂μ = ⨆ (n : ℕ), (SimpleFunc.eapprox (AEMeasurable.mk f hf) n).lintegral μ

Generalization of MeasureTheory.lintegral_eq_iSup_eapprox_lintegral assuming a.e. measurability of f

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

Generalization of MeasureTheory.lintegral_comp assuming a.e. measurability of f and g

theorem MeasureTheory.lintegral_set_mono_fn {α : Type u_3} {m : MeasurableSpace α} {μ : Measure α} {s : Set α} (hs : MeasurableSet s) ⦃f g : α → ENNReal⦄ (hfg : ∀ x ∈ s, f x ≤ g x) : ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ