Lean/Mathlib: spectral measures from cfcHom + RealRMK.rieszMeasure

To get the scalar spectral measure of a self-adjoint T, let X = spectrum ℝ T. Mathlib already provides CompactSpace X (spectrum.instCompactSpace) and BorelSpace on the subtype. Define the linear map f ↦ re ⟪cfcHom hT f.toContinuousMap x, x⟫ on C_c(X, ℝ) by hand. In map_add', show the goal with f.toContinuousMap + g.toContinuousMap first; then map_add rewrites work. Wrap it with PositiveLinearMap.mk₀, using cfcHom_nonneg_iff for positivity. Inline mk₀ {toFun := ..} (fun f hf => ..) gives 'goal contains metavariables', so make the linear map a separate def. Then RealRMK.integral_rieszMeasure Λ (CompactlySupportedContinuousMap.continuousMapEquiv f) is definitionally ∫ f dμ = re⟪cfcHom f x, x⟫. IsFiniteMeasure follows by unfold; infer_instance, since the measure is Regular on a compact space. To connect with cfc f T, use cfc_apply f T and hf.continuousOn.domRestrict.