The scalar spectral functional as an ℝ-linear map on compactly-supported continuous functions on the spectrum: f ↦ re ⟪x, f(T) x⟫, where f(T) := cfcHom ha f.

\mathrm{specFunctional}\,H\,T\,x \;:=\; \{\mathrm{toFun} :=\lambda f \mapsto \mathrm{re}\,(\langle {x},{((\mathrm{cfcHom}\,\mathrm{ha})\,f.\mathrm{toContinuousMap})\,x}\rangle) , \mathrm{map\_add}^{\prime} :=\cdots , \mathrm{map\_smul}^{\prime} :=\cdots \}

Used by specPLM.

Definition 675 (specPLM). source ↗

The scalar spectral functional bundled as a positive linear functional Λ_x : C_c(spectrum ℝ T, ℝ) →ₚ[ℝ] ℝ.

Used by specMeasure, integral_specMeasure, instIsFiniteMeasureElemRealSpectrumContinuousLinearMapComplexIdSpecMeasure.

Definition 676 (specMeasure). source ↗

The scalar spectral measure μ_x of a self-adjoint T at a vector x: the Riesz–Markov measure of the positive functional Λ_x = specPLM.

\mu_{\mathrm{sp}}\,H\,T\,x \;:=\; \mathrm{rieszMeasure}\,(\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specplm}{\mathrm{specPLM}}\,T\,\mathrm{ha}\,x)

Used by congr_simp, integral_specMeasure, instIsFiniteMeasureElemRealSpectrumContinuousLinearMapComplexIdSpecMeasure, specMeasure_real_univ, specMeasure_real_le, specMeasure_smul, specMeasure_parallelogram, specMeasure_add, and 22 more.

Lemma 677 (integral_specMeasure). source ↗

Defining property of the scalar spectral measure (Riesz–Markov representation): ∫ f dμ_x = re ⟪x, f(T) x⟫ for every f ∈ C_c(spectrum ℝ T, ℝ).

\int (s : (\mathrm{sp}\,\mathbb{R}\,T)), f\,s \partial \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,x = \mathrm{re}\,(\langle {x},{((\mathrm{cfcHom}\,\mathrm{ha})\,f.\mathrm{toContinuousMap})\,x}\rangle)

Proof. By specPLM. $\square$

Used by specMeasure_real_univ, specMeasure_smul, specMeasure_parallelogram, specMeasure_add, integral_specMeasure_cont, re_inner_T_eq_integral.

Lemma 678 (instIsFiniteMeasureElemRealSpectrumContinuousLinearMapComplexIdSpecMeasure). source ↗

μ_x is a finite measure (the spectrum is compact).

\mathrm{IsFiniteMeasure}\,(\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,x)

Proof. By specPLM. $\square$

Used by specMeasure_real_le, specMeasure_smul, specMeasure_parallelogram, specMeasure_add, qForm_parallelogram, qForm_add, qForm_union, specProj_hasSum, and 6 more.

Lemma 679 (specMeasure_real_univ). source ↗

Total mass of the scalar spectral measure — the scalar-level E(univ) = 1: μ_x(univ) = ‖x‖² (as a real number), since 1(T) = 1 and re ⟪x, x⟫ = ‖x‖².

(\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,x).\mathrm{real} = {\|x\|}^{2}

Proof. By integral_specMeasure. $\square$

Used by specMeasure_real_le, qForm_univ.

Lemma 680 (specMeasure_real_le). source ↗

Per-set bound for the scalar spectral measure: μ_z(B) ≤ ‖z‖² for every set B (monotonicity against the total mass μ_z(univ) = ‖z‖²). This feeds the operator-norm bound on the spectral projections E(B).

(\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,z).\mathrm{real}\,B \le {\|z\|}^{2}

Proof. By instIsFiniteMeasureElemRealSpectrumContinuousLinearMapComplexIdSpecMeasure, specMeasure_real_univ. $\square$

Used by bForm_abs_le, specProj_le_one.

Lemma 681 (specMeasure_smul). source ↗

Scaling law of the scalar spectral measure: μ_{c•x} = ‖c‖² · μ_x.

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(c \cdot x) = {\|c\|_{+}}^{2} \cdot \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,x

Proof. By integral_specMeasure, instIsFiniteMeasureElemRealSpectrumContinuousLinearMapComplexIdSpecMeasure. $\square$

Used by specMeasure_zero, qForm_smul.

Lemma 682 (specMeasure_parallelogram). source ↗

Parallelogram law of the scalar spectral measure: μ_{x+y} + μ_{x−y} = 2·μ_x + 2·μ_y (the cross terms of the quadratic form cancel). Holds for any operator; the engine for sesquilinearity of the polarized form.

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(x + y) + \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(x - y) = 2 \cdot \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,x + 2 \cdot \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,y

Proof. By integral_specMeasure, instIsFiniteMeasureElemRealSpectrumContinuousLinearMapComplexIdSpecMeasure. $\square$

Used by qForm_parallelogram.

Lemma 683 (specMeasure_add). source ↗

Additivity engine (measure level): the second-difference identity μ_{x+a+b} + μ_{x−a} + μ_{x−b} = μ_{x−a−b} + μ_{x+a} + μ_{x+b} (both sides expand to 3q(x)+2q(a)+2q(b)+g(a,b) for the quadratic form q and its symmetric bilinear part g). Applied with (a,b)=(y₁,y₂) and (a,b)=(I·y₁, I·y₂) it yields additivity of the polarized spectral form in y.

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(x + a + b) + \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(x - a) + \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(x - b) = \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(x - a - b) + \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(x + a) + \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(x + b)

