English
If ∫ f dμ is finite, there exists a measurable set s of finite measure such that ∫_{s^c} f dμ < ε for any ε > 0.
Русский
Если интеграл f по μ конечен, существует измеримое множество s с конечной мерой, such что ∫_{s^c} f dμ < ε для любого ε > 0.
LaTeX
$$$(hf : ∫⁻ a, f a ∂μ ≠ ∞) \\wedge (hε : ε ≠ 0) \\Rightarrow ∃ s, MeasurableSet s ∧ μ s < ∞ ∧ ∫⁻ a in s^c, f a ∂μ < ε$$$
Lean4
/-- If `f : α → ℝ≥0∞` has finite integral, then there exists a measurable set `s` of finite measure
such that the integral of `f` over `sᶜ` is less than a given positive number.
Also used to prove an `Lᵖ`-norm version in
`MeasureTheory.MemLp.exists_eLpNorm_indicator_compl_le`. -/
theorem exists_setLIntegral_compl_lt {f : α → ℝ≥0∞} (hf : ∫⁻ a, f a ∂μ ≠ ∞) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
∃ s : Set α, MeasurableSet s ∧ μ s < ∞ ∧ ∫⁻ a in sᶜ, f a ∂μ < ε :=
by
by_cases hf₀ : ∫⁻ a, f a ∂μ = 0
· exact ⟨∅, .empty, by simp, by simpa [hf₀, pos_iff_ne_zero]⟩
obtain ⟨g, hgf, hg_meas, hgsupp, hgε⟩ : ∃ g ≤ f, Measurable g ∧ μ (support g) < ∞ ∧ ∫⁻ a, f a ∂μ - ε < ∫⁻ a, g a ∂μ :=
by
obtain ⟨g, hgf, hgε⟩ : ∃ (g : α →ₛ ℝ≥0∞) (_ : g ≤ f), ∫⁻ a, f a ∂μ - ε < g.lintegral μ := by
simpa only [← lt_iSup_iff, ← lintegral_def] using ENNReal.sub_lt_self hf hf₀ hε
refine ⟨g, hgf, g.measurable, ?_, by rwa [g.lintegral_eq_lintegral]⟩
exact
SimpleFunc.FinMeasSupp.of_lintegral_ne_top <|
ne_top_of_le_ne_top hf <| g.lintegral_eq_lintegral μ ▸ lintegral_mono hgf
refine ⟨_, measurableSet_support hg_meas, hgsupp, ?_⟩
calc
∫⁻ a in (support g)ᶜ, f a ∂μ = ∫⁻ a in (support g)ᶜ, f a - g a ∂μ :=
setLIntegral_congr_fun (measurableSet_support hg_meas).compl <| by intro; simp_all
_ ≤ ∫⁻ a, f a - g a ∂μ := (setLIntegral_le_lintegral _ _)
_ = ∫⁻ a, f a ∂μ - ∫⁻ a, g a ∂μ :=
(lintegral_sub hg_meas (ne_top_of_le_ne_top hf <| lintegral_mono hgf) (ae_of_all _ hgf))
_ < ε := ENNReal.sub_lt_of_lt_add (lintegral_mono hgf) <| ENNReal.lt_add_of_sub_lt_left (.inl hf) hgε
