Physicslib4.Spectral.Unbounded.Normal

Bounded normal operators

The Cayley transform turns an unbounded self-adjoint operator into a bounded operator that is normal but not self-adjoint, so the spectral theorem is needed for bounded normal operators. This file carries out the first stage: the continuous functional calculus for a bounded normal operator, built through a two-variable spectral mapping theorem for polynomials in A and A*.

A normal operator is Mathlib's IsStarNormal. A polynomial in two variables is an MvPolynomial (Fin 2) ℂ; substituting A for the first variable and A* for the second is mvApply, defined coefficientwise (so no commutativity of the target algebra is required), and the corresponding scalar function λ ↦ p(λ, conj λ) is mvEvalConj.

Main definitions

• mvApply, mvEvalConj, mvPolyOn — polynomials in A and A*.
• spectralSubspace — the range of a spectral projection.
• IsAlmostEigenvector — the blueprint's ε-almost eigenvector.
• normalCalculus — the continuous functional calculus of a normal operator.

Main statements

• tendsto_norm_pow_div_atTop, spectralRadius_mul_le_of_commute — power growth and the spectral radius of a commuting product.
• mapsTo_pvmOperator_spectralSubspace, norm_sub_smul_le_of_mem_spectralSubspace, spectralSubspace_ne_bot — properties of spectral subspaces.
• commute_borelCalculus, mapsTo_spectralSubspace_of_commute — commuting operators preserve spectral subspaces.
• norm_adjoint_sub_smul_apply, isAlmostEigenvector_adjoint, mem_spectrum_iff_forall_isAlmostEigenvector — almost eigenvectors.
• spectrum_mvApply — the two-variable spectral mapping theorem.
• norm_mvApply — the norm of a polynomial in A and A*.
• existsUnique_normalCalculus and the property lemmas — the continuous functional calculus for a normal operator.

Polynomials in A and A*

noncomputable def Physicslib4.Spectral.Unbounded.mvApply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A : H →L[ℂ] H) (p : MvPolynomial (Fin 2) ℂ) : H →L[ℂ] H

The operator p(A, A*) obtained by substituting a bounded operator A and its adjoint into a polynomial in two variables.

A polynomial p(λ, λ̄) = Σ a(kl) λᵏ λ̄ˡ in a complex variable and its conjugate becomes the bounded operator p(A, A*) = Σ a(kl) Aᵏ (A*)ˡ, with all powers of A written to the left of the powers of A*. For a normal A (one that commutes with its adjoint) the ordering does not matter, and p(A, A*) is again normal and commutes with A and A* (isStarNormal_mvApply, commute_mvApply). These are the operators from which the continuous functional calculus of a normal operator is built.

Implementation note: the polynomial is an MvPolynomial (Fin 2) ℂ, whose first variable stands for λ and second for λ̄. The definition is the sum over the coefficients, so it needs no commutativity of A and A* and makes sense for every bounded A; normality is used only in the theorems about it.

Blueprint: lmm:polynomials-in-normal-are-normal

Equations

• Physicslib4.Spectral.Unbounded.mvApply A p = ∑ d ∈ p.support, p.coeff d • (A ^ d 0 * ContinuousLinearMap.adjoint A ^ d 1)

noncomputable def Physicslib4.Spectral.Unbounded.mvEvalConj (p : MvPolynomial (Fin 2) ℂ) (lam : ℂ) : ℂ

The complex function λ ↦ p(λ, λ̄) defined by a polynomial in two variables.

This is the scalar counterpart of mvApply: the same polynomial, with λ substituted for the first variable and its complex conjugate λ̄ for the second. By the two-variable spectral mapping theorem (spectrum_mvApply), for a normal A the spectrum of p(A, A*) is the image of the spectrum of A under this function.

Blueprint: lmm:polynomials-in-normal-are-normal

Equations

