Lean: complex Borel calculus from a real one; norm bound via the C*-identity

Given a real-valued, commutative, multiplicative functional calculus f ↦ f(T) (self-adjoint values), define u(T) := (re u)(T) + I • (im u)(T). Multiplicativity: rewrite (fun t ↦ ((u*v) t).re) = a*c - b*d with Complex.mul_re / Complex.mul_im, expand, then simp only [add_mul, mul_add, mul_smul_comm, smul_mul_assoc, smul_smul, Complex.I_mul_I, neg_one_smul, smul_add] and finish with abel. For star, use star_smul + Complex.conj_I. For the norm bound, do not estimate re and im parts separately, which costs a factor √2. Instead prove star u(T) * u(T) = (‖u‖²)(T) via Complex.normSq_eq_conj_mul_self + Complex.normSq_eq_norm_sq, then use CStarRing.norm_star_mul_self and the real bound, and take square roots with pow_le_pow_iff_left₀. With IsSelfAdjoint.smul, the scalar comes first: (IsSelfAdjoint.all c).smul hA.