Spectral · section of the QIQT-H book

QIQTH.Spectral.PVM

← all sections · ← RicciSymm · SpectralTheorem →

Spectral · entries 586–669 of 1000

Lemma 586 (ProjectionValuedMeasure).  source ↗

A projection-valued measure on a measurable space Ω acting on H: laws on measurable sets, with strong-operator countable additivity. This is the corrected primitive (cf. PVContent): on it the scalar measures μ_x are genuine finite measures and the Phase-1 analytic targets are sound.

hasSum_iUnion states σ-additivity vectorwise/strongly — HasSum in H, not in H →L[ℂ] H (operator-norm σ-additivity is false).

(Ω:Typeu_3)→(H:Typeu_4)→[MeasurableSpace Ω]→[inst:NormedAddCommGroup H]→[InnerProductSpace C H]→[CompleteSpace H]→Type(maxu_3u_4)(\Omega : Type\mathrm{u\_3}) \to (H : Type\mathrm{u\_4}) \to [\mathrm{MeasurableSpace}\,\Omega] \to [\mathrm{inst} : \mathrm{NormedAddCommGroup}\,H] \to [\mathrm{InnerProductSpace}\,\mathbb{C}\,H] \to [\mathrm{CompleteSpace}\,H] \to Type(max\mathrm{u\_3} \mathrm{u\_4})

Proof. Immediate from the definitions. □\square

Used by mk, E, isSA, isIdem, E_univ, E_inter, adjoint_eq, E_apply_idem, and 70 more.

Lemma 587 (mk).  source ↗