• Physicslib4.Spectral.Unbounded.mvEvalConj p lam = ∑ d ∈ p.support, p.coeff d * lam ^ d 0 * (starRingEnd ℂ) lam ^ d 1

Norm and spectral radius

theorem Physicslib4.Spectral.Unbounded.tendsto_norm_pow_div_atTop {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A : H →L[ℂ] H) {T : ℝ} (hT : 0 < T) (hRT : spectralRadius ℂ A < ENNReal.ofReal T) : Filter.Tendsto (fun (m : ℕ) => ‖A ^ m‖ / T ^ m) Filter.atTop (nhds 0)

Powers of a bounded operator grow no faster than the spectral radius allows: if R(A) < T then ‖Aᵐ‖ / Tᵐ → 0.

The blueprint's standing hypothesis H ≠ {0}, needed there for σ(A) to be non-empty and hence R(A) to be a supremum over a non-empty set, is Nontrivial H.

Blueprint reference: lmm:power-growth-controlled-by-spectral-radius.

theorem Physicslib4.Spectral.Unbounded.spectralRadius_mul_le_of_commute {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A B : H →L[ℂ] H} (h : Commute A B) : spectralRadius ℂ (A * B) ≤ spectralRadius ℂ A * spectralRadius ℂ B

The spectral radius is submultiplicative on commuting operators.

Blueprint reference: lmm:hall-10.22.

Spectral subspaces

def Physicslib4.Spectral.Unbounded.spectralSubspace {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : Type u_2} [MeasurableSpace X] (μ : ProjectionValuedMeasure X H) (E : Set X) : Submodule ℂ H

The spectral subspace V(E) of a projection-valued measure μ and a measurable set E: the range of the projection μ(E).

When μ is the spectral measure of an observable A, V(E) consists of the states in which a measurement of A gives a value in E with certainty. Each V(E) is a closed subspace of H, because the range of an orthogonal projection is closed (isClosed_range_of_isStarProjection), and hence a Hilbert space in its own right.

Implementation note: the measure is on an arbitrary measurable space X, so the definition covers both the self-adjoint and the normal case of the blueprint. The subspace is the range of the underlying linear map of μ E, as a Submodule ℂ H.

Blueprint: def:hall-7.14

Equations

• Physicslib4.Spectral.Unbounded.spectralSubspace μ E = (↑(μ E)).range

