lintegral_lintegral_mul — Mathlib

English

For ENNReal r and Measurable f, ∫⁻ f a * r = (∫⁻ f a) * r.

Русский

Для ENNReal r и измеримой f: ∫⁻ f a · r = (∫⁻ f a) · r.

LaTeX

$$$\forall r : \mathbb{R}_{\ge 0}^{\infty},\; {f : α \to \mathbb{R}_{\ge 0}^{\infty}}\; (hf : AEMeasurable f μ) \Rightarrow ∫^- a, f a * r ∂μ = (∫^- a, f a ∂μ) * r$$$

Lean4

theorem lintegral_lintegral_mul {β} [MeasurableSpace β] {ν : Measure β} {f : α → ℝ≥0∞} {g : β → ℝ≥0∞}
    (hf : AEMeasurable f μ) (hg : AEMeasurable g ν) : ∫⁻ x, ∫⁻ y, f x * g y ∂ν ∂μ = (∫⁻ x, f x ∂μ) * ∫⁻ y, g y ∂ν := by
  simp [lintegral_const_mul'' _ hg, lintegral_mul_const'' _ hf]

Похожие утверждения