Proof. By integral_specMeasure, instIsFiniteMeasureElemRealSpectrumContinuousLinearMapComplexIdSpecMeasure. $\square$

Used by qForm_add.

Definition 684 (qForm). source ↗

The diagonal quadratic form q_s(z) = μ_z(s) (real, nonnegative).

q\,H\,T\,s\,z \;:=\; (\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,z).\mathrm{real}\,s

Used by congr_simp, qForm_nonneg, qForm_zero, qForm_smul, qForm_neg, qForm_parallelogram, qForm_add, bForm, and 23 more.

Lemma 685 (qForm_nonneg). source ↗

0 \le \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,z

Proof. By specMeasure. $\square$

Used by bForm_sq_le, bForm_abs_le, specProj_isPositive.

Lemma 686 (specMeasure_zero). source ↗

μ_0 = 0 (the zero vector gives the zero measure).

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,0 = 0

Proof. By congr_simp, specMeasure_smul. $\square$

Used by qForm_zero.

Lemma 687 (qForm_zero). source ↗

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,0 = 0

Proof. By specMeasure, specMeasure_zero. $\square$

Used by bForm_self.

Lemma 688 (qForm_smul). source ↗

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,(c \cdot z) = {\|c\|}^{2} \cdot \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,z

Proof. By specMeasure, specMeasure_smul. $\square$

Used by qForm_neg, bForm_self, qForm_real_smul, bForm_I_smul.

Lemma 689 (qForm_neg). source ↗

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,(-z) = \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,z

Proof. By congr_simp, qForm_smul. $\square$

Used by bForm_comm.

Lemma 690 (qForm_parallelogram). source ↗

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,(x + y) + \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,(x - y) = 2 \cdot \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,x + 2 \cdot \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,y

Proof. By specMeasure, instIsFiniteMeasureElemRealSpectrumContinuousLinearMapComplexIdSpecMeasure, specMeasure_parallelogram. $\square$

Used by qForm_add_expand.

Lemma 691 (qForm_add). source ↗

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,(x + a + b) + \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,(x - a) + \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,(x - b) = \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,(x - a - b) + \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,(x + a) + \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,(x + b)

Proof. By specMeasure, instIsFiniteMeasureElemRealSpectrumContinuousLinearMapComplexIdSpecMeasure, specMeasure_add. $\square$

Used by bForm_add_right.

Definition 692 (bForm). source ↗

The polarized bilinear form b_s(u,v) = ¼(q_s(u+v) − q_s(u−v)).

b\,H\,T\,s\,u\,v \;:=\; (\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,(u + v) - \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,(u - v)) / 4

Used by congr_simp, qForm_add_expand, bForm_self, bForm_comm, bForm_add_right, bForm_zero_right, bFormRight, bForm_sq_le, and 22 more.

Lemma 693 (qForm_add_expand). source ↗

Expansion identity: q_s(p+q) = q_s(p) + q_s(q) + 2 b_s(p,q) (from the parallelogram law).

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,(p + q) = \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,p + \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,q + 2 \cdot \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,p\,q

Proof. By qForm_parallelogram. $\square$

Used by bForm_sq_le.

Lemma 694 (bForm_self). source ↗

b_s(u,u) = q_s(u).

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,u\,u = \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,u

Proof. By qForm_zero, qForm_smul. $\square$

Used by reApplyInnerSelf_specProj.

Lemma 695 (bForm_comm). source ↗

b_s is symmetric.

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,u\,v = \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,v\,u

Proof. By qForm, qForm_neg. $\square$

Used by cForm_hermitian, bForm_sub_left.

Lemma 696 (bForm_add_right). source ↗

b_s is additive in its right argument.

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,u\,(v + w) = \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,u\,v + \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,u\,w

Proof. By qForm, qForm_add. $\square$

Used by bFormRight, bForm_sub_right, cForm_add_right.

Lemma 697 (qForm_real_smul). source ↗

Real-scalar version of the scaling law: q_s(r•z) = r²·q_s(z).

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,(r \cdot z) = {r}^{2} \cdot \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,z

Proof. By qForm_smul. $\square$

Used by bForm_sq_le.

Lemma 698 (bForm_zero_right). source ↗

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,u\,0 = 0

Proof. By congr_simp, qForm. $\square$

Used by bFormRight.

Definition 699 (bFormRight). source ↗

b_s(u, ·) bundled as an additive homomorphism (used for ℚ-homogeneity in Cauchy–Schwarz).

\mathrm{bFormRight}\,H\,T\,s\,u \;:=\; \{\mathrm{toFun} :=\lambda w \mapsto \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,u\,w , \mathrm{map\_zero}^{\prime} :=\cdots , \mathrm{map\_add}^{\prime} :=\cdots \}

Used by bForm_sq_le, bForm_real_smul_right.

Lemma 700 (bForm_sq_le). source ↗

Cauchy–Schwarz for the spectral form: b_s(u,v)² ≤ q_s(u)·q_s(v). Because q_s ≥ 0, the quadratic t ↦ q_s(u + t•v) = q_s(v)·t² + 2 b_s(u,v)·t + q_s(u) is nonnegative on ℚ (hence on ℝ by density), so its discriminant is ≤ 0.