{Ω:Typeu_3}→{H:Typeu_4}→[inst:MeasurableSpace Ω]→[inst_1:NormedAddCommGroup H]→[inst_2:InnerProductSpace C H]→[inst_3:CompleteSpace H]→(E:Set Ω→H→L[C]H)→(∀s:Set Ω,MeasurableSet s→IsSelfAdjoint (E s))→(∀s:Set Ω,MeasurableSet s→IsIdempotentElem (E s))→E ∅=0→E=1→(∀st:Set Ω,MeasurableSet s→MeasurableSet t→E (s∩t)=E s⋅E t)→(∀{A:N→Set Ω},(∀(n:N),MeasurableSet (A n))→(Pairwise λmn↦Disjoint (A m) (A n))→∀(x:H),HasSum (λn↦(E (A n)) x) ((E (⋃n,A n)) x))→ProjectionValuedMeasure Ω H\{\Omega : Type\mathrm{u\_3}\} \to \{H : Type\mathrm{u\_4}\} \to [\mathrm{inst} : \mathrm{MeasurableSpace}\,\Omega] \to [\mathrm{inst\_1} : \mathrm{NormedAddCommGroup}\,H] \to [\mathrm{inst\_2} : \mathrm{InnerProductSpace}\,\mathbb{C}\,H] \to [\mathrm{inst\_3} : \mathrm{CompleteSpace}\,H] \to (E : \mathrm{Set}\,\Omega \to H \to L[\mathbb{C}] H) \to (\forall s : \mathrm{Set}\,\Omega, \mathrm{MeasurableSet}\,s \to \mathrm{IsSelfAdjoint}\,(E\,s)) \to (\forall s : \mathrm{Set}\,\Omega, \mathrm{MeasurableSet}\,s \to \mathrm{IsIdempotentElem}\,(E\,s)) \to E\,\emptyset = 0 \to E = 1 \to (\forall s t : \mathrm{Set}\,\Omega, \mathrm{MeasurableSet}\,s \to \mathrm{MeasurableSet}\,t \to E\,(s \cap t) = E\,s \cdot E\,t) \to (\forall \{A : \mathbb{N} \to \mathrm{Set}\,\Omega\}, (\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 (E\,(A\,n))\,x)\,((E\,(\bigcup n, A\,n))\,x)) \to \href{/browser/qiqth-spectral-pvm#d-qiqth-spectral-projectionvaluedmeasure}{\mathrm{ProjectionValuedMeasure}}\,\Omega\,H

Proof. Immediate from the definitions. □\square

Used by PVM_of_selfAdjoint.

Definition 588 (E).  source ↗

E Ω H self  :=  self.1E\,\Omega\,H\,\mathrm{self} \;:=\; \mathrm{self}.1

Used by rvdSpecMeasure_zero_levelSet, rvdSpecMeasure_two_levelSet, isSA, isIdem, E_univ, E_inter, adjoint_eq, E_apply_idem, and 21 more.

Lemma 589 (isSA).  source ↗

MeasurableSet s→IsSelfAdjoint (self.E s)\mathrm{MeasurableSet}\,s \to \mathrm{IsSelfAdjoint}\,(\mathrm{self}.E\,s)

Proof. Immediate from the definitions. □\square

Used by adjoint_eq.

Lemma 590 (isIdem).  source ↗

MeasurableSet s→IsIdempotentElem (self.E s)\mathrm{MeasurableSet}\,s \to \mathrm{IsIdempotentElem}\,(\mathrm{self}.E\,s)

Proof. Immediate from the definitions. □\square

Used by E_apply_idem.

Lemma 591 (E_univ).  source ↗

self.E=1\mathrm{self}.E = 1

Proof. Immediate from the definitions. □\square

Used by scalarMeasure_univ.

Lemma 592 (E_inter).  source ↗

MeasurableSet s→MeasurableSet t→self.E (s∩t)=self.E s⋅self.E t\mathrm{MeasurableSet}\,s \to \mathrm{MeasurableSet}\,t \to \mathrm{self}.E\,(s \cap t) = \mathrm{self}.E\,s \cdot \mathrm{self}.E\,t

Proof. Immediate from the definitions. □\square

Used by integralSimple_mul_eq.

Lemma 593 (adjoint_eq).  source ↗

MeasurableSet s→P.E s†=P.E s\mathrm{MeasurableSet}\,s \to {{P.E\,s}}^{\dagger} = P.E\,s

Proof. By isSA. □\square

Used by inner_E_self.

Lemma 594 (E_apply_idem).  source ↗

MeasurableSet s→∀(x:H),(P.E s) ((P.E s) x)=(P.E s) x\mathrm{MeasurableSet}\,s \to \forall (x : H), (P.E\,s)\,((P.E\,s)\,x) = (P.E\,s)\,x

Proof. By isIdem. □\square

Used by inner_E_self.

Lemma 595 (inner_E_self).  source ↗

⟪x, E s x⟫ = ‖E s x‖² for measurable s.

MeasurableSet s→∀(x:H),⟨x,(P.E s) x⟩=∥(P.E s) x∥2\mathrm{MeasurableSet}\,s \to \forall (x : H), \langle {x},{(P.E\,s)\,x}\rangle = {\|(P.E\,s)\,x\|}^{2}

Proof. By adjoint_eq, E_apply_idem. □\square

Used by diagInt_indicator_eq_inner.

Definition 596 (scalarMeasure).  source ↗

The scalar spectral measure μ_x — now a genuine MeasureTheory.Measure Ω (this is Phase-1 target T1, PROVED): the strong- operator σ-additivity of E (hasSum_iUnion) pushed through the bounded linear functional ⟪x,·⟫ gives σ-additivity of s ↦ ‖E s x‖².

Used by rvdSpecMeasure, borelFC_inner_self, rvdSpec_borelFC_diag, rvdSpecMeasure_zero_levelSet, rvdSpecMeasure_two_levelSet, tendsto_integral_devChar_remainder_sq, tendsto_integral_devChar_diff_sq, scalarMeasure_apply, and 23 more.

Lemma 597 (scalarMeasure_apply).  source ↗

Value of the scalar spectral measure on a measurable set.

MeasurableSet s→(P.μ x) s=∥(P.E s) x∥2\mathrm{MeasurableSet}\,s \to (P.\mu\,x)\,s = {{{\|(P.E\,s)\,x\|}^{2}}}

Proof. Immediate from the definitions. □\square

Used by rvdSpecMeasure_zero_levelSet, rvdSpecMeasure_two_levelSet, scalarMeasure_univ, scalarMeasure_toReal, scalarMeasure_smul, scalarMeasure_parallelogram_measure, scalarMeasure_odd_measure, scalarMeasure_eq_specMeasure.

Lemma 598 (scalarMeasure_univ).  source ↗

Total mass ‖x‖² — μ_x is a finite measure summing the resolution of identity.

(P.μ x)=∥x∥2(P.\mu\,x) = {{{\|x\|}^{2}}}

Proof. By E, E_univ, scalarMeasure_apply. □\square

Used by instIsFiniteMeasure_scalarMeasure, diagInt_norm_le, diagInt_const.

Definition 599 (integralSimple).  source ↗

Spectral integral of a simple function on the genuine PVM: ∫(∑ᵢ cᵢ 𝟙_{sᵢ}) dE = ∑ᵢ cᵢ E sᵢ.

∫ Ω H P ι t c sets  :=  ∑itc i⋅P.E (sets i)\textstyle\int\,\Omega\,H\,P\,\iota\,t\,c\,\mathrm{sets} \;:=\; \sum_{i t} c\,i \cdot P.E\,(\mathrm{sets}\,i)

Used by inner_integralSimple_left, boundedFC_eq_integralSimple, integralSimple_mul_eq, integralSimple_product_eq, boundedFC_simple_mul, boundedFC_simpleFunc, boundedFC_simpleFunc_mul.

Lemma 600 (inner_integralSimple_left).  source ↗

Sesquilinear form of the simple integral (pure linearity, no measurability needed): ⟪x, (∫f dE) y⟫ = ∑ᵢ cᵢ ⟪x, E sᵢ y⟫. This is the bilinear datum whose diagonal is ∫ f dμ_x and whose polarization gives the complex measures μ_{x,y}.

⟨x,(P.∫ t c sets) y⟩=∑itc i⋅⟨x,(P.E (sets i)) y⟩\langle {x},{(P.\textstyle\int\,t\,c\,\mathrm{sets})\,y}\rangle = \sum_{i t} c\,i \cdot \langle {x},{(P.E\,(\mathrm{sets}\,i))\,y}\rangle

Proof. Immediate from the definitions. □\square

Used by boundedFC_eq_integralSimple.

Lemma 601 (scalarMeasure_toReal).  source ↗

The real value of μ_x on a measurable set: (μ_x s).toReal = ‖E s x‖².

MeasurableSet s→((P.μ x) s).toReal=∥(P.E s) x∥2\mathrm{MeasurableSet}\,s \to ((P.\mu\,x)\,s).\mathrm{toReal} = {\|(P.E\,s)\,x\|}^{2}

Proof. By scalarMeasure_apply. □\square

Used by diagInt_indicator_eq_inner.

Lemma 602 (instIsFiniteMeasure_scalarMeasure).  source ↗

μ_x is a finite measure (total mass ‖x‖²) — so every bounded measurable function is Bochner-integrable against it. Prerequisite for the integral functional f ↦ ∫ f dμ_x of the bounded-Borel FC.

IsFiniteMeasure (P.μ x)\mathrm{IsFiniteMeasure}\,(P.\mu\,x)

Proof. By scalarMeasure_univ. □\square

Used by tendsto_integral_devChar_remainder_sq, tendsto_integral_devChar_diff_sq, integrable_boundedMeasurable, diagInt_norm_le, tendsto_diagInt_of_dominated.

Lemma 603 (scalarMeasure_smul).  source ↗

Scaling at the measure level: μ_{c·x} = ‖c‖² · μ_x. (E s (c•x) = c•E s x so ‖E s (c•x)‖² = ‖c‖²‖E s x‖².)

P.μ (c⋅x)=∥c∥2⋅P.μ xP.\mu\,(c \cdot x) = {{{\|c\|}^{2}}} \cdot P.\mu\,x

Proof. By E, scalarMeasure_apply. □\square

Used by diagInt_smul.

Lemma 604 (scalarMeasure_parallelogram_measure).  source ↗

Parallelogram at the measure level: μ_{x+y} + μ_{x−y} = 2·μ_x + 2·μ_y.

P.μ (x+y)+P.μ (x−y)=2⋅P.μ x+2⋅P.μ yP.\mu\,(x + y) + P.\mu\,(x - y) = 2 \cdot P.\mu\,x + 2 \cdot P.\mu\,y

Proof. By E, scalarMeasure_apply. □\square

Used by diagInt_parallelogram.

Lemma 605 (integrable_boundedMeasurable).  source ↗

A bounded measurable function is Bochner-integrable against the finite measure μ_x.

Measurable f→∀{C:R},(∀(ω:Ω),∥f ω∥≤C)→∀(x:H),Integrable f (P.μ x)\mathrm{Measurable}\,f \to \forall \{C : \mathbb{R}\}, (\forall (\omega : \Omega), \|f\,\omega\| \le C) \to \forall (x : H), \mathrm{Integrable}\,f\,(P.\mu\,x)

Proof. By instIsFiniteMeasure_scalarMeasure. □\square

Used by diagInt_parallelogram, diagInt_odd, diagInt_norm_le, diagInt_add, boundedFC_eq_integralSimple.

Definition 606 (diagInt).  source ↗

The diagonal functional D_f(x) := ∫ f dμ_x (E2a of the bounded-Borel FC sub-plan). Its homogeneity D_f(c·x) = ‖c‖² D_f(x) and parallelogram law are what make the polarized form B_f(x,y) sesquilinear.

∫ Ω H P f x  :=  ∫(ω:Ω),f ω∂P.μ x\textstyle\int\,\Omega\,H\,P\,f\,x \;:=\; \int (\omega : \Omega), f\,\omega \partial P.\mu\,x

Used by borelFC_inner_self, rvdSpec_borelFC_diag, diagInt_smul, diagInt_parallelogram, bilinDiag, bilinDiag_add_left, diagInt_unit_smul, diagInt_neg, and 26 more.

Lemma 607 (diagInt_smul).  source ↗

Homogeneity of the diagonal functional: D_f(c·x) = ‖c‖² D_f(x).

P.∫ f (c⋅x)=(∥c∥2)⋅P.∫ f xP.\textstyle\int\,f\,(c \cdot x) = ({\|c\|}^{2}) \cdot P.\textstyle\int\,f\,x

Proof. By scalarMeasure, scalarMeasure_smul. □\square

Used by diagInt_unit_smul.

Lemma 608 (diagInt_parallelogram).  source ↗

Parallelogram law for the diagonal functional: D_f(x+y) + D_f(x−y) = 2 D_f(x) + 2 D_f(y).

Measurable f→∀{C:R},(∀(ω:Ω),∥f ω∥≤C)→∀(xy:H),P.∫ f (x+y)+P.∫ f (x−y)=2⋅P.∫ f x+2⋅P.∫ f y\mathrm{Measurable}\,f \to \forall \{C : \mathbb{R}\}, (\forall (\omega : \Omega), \|f\,\omega\| \le C) \to \forall (x y : H), P.\textstyle\int\,f\,(x + y) + P.\textstyle\int\,f\,(x - y) = 2 \cdot P.\textstyle\int\,f\,x + 2 \cdot P.\textstyle\int\,f\,y

Proof. By scalarMeasure, scalarMeasure_parallelogram_measure, integrable_boundedMeasurable. □\square

Used by bilinDiag_add_left.

Definition 609 (bilinDiag).  source ↗

E2b — the polarized sesquilinear form B_f(x,y), mirroring Mathlib’s Fréchet–von Neumann–Jordan inner_ but with the quadratic functional D_f = diagInt f in place of ‖·‖². Its diagonal is D_f and (once shown sesquilinear + bounded) it represents ∫ f dE via continuousLinearMapOfBilin.

bd Ω H P f x y  :=  4−1⋅(P.∫ f (x+y)−P.∫ f (x−y)+i⋅P.∫ f (i⋅x+y)−i⋅P.∫ f (i⋅x−y))\mathrm{bd}\,\Omega\,H\,P\,f\,x\,y \;:=\; {4}^{-1} \cdot (P.\textstyle\int\,f\,(x + y) - P.\textstyle\int\,f\,(x - y) + i \cdot P.\textstyle\int\,f\,(i \cdot x + y) - i \cdot P.\textstyle\int\,f\,(i \cdot x - y))

Used by borelFC_inner_self, rvdSpec_borelFC_diag, bilinDiag_add_left, bilinDiag_conj_symm, bilinDiag_add_right, bilinDiag_I_smul_left, bilinDiag_real_smul_left_nonneg, bilinDiag_zero_left, and 28 more.

Lemma 610 (bilinDiag_add_left).  source ↗

Additivity in the first slot of B_f — the Jordan–von Neumann core, ported from InnerProductSpace.OfNorm.add_left (no algebraMap casting needed since D_f is already ℂ-valued), using diagInt_parallelogram.

Measurable f→∀{C:R},(∀(ω:Ω),∥f ω∥≤C)→∀(xyz:H),P.bd f (x+y) z=P.bd f x z+P.bd f y z\mathrm{Measurable}\,f \to \forall \{C : \mathbb{R}\}, (\forall (\omega : \Omega), \|f\,\omega\| \le C) \to \forall (x y z : H), P.\mathrm{bd}\,f\,(x + y)\,z = P.\mathrm{bd}\,f\,x\,z + P.\mathrm{bd}\,f\,y\,z

Proof. By diagInt, diagInt_parallelogram. □\square

Used by bilinDiag_add_right, bilinDiag_neg_left, bilinDiag_smul_left, bilinDiagₗ.

Lemma 611 (diagInt_unit_smul).  source ↗

D_f is invariant under unit-modulus scaling: D_f(c·x) = D_f(x) when ‖c‖ = 1 (special case of diagInt_smul).

∥c∥=1→∀(x:H),P.∫ f (c⋅x)=P.∫ f x\|c\| = 1 \to \forall (x : H), P.\textstyle\int\,f\,(c \cdot x) = P.\textstyle\int\,f\,x

Proof. By diagInt_smul. □\square

Used by diagInt_neg, diagInt_I_left, diagInt_I_right.

Lemma 612 (diagInt_neg).  source ↗

D_f is even: D_f(-x) = D_f(x).

P.∫ f (−x)=P.∫ f xP.\textstyle\int\,f\,(-x) = P.\textstyle\int\,f\,x

Proof. By diagInt_unit_smul. □\square

Used by diagInt_I_left, bilinDiag_conj_symm, bilinDiag_I_smul_left, bilinDiag_zero_left.

Lemma 613 (diagInt_conj).  source ↗

Conjugation passes through D_f: conj (D_f x) = D_{f̄}(x) (the scalar measure μ_x is real, so conj ∫ f = ∫ conj f).

(starRingEnd C) (P.∫ f x)=P.∫ (λω↦(starRingEnd C) (f ω)) x(\mathrm{starRingEnd}\,\mathbb{C})\,(P.\textstyle\int\,f\,x) = P.\textstyle\int\,(\lambda \omega \mapsto (\mathrm{starRingEnd}\,\mathbb{C})\,(f\,\omega))\,x

Proof. By scalarMeasure. □\square

Used by bilinDiag_conj_symm.

Lemma 614 (diagInt_I_left).  source ↗

D_f(i·y + x) = D_f(i·x − y) (unit-scaling invariance + evenness; used to establish the conjugate-symmetry of B_f).

P.∫ f (i⋅y+x)=P.∫ f (i⋅x−y)P.\textstyle\int\,f\,(i \cdot y + x) = P.\textstyle\int\,f\,(i \cdot x - y)

Proof. By diagInt_unit_smul, diagInt_neg. □\square

Used by bilinDiag_conj_symm.

Lemma 615 (diagInt_I_right).  source ↗

D_f(i·y − x) = D_f(i·x + y) (companion of diagInt_I_left).

P.∫ f (i⋅y−x)=P.∫ f (i⋅x+y)P.\textstyle\int\,f\,(i \cdot y - x) = P.\textstyle\int\,f\,(i \cdot x + y)

Proof. By diagInt_unit_smul. □\square

Used by bilinDiag_conj_symm.

Lemma 616 (bilinDiag_conj_symm).  source ↗

Conjugate-symmetry of the polarized form for complex f: conj (B_f(y,x)) = B_{f̄}(x,y) where f̄ = conj ∘ f. (For real f this is the usual ⟪x,y⟫ = conj⟪y,x⟫.) This transfers slot-1 additivity to slot 2.

(starRingEnd C) (P.bd f y x)=P.bd (λω↦(starRingEnd C) (f ω)) x y(\mathrm{starRingEnd}\,\mathbb{C})\,(P.\mathrm{bd}\,f\,y\,x) = P.\mathrm{bd}\,(\lambda \omega \mapsto (\mathrm{starRingEnd}\,\mathbb{C})\,(f\,\omega))\,x\,y

Proof. By diagInt, diagInt_neg, diagInt_conj, diagInt_I_left, diagInt_I_right. □\square

Used by bilinDiag_add_right, bilinDiag_smul_right, borelFC_adjoint.

Lemma 617 (bilinDiag_add_right).  source ↗

Additivity in the second slot of B_f, from slot-1 additivity (of f̄) through bilinDiag_conj_symm.

Measurable f→∀{C:R},(∀(ω:Ω),∥f ω∥≤C)→∀(xyz:H),P.bd f x (y+z)=P.bd f x y+P.bd f x z\mathrm{Measurable}\,f \to \forall \{C : \mathbb{R}\}, (\forall (\omega : \Omega), \|f\,\omega\| \le C) \to \forall (x y z : H), P.\mathrm{bd}\,f\,x\,(y + z) = P.\mathrm{bd}\,f\,x\,y + P.\mathrm{bd}\,f\,x\,z

Proof. By bilinDiag_add_left, bilinDiag_conj_symm. □\square

Used by bilinDiagₗ.

Lemma 618 (bilinDiag_I_smul_left).  source ↗

i-scaling in the first slot (the I_prop of Jordan–von Neumann, pure algebra via i² = −1 and evenness of D_f): B_f(i·x, y) = conj(i)·B_f(x,y).

P.bd f (i⋅x) y=(starRingEnd C) i⋅P.bd f x yP.\mathrm{bd}\,f\,(i \cdot x)\,y = (\mathrm{starRingEnd}\,\mathbb{C})\,i \cdot P.\mathrm{bd}\,f\,x\,y

Proof. By diagInt, diagInt_neg. □\square

Used by bilinDiag_smul_left.

Lemma 619 (scalarMeasure_odd_measure).  source ↗

Odd measure identity (the continuity-free key to real homogeneity): for r ≥ 0, μ_{r·x+y} + r·μ_{x−y} = μ_{r·x−y} + r·μ_{x+y} (both sides equal r²‖Ex‖² + ‖Ey‖² + r‖Ex‖² + r‖Ey‖² at each set; all positive measures, no signed-measure machinery).

0≤r→P.μ (r⋅x+y)+r⋅P.μ (x−y)=P.μ (r⋅x−y)+r⋅P.μ (x+y)0 \le r \to P.\mu\,(r \cdot x + y) + {{r}} \cdot P.\mu\,(x - y) = P.\mu\,(r \cdot x - y) + {{r}} \cdot P.\mu\,(x + y)

Proof. By E, scalarMeasure_apply. □\square

Used by diagInt_odd.

Lemma 620 (diagInt_odd).  source ↗

Odd functional identity: D_f(r·x+y) − D_f(r·x−y) = r(D_f(x+y) − D_f(x−y)) (here as D_f(r·x+y) + r·D_f(x−y) = D_f(r·x−y) + r·D_f(x+y)), r ≥ 0. Integrates scalarMeasure_odd_measure; the seed of real homogeneity of B_f.

Measurable f→∀{C:R},(∀(ω:Ω),∥f ω∥≤C)→∀(xy:H){r:R},0≤r→P.∫ f (r⋅x+y)+r⋅P.∫ f (x−y)=P.∫ f (r⋅x−y)+r⋅P.∫ f (x+y)\mathrm{Measurable}\,f \to \forall \{C : \mathbb{R}\}, (\forall (\omega : \Omega), \|f\,\omega\| \le C) \to \forall (x y : H) \{r : \mathbb{R}\}, 0 \le r \to P.\textstyle\int\,f\,(r \cdot x + y) + r \cdot P.\textstyle\int\,f\,(x - y) = P.\textstyle\int\,f\,(r \cdot x - y) + r \cdot P.\textstyle\int\,f\,(x + y)

Proof. By scalarMeasure, integrable_boundedMeasurable, scalarMeasure_odd_measure. □\square

Used by bilinDiag_real_smul_left_nonneg.

Lemma 621 (bilinDiag_real_smul_left_nonneg).  source ↗

Real homogeneity in the first slot, r ≥ 0: B_f(r·x, y) = r·B_f(x,y). Both the x and the i·x odd identities feed in; no continuity used.

Measurable f→∀{C:R},(∀(ω:Ω),∥f ω∥≤C)→∀(xy:H){r:R},0≤r→P.bd f (r⋅x) y=r⋅P.bd f x y\mathrm{Measurable}\,f \to \forall \{C : \mathbb{R}\}, (\forall (\omega : \Omega), \|f\,\omega\| \le C) \to \forall (x y : H) \{r : \mathbb{R}\}, 0 \le r \to P.\mathrm{bd}\,f\,(r \cdot x)\,y = r \cdot P.\mathrm{bd}\,f\,x\,y

Proof. By diagInt, diagInt_odd. □\square

Used by bilinDiag_real_smul_left.

Lemma 622 (bilinDiag_zero_left).  source ↗

B_f(0, y) = 0.

P.bd f 0 y=0P.\mathrm{bd}\,f\,0\,y = 0

Proof. By diagInt, diagInt_neg. □\square

Used by bilinDiag_neg_left, bilinDiag_norm_le.

Lemma 623 (bilinDiag_neg_left).  source ↗

B_f(-x, y) = -B_f(x, y) (from additivity in the first slot).

Measurable f→∀{C:R},(∀(ω:Ω),∥f ω∥≤C)→∀(xy:H),P.bd f (−x) y=−P.bd f x y\mathrm{Measurable}\,f \to \forall \{C : \mathbb{R}\}, (\forall (\omega : \Omega), \|f\,\omega\| \le C) \to \forall (x y : H), P.\mathrm{bd}\,f\,(-x)\,y = -P.\mathrm{bd}\,f\,x\,y

Proof. By bilinDiag_add_left, bilinDiag_zero_left. □\square

Used by bilinDiag_real_smul_left.

Lemma 624 (bilinDiag_real_smul_left).  source ↗

Real homogeneity in the first slot (all r : ℝ): B_f(r·x,y) = r·B_f(x,y).

Measurable f→∀{C:R},(∀(ω:Ω),∥f ω∥≤C)→∀(xy:H)(r:R),P.bd f (r⋅x) y=r⋅P.bd f x y\mathrm{Measurable}\,f \to \forall \{C : \mathbb{R}\}, (\forall (\omega : \Omega), \|f\,\omega\| \le C) \to \forall (x y : H) (r : \mathbb{R}), P.\mathrm{bd}\,f\,(r \cdot x)\,y = r \cdot P.\mathrm{bd}\,f\,x\,y

Proof. By bilinDiag_real_smul_left_nonneg, bilinDiag_neg_left. □\square

Used by bilinDiag_smul_left.

Lemma 625 (bilinDiag_smul_left).  source ↗

Conjugate-linearity in the first slot (full ℂ): B_f(c·x, y) = conj(c)·B_f(x,y) — combines real homogeneity, i-scaling and additivity via c = c.re + c.im·i. This is the sesquilinear half (with bilinDiag_conj_symm giving linearity in the second slot).

Measurable f→∀{C:R},(∀(ω:Ω),∥f ω∥≤C)→∀(c:C)(xy:H),P.bd f (c⋅x) y=(starRingEnd C) c⋅P.bd f x y\mathrm{Measurable}\,f \to \forall \{C : \mathbb{R}\}, (\forall (\omega : \Omega), \|f\,\omega\| \le C) \to \forall (c : \mathbb{C}) (x y : H), P.\mathrm{bd}\,f\,(c \cdot x)\,y = (\mathrm{starRingEnd}\,\mathbb{C})\,c \cdot P.\mathrm{bd}\,f\,x\,y

Proof. By bilinDiag_add_left, bilinDiag_I_smul_left, bilinDiag_real_smul_left. □\square

Used by bilinDiag_smul_right, bilinDiag_norm_le.

Lemma 626 (diagInt_norm_le).  source ↗

Diagonal bound ‖D_f x‖ ≤ C‖x‖² from ‖f‖ ≤ C and μ_x(univ) = ‖x‖².

Measurable f→∀{C:R},0≤C→(∀(ω:Ω),∥f ω∥≤C)→∀(x:H),∥P.∫ f x∥≤C⋅∥x∥2\mathrm{Measurable}\,f \to \forall \{C : \mathbb{R}\}, 0 \le C \to (\forall (\omega : \Omega), \|f\,\omega\| \le C) \to \forall (x : H), \|P.\textstyle\int\,f\,x\| \le C \cdot {\|x\|}^{2}

Proof. By scalarMeasure, scalarMeasure_univ, instIsFiniteMeasure_scalarMeasure, integrable_boundedMeasurable. □\square

Used by bilinDiag_norm_le_add.

Lemma 627 (bilinDiag_smul_right).  source ↗

Linearity in the second slot: B_f(x, c·y) = c·B_f(x,y) (from conjugate-symmetry + first-slot conjugate-linearity of f̄).

Measurable f→∀{C:R},(∀(ω:Ω),∥f ω∥≤C)→∀(c:C)(xy:H),P.bd f x (c⋅y)=c⋅P.bd f x y\mathrm{Measurable}\,f \to \forall \{C : \mathbb{R}\}, (\forall (\omega : \Omega), \|f\,\omega\| \le C) \to \forall (c : \mathbb{C}) (x y : H), P.\mathrm{bd}\,f\,x\,(c \cdot y) = c \cdot P.\mathrm{bd}\,f\,x\,y

Proof. By bilinDiag_conj_symm, bilinDiag_smul_left. □\square

Used by bilinDiag_norm_le.

Lemma 628 (bilinDiag_zero_right).  source ↗

B_f(x, 0) = 0.

P.bd f x 0=0P.\mathrm{bd}\,f\,x\,0 = 0

Proof. By diagInt. □\square

Used by bilinDiag_norm_le.

Lemma 629 (bilinDiag_norm_le_add).  source ↗

Quadratic bound ‖B_f(x,y)‖ ≤ C(‖x‖²+‖y‖²) (polarization + diagonal bound + two parallelogram laws).

Measurable f→∀{C:R},0≤C→(∀(ω:Ω),∥f ω∥≤C)→∀(xy:H),∥P.bd f x y∥≤C⋅(∥x∥2+∥y∥2)\mathrm{Measurable}\,f \to \forall \{C : \mathbb{R}\}, 0 \le C \to (\forall (\omega : \Omega), \|f\,\omega\| \le C) \to \forall (x y : H), \|P.\mathrm{bd}\,f\,x\,y\| \le C \cdot ({\|x\|}^{2} + {\|y\|}^{2})

Proof. By diagInt, diagInt_norm_le. □\square

Used by bilinDiag_norm_le.

Lemma 630 (bilinDiag_norm_le).  source ↗

Product (bilinear) bound ‖B_f(x,y)‖ ≤ 2C·‖x‖·‖y‖ — the bound feeding LinearMap.mkContinuous₂. Proof: normalize to unit vectors and apply the quadratic bound (giving ‖u‖²+‖v‖² = 2).

Measurable f→∀{C:R},0≤C→(∀(ω:Ω),∥f ω∥≤C)→∀(xy:H),∥P.bd f x y∥≤2⋅C⋅∥x∥⋅∥y∥\mathrm{Measurable}\,f \to \forall \{C : \mathbb{R}\}, 0 \le C \to (\forall (\omega : \Omega), \|f\,\omega\| \le C) \to \forall (x y : H), \|P.\mathrm{bd}\,f\,x\,y\| \le 2 \cdot C \cdot \|x\| \cdot \|y\|

Proof. By bilinDiag_zero_left, bilinDiag_smul_left, bilinDiag_smul_right, bilinDiag_zero_right, bilinDiag_norm_le_add. □\square

Used by intBorel, inner_intBorel, intBorel_norm_le.

Definition 631 (bilinDiagₗ).  source ↗

The polarized form as a bundled sesquilinear LinearMap H →ₗ⋆[ℂ] H →ₗ[ℂ] ℂ (conjugate-linear in the first slot, linear in the second), mirroring innerₛₗ.

bilinDiagl Ω H P f C  :=  mk′ (starRingEnd C) (id C) (λxy↦P.bd f x y) ⋯ ⋯ ⋯ ⋯\mathrm{bilinDiagₗ}\,\Omega\,H\,P\,f\,C \;:=\; \mathrm{mk'}\,(\mathrm{starRingEnd}\,\mathbb{C})\,(\mathrm{id}\,\mathbb{C})\,(\lambda x y \mapsto P.\mathrm{bd}\,f\,x\,y)\,\cdots \,\cdots \,\cdots \,\cdots

Used by intBorel, inner_intBorel.

Definition 632 (intBorel).  source ↗

The bounded-Borel functional calculus ∫ f dE (E2c), defined via the Riesz representation continuousLinearMapOfBilin of the bounded sesquilinear form B_f. Requires 0 ≤ C and ‖f‖ ≤ C.

∫ Ω H P f C  :=  continuousLinearMapOfBilin ((P.bdl hf hC).mkContinuous2 (2⋅C) ⋯ )\textstyle\int\,\Omega\,H\,P\,f\,C \;:=\; \mathrm{continuousLinearMapOfBilin}\,((P.\mathrm{bd}_{l}\,\mathrm{hf}\,\mathrm{hC}).\mathrm{mkContinuous}_{2}\,(2 \cdot C)\,\cdots )

Used by inner_intBorel, intBorel_norm_le, boundedFC, inner_boundedFC, boundedFC_norm_le.

Lemma 633 (inner_intBorel).  source ↗

Defining property of ∫ f dE: ⟪(∫f dE) x, y⟫ = B_f(x,y) — the sesquilinear form B_f(x,y) = ∫ f dμ_{x,y} is realized by the operator.

⟨(P.∫ hf hC0 hC) x,y⟩=P.bd f x y\langle {(P.\textstyle\int\,\mathrm{hf}\,\mathrm{hC0}\,\mathrm{hC})\,x},{y}\rangle = P.\mathrm{bd}\,f\,x\,y

Proof. By bilinDiag_norm_le, bilinDiagₗ. □\square

Used by intBorel_norm_le, inner_boundedFC.

Lemma 634 (intBorel_norm_le).  source ↗

Operator norm bound: ‖∫f dE‖ ≤ 2C. From ‖T x‖² = Re B_f(x, T x) ≤ ‖B_f(x, T x)‖ ≤ 2C‖x‖‖T x‖.

∥P.∫ hf hC0 hC∥≤2⋅C\|P.\textstyle\int\,\mathrm{hf}\,\mathrm{hC0}\,\mathrm{hC}\| \le 2 \cdot C

Proof. By bilinDiag, bilinDiag_norm_le, inner_intBorel. □\square

Used by boundedFC_norm_le.

Lemma 635 (diagInt_const).  source ↗

D_f of a CONSTANT function: ∫ c dμ_z = ‖z‖²·c.

P.∫ (λx↦c) z=∥z∥2⋅cP.\textstyle\int\,(\lambda x \mapsto c)\,z = {\|z\|}^{2} \cdot c

Proof. By scalarMeasure, scalarMeasure_univ. □\square

Used by bilinDiag_const.

Lemma 636 (bilinDiag_const).  source ↗

B_f of a CONSTANT function is c·⟪x,y⟫ (polarization of ‖·‖² = ⟪x,y⟫). Note this is conjugate-linear in x — confirming that the Riesz operator intBorel is the conjugated calculus (see intBorel_const).

P.bd (λx↦c) x y=c⋅⟨x,y⟩P.\mathrm{bd}\,(\lambda x \mapsto c)\,x\,y = c \cdot \langle {x},{y}\rangle

Proof. By diagInt, diagInt_const. □\square

Used by boundedFC_const.

Definition 637 (boundedFC).  source ↗

The correctly-oriented bounded-Borel functional calculus Φ(f) := (∫f dE)* (the adjoint of the Riesz operator), so that ⟪x, Φ(f) y⟫ = B_f(x,y) = ∫ f dμ_{x,y} with the operator on the SECOND slot — the standard convention.

Φ Ω H P f C  :=  P.∫ hf hC0 hC†\Phi\,\Omega\,H\,P\,f\,C \;:=\; {{P.\textstyle\int\,\mathrm{hf}\,\mathrm{hC0}\,\mathrm{hC}}}^{\dagger}

Used by deviceOpC_norm_le, inner_boundedFC, boundedFC_const, boundedFC_add, boundedFC_smul, boundedFC_norm_le, boundedFC_congr, boundedFC_indicator, and 9 more.

Lemma 638 (inner_boundedFC).  source ↗

Defining property of the oriented FC: ⟪x, Φ(f) y⟫ = B_f(x,y).

⟨x,(P.Φ hf hC0 hC) y⟩=P.bd f x y\langle {x},{(P.\Phi\,\mathrm{hf}\,\mathrm{hC0}\,\mathrm{hC})\,y}\rangle = P.\mathrm{bd}\,f\,x\,y

Proof. By intBorel, inner_intBorel. □\square

Used by boundedFC_const, boundedFC_add, boundedFC_smul, boundedFC_congr, boundedFC_indicator, boundedFC_eq_integralSimple, boundedFC_mul_simpleFunc_left, boundedFC_mul, and 1 more.

Lemma 639 (boundedFC_const).  source ↗

Unitality / constant rule: Φ(const c) = c·1. In particular Φ(1) = 1, so the oriented calculus is unital (a genuine functional calculus).

P.Φ ⋯ ⋯ ⋯=c⋅1P.\Phi\,\cdots \,\cdots \,\cdots = c \cdot 1

Proof. By bilinDiag, bilinDiag_const, inner_boundedFC. □\square

Used by borelFC_one, borelFC_const.

Lemma 640 (diagInt_add).  source ↗

Additivity of the diagonal functional in f: D_{f+g} = D_f + D_g.

Measurable f→Measurable g→∀{CfCg:R},(∀(ω:Ω),∥f ω∥≤Cf)→(∀(ω:Ω),∥g ω∥≤Cg)→∀(z:H),P.∫ (λω↦f ω+g ω) z=P.∫ f z+P.∫ g z\mathrm{Measurable}\,f \to \mathrm{Measurable}\,g \to \forall \{\mathrm{Cf} \mathrm{Cg} : \mathbb{R}\}, (\forall (\omega : \Omega), \|f\,\omega\| \le \mathrm{Cf}) \to (\forall (\omega : \Omega), \|g\,\omega\| \le \mathrm{Cg}) \to \forall (z : H), P.\textstyle\int\,(\lambda \omega \mapsto f\,\omega + g\,\omega)\,z = P.\textstyle\int\,f\,z + P.\textstyle\int\,g\,z

Proof. By scalarMeasure, integrable_boundedMeasurable. □\square

Used by bilinDiag_add_f.

Lemma 641 (diagInt_finsetSum).  source ↗

Linearity of the diagonal functional over finite sums: D_{∑ᵢ Fᵢ} = ∑ᵢ D_{Fᵢ} (each Fᵢ integrable against μ_z). Bound-free.

(∀i∈t,Integrable (F i) (P.μ z))→P.∫ (λω↦∑itF i ω) z=∑itP.∫ (F i) z(\forall i\in t, \mathrm{Integrable}\,(F\,i)\,(P.\mu\,z)) \to P.\textstyle\int\,(\lambda \omega \mapsto \sum_{i t} F\,i\,\omega)\,z = \sum_{i t} P.\textstyle\int\,(F\,i)\,z

Proof. Immediate from the definitions. □\square

Used by bilinDiag_finsetSum.

Lemma 642 (bilinDiag_add_f).  source ↗

Additivity of the polarized sesquilinear form in f: B_{f+g} = B_f + B_g.

Measurable f→Measurable g→∀{CfCg:R},(∀(ω:Ω),∥f ω∥≤Cf)→(∀(ω:Ω),∥g ω∥≤Cg)→∀(xy:H),P.bd (λω↦f ω+g ω) x y=P.bd f x y+P.bd g x y\mathrm{Measurable}\,f \to \mathrm{Measurable}\,g \to \forall \{\mathrm{Cf} \mathrm{Cg} : \mathbb{R}\}, (\forall (\omega : \Omega), \|f\,\omega\| \le \mathrm{Cf}) \to (\forall (\omega : \Omega), \|g\,\omega\| \le \mathrm{Cg}) \to \forall (x y : H), P.\mathrm{bd}\,(\lambda \omega \mapsto f\,\omega + g\,\omega)\,x\,y = P.\mathrm{bd}\,f\,x\,y + P.\mathrm{bd}\,g\,x\,y

Proof. By diagInt, diagInt_add. □\square

Used by boundedFC_add.

Lemma 643 (bilinDiag_finsetSum).  source ↗

Linearity of the polarized form over finite sums: B_{∑ᵢ Fᵢ} = ∑ᵢ B_{Fᵢ}.

(∀(z:H),∀i∈t,Integrable (F i) (P.μ z))→∀(xy:H),P.bd (λω↦∑itF i ω) x y=∑itP.bd (F i) x y(\forall (z : H), \forall i\in t, \mathrm{Integrable}\,(F\,i)\,(P.\mu\,z)) \to \forall (x y : H), P.\mathrm{bd}\,(\lambda \omega \mapsto \sum_{i t} F\,i\,\omega)\,x\,y = \sum_{i t} P.\mathrm{bd}\,(F\,i)\,x\,y

Proof. By diagInt, diagInt_finsetSum. □\square

Used by boundedFC_eq_integralSimple.

Lemma 644 (boundedFC_add).  source ↗

Additivity of the bounded-Borel FC in f: Φ(f+g) = Φ(f) + Φ(g).

P.Φ ⋯ ⋯ ⋯=P.Φ hf hCf0 hCf+P.Φ hg hCg0 hCgP.\Phi\,\cdots \,\cdots \,\cdots = P.\Phi\,\mathrm{hf}\,\mathrm{hCf0}\,\mathrm{hCf} + P.\Phi\,\mathrm{hg}\,\mathrm{hCg0}\,\mathrm{hCg}

Proof. By bilinDiag, inner_boundedFC, bilinDiag_add_f. □\square

Used by borelFC_add.

Lemma 645 (diagInt_smul_f).  source ↗

Scalar-homogeneity of the diagonal functional in f: D_{c·f} = c·D_f.

P.∫ (λω↦c⋅f ω) z=c⋅P.∫ f zP.\textstyle\int\,(\lambda \omega \mapsto c \cdot f\,\omega)\,z = c \cdot P.\textstyle\int\,f\,z

Proof. By scalarMeasure. □\square

Used by bilinDiag_smul_f.

Lemma 646 (bilinDiag_smul_f).  source ↗

Scalar-homogeneity of the polarized form in f: B_{c·f} = c·B_f.

P.bd (λω↦c⋅f ω) x y=c⋅P.bd f x yP.\mathrm{bd}\,(\lambda \omega \mapsto c \cdot f\,\omega)\,x\,y = c \cdot P.\mathrm{bd}\,f\,x\,y

Proof. By diagInt, diagInt_smul_f. □\square

Used by boundedFC_smul, boundedFC_eq_integralSimple.

Lemma 647 (boundedFC_smul).  source ↗

ℂ-homogeneity of the bounded-Borel FC in f: Φ(c·f) = c·Φ(f).

P.Φ ⋯ ⋯ ⋯=c⋅P.Φ hf hC0 hCP.\Phi\,\cdots \,\cdots \,\cdots = c \cdot P.\Phi\,\mathrm{hf}\,\mathrm{hC0}\,\mathrm{hC}

Proof. By bilinDiag, inner_boundedFC, bilinDiag_smul_f. □\square

Used by borelFC_smul.

Lemma 648 (boundedFC_norm_le).  source ↗

Operator-norm bound for the bounded-Borel FC: ‖Φ(f)‖ ≤ 2C for ‖f‖∞ ≤ C. (Φ(f) is the adjoint of the Riesz operator intBorel f, and the adjoint is a linear isometry.) This is the estimate that makes the simple→bounded-Borel extension converge in OPERATOR NORM — the route to multiplicativity Φ(fg)=Φ(f)Φ(g) that weak-operator convergence cannot deliver.

∥P.Φ hf hC0 hC∥≤2⋅C\|P.\Phi\,\mathrm{hf}\,\mathrm{hC0}\,\mathrm{hC}\| \le 2 \cdot C

Proof. By intBorel, intBorel_norm_le. □\square

Used by deviceOpC_norm_le, cfcCont_norm_le.

Lemma 649 (boundedFC_congr).  source ↗

Φ(f) depends only on f, not on the bound: equal functions give equal operators (the value is ⟪x,Φ(f)y⟫ = B_f(x,y), independent of the bound proof). Lets us rewrite f to any pointwise-equal form (e.g. reindex a product).

f=f′→P.Φ hf hCf0 hCf=P.Φ hf′ hCf0′ hCf′f = f^{\prime} \to P.\Phi\,\mathrm{hf}\,\mathrm{hCf0}\,\mathrm{hCf} = P.\Phi\,\mathrm{hf}^{\prime}\,\mathrm{hCf0}^{\prime}\,\mathrm{hCf}^{\prime}

Proof. By bilinDiag, inner_boundedFC. □\square

Used by boundedFC_simple_mul, boundedFC_simpleFunc, boundedFC_simpleFunc_mul, borelFC_congr.

Lemma 650 (norm_indicatorOne_le).  source ↗

The complex indicator 𝟙_s is bounded by 1.

∥s.1 (λx↦1) ω∥≤1\|s.\mathbf{1}\,(\lambda x \mapsto 1)\,\omega\| \le 1

Proof. Immediate from the definitions. □\square

Used by boundedFC_indicator, boundedFC_eq_integralSimple, boundedFC_simple_mul, boundedFC_simpleFunc, boundedFC_simpleFunc_mul, borelFC_indicator, rvdRC_mul_E_levelSet.

Lemma 651 (diagInt_indicator).  source ↗

D_{𝟙_s}(z) = μ_z(s) — the diagonal functional of an indicator is the scalar spectral mass.

MeasurableSet s→∀(z:H),P.∫ (s.1 λx↦1) z=((P.μ z) s).toReal\mathrm{MeasurableSet}\,s \to \forall (z : H), P.\textstyle\int\,(s.\mathbf{1}\,\lambda x \mapsto 1)\,z = ((P.\mu\,z)\,s).\mathrm{toReal}

Proof. Immediate from the definitions. □\square

Used by diagInt_indicator_eq_inner.

Lemma 652 (diagInt_indicator_eq_inner).  source ↗

D_{𝟙_s}(z) = ⟪z, E s z⟫ — the diagonal of the indicator’s form is the projection’s quadratic form.

MeasurableSet s→∀(z:H),P.∫ (s.1 λx↦1) z=⟨z,(P.E s) z⟩\mathrm{MeasurableSet}\,s \to \forall (z : H), P.\textstyle\int\,(s.\mathbf{1}\,\lambda x \mapsto 1)\,z = \langle {z},{(P.E\,s)\,z}\rangle

Proof. By inner_E_self, scalarMeasure, scalarMeasure_toReal, diagInt_indicator. □\square

Used by bilinDiag_indicator.

Lemma 653 (bilinDiag_indicator).  source ↗

Indicator bridge (polarized): the bounded-Borel sesquilinear form of an indicator is the spectral projection’s form, B_{𝟙_s}(x,y) = ⟪x, E s y⟫. Proved by reducing the four polarization points to ⟪z, E s z⟫ and expanding by sesquilinearity (the same Jordan–von Neumann computation as inner_E_polarization, with the I•x ± y convention of bilinDiag).

MeasurableSet s→∀(xy:H),P.bd (s.1 λx↦1) x y=⟨x,(P.E s) y⟩\mathrm{MeasurableSet}\,s \to \forall (x y : H), P.\mathrm{bd}\,(s.\mathbf{1}\,\lambda x \mapsto 1)\,x\,y = \langle {x},{(P.E\,s)\,y}\rangle

Proof. By diagInt, diagInt_indicator_eq_inner. □\square

Used by boundedFC_indicator, boundedFC_eq_integralSimple.

Lemma 654 (boundedFC_indicator).  source ↗

The bounded-Borel FC of an indicator is the spectral projection: Φ(𝟙_s) = E s. This anchors the abstract Borel functional calculus to the PVM it came from.

P.Φ ⋯ ⋯ ⋯=P.E sP.\Phi\,\cdots \,\cdots \,\cdots = P.E\,s

Proof. By bilinDiag, inner_boundedFC, bilinDiag_indicator. □\square

Used by borelFC_indicator.

Lemma 655 (boundedFC_eq_integralSimple).  source ↗

The bounded-Borel FC of a simple function is its spectral integral: Φ(∑ᵢ cᵢ 𝟙_{sᵢ}) = ∑ᵢ cᵢ E sᵢ = integralSimple. Proved at the sesquilinear-form level: B_{∑cᵢ𝟙_{sᵢ}} = ∑ cᵢ B_{𝟙_{sᵢ}} = ∑ cᵢ ⟪x, E sᵢ y⟫ (finset linearity + smul-in-f + the indicator bridge).

P.Φ ⋯ ⋯ ⋯=P.∫ t c setsP.\Phi\,\cdots \,\cdots \,\cdots = P.\textstyle\int\,t\,c\,\mathrm{sets}

Proof. By E, inner_integralSimple_left, integrable_boundedMeasurable, bilinDiag, inner_boundedFC, bilinDiag_finsetSum, bilinDiag_smul_f, bilinDiag_indicator. □\square

Used by boundedFC_simple_mul, boundedFC_simpleFunc.

Lemma 656 (integralSimple_mul_eq).  source ↗

Operator product of two simple integrals (the algebraic core of multiplicativity Φ(fg)=Φ(f)Φ(g) for simple f,g): cross terms collapse by E Aᵢ · E Bⱼ = E(Aᵢ ∩ Bⱼ).

(∀i∈t,MeasurableSet (A i))→(∀j∈s,MeasurableSet (B j))→P.∫ t a A⋅P.∫ s b B=∑it∑js(a i⋅b j)⋅P.E (A i∩B j)(\forall i\in t, \mathrm{MeasurableSet}\,(A\,i)) \to (\forall j\in s, \mathrm{MeasurableSet}\,(B\,j)) \to P.\textstyle\int\,t\,a\,A \cdot P.\textstyle\int\,s\,b\,B = \sum_{i t} \sum_{j s} (a\,i \cdot b\,j) \cdot P.E\,(A\,i \cap B\,j)

Proof. By E_inter. □\square

Used by integralSimple_product_eq.

Lemma 657 (integralSimple_product_eq).  source ↗

The simple integral over the product index t ×ˢ s (weights aᵢbⱼ, sets Aᵢ ∩ Bⱼ) equals the product of the two simple integrals. Pure operator algebra (integralSimple_mul_eq + Finset.sum_product).

(∀i∈t,MeasurableSet (A i))→(∀j∈s,MeasurableSet (B j))→(P.∫ (t×s) (λp↦a p.1⋅b p.2) λp↦A p.1∩B p.2)=P.∫ t a A⋅P.∫ s b B(\forall i\in t, \mathrm{MeasurableSet}\,(A\,i)) \to (\forall j\in s, \mathrm{MeasurableSet}\,(B\,j)) \to (P.\textstyle\int\,(t \times s)\,(\lambda p \mapsto a\,p.1 \cdot b\,p.2)\,\lambda p \mapsto A\,p.1 \cap B\,p.2) = P.\textstyle\int\,t\,a\,A \cdot P.\textstyle\int\,s\,b\,B

Proof. By E, integralSimple_mul_eq. □\square

Used by boundedFC_simple_mul.

Lemma 658 (boundedFC_simple_mul).  source ↗

Multiplicativity on simple functions: Φ(f·g) = Φ(f)·Φ(g) for simple f = ∑ᵢ aᵢ 𝟙_{Aᵢ}, g = ∑ⱼ bⱼ 𝟙_{Bⱼ}. Stated with Φ(f), Φ(g) as the simple integrals (= Φ(f), Φ(g) by boundedFC_eq_integralSimple). Proof: the product f·g reindexes pointwise to the t ×ˢ s simple function (boundedFC_congr + Finset.sum_mul_sum + the indicator product 𝟙_A·𝟙_B = 𝟙_{A∩B}), whose FC is integralSimple (t ×ˢ s) = (integralSimple t)·(integralSimple s).

P.Φ ⋯ ⋯ ⋯=P.∫ t a A⋅P.∫ s b BP.\Phi\,\cdots \,\cdots \,\cdots = P.\textstyle\int\,t\,a\,A \cdot P.\textstyle\int\,s\,b\,B

Proof. By boundedFC_congr, boundedFC_eq_integralSimple, integralSimple_product_eq. □\square

Used by boundedFC_simpleFunc_mul.

Lemma 659 (simpleFunc_eq_sum).  source ↗

SimpleFunc as a sum of scaled indicators (the bridge from Mathlib’s SimpleFunc, produced by approxOn, to the ∑ cᵢ 𝟙_{sᵢ} form of our FC lemmas): φ a = ∑_{y ∈ φ.range} y · 𝟙_{φ⁻¹{y}}(a). Exactly one range term is nonzero.

φ a=∑yφrangey⋅(φ−1′{y}).1 (λx↦1) a\varphi\,a = \sum_{y \varphi \mathrm{range}} y \cdot (\varphi ^{-1}{}' \{y\}).\mathbf{1}\,(\lambda x \mapsto 1)\,a

Proof. Immediate from the definitions. □\square

Used by boundedFC_simpleFunc, boundedFC_simpleFunc_mul.

Lemma 660 (boundedFC_simpleFunc).  source ↗

The FC of a SimpleFunc equals the spectral integral over its range: Φ(⇑φ) = ∑_{y ∈ φ.range} y · E(φ⁻¹{y}).

P.Φ hf hC0 hC=P.∫ φ.range id λy↦φ−1′{y}P.\Phi\,\mathrm{hf}\,\mathrm{hC0}\,\mathrm{hC} = P.\textstyle\int\,\varphi.\mathrm{range}\,\mathrm{id}\,\lambda y \mapsto \varphi ^{-1}{}' \{y\}

Proof. By boundedFC_congr, norm_indicatorOne_le, boundedFC_eq_integralSimple, simpleFunc_eq_sum. □\square

Used by boundedFC_simpleFunc_mul.

Lemma 661 (boundedFC_simpleFunc_mul).  source ↗

Multiplicativity on SimpleFuncs: Φ(⇑φ · ⇑ψ) = Φ(⇑φ)·Φ(⇑ψ). Reduces to boundedFC_simple_mul over the ranges of φ, ψ via simpleFunc_eq_sum.

P.Φ hfp hC0p hCp=P.Φ hfφ hC0φ hCφ⋅P.Φ hfψ hC0ψ hCψP.\Phi\,\mathrm{hfp}\,\mathrm{hC0p}\,\mathrm{hCp} = P.\Phi\,\mathrm{hf}\varphi\,\mathrm{hC0}\varphi\,\mathrm{hC}\varphi \cdot P.\Phi\,\mathrm{hf}\psi\,\mathrm{hC0}\psi\,\mathrm{hC}\psi

Proof. By integralSimple, boundedFC_congr, norm_indicatorOne_le, boundedFC_simple_mul, simpleFunc_eq_sum, boundedFC_simpleFunc. □\square

Used by boundedFC_mul_simpleFunc_left.

Lemma 662 (tendsto_diagInt_of_dominated).  source ↗

Dominated/bounded convergence for the diagonal functional: if fₙ → f pointwise with a common bound C, then D_{fₙ}(z) → D_f(z). (DCT against the finite measure μ_z.) The engine for extending FC identities from simple to all bounded Borel functions.

(∀(n:N),Measurable (f n))→(∀(n:N)(ω:Ω),∥f n ω∥≤C)→(∀(ω:Ω),Tendsto (λn↦f n ω) atTop (N (g ω)))→∀(z:H),Tendsto (λn↦P.∫ (f n) z) atTop (N (P.∫ g z))(\forall (n : \mathbb{N}), \mathrm{Measurable}\,(f\,n)) \to (\forall (n : \mathbb{N}) (\omega : \Omega), \|f\,n\,\omega\| \le C) \to (\forall (\omega : \Omega), \mathrm{Tendsto}\,(\lambda n \mapsto f\,n\,\omega)\,\mathrm{atTop}\,(\mathcal{N}\,(g\,\omega))) \to \forall (z : H), \mathrm{Tendsto}\,(\lambda n \mapsto P.\textstyle\int\,(f\,n)\,z)\,\mathrm{atTop}\,(\mathcal{N}\,(P.\textstyle\int\,g\,z))

Proof. By scalarMeasure, instIsFiniteMeasure_scalarMeasure. □\square

Used by tendsto_bilinDiag_of_dominated.

Lemma 663 (tendsto_bilinDiag_of_dominated).  source ↗

Bound-free form of the normality engine: B_{fₙ}(x,y) → B_f(x,y) under bounded pointwise convergence (the limit f needs no bound — bilinDiag carries none). This is the workhorse for the simple→bounded-Borel multiplicativity extension.

(∀(n:N),Measurable (f n))→(∀(n:N)(ω:Ω),∥f n ω∥≤C)→(∀(ω:Ω),Tendsto (λn↦f n ω) atTop (N (g ω)))→∀(xy:H),Tendsto (λn↦P.bd (f n) x y) atTop (N (P.bd g x y))(\forall (n : \mathbb{N}), \mathrm{Measurable}\,(f\,n)) \to (\forall (n : \mathbb{N}) (\omega : \Omega), \|f\,n\,\omega\| \le C) \to (\forall (\omega : \Omega), \mathrm{Tendsto}\,(\lambda n \mapsto f\,n\,\omega)\,\mathrm{atTop}\,(\mathcal{N}\,(g\,\omega))) \to \forall (x y : H), \mathrm{Tendsto}\,(\lambda n \mapsto P.\mathrm{bd}\,(f\,n)\,x\,y)\,\mathrm{atTop}\,(\mathcal{N}\,(P.\mathrm{bd}\,g\,x\,y))

Proof. By diagInt, tendsto_diagInt_of_dominated. □\square

Used by boundedFC_mul_simpleFunc_left, boundedFC_mul.

Definition 664 (approxSeq).  source ↗

The approxOn simple-function sequence for a bounded measurable f (base point 0, set univ): approxSeq f hf n is a SimpleFunc, → f pointwise, with ‖approxSeq f hf n ω‖ ≤ 2‖f ω‖.

aseq Ω f n  :=  approxOn f hf 0 _proof_2 n\mathrm{aseq}\,\Omega\,f\,n \;:=\; \mathrm{approxOn}\,f\,\mathrm{hf}\,0\,\mathrm{\_proof\_2}\,n

Used by approxSeq_tendsto, approxSeq_norm_le, approxSeq_measurable, boundedFC_mul_simpleFunc_left, boundedFC_mul.

Lemma 665 (approxSeq_tendsto).  source ↗

Tendsto (λn↦(aseq f hf n) ω) atTop (N (f ω))\mathrm{Tendsto}\,(\lambda n \mapsto (\href{/browser/qiqth-spectral-pvm#d-qiqth-spectral-projectionvaluedmeasure-approxseq}{\mathrm{aseq}}\,f\,\mathrm{hf}\,n)\,\omega)\,\mathrm{atTop}\,(\mathcal{N}\,(f\,\omega))

Proof. Immediate from the definitions. □\square

Used by boundedFC_mul_simpleFunc_left, boundedFC_mul.

Lemma 666 (approxSeq_norm_le).  source ↗

∥(aseq f hf n) ω∥≤∥f ω∥+∥f ω∥\|(\href{/browser/qiqth-spectral-pvm#d-qiqth-spectral-projectionvaluedmeasure-approxseq}{\mathrm{aseq}}\,f\,\mathrm{hf}\,n)\,\omega\| \le \|f\,\omega\| + \|f\,\omega\|

Proof. Immediate from the definitions. □\square

Used by boundedFC_mul_simpleFunc_left, boundedFC_mul.

Lemma 667 (approxSeq_measurable).  source ↗

Measurable (aseq f hf n)\mathrm{Measurable}\,(\href{/browser/qiqth-spectral-pvm#d-qiqth-spectral-projectionvaluedmeasure-approxseq}{\mathrm{aseq}}\,f\,\mathrm{hf}\,n)

Proof. Immediate from the definitions. □\square

Used by boundedFC_mul_simpleFunc_left, boundedFC_mul.

Lemma 668 (boundedFC_mul_simpleFunc_left).  source ↗

Stage 1 (left simple): Φ(⇑φ · g) = Φ(⇑φ)·Φ(g) for a SimpleFunc φ and a bounded measurable g. Approximate g by SimpleFuncs gₘ → g and pass to the weak limit: ⟪x, Φ(φ·gₘ)y⟫ = ⟪Φ(φ)†x, Φ(gₘ)y⟫ (by boundedFC_simpleFunc_mul), both sides converge (tendsto_bilinDiag), so the limits agree.

P.Φ hfp hC0p hCp=P.Φ hfφ hC0φ hCφ⋅P.Φ hg hC0g hCgP.\Phi\,\mathrm{hfp}\,\mathrm{hC0p}\,\mathrm{hCp} = P.\Phi\,\mathrm{hf}\varphi\,\mathrm{hC0}\varphi\,\mathrm{hC}\varphi \cdot P.\Phi\,\mathrm{hg}\,\mathrm{hC0g}\,\mathrm{hCg}

Proof. By bilinDiag, inner_boundedFC, boundedFC_simpleFunc_mul, tendsto_bilinDiag_of_dominated, approxSeq, approxSeq_tendsto, approxSeq_norm_le, approxSeq_measurable. □\square

Used by boundedFC_mul.

Lemma 669 (boundedFC_mul).  source ↗

MULTIPLICATIVITY OF THE BOUNDED-BOREL FUNCTIONAL CALCULUS (the keystone): Φ(f·g) = Φ(f)·Φ(g) for all bounded measurable f, g. Approximate f by SimpleFuncs fₙ → f and pass to the weak limit, using Stage 1 (left-simple multiplicativity) for each fₙ: ⟪x, Φ(fₙ·g)y⟫ = ⟪x, Φ(fₙ)(Φ(g)y)⟫, both sides converge (tendsto_bilinDiag), so the limits agree. Together with boundedFC_add, boundedFC_smul and boundedFC_const, the FC Φ : Bᵇ(Ω) → (H →L[ℂ] H) is a unital *-algebra homomorphism.

P.Φ hfp hC0p hCp=P.Φ hf hC0f hCf⋅P.Φ hg hC0g hCgP.\Phi\,\mathrm{hfp}\,\mathrm{hC0p}\,\mathrm{hCp} = P.\Phi\,\mathrm{hf}\,\mathrm{hC0f}\,\mathrm{hCf} \cdot P.\Phi\,\mathrm{hg}\,\mathrm{hC0g}\,\mathrm{hCg}

Proof. By bilinDiag, inner_boundedFC, tendsto_bilinDiag_of_dominated, approxSeq, approxSeq_tendsto, approxSeq_norm_le, approxSeq_measurable, boundedFC_mul_simpleFunc_left. □\square

Used by borelFC_mul.

← all sections · ← RicciSymm · SpectralTheorem →