FiniteCoefficientFactorization.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Sharp finite coefficient factorization on an arbitrary Hilbert space

All vectors involved lie in a finite-dimensional subspace. Compression and extension by zero preserve the dual norm, so finite-dimensional polar duality applies without a separability assumption on the ambient space.

def OAI.KadisonKastler.isometricOperatorLift line 24
theorem OAI.KadisonKastler.isometricOperatorLift_norm_le line 27
theorem OAI.KadisonKastler.finiteOperatorCoefficient_lift line 41
theorem OAI.KadisonKastler.finiteOperatorCoefficient_compress line 49
theorem OAI.KadisonKastler.finiteOperatorCoefficient_norm_lift line 59
theorem OAI.KadisonKastler.isometric_coefficient_factorization line 69

theorem OAI.KadisonKastler.finite_coefficient_factorization line 88

Source documentation

Every finite vector functional on an arbitrary Hilbert space admits coefficient vectors with each squared Hilbert sum at most its dual norm.

theorem finite_coefficient_factorization {ι : Type*} [Fintype ι] (x y : ι → H) :
    ∃ (n : ℕ) (a b : Fin n → H),
      finiteOperatorCoefficient x y = finiteOperatorCoefficient a b ∧
      (∑ i, ‖a i‖ ^ 2) ≤ ‖finiteOperatorCoefficient x y‖ ∧
      (∑ i, ‖b i‖ ^ 2) ≤ ‖finiteOperatorCoefficient x y‖ := by
…

Mentions: OAI.KadisonKastler.finiteOperatorCoefficient