hasSum_intervalIntegral — Mathlib

English

If f and g are interval-integrable and f ≤ g a.e., then ∫ f ≤ ∫ g.

Русский

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

LaTeX

$$$f ≤^a_\\mu g \\Rightarrow ∫ f ≤ ∫ g$.$$

Lean4

theorem _root_.MeasureTheory.Integrable.hasSum_intervalIntegral (hfi : Integrable f μ) (y : ℝ) :
    HasSum (fun n : ℤ => ∫ x in y + n..y + n + 1, f x ∂μ) (∫ x, f x ∂μ) :=
  by
  simp_rw [integral_of_le (le_add_of_nonneg_right zero_le_one)]
  rw [← setIntegral_univ, ← iUnion_Ioc_add_intCast y]
  exact hasSum_integral_iUnion (fun i => measurableSet_Ioc) (pairwise_disjoint_Ioc_add_intCast y) hfi.integrableOn

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