noncomputable def Physicslib4.Spectral.Unbounded.pvmOperator {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {Y : Set ℂ} (μ : ProjectionValuedMeasure (↑Y) H) : H →L[ℂ] H

The bounded operator ∫ λ dμ(λ) defined by a projection-valued measure μ on a subset Y of ℂ.

It is the operator whose spectral measure μ is meant to be: the integral of the coordinate function λ ↦ λ against μ. On a compact Y this function is bounded and measurable (coe_mem_bddMeasurable), so the integral is a bounded operator. Its spectral subspaces are invariant under it (mapsTo_pvmOperator_spectralSubspace), and it acts on V(E) as multiplication by λ₀ up to an error ε when E lies within distance ε of λ₀ (norm_sub_smul_le_of_mem_spectralSubspace).

Implementation note: the definition takes any Y; compactness of Y is a hypothesis of the theorems about it.

Blueprint: prpstn:hall-7.15

Equations

• Physicslib4.Spectral.Unbounded.pvmOperator μ = μ.integral fun (y : ↑Y) => ↑y

theorem Physicslib4.Spectral.Unbounded.coe_mem_bddMeasurable {Y : Set ℂ} (hY : IsCompact Y) : (fun (y : ↑Y) => ↑y) ∈ BddMeasurable ↑Y

The inclusion Y ↪ ℂ of a compact set is bounded and measurable.

theorem Physicslib4.Spectral.Unbounded.indicator_one_mem_bddMeasurable {X : Type u_2} [MeasurableSpace X] {E : Set X} (hE : MeasurableSet E) : E.indicator 1 ∈ BddMeasurable X

The indicator function of a measurable set is bounded and measurable.

theorem Physicslib4.Spectral.Unbounded.integral_coe_sub_const {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {Y : Set ℂ} (hY : IsCompact Y) (μ : ProjectionValuedMeasure (↑Y) H) (lam₀ : ℂ) : (μ.integral fun (y : ↑Y) => ↑y - lam₀) = pvmOperator μ - lam₀ • 1

∫ (ι - λ₀) dμ = ∫ ι dμ - λ₀ 1.

theorem Physicslib4.Spectral.Unbounded.mapsTo_pvmOperator_spectralSubspace {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {Y : Set ℂ} (hY : IsCompact Y) (μ : ProjectionValuedMeasure (↑Y) H) (E : Set ↑Y) (ψ : H) (hψ : ψ ∈ spectralSubspace μ E) : (pvmOperator μ) ψ ∈ spectralSubspace μ E

Each spectral subspace is invariant under ∫ ι dμ.

Blueprint reference: prpstn:hall-7.15 (Part 1).

theorem Physicslib4.Spectral.Unbounded.norm_sub_smul_le_of_mem_spectralSubspace {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {Y : Set ℂ} (hY : IsCompact Y) (μ : ProjectionValuedMeasure (↑Y) H) {E : Set ↑Y} {lam₀ : ℂ} {ε : ℝ} (hε : 0 < ε) (hE : ∀ y ∈ E, ‖↑y - lam₀‖ ≤ ε) {ψ : H} (hψ : ψ ∈ spectralSubspace μ E) : ‖(pvmOperator μ - lam₀ • 1) ψ‖ ≤ ε * ‖ψ‖

If E sits in the closed ε-disc about λ₀, then ‖(A - λ₀ 1) ψ‖ ≤ ε ‖ψ‖ on the corresponding spectral subspace.

Blueprint reference: prpstn:hall-7.15 (Part 2).

theorem Physicslib4.Spectral.Unbounded.spectralSubspace_ne_bot {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {Y : Set ℂ} (hY : IsCompact Y) (μ : ProjectionValuedMeasure (↑Y) H) {lam₀ : ℂ} (hlam : lam₀ ∈ spectrum ℂ (pvmOperator μ)) {U : Set ℂ} (hU : IsOpen U) (hlamU : lam₀ ∈ U) : spectralSubspace μ {y : ↑Y | ↑y ∈ U} ≠ ⊥

Spectral subspaces attached to neighbourhoods of a spectral point are non-trivial.

Blueprint reference: prpstn:hall-7.15 (Part 3).

theorem Physicslib4.Spectral.Unbounded.commute_borelCalculus {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) {B : H →L[ℂ] H} (hB : Commute A B) {f : ↑(spectrum ℝ A) → ℂ} (hf : f ∈ BddMeasurable ↑(spectrum ℝ A)) : Commute (borelCalculus hA f) B

An operator commuting with a bounded self-adjoint A commutes with the whole bounded Borel functional calculus of A.

Blueprint reference: prpstn:hall-7.16 (Part 1).

theorem Physicslib4.Spectral.Unbounded.mapsTo_spectralSubspace_of_commute {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) {B : H →L[ℂ] H} (hB : Commute A B) (E : Set ↑(spectrum ℝ A)) (ψ : H) (hψ : ψ ∈ spectralSubspace (spectralMeasure hA) E) : B ψ ∈ spectralSubspace (spectralMeasure hA) E

Consequently every spectral subspace of A is invariant under B.

Blueprint reference: prpstn:hall-7.16 (Part 2).

Almost eigenvectors

theorem Physicslib4.Spectral.Unbounded.norm_adjoint_sub_smul_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} [IsStarNormal A] (lam : ℂ) (ψ : H) : ‖(ContinuousLinearMap.adjoint A - (starRingEnd ℂ) lam • 1) ψ‖ = ‖(A - lam • 1) ψ‖

For a normal A, the operators A - λ 1 and A* - conj λ 1 have the same action on norms.

Blueprint reference: lmm:normality-balances-norms.

structure Physicslib4.Spectral.Unbounded.IsAlmostEigenvector {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A : H →L[ℂ] H) (lam : ℂ) (ε : ℝ) (ψ : H) : Prop

A vector ψ is an ε-almost eigenvector of a bounded operator A with eigenvalue λ: ψ is nonzero and ‖(A − λ𝟙)ψ‖ < ε‖ψ‖.

A point of the continuous spectrum, such as a value of the position operator, has no eigenvector, but it has approximate ones: wave packets sharply peaked at that point. For a normal A, λ lies in the spectrum exactly when, for every ε > 0, there is an ε-almost eigenvector with eigenvalue λ (mem_spectrum_iff_forall_isAlmostEigenvector).

Implementation note: the definition places no condition on ε; the blueprint's ε > 0 is a hypothesis of the theorems that use it.

Blueprint: def:hall-10.24

• ne_zero : ψ ≠ 0

  The vector ψ is nonzero.

• norm_lt : ‖(A - lam • 1) ψ‖ < ε * ‖ψ‖

  The strict inequality ‖(A − λ𝟙)ψ‖ < ε‖ψ‖.

theorem Physicslib4.Spectral.Unbounded.isAlmostEigenvector_adjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} [IsStarNormal A] {lam : ℂ} {ε : ℝ} {ψ : H} (h : IsAlmostEigenvector A lam ε ψ) : IsAlmostEigenvector (ContinuousLinearMap.adjoint A) ((starRingEnd ℂ) lam) ε ψ

An almost eigenvector of a normal A with eigenvalue λ is one for A* with eigenvalue conj λ.

Blueprint reference: lmm:hall-10.25 (Part 1).

theorem Physicslib4.Spectral.Unbounded.mem_spectrum_iff_forall_isAlmostEigenvector {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} [IsStarNormal A] (lam : ℂ) : lam ∈ spectrum ℂ A ↔ ∀ (ε : ℝ), 0 < ε → ∃ (ψ : H), IsAlmostEigenvector A lam ε ψ

For a normal operator, the spectrum is exactly the set of λ admitting ε-almost eigenvectors for every ε > 0.

Blueprint reference: lmm:hall-10.25 (Part 2).

theorem Physicslib4.Spectral.Unbounded.exists_const_isAlmostEigenvector_mvApply_uniform {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} [IsStarNormal A] (p : MvPolynomial (Fin 2) ℂ) (R : ℝ) : ∃ (C : ℝ), 0 < C ∧ ∀ (lam : ℂ), ‖lam‖ ≤ R → ∀ (ε : ℝ) (ψ : H), IsAlmostEigenvector A lam ε ψ → IsAlmostEigenvector (mvApply A p) (mvEvalConj p lam) (C * ε) ψ

Uniform constant for polynomials in A and A*. For every radius R, one constant C works for all eigenvalues λ with ‖λ‖ ≤ R: it depends only on p, A and R.

Blueprint reference: lmm:hall-10.26.

theorem Physicslib4.Spectral.Unbounded.exists_const_isAlmostEigenvector_mvApply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} [IsStarNormal A] (p : MvPolynomial (Fin 2) ℂ) (lam : ℂ) : ∃ (C : ℝ), 0 < C ∧ ∀ (ε : ℝ) (ψ : H), IsAlmostEigenvector A lam ε ψ → IsAlmostEigenvector (mvApply A p) (mvEvalConj p lam) (C * ε) ψ

Polynomials in A and A* turn ε-almost eigenvectors into (C ε)-almost eigenvectors, with C independent of ε and ψ.

Blueprint reference: lmm:hall-10.26.

theorem Physicslib4.Spectral.Unbounded.adjoint_mvApply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (p : MvPolynomial (Fin 2) ℂ) : ContinuousLinearMap.adjoint (mvApply A p) = ∑ d ∈ p.support, (starRingEnd ℂ) (p.coeff d) • (A ^ d 1 * ContinuousLinearMap.adjoint A ^ d 0)

The adjoint of p(A, A*) is obtained by conjugating the coefficients and swapping the two exponents.

Blueprint reference: lmm:polynomials-in-normal-are-normal.

theorem Physicslib4.Spectral.Unbounded.isStarNormal_mvApply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} [IsStarNormal A] (p : MvPolynomial (Fin 2) ℂ) : IsStarNormal (mvApply A p)

p(A, A*) is again normal.

Blueprint reference: lmm:polynomials-in-normal-are-normal.

theorem Physicslib4.Spectral.Unbounded.commute_mvApply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} [IsStarNormal A] (p : MvPolynomial (Fin 2) ℂ) : Commute (mvApply A p) A ∧ Commute (mvApply A p) (ContinuousLinearMap.adjoint A) ∧ Commute (ContinuousLinearMap.adjoint (mvApply A p)) A ∧ Commute (ContinuousLinearMap.adjoint (mvApply A p)) (ContinuousLinearMap.adjoint A)

