setLIntegral_strict_mono — Mathlib

English

If f ≤ᵐ g and μ s ≠ 0, with g measurable and f < g almost everywhere on s, then ∫_s f < ∫_s g.

Русский

Если f ≤ᵐ g, μ s ≠ 0 и g измерим, а на s почти везде f < g, то ∫_s f < ∫_s g.

LaTeX

$$$(f \\leq_{a.e.}^{μ} g) \\wedge (μ s \\neq 0) \\wedge (Measurable g) \\wedge (∀ᵐ x ∂μ, x ∈ s → f(x) < g(x)) \\Rightarrow ∫⁻ x, f(x) ∂μ < ∫⁻ x, g(x) ∂μ$$$

Lean4

theorem setLIntegral_strict_mono {f g : α → ℝ≥0∞} {s : Set α} (hsm : MeasurableSet s) (hs : μ s ≠ 0) (hg : Measurable g)
    (hfi : ∫⁻ x in s, f x ∂μ ≠ ∞) (h : ∀ᵐ x ∂μ, x ∈ s → f x < g x) : ∫⁻ x in s, f x ∂μ < ∫⁻ x in s, g x ∂μ :=
  lintegral_strict_mono (by simp [hs]) hg.aemeasurable hfi ((ae_restrict_iff' hsm).mpr h)

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