lintegral_le_of_forall_fin_meas_trim_le

English

Same as above expressed in ENNReal setting with ENNReal bounds.

Русский

То же самое в рамках ENNReal-обоснования.

LaTeX

$$f(\mathrm{univ}) ≤ C$$

Lean4

/-- If the Lebesgue integral of a function is bounded by some constant on all sets with finite
measure in a sub-σ-algebra and the measure is σ-finite on that sub-σ-algebra, then the integral
over the whole space is bounded by that same constant. -/
theorem lintegral_le_of_forall_fin_meas_trim_le {μ : Measure α} (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] (C : ℝ≥0∞)
    {f : α → ℝ≥0∞} (hf : ∀ s, MeasurableSet[m] s → μ s ≠ ∞ → ∫⁻ x in s, f x ∂μ ≤ C) : ∫⁻ x, f x ∂μ ≤ C :=
  by
  have : ∫⁻ x in univ, f x ∂μ = ∫⁻ x, f x ∂μ := by simp only [Measure.restrict_univ]
  rw [← this]
  refine univ_le_of_forall_fin_meas_le hm C hf fun S _ hS_mono => ?_
  rw [setLIntegral_iUnion_of_directed]
  exact directed_of_isDirected_le hS_mono

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