Physicslib4.Spectral.Unbounded.Integral

Integration of an unbounded function against a projection-valued measure

Physicslib4/Spectral/OperatorIntegral.lean defines μ.integral f : H →L[ℂ] H for a bounded measurable f. Here the integrand is allowed to be unbounded, so the resulting operator pmapIntegral μ f is an unbounded operator — a LinearPMap — with domain

W_f = {ψ | ∫ |f|² dμ_ψ < ∞},

which is integralDomain μ f, spelled with Mathlib's MemLp f 2 (μ.assoc ψ).

Along the way we need quadratic and sesquilinear forms defined on a subspace D ⊆ H rather than on all of H, since W_f (and, in the proof of prpstn:hall-10.3, a spectral subspace) is not all of H. These mirror Physicslib4/Spectral/Forms.lean.

Main definitions

• SesquilinearFormOn, polarizationOn, IsQuadraticFormOn, IsBoundedQuadraticFormOn — forms on a subspace.
• integralDomain, integralForm — W_f and Q_f.
• pmapIntegral — ∫ f dμ as an unbounded operator.

Main statements

• assoc_univ_eq, norm_sq_integral_apply — total mass of μ_ψ and the norm identity for the bounded integral.
• dense_integralDomain, isQuadraticFormOn_integralForm, norm_polarizationOn_integralForm_le, existsUnique_repr_integralForm — the blueprint's Proposition 10.2.
• inner_pmapIntegral, inner_self_pmapIntegral, norm_sq_pmapIntegral, eq_pmapIntegral_of_inner_self — the blueprint's Proposition 10.1.
• integralDomain_eq_top_of_bddMeasurable, pmapIntegral_of_bddMeasurable — agreement with the bounded integral.
• integralDomain_congr_of_null, pmapIntegral_congr_of_null, tendsto_integral_truncation, assoc_integral_apply, mapsTo_pmapIntegral_range — the further facts needed for the Cayley transform.
• isSelfAdjoint_pmapIntegral_of_real — the integral of a real-valued function is self-adjoint.

Quadratic and sesquilinear forms on a subspace

@[reducible, inline]