p(A, A*) and its adjoint commute with A and with A*.

Blueprint reference: lmm:polynomials-in-normal-are-normal.

theorem Physicslib4.Spectral.Unbounded.exists_restrict_isStarNormal {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} [IsStarNormal A] {W : Submodule ℂ H} (_hW : IsClosed ↑W) [CompleteSpace ↥W] (_hne : W ≠ ⊥) (hAW : ∀ ψ ∈ W, A ψ ∈ W) (hA'W : ∀ ψ ∈ W, (ContinuousLinearMap.adjoint A) ψ ∈ W) : ∃ (B : ↥W →L[ℂ] ↥W), (∀ (ψ : ↥W), ↑(B ψ) = A ↑ψ) ∧ IsStarNormal B ∧ (∀ (ψ : ↥W), ↑((ContinuousLinearMap.adjoint B) ψ) = (ContinuousLinearMap.adjoint A) ↑ψ) ∧ ‖B‖ ≤ ‖A‖

A normal operator restricted to a nonzero closed subspace invariant under both A and A* is again normal, with adjoint the restriction of A* and norm at most ‖A‖.

Blueprint reference: lmm:restriction-of-normal-operator.

theorem Physicslib4.Spectral.Unbounded.exists_subspace_isAlmostEigenvector {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} [IsStarNormal A] (p : MvPolynomial (Fin 2) ℂ) {ν : ℂ} (hν : ν ∈ spectrum ℂ (mvApply A p)) {ε : ℝ} (hε : 0 < ε) : ∃ (W : Submodule ℂ H), W ≠ ⊥ ∧ IsClosed ↑W ∧ (∀ ψ ∈ W, A ψ ∈ W) ∧ (∀ ψ ∈ W, (ContinuousLinearMap.adjoint A) ψ ∈ W) ∧ ∀ ψ ∈ W, ψ ≠ 0 → IsAlmostEigenvector (mvApply A p) ν ε ψ

For ν in the spectrum of p(A, A*) there is, for every ε > 0, a nonzero closed subspace invariant under A and A* all of whose nonzero vectors are ε-almost eigenvectors for p(A, A*) with eigenvalue ν.

The proof does not follow the blueprint's route through lmm:hall-10.26, the spectral subspaces of B*B and prpstn:hall-7.15/prpstn:hall-7.16. With B = p(A, A*) - ν, it gets 0 ∈ σ(B*B) directly from Commute.isUnit_mul_iff, and takes W to be the kernel of f(B*B) for a clamp function f, built with Mathlib's continuous functional calculus cfc.

Blueprint reference: lmm:hall-10.27.

The two-variable spectral mapping theorem

theorem Physicslib4.Spectral.Unbounded.spectrum_mvApply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} [IsStarNormal A] (p : MvPolynomial (Fin 2) ℂ) : spectrum ℂ (mvApply A p) = mvEvalConj p '' spectrum ℂ A

