OAI/Combinatorics/TreeEdit/FiniteFourier.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TreeEdit.FiniteFourier.coefficient line 18
  2. lemma OAI.TreeEdit.FiniteFourier.expansion line 21
  3. lemma OAI.TreeEdit.FiniteFourier.weighted_sum_right line 27
  4. lemma OAI.TreeEdit.FiniteFourier.weighted_sum_left line 33
  5. lemma OAI.TreeEdit.FiniteFourier.coefficient_inner line 38
  6. lemma OAI.TreeEdit.FiniteFourier.parseval_complex line 46
  7. lemma OAI.TreeEdit.FiniteFourier.coefficient_translate line 53
  8. lemma OAI.TreeEdit.FiniteFourier.parseval line 69
  9. lemma OAI.TreeEdit.FiniteFourier.displacement_parseval line 80
  10. def OAI.TreeEdit.FiniteFourier.multiplier line 89
  11. lemma OAI.TreeEdit.FiniteFourier.multiplier_zero line 92
  12. lemma OAI.TreeEdit.FiniteFourier.multiplier_nonneg line 96
  13. def OAI.TreeEdit.FiniteFourier.average line 98
  14. def OAI.TreeEdit.FiniteFourier.HasSpectrum line 100
  15. lemma OAI.TreeEdit.FiniteFourier.spectrum_zero line 104
  16. lemma OAI.TreeEdit.FiniteFourier.HasSpectrum.add line 107
  17. lemma OAI.TreeEdit.FiniteFourier.HasSpectrum.mul line 115
  18. lemma OAI.TreeEdit.FiniteFourier.cut_spectrum line 125
  19. lemma OAI.TreeEdit.FiniteFourier.scalar_spectrum_aux line 145
  20. lemma OAI.TreeEdit.FiniteFourier.scalar_spectrum line 193
  21. lemma OAI.TreeEdit.FiniteFourier.multiplier_eq line 200
  22. lemma OAI.TreeEdit.FiniteFourier.average_const line 205
  23. lemma OAI.TreeEdit.FiniteFourier.average_nonneg line 209
  24. lemma OAI.TreeEdit.FiniteFourier.average_le_const line 212
  25. lemma OAI.TreeEdit.FiniteFourier.average_multiplier line 216
  26. lemma OAI.TreeEdit.FiniteFourier.spectrum_total line 226
  27. lemma OAI.TreeEdit.FiniteFourier.scalar_spectrum_bounded line 249
  28. lemma OAI.TreeEdit.FiniteFourier.l1_distance_series line 273
  29. lemma OAI.TreeEdit.FiniteFourier.l1_coordinate_summable line 279
  30. lemma OAI.TreeEdit.FiniteFourier.l1_distance_summable line 283
  31. theorem OAI.TreeEdit.FiniteFourier.l1_displacement_spectrum line 286
  32. def OAI.TreeEdit.FiniteFourier.energy line 315
  33. lemma OAI.TreeEdit.FiniteFourier.multiplier_le_four line 318
  34. lemma OAI.TreeEdit.FiniteFourier.energy_nonneg line 327
  35. def OAI.TreeEdit.FiniteFourier.pushSpectrum line 330
  36. lemma OAI.TreeEdit.FiniteFourier.pushSpectrum_nonneg line 334
  37. lemma OAI.TreeEdit.FiniteFourier.pushSpectrum_sum line 340
  38. lemma OAI.TreeEdit.FiniteFourier.energy_push line 352
  39. lemma OAI.TreeEdit.FiniteFourier.average_energy line 357
  40. lemma OAI.TreeEdit.FiniteFourier.sum_multiplier_period line 376
  41. lemma OAI.TreeEdit.FiniteFourier.period_detect line 391
  42. def OAI.TreeEdit.FiniteFourier.active line 415
  43. def OAI.TreeEdit.FiniteFourier.activeMass line 417
  44. lemma OAI.TreeEdit.FiniteFourier.active_nonneg line 421
  45. lemma OAI.TreeEdit.FiniteFourier.activeMass_nonneg line 424
  46. lemma OAI.TreeEdit.FiniteFourier.activeMass_push line 427
  47. lemma OAI.TreeEdit.FiniteFourier.energy_le_mass line 432
  48. lemma OAI.TreeEdit.FiniteFourier.twice_activeMass_le_average line 443
  49. lemma OAI.TreeEdit.FiniteFourier.average_mono line 462
  50. lemma OAI.TreeEdit.FiniteFourier.average_le line 465