exists_lt_lintegral_simpleFunc_of_lt_lintegral

English

If a ∉ s, then integrating over insert a s splits into a singleton part plus integration over s.

Русский

Если a ∉ s, то интегрирование по insert a s делится на вклад множества {a} и интеграл по s.

LaTeX

$$$\int_{\mathrm{insert}\,a\,s} f(x) \, d\mu = f(a) \mu\{a\} + \int_{s} f(x) \, d\mu$$$

Lean4

theorem exists_lt_lintegral_simpleFunc_of_lt_lintegral {m : MeasurableSpace α} {μ : Measure α} [SigmaFinite μ]
    {f : α → ℝ≥0} {L : ℝ≥0∞} (hL : L < ∫⁻ x, f x ∂μ) :
    ∃ g : α →ₛ ℝ≥0, (∀ x, g x ≤ f x) ∧ ∫⁻ x, g x ∂μ < ∞ ∧ L < ∫⁻ x, g x ∂μ :=
  by
  simp_rw [lintegral_eq_nnreal, lt_iSup_iff] at hL
  rcases hL with ⟨g₀, hg₀, g₀L⟩
  have h'L : L < ∫⁻ x, g₀ x ∂μ := by
    convert g₀L
    rw [← SimpleFunc.lintegral_eq_lintegral, SimpleFunc.coe_map]
    simp only [Function.comp_apply]
  rcases SimpleFunc.exists_lt_lintegral_simpleFunc_of_lt_lintegral h'L with ⟨g, hg, gL, gtop⟩
  exact ⟨g, fun x => (hg x).trans (coe_le_coe.1 (hg₀ x)), gL, gtop⟩

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