The spectral mapping theorem for polynomials in a normal operator and its adjoint: the spectrum of p(A, A*) is the set of values p(λ, λ̄) with λ in the spectrum of A.

For a normal A this is the statement that p(A, A*) acts on the spectrum the way the polynomial acts on numbers. It gives the norm of p(A, A*) as the supremum of |p(λ, λ̄)| over the spectrum (norm_mvApply), the estimate on which the continuous functional calculus of a normal operator rests.

Implementation note: the proof does not follow the blueprint's almost-eigenvector argument (lmm:hall-10.25 to lmm:hall-10.27). It identifies mvApply A p with Mathlib's continuous functional calculus of A applied to λ ↦ p(λ, λ̄) (mvApply_eq_cfc) and uses Mathlib's spectral mapping theorem cfc_map_spectrum. The blueprint's hypothesis H ≠ {0} is not needed.

Blueprint: thrm:hall-10.23

theorem Physicslib4.Spectral.Unbounded.norm_mvApply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] {A : H →L[ℂ] H} [IsStarNormal A] (p : MvPolynomial (Fin 2) ℂ) : ‖mvApply A p‖ = sSup ((fun (lam : ℂ) => ‖mvEvalConj p lam‖) '' spectrum ℂ A)

The norm of a polynomial in A and A* is the supremum of |p(λ, conj λ)| over the spectrum.