{\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,u\,v}^{2} \le \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,u \cdot \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,v

Proof. By qForm_nonneg, qForm_add_expand, qForm_real_smul, bFormRight. $\square$

Used by bForm_abs_le.

Lemma 701 (bForm_sub_right). source ↗

b_s is subtractive in its right argument.

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,u\,(v - w) = \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,u\,v - \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,u\,w

Proof. By bForm_add_right. $\square$

Used by bForm_continuous_right, bForm_sub_left.

Lemma 702 (bForm_abs_le). source ↗

Boundedness of the spectral form: |b_s(u,v)| ≤ ‖u‖·‖v‖ (from Cauchy–Schwarz and q_s(z) ≤ ‖z‖²).

|\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,u\,v| \le \|u\| \cdot \|v\|

Proof. By specMeasure_real_le, qForm, qForm_nonneg, bForm_sq_le. $\square$

Used by bForm_continuous_right, cForm_norm_le.

Lemma 703 (bForm_continuous_right). source ↗

b_s(u, ·) is continuous (Lipschitz with constant ‖u‖).

\mathrm{Continuous}\,\lambda v \mapsto \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,u\,v

Proof. By bForm_sub_right, bForm_abs_le. $\square$

Used by bForm_real_smul_right.

Lemma 704 (bForm_real_smul_right). source ↗

ℝ-homogeneity of b_s(u, ·) (continuity + map_real_smul).

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,u\,(r \cdot v) = r \cdot \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,u\,v

Proof. By bFormRight, bForm_continuous_right. $\square$

Used by bForm_neg_right.

Lemma 705 (bForm_neg_right). source ↗

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,u\,(-v) = -\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,u\,v

Proof. By congr_simp, bForm_real_smul_right. $\square$

Used by bForm_I_comm.

Lemma 706 (bForm_I_smul). source ↗

b_s is invariant under simultaneous multiplication by i: b_s(I•u, I•v) = b_s(u,v) (from the i-invariance q_s(I•z) = q_s(z)).

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,(i \cdot u)\,(i \cdot v) = \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,u\,v

Proof. By qForm, qForm_smul. $\square$

Used by bForm_I_comm.

Lemma 707 (bForm_I_comm). source ↗

The i-twist: b_s(I•x, y) = − b_s(x, I•y).

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,(i \cdot x)\,y = -\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,x\,(i \cdot y)

Proof. By bForm_neg_right, bForm_I_smul. $\square$

Used by cForm_hermitian.

Definition 708 (cForm). source ↗

The complex spectral form c_s(x,y) = b_s(x,y) − i·b_s(x, I•y); its Riesz representation will be the spectral projection E(s), with ⟪E(s) x, y⟫ = c_s(x,y).

c\,H\,T\,s\,x\,y \;:=\; (\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,x\,y) - i \cdot (\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,x\,(i \cdot y))

Used by cForm_add_right, cForm_norm_le, cFormCLM, cFormCLM_norm_le, inner_specProj, cForm_empty, specProj_empty, cForm_hermitian, and 8 more.

Lemma 709 (cForm_add_right). source ↗

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-cform}{c}\,T\,\mathrm{ha}\,s\,x\,(y + z) = \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-cform}{c}\,T\,\mathrm{ha}\,s\,x\,y + \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-cform}{c}\,T\,\mathrm{ha}\,s\,x\,z

Proof. By bForm, bForm_add_right. $\square$

Used by cFormCLM, cFormCLM_norm_le.

Lemma 710 (cForm_norm_le). source ↗

Norm bound: ‖c_s(x,y)‖ ≤ 2·‖x‖·‖y‖.

\|\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-cform}{c}\,T\,\mathrm{ha}\,s\,x\,y\| \le 2 \cdot \|x\| \cdot \|y\|

Proof. By bForm, bForm_abs_le. $\square$

Used by cFormCLM, cFormCLM_norm_le.

Definition 711 (cFormCLM). source ↗

c_s(x, ·) bundled as a continuous ℂ-linear functional H →L[ℂ] ℂ.

\mathrm{cFormCLM}\,H\,T\,s\,x \;:=\; \{\mathrm{toFun} :=\lambda y \mapsto \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-cform}{c}\,T\,\mathrm{ha}\,s\,x\,y , \mathrm{map\_add}^{\prime} :=\cdots , \mathrm{map\_smul}^{\prime} :=\cdots \}.\mathrm{mkContinuous}\,(2 \cdot \|x\|)\,\cdots

Used by cFormCLM_norm_le, specProj, inner_specProj.

Lemma 712 (cFormCLM_norm_le). source ↗

\|\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-cformclm}{\mathrm{cFormCLM}}\,T\,\mathrm{ha}\,s\,x\| \le 2 \cdot \|x\|

Proof. By cForm, cForm_add_right, cForm_norm_le. $\square$

Used by specProj, inner_specProj.

Definition 713 (specProj). source ↗

The spectral projection E(s) : H →L[ℂ] H, obtained by Riesz-representing the bounded sesquilinear form c_s (⟪E(s) x, y⟫ = c_s(x,y)).

E\,H\,T\,s \;:=\; \mathrm{continuousLinearMapOfBilin}\,(\{\mathrm{toFun} :=\lambda x \mapsto \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-cformclm}{\mathrm{cFormCLM}}\,T\,\mathrm{ha}\,s\,x , \mathrm{map\_add}^{\prime} :=\cdots , \mathrm{map\_smul}^{\prime} :=\cdots \}.\mathrm{mkContinuous}\,2\,\cdots )

