OAI/Analysis/ModularRecovery/FourthMoments.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Exact noncommutative fourth-moment pairings and overlap subtraction.

  1. lemma OAI.BoundedRecovery.StandardModularData.modularAverage_add_time line 20
  2. lemma OAI.BoundedRecovery.StandardModularData.average_square_state_translate line 25
  3. lemma OAI.BoundedRecovery.StandardModularData.average_sandwich_state_translate line 31
  4. lemma OAI.BoundedRecovery.StandardModularData.exists_translate_defect line 40
  5. lemma OAI.BoundedRecovery.StandardModularData.exists_finite_defect_moment_average line 57
  6. def OAI.BoundedRecovery.phase line 85
  7. def OAI.BoundedRecovery.phaseAverage line 87
  8. lemma OAI.BoundedRecovery.phase_quadratic_step line 89
  9. lemma OAI.BoundedRecovery.phase_fourth_step line 100
  10. lemma OAI.BoundedRecovery.phase_reverse_quadratic_step line 114
  11. def OAI.BoundedRecovery.phaseExpectation line 129
  12. lemma OAI.BoundedRecovery.phaseExpectation_add line 134
  13. lemma OAI.BoundedRecovery.phaseExpectation_smul line 142
  14. lemma OAI.BoundedRecovery.phaseExpectation_const line 150
  15. lemma OAI.BoundedRecovery.phaseExpectation_map line 159
  16. lemma OAI.BoundedRecovery.phaseExpectation_sub line 174
  17. lemma OAI.BoundedRecovery.phaseExpectation_mul_left line 183
  18. lemma OAI.BoundedRecovery.phaseExpectation_mul_right line 192
  19. def OAI.BoundedRecovery.phaseSum line 200
  20. lemma OAI.BoundedRecovery.phaseSum_succ line 204
  21. lemma OAI.BoundedRecovery.phaseExpectation_quadratic line 208
  22. lemma OAI.BoundedRecovery.phaseExpectation_reverse_quadratic line 222
  23. lemma OAI.BoundedRecovery.phaseExpectation_square line 236
  24. lemma OAI.BoundedRecovery.phaseExpectation_reverse_square line 241
  25. lemma OAI.BoundedRecovery.phaseExpectation_fourth line 246
  26. def OAI.BoundedRecovery.phaseMean line 266
  27. lemma OAI.BoundedRecovery.phaseMean_mono line 270
  28. lemma OAI.BoundedRecovery.phaseMean_const line 279
  29. lemma OAI.BoundedRecovery.phaseMean_add line 288
  30. lemma OAI.BoundedRecovery.phaseMean_mul line 294
  31. lemma OAI.BoundedRecovery.phaseMean_nonneg line 302
  32. lemma OAI.BoundedRecovery.exists_phaseMean_le line 306
  33. lemma OAI.BoundedRecovery.phaseMean_re line 313
  34. lemma OAI.BoundedRecovery.StandardModularData.state_T_square line 331
  35. lemma OAI.BoundedRecovery.StandardModularData.real_sqrt_sandwich line 339
  36. lemma OAI.BoundedRecovery.StandardModularData.real_sqrt_square line 344
  37. lemma OAI.BoundedRecovery.StandardModularData.real_sqrt_reverse_square line 348
  38. lemma OAI.BoundedRecovery.StandardModularData.phaseMean_defect line 353
  39. lemma OAI.BoundedRecovery.StandardModularData.phaseMean_fourth_le line 367