Blueprint reference: crllr:norm-of-polynomial-in-a-astar.

The continuous functional calculus for a normal operator

noncomputable def Physicslib4.Spectral.Unbounded.mvPolyOn {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A : H →L[ℂ] H) (p : MvPolynomial (Fin 2) ℂ) : C(↑(spectrum ℂ A), ℂ)

The function λ ↦ p(λ, λ̄) on the spectrum of A, as a continuous function.

This is mvEvalConj restricted to σ(A) and regarded as an element of C(σ(A), ℂ), the domain of the continuous functional calculus normalCalculus, which sends it to p(A, A*) (normalCalculus_mvPolyOn).

Blueprint: thrm:continuous-functional-calculus-normal

Equations

• Physicslib4.Spectral.Unbounded.mvPolyOn A p = { toFun := fun (lam : ↑(spectrum ℂ A)) => Physicslib4.Spectral.Unbounded.mvEvalConj p ↑lam, continuous_toFun := ⋯ }

noncomputable def Physicslib4.Spectral.Unbounded.normalCalculus {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsStarNormal A) : C(↑(spectrum ℂ A), ℂ) →⋆ₐ[ℂ] H →L[ℂ] H

The continuous functional calculus f ↦ f(A) of a bounded normal operator A, for continuous complex functions f on the spectrum of A.

A bounded operator A is normal when it commutes with its adjoint, A A* = A* A; self-adjoint and unitary operators are the main examples. For such A every continuous f on σ(A) defines a bounded operator f(A). The map f ↦ f(A) is linear and multiplicative, sends f̄ to f(A)*, is isometric (‖f(A)‖ = sup |f| on σ(A)), and sends 1 to 𝟙 and λ ↦ λ to A (normalCalculus_mul, normalCalculus_star, norm_normalCalculus, normalCalculus_one_and_id). It is the unique bounded linear map extending p ↦ p(A, A*) (existsUnique_normalCalculus).

Implementation note: the definition is Mathlib's continuous functional calculus cfcHom for the predicate IsStarNormal, available because Mathlib makes H →L[ℂ] H a C*-algebra. It is a star-algebra homomorphism, so linearity, multiplicativity and the adjoint property hold by construction. Mathlib's construction replaces the blueprint's density argument through the two-variable spectral mapping theorem; existsUnique_normalCalculus connects the two.

Blueprint: thrm:continuous-functional-calculus-normal

Equations

