English
The lintegral of f is the supremum over all NNReal-simple approximations φ ≤ f of the lintegral of φ mapped into ENNReal.
Русский
Линтеграл f равен супремуму по простым NNReal-функциям φ ≤ f их линегралу после отображения в ENNReal.
LaTeX
$$$$ \int^- a, f(a) \partial \mu = \big\!\big\sups \_{\varphi: a \mapsto \mathbb{R}_{\ge 0}, \ \forall x, \uparrow(\varphi(x)) \le f(x)} (\varphi.map(\uparrow))\operatorname{lintegral} \mu. $$$$
Lean4
/-- `∫⁻ a in s, f a ∂μ` is defined as the supremum of integrals of simple functions
`φ : α →ₛ ℝ≥0∞` such that `φ ≤ f`. This lemma says that it suffices to take
functions `φ : α →ₛ ℝ≥0`. -/
theorem lintegral_eq_nnreal {m : MeasurableSpace α} (f : α → ℝ≥0∞) (μ : Measure α) :
∫⁻ a, f a ∂μ = ⨆ (φ : α →ₛ ℝ≥0) (_ : ∀ x, ↑(φ x) ≤ f x), (φ.map ((↑) : ℝ≥0 → ℝ≥0∞)).lintegral μ :=
by
rw [lintegral]
refine le_antisymm (iSup₂_le fun φ hφ ↦ ?_) (iSup_mono' fun φ ↦ ⟨φ.map ((↑) : ℝ≥0 → ℝ≥0∞), le_rfl⟩)
by_cases h : ∀ᵐ a ∂μ, φ a ≠ ∞
· let ψ := φ.map ENNReal.toNNReal
replace h : ψ.map ((↑) : ℝ≥0 → ℝ≥0∞) =ᵐ[μ] φ := h.mono fun a => ENNReal.coe_toNNReal
have : ∀ x, ↑(ψ x) ≤ f x := fun x => le_trans ENNReal.coe_toNNReal_le_self (hφ x)
exact le_iSup₂_of_le (φ.map ENNReal.toNNReal) this (ge_of_eq <| lintegral_congr h)
· have h_meas : μ (φ ⁻¹' {∞}) ≠ 0 := mt measure_eq_zero_iff_ae_notMem.1 h
refine le_trans le_top (ge_of_eq <| (iSup_eq_top _).2 fun b hb => ?_)
obtain ⟨n, hn⟩ : ∃ n : ℕ, b < n * μ (φ ⁻¹' {∞}) := exists_nat_mul_gt h_meas (ne_of_lt hb)
use (const α (n : ℝ≥0)).restrict (φ ⁻¹' {∞})
simp only [lt_iSup_iff, exists_prop, coe_restrict, φ.measurableSet_preimage, coe_const, ENNReal.coe_indicator,
map_coe_ennreal_restrict, SimpleFunc.map_const, ENNReal.coe_natCast, restrict_const_lintegral]
refine ⟨indicator_le fun x hx => le_trans ?_ (hφ _), hn⟩
simp only [mem_preimage, mem_singleton_iff] at hx
simp only [hx, le_top]
