Documentation

TauCeti.Analysis.InnerProductSpace.ProjValMeasure.Basic

Projection-valued measures #

A projection-valued measure on the measurable sets of an arbitrary measurable space X, acting on a complex Hilbert space H.

The finite diagonal scalar measures are provided by the DKPS donor's diag field. Their measure-theoretic countable additivity supplies strong countable additivity of the projections. Idempotence, self-adjointness, positivity, and finite additivity are proved from the structure's laws.

Main declarations #

References #

The structure #

source
structure TauCeti.ProjValMeasure (X : Type u_3) [MeasurableSpace X] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] :
Type (max u_3 u_4)

A projection-valued measure on the measurable sets of X, acting on a complex Hilbert space H.

The diagonal scalar measures diag ξ are supplied as finite measures, related to the projections by inner_proj. This follows the donor's carrier representation, in which the diagonal measures are uniquely determined by proj. Idempotence, self-adjointness, positivity, finite additivity, contraction, and strong countable additivity follow from these laws.

Instances For

    The classical axioms, recovered as theorems #

    source
    instance TauCeti.ProjValMeasure.instIsFiniteMeasureDiag {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (ξ : H) :
    MeasureTheory.IsFiniteMeasure (P.diag ξ)

    Each scalar diagonal measure is finite, as witnessed by the diag_finite field. Its total mass is computed by diag_univ.

    source
    theorem TauCeti.ProjValMeasure.inner_proj_apply_left {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (B : Set X) (hB : MeasurableSet B) (ξ : H) :
    inner ℂ ((P.proj B hB) ξ) ξ = ↑((P.diag ξ) B).toReal

    The diagonal identity with the projection in the first inner-product slot.

    source
    theorem TauCeti.ProjValMeasure.proj_congr {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) {B₁ B₂ : Set X} (h : B₁ = B₂) (h₁ : MeasurableSet B₁) (h₂ : MeasurableSet B₂) :
    P.proj B₁ h₁ = P.proj B₂ h₂

    The projections do not depend on the measurability witness — proof irrelevance: only the set matters.

    source
    @[simp]
    theorem TauCeti.ProjValMeasure.proj_empty {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) :
    P.proj ∅ ⋯ = 0

    The projection of the empty measurable set is zero.

    source
    @[simp]
    theorem TauCeti.ProjValMeasure.proj_idem {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (B : Set X) (hB : MeasurableSet B) :
    P.proj B hB * P.proj B hB = P.proj B hB

    Every measurable-set projection is idempotent.

    source
    theorem TauCeti.ProjValMeasure.isSelfAdjoint_proj {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (B : Set X) (hB : MeasurableSet B) :
    IsSelfAdjoint (P.proj B hB)

    Every measurable-set projection is self-adjoint.

    source
    @[simp]
    theorem TauCeti.ProjValMeasure.proj_apply_proj {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (B : Set X) (hB : MeasurableSet B) (v : H) :
    (P.proj B hB) ((P.proj B hB) v) = (P.proj B hB) v

    Applying a measurable-set projection twice is the same as applying it once.

    source
    theorem TauCeti.ProjValMeasure.inner_proj_eq_inner_proj_proj {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (B : Set X) (hB : MeasurableSet B) (ψ ξ : H) :
    inner ℂ ψ ((P.proj B hB) ξ) = inner ℂ ((P.proj B hB) ψ) ((P.proj B hB) ξ)

    A measurable projection has the same matrix element when applied in both arguments.

    source
    theorem TauCeti.ProjValMeasure.isStarProjection_proj {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (B : Set X) (hB : MeasurableSet B) :
    IsStarProjection (P.proj B hB)

    Each measurable-set value of a PVM is an orthogonal (star) projection.

    source
    theorem TauCeti.ProjValMeasure.isPositive_proj {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (B : Set X) (hB : MeasurableSet B) :
    (P.proj B hB).IsPositive

    For each measurable set B, the operator P(B) is positive.

    source
    theorem TauCeti.ProjValMeasure.proj_mul_comm {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (B C : Set X) (hB : MeasurableSet B) (hC : MeasurableSet C) :
    P.proj B hB * P.proj C hC = P.proj C hC * P.proj B hB

    Measurable-set projections commute, because intersection is symmetric.

    source
    @[simp]
    theorem TauCeti.ProjValMeasure.proj_mul_eq_zero_of_disjoint {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) {B C : Set X} (hB : MeasurableSet B) (hC : MeasurableSet C) (hd : Disjoint B C) :
    P.proj B hB * P.proj C hC = 0

    Projections of disjoint measurable sets have zero product.

    source
    theorem TauCeti.ProjValMeasure.proj_mul_eq_left_of_subset {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) {B C : Set X} (hBC : B ⊆ C) (hB : MeasurableSet B) (hC : MeasurableSet C) :
    P.proj B hB * P.proj C hC = P.proj B hB

    For measurable B ⊆ C, the projection product P(B) * P(C) is P(B).

    source
    theorem TauCeti.ProjValMeasure.proj_mul_eq_right_of_subset {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) {B C : Set X} (hBC : B ⊆ C) (hB : MeasurableSet B) (hC : MeasurableSet C) :
    P.proj C hC * P.proj B hB = P.proj B hB

    Right absorption: if B ⊆ C, then P(C) * P(B) = P(B).

    source
    theorem TauCeti.ProjValMeasure.proj_range_mono {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) {B C : Set X} (hBC : B ⊆ C) (hB : MeasurableSet B) (hC : MeasurableSet C) :
    (↑(P.proj B hB)).range ≤ (↑(P.proj C hC)).range

    If measurable B ⊆ C, then the range of P(B) is contained in the range of P(C).

    source
    theorem TauCeti.ProjValMeasure.proj_union {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) {B₁ B₂ : Set X} (hB₁ : MeasurableSet B₁) (hB₂ : MeasurableSet B₂) (hd : Disjoint B₁ B₂) :
    P.proj (B₁ ∪ B₂) ⋯ = P.proj B₁ hB₁ + P.proj B₂ hB₂

    For disjoint measurable sets, the projection of their union is the sum of their projections.

    source
    @[simp]
    theorem TauCeti.ProjValMeasure.proj_compl {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (B : Set X) (hB : MeasurableSet B) :
    P.proj Bᶜ ⋯ = ContinuousLinearMap.id ℂ H - P.proj B hB

    Complementation: the projection of a complement is the complementary projection.

    source
    theorem TauCeti.ProjValMeasure.norm_sq_proj_apply {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (B : Set X) (hB : MeasurableSet B) (ξ : H) :
    ‖(P.proj B hB) ξ‖ ^ 2 = ((P.diag ξ) B).toReal

    The squared norm of the projection of ξ equals its diagonal measure on the measurable set, interpreted as a real number.

    source
    theorem TauCeti.ProjValMeasure.diag_univ_toReal {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (ξ : H) :
    ((P.diag ξ) Set.univ).toReal = ‖ξ‖ ^ 2

    Total mass of the diagonal scalar measure, as a real number.

    source
    @[simp]
    theorem TauCeti.ProjValMeasure.diag_real_univ {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (ξ : H) :
    (P.diag ξ).real Set.univ = ‖ξ‖ ^ 2

    The total mass of the diagonal measure as a real number.

    source
    @[simp]
    theorem TauCeti.ProjValMeasure.diag_univ {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (ξ : H) :
    (P.diag ξ) Set.univ = ‖ξ‖ₑ ^ 2

    The total mass of the diagonal measure in ℝ≥0∞.

    source
    theorem TauCeti.ProjValMeasure.norm_proj_apply_le {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (B : Set X) (hB : MeasurableSet B) (ξ : H) :
    ‖(P.proj B hB) ξ‖ ≤ ‖ξ‖

    For every measurable set B, P(B) is a contraction on vectors.

    Strong countable additivity #

    For a pairwise-disjoint measurable family (B_k) with measurable union B, write S n = ∑_{k < n} P(B_k). The diagonal measures are genuine measures, so μ(B) = ∑' μ(B_k) for every ξ; the squared distance ‖(S n) ξ - P(B) ξ‖² then equals μ(B) - ∑_{k < n} μ(B_k) — the mass of B not yet covered — and that tends to 0. This is strong countable additivity: the partial sums converge strongly to P(B).

    source
    theorem TauCeti.ProjValMeasure.tendsto_sum_proj_of_pairwise_disjoint {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {P : ProjValMeasure X H} {f : ℕ → Set X} (hf : ∀ (n : ℕ), MeasurableSet (f n)) (hdisj : Pairwise (Function.onFun Disjoint f)) (ξ : H) :
    Filter.Tendsto (fun (n : ℕ) => (∑ k < n, P.proj (f k) ⋯) ξ) Filter.atTop (nhds ((P.proj (⋃ (k : ℕ), f k) ⋯) ξ))

    For pairwise disjoint measurable sets, the finite sums of their projections, applied to any vector, converge to the projection of their union applied to that vector.

    source
    theorem TauCeti.ProjValMeasure.hasSum_proj_of_pairwise_disjoint {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {P : ProjValMeasure X H} {f : ℕ → Set X} (hf : ∀ (n : ℕ), MeasurableSet (f n)) (hdisj : Pairwise (Function.onFun Disjoint f)) (ξ : H) :
    HasSum (fun (n : ℕ) => (P.proj (f n) ⋯) ξ) ((P.proj (⋃ (n : ℕ), f n) ⋯) ξ)

    Unconditional strong countable additivity: disjoint measurable-set projections form a summable family of vectors, and their sum is the projection of the union. This is the HasSum interface needed by the spectral integral.

    Extensionality #

    A ProjValMeasure is determined by either its projection field or its finite diagonal scalar measures. The identity inner_proj relates these fields; finite measure values are recovered from their real embeddings.

    source
    theorem TauCeti.ProjValMeasure.ext_of_diag {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {P Q : ProjValMeasure X H} (h : ∀ (ξ : H), P.diag ξ = Q.diag ξ) :
    P = Q

    Two projection-valued measures with the same diagonal scalar measures are equal.

    source
    theorem TauCeti.ProjValMeasure.ext {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {P Q : ProjValMeasure X H} (h : ∀ (B : Set X) (hB : MeasurableSet B), P.proj B hB = Q.proj B hB) :
    P = Q

    Two projection-valued measures agreeing on all measurable-set projections are equal.

    source
    theorem TauCeti.ProjValMeasure.ext_iff {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {P Q : ProjValMeasure X H} :
    P = Q ↔ ∀ (B : Set X) (hB : MeasurableSet B), P.proj B hB = Q.proj B hB
    source
    theorem TauCeti.ProjValMeasure.ext_iff_diag {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {P Q : ProjValMeasure X H} :
    P = Q ↔ ∀ (ξ : H), P.diag ξ = Q.diag ξ

    Equality of projection-valued measures is equivalent to equality of all diagonal scalar measures.