OAI/Analysis/JiangSu/TraceCone/MatrixMasks.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TraceCone.matrixMask line 14
  2. lemma OAI.TraceCone.matrixMask_apply line 17
  3. lemma OAI.TraceCone.matrixMask_eq_self line 21
  4. lemma OAI.TraceCone.matrixMask_zero line 26
  5. lemma OAI.TraceCone.matrixMask_add line 29
  6. lemma OAI.TraceCone.matrixMask_smul line 33
  7. lemma OAI.TraceCone.matrixMask_sub line 37
  8. def OAI.TraceCone.matrixUnitize line 42
  9. lemma OAI.TraceCone.matrixUnitize_injective line 45
  10. lemma OAI.TraceCone.matrixUnitize_norm line 51
  11. def OAI.TraceCone.matrixMaskProjection line 55
  12. lemma OAI.TraceCone.matrixMaskProjection_star line 58
  13. lemma OAI.TraceCone.matrixMaskProjection_mul line 65
  14. lemma OAI.TraceCone.matrixMaskProjection_norm_le line 75
  15. lemma OAI.TraceCone.matrixMask_unitize line 80
  16. theorem OAI.TraceCone.matrixMask_norm_le line 91
  17. lemma OAI.TraceCone.matrixMask_successor line 103
  18. lemma OAI.TraceCone.matrixMask_inclusion line 114
  19. def OAI.TraceCone.matrixFamilyMask line 132
  20. lemma OAI.TraceCone.matrixFamilyMask_vanishing line 139
  21. def OAI.TraceCone.matrixQuotientMask line 144
  22. lemma OAI.TraceCone.matrixQuotientMask_mk line 148
  23. lemma OAI.TraceCone.matrixQuotientMask_norm_le line 151
  24. def OAI.TraceCone.matrixQuotientMaskCLM line 158
  25. lemma OAI.TraceCone.matrixQuotientMask_stage line 161
  26. lemma OAI.TraceCone.matrixQuotientMask_mem_limit line 169
  27. def OAI.TraceCone.matrixCompression line 176
  28. lemma OAI.TraceCone.matrixCompression_norm_le line 181
  29. lemma OAI.TraceCone.matrixCompression_stage line 184
  30. theorem OAI.TraceCone.contractions_tendsto line 188
  31. theorem OAI.TraceCone.matrixCompression_tendsto line 205