OAI/Analysis/CStarAlgebra/PureInfiniteness/Compression.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MainGap.cutInverseFn line 12
  2. lemma OAI.MainGap.continuous_cutInverseFn line 14
  3. lemma OAI.MainGap.cutInverseFn_zero line 18
  4. def OAI.MainGap.cutInverse line 20
  5. lemma OAI.MainGap.cutInverseFn_bound line 22
  6. lemma OAI.MainGap.norm_cutInverse_le line 40
  7. lemma OAI.MainGap.cut_mul_cutInverse line 48
  8. lemma OAI.MainGap.Her_right_fixed_cutInverse line 70
  9. def OAI.MainGap.HerCompression line 79
  10. lemma OAI.MainGap.cut_sqrt_lower line 82
  11. lemma OAI.MainGap.norm_mul_factor_of_order line 106
  12. lemma OAI.MainGap.norm_mul_Her_of_order line 121
  13. lemma OAI.MainGap.conditional_defect_bounds line 136
  14. lemma OAI.MainGap.conditional_order_loss line 157
  15. lemma OAI.MainGap.conditional_Her_loss line 186
  16. lemma OAI.MainGap.conditional_q_zero line 214
  17. lemma OAI.MainGap.compression_of_conditional_loss line 244