theorem MeasurableEmbedding.map_restrict {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} (hf : MeasurableEmbedding f) (μ : MeasureTheory.Measure α) (s : Set α) : MeasureTheory.Measure.map f (μ.restrict s) = (MeasureTheory.Measure.map f μ).restrict (f '' s)

theorem MeasurableEmbedding.setLIntegral_map {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : β → ENNReal} {g : α → β} {s : Set β} (hg : MeasurableEmbedding g) : ∫⁻ (y : β) in s, f y ∂MeasureTheory.Measure.map g μ = ∫⁻ (x : α) in g ⁻¹' s, f (g x) ∂μ

@[simp]

theorem lintegral_comp_neg_Iic (c : ℝ) (f : ℝ → ENNReal) : ∫⁻ (x : ℝ) in Set.Iic c, f (-x) = ∫⁻ (x : ℝ) in Set.Ioi (-c), f x

@[simp]

theorem lintegral_comp_neg_Ioi (c : ℝ) (f : ℝ → ENNReal) : ∫⁻ (x : ℝ) in Set.Ioi c, f (-x) = ∫⁻ (x : ℝ) in Set.Iic (-c), f x

theorem lintegral_comp_abs {f : ℝ → ENNReal} : ∫⁻ (x : ℝ), f |x| = 2 * ∫⁻ (x : ℝ) in Set.Ioi 0, f x