Used by congr_simp, inner_specProj, specProj_empty, specProj_isSelfAdjoint, specProj_univ, reApplyInnerSelf_specProj, specProj_isPositive, specProj_union_disjoint, and 10 more.

Lemma 714 (inner_specProj). source ↗

Defining identity of the spectral projection: ⟪E(s) x, y⟫ = c_s(x,y).

\langle {(\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specproj}{E}\,T\,\mathrm{ha}\,s)\,x},{y}\rangle = \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-cform}{c}\,T\,\mathrm{ha}\,s\,x\,y

Proof. By cFormCLM, cFormCLM_norm_le. $\square$

Used by specProj_empty, specProj_isSelfAdjoint, specProj_univ, reApplyInnerSelf_specProj, specProj_union_disjoint, re_inner_cfcHom_specProj, specProj_inter.

Lemma 715 (cForm_empty). source ↗

c_∅ = 0.

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-cform}{c}\,T\,\mathrm{ha}\,\emptyset \,x\,y = 0

Proof. By specMeasure, qForm, bForm. $\square$

Used by specProj_empty.

Lemma 716 (specProj_empty). source ↗

E(∅) = 0.

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specproj}{E}\,T\,\mathrm{ha}\,\emptyset = 0

Proof. By cForm, inner_specProj, cForm_empty. $\square$

Used by specProj_finset_sum, PVM_of_selfAdjoint.

Lemma 717 (cForm_hermitian). source ↗

Hermitian symmetry of the form: conj(c_s(y,x)) = c_s(x,y).

(\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-cform}{c}\,T\,\mathrm{ha}\,s\,y\,x) = \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-cform}{c}\,T\,\mathrm{ha}\,s\,x\,y

Proof. By bForm, bForm_comm, bForm_I_comm. $\square$

Used by specProj_isSelfAdjoint.

Lemma 718 (specProj_isSelfAdjoint). source ↗

E(s) is self-adjoint.

\mathrm{IsSelfAdjoint}\,(\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specproj}{E}\,T\,\mathrm{ha}\,s)

Proof. By cForm, inner_specProj, cForm_hermitian. $\square$

Used by specProj_isPositive, specProj_le_one, norm_specProj_sq_le, re_inner_cfcHom_specProj, specProj_inter, PVM_of_selfAdjoint, scalarMeasure_eq_specMeasure.

Lemma 719 (qForm_univ). source ↗

q_univ(z) = ‖z‖².

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,z = {\|z\|}^{2}

Proof. By specMeasure_real_univ. $\square$

Used by bForm_univ.

Lemma 720 (bForm_univ). source ↗

b_univ(x,y) = re ⟪x,y⟫ (polarization of the norm).

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,x\,y = \mathrm{re}\,(\langle {x},{y}\rangle)

Proof. By qForm, qForm_univ. $\square$

Used by cForm_univ.

Lemma 721 (cForm_univ). source ↗

c_univ(x,y) = ⟪x,y⟫.

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-cform}{c}\,T\,\mathrm{ha}\,x\,y = \langle {x},{y}\rangle

Proof. By bForm, bForm_univ. $\square$

Used by specProj_univ.

Lemma 722 (specProj_univ). source ↗

E(univ) = 1.

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specproj}{E}\,T\,\mathrm{ha} = 1

Proof. By cForm, inner_specProj, cForm_univ. $\square$

Used by PVM_of_selfAdjoint.

Lemma 723 (reApplyInnerSelf_specProj). source ↗

The diagonal of the spectral form is the (real, nonnegative) quadratic form: re ⟪E(s) x, x⟫ = q_s(x).

(\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specproj}{E}\,T\,\mathrm{ha}\,s).\mathrm{reApplyInnerSelf}\,x = \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,x

Proof. By bForm, bForm_self, cForm, inner_specProj. $\square$

Used by specProj_isPositive, specProj_le_one, norm_specProj_sq_le, scalarMeasure_eq_specMeasure.

Lemma 724 (specProj_isPositive). source ↗

E(s) is a positive operator.

(\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specproj}{E}\,T\,\mathrm{ha}\,s).\mathrm{IsPositive}

Proof. By qForm, qForm_nonneg, specProj_isSelfAdjoint, reApplyInnerSelf_specProj. $\square$

Used by norm_specProj_sq_le.

Lemma 725 (qForm_union). source ↗

Finite additivity of the diagonal form on disjoint sets.

\mathrm{Disjoint}\,s\,t \to \mathrm{MeasurableSet}\,t \to \forall (z : H), \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,(s \cup t)\,z = \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,z + \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,t\,z

Proof. By specMeasure, instIsFiniteMeasureElemRealSpectrumContinuousLinearMapComplexIdSpecMeasure. $\square$

Used by cForm_union_disjoint.

Lemma 726 (cForm_union_disjoint). source ↗

Finite additivity of the complex form on disjoint sets.

\mathrm{Disjoint}\,s\,t \to \mathrm{MeasurableSet}\,t \to \forall (x y : H), \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-cform}{c}\,T\,\mathrm{ha}\,(s \cup t)\,x\,y = \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-cform}{c}\,T\,\mathrm{ha}\,s\,x\,y + \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-cform}{c}\,T\,\mathrm{ha}\,t\,x\,y

