OAI/Analysis/FourierLLogL/Fourier/Coordinates.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Using period one in real coordinates

  1. def OAI.FourierLLogL.Period.unitInt line 15
  2. def OAI.FourierLLogL.Period.μ₁ line 17
  3. def OAI.FourierLLogL.Period.circle line 19
  4. lemma OAI.FourierLLogL.Period.measurable_unitInt line 21
  5. instance OAI.FourierLLogL.Period.(instance at line 23) line 23
  6. theorem OAI.FourierLLogL.Period.measurable_circle line 27
  7. lemma OAI.FourierLLogL.Period.map_circle_volume line 30
  8. lemma OAI.FourierLLogL.Period.periodic_circle line 53
  9. def OAI.FourierLLogL.Period.coord line 57
  10. theorem OAI.FourierLLogL.Period.measurable_coord line 60
  11. lemma OAI.FourierLLogL.Period.coord_circle_eq line 63
  12. def OAI.FourierLLogL.Period.phase line 75

    Source documentation

    Character with cycles-per-unit real frequency.

    def phase (u x : ℝ) : ℂ :=
…
  13. lemma OAI.FourierLLogL.Period.phase_cont line 78
  14. lemma OAI.FourierLLogL.Period.phase_unimod line 79
  15. lemma OAI.FourierLLogL.Period.fourier_circle line 82
  16. lemma OAI.FourierLLogL.Period.phase_periodic line 86
  17. def OAI.FourierLLogL.Period.sumReal line 89
  18. def OAI.FourierLLogL.Period.maxReal line 92
  19. lemma OAI.FourierLLogL.Period.sum_eq line 95
  20. def OAI.FourierLLogL.Period.RealGoodBound line 104
  21. def OAI.FourierLLogL.HasMaxCost line 114
  22. lemma OAI.FourierLLogL.Period.cost_transfer line 121
  23. lemma OAI.FourierLLogL.HasMaxCost.add line 147
  24. lemma OAI.FourierLLogL.HasMaxCost.rot line 172
  25. theorem OAI.FourierLLogL.Period.RealGoodBound.goodBound line 177