English
For a rational q, ennrealRatEmbed (Encodable.encode q) equals ENNReal.ofNNReal (Real.toNNReal q).
Русский
Для рационального q: ennrealRatEmbed(Encodable.encode q) = ENNReal.ofNNReal(Real.toNNReal q).
LaTeX
$$$ ennrealRatEmbed(Encodable.encode\ q) = ENNReal.ofNNReal\left( Real.toNNReal\ q \right)$$$
Lean4
theorem sum_eapproxDiff (f : α → ℝ≥0∞) (n : ℕ) (a : α) :
(∑ k ∈ Finset.range (n + 1), (eapproxDiff f k a : ℝ≥0∞)) = eapprox f n a := by
induction n with
| zero => simp [eapproxDiff, (eapprox_lt_top f 0 a).ne]
| succ n
IH =>
rw [Finset.sum_range_succ, IH, eapproxDiff, coe_map, Function.comp_apply, coe_sub, Pi.sub_apply,
ENNReal.coe_toNNReal, add_tsub_cancel_of_le (monotone_eapprox f (Nat.le_succ _) _)]
apply (lt_of_le_of_lt _ (eapprox_lt_top f (n + 1) a)).ne
rw [tsub_le_iff_right]
exact le_self_add
