OAI/Analysis/Quasitrace/Defect.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

The fixed positive contraction pair and its uniform real additivity defect.

  1. theorem OAI.Kaplansky.defect_telescoping line 17
  2. theorem OAI.Kaplansky.defect_constant line 28
  3. theorem OAI.Kaplansky.approximation_margin line 30
  4. def OAI.Kaplansky.partialSum line 45
  5. theorem OAI.Kaplansky.partialSum_zero line 46
  6. theorem OAI.Kaplansky.partialSum_succ line 47
  7. theorem OAI.Kaplansky.partialSum_nonneg line 50
  8. theorem OAI.Kaplansky.partialSum_mono line 53
  9. theorem OAI.Kaplansky.term_le_partialSum line 58
  10. def OAI.Kaplansky.leftSquare line 62
  11. def OAI.Kaplansky.rightSquare line 63
  12. def OAI.Kaplansky.defectAEntries line 65
  13. def OAI.Kaplansky.defectBEntries line 68
  14. def OAI.Kaplansky.defectA line 70
  15. def OAI.Kaplansky.defectB line 71
  16. theorem OAI.Kaplansky.defect_entries_bounds line 73
  17. theorem OAI.Kaplansky.defect_pair_positiveContractions line 94

    Source documentation

    Positivity and the C*-norm contraction condition for the actual pair.

    theorem defect_pair_positiveContractions (x : ℕ → A) (N : ℕ)
    (hcol : partialSum (leftSquare x) N = 1)
    (hrow : partialSum (rightSquare x) N ≤ 1) :
    PositiveContraction (defectA x N) ∧ PositiveContraction (defectB x N) := by
…

    Mentions: OAI.Kaplansky.partialSum, OAI.Kaplansky.leftSquare, OAI.Kaplansky.rightSquare, OAI.Kaplansky.PositiveContraction, OAI.Kaplansky.defectA, OAI.Kaplansky.defectB

  18. theorem OAI.Kaplansky.reflected_defect line 115
  19. theorem OAI.Kaplansky.defect_pair_identity line 130
  20. theorem OAI.Kaplansky.scalar_unit_le_one line 174
  21. theorem OAI.Kaplansky.uniform_defect line 178
  22. theorem OAI.Kaplansky.uniform_defect_twentyFour line 204