Physicslib4.Spectral.OperatorIntegral

Integration of bounded measurable functions against a projection-valued measure

Given a projection-valued measure μ on a measurable space X with values in 𝓑(H), every bounded measurable f : X → ℂ has an operator-valued integral ∫ f dμ ∈ 𝓑(H), characterised by ⟪ψ, (∫ f dμ) ψ⟫ = ∫ f dμ_ψ for every ψ ∈ H.

Main definitions

• Physicslib4.Spectral.ProjectionValuedMeasure.integral — the operator-valued integral f ↦ ∫ f dμ, extended by 0 to arbitrary functions.

The class of admissible integrands is Physicslib4.Spectral.BddMeasurable, defined in Physicslib4/Spectral/Basic.lean; every statement below takes f ∈ BddMeasurable X rather than a Measurable f/bounded hypothesis pair.

Main statements

• Physicslib4.Spectral.ProjectionValuedMeasure.existsUnique_integral — existence and uniqueness of the operator-valued integral as a linear map.
• Physicslib4.Spectral.ProjectionValuedMeasure.integral_add, Physicslib4.Spectral.ProjectionValuedMeasure.integral_smul — linearity of f ↦ ∫ f dμ.
• Physicslib4.Spectral.ProjectionValuedMeasure.integral_indicator — the integral of an indicator is the corresponding projection.
• Physicslib4.Spectral.ProjectionValuedMeasure.norm_integral_le — the integral is bounded by the supremum norm of the integrand.
• Physicslib4.Spectral.ProjectionValuedMeasure.integral_mul — multiplicativity.
• Physicslib4.Spectral.ProjectionValuedMeasure.integral_conj — compatibility with conjugation and the adjoint.

Supporting lemmas

• Physicslib4.Spectral.isSelfAdjoint_integral_of_real — the integral of a real-valued integrand is self-adjoint, the second part of prpstn:integral-conjugation.

The quadratic forms behind the construction

theorem Physicslib4.Spectral.ProjectionValuedMeasure.isBoundedQuadraticForm_integral_indicator {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) : IsBoundedQuadraticForm fun (ψ : H) => ∫ (x : X), E.indicator 1 x ∂μ.assoc ψ

For an indicator function Q_{1_E} is a bounded quadratic form.

Blueprint reference: prpstn:Q-indicator-bounded-form (first part).

theorem Physicslib4.Spectral.ProjectionValuedMeasure.norm_integral_indicator_le {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) : ‖∫ (x : X), E.indicator 1 x ∂μ.assoc ψ‖ ≤ ‖ψ‖ ^ 2

For an indicator function Q_{1_E} is bounded with constant 1.

Blueprint reference: prpstn:Q-indicator-bounded-form (second part).

theorem Physicslib4.Spectral.ProjectionValuedMeasure.isBoundedQuadraticForm_integral_simpleFunc {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) (s : MeasureTheory.SimpleFunc X ℂ) : IsBoundedQuadraticForm fun (ψ : H) => ∫ (x : X), s x ∂μ.assoc ψ

For a simple function the quadratic form Q_s is a bounded quadratic form.

Blueprint reference: prpstn:Q-simple-bounded-form.

theorem Physicslib4.Spectral.ProjectionValuedMeasure.isBoundedQuadraticForm_integral_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) : IsBoundedQuadraticForm fun (ψ : H) => ∫ (x : X), f x ∂μ.assoc ψ

For a bounded measurable f the quadratic form Q_f is a bounded quadratic form.

This is the third and last stage of the argument summarised by isBoundedQuadraticForm_integral: it is obtained from isBoundedQuadraticForm_integral_simpleFunc by uniform approximation.

Blueprint reference: prpstn:Q-measurable-bounded-form.

theorem Physicslib4.Spectral.ProjectionValuedMeasure.isBoundedQuadraticForm_integral {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) : IsBoundedQuadraticForm fun (ψ : H) => ∫ (x : X), f x ∂μ.assoc ψ

For a bounded measurable f, the map Q_f : ψ ↦ ∫ f dμ_ψ is a bounded quadratic form on H.

This is the summary statement of the three-stage argument: indicator functions in isBoundedQuadraticForm_integral_indicator, simple functions in isBoundedQuadraticForm_integral_simpleFunc, and general bounded measurable functions in isBoundedQuadraticForm_integral_bddMeasurable, which is the stage that carries the whole statement and so discharges this node.

Blueprint reference: lmm:lemma1-of-operator-valued-integration.

theorem Physicslib4.Spectral.ProjectionValuedMeasure.existsUnique_integral {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) : ∃! T : ↥(BddMeasurable X) →ₗ[ℂ] H →L[ℂ] H, ∀ (f : ↥(BddMeasurable X)) (ψ : H), inner ℂ ψ ((T f) ψ) = ∫ (x : X), ↑f x ∂μ.assoc ψ

Operator-valued integration. There is a unique linear map from the space of bounded measurable complex-valued functions on X into 𝓑(H), written f ↦ ∫ f dμ, such that ⟪ψ, (∫ f dμ) ψ⟫ = ∫ f dμ_ψ for every f and every ψ ∈ H.

Blueprint reference: thrm:operator-valued-integration.

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

The operator-valued integral ∫ f dμ of a bounded measurable f : X → ℂ against a projection-valued measure μ.

It is the bounded operator with ⟨ψ, (∫ f dμ)ψ⟩ = ∫ f dμ_ψ for every vector ψ (inner_integral), where μ_ψ(E) = ⟨ψ, μ(E)ψ⟩. For a step function f = Σ c_k 1_(E_k) it is Σ c_k μ(E_k), and in general a norm limit of such sums; the spectral theorem writes a self-adjoint operator as A = ∫ λ dμ^A(λ). The integral of 1_E is μ(E) (integral_indicator), it is linear (integral_add, integral_smul) and multiplicative (integral_mul), satisfies ‖∫ f dμ‖ ≤ sup |f| (norm_integral_le), and sends the complex conjugate f̄ to the adjoint (integral_conj).

Implementation note: the operator is chosen from the unique linear map of existsUnique_integral, built from the bounded quadratic form Q_f(ψ) = ∫ f dμ_ψ, so linearity is recovered by integral_add and integral_smul rather than definitional. On functions that are not bounded and measurable the integral is defined to be 0, so it is a total function.

Blueprint: the integral ∫ f dμ of thrm:operator-valued-integration

Equations

• μ.integral f = if h : f ∈ Physicslib4.Spectral.BddMeasurable X then (Exists.choose ⋯) ⟨f, h⟩ else 0

theorem Physicslib4.Spectral.ProjectionValuedMeasure.inner_integral {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) : inner ℂ ψ ((μ.integral f) ψ) = ∫ (x : X), f x ∂μ.assoc ψ

Linearity of the integral

integral is defined through Exists.choose applied to existsUnique_integral, so its linearity in the integrand is not definitional. The two computation rules below recover it, and are what the vector-space arguments elsewhere in the directory consume.

theorem Physicslib4.Spectral.ProjectionValuedMeasure.integral_add {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {f g : X → ℂ} (hf : f ∈ BddMeasurable X) (hg : g ∈ BddMeasurable X) : μ.integral (f + g) = μ.integral f + μ.integral g

Additivity of the operator-valued integral.

theorem Physicslib4.Spectral.ProjectionValuedMeasure.integral_smul {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) : μ.integral (α • f) = α • μ.integral f

Homogeneity of the operator-valued integral.

Basic properties of the operator-valued integral

theorem Physicslib4.Spectral.ProjectionValuedMeasure.integral_indicator {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) : μ.integral (E.indicator 1) = μ E

The integral of an indicator function is the corresponding projection.

Blueprint reference: prpstn:integral-of-indicator (first part).

theorem Physicslib4.Spectral.ProjectionValuedMeasure.integral_one {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) : μ.integral 1 = 1

The integral of the constant function 1 is the identity operator.

This is integral_indicator at E = Set.univ, together with the field univ' of ProjectionValuedMeasure.

Blueprint reference: prpstn:integral-of-indicator (second part).

theorem Physicslib4.Spectral.ProjectionValuedMeasure.norm_integral_simple_le {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) (s : MeasureTheory.SimpleFunc X ℂ) : ‖μ.integral fun (x : X) => s x‖ ≤ ⨆ (x : X), ‖s x‖

The norm bound for the integral of a simple function.

This is the special case of norm_integral_le for a simple integrand; it is kept as a separate declaration only because the blueprint proves the general bound by reducing to it.

The blueprint spells the integrand as ∑ᵢ cᵢ 1_{Eᵢ} for a finite measurable family E that is pairwise disjoint and covers X. Here it is a MeasureTheory.SimpleFunc X ℂ, matching the sibling statements isBoundedQuadraticForm_integral_simpleFunc and integral_simpleFunc_mul: a simple function is canonically of that form, over the pairwise disjoint fibres s ⁻¹' {c}, which cover X. So no generality is gained or lost.

Blueprint reference: prpstn:integral-norm-bound-simple.

theorem Physicslib4.Spectral.ProjectionValuedMeasure.norm_integral_le {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) : ‖μ.integral f‖ ≤ ⨆ (x : X), ‖f x‖

The operator norm of ∫ f dμ is bounded by the supremum norm of f.

Blueprint reference: prpstn:integral-norm-bound.

theorem Physicslib4.Spectral.ProjectionValuedMeasure.tendsto_integral_of_tendstoUniformly {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) {s : ℕ → MeasureTheory.SimpleFunc X ℂ} (hs : TendstoUniformly (fun (n : ℕ) (x : X) => (s n) x) f Filter.atTop) : Filter.Tendsto (fun (n : ℕ) => μ.integral fun (x : X) => (s n) x) Filter.atTop (nhds (μ.integral f))

If simple functions sᵢ converge uniformly to a bounded measurable f, then the operators ∫ sᵢ dμ converge in operator norm to ∫ f dμ.

The blueprint also asserts that ∫ sᵢ dμ is a Cauchy sequence; that is Filter.Tendsto.cauchySeq applied to the conclusion below, so it is not restated.

Blueprint reference: prpstn:integral-as-limit-of-simple.

theorem Physicslib4.Spectral.ProjectionValuedMeasure.integral_indicator_mul {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {E F : Set X} (hE : MeasurableSet E) (hF : MeasurableSet F) : μ.integral (E.indicator 1 * F.indicator 1) = μ.integral (E.indicator 1) * μ.integral (F.indicator 1)

Multiplicativity of the integral on indicator functions.

Blueprint reference: prpstn:integral-mult-indicator.

theorem Physicslib4.Spectral.ProjectionValuedMeasure.integral_simpleFunc_mul {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) (s r : MeasureTheory.SimpleFunc X ℂ) : (μ.integral fun (x : X) => s x * r x) = (μ.integral fun (x : X) => s x) * μ.integral fun (x : X) => r x

Multiplicativity of the integral on simple functions.

Blueprint reference: prpstn:integral-mult-simple.

theorem Physicslib4.Spectral.ProjectionValuedMeasure.integral_bddMeasurable_mul {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {f g : X → ℂ} (hf : f ∈ BddMeasurable X) (hg : g ∈ BddMeasurable X) : μ.integral (f * g) = μ.integral f * μ.integral g

Multiplicativity of the integral on bounded measurable functions.

This is the third and last stage of the argument summarised by integral_mul: it is obtained from integral_simpleFunc_mul by uniform approximation, using tendstoUniformly_mul_of_bounded and tendsto_integral_of_tendstoUniformly.

Blueprint reference: prpstn:integral-mult-measurable.

theorem Physicslib4.Spectral.ProjectionValuedMeasure.integral_mul {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H) {f g : X → ℂ} (hf : f ∈ BddMeasurable X) (hg : g ∈ BddMeasurable X) : μ.integral (f * g) = μ.integral f * μ.integral g

Multiplicativity of the operator-valued integral.

This is the summary statement of the three-stage argument: indicator functions in integral_indicator_mul, simple functions in integral_simpleFunc_mul, and general bounded measurable functions in integral_bddMeasurable_mul, which is the stage that carries the whole statement and so discharges this node.

Blueprint reference: prpstn:integral-multiplicative.

theorem Physicslib4.Spectral.ProjectionValuedMeasure.integral_conj {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) : (μ.integral fun (x : X) => (starRingEnd ℂ) (f x)) = ContinuousLinearMap.adjoint (μ.integral f)

The integral of the complex conjugate of f is the adjoint of the integral of f.

Blueprint reference: prpstn:integral-conjugation (first part).

theorem Physicslib4.Spectral.ProjectionValuedMeasure.isSelfAdjoint_integral_of_real {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) (hreal : ∀ (x : X), (f x).im = 0) : IsSelfAdjoint (μ.integral f)

The integral of a real-valued function is self-adjoint.

Blueprint reference: prpstn:integral-conjugation (second part).

theorem Physicslib4.Spectral.tendstoUniformly_mul_of_bounded {Y : Type u_3} {f g : Y → ℂ} (hf : ∃ (C : ℝ), ∀ (x : Y), ‖f x‖ ≤ C) {s r : ℕ → Y → ℂ} (hs : TendstoUniformly s f Filter.atTop) (hr : TendstoUniformly r g Filter.atTop) (hrb : ∀ (j : ℕ), ∃ (C : ℝ), ∀ (x : Y), ‖r j x‖ ≤ C) : TendstoUniformly (fun (p : ℕ × ℕ) (x : Y) => s p.1 x * r p.2 x) (f * g) (Filter.atTop ×ˢ Filter.atTop)

Uniform convergence is preserved by products of uniformly bounded sequences: if sᵢ → f and rⱼ → g uniformly with each rⱼ bounded, then sᵢ rⱼ → f g uniformly as i, j → ∞.

The blueprint's boundedness assumption on g is not stated: it follows from hr together with hrb.

Blueprint reference: prpstn:products-converge-uniformly.