lintegral_const_mul_le — Mathlib

English

For r ∈ ℝ≥0∞ and f : α → ℝ≥0∞, (∫ f) · r ≤ ∫ (f · r).

Русский

Для r ∈ ℝ≥0∞ и f: ∫ f · r ≤ ∫ (f · r).

LaTeX

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

Lean4

theorem lintegral_const_mul_le (r : ℝ≥0∞) (f : α → ℝ≥0∞) : r * ∫⁻ a, f a ∂μ ≤ ∫⁻ a, r * f a ∂μ :=
  by
  rw [lintegral, ENNReal.mul_iSup]
  refine iSup_le fun s => ?_
  rw [ENNReal.mul_iSup, iSup_le_iff]
  intro hs
  rw [← SimpleFunc.const_mul_lintegral, lintegral]
  refine le_iSup_of_le (const α r * s) (le_iSup_of_le (fun x => ?_) le_rfl)
  exact mul_le_mul_left' (hs x) _

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