Physicslib4.Spectral.Forms

Sesquilinear and quadratic forms on a Hilbert space

The blueprint constructs operators out of quadratic forms: an operator-valued integral against a projection-valued measure, and the bounded Borel functional calculus of a self-adjoint operator, are both obtained by exhibiting a bounded quadratic form and invoking existsUnique_operator_of_isBoundedQuadraticForm (the blueprint's Proposition A.63).

Main definitions

• Physicslib4.Spectral.SesquilinearForm — H →ₗ⋆[ℂ] H →ₗ[ℂ] ℂ, conjugate linear in the first slot and linear in the second (the physics convention, and the shape of Mathlib's innerSL).
• Physicslib4.Spectral.BoundedSesquilinearForm — H →L⋆[ℂ] H →L[ℂ] ℂ.
• Physicslib4.Spectral.polarization — the sesquilinear form associated with a quadratic form.
• Physicslib4.Spectral.IsQuadraticForm, Physicslib4.Spectral.IsBoundedQuadraticForm.
• Physicslib4.Spectral.IsBoundedQuadraticForm.toOperator — the bounded operator representing a bounded quadratic form.

Main statements

• Physicslib4.Spectral.sesquilinear_polarization — a sesquilinear form is determined by its diagonal.
• Physicslib4.Spectral.polarization_diag, Physicslib4.Spectral.exists_bound_polarization, Physicslib4.Spectral.polarization_conj_symm — the three properties of the polarization of a quadratic form asserted by the blueprint's Proposition A.61.
• Physicslib4.Spectral.existsUnique_operator_of_isBoundedQuadraticForm — a bounded quadratic form is ψ ↦ ⟪ψ, A ψ⟫ for a unique A ∈ 𝓑(H), and Physicslib4.Spectral.IsBoundedQuadraticForm.isSelfAdjoint_toOperator — that operator is self-adjoint when the form is real-valued.

Supporting lemmas

• Physicslib4.Spectral.norm_le_of_tendsto_of_bound — the quantitative half of lmm:bqf-pointwise-limit: a pointwise limit of uniformly bounded forms obeys the same bound.

Implementation notes

Sesquilinearity and bounded sesquilinearity are not recorded as predicates on raw functions H → H → ℂ: Mathlib bundles them as the semilinear map spaces H →ₗ⋆[ℂ] H →ₗ[ℂ] ℂ and H →L⋆[ℂ] H →L[ℂ] ℂ. A raw function F : H → H → ℂ is therefore asserted to be sesquilinear in the form ∃ L : SesquilinearForm H, ∀ φ ψ, L φ ψ = F φ ψ, which is the spelling used by IsQuadraticForm.isSesquilinear, exists_sesquilinearForm_sum (lmm:sesquilinear-linear-combination) and exists_sesquilinearForm_of_tendsto (lmm:sesquilinear-pointwise-limit).

Note that H →L⋆[ℂ] H →L[ℂ] ℂ is exactly the blueprint's notion of a bounded sesquilinear form: continuity of the outer map says ‖L φ‖ ≤ C ‖φ‖ in the operator norm, i.e. |L φ ψ| ≤ C ‖φ‖ ‖ψ‖.

Sesquilinear forms

@[reducible, inline]

abbrev Physicslib4.Spectral.SesquilinearForm (H : Type u_2) [NormedAddCommGroup H] [InnerProductSpace ℂ H] : Type u_2

The sesquilinear forms on H: maps L(φ, ψ) conjugate linear in φ and linear in ψ.

So L(aφ, ψ) = a̅ L(φ, ψ) and L(φ, aψ) = a L(φ, ψ) for a ∈ ℂ, and L is additive in each slot. This is the physics convention, the one of the inner product ⟨φ, ψ⟩, and the matrix elements ⟨φ, Aψ⟩ of any operator A form such a form. No boundedness is required.

Implementation note: this is Mathlib's semilinear map space H →ₗ⋆[ℂ] H →ₗ[ℂ] ℂ, the shape of innerSL. A raw function F : H → H → ℂ is said to be sesquilinear by ∃ L : SesquilinearForm H, ∀ φ ψ, L φ ψ = F φ ψ.

Blueprint: the sesquilinear forms of def:bounded-sesquilinear-form

Equations

• Physicslib4.Spectral.SesquilinearForm H = (H →ₗ⋆[ℂ] H →ₗ[ℂ] ℂ)

@[reducible, inline]

abbrev Physicslib4.Spectral.BoundedSesquilinearForm (H : Type u_2) [NormedAddCommGroup H] [InnerProductSpace ℂ H] : Type u_2

The bounded sesquilinear forms on H: sesquilinear L with |L(φ, ψ)| ≤ C‖φ‖‖ψ‖ for some constant C.

The matrix elements L(φ, ψ) = ⟨φ, Aψ⟩ of a bounded operator A are the basic example, with C = ‖A‖. The polarization of a bounded quadratic form is one (IsBoundedQuadraticForm.toSesq), and this is how the spectral files turn quadratic forms into operators.

Implementation note: this is Mathlib's space H →L⋆[ℂ] H →L[ℂ] ℂ of continuous conjugate-linear maps into the continuous linear functionals. Continuity of the outer map is the bound ‖L φ‖ ≤ C‖φ‖ in the operator norm, which is the bound |L(φ, ψ)| ≤ C‖φ‖‖ψ‖.

Blueprint: def:bounded-sesquilinear-form

Equations

• Physicslib4.Spectral.BoundedSesquilinearForm H = (H →L⋆[ℂ] H →L[ℂ] ℂ)

theorem Physicslib4.Spectral.sesquilinear_polarization {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (L : SesquilinearForm H) (φ ψ : H) : (L φ) ψ = 1 / 2 * ((L (φ + ψ)) (φ + ψ) - (L φ) φ - (L ψ) ψ) - Complex.I / 2 * ((L (φ + Complex.I • ψ)) (φ + Complex.I • ψ) - (L φ) φ - (L (Complex.I • ψ)) (Complex.I • ψ))

A sesquilinear form is determined by its values on the diagonal, through the polarization identity.

Blueprint reference: prpstn:hall-a.59.

theorem Physicslib4.Spectral.exists_sesquilinearForm_sum {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {ι : Type u_2} (s : Finset ι) (L : ι → SesquilinearForm H) (α : ι → ℂ) : ∃ (L₀ : SesquilinearForm H), ∀ (φ ψ : H), (L₀ φ) ψ = ∑ k ∈ s, α k * ((L k) φ) ψ

A finite linear combination ∑ k ∈ s, α k • L k of sesquilinear forms is a sesquilinear form. With sesquilinearity bundled into the type SesquilinearForm H this is the module structure on that space; what the blueprint asserts is that the raw function fun φ ψ => ∑ k ∈ s, α k * L k φ ψ is the value function of a sesquilinear form.

Blueprint reference: lmm:sesquilinear-linear-combination.

theorem Physicslib4.Spectral.exists_sesquilinearForm_of_tendsto {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {L : ℕ → SesquilinearForm H} {F : H → H → ℂ} (h : ∀ (φ ψ : H), Filter.Tendsto (fun (i : ℕ) => ((L i) φ) ψ) Filter.atTop (nhds (F φ ψ))) : ∃ (L₀ : SesquilinearForm H), ∀ (φ ψ : H), (L₀ φ) ψ = F φ ψ

A pointwise limit of sesquilinear forms is sesquilinear.

Blueprint reference: lmm:sesquilinear-pointwise-limit.

Quadratic forms

noncomputable def Physicslib4.Spectral.polarization {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (Q : H → ℂ) : H → H → ℂ

The polarization of a map Q : H → ℂ, the candidate sesquilinear form with diagonal Q.

It is L(φ, ψ) = ½ [Q(φ + ψ) − Q(φ) − Q(ψ)] − (i/2) [Q(φ + iψ) − Q(φ) − Q(iψ)]. For Q(ψ) = ⟨ψ, Aψ⟩ it gives back the matrix elements ⟨φ, Aψ⟩ (polarization_inner), and for a quadratic form it recovers Q on the diagonal, L(ψ, ψ) = Q(ψ) (polarization_diag). Whether L is sesquilinear is the second condition of IsQuadraticForm.

Implementation note: the definition is the raw function H → H → ℂ; for a bounded quadratic form it is bundled as IsBoundedQuadraticForm.toSesq.

Blueprint: the polarization L of def:bounded-quadratic-form

Equations

• Physicslib4.Spectral.polarization Q φ ψ = 1 / 2 * (Q (φ + ψ) - Q φ - Q ψ) - Complex.I / 2 * (Q (φ + Complex.I • ψ) - Q φ - Q (Complex.I • ψ))

structure Physicslib4.Spectral.IsQuadraticForm {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (Q : H → ℂ) : Prop

A quadratic form on H: a map Q : H → ℂ, |λ|²-homogeneous, whose polarization is sesquilinear.

The conditions are Q(λψ) = |λ|² Q(ψ) for λ ∈ ℂ and that the polarization of Q is a sesquilinear form. The prototype is the expectation-value map Q(ψ) = ⟨ψ, Aψ⟩ of an operator A. The spectral files build operators from quadratic forms: Q_f(ψ) = ∫ f dμ_ψ defines the operator-valued integral and the Borel functional calculus.

Blueprint: the quadratic forms of def:bounded-quadratic-form

• smul (l : ℂ) (ψ : H) : Q (l • ψ) = ↑‖l‖ ^ 2 * Q ψ

  Q (λ • ψ) = |λ|² Q ψ.

• isSesquilinear : ∃ (L : SesquilinearForm H), ∀ (φ ψ : H), (L φ) ψ = polarization Q φ ψ

  The polarization of Q is a sesquilinear form.

structure Physicslib4.Spectral.IsBoundedQuadraticForm {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (Q : H → ℂ) : Prop

A bounded quadratic form on H: a quadratic form Q with |Q(φ)| ≤ C‖φ‖² for some constant C.

Every bounded quadratic form is the expectation-value map of a unique bounded operator: Q(ψ) = ⟨ψ, Aψ⟩ for exactly one A (existsUnique_operator_of_isBoundedQuadraticForm; the operator is IsBoundedQuadraticForm.toOperator), and A is self-adjoint when Q is real-valued (IsBoundedQuadraticForm.isSelfAdjoint_toOperator). This is the route by which the operator-valued integral and the Borel functional calculus are defined.

Blueprint: def:bounded-quadratic-form

• isQuadratic : IsQuadraticForm Q

  The underlying form is quadratic.

• bounded : ∃ (C : ℝ), ∀ (φ : H), ‖Q φ‖ ≤ C * ‖φ‖ ^ 2

  The form is bounded by a multiple of ‖φ‖².

theorem Physicslib4.Spectral.polarization_diag {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {Q : H → ℂ} (hQ : IsQuadraticForm Q) (ψ : H) : Q ψ = polarization Q ψ ψ

The polarization of a quadratic form recovers Q on the diagonal.

Blueprint reference: prpstn:hall-a.61 (first part).

theorem Physicslib4.Spectral.exists_bound_polarization {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {Q : H → ℂ} (hQ : IsBoundedQuadraticForm Q) : ∃ (C : ℝ), ∀ (φ ψ : H), ‖polarization Q φ ψ‖ ≤ C * ‖φ‖ * ‖ψ‖

The polarization of a bounded quadratic form is a bounded sesquilinear form.

Blueprint reference: prpstn:hall-a.61 (second part).

theorem Physicslib4.Spectral.polarization_conj_symm {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {Q : H → ℂ} (hQ : IsQuadraticForm Q) (hreal : ∀ (ψ : H), (Q ψ).im = 0) (φ ψ : H) : polarization Q φ ψ = (starRingEnd ℂ) (polarization Q ψ φ)

The polarization of a real-valued quadratic form is conjugate symmetric.

Blueprint reference: prpstn:hall-a.61 (third part).

theorem Physicslib4.Spectral.IsBoundedQuadraticForm.add {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {Q R : H → ℂ} (hQ : IsBoundedQuadraticForm Q) (hR : IsBoundedQuadraticForm R) : IsBoundedQuadraticForm (Q + R)

A sum of bounded quadratic forms is a bounded quadratic form.

Blueprint reference: lmm:bqf-linear-combination.

theorem Physicslib4.Spectral.IsBoundedQuadraticForm.smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {Q : H → ℂ} (hQ : IsBoundedQuadraticForm Q) (α : ℂ) : IsBoundedQuadraticForm (α • Q)

A scalar multiple of a bounded quadratic form is a bounded quadratic form.

Blueprint reference: lmm:bqf-linear-combination.

theorem Physicslib4.Spectral.IsBoundedQuadraticForm.sum {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {ι : Type u_2} (s : Finset ι) {Q : ι → H → ℂ} (hQ : ∀ k ∈ s, IsBoundedQuadraticForm (Q k)) (α : ι → ℂ) : IsBoundedQuadraticForm fun (φ : H) => ∑ k ∈ s, α k * Q k φ

A finite linear combination of bounded quadratic forms is a bounded quadratic form.

Blueprint reference: lmm:bqf-linear-combination.

theorem Physicslib4.Spectral.isBoundedQuadraticForm_of_tendsto {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {Q : ℕ → H → ℂ} {Q₀ : H → ℂ} {C : ℝ} (hQ : ∀ (i : ℕ), IsQuadraticForm (Q i)) (h : BoundedPointwiseLimit Q Q₀ fun (φ : H) => C * ‖φ‖ ^ 2) : IsBoundedQuadraticForm Q₀

A pointwise limit of quadratic forms with a uniform bound C is a bounded quadratic form.

The blueprint takes the approximating forms to be bounded, but only their quadraticity is used: the bound on the limit comes from the uniform bound carried by BoundedPointwiseLimit, so hQ asks for no more than IsQuadraticForm.

Blueprint reference: lmm:bqf-pointwise-limit.

theorem Physicslib4.Spectral.norm_le_of_tendsto_of_bound {H : Type u_1} [NormedAddCommGroup H] {Q : ℕ → H → ℂ} {Q₀ : H → ℂ} {C : ℝ} (h : BoundedPointwiseLimit Q Q₀ fun (φ : H) => C * ‖φ‖ ^ 2) (φ : H) : ‖Q₀ φ‖ ≤ C * ‖φ‖ ^ 2

A pointwise limit of forms obeying a uniform bound C obeys the same bound. This is the quantitative half of lmm:bqf-pointwise-limit, and needs neither completeness nor the quadratic-form hypotheses: it is Physicslib4.Spectral.norm_le_of_tendsto with the dominating function fun φ => C * ‖φ‖ ^ 2.

Blueprint reference: lmm:bqf-pointwise-limit.

Bounded quadratic forms and bounded operators

theorem Physicslib4.Spectral.isBoundedQuadraticForm_inner {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A : H →L[ℂ] H) : IsBoundedQuadraticForm fun (ψ : H) => inner ℂ ψ (A ψ)

Every bounded operator A gives a bounded quadratic form ψ ↦ ⟪ψ, A ψ⟫.

Blueprint reference: prpstn:hall-a.62 (first part).

theorem Physicslib4.Spectral.polarization_inner {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A : H →L[ℂ] H) (φ ψ : H) : polarization (fun (χ : H) => inner ℂ χ (A χ)) φ ψ = inner ℂ φ (A ψ)

The polarization of the quadratic form of A is the sesquilinear form (φ, ψ) ↦ ⟪φ, A ψ⟫.

Blueprint reference: prpstn:hall-a.62 (second part).

noncomputable def Physicslib4.Spectral.IsBoundedQuadraticForm.toSesq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {Q : H → ℂ} (hQ : IsBoundedQuadraticForm Q) : BoundedSesquilinearForm H

The polarization of a bounded quadratic form Q, as a bounded sesquilinear form.

Its values are those of the polarization, L(φ, ψ) = polarization Q φ ψ (IsBoundedQuadraticForm.toSesq_apply), and it is bounded because Q is (exists_bound_polarization).

Implementation note: the Exists.chooses in the definition only pick a sesquilinear structure and a bound for a form whose values are already fixed, so the result does not depend on a choice.

Blueprint: the bounded sesquilinear form of prpstn:hall-a.61

Equations

• hQ.toSesq = LinearMap.mkContinuous₂ ⋯.choose ⋯.choose ⋯

@[simp]

theorem Physicslib4.Spectral.IsBoundedQuadraticForm.toSesq_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {Q : H → ℂ} (hQ : IsBoundedQuadraticForm Q) (φ ψ : H) : (hQ.toSesq φ) ψ = polarization Q φ ψ

noncomputable def Physicslib4.Spectral.IsBoundedQuadraticForm.toOperator {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {Q : H → ℂ} (hQ : IsBoundedQuadraticForm Q) : H →L[ℂ] H

The bounded operator A representing a bounded quadratic form Q, with Q(ψ) = ⟨ψ, Aψ⟩ for all ψ.

The identity is IsBoundedQuadraticForm.inner_toOperator, and A is the only bounded operator satisfying it (IsBoundedQuadraticForm.eq_toOperator). The operator-valued integral and the Borel functional calculus are both constructed this way, from the quadratic forms Q_f.

Implementation note: A is the adjoint of the Riesz representative of toSesq in Mathlib's InnerProductSpace.continuousLinearMapOfBilin, so that Q(ψ) is ⟨ψ, Aψ⟩ and not ⟨Aψ, ψ⟩. Other files use inner_toOperator and eq_toOperator, which characterise A, rather than unfolding it.

Blueprint: the operator of prpstn:hall-a.63

Equations

• hQ.toOperator = ContinuousLinearMap.adjoint (InnerProductSpace.continuousLinearMapOfBilin hQ.toSesq)

theorem Physicslib4.Spectral.IsBoundedQuadraticForm.inner_toOperator {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {Q : H → ℂ} (hQ : IsBoundedQuadraticForm Q) (ψ : H) : Q ψ = inner ℂ ψ (hQ.toOperator ψ)

The defining property of IsBoundedQuadraticForm.toOperator.

theorem Physicslib4.Spectral.existsUnique_operator_of_isBoundedQuadraticForm {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {Q : H → ℂ} (hQ : IsBoundedQuadraticForm Q) : ∃! A : H →L[ℂ] H, ∀ (ψ : H), Q ψ = inner ℂ ψ (A ψ)

A bounded quadratic form is represented by a unique bounded operator.

Blueprint reference: prpstn:hall-a.63.

theorem Physicslib4.Spectral.IsBoundedQuadraticForm.eq_toOperator {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {Q : H → ℂ} (hQ : IsBoundedQuadraticForm Q) {A : H →L[ℂ] H} (hA : ∀ (ψ : H), Q ψ = inner ℂ ψ (A ψ)) : A = hQ.toOperator

IsBoundedQuadraticForm.toOperator is the only operator representing Q.

theorem Physicslib4.Spectral.isSelfAdjoint_of_inner_self_real {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hreal : ∀ (ψ : H), (inner ℂ ψ (A ψ)).im = 0) : IsSelfAdjoint A

An operator whose quadratic form ψ ↦ ⟪ψ, A ψ⟫ is real-valued is self-adjoint.

This is the content of the second part of prpstn:hall-a.63, stripped of the quadratic form: the blueprint hypothesis IsBoundedQuadraticForm Q plays no role once Q is known to be ψ ↦ ⟪ψ, A ψ⟫, since a bounded operator is determined by, and symmetric as soon as it is real on, its diagonal.

theorem Physicslib4.Spectral.IsBoundedQuadraticForm.isSelfAdjoint_toOperator {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {Q : H → ℂ} (hQ : IsBoundedQuadraticForm Q) (hreal : ∀ (ψ : H), (Q ψ).im = 0) : IsSelfAdjoint hQ.toOperator

The operator representing a real-valued bounded quadratic form is self-adjoint.

Blueprint reference: prpstn:hall-a.63 (second part).