• Physicslib4.Spectral.Unbounded.normalCalculus hA = cfcHom hA

theorem Physicslib4.Spectral.Unbounded.normalCalculus_mvPolyOn {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsStarNormal A) (p : MvPolynomial (Fin 2) ℂ) : (normalCalculus hA) (mvPolyOn A p) = mvApply A p

normalCalculus extends p ↦ p(A, A*).

Blueprint reference: thrm:continuous-functional-calculus-normal (the defining property).

theorem Physicslib4.Spectral.Unbounded.existsUnique_normalCalculus {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsStarNormal A) : ∃! T : C(↑(spectrum ℂ A), ℂ) →L[ℂ] H →L[ℂ] H, ∀ (p : MvPolynomial (Fin 2) ℂ), T (mvPolyOn A p) = mvApply A p

The continuous functional calculus of a normal operator is unique: exactly one bounded linear map from C(σ(A), ℂ) to the bounded operators sends each λ ↦ p(λ, λ̄) to p(A, A*).

The functions λ ↦ p(λ, λ̄) are dense in C(σ(A), ℂ) by the Stone–Weierstrass theorem, so a bounded linear map is fixed by its values on them. The map in question is normalCalculus.

Implementation note: uniqueness comes from Mathlib's Stone–Weierstrass theorem in the form ContinuousMap.elemental_id_eq_top: the star-subalgebra generated by λ ↦ λ is dense. The blueprint's hypothesis H ≠ {0} is not needed.

Blueprint: thrm:continuous-functional-calculus-normal

theorem Physicslib4.Spectral.Unbounded.normalCalculus_mul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsStarNormal A) (f g : C(↑(spectrum ℂ A), ℂ)) : (normalCalculus hA) (f * g) = (normalCalculus hA) f * (normalCalculus hA) g

Multiplicativity of the normal functional calculus.

Blueprint reference: thrm:continuous-functional-calculus-normal (Property 2).

theorem Physicslib4.Spectral.Unbounded.normalCalculus_star {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsStarNormal A) (f : C(↑(spectrum ℂ A), ℂ)) : (normalCalculus hA) (star f) = star ((normalCalculus hA) f)

The calculus intertwines complex conjugation with the adjoint.

Blueprint reference: thrm:continuous-functional-calculus-normal (Property 3).

theorem Physicslib4.Spectral.Unbounded.norm_normalCalculus {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsStarNormal A) (f : C(↑(spectrum ℂ A), ℂ)) : ‖(normalCalculus hA) f‖ = ‖f‖

The calculus is isometric.

Blueprint reference: thrm:continuous-functional-calculus-normal (Property 4).

theorem Physicslib4.Spectral.Unbounded.normalCalculus_one_and_id {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsStarNormal A) : (normalCalculus hA) 1 = 1 ∧ (normalCalculus hA) { toFun := fun (lam : ↑(spectrum ℂ A)) => ↑lam, continuous_toFun := ⋯ } = A

The calculus sends the constant 1 to 1 and the identity function to A.

Blueprint reference: thrm:continuous-functional-calculus-normal (Property 5).

theorem Physicslib4.Spectral.Unbounded.isSelfAdjoint_normalCalculus_of_real {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsStarNormal A) {f : C(↑(spectrum ℂ A), ℂ)} (hf : ∀ (lam : ↑(spectrum ℂ A)), (f lam).im = 0) : IsSelfAdjoint ((normalCalculus hA) f)

A real-valued f gives a self-adjoint operator, and every f gives a normal one.

Blueprint reference: thrm:continuous-functional-calculus-normal (final paragraph).

theorem Physicslib4.Spectral.Unbounded.isStarNormal_normalCalculus {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsStarNormal A) (f : C(↑(spectrum ℂ A), ℂ)) : IsStarNormal ((normalCalculus hA) f)

Every value of the calculus is normal.

Blueprint reference: thrm:continuous-functional-calculus-normal (final paragraph).