English
If the lintegral of f is finite, then for every positive ε there exists a simple φ ≤ f such that for any simple ψ ≤ f, the lintegral of ψ − φ is less than ε.
Русский
Если линеграл f конечен, то существует простая φ ≤ f с тем свойством, что для любой простой ψ ≤ f ∫ ψ − φ < ε.
LaTeX
$$$$ \text{If } \int^- x, f(x) \partial \mu ≠ ∞ \text{ and } ε ≠ 0, \; \exists φ: α \to_{\mathrm{simple}} \mathbb{R}_{\ge 0}, \; (∀ x, ↑(φ(x)) ≤ f(x)) \,\wedge \, \forall ψ: α \to_{\mathrm{simple}} \mathbb{R}_{\ge 0}, (∀ x, ↑(ψ(x)) ≤ f(x)) \Rightarrow (\operatorname{lintegral}( (↑) (ψ−φ) )) < ε. $$$$
Lean4
theorem exists_simpleFunc_forall_lintegral_sub_lt_of_pos {f : α → ℝ≥0∞} (h : ∫⁻ x, f x ∂μ ≠ ∞) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
∃ φ : α →ₛ ℝ≥0, (∀ x, ↑(φ x) ≤ f x) ∧ ∀ ψ : α →ₛ ℝ≥0, (∀ x, ↑(ψ x) ≤ f x) → (map (↑) (ψ - φ)).lintegral μ < ε :=
by
rw [lintegral_eq_nnreal] at h
have := ENNReal.lt_add_right h hε
erw [ENNReal.biSup_add] at this <;> [skip; exact ⟨0, fun x => zero_le _⟩]
simp_rw [lt_iSup_iff, iSup_lt_iff, iSup_le_iff] at this
rcases this with ⟨φ, hle : ∀ x, ↑(φ x) ≤ f x, b, hbφ, hb⟩
refine ⟨φ, hle, fun ψ hψ => ?_⟩
have : (map (↑) φ).lintegral μ ≠ ∞ := ne_top_of_le_ne_top h (by exact le_iSup₂ (α := ℝ≥0∞) φ hle)
rw [← ENNReal.add_lt_add_iff_left this, ← add_lintegral, ← SimpleFunc.map_add @ENNReal.coe_add]
refine (hb _ fun x => le_trans ?_ (max_le (hle x) (hψ x))).trans_lt hbφ
norm_cast
simp only [add_apply, sub_apply, add_tsub_eq_max]
rfl
