OAI/Analysis/FourierLLogL/Dyadic/Circle.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Grid distance and elementary counting

  1. def OAI.FourierLLogL.Dyadic.rad line 14
  2. def OAI.FourierLLogL.Dyadic.diam line 15
  3. def OAI.FourierLLogL.Dyadic.liftInt line 17
  4. lemma OAI.FourierLLogL.Dyadic.rad_abs line 19
  5. lemma OAI.FourierLLogL.Dyadic.liftInt_cast line 25
  6. lemma OAI.FourierLLogL.Dyadic.rad_even line 26
  7. lemma OAI.FourierLLogL.Dyadic.diam_even line 27
  8. lemma OAI.FourierLLogL.Dyadic.rad_nonneg line 29
  9. lemma OAI.FourierLLogL.Dyadic.diam_nonneg line 30
  10. lemma OAI.FourierLLogL.Dyadic.pos_nonneg line 32
  11. lemma OAI.FourierLLogL.Dyadic.pos_lt line 33
  12. lemma OAI.FourierLLogL.Dyadic.pos_neg line 34
  13. lemma OAI.FourierLLogL.Dyadic.diam_min line 40
  14. lemma OAI.FourierLLogL.Dyadic.diam_le_half line 44
  15. lemma OAI.FourierLLogL.Dyadic.rad_le_val line 53
  16. lemma OAI.FourierLLogL.Dyadic.rad_le_nat line 54
  17. lemma OAI.FourierLLogL.Dyadic.rad_le_int line 58
  18. lemma OAI.FourierLLogL.Dyadic.rad_add line 67
  19. lemma OAI.FourierLLogL.Dyadic.diam_add line 72
  20. lemma OAI.FourierLLogL.Dyadic.pos_sub_val line 76
  21. lemma OAI.FourierLLogL.Dyadic.diam_le_diff line 79
  22. lemma OAI.FourierLLogL.Dyadic.phase_distance line 86
  23. def OAI.FourierLLogL.Dyadic.first line 94
  24. lemma OAI.FourierLLogL.Dyadic.mem_first line 96
  25. lemma OAI.FourierLLogL.Dyadic.first_eq_range line 98
  26. lemma OAI.FourierLLogL.Dyadic.range_inj line 107
  27. lemma OAI.FourierLLogL.Dyadic.first_card line 114
  28. lemma OAI.FourierLLogL.Dyadic.first_card_le line 117
  29. lemma OAI.FourierLLogL.Dyadic.sum_first line 123
  30. lemma OAI.FourierLLogL.Dyadic.first_max line 131
  31. lemma OAI.FourierLLogL.Dyadic.sum_grid line 134
  32. def OAI.FourierLLogL.Dyadic.arc line 138
  33. lemma OAI.FourierLLogL.Dyadic.mem_arc line 139
  34. lemma OAI.FourierLLogL.Dyadic.arc_card_hi line 141
  35. lemma OAI.FourierLLogL.Dyadic.arc_card_lo line 159
  36. lemma OAI.FourierLLogL.Dyadic.side_card line 171
  37. lemma OAI.FourierLLogL.Dyadic.arc_length line 173