OAI/Combinatorics/SquareDifference/FiniteKernel.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SquareDifference.finiteSquareKernel line 10
  2. def OAI.SquareDifference.finiteRationalCoefficient line 14
  3. lemma OAI.SquareDifference.finite_square_kernel_major line 18
  4. lemma OAI.SquareDifference.finite_kernel_uniform line 40
  5. def OAI.SquareDifference.boundedRationals line 109
  6. lemma OAI.SquareDifference.mem_boundedRationals line 113
  7. lemma OAI.SquareDifference.boundedRationals_card line 136
  8. lemma OAI.SquareDifference.boundedRationals_fract line 139
  9. lemma OAI.SquareDifference.boundedRationals_equiv_int line 144
  10. lemma OAI.SquareDifference.boundedRationals_sum_mod_int line 152
  11. lemma OAI.SquareDifference.actualCompleteQuadratic_periodic line 180
  12. def OAI.SquareDifference.completeRationalCoefficient line 189
  13. lemma OAI.SquareDifference.completeRationalCoefficient_eq line 193
  14. def OAI.SquareDifference.kernelModelCoefficient line 204
  15. lemma OAI.SquareDifference.primaryModelCoefficient_eq_kernelModel line 207
  16. lemma OAI.SquareDifference.expPhase_rat_add_int_square line 217
  17. lemma OAI.SquareDifference.completeRationalCoefficient_add_int line 222
  18. lemma OAI.SquareDifference.kernelModelCoefficient_add_int line 231
  19. lemma OAI.SquareDifference.kernelModelCoefficient_fract line 235
  20. lemma OAI.SquareDifference.kernelModelCoefficient_norm line 241
  21. lemma OAI.SquareDifference.kernelModelCoefficient_zero_of_denominator line 247
  22. lemma OAI.SquareDifference.bounded_kernel_model_center line 255
  23. lemma OAI.SquareDifference.stdAddChar_eq_expPhase line 274
  24. def OAI.SquareDifference.boundedSieveSets line 287
  25. def OAI.SquareDifference.sieveTermSign line 290
  26. def OAI.SquareDifference.sieveTermWeight line 292
  27. def OAI.SquareDifference.sieveTermPeriod line 295
  28. lemma OAI.SquareDifference.sieveTermPeriod_pos line 298
  29. lemma OAI.SquareDifference.sieveTermWeight_periodic line 303
  30. lemma OAI.SquareDifference.sieveTermWeight_norm line 308
  31. lemma OAI.SquareDifference.sieveTermSign_norm line 315
  32. lemma OAI.SquareDifference.actualDivisorWeight_eq_terms line 318
  33. lemma OAI.SquareDifference.sieveTermQuadratic_periodic line 330
  34. lemma OAI.SquareDifference.sieveTermCoefficient_eq line 342
  35. lemma OAI.SquareDifference.finiteRationalCoefficient_actual line 353
  36. lemma OAI.SquareDifference.finiteRationalCoefficient_actual_uniform line 368
  37. lemma OAI.SquareDifference.actualDivisorWeight_fourier line 380
  38. lemma OAI.SquareDifference.boundedSieveSets_card line 401
  39. lemma OAI.SquareDifference.sieveTermCost line 409
  40. def OAI.SquareDifference.actualSquareTransform line 430
  41. def OAI.SquareDifference.actualModelTransform line 433
  42. lemma OAI.SquareDifference.finiteSquareKernel_actual line 437
  43. lemma OAI.SquareDifference.actual_kernel_uniform line 450
  44. def OAI.SquareDifference.rationalGridPoint line 504
  45. lemma OAI.SquareDifference.rationalGridPoint_nonneg line 506
  46. lemma OAI.SquareDifference.rationalGridPoint_lt_one line 510
  47. lemma OAI.SquareDifference.rationalGridPoint_den_dvd line 515