OAI/Combinatorics/Progressions/Fourier/TorusCellBudget.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.torusGridCenter line 14
  2. theorem OAI.Erdos3.fractionalPartBin_center_error line 17
  3. theorem OAI.Erdos3.torusGrid_coordinate_cover line 31
  4. theorem OAI.Erdos3.torusGrid_cover line 45
  5. theorem OAI.Erdos3.circle_grid_cover line 63
  6. def OAI.Erdos3.ambientTorusGrid line 76
  7. theorem OAI.Erdos3.ambientTorusGrid_cover line 79
  8. theorem OAI.Erdos3.ambientTorus_image_cover line 84
  9. def OAI.Erdos3.ambientTorusTent line 103
  10. theorem OAI.Erdos3.ambientTorusTent_range line 106
  11. theorem OAI.Erdos3.ambientTorusTent_ge_half line 112
  12. theorem OAI.Erdos3.ambientTorusTent_support line 119
  13. theorem OAI.Erdos3.ambientTorusTent_lipschitz line 128
  14. theorem OAI.Erdos3.residue_quotient_double_bound line 153
  15. theorem OAI.Erdos3.exists_residue_circle_neighborhood_embedding line 159
  16. def OAI.Erdos3.centeredTorusTent line 206
  17. theorem OAI.Erdos3.centeredTorusTent_range line 209
  18. theorem OAI.Erdos3.centeredTorusTent_lipschitz line 213
  19. theorem OAI.Erdos3.centeredTorusTent_coordinate_support line 219
  20. theorem OAI.Erdos3.centeredTorusTent_residue_mean line 228
  21. theorem OAI.Erdos3.localTent_translateSum_ge_half line 286
  22. def OAI.Erdos3.torusGridKernel line 293
  23. theorem OAI.Erdos3.torusGridKernel_lip line 297
  24. theorem OAI.Erdos3.torusGridKernel_support line 302
  25. theorem OAI.Erdos3.sum_torusGridKernel_periodicValue line 311
  26. theorem OAI.Erdos3.PolynomialPatch.ofCoordinates_value line 329
  27. def OAI.Erdos3.polynomialTorusCell line 345
  28. theorem OAI.Erdos3.polynomialTorusCell_value line 353
  29. theorem OAI.Erdos3.polynomialTorusCell_lip line 364
  30. theorem OAI.Erdos3.sum_polynomialTorusCell_value line 371
  31. theorem OAI.Erdos3.exists_polynomialTorusCell_score line 379
  32. theorem OAI.Erdos3.exists_torusCell_lift_offset line 401
  33. def OAI.Erdos3.PatchKernel.integerLift line 437
  34. theorem OAI.Erdos3.PatchKernel.periodicValue_eq_integerLift line 441
  35. theorem OAI.Erdos3.PatchKernel.integerLift_contributes line 451
  36. theorem OAI.Erdos3.exists_torusCell_affine_recovery line 457
  37. theorem OAI.Erdos3.torusGrid_log_card line 482
  38. theorem OAI.Erdos3.torusGridKernel_lip_add_one_le line 486
  39. theorem OAI.Erdos3.torusGridKernel_log_lip line 497
  40. theorem OAI.Erdos3.exists_torus_lift_mesh line 506
  41. theorem OAI.Erdos3.exists_polynomialTorusCell_exp_score line 515