English
For a real-valued function f, under appropriate integrability conditions, the integral of |f| over R equals twice the integral of f over the positive half-line, i.e., ∫R |f| = 2 ∫0^∞ f.
Русский
Для вещественной функции f при подходящей интегрируемости имеет место ∫R |f| = 2 ∫0^∞ f.
LaTeX
$$$\int_{-\infty}^{\infty} f(|x|) \, dx = 2 \int_{0}^{\infty} f(x) \, dx$$$
Lean4
theorem integral_comp_abs {f : ℝ → ℝ} : ∫ x, f |x| = 2 * ∫ x in Ioi (0 : ℝ), f x :=
by
have eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x :=
by
refine setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)
rw [abs_eq_self.mpr (le_of_lt (by exact hx))]
by_cases hf : IntegrableOn (fun x => f |x|) (Ioi 0)
· have int_Iic : IntegrableOn (fun x ↦ f |x|) (Iic 0) :=
by
rw [← Measure.map_neg_eq_self (volume : Measure ℝ)]
let m : MeasurableEmbedding fun x : ℝ => -x := (Homeomorph.neg ℝ).measurableEmbedding
rw [m.integrableOn_map_iff]
simp_rw [Function.comp_def, abs_neg, neg_preimage, neg_Iic, neg_zero]
exact Iff.mpr integrableOn_Ici_iff_integrableOn_Ioi hf
calc
_ = (∫ x in Iic 0, f |x|) + ∫ x in Ioi 0, f |x| := by
rw [← setIntegral_union (Iic_disjoint_Ioi le_rfl) measurableSet_Ioi int_Iic hf, Iic_union_Ioi, restrict_univ]
_ = 2 * ∫ x in Ioi 0, f x := by
rw [two_mul, eq]
congr! 1
rw [← neg_zero, ← integral_comp_neg_Iic, neg_zero]
refine setIntegral_congr_fun measurableSet_Iic (fun _ hx => ?_)
rw [abs_eq_neg_self.mpr (by exact hx)]
· have : ¬Integrable (fun x => f |x|) := by
contrapose! hf
exact hf.integrableOn
rw [← eq, integral_undef hf, integral_undef this, mul_zero]
