integral_eq_iff_of_ae_le — Mathlib

English

If f ≤ g a.e. with integrable f and g, then ∫ f = ∫ g iff f = g a.e.

Русский

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

LaTeX

$$$\\\\int a \\, f(a) \\, d\\\\mu = \\\\int a \\, g(a) \\, d\\\\mu \\\\iff f = a.e. \\\\ g$$$

Lean4

theorem integral_eq_iff_of_ae_le {f g : α → ℝ} (hf : Integrable f μ) (hg : Integrable g μ) (hfg : f ≤ᵐ[μ] g) :
    ∫ a, f a ∂μ = ∫ a, g a ∂μ ↔ f =ᵐ[μ] g :=
  by
  refine ⟨fun h_le ↦ EventuallyEq.symm ?_, fun h ↦ integral_congr_ae h⟩
  rw [← sub_ae_eq_zero, ← integral_eq_zero_iff_of_nonneg_ae ((sub_nonneg_ae _ _).mpr hfg) (hg.sub hf)]
  simpa [Pi.sub_apply, integral_sub hg hf, sub_eq_zero, eq_comm]

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