Proof. By qForm, bForm, qForm_union. $\square$

Used by specProj_union_disjoint.

Lemma 727 (specProj_union_disjoint). source ↗

Finite additivity of the spectral projection on disjoint measurable sets: E(s ∪ t) = E(s) + E(t).

\mathrm{Disjoint}\,s\,t \to \mathrm{MeasurableSet}\,t \to \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specproj}{E}\,T\,\mathrm{ha}\,(s \cup t) = \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specproj}{E}\,T\,\mathrm{ha}\,s + \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specproj}{E}\,T\,\mathrm{ha}\,t

Proof. By cForm, inner_specProj, cForm_union_disjoint. $\square$

Used by specProj_finset_sum, specProj_hasSum.

Lemma 728 (specProj_le_one). source ↗

E(s) ≤ 1 (the spectral projection is a contraction in the Loewner order): 1 − E(s) is positive since re ⟪(1−E(s)) x, x⟫ = ‖x‖² − q_s(x) ≥ 0.

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specproj}{E}\,T\,\mathrm{ha}\,s \le 1

Proof. By specMeasure_real_le, qForm, specProj_isSelfAdjoint, reApplyInnerSelf_specProj. $\square$

Used by norm_specProj_sq_le.

Lemma 729 (norm_specProj_sq_le). source ↗

Effect estimate: for the positive contraction E(s), ‖E(s) x‖² ≤ q_s(x). (From E(s)² ≤ E(s), i.e. E(s)·(1−E(s)) ≥ 0 for commuting positives.)

{\|(\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specproj}{E}\,T\,\mathrm{ha}\,s)\,x\|}^{2} \le \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-qform}{q}\,T\,\mathrm{ha}\,s\,x

Proof. By specProj_isSelfAdjoint, reApplyInnerSelf_specProj, specProj_isPositive, specProj_le_one. $\square$

Used by specProj_hasSum.

Lemma 730 (specProj_finset_sum). source ↗

Finite (Finset) additivity of the spectral projection over pairwise-disjoint measurable sets: ∑ n ∈ F, E(A n) = E(⋃ n ∈ F, A n).

(\forall (n : \mathbb{N}), \mathrm{MeasurableSet}\,(A\,n)) \to (\mathrm{Pairwise}\,\lambda m n \mapsto \mathrm{Disjoint}\,(A\,m)\,(A\,n)) \to \forall (F : \mathrm{Finset}\,\mathbb{N}), \sum_{n F} \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specproj}{E}\,T\,\mathrm{ha}\,(A\,n) = \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specproj}{E}\,T\,\mathrm{ha}\,(\bigcup n\in F, A\,n)

Proof. By congr_simp, specProj_empty, specProj_union_disjoint. $\square$

Used by specProj_hasSum.

Lemma 731 (specProj_hasSum). source ↗

σ-additivity of the spectral projection (strong/SOT): for pairwise-disjoint measurable A, HasSum (fun n => E(A n) x) (E(⋃ n, A n) x). Proved by a norm-tail estimate: ‖∑_{n∈s} E(A n) x − E(⋃A) x‖² ≤ q_{(⋃A)∖(⋃_s)}(x) = q_{⋃A}(x) − ∑_{n∈s} q_{A n}(x) → 0 (effect estimate + scalar measure σ-additivity).

(\forall (n : \mathbb{N}), \mathrm{MeasurableSet}\,(A\,n)) \to (\mathrm{Pairwise}\,\lambda m n \mapsto \mathrm{Disjoint}\,(A\,m)\,(A\,n)) \to \forall (x : H), \mathrm{HasSum}\,(\lambda n \mapsto (\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specproj}{E}\,T\,\mathrm{ha}\,(A\,n))\,x)\,((\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specproj}{E}\,T\,\mathrm{ha}\,(\bigcup n, A\,n))\,x)

Proof. By specMeasure, instIsFiniteMeasureElemRealSpectrumContinuousLinearMapComplexIdSpecMeasure, qForm, specProj_union_disjoint, norm_specProj_sq_le, specProj_finset_sum. $\square$

Used by PVM_of_selfAdjoint.

Lemma 732 (inner_cfcHom_mul). source ↗

cfcHom-multiplicativity in the inner product: ⟪g(T)x, h(T)y⟫ = ⟪x, (g·h)(T)y⟫ (self-adjointness of g(T) + cfcHom is an algebra hom). This is the clean engine for the off-diagonal measure identity ν_{g(T)x,y} = g·ν_{x,y} that yields E_inter directly.

\langle {((\mathrm{cfcHom}\,\mathrm{ha})\,g)\,x},{((\mathrm{cfcHom}\,\mathrm{ha})\,h)\,y}\rangle = \langle {x},{((\mathrm{cfcHom}\,\mathrm{ha})\,(g \cdot h))\,y}\rangle

Proof. Immediate from the definitions. $\square$

Used by specMeasure_engine.

Lemma 733 (integral_specMeasure_cont). source ↗

Bridge: the scalar-measure integral of a continuous h is re ⟪z, h(T) z⟫ (the C_c version integral_specMeasure specialised via HasCompactSupport.of_compactSpace).

\int (\omega : (\mathrm{sp}\,\mathbb{R}\,T)), h\,\omega \partial \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,z = \mathrm{re}\,(\langle {z},{((\mathrm{cfcHom}\,\mathrm{ha})\,h)\,z}\rangle)

