OAI/Analysis/JiangSu/Excision/ExcisionSoftCompression.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PureStateExcision.softScalar line 15
  2. lemma OAI.PureStateExcision.softScalar_continuous line 16
  3. lemma OAI.PureStateExcision.softScalar_nonneg line 21
  4. lemma OAI.PureStateExcision.softScalar_le_one line 22
  5. lemma OAI.PureStateExcision.softScalar_error line 25
  6. lemma OAI.PureStateExcision.softScalar_compressed line 32
  7. def OAI.PureStateExcision.softCompression line 40
  8. lemma OAI.PureStateExcision.softCompression_nonneg line 41
  9. lemma OAI.PureStateExcision.softCompression_le_one line 43
  10. lemma OAI.PureStateExcision.softCompression_norm_le line 45
  11. lemma OAI.PureStateExcision.softCompression_error line 47
  12. lemma OAI.PureStateExcision.softCompression_compressed line 59
  13. lemma OAI.PureStateExcision.norm_mul_softCompression_le line 71
  14. lemma OAI.PureStateExcision.realPart_compression line 88
  15. lemma OAI.PureStateExcision.realPart_compression_norm_le line 96
  16. lemma OAI.PureStateExcision.state_left_norm_sq line 114
  17. lemma OAI.PureStateExcision.state_real_smul line 123
  18. lemma OAI.PureStateExcision.state_selfadjoint_real line 128
  19. theorem OAI.PureStateExcision.pure_state_finite_selfadjoint_excision line 135