OAI/Analysis/FourierLLogL/Fourier/Affine.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Changing the size and origin of the top interval

  1. lemma OAI.FourierLLogL.Period.phase_add line 12
  2. lemma OAI.FourierLLogL.Period.phase_freq_add line 20
  3. lemma OAI.FourierLLogL.Period.phase_mul_arg line 28
  4. lemma OAI.FourierLLogL.Period.norm_phase_sub line 31
  5. lemma OAI.FourierLLogL.Period.norm_mod line 42
  6. lemma OAI.FourierLLogL.Period.coeff_near line 47
  7. lemma OAI.FourierLLogL.Period.cell_unique line 104
  8. lemma OAI.FourierLLogL.Period.shift_near_unit line 121
  9. lemma OAI.FourierLLogL.Period.shift_pull line 168
  10. lemma OAI.FourierLLogL.Period.shift_scale line 184
  11. lemma OAI.FourierLLogL.Period.map_affine line 194
  12. lemma OAI.FourierLLogL.Period.restrict_affine line 203
  13. def OAI.FourierLLogL.Period.shiftD line 216
  14. def OAI.FourierLLogL.Period.AffineTreeBound line 220
  15. lemma OAI.FourierLLogL.Period.cube_eventually line 228
  16. theorem OAI.FourierLLogL.Period.UnitTreeBound.affine line 240