The sharp variation estimate for polarized spectral measures

For the complex measure P.polarizedComplexMeasure ψ ξ associated with a normalized projection-valued measure, we prove

(P.polarizedComplexMeasure ψ ξ).variation univ ≤ ofReal (‖ψ‖ * ‖ξ‖).

This sharp bound makes the polarized complex measure a finite-variation measure, with its total variation controlled by the product of the norms of the two vectors. It gives uniform norm control for integration against polarized spectral measures: integrating a bounded measurable function is bounded in absolute value by its supremum norm times ‖ψ‖ * ‖ξ‖.

On the diagonal, the variation of P.polarizedComplexMeasure ξ ξ is exactly P.diag ξ.

The finite-variation instance makes this property available to the vector-measure integration API and subsequent spectral-integral estimates.

The underlying PVM and polarized-measure constructions are adapted from the AIQ-Kitware DKPS formalization (Apache-2.0): https://github.com/AIQ-Kitware/aiq-dkps-formalization.

theorem TauCeti.ProjValMeasure.polarizedComplexMeasure_variation_univ_le {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (ψ ξ : H) : (MeasureTheory.VectorMeasure.variation (P.polarizedComplexMeasure ψ ξ)) Set.univ ≤ ENNReal.ofReal (‖ψ‖ * ‖ξ‖)

The variation of a polarized spectral measure has the sharp mass bound.

instance TauCeti.ProjValMeasure.instIsFiniteMeasurePolarizedVariation {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (ψ ξ : H) : MeasureTheory.IsFiniteMeasure (MeasureTheory.VectorMeasure.variation (P.polarizedComplexMeasure ψ ξ))

The variation of a polarized complex measure is finite.

@[simp]

theorem TauCeti.ProjValMeasure.variation_polarizedComplexMeasure_self {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (ξ : H) : MeasureTheory.VectorMeasure.variation (P.polarizedComplexMeasure ξ ξ) = P.diag ξ

The variation of the diagonal polarized measure is the diagonal measure.