OAI/Probability/SignedSweeps/HilbertFibers.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SignedSweeps.HilbertFibers line 12
  2. def OAI.SignedSweeps.fiberEvaluation line 15
  3. def OAI.SignedSweeps.fiberInsertionLinear line 20
  4. lemma OAI.SignedSweeps.fiberInsertionLinear_apply line 34
  5. def OAI.SignedSweeps.fiberInsertion line 38
  6. lemma OAI.SignedSweeps.fiberInsertion_apply line 46
  7. lemma OAI.SignedSweeps.fiberEvaluation_insertion line 49
  8. lemma OAI.SignedSweeps.fiberInsertion_adjoint line 54
  9. lemma OAI.SignedSweeps.hilbertBlock_fiber_apply line 70
  10. def OAI.SignedSweeps.fiberDiagonal line 74
  11. lemma OAI.SignedSweeps.fiberDiagonal_apply line 80
  12. lemma OAI.SignedSweeps.fiberDiagonal_eq_sum line 84
  13. lemma OAI.SignedSweeps.fiberDiagonal_mul line 95
  14. lemma OAI.SignedSweeps.fiberDiagonal_positive line 104
  15. lemma OAI.SignedSweeps.fiberDiagonal_idempotent line 117
  16. lemma OAI.SignedSweeps.trace_fiberDiagonal_mul line 122