OAI/Analysis/Commutator/DyadicSpectral.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.Polar.binaryRemainder line 18
  2. lemma OAI.Kadison.Polar.binaryRemainder_nonneg line 20
  3. lemma OAI.Kadison.Polar.binaryRemainder_le_one line 33
  4. lemma OAI.Kadison.Polar.halfCut_commutes line 56
  5. def OAI.Kadison.Polar.dyadicRemainder line 65
  6. lemma OAI.Kadison.Polar.dyadicRemainder_bounds line 69
  7. lemma OAI.Kadison.Polar.dyadicRemainder_mem line 75
  8. def OAI.Kadison.Polar.dyadicStep line 81
  9. lemma OAI.Kadison.Polar.dyadicStep_remainder line 84
  10. lemma OAI.Kadison.Polar.dyadicStep_norm_error line 96
  11. lemma OAI.Kadison.Polar.dyadicRemainder_commutes line 102
  12. lemma OAI.Kadison.Polar.dyadicCut_commutes_original line 109
  13. lemma OAI.Kadison.Polar.dyadicCuts_commute line 114
  14. theorem OAI.Kadison.Polar.exists_positive_spectral_sum line 121