Physlib

PhyslibAlpha.AlgebraicFramework.WStarAlgebra.BoundedSesquilinearForm

Riesz realization of a bounded sesquilinear form

Trimmed port of the `BoundedSesquilinearForm` structure from `unbounded-alpha-public`'s `QuantumMechanics/Unbounded/Operators/SpectralTheory/BoundedSesquilinear.lean` — only the pieces `WStarAlgebra/TracePairingSurjectivity.lean` actually needs (`form`, `bound`, `operator`, `operator_inner`), dropping that file's weak-operator-topology bridge (`ofWOT`) and other self-adjointness helpers, which belong to spectral-measure infrastructure this repo's `AlgebraicFramework` scope does not include.

The convention is the one used by `InnerProductSpace.continuousLinearMapOfBilin`: `form x y` is conjugate-linear in `x` and linear in `y`, and the represented operator satisfies `⟪y, operator x⟫ = conj (form x y)`.

6 declarations

definition

Bound constant CC of a bounded sesquilinear form BB satisfying ∥B(x,y)∥≤C∥x∥∥y∥\|B(x, y)\| \le C \|x\| \|y\|

Let BB be a bounded sesquilinear form on a Hilbert space HH. The `boundConstant` is a real number CC that serves as a witness to the boundedness of the form, satisfying the inequality ∥B(x,y)∥≤C∥x∥∥y∥\|B(x, y)\| \le C \|x\| \|y\| for all x,y∈Hx, y \in H.

theorem

Boundedness inequality ∥B(x,y)∥≤C∥x∥∥y∥\|B(x, y)\| \le C \|x\| \|y\| for sesquilinear forms

Let BB be a bounded sesquilinear form. For all vectors xx and yy, the norm of the value of the form at (x,y)(x, y) is bounded by the product of the form's bound constant CC and the norms of xx and yy, such that ∥B(x,y)∥≤C∥x∥∥y∥\|B(x, y)\| \le C \|x\| \|y\|.

definition

Continuous map representation of a bounded sesquilinear form BB

Given a bounded sesquilinear form BB on a complex Hilbert space HH, this definition represents BB as a continuous conjugate-linear map from HH to the space of continuous linear functionals on HH. Specifically, it is the map that sends each x∈Hx \in H to the continuous linear functional y↦B(x,y)y \mapsto B(x, y), where the mapping is conjugate-linear in xx and linear in yy.

theorem

The continuous map representation of BB evaluated at x,yx, y equals B(x,y)B(x, y)

Let HH be a complex Hilbert space and BB be a bounded sesquilinear form on HH. For any vectors x,y∈Hx, y \in H, the value of the continuous conjugate-linear map representation of BB applied to xx and yy is equal to the value of the form B(x,y)B(x, y).

definition

Bounded linear operator TT satisfying ⟨y,Tx⟩=B(x,y)‾\langle y, Tx \rangle = \overline{B(x, y)}

Let HH be a complex Hilbert space and BB be a bounded sesquilinear form on HH that is conjugate-linear in its first argument and linear in its second. This definition represents the unique continuous linear operator T:H→HT: H \to H associated with BB such that for all x,y∈Hx, y \in H, the inner product satisfies ⟨y,Tx⟩=B(x,y)‾\langle y, Tx \rangle = \overline{B(x, y)}, where B(x,y)‾\overline{B(x, y)} denotes the complex conjugate of the form.

theorem

⟨y,Tx⟩=B(x,y)‾\langle y, Tx \rangle = \overline{B(x, y)} for the operator associated with a bounded sesquilinear form

Let HH be a complex Hilbert space and BB be a bounded sesquilinear form on HH that is conjugate-linear in its first argument and linear in its second. Let TT be the unique bounded linear operator associated with BB (the Riesz realization). For any x,y∈Hx, y \in H, the inner product of yy and TxTx is equal to the complex conjugate of the sesquilinear form evaluated at xx and yy: ⟨y,Tx⟩=B(x,y)‾\langle y, Tx \rangle = \overline{B(x, y)}