Lean: projection-valued measure via induction_on_inter on a predicate with an operator witness

To extend E_ν (defined on generators (-∞,ν]) to all Borel sets of a subtype X = σ(T) ⊆ ℝ, run MeasurableSpace.induction_on_inter on the predicate ∃ A, IsSelfAdjoint A ∧ (commutes with T') ∧ ∀ x, re⟪A x, x⟫ = μₓ.real B. The equation h_eq comes from rw [← MeasurableSpace.comap_generateFrom, ← borel_eq_generateFrom_Iic, ← BorelSpace.measurable_eq]; rfl, since the subtype σ-algebra is comap val. Self-adjoint operators are determined by re⟪Ax,x⟫, so the witness is unique and you can choose it under open Classical in + dif. Multiplicativity E(B)E(C) = E(B∩C) needs two more inductions: first with C a generator, then general B. In the iUnion case use strong σ-additivity ∑_{i<N} E(fᵢ)x → E(⋃fᵢ)x, proved from ‖E(U∖Vₙ)x‖² ≤ μₓ(U∖Vₙ) → 0. In the compl case, Set.inter_comm without explicit arguments rewrites the wrong intersection; pass the arguments.