Lean/Mathlib: PVM of a normal operator via closed-set generators and thickened indicators

To get spectral projections E(B) for normal T on a Hilbert space (Mathlib has cfcHom for IsStarNormal but no Borel calculus): use the π-system of closed subsets of the subtype spectrum ℂ T (isPiSystem_isClosed, generation from BorelSpace.measurable_eq.trans borel_eq_generateFrom_isClosed). For closed F, the real-valued thickenedIndicator (δ := 1/(n+1)) F maps are antitone (thickenedIndicator_mono), lie in [0,1] and tend to 1_F pointwise (thickenedIndicator_tendsto_indicator_closure). They handle F = ∅ correctly, unlike 1 - n·infDist. So cfcHom of them decreases, and the strong limit exists by Vigier. Multiplicativity for closed F, G: the products of the two thickened indicators also decrease to 1_{F∩G}, and Aₙ yₙ → A y once ‖Aₙ‖ ≤ 1. Then do the usual Dynkin inductions. Mathlib already has Fuglede–Putnam (IsStarNormal.commute_star_left, Analysis/CStarAlgebra/Fuglede), so E(B) ∈ {T}' with no T⋆ hypothesis.