Proof. By integral_specMeasure. $\square$

Used by specMeasure_engine, integral_specMeasure_polarization.

Lemma 734 (specMeasure_engine). source ↗

Off-diagonal engine (integral form): for continuous g, h and any vectors x, v, (∫h dμ_{g(T)x+v} − ∫h dμ_{g(T)x−v}) = (∫(h·g) dμ_{x+v} − ∫(h·g) dμ_{x−v}). Both sides equal 4·re⟪x, (h·g)(T) v⟫ (polarization + inner_cfcHom_mul).

\int (\omega : (\mathrm{sp}\,\mathbb{R}\,T)), h\,\omega \partial \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(((\mathrm{cfcHom}\,\mathrm{ha})\,g)\,x + v) - \int (\omega : (\mathrm{sp}\,\mathbb{R}\,T)), h\,\omega \partial \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(((\mathrm{cfcHom}\,\mathrm{ha})\,g)\,x - v) = \int (\omega : (\mathrm{sp}\,\mathbb{R}\,T)), (h \cdot g)\,\omega \partial \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(x + v) - \int (\omega : (\mathrm{sp}\,\mathbb{R}\,T)), (h \cdot g)\,\omega \partial \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(x - v)

Proof. By inner_cfcHom_mul, integral_specMeasure_cont. $\square$

Used by specMeasure_engine_measure.

Lemma 735 (specMeasure_engine_measure). source ↗

Engine, measure form (g ≥ 0): μ_{g(T)x+v} + (μ_{x−v}·g) = μ_{g(T)x−v} + (μ_{x+v}·g), where ·g is withDensity (ENNReal.ofReal ∘ g). Lifts specMeasure_engine to a measure identity by Riesz–Markov uniqueness.

(\forall (\omega : (\mathrm{sp}\,\mathbb{R}\,T)), 0 \le g\,\omega) \to \forall (x v : H), (\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(((\mathrm{cfcHom}\,\mathrm{ha})\,g)\,x + v) + (\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(x - v)).\mathrm{wd}\,\lambda \omega \mapsto {{g\,\omega}}) = \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(((\mathrm{cfcHom}\,\mathrm{ha})\,g)\,x - v) + (\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(x + v)).\mathrm{wd}\,\lambda \omega \mapsto {{g\,\omega}}

Proof. By instIsFiniteMeasureElemRealSpectrumContinuousLinearMapComplexIdSpecMeasure, specMeasure_engine. $\square$

Used by specMeasure_setEngine_nonneg.

Lemma 736 (withDensity_real_setIntegral). source ↗

withDensity-to-setIntegral bridge: ((μ_z)·g).real s = ∫_s g dμ_z for g ≥ 0.

(\forall (\omega : (\mathrm{sp}\,\mathbb{R}\,T)), 0 \le g\,\omega) \to \forall (z : H) \{s : \mathrm{Set}\,(\mathrm{sp}\,\mathbb{R}\,T)\}, \mathrm{MeasurableSet}\,s \to ((\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,z).\mathrm{wd}\,\lambda \omega \mapsto {{g\,\omega}}).\mathrm{real}\,s = \int (\omega : (\mathrm{sp}\,\mathbb{R}\,T)) in s, g\,\omega \partial \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,z

Proof. Immediate from the definitions. $\square$

Used by specMeasure_setEngine_nonneg.

Lemma 737 (specMeasure_setEngine_nonneg). source ↗

Set-level engine for g ≥ 0: q_s(g(T)x+v) − q_s(g(T)x−v) = ∫_s g dμ_{x+v} − ∫_s g dμ_{x−v} (the .real-at-s evaluation of specMeasure_engine_measure).

(\forall (\omega : (\mathrm{sp}\,\mathbb{R}\,T)), 0 \le g\,\omega) \to \forall (x v : H) \{s : \mathrm{Set}\,(\mathrm{sp}\,\mathbb{R}\,T)\}, \mathrm{MeasurableSet}\,s \to (\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(((\mathrm{cfcHom}\,\mathrm{ha})\,g)\,x + v)).\mathrm{real}\,s - (\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(((\mathrm{cfcHom}\,\mathrm{ha})\,g)\,x - v)).\mathrm{real}\,s = \int (\omega : (\mathrm{sp}\,\mathbb{R}\,T)) in s, g\,\omega \partial \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(x + v) - \int (\omega : (\mathrm{sp}\,\mathbb{R}\,T)) in s, g\,\omega \partial \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(x - v)

Proof. By instIsFiniteMeasureElemRealSpectrumContinuousLinearMapComplexIdSpecMeasure, specMeasure_engine_measure, withDensity_real_setIntegral. $\square$

Used by specMeasure_setEngine.

Lemma 738 (bForm_sub_left). source ↗

b_s is subtractive in its left argument.

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,(u - w)\,v = \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,u\,v - \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,w\,v

Proof. By bForm_comm, bForm_sub_right. $\square$

Used by specMeasure_setEngine.

Lemma 739 (specMeasure_setEngine). source ↗

Set-level engine (general continuous g): q_s(g(T)x+v) − q_s(g(T)x−v) = ∫_s g dμ_{x+v} − ∫_s g dμ_{x−v}. Both sides are linear in g; extend the g≥0 case by g = (g+‖g‖) − ‖g‖.

