lintegral_strict_mono — Mathlib

English

If f ≤ᵐ g, ∫ f ≠ ∞, and f < g almost everywhere, then ∫ f < ∫ g.

Русский

Если f ≤ᵐ g, интеграл f конечен, и f < g почти всюду, тогда ∫ f < ∫ g.

LaTeX

$$$(f \\leq_{a.e.}^{μ} g) \\wedge (∫ f dμ \\neq ∞) \\wedge (∀ᵐ x, f(x) < g(x)) \\Rightarrow ∫ f dμ < ∫ g dμ$$$

Lean4

theorem lintegral_strict_mono {f g : α → ℝ≥0∞} (hμ : μ ≠ 0) (hg : AEMeasurable g μ) (hfi : ∫⁻ x, f x ∂μ ≠ ∞)
    (h : ∀ᵐ x ∂μ, f x < g x) : ∫⁻ x, f x ∂μ < ∫⁻ x, g x ∂μ :=
  by
  rw [Ne, ← Measure.measure_univ_eq_zero] at hμ
  refine lintegral_strict_mono_of_ae_le_of_ae_lt_on hg hfi (ae_le_of_ae_lt h) hμ ?_
  simpa using h

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