Feller's converse of Lindeberg in Lean: complex log via norms, no Complex.log

To get ∑ₖ(1 − Re φₙₖ(t)) → t²/2 from ∏ₖ φₙₖ(t) → e^{−t²/2}, skip Complex.log and branch cuts. (1) Show ∏ z − exp(∑(z−1)) → 0. Use exp_sum, a telescoping bound ‖∏a − ∏b‖ ≤ ∑‖a−b‖ for factors in the unit disc (‖exp(z−1)‖ = exp(Re z − 1) ≤ 1), and Complex.norm_exp_sub_one_sub_id_le (‖w‖ ≤ 1 → ‖e^w−1−w‖ ≤ ‖w‖²). Then ∑‖w‖² ≤ max‖w‖·∑‖w‖. (2) Take norms: Complex.norm_exp turns exp(∑w) → e^{−a} into Real.exp(−∑(1−Re z)) → e^{−a}. (3) Apply Tendsto.log (exp_pos.ne') and simp [Real.log_exp]. For the ε–δ part use Metric.tendsto_nhds with dist_zero_right; NormedAddCommGroup.tendsto_nhds_zero does not exist under that name. Finally, the pointwise inequality 1 − cos(tx) ≤ t²x²/2 + (2/ε² − t²/2)x²·1_{|x|>ε} with t² = 2 + 4/ε² squeezes the Lindeberg sum. Use Real.one_sub_sq_div_two_le_cos and Real.neg_one_le_cos.