CreationGram.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The creation row from its covariance matrix

def OAI.KadisonKastler.scalarProjectionHom line 23
Source documentation
Scalars acting on a projection corner form a nonunital star representation.
```
def scalarProjectionHom (P : H →L[ℂ] H) (hP : IsStarProjection P) :
    ℂ →⋆ₙₐ[ℂ] (H →L[ℂ] H) where
…
```
def OAI.KadisonKastler.centeredCovariance line 35
theorem OAI.KadisonKastler.norm_centeredCovariance_le line 38

theorem OAI.KadisonKastler.norm_creationRow_le line 51

Source documentation

An operator row whose Gram matrix is the centered covariance has the required dimension decay, even with an arbitrary Hilbert tail projection.

theorem norm_creationRow_le (C : α → H →L[ℂ] H) (P : H →L[ℂ] H)
    (hP : IsStarProjection P)
    (hGram : ∀ a b, star (C a) * C b =
      ((Fintype.card α : ℂ)⁻¹ *
        ((if a = b then 1 else 0) - (Fintype.card α : ℂ)⁻¹)) • P) :
    ‖(CStarMatrix.ofMatrix (fun (_ : Unit) a => C a))‖ ≤
      (Real.sqrt (Fintype.card α : ℝ))⁻¹ := by
…