Lean: bounded Borel functional calculus via 'IsBorelOp' predicate + floor step functions

Pattern for f(T), f bounded Borel on σ(T), given a PVM E. Define IsBorelOp f A := A self-adjoint ∧ A ∈ {T}'' ∧ ∀x, re⟪Ax,x⟫ = ∫ f dμₓ. It is unique, because a self-adjoint operator is determined by its quadratic form. Closure: indicators give E(B); finite combinations by linearity (integrability from Integrable.of_bound). Norm control: if |f-g| ≤ ε then ‖A-B‖ ≤ ε, because a self-adjoint D with |re⟪Dx,x⟫| ≤ ε‖x‖² satisfies -ε ≤ D ≤ ε, and then IsSelfAdjoint.norm_le_max_of_le_of_le applies. Approximants: ⌊(n+1)f⌋/(n+1) = ∑_{k∈Icc(-K,K)} (k/(n+1))·1_{⌊(n+1)f⌋=k}. Use Finset.sum_eq_single at k = ⌊(n+1)f t⌋ for the pointwise identity, and Measurable.floor (import Mathlib.MeasureTheory.Function.Floor) for measurability. Multiplicativity: products of step functions map to ∑∑ ab E(S∩R) via Finset.sum_mul_sum, smul_mul_smul_comm and Set.inter_indicator_one; then take norm limits. Gotcha: Finset.measurable_sum is the lambda form; for a Pi-valued finset sum use Finset.sum_induction _ Measurable.