iSup_lintegral_eq_of_countably_generated

English

If hφ is an ae-cover along l and hfm is AEMeasurable, then the supremum over i of ∫⁻ x in φ i, f x dμ equals ∫⁻ x f x dμ.

Русский

Если hφ — ae-покрытие вдоль l и f — AEMeasurable, то наибольший интеграл по i равен интегралу по μ.

LaTeX

$$$⨆ i : ι, ∫⁻ x in φ i, f x ∂μ = ∫⁻ x, f x ∂μ$$$

Lean4

theorem iSup_lintegral_eq_of_countably_generated [Nonempty ι] [l.NeBot] [l.IsCountablyGenerated] {φ : ι → Set α}
    (hφ : AECover μ l φ) {f : α → ℝ≥0∞} (hfm : AEMeasurable f μ) : ⨆ i : ι, ∫⁻ x in φ i, f x ∂μ = ∫⁻ x, f x ∂μ :=
  by
  have := hφ.lintegral_tendsto_of_countably_generated hfm
  refine
    ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun i => lintegral_mono' Measure.restrict_le_self le_rfl) fun w hw =>
      ?_
  exact (this.eventually_const_lt hw).exists

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