OAI/Analysis/CStarAlgebra/PureInfiniteness/Defect.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MainGap.deficiency_eq_sub line 14
  2. lemma OAI.MainGap.sandwich_zero_eigen line 31
  3. lemma OAI.MainGap.Her_eigen_left line 41
  4. lemma OAI.MainGap.firstH_mem_firstX line 48
  5. lemma OAI.MainGap.firstK_fixes_H line 52
  6. lemma OAI.MainGap.firstR_fixed_left line 56
  7. lemma OAI.MainGap.firstR_inner line 64
  8. lemma OAI.MainGap.firstR_orthogonal line 76
  9. lemma OAI.MainGap.ramp_projection line 91
  10. lemma OAI.MainGap.cut_projection line 103
  11. lemma OAI.MainGap.scalingDefect_expansion line 116
  12. lemma OAI.MainGap.scalingDefect_compress line 124
  13. theorem OAI.MainGap.four_fixed_impossible line 153
  14. lemma OAI.MainGap.firstSandwich_single_le line 221
  15. lemma OAI.MainGap.represented_single_sq_le line 238
  16. lemma OAI.MainGap.represented_mixed_estimate line 246