iSup_lintegral_measurable_le_eq_lintegral

English

For any ENNReal f, the iSup over all measurable g with g ≤ f of lintegral(g) equals lintegral(f).

Русский

Для любого f ∈ ENNReal, супр над измеримыми g с g ≤ f равен линегралу f.

LaTeX

$$$\forall f : α \to ENNReal,\; \text{Eq}(\; \sup\{ ∫^- a, g a ∂μ : g \text{ measurable}, g ≤ f \} , ∫^- a, f a ∂μ)$$$

Lean4

theorem iSup_lintegral_measurable_le_eq_lintegral (f : α → ℝ≥0∞) :
    ⨆ (g : α → ℝ≥0∞) (_ : Measurable g) (_ : g ≤ f), ∫⁻ a, g a ∂μ = ∫⁻ a, f a ∂μ :=
  by
  apply le_antisymm
  · exact iSup_le fun i => iSup_le fun _ => iSup_le fun h'i => lintegral_mono h'i
  · rw [lintegral]
    refine iSup₂_le fun i hi => le_iSup₂_of_le i i.measurable <| le_iSup_of_le hi ?_
    exact le_of_eq (i.lintegral_eq_lintegral _).symm

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