integral_eq_of_tendsto_of_nonneg_ae

English

If hnng holds a.e. for f and integrability on φ i holds, then integrating the function on μ corresponds to the ae-nonneg bound for integrals.

Русский

Если hnng выполняется а.е. для f и интегрируемость на φ(i) держится, то интегрирование по μ соответствует ae-ограничению неотрицательности интегралов.

LaTeX

$$$(hnng) \\Rightarrow \\text{Integrator}$$$

Lean4

theorem integral_eq_of_tendsto_of_nonneg_ae [l.NeBot] [l.IsCountablyGenerated] {φ : ι → Set α} (hφ : AECover μ l φ)
    {f : α → ℝ} (I : ℝ) (hnng : 0 ≤ᵐ[μ] f) (hfi : ∀ n, IntegrableOn f (φ n) μ)
    (htendsto : Tendsto (fun n => ∫ x in φ n, f x ∂μ) l (𝓝 I)) : ∫ x, f x ∂μ = I :=
  have hfi' : Integrable f μ := hφ.integrable_of_integral_tendsto_of_nonneg_ae I hfi hnng htendsto
  hφ.integral_eq_of_tendsto I hfi' htendsto

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