OAI/Analysis/KadisonKastler/MeasurableProjectionFrame.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Measurable orthogonal frames for projection fields

A countable family of measurable vectors can be orthogonalized measurably, including at points where its rank changes. Zero vectors are retained until the dimension strata are selected.

  1. theorem OAI.KadisonKastler.measurable_gramSchmidt_sequence line 27
  2. theorem OAI.KadisonKastler.measurable_gramSchmidtNormed_sequence line 41
  3. def OAI.KadisonKastler.measurableProjectionFrame line 48

    Source documentation

    The normalized Gram-Schmidt vectors of a measurable projection field.

    def measurableProjectionFrame (P : X → H →L[ℂ] H) (b : ℕ → H) (x : X) (n : ℕ) : H :=
…
  4. theorem OAI.KadisonKastler.measurableProjectionFrame_measurable line 51
  5. theorem OAI.KadisonKastler.measurableProjectionFrame_orthonormal line 57
  6. theorem OAI.KadisonKastler.projectedTotalSequence line 64
  7. theorem OAI.KadisonKastler.projectionFrame_total_of_total line 82
  8. theorem OAI.KadisonKastler.projectedHilbertBasis_total line 91
  9. theorem OAI.KadisonKastler.projectionFrame_total line 110