English
If f is measurable, then the pointwise supremum of eapprox f n equals f.
Русский
Если f измерима, то точечный супремум eapprox f n равен f.
LaTeX
$$$ \text{Measurable}(f) \Rightarrow \forall a, \; \big( \bigsqcup_{n} (eapprox f n) \big)(a) = f(a) $$$
Lean4
theorem iSup_eapprox_apply (hf : Measurable f) (a : α) : ⨆ n, (eapprox f n : α →ₛ ℝ≥0∞) a = f a :=
by
rw [eapprox, iSup_approx_apply ennrealRatEmbed f a hf rfl]
refine le_antisymm (iSup_le fun i => iSup_le fun hi => hi) (le_of_not_gt ?_)
intro h
rcases ENNReal.lt_iff_exists_rat_btwn.1 h with ⟨q, _, lt_q, q_lt⟩
have : (Real.toNNReal q : ℝ≥0∞) ≤ ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k :=
by
refine le_iSup_of_le (Encodable.encode q) ?_
rw [ennrealRatEmbed_encode q]
exact le_iSup_of_le (le_of_lt q_lt) le_rfl
exact lt_irrefl _ (lt_of_le_of_lt this lt_q)