\mathrm{MeasurableSet}\,s \to (\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(((\mathrm{cfcHom}\,\mathrm{ha})\,g)\,x + v)).\mathrm{real}\,s - (\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(((\mathrm{cfcHom}\,\mathrm{ha})\,g)\,x - v)).\mathrm{real}\,s = \int (\omega : (\mathrm{sp}\,\mathbb{R}\,T)) in s, g\,\omega \partial \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(x + v) - \int (\omega : (\mathrm{sp}\,\mathbb{R}\,T)) in s, g\,\omega \partial \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(x - v)

Proof. By instIsFiniteMeasureElemRealSpectrumContinuousLinearMapComplexIdSpecMeasure, qForm, bForm, specMeasure_setEngine_nonneg, bForm_sub_left. $\square$

Used by specProj_engine_measure.

Lemma 740 (re_inner_cfcHom_specProj). source ↗

Diagonal–E(s) identity: re ⟪x, h(T)(E(s)v)⟫ = b_s(h(T)x, v) for continuous h. (Move h(T) and E(s) across by self-adjointness; the imaginary part of c_s drops under re.)

\mathrm{re}\,(\langle {x},{((\mathrm{cfcHom}\,\mathrm{ha})\,h)\,((\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specproj}{E}\,T\,\mathrm{ha}\,s)\,v)}\rangle) = \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,s\,(((\mathrm{cfcHom}\,\mathrm{ha})\,h)\,x)\,v

Proof. By cForm, inner_specProj, specProj_isSelfAdjoint. $\square$

Used by specProj_engine_measure.

Lemma 741 (integral_specMeasure_polarization). source ↗

Polarization at the scalar-measure level: ∫f dμ_{w+u} − ∫f dμ_{w−u} = 4·re⟪w, f(T)u⟫.

\int (\omega : (\mathrm{sp}\,\mathbb{R}\,T)), f\,\omega \partial \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(w + u) - \int (\omega : (\mathrm{sp}\,\mathbb{R}\,T)), f\,\omega \partial \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(w - u) = 4 \cdot \mathrm{re}\,(\langle {w},{((\mathrm{cfcHom}\,\mathrm{ha})\,f)\,u}\rangle)

Proof. By integral_specMeasure_cont. $\square$

Used by specProj_engine_measure.

Lemma 742 (specProj_engine_measure). source ↗

Final measure identity: μ_{x+E(s)v} + (μ_{x−v})↾s = μ_{x−E(s)v} + (μ_{x+v})↾s. Proved by Riesz–Markov uniqueness: the test against continuous f reduces, via the polarization + re_inner_cfcHom_specProj + specMeasure_setEngine, to an identity that holds.

\mathrm{MeasurableSet}\,s \to \forall (x v : H), \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(x + (\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specproj}{E}\,T\,\mathrm{ha}\,s)\,v) + (\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(x - v)).\mathrm{restr}\,s = \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(x - (\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specproj}{E}\,T\,\mathrm{ha}\,s)\,v) + (\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,(x + v)).\mathrm{restr}\,s

Proof. By instIsFiniteMeasureElemRealSpectrumContinuousLinearMapComplexIdSpecMeasure, qForm, bForm, specMeasure_setEngine, re_inner_cfcHom_specProj, integral_specMeasure_polarization. $\square$

Used by bForm_specProj.

Lemma 743 (bForm_specProj). source ↗

The intersection identity at the form level: b_t(x, E(s)v) = b_{s∩t}(x, v) (evaluate specProj_engine_measure at t via .real).

\mathrm{MeasurableSet}\,s \to \mathrm{MeasurableSet}\,t \to \forall (x v : H), \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,t\,x\,((\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specproj}{E}\,T\,\mathrm{ha}\,s)\,v) = \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-bform}{b}\,T\,\mathrm{ha}\,(s \cap t)\,x\,v

Proof. By specMeasure, instIsFiniteMeasureElemRealSpectrumContinuousLinearMapComplexIdSpecMeasure, qForm, specProj_engine_measure. $\square$

Used by specProj_inter.

Lemma 744 (specProj_inter). source ↗

E_inter: E(s∩t) = E(s)·E(t) — the projection / multiplicativity property, the final ProjectionValuedMeasure field. E(s)·E(t) tested against ⟪·x,y⟫ is c_t(x,E(s)y), which equals c_{s∩t}(x,y) by bForm_specProj (using E(s) ℂ-linear for the imaginary part).

\mathrm{MeasurableSet}\,s \to \mathrm{MeasurableSet}\,t \to \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specproj}{E}\,T\,\mathrm{ha}\,(s \cap t) = \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specproj}{E}\,T\,\mathrm{ha}\,s \cdot \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specproj}{E}\,T\,\mathrm{ha}\,t

Proof. By bForm, cForm, inner_specProj, specProj_isSelfAdjoint, bForm_specProj. $\square$

Used by PVM_of_selfAdjoint, scalarMeasure_eq_specMeasure.

Definition 745 (PVM_of_selfAdjoint). source ↗

The bounded spectral theorem (PVM form): every bounded self-adjoint T : H →L[ℂ] H induces a projection-valued measure on spectrum ℝ T, with E(s) = specProj. All structure fields are the lemmas proved above; isIdem is E_inter at s = t.

\mathrm{PVM\_of\_selfAdjoint}\,H\,T \;:=\; \{E :=\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specproj}{E}\,T\,\mathrm{ha} , \mathrm{isSA} :=\cdots , \mathrm{isIdem} :=\cdots , \mathrm{E\_empty} :=\cdots , \mathrm{E\_univ} :=\cdots , \mathrm{E\_inter} :=\cdots , \mathrm{hasSum\_iUnion} :=\cdots \}

