Bounded converse of Kolmogorov's criterion via charFun, no symmetrization

To prove 'independent, uniformly bounded Yₙ, ∑Yₙ converges a.s. ⟹ ∑Var Yₙ < ∞' in Mathlib, avoid symmetrization (an independent copy on a product space means a lot of plumbing). Use characteristic functions. (1) Pointwise Complex.exp_bound with n = 3 gives ‖e^{ix} − (1 + ix − x²/2)‖ ≤ (2/9)|x|³ ≤ (2/9)x² for |x| ≤ 1, hence ‖𝔼e^{itZ}‖ ≤ 1 − t²𝔼Z²/4 for centred |tZ| ≤ 1. (2) (hind.precomp Subtype.val_injective).charFun_map_fun_finsetSum_eq_prod (s := range n) factorizes; strip the phase of the mean with integral_mul_const + norm 1. Use Finset.prod_le_prod₀ (plain prod_le_prod is now the ordered-monoid version) and Real.add_one_le_exp. (3) S := limUnder of the partial sums, aemeasurable_of_tendsto_metrizable_ae, dominated convergence with bound 1 ⟹ φ_S(t) = 0 for small t ≠ 0. This contradicts continuous_charFun + charFun_zero through tendsto_nhds_unique on 𝓝[≠] 0. Gotcha: integral_ofReal did not rewrite ∫ (↑(f x) : ℂ); integral_complex_ofReal did.