abbrev Physicslib4.Spectral.Unbounded.SesquilinearFormOn {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (D : Submodule ℂ H) : Type u_2

The type of sesquilinear forms L(φ, ψ) on a subspace D of H: maps D × D → ℂ that are conjugate-linear in φ and linear in ψ.

The inner product ⟨φ, ψ⟩ and the matrix elements ⟨φ, Aψ⟩ of an operator are the basic examples. Forms on a subspace, rather than on all of H, are needed because the integral of an unbounded function is built from a form on its domain W_f (integralDomain), which is in general smaller than H. For D = H this is the notion of Physicslib4.Spectral.SesquilinearForm.

Implementation note: as in Physicslib4/Spectral/Forms.lean, sesquilinearity is not a predicate on functions D → D → ℂ but Mathlib's type of bundled semilinear maps D →ₗ⋆[ℂ] D →ₗ[ℂ] ℂ. A raw function is sesquilinear when it agrees with some element of this type, which is how IsQuadraticFormOn.isSesquilinear is stated.

Blueprint: def:hall-sesquilinear-form-on-a-subspace

Equations

• Physicslib4.Spectral.Unbounded.SesquilinearFormOn D = (↥D →ₗ⋆[ℂ] ↥D →ₗ[ℂ] ℂ)

noncomputable def Physicslib4.Spectral.Unbounded.polarizationOn {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {D : Submodule ℂ H} (Q : ↥D → ℂ) : ↥D → ↥D → ℂ

The polarization L(φ, ψ) of a function Q on a subspace D: the formula that recovers a sesquilinear form from its values on the diagonal.

Explicitly, L(φ, ψ) = ½[Q(φ + ψ) − Q(φ) − Q(ψ)] − (i/2)[Q(φ + iψ) − Q(φ) − Q(iψ)]. If Q(ψ) = ⟨ψ, Tψ⟩ for a linear map T on D, then L(φ, ψ) = ⟨φ, Tψ⟩ (polarizationOn_eq_inner): the expectation values of an operator determine all its matrix elements. For a quadratic form Q the polarization is the associated sesquilinear form.

Implementation note: defined for every function Q : D → ℂ; only for a quadratic form is it sesquilinear. The subspace version of Physicslib4.Spectral.polarization.

Blueprint: def:hall-quadratic-form-on-a-subspace (point 2)

Equations

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

structure Physicslib4.Spectral.Unbounded.IsQuadraticFormOn {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {D : Submodule ℂ H} (Q : ↥D → ℂ) : Prop

A function Q on a subspace D of H is a quadratic form: Q(λψ) = |λ|²Q(ψ), and its polarization is sesquilinear.

A quadratic form is the diagonal ψ ↦ L(ψ, ψ) of a sesquilinear form L, the way an expectation value ⟨ψ, Aψ⟩ is the diagonal of the matrix elements ⟨φ, Aψ⟩. The integral of an unbounded function f is first constructed as the quadratic form Q_f(ψ) = ∫ f dμ_ψ on W_f (isQuadraticFormOn_integralForm), and only then as an operator.

Implementation note: no density or closedness of D is assumed. The subspace version of Physicslib4.Spectral.IsQuadraticForm.

Blueprint: def:hall-quadratic-form-on-a-subspace

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

  Homogeneity of degree two: Q(λψ) = |λ|²Q(ψ) for every complex λ and ψ in D.

• isSesquilinear : ∃ (L : SesquilinearFormOn D), ∀ (φ ψ : ↥D), (L φ) ψ = polarizationOn Q φ ψ

  The polarization of Q agrees with some sesquilinear form on D.

structure Physicslib4.Spectral.Unbounded.IsBoundedQuadraticFormOn {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {D : Submodule ℂ H} (Q : ↥D → ℂ) : Prop

A function Q on a subspace D of H is a bounded quadratic form: a quadratic form with |Q(ψ)| ≤ C‖ψ‖² for some constant C.

A bounded quadratic form on all of H is the diagonal of a bounded operator (Physicslib4.Spectral.IsBoundedQuadraticForm.toOperator). For an unbounded f the integral form Q_f is a quadratic form on W_f that is in general not bounded, which is why the integral of f is an unbounded operator.

Implementation note: the subspace version of Physicslib4.Spectral.IsBoundedQuadraticForm; the norm of ψ is that of H.

Blueprint: def:hall-quadratic-form-on-a-subspace (final paragraph)

• isQuadratic : IsQuadraticFormOn Q

  Q is a quadratic form on D.

• bounded : ∃ (C : ℝ), ∀ (ψ : ↥D), ‖Q ψ‖ ≤ C * ‖↑ψ‖ ^ 2

  Boundedness: |Q(ψ)| ≤ C‖ψ‖² for some real C and every ψ in D.

theorem Physicslib4.Spectral.Unbounded.polarizationOn_eq_inner {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {D : Submodule ℂ H} {Q : ↥D → ℂ} (T : ↥D →ₗ[ℂ] H) (hT : ∀ (ψ : ↥D), Q ψ = inner ℂ (↑ψ) (T ψ)) (φ ψ : ↥D) : polarizationOn Q φ ψ = inner ℂ (↑φ) (T ψ)

If a quadratic form on D is induced on the diagonal by a linear map T : D → H, then its polarization is the off-diagonal form (φ, ψ) ↦ ⟪φ, T ψ⟫.

Blueprint reference: prpstn:quadratic-forms-on-a-subspace-properties (Part 1).

theorem Physicslib4.Spectral.Unbounded.polarizationOn_conj_symm {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {D : Submodule ℂ H} {Q : ↥D → ℂ} (hQ : IsQuadraticFormOn Q) (hreal : ∀ (ψ : ↥D), (Q ψ).im = 0) (φ ψ : ↥D) : polarizationOn Q φ ψ = (starRingEnd ℂ) (polarizationOn Q ψ φ)

A real-valued quadratic form on D has conjugate-symmetric polarization.

Blueprint reference: prpstn:quadratic-forms-on-a-subspace-properties (Part 2).

theorem Physicslib4.Spectral.Unbounded.isQuadraticFormOn_restrict {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {D D' : Submodule ℂ H} (h : D' ≤ D) {Q : ↥D → ℂ} (hQ : IsQuadraticFormOn Q) : IsQuadraticFormOn fun (ψ : ↥D') => Q ⟨↑ψ, ⋯⟩

The restriction of a quadratic form to a smaller subspace is again a quadratic form.

Blueprint reference: lmm:restriction-of-quadratic-form.

theorem Physicslib4.Spectral.Unbounded.polarizationOn_restrict {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {D D' : Submodule ℂ H} (h : D' ≤ D) {Q : ↥D → ℂ} (φ ψ : ↥D') : polarizationOn (fun (ξ : ↥D') => Q ⟨↑ξ, ⋯⟩) φ ψ = polarizationOn Q ⟨↑φ, ⋯⟩ ⟨↑ψ, ⋯⟩

Its associated sesquilinear form is the restriction of the original one.

Blueprint reference: lmm:restriction-of-quadratic-form.

Preliminaries on the associated measures

theorem Physicslib4.Spectral.Unbounded.assoc_univ_eq {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) (ψ : H) : (μ.assoc ψ) Set.univ = ENNReal.ofReal (‖ψ‖ ^ 2)

The associated measure μ_ψ has total mass ‖ψ‖²; in particular it is finite.

Blueprint reference: lmm:associated-measure-total-mass.

theorem Physicslib4.Spectral.Unbounded.assoc_le_norm_sq {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) (ψ : H) (E : Set X) : (μ.assoc ψ) E ≤ ENNReal.ofReal (‖ψ‖ ^ 2)

Consequently μ_ψ(E) ≤ ‖ψ‖² for every E.

Blueprint reference: lmm:associated-measure-total-mass.

theorem Physicslib4.Spectral.Unbounded.norm_sq_integral_apply {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {f : X → ℂ} (hf : f ∈ BddMeasurable X) (ψ : H) : ‖(μ.integral f) ψ‖ ^ 2 = ∫ (x : X), ‖f x‖ ^ 2 ∂μ.assoc ψ

The norm identity for the bounded integral: ‖(∫ f dμ) ψ‖² = ∫ |f|² dμ_ψ for bounded measurable f.

Blueprint reference: lmm:norm-identity-bounded-integral.

theorem Physicslib4.Spectral.Unbounded.assoc_compl_eq_zero {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {E : Set X} (hE : MeasurableSet E) {η : H} (hη : η ∈ Set.range ⇑(μ E)) : (μ.assoc η) Eᶜ = 0

If η lies in the range of the projection μ E, then μ_η is concentrated on E.

Blueprint reference: lmm:range-membership-concentrates-measure.

theorem Physicslib4.Spectral.Unbounded.lintegral_assoc_eq_setLIntegral {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {E : Set X} (hE : MeasurableSet E) {η : H} (hη : η ∈ Set.range ⇑(μ E)) (g : X → ENNReal) : ∫⁻ (x : X), g x ∂μ.assoc η = ∫⁻ (x : X) in E, g x ∂μ.assoc η

Hence integrals against μ_η may be computed over E alone.

Blueprint reference: lmm:range-membership-concentrates-measure.

theorem Physicslib4.Spectral.Unbounded.hasSum_apply_of_partition {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) (F : ℕ → Set X) (hF : ∀ (n : ℕ), MeasurableSet (F n)) (hdisj : Pairwise fun (i j : ℕ) => Disjoint (F i) (F j)) (hcover : ⋃ (n : ℕ), F n = Set.univ) (ψ : H) : HasSum (fun (n : ℕ) => (μ (F n)) ψ) ψ

Over a countable measurable partition of X, every vector is the norm-convergent sum of its pieces.

Blueprint reference: lmm:norm-convergent-decomposition (Part 1).

theorem Physicslib4.Spectral.Unbounded.apply_biUnion_eq_sum {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) (F : ℕ → Set X) (hF : ∀ (n : ℕ), MeasurableSet (F n)) (hdisj : Pairwise fun (i j : ℕ) => Disjoint (F i) (F j)) (N : ℕ) (ψ : H) : (μ (⋃ n ∈ Finset.range N, F n)) ψ = ∑ n ∈ Finset.range N, (μ (F n)) ψ

The N-th partial sum of that series is μ (⋃_{n<N} Fₙ) ψ.

Blueprint reference: lmm:norm-convergent-decomposition (Part 2).

Projections: range, kernel, closedness

theorem Physicslib4.Spectral.Unbounded.range_eq_ker_one_sub {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {P : H →L[ℂ] H} (hP : IsStarProjection P) : (↑P).range = (↑(1 - P)).ker

The range of an orthogonal projection is the kernel of 1 - P.

Blueprint reference: lmm:range-of-projection-is-kernel.

theorem Physicslib4.Spectral.Unbounded.mem_range_iff_apply_eq {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {P : H →L[ℂ] H} (hP : IsStarProjection P) (η : H) : η ∈ Set.range ⇑P ↔ P η = η

A vector lies in the range of an orthogonal projection exactly when it is fixed by it.

Blueprint reference: lmm:range-of-projection-is-kernel.

theorem Physicslib4.Spectral.Unbounded.isClosed_range_of_isStarProjection {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {P : H →L[ℂ] H} (hP : IsStarProjection P) : IsClosed (Set.range ⇑P)

The range of an orthogonal projection is closed.

Blueprint reference: lmm:range-of-projection-is-kernel.

theorem Physicslib4.Spectral.Unbounded.completeSpace_and_separableSpace_of_isClosed {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [TopologicalSpace.SeparableSpace H] {K : Submodule ℂ H} (hK : IsClosed ↑K) : CompleteSpace ↥K ∧ TopologicalSpace.SeparableSpace ↥K

A closed subspace of a separable Hilbert space is again a separable Hilbert space: it is complete, and separable. The separability hypothesis on H is the blueprint's standing assumption; the rest of this file does not need it.

Blueprint reference: lmm:closed-subspace-is-hilbert.

Measure-theoretic facts not already in Mathlib

theorem Physicslib4.Spectral.Unbounded.setLIntegral_congr_measure {X : Type u_1} [MeasurableSpace X] {ν ν' : MeasureTheory.Measure X} {E : Set X} (hE : MeasurableSet E) (h : ∀ (S : Set X), MeasurableSet S → S ⊆ E → ν S = ν' S) (g : X → ENNReal) : ∫⁻ (x : X) in E, g x ∂ν = ∫⁻ (x : X) in E, g x ∂ν'

Two measures agreeing on all measurable subsets of E give the same integral over E.

Blueprint reference: prpstn:integrals-agree-when-measures-agree.

The unbounded integral

theorem Physicslib4.Spectral.Unbounded.assoc_apply_eq_norm_sq {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) (ψ : H) {E : Set X} (hE : MeasurableSet E) : (μ.assoc ψ) E = ENNReal.ofReal (‖(μ E) ψ‖ ^ 2)

On a measurable set E, the associated measure is μ_ψ(E) = ‖μ(E) ψ‖².

theorem Physicslib4.Spectral.Unbounded.assoc_add_le {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) (φ ψ : H) : μ.assoc (φ + ψ) ≤ 2 • (μ.assoc φ + μ.assoc ψ)

The associated measure of a sum: μ_{φ+ψ} ≤ 2 (μ_φ + μ_ψ).

theorem Physicslib4.Spectral.Unbounded.assoc_smul {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) (c : ℂ) (ψ : H) : μ.assoc (c • ψ) = ENNReal.ofReal (‖c‖ ^ 2) • μ.assoc ψ

The associated measure of a multiple: μ_{cψ} = |c|² μ_ψ.

theorem Physicslib4.Spectral.Unbounded.assoc_zero {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) : μ.assoc 0 = 0

The associated measure of the zero vector is zero.

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

The domain W_f = {ψ ∈ H : ∫ |f|² dμ_ψ < ∞} of the integral of a function f against a projection-valued measure μ.

Here μ_ψ(E) = ⟨ψ, μ(E)ψ⟩ is the measure of ψ, a probability distribution when ‖ψ‖ = 1. If μ is the spectral measure of an observable A, the integral of f plays the role of f(A), and W_f is the set of ψ on which it is defined; there ‖(∫ f dμ)ψ‖² = ∫ |f|² dμ_ψ (norm_sq_pmapIntegral). For f(λ) = λ the condition says that the distribution of measured values of A in the state ψ has a finite second moment ∫ λ² dμ_ψ. For bounded measurable f, W_f = H (integralDomain_eq_top_of_bddMeasurable); for measurable f, W_f is dense (dense_integralDomain).

Implementation note: membership is Mathlib's MemLp f 2 (μ.assoc ψ) (mem_integralDomain), which also asks f to be almost everywhere strongly measurable for μ_ψ; for measurable f this holds automatically and the condition is ∫ |f|² dμ_ψ < ∞. The domain is a submodule because μ_(φ+ψ) ≤ 2(μ_φ + μ_ψ) (assoc_add_le) and μ_(cψ) = |c|²μ_ψ (assoc_smul).

Blueprint: prpstn:hall-10.2

Equations

• Physicslib4.Spectral.Unbounded.integralDomain μ f = { carrier := {ψ : H | MeasureTheory.MemLp f 2 (μ.assoc ψ)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem Physicslib4.Spectral.Unbounded.mem_integralDomain {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {f : X → ℂ} {ψ : H} : ψ ∈ integralDomain μ f ↔ MeasureTheory.MemLp f 2 (μ.assoc ψ)

noncomputable def Physicslib4.Spectral.Unbounded.integralForm {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) (f : X → ℂ) (ψ : ↥(integralDomain μ f)) : ℂ

The function Q_f(ψ) = ∫ f dμ_ψ on the domain W_f: the would-be expectation value ⟨ψ, (∫ f dμ)ψ⟩.

In the spectral picture, Q_f(ψ) is the expectation value of f(A) in the state ψ, the average of f over the distribution μ_ψ of measured values. For measurable f it is a quadratic form on W_f (isQuadraticFormOn_integralForm), and its polarization L_f defines the operator: (∫ f dμ)ψ is the vector χ with L_f(φ, ψ) = ⟨φ, χ⟩ for all φ in W_f (existsUnique_repr_integralForm). For ψ in W_f the function f is μ_ψ-integrable, being square-integrable for a finite measure.

Implementation note: the integral is Mathlib's Bochner integral against the measure μ.assoc ψ, which is 0 when f is not integrable.

Blueprint: prpstn:hall-10.2 (Part 1)

Equations

• Physicslib4.Spectral.Unbounded.integralForm μ f ψ = ∫ (x : X), f x ∂μ.assoc ↑ψ

theorem Physicslib4.Spectral.Unbounded.dense_integralDomain {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {f : X → ℂ} (hf : Measurable f) : Dense ↑(integralDomain μ f)

W_f is dense in H.

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

theorem Physicslib4.Spectral.Unbounded.indicator_lt_mem_bddMeasurable {X : Type u_1} [MeasurableSpace X] {f : X → ℂ} (hf : Measurable f) (n : ℕ) : {x : X | ‖f x‖ < ↑n}.indicator f ∈ BddMeasurable X

The truncation f · 1_{|f| < n} of a measurable f is bounded and measurable.

theorem Physicslib4.Spectral.Unbounded.tendsto_integral_trunc_assoc {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {f : X → ℂ} (hf : Measurable f) {ψ : H} (hψ : ψ ∈ integralDomain μ f) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : X), {x : X | ‖f x‖ < ↑n}.indicator f x ∂μ.assoc ψ) Filter.atTop (nhds (∫ (x : X), f x ∂μ.assoc ψ))

For ψ ∈ W_f, ∫ f · 1_{|f| < n} dμ_ψ → ∫ f dμ_ψ (dominated convergence).

theorem Physicslib4.Spectral.Unbounded.tendsto_integral_trunc_apply {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {f : X → ℂ} (hf : Measurable f) {ψ : H} (hψ : ψ ∈ integralDomain μ f) : ∃ (χ : H), Filter.Tendsto (fun (n : ℕ) => (μ.integral ({x : X | ‖f x‖ < ↑n}.indicator f)) ψ) Filter.atTop (nhds χ)

For ψ ∈ W_f, the vectors (∫ f · 1_{|f| < n} dμ) ψ converge in H: their differences are controlled by the tails ∫_{|f| ≥ N} |f|² dμ_ψ → 0.

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

theorem Physicslib4.Spectral.Unbounded.exists_linearMap_integralForm_eq_inner {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {f : X → ℂ} (hf : Measurable f) : ∃ (T : ↥(integralDomain μ f) →ₗ[ℂ] H), (∀ (ψ : ↥(integralDomain μ f)), Filter.Tendsto (fun (n : ℕ) => (μ.integral ({x : X | ‖f x‖ < ↑n}.indicator f)) ↑ψ) Filter.atTop (nhds (T ψ))) ∧ ∀ (ψ : ↥(integralDomain μ f)), integralForm μ f ψ = inner ℂ (↑ψ) (T ψ)

There is a linear map T : W_f → H, the pointwise limit of the truncated integrals, which induces Q_f on the diagonal: Q_f(ψ) = ⟪ψ, T ψ⟫.

Blueprint reference: prpstn:hall-10.2 (Parts 1 and 3).

theorem Physicslib4.Spectral.Unbounded.isQuadraticFormOn_integralForm {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {f : X → ℂ} (hf : Measurable f) : IsQuadraticFormOn (integralForm μ f)

Q_f is a quadratic form on W_f.

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

theorem Physicslib4.Spectral.Unbounded.norm_polarizationOn_integralForm_le {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {f : X → ℂ} (hf : Measurable f) (φ ψ : ↥(integralDomain μ f)) : ‖polarizationOn (integralForm μ f) φ ψ‖ ≤ ‖↑φ‖ * √(∫ (x : X), ‖f x‖ ^ 2 ∂μ.assoc ↑ψ)

The associated sesquilinear form L_f obeys |L_f(φ, ψ)| ≤ ‖φ‖ ‖f‖_{L²(μ_ψ)}.

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

theorem Physicslib4.Spectral.Unbounded.existsUnique_repr_integralForm {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {f : X → ℂ} (hf : Measurable f) (ψ : ↥(integralDomain μ f)) : ∃! χ : H, ∀ (φ : ↥(integralDomain μ f)), polarizationOn (integralForm μ f) φ ψ = inner ℂ (↑φ) χ

For each ψ ∈ W_f there is a unique χ ∈ H representing φ ↦ L_f(φ, ψ).

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

noncomputable def Physicslib4.Spectral.Unbounded.integralApply {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) (f : X → ℂ) (ψ : ↥(integralDomain μ f)) : H

The action ψ ↦ (∫ f dμ)ψ of the integral on W_f: the unique vector χ with L_f(φ, ψ) = ⟨φ, χ⟩ for every φ in W_f.

Here L_f is the polarization of Q_f, so χ is fixed by its matrix elements against the dense subspace W_f. For measurable f such a χ exists and is unique (existsUnique_repr_integralForm): it is the limit of the bounded integrals of the truncations f·1_(|f| < n) (tendsto_integral_truncation).

Implementation note: the value is 0 when f is not measurable or no unique χ exists. The measurability guard makes pmapIntegral linear by a direct argument, without a hypothesis; every result about the values of pmapIntegral assumes f measurable.

Blueprint: prpstn:hall-10.1

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Physicslib4.Spectral.Unbounded.pmapIntegral {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) (f : X → ℂ) : H →ₗ.[ℂ] H

The integral ∫ f dμ of a possibly unbounded function f against a projection-valued measure μ, as an unbounded operator with domain W_f.

The unbounded spectral theorem writes a self-adjoint A as A = ∫ λ dμ(λ) for a unique μ (existsUnique_spectralMeasure_unbounded), and the functional calculus f(A) is ∫ f dμ for that μ (functionalCalculus). For measurable f the integral is characterised by ⟨ψ, (∫ f dμ)ψ⟩ = ∫ f dμ_ψ on W_f (inner_self_pmapIntegral), and any operator with domain W_f satisfying this identity equals it (eq_pmapIntegral_of_inner_self). It obeys ‖(∫ f dμ)ψ‖² = ∫ |f|² dμ_ψ (norm_sq_pmapIntegral), agrees with the bounded integral ProjectionValuedMeasure.integral for bounded measurable f (pmapIntegral_of_bddMeasurable), and is self-adjoint for real-valued measurable f (isSelfAdjoint_pmapIntegral_of_real).

Implementation note: a LinearPMap with domain integralDomain μ f and action integralApply μ f, which is 0 for non-measurable f.

Blueprint: prpstn:hall-10.1

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Physicslib4.Spectral.Unbounded.pmapIntegral_domain {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) (f : X → ℂ) : (pmapIntegral μ f).domain = integralDomain μ f

theorem Physicslib4.Spectral.Unbounded.inner_pmapIntegral {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {f : X → ℂ} (hf : Measurable f) (φ ψ : ↥(integralDomain μ f)) : inner ℂ (↑φ) (↑(pmapIntegral μ f) ψ) = polarizationOn (integralForm μ f) φ ψ

The defining off-diagonal identity ⟪φ, (∫ f dμ) ψ⟫ = L_f(φ, ψ).

Blueprint reference: prpstn:hall-10.1.

theorem Physicslib4.Spectral.Unbounded.inner_self_pmapIntegral {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {f : X → ℂ} (hf : Measurable f) (ψ : ↥(integralDomain μ f)) : inner ℂ (↑ψ) (↑(pmapIntegral μ f) ψ) = ∫ (x : X), f x ∂μ.assoc ↑ψ

The diagonal identity ⟪ψ, (∫ f dμ) ψ⟫ = ∫ f dμ_ψ.

Blueprint reference: prpstn:hall-10.1.

theorem Physicslib4.Spectral.Unbounded.tendsto_integral_truncation {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {f : X → ℂ} (hf : Measurable f) (ψ : ↥(integralDomain μ f)) : Filter.Tendsto (fun (n : ℕ) => (μ.integral ({x : X | ‖f x‖ < ↑n}.indicator f)) ↑ψ) Filter.atTop (nhds (↑(pmapIntegral μ f) ψ))

The bounded truncations f · 1_{|f| < n} converge to ∫ f dμ pointwise in H.

Blueprint reference: lmm:truncations-converge.

theorem Physicslib4.Spectral.Unbounded.norm_sq_pmapIntegral {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {f : X → ℂ} (hf : Measurable f) (ψ : ↥(integralDomain μ f)) : ‖↑(pmapIntegral μ f) ψ‖ ^ 2 = ∫ (x : X), ‖f x‖ ^ 2 ∂μ.assoc ↑ψ

The norm formula ‖(∫ f dμ) ψ‖² = ∫ |f|² dμ_ψ.

Blueprint reference: prpstn:hall-10.1.

theorem Physicslib4.Spectral.Unbounded.eq_pmapIntegral_of_inner_self {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {f : X → ℂ} (hf : Measurable f) (A : H →ₗ.[ℂ] H) (hdom : A.domain = integralDomain μ f) (h : ∀ (ψ : ↥A.domain), inner ℂ (↑ψ) (↑A ψ) = ∫ (x : X), f x ∂μ.assoc ↑ψ) : A = pmapIntegral μ f

Strengthened uniqueness: any unbounded operator with domain W_f satisfying merely the diagonal identity equals ∫ f dμ.

Blueprint reference: prpstn:hall-10.1.

theorem Physicslib4.Spectral.Unbounded.integralDomain_eq_top_of_bddMeasurable {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {f : X → ℂ} (hf : f ∈ BddMeasurable X) : integralDomain μ f = ⊤

For bounded measurable f, W_f = H.

Blueprint reference: prpstn:coincidence-with-the-bounded-integral.

theorem Physicslib4.Spectral.Unbounded.pmapIntegral_of_bddMeasurable {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {f : X → ℂ} (hf : f ∈ BddMeasurable X) : pmapIntegral μ f = (↑(μ.integral f)).toPMap ⊤

For bounded measurable f, the unbounded integral is the bounded one.

Blueprint reference: prpstn:coincidence-with-the-bounded-integral.

theorem Physicslib4.Spectral.Unbounded.integralDomain_congr_of_null {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {f g : X → ℂ} {N : Set X} (hN : MeasurableSet N) (hμN : μ N = 0) (hfg : ∀ x ∉ N, f x = g x) : integralDomain μ f = integralDomain μ g

If f and g agree off a set annihilated by μ, they have the same domain.

Blueprint reference: lmm:integral-ignores-null-sets.

theorem Physicslib4.Spectral.Unbounded.pmapIntegral_congr_of_null {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {f g : X → ℂ} (hf : Measurable f) (hg : Measurable g) {N : Set X} (hN : MeasurableSet N) (hμN : μ N = 0) (hfg : ∀ x ∉ N, f x = g x) : pmapIntegral μ f = pmapIntegral μ g

If f and g agree off a set annihilated by μ, they have the same integral.

Blueprint reference: lmm:integral-ignores-null-sets.

theorem Physicslib4.Spectral.Unbounded.range_subset_integralDomain {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {f : X → ℂ} (hf : Measurable f) {E : Set X} (hE : MeasurableSet E) {c : ℝ} (hc : ∀ x ∈ E, ‖f x‖ ≤ c) : Set.range ⇑(μ E) ⊆ ↑(integralDomain μ f)

If |f| ≤ c on E, then the range of μ E lies in W_f.

Blueprint reference: lmm:bounded-on-set-range-in-domain.

theorem Physicslib4.Spectral.Unbounded.integral_norm_sq_le_of_mem_range {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {f : X → ℂ} (hf : Measurable f) {E : Set X} (hE : MeasurableSet E) {c : ℝ} (hc : ∀ x ∈ E, ‖f x‖ ≤ c) {η : H} (hη : η ∈ Set.range ⇑(μ E)) : ∫ (x : X), ‖f x‖ ^ 2 ∂μ.assoc η ≤ c ^ 2 * ‖η‖ ^ 2

The quantitative half of lmm:bounded-on-set-range-in-domain.

Blueprint reference: lmm:bounded-on-set-range-in-domain.

theorem Physicslib4.Spectral.Unbounded.assoc_integral_apply {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {h : X → ℂ} (hh : h ∈ BddMeasurable X) (ψ : H) {E : Set X} (hE : MeasurableSet E) : (μ.assoc ((μ.integral h) ψ)) E = ∫⁻ (x : X) in E, ↑‖h x‖₊ ^ 2 ∂μ.assoc ψ

For bounded measurable h and T = ∫ h dμ, the associated measure of T ψ has density |h|² with respect to μ_ψ.

Blueprint reference: lmm:associated-measure-of-image.

theorem Physicslib4.Spectral.Unbounded.lintegral_assoc_integral_apply {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {h : X → ℂ} (hh : h ∈ BddMeasurable X) (ψ : H) {g : X → ENNReal} (hg : Measurable g) : ∫⁻ (x : X), g x ∂μ.assoc ((μ.integral h) ψ) = ∫⁻ (x : X), g x * ↑‖h x‖₊ ^ 2 ∂μ.assoc ψ

Consequently integrals against μ_{Tψ} are integrals against μ_ψ weighted by |h|².

Blueprint reference: lmm:associated-measure-of-image.

theorem Physicslib4.Spectral.Unbounded.mapsTo_pmapIntegral_range {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {f : X → ℂ} (hf : Measurable f) {E : Set X} (hE : MeasurableSet E) {c : ℝ} (_hc : ∀ x ∈ E, ‖f x‖ ≤ c) (ψ : ↥(integralDomain μ f)) (hψ : ↑ψ ∈ Set.range ⇑(μ E)) : ↑(pmapIntegral μ f) ψ ∈ Set.range ⇑(μ E)

If f is bounded on E, then ∫ f dμ preserves the spectral subspace V_E = Range(μ E) (which lies in W_f by range_subset_integralDomain).

Blueprint reference: lmm:integral-preserves-spectral-subspaces.

theorem Physicslib4.Spectral.Unbounded.isSymmetric_pmapIntegral_of_real {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {f : X → ℂ} (hf : Measurable f) (hreal : ∀ (x : X), (f x).im = 0) : IsSymmetric (pmapIntegral μ f)

For real-valued measurable f, the integral ∫ f dμ is symmetric on W_f.

Blueprint reference: prpstn:hall-10.3.

theorem Physicslib4.Spectral.Unbounded.pmapIntegral_sub_smul_integral_inv {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {f : X → ℂ} (hf : Measurable f) (hreal : ∀ (x : X), (f x).im = 0) {c : ℂ} (hc : c.im ≠ 0) (η : H) : ∃ (hψ : (μ.integral fun (x : X) => (f x - c)⁻¹) η ∈ integralDomain μ f), ↑(pmapIntegral μ f) ⟨(μ.integral fun (x : X) => (f x - c)⁻¹) η, hψ⟩ - c • (μ.integral fun (x : X) => (f x - c)⁻¹) η = η

For real measurable f and non-real c, the bounded operator ∫ (f - c)⁻¹ dμ is a right inverse of ∫ f dμ - c 1: it maps into W_f and (∫ f dμ - c)(∫ (f - c)⁻¹ dμ) η = η.

Blueprint reference: prpstn:hall-10.3; also Step 1 of the uniqueness proof of thrm:hall-10.4.

theorem Physicslib4.Spectral.Unbounded.range_subSmul_pmapIntegral_eq_top {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {f : X → ℂ} (hf : Measurable f) (hreal : ∀ (x : X), (f x).im = 0) {c : ℂ} (hc : c.im ≠ 0) : range (subSmul (pmapIntegral μ f) c) = ⊤

For real-valued measurable f and non-real c, the operator ∫ f dμ - c 1 maps W_f onto H: a preimage of η is (∫ (f - c)⁻¹ dμ) η.

Blueprint reference: prpstn:hall-10.3.

theorem Physicslib4.Spectral.Unbounded.isSelfAdjoint_pmapIntegral_of_real {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {f : X → ℂ} (hf : Measurable f) (hreal : ∀ (x : X), (f x).im = 0) : IsSelfAdjoint (pmapIntegral μ f)

The integral ∫ f dμ of a real-valued measurable function f is a self-adjoint operator on W_f.

This is the unbounded counterpart of the fact that a real function of an observable is again an observable. It is what makes ∫ λ dμ(λ) self-adjoint in the unbounded spectral theorem. The proof shows that ∫ f dμ is symmetric (isSymmetric_pmapIntegral_of_real) and that ∫ f dμ − c𝟙 maps W_f onto H for non-real c (range_subSmul_pmapIntegral_eq_top), with the bounded integral of 1/(f − c) as a right inverse.

Implementation note: real-valuedness is the hypothesis that f has imaginary part 0 everywhere.

Blueprint: prpstn:hall-10.3