Used by rvdSpecMeasure, deviceOpC_norm_le, borelFC_inner_self, rvdSpec_borelFC_diag, rvdSpecMeasure_zero_levelSet, rvdSpecMeasure_two_levelSet, tendsto_integral_devChar_remainder_sq, tendsto_integral_devChar_diff_sq, and 17 more.

Lemma 746 (re_inner_T_eq_integral). source ↗

Spectral representation of T (diagonal form): ∫_{σ(T)} λ dμ_x(λ) = re ⟪x, T x⟫. Since μ_x is the scalar spectral measure of the PVM_of_selfAdjoint (μ_x(s) = ⟪E(s)x,x⟫), this is the statement T = ∫ λ dE(λ) tested on the diagonal — T recovered from its PVM.

\int (\omega : (\mathrm{sp}\,\mathbb{R}\,T)), \omega \partial \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-specmeasure}{\mu_{\mathrm{sp}}}\,T\,\mathrm{ha}\,x = \mathrm{re}\,(\langle {x},{T\,x}\rangle)

Proof. By integral_specMeasure. $\square$

Used by diagInt_specCoord.

Definition 747 (borelFC). source ↗

The bounded Borel functional calculus of a bounded self-adjoint T: f(T) for bounded measurable f : σ(T) → ℂ.

\Phi_{B}\,H\,T\,f\,C \;:=\; (\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-pvm-of-selfadjoint}{\mathrm{PVM\_of\_selfAdjoint}}\,T\,\mathrm{ha}).\Phi\,\mathrm{hf}\,\mathrm{hC0}\,\mathrm{hC}

Used by borelFC_congr_ae, deviceOpC_neg_half_eq, deviceOpReal, deviceOpC, deviceOpC_norm_le, deviceOpReal_zero, deviceOpReal_eq, borelFC_inner_self, and 36 more.

Lemma 748 (inner_borelFC). source ↗

Defining property: ⟪x, f(T) y⟫ = B_f(x,y) (the polarized scalar-measure form).

\langle {x},{(\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-borelfc}{\Phi_{B}}\,T\,\mathrm{ha}\,\mathrm{hf}\,\mathrm{hC0}\,\mathrm{hC})\,y}\rangle = (\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-pvm-of-selfadjoint}{\mathrm{PVM\_of\_selfAdjoint}}\,T\,\mathrm{ha}).\mathrm{bd}\,f\,x\,y

Proof. By inner_boundedFC. $\square$

Used by borelFC_inner_self, rvdSpec_borelFC_diag, borelFC_adjoint, rvdRC_eq_borelFC.

Lemma 749 (borelFC_mul). source ↗

Multiplicativity of the bounded Borel FC: (f·g)(T) = f(T)·g(T).

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-borelfc}{\Phi_{B}}\,T\,\mathrm{ha}\,\mathrm{hfp}\,\mathrm{hC0p}\,\mathrm{hCp} = \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-borelfc}{\Phi_{B}}\,T\,\mathrm{ha}\,\mathrm{hf}\,\mathrm{hC0f}\,\mathrm{hCf} \cdot \href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-borelfc}{\Phi_{B}}\,T\,\mathrm{ha}\,\mathrm{hg}\,\mathrm{hC0g}\,\mathrm{hCg}

Proof. By boundedFC_mul, PVM_of_selfAdjoint. $\square$

Used by deviceOpReal_eq, borelFC_inner_self, deviceOpC_bottomEdge_eq, modUnitary_add, borelFC_comm, cfcCont_mul, cfcΩ_hΩ, rvdRC_mul_E_levelSet.

Lemma 750 (borelFC_one). source ↗

The bounded Borel FC is unital: (fun _ => 1)(T) = 1.

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-borelfc}{\Phi_{B}}\,T\,\mathrm{ha}\,\cdots \,\cdots \,\cdots = 1

Proof. By boundedFC, boundedFC_const, PVM_of_selfAdjoint. $\square$

Used by modUnitary_zero, cfcCont_one.

Lemma 751 (borelFC_const). source ↗

Constant rule (fun _ => c)(T) = c·1 — the QIQTH-layer wrapper of boundedFC_const.

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-borelfc}{\Phi_{B}}\,T\,\mathrm{ha}\,\cdots \,\cdots \,\cdots = c \cdot 1

Proof. By boundedFC_const, PVM_of_selfAdjoint. $\square$

Used by rvdRC_mul_E_levelSet.

Lemma 752 (borelFC_indicator). source ↗

Indicator rule 𝟙_s(T) = E s — the QIQTH-layer wrapper of boundedFC_indicator: the bounded Borel FC of a level-set indicator is the corresponding spectral projection of the PVM.

\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-borelfc}{\Phi_{B}}\,T\,\mathrm{ha}\,\cdots \,\cdots \,\cdots = (\href{/browser/qiqth-spectral-spectraltheorem#d-qiqth-spectraltheorem-pvm-of-selfadjoint}{\mathrm{PVM\_of\_selfAdjoint}}\,T\,\mathrm{ha}).E\,s

Proof. By boundedFC_indicator. $\square$

Used by rvdRC_mul_E_levelSet.

← all sections · ← PVM · StandardSubspaceModular →