lintegral_const_mul'' — Mathlib

English

For r ∈ ℝ≥0∞ and AEMeasurable f, one has ∫⁻ r * f = r * ∫⁻ f.

Русский

Для r ∈ ℝ≥0∞ и AEMеасываемой f: ∫⁻ r f = r ∫⁻ f.

LaTeX

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

Lean4

theorem lintegral_const_mul'' (r : ℝ≥0∞) {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) : ∫⁻ a, r * f a ∂μ = r * ∫⁻ a, f a ∂μ :=
  by
  have A : ∫⁻ a, f a ∂μ = ∫⁻ a, hf.mk f a ∂μ := lintegral_congr_ae hf.ae_eq_mk
  have B : ∫⁻ a, r * f a ∂μ = ∫⁻ a, r * hf.mk f a ∂μ := lintegral_congr_ae (EventuallyEq.fun_comp hf.ae_eq_mk _)
  rw [A, B, lintegral_const_mul _ hf.measurable_mk]

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