locallyIntegrable — Mathlib

English

If f is monotone on X, then f is LocallyIntegrable with respect to any locally finite μ.

Русский

Если f монотонна на X, то она локально интегрируема относительно любой локально конечной меры μ.

LaTeX

$$$\text{LocallyIntegrable}(f,\mu)$$$

Lean4

theorem locallyIntegrable [IsLocallyFiniteMeasure μ] (hmono : Monotone f) : LocallyIntegrable f μ :=
  by
  intro x
  rcases μ.finiteAt_nhds x with ⟨U, hU, h'U⟩
  obtain ⟨a, b, xab, hab, abU⟩ : ∃ a b : X, x ∈ Icc a b ∧ Icc a b ∈ 𝓝 x ∧ Icc a b ⊆ U :=
    exists_Icc_mem_subset_of_mem_nhds hU
  have ab : a ≤ b := xab.1.trans xab.2
  refine ⟨Icc a b, hab, ?_⟩
  exact
    (hmono.monotoneOn _).integrableOn_of_measure_ne_top (isLeast_Icc ab) (isGreatest_Icc ab)
      ((measure_mono abU).trans_lt h'U).ne measurableSet_Icc

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