Unbounded spectral integration

This file extends the bounded spectral integral to unbounded measurable functions by a monotone-limit construction, giving the partial operator E_pvm.unboundedIntegral f hf for a PVM E_pvm and measurable f.

def PVM.scalarContent {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (x : E) (S : Set ℝ) : ℝ

The nonnegative scalar set function induced by a PVM and a vector.

Equations

• E_pvm.scalarContent x S = (inner ℂ ((E_pvm.proj S) x) x).re

theorem PVM.scalarContent_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (x : E) (S : Set ℝ) (hS : MeasurableSet S) : 0 ≤ E_pvm.scalarContent x S

Scalar PVM content is nonnegative for measurable sets.

theorem PVM.scalarContent_empty {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (x : E) : E_pvm.scalarContent x ∅ = 0

Scalar PVM content vanishes on the empty set.

theorem PVM.scalarContent_union {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (x : E) {S T : Set ℝ} (hS : MeasurableSet S) (hT : MeasurableSet T) (hdisj : Disjoint S T) : E_pvm.scalarContent x (S ∪ T) = E_pvm.scalarContent x S + E_pvm.scalarContent x T

Scalar PVM content is additive on disjoint measurable sets.

theorem PVM.scalarContent_countably_additive_tendsto {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (x : E) (S : ℕ → Set ℝ) (hmeas : ∀ (i : ℕ), MeasurableSet (S i)) (hpair : Pairwise (Function.onFun Disjoint S)) : Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, E_pvm.scalarContent x (S i)) Filter.atTop (nhds (E_pvm.scalarContent x (⋃ (i : ℕ), S i)))

Strong countable additivity of a PVM implies scalar countable-additivity convergence.

noncomputable def PVM.scalarMeasure {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (x : E) : MeasureTheory.Measure ℝ

The finite positive measure obtained by evaluating the PVM at a vector.

Equations

• E_pvm.scalarMeasure x = MeasureTheory.Measure.ofMeasurable (fun (S : Set ℝ) (x_1 : MeasurableSet S) => ENNReal.ofReal (E_pvm.scalarContent x S)) ⋯ ⋯

theorem PVM.scalarMeasure_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (x : E) (S : Set ℝ) (hS : MeasurableSet S) : (E_pvm.scalarMeasure x) S = ENNReal.ofReal (E_pvm.scalarContent x S)

On measurable sets, the scalar measure agrees with the PVM quadratic form.

theorem PVM.scalarContent_eq_norm_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (x : E) (S : Set ℝ) (hS : MeasurableSet S) : E_pvm.scalarContent x S = ‖(E_pvm.proj S) x‖ ^ 2

Scalar PVM content is the squared norm of the projected vector.

theorem PVM.scalarMeasure_univ {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (x : E) : (E_pvm.scalarMeasure x) Set.univ = ENNReal.ofReal (‖x‖ ^ 2)

The total mass of the scalar measure is the squared norm of its vector.

theorem PVM.scalarMeasure_lt_top {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (x : E) (S : Set ℝ) : (E_pvm.scalarMeasure x) S < ⊤

Every set has finite scalar measure.

instance PVM.scalarMeasure_isFiniteMeasure {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (x : E) : MeasureTheory.IsFiniteMeasure (E_pvm.scalarMeasure x)

Scalar PVM measures are finite measures.

theorem PVM.inner_simpleIntegral_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (f : MeasureTheory.SimpleFunc ℝ ℂ) (x : E) : inner ℂ x ((E_pvm.simpleIntegral f) x) = ∫ (t : ℝ), f t ∂E_pvm.scalarMeasure x

Diagonal matrix coefficients of simple spectral integrals are scalar integrals.

theorem PVM.inner_integral_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (f : ℝ → ℂ) (hf : Measurable f) (hbdd : ∃ (C : ℝ), ∀ (t : ℝ), ‖f t‖ ≤ C) (x : E) : inner ℂ x ((E_pvm.integral f hf hbdd) x) = ∫ (t : ℝ), f t ∂E_pvm.scalarMeasure x

Diagonal matrix coefficients of bounded measurable spectral integrals are scalar integrals.

theorem PVM.ofReal_norm_sq_simpleIntegral {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (f : MeasureTheory.SimpleFunc ℝ ℂ) (x : E) : ENNReal.ofReal (‖(E_pvm.simpleIntegral f) x‖ ^ 2) = ∫⁻ (t : ℝ), ↑‖f t‖₊ ^ 2 ∂E_pvm.scalarMeasure x

The simple spectral integral satisfies the pointwise L² norm identity.

theorem PVM.ofReal_norm_sq_integral {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (f : ℝ → ℂ) (hf : Measurable f) (hbdd : ∃ (C : ℝ), ∀ (t : ℝ), ‖f t‖ ≤ C) (x : E) : ENNReal.ofReal (‖(E_pvm.integral f hf hbdd) x‖ ^ 2) = ∫⁻ (t : ℝ), ↑‖f t‖₊ ^ 2 ∂E_pvm.scalarMeasure x

The bounded spectral integral satisfies the pointwise L² norm identity.

theorem PVM.scalarContent_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (c : ℂ) (x : E) (S : Set ℝ) (hS : MeasurableSet S) : E_pvm.scalarContent (c • x) S = ‖c‖ ^ 2 * E_pvm.scalarContent x S

Scalar PVM content is quadratic under complex scalar multiplication.

theorem PVM.scalarContent_add_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (x y : E) (S : Set ℝ) (hS : MeasurableSet S) : E_pvm.scalarContent (x + y) S ≤ 2 * (E_pvm.scalarContent x S + E_pvm.scalarContent y S)

Scalar content of a sum is controlled by the two summands.

theorem PVM.scalarContent_proj {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (x : E) (S T : Set ℝ) (hS : MeasurableSet S) (hT : MeasurableSet T) : E_pvm.scalarContent ((E_pvm.proj S) x) T = E_pvm.scalarContent x (T ∩ S)

Projecting the vector restricts its scalar content to the projection set.

theorem PVM.scalarMeasure_proj {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (x : E) (S : Set ℝ) (hS : MeasurableSet S) : E_pvm.scalarMeasure ((E_pvm.proj S) x) = (E_pvm.scalarMeasure x).restrict S

Projecting a vector restricts its scalar measure to the projection set.

@[simp]

theorem PVM.scalarMeasure_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) : E_pvm.scalarMeasure 0 = 0

The scalar measure associated to the zero vector is the zero measure.

theorem PVM.scalarMeasure_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (c : ℂ) (x : E) : E_pvm.scalarMeasure (c • x) = ENNReal.ofReal (‖c‖ ^ 2) • E_pvm.scalarMeasure x

The scalar measure is quadratic under complex scalar multiplication.

theorem PVM.scalarMeasure_add_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (x y : E) : E_pvm.scalarMeasure (x + y) ≤ 2 • (E_pvm.scalarMeasure x + E_pvm.scalarMeasure y)

The scalar measure of a sum is dominated by twice the sum of the scalar measures.

noncomputable def PVM.squareIntegrableDomain {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (f : ℝ → ℂ) : Submodule ℂ E

The vectors square-integrable against their scalar PVM measures form a submodule.

Equations

• E_pvm.squareIntegrableDomain f = { carrier := {x : E | ∫⁻ (t : ℝ), ↑‖f t‖₊ ^ 2 ∂E_pvm.scalarMeasure x < ⊤}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

noncomputable def PVM.spectralTruncation (f : ℝ → ℂ) (n : ℕ) (t : ℝ) : ℂ

The bounded truncation of a measurable function at level n.

Equations

• PVM.spectralTruncation f n t = if ‖f t‖ ≤ ↑n then f t else 0

noncomputable def PVM.truncatedIntegral {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (f : ℝ → ℂ) (hf : Measurable f) (n : ℕ) : E →L[ℂ] E

The bounded spectral integral of the nth truncation.

Equations

• E_pvm.truncatedIntegral f hf n = E_pvm.integral (PVM.spectralTruncation f n) ⋯ ⋯

noncomputable def PVM.unboundedIntegral {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (f : ℝ → ℂ) (hf : Measurable f) : E →ₗ.[ℂ] E

Spectral integration on the domain of vectors with finite second moment.

Equations

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

theorem PVM.mem_domain_unboundedIntegral {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (f : ℝ → ℂ) (hf : Measurable f) (x : E) : x ∈ (E_pvm.unboundedIntegral f hf).domain ↔ ∫⁻ (t : ℝ), ↑‖f t‖₊ ^ 2 ∂E_pvm.scalarMeasure x < ⊤

theorem PVM.inner_coordinate_unboundedIntegral_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (x : ↥(E_pvm.unboundedIntegral Complex.ofReal ⋯).domain) : inner ℂ (↑x) (↑(E_pvm.unboundedIntegral Complex.ofReal ⋯) x) = ∫ (t : ℝ), ↑t ∂E_pvm.scalarMeasure ↑x

The diagonal matrix coefficient of the coordinate spectral integral is the first moment of the associated scalar spectral measure.

theorem PVM.ofReal_norm_sq_integral_sub_unboundedIntegral {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (f : ℝ → ℂ) (hf : Measurable f) (hbdd : ∃ (C : ℝ), ∀ (r : ℝ), ‖f r‖ ≤ C) (g : ℝ → ℂ) (hg : Measurable g) (x : ↥(E_pvm.unboundedIntegral g hg).domain) : ENNReal.ofReal (‖(E_pvm.integral f hf hbdd) ↑x - ↑(E_pvm.unboundedIntegral g hg) x‖ ^ 2) = ∫⁻ (r : ℝ), ↑‖f r - g r‖₊ ^ 2 ∂E_pvm.scalarMeasure ↑x

The pointwise L² identity comparing a bounded spectral integral with an unbounded spectral integral on the latter's domain.

theorem PVM.scalarMeasure_integral {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (f : ℝ → ℂ) (hf : Measurable f) (hbdd : ∃ (C : ℝ), ∀ (r : ℝ), ‖f r‖ ≤ C) (x : E) : E_pvm.scalarMeasure ((E_pvm.integral f hf hbdd) x) = (E_pvm.scalarMeasure x).withDensity fun (r : ℝ) => ↑(‖f r‖₊ ^ 2)

The scalar measure of a bounded spectral-integral vector is the original scalar measure weighted by the squared norm of the integrand.

theorem PVM.integral_mem_domain_unboundedIntegral {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (f : ℝ → ℂ) (hf : Measurable f) (hbdd : ∃ (C : ℝ), ∀ (r : ℝ), ‖f r‖ ≤ C) (g : ℝ → ℂ) (hg : Measurable g) (hprodBdd : ∃ (C : ℝ), ∀ (r : ℝ), ‖g r * f r‖ ≤ C) (x : E) : (E_pvm.integral f hf hbdd) x ∈ (E_pvm.unboundedIntegral g hg).domain

A bounded spectral integral lies in the domain of an unbounded spectral integral when the pointwise product of their integrands is bounded.

theorem PVM.unboundedIntegral_integral {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (f : ℝ → ℂ) (hf : Measurable f) (hfBdd : ∃ (C : ℝ), ∀ (r : ℝ), ‖f r‖ ≤ C) (g : ℝ → ℂ) (hg : Measurable g) (hprodBdd : ∃ (C : ℝ), ∀ (r : ℝ), ‖(g * f) r‖ ≤ C) (x : E) : ↑(E_pvm.unboundedIntegral g hg) ⟨(E_pvm.integral f hf hfBdd) x, ⋯⟩ = (E_pvm.integral (g * f) ⋯ hprodBdd) x

Unbounded spectral integration acts on bounded spectral-integral vectors by pointwise multiplication, provided the product integrand is bounded.

theorem PVM.coordinate_unboundedIntegral_isFormalAdjoint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) : have A := E_pvm.unboundedIntegral Complex.ofReal ⋯; A.IsFormalAdjoint A

Integration of the real coordinate against any PVM is a symmetric partial operator.

theorem PVM.unboundedIntegral_eq_of_proj_eq_on_measurable {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E₁ E₂ : PVM E) (hproj : ∀ (S : Set ℝ), MeasurableSet S → E₁.proj S = E₂.proj S) (f : ℝ → ℂ) (hf : Measurable f) : E₁.unboundedIntegral f hf = E₂.unboundedIntegral f hf

Unbounded spectral integration depends only on a PVM's values on measurable sets.