English
Let ε > 0, ι be countable, and w : ι → ℝ≥0∞ with w i ≠ ∞ for all i. Then there exists δ : ι → ℝ≥0 with δ i > 0 for all i, such that the weighted sum ∑' i, w i * δ i is strictly less than ε.
Русский
Пусть ε > 0, ι счётно, и w : ι → ℝ≥0∞ так, что для всех i верно w i ≠ ∞. Тогда существует δ : ι → ℝ≥0, причём для всех i выполняется δ i > 0, и взвешенная сумма ∑' i w i δ i < ε.
LaTeX
$$$\\\\exists δ : ι → ℝ_{\\\\ge 0}, (∀ i, 0 < δ i) \\\\land \\\\sum' i, (w i * δ i : ℝ_{\\\\ge 0}^{∞}) < ε$$$
Lean4
theorem exists_pos_tsum_mul_lt_of_countable {ε : ℝ≥0∞} (hε : ε ≠ 0) {ι} [Countable ι] (w : ι → ℝ≥0∞)
(hw : ∀ i, w i ≠ ∞) : ∃ δ : ι → ℝ≥0, (∀ i, 0 < δ i) ∧ (∑' i, (w i * δ i : ℝ≥0∞)) < ε :=
by
lift w to ι → ℝ≥0 using hw
rcases exists_pos_sum_of_countable hε ι with ⟨δ', Hpos, Hsum⟩
have : ∀ i, 0 < max 1 (w i) := fun i ↦ zero_lt_one.trans_le (le_max_left _ _)
refine ⟨fun i ↦ δ' i / max 1 (w i), fun i ↦ div_pos (Hpos _) (this i), ?_⟩
refine lt_of_le_of_lt (ENNReal.tsum_le_tsum fun i ↦ ?_) Hsum
rw [coe_div (this i).ne']
refine mul_le_of_le_div' (mul_le_mul_left' (ENNReal.inv_le_inv.2 ?_) _)
exact coe_le_coe.2 (le_max_right _ _)
