OAI/Analysis/FreeWords/DyadicPhases.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KKProjectionSupport.dyadicRoot line 38
  2. theorem OAI.KKProjectionSupport.dyadicRoot_zero line 40
  3. theorem OAI.KKProjectionSupport.dyadicRoot_norm line 43
  4. theorem OAI.KKProjectionSupport.dyadicRoot_square line 49
  5. theorem OAI.KKProjectionSupport.dyadicRoot_sub_one line 56
  6. theorem OAI.KKProjectionSupport.dyadicRoot_pow_ne_one line 62
  7. def OAI.KKProjectionSupport.dyadicPhase line 69
  8. theorem OAI.KKProjectionSupport.dyadicPhase_norm line 73
  9. def OAI.KKProjectionSupport.phaseMoment line 80
  10. theorem OAI.KKProjectionSupport.phaseMoment_zero line 82
  11. theorem OAI.KKProjectionSupport.phaseMoment_succ line 86
  12. theorem OAI.KKProjectionSupport.phaseMoment_annihilation line 94
  13. theorem OAI.KKProjectionSupport.phaseMoment_eq_zero line 107