Polarized complex measures of a projection-valued measure

A normalized projection-valued measure P carries a finite diagonal positive measure P.diag ξ for every vector ξ. Complex polarization produces a genuine complex vector measure P.polarizedComplexMeasure ψ ξ whose value on a measurable set B is ⟪ψ, P.proj B hB ξ⟫_ℂ. Its dependence on ψ is conjugate-linear and on ξ linear. On the diagonal, P.polarizedComplexMeasure ξ ξ is P.diag ξ with the constant complex density 1.

The construction uses Mathlib's signed-measure and complex-measure conversions: countable additivity comes from the existing diagonal measures, not a second PVM construction.

Provenance

Adapted from the four-term polarization formula in the maintained Kitware DKPS formalization (AIQ-Kitware, Apache-2.0): https://github.com/AIQ-Kitware/aiq-dkps-formalization (ForTauCeti/Analysis/InnerProductSpace/BorelCalculus/Polarization.lean).

The underlying ProjValMeasure diagonal measures were originally adapted from Adam Bornemann's Spectra (Apache-2.0); see ProjValMeasure/Basic.lean for the retained notices.

noncomputable def TauCeti.ProjValMeasure.diagComplex {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (v : H) : MeasureTheory.ComplexMeasure X

A finite diagonal measure, embedded as a complex vector measure.

@[simp]

theorem TauCeti.ProjValMeasure.diagComplex_apply {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (v : H) (B : Set X) (hB : MeasurableSet B) : (P.diagComplex v) B = ↑((P.diag v) B).toReal

noncomputable def TauCeti.ProjValMeasure.polarizedComplexMeasure {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (ψ ξ : H) : MeasureTheory.ComplexMeasure X

The polarized complex measure associated to a pair of vectors.

@[simp]

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

Polarization evaluates to the matrix element of the PVM projection.

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

On the diagonal, the polarized measure recovers the PVM's positive scalar measure.

theorem TauCeti.ProjValMeasure.polarizedComplexMeasure_self_eq_withDensityᵥ {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (ξ : H) : P.polarizedComplexMeasure ξ ξ = (P.diag ξ).withDensityᵥ fun (x : X) => 1

On the diagonal, the polarized measure is the diagonal measure P.diag ξ regarded as a complex measure, that is, with the constant complex density 1.

@[simp]

theorem TauCeti.ProjValMeasure.polarizedComplexMeasure_zero_left {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (v : H) : P.polarizedComplexMeasure 0 v = 0

Polarizing against the zero vector in the first argument yields zero.

@[simp]

theorem TauCeti.ProjValMeasure.polarizedComplexMeasure_zero_right {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (u : H) : P.polarizedComplexMeasure u 0 = 0

Polarizing against the zero vector in the second argument yields zero.

theorem TauCeti.ProjValMeasure.polarizedComplexMeasure_add_left {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (ψ ψ' ξ : H) : P.polarizedComplexMeasure (ψ + ψ') ξ = P.polarizedComplexMeasure ψ ξ + P.polarizedComplexMeasure ψ' ξ

The complex measure is additive in its first (conjugate-linear) argument.

theorem TauCeti.ProjValMeasure.polarizedComplexMeasure_add_right {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (ψ ξ ξ' : H) : P.polarizedComplexMeasure ψ (ξ + ξ') = P.polarizedComplexMeasure ψ ξ + P.polarizedComplexMeasure ψ ξ'

The complex measure is additive in its second (linear) argument.

theorem TauCeti.ProjValMeasure.polarizedComplexMeasure_smul_left {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (c : ℂ) (ψ ξ : H) : P.polarizedComplexMeasure (c • ψ) ξ = star c • P.polarizedComplexMeasure ψ ξ

The first argument of the polarized complex measure is conjugate-homogeneous.

theorem TauCeti.ProjValMeasure.polarizedComplexMeasure_smul_right {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (c : ℂ) (ψ ξ : H) : P.polarizedComplexMeasure ψ (c • ξ) = c • P.polarizedComplexMeasure ψ ξ

The second argument of the polarized complex measure is homogeneous.

theorem TauCeti.ProjValMeasure.norm_polarizedComplexMeasure_apply_le {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) {ψ ξ : H} (B : Set X) (hB : MeasurableSet B) : ‖(P.polarizedComplexMeasure ψ ξ) B‖ ≤ ‖ξ‖ / (2 * ‖ψ‖) * (P.diag ψ).real B + ‖ψ‖ / (2 * ‖ξ‖) * (P.diag ξ).real B

Pointwise Young-type bound on a polarized spectral measure by a weighted sum of the two diagonal measures.