OAI/Analysis/CStarAlgebra/PureInfiniteness/ChoicePairs.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MainGap.norm_sqrt_le_one line 14
  2. lemma OAI.MainGap.fixed_left_of_modulus line 20
  3. lemma OAI.MainGap.carrier_mem_Her line 30
  4. theorem OAI.MainGap.first_pair_choice line 38
  5. theorem OAI.MainGap.last_pair_choice line 69
  6. def OAI.MainGap.firstSandwich line 107
  7. lemma OAI.MainGap.firstSandwich_nonneg line 110
  8. lemma OAI.MainGap.firstSandwich_mem line 117
  9. lemma OAI.MainGap.firstSandwich_two_cuntzLE line 122
  10. lemma OAI.MainGap.norm_ramp_bound line 135
  11. def OAI.MainGap.scalingComplement line 151
  12. def OAI.MainGap.scalingIsometry line 153
  13. def OAI.MainGap.scalingDefect line 155
  14. lemma OAI.MainGap.complement_nonneg line 157
  15. lemma OAI.MainGap.scalingComplement_mul_self line 166
  16. lemma OAI.MainGap.scalingComplement_selfAdjoint line 170
  17. lemma OAI.MainGap.scalingComplement_mul_eq_zero line 173
  18. lemma OAI.MainGap.scalingIsometry_star_mul_self line 183
  19. lemma OAI.MainGap.scalingDefect_projection line 194
  20. lemma OAI.MainGap.scalingDefect_fixes_second line 206
  21. lemma OAI.MainGap.scalingDefect_ne_zero line 215
  22. lemma OAI.MainGap.last_pair_kills_defect line 228
  23. def OAI.MainGap.deficiency line 251
  24. def OAI.MainGap.firstX line 253
  25. def OAI.MainGap.firstV line 254
  26. def OAI.MainGap.firstU line 255
  27. def OAI.MainGap.firstH line 258
  28. def OAI.MainGap.firstK line 259
  29. def OAI.MainGap.firstR line 260
  30. def OAI.MainGap.prospectiveDefect line 261
  31. def OAI.MainGap.lastX line 264
  32. def OAI.MainGap.lastR line 265
  33. def OAI.MainGap.fourHer line 268
  34. lemma OAI.MainGap.deficiency_nonneg line 270
  35. lemma OAI.MainGap.deficiency_selfAdjoint line 271
  36. lemma OAI.MainGap.squareSandwich_nonneg line 273
  37. lemma OAI.MainGap.squareSandwich_mem line 278
  38. lemma OAI.MainGap.cut_mem_cutHer line 282
  39. lemma OAI.MainGap.firstX_mem line 291
  40. lemma OAI.MainGap.firstV_mem line 293
  41. lemma OAI.MainGap.firstU_nonneg line 295
  42. lemma OAI.MainGap.firstU_mem line 297
  43. lemma OAI.MainGap.firstK_mem line 300
  44. lemma OAI.MainGap.prospectiveDefect_nonneg line 304
  45. lemma OAI.MainGap.prospectiveDefect_norm line 306
  46. lemma OAI.MainGap.prospectiveDefect_mem line 308
  47. lemma OAI.MainGap.lastX_nonneg line 315
  48. lemma OAI.MainGap.lastX_mem line 316
  49. lemma OAI.MainGap.lastR_nonneg line 318
  50. lemma OAI.MainGap.lastR_mem line 320