English
In a sigma-finite space, there exists a positive function g with finite integral that can be made arbitrarily small.
Русский
В σ-конечной мере существует положительная функция g с конечным интегралом, который можно сделать сколь угодно малым.
LaTeX
$$∃ g : α → ℝ≥0, (∀ x, 0 < g(x)) ∧ Measurable g ∧ ∫⁻ x, g x ∂μ < ε$$
Lean4
/-- In a sigma-finite measure space, there exists an integrable function which is
positive everywhere (and with an arbitrarily small integral). -/
theorem exists_pos_lintegral_lt_of_sigmaFinite (μ : Measure α) [SigmaFinite μ] {ε : ℝ≥0∞} (ε0 : ε ≠ 0) :
∃ g : α → ℝ≥0, (∀ x, 0 < g x) ∧ Measurable g ∧ ∫⁻ x, g x ∂μ < ε := by
/- Let `s` be a covering of `α` by pairwise disjoint measurable sets of finite measure. Let
`δ : ℕ → ℝ≥0` be a positive function such that `∑' i, μ (s i) * δ i < ε`. Then the function that
is equal to `δ n` on `s n` is a positive function with integral less than `ε`. -/
set s : ℕ → Set α := disjointed (spanningSets μ)
have : ∀ n, μ (s n) < ∞ := fun n => (measure_mono <| disjointed_subset _ _).trans_lt (measure_spanningSets_lt_top μ n)
obtain ⟨δ, δpos, δsum⟩ : ∃ δ : ℕ → ℝ≥0, (∀ i, 0 < δ i) ∧ (∑' i, μ (s i) * δ i) < ε :=
ENNReal.exists_pos_tsum_mul_lt_of_countable ε0 _ fun n => (this n).ne
set N : α → ℕ := spanningSetsIndex μ
have hN_meas : Measurable N := measurableSet_spanningSetsIndex μ
have hNs : ∀ n, N ⁻¹' { n } = s n := preimage_spanningSetsIndex_singleton μ
refine ⟨δ ∘ N, fun x => δpos _, measurable_from_nat.comp hN_meas, ?_⟩
erw [lintegral_comp measurable_from_nat.coe_nnreal_ennreal hN_meas]
simpa [N, hNs, lintegral_countable', measurableSet_spanningSetsIndex, mul_comm] using δsum
