OAI/LinearAlgebra/MatrixState/QuarterRoot.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.RowColumn.MatrixState.quarterRoot line 11
  2. def OAI.RowColumn.MatrixState.inverseQuarter line 12
  3. def OAI.RowColumn.MatrixState.quarterSupport line 14
  4. lemma OAI.RowColumn.MatrixState.quarter_positive line 16
  5. lemma OAI.RowColumn.MatrixState.quarter_square line 18
  6. lemma OAI.RowColumn.MatrixState.quarter_four line 20
  7. lemma OAI.RowColumn.MatrixState.inverseQuarter_positive line 25
  8. lemma OAI.RowColumn.MatrixState.inverseQuarter_commute line 32
  9. lemma OAI.RowColumn.MatrixState.quarter_inverse_quarter line 35
  10. lemma OAI.RowColumn.MatrixState.quarterSupport_hermitian line 49
  11. lemma OAI.RowColumn.MatrixState.quarterSupport_mul_self line 54
  12. lemma OAI.RowColumn.MatrixState.quarterSupport_mul line 59
  13. lemma OAI.RowColumn.MatrixState.quarter_whitening_mean line 67
  14. lemma OAI.RowColumn.MatrixState.positive_kernel_mono line 84

    Source documentation

    Kernel propagation for positive matrices, used to justify all inverses on supports in the quarter-root normalization, including singular states.

    lemma positive_kernel_mono (S A P : Matrix C C ℂ) (hS : S.PosSemidef)
    (hle : S ≤ A) (hP : P.IsHermitian) (hPA : P*A=0) : P*S=0 := by
…
  15. lemma OAI.RowColumn.MatrixState.quarterSupport_of_le line 103
  16. lemma OAI.RowColumn.MatrixState.undo_quarter_whitening line 111