OAI/Combinatorics/SquareDifference/UniformRates.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SquareDifference.rationalGridPoint_injective line 11
  2. lemma OAI.SquareDifference.exists_rationalGridPoint line 18
  3. def OAI.SquareDifference.rationalGrid line 45
  4. lemma OAI.SquareDifference.mem_rationalGrid line 48
  5. lemma OAI.SquareDifference.sum_rationalGrid line 59
  6. lemma OAI.SquareDifference.bounded_sum_eq_grid line 64
  7. lemma OAI.SquareDifference.bounded_sum_grid_of line 89
  8. lemma OAI.SquareDifference.prime_dvd_smallQuadraticModulus_iff line 107
  9. lemma OAI.SquareDifference.primary_cover_of_prime_support line 127
  10. lemma OAI.SquareDifference.smallProduct_primary_cover line 137
  11. lemma OAI.SquareDifference.root_active_div_smallProduct line 153
  12. lemma OAI.SquareDifference.kernelModelCoefficient_den_smallProduct line 161
  13. instance OAI.SquareDifference.smallProductNeZero line 172
  14. lemma OAI.SquareDifference.actualModelTransform_grid line 175
  15. def OAI.SquareDifference.smallTupleEquiv line 213
  16. def OAI.SquareDifference.smallCoordinateChar line 217
  17. lemma OAI.SquareDifference.smallCoordinateChar_trivial line 224
  18. lemma OAI.SquareDifference.smallCoordinateChar_primitive line 234
  19. lemma OAI.SquareDifference.smallCompleteLocal line 243
  20. lemma OAI.SquareDifference.completeRationalCoefficient_small line 267
  21. lemma OAI.SquareDifference.kernelModelCoefficient_small line 292
  22. lemma OAI.SquareDifference.pow_le_pow_of_one_le line 313
  23. lemma OAI.SquareDifference.kernel_rate_log line 316
  24. lemma OAI.SquareDifference.kernel_rate_first line 329
  25. lemma OAI.SquareDifference.kernel_rate_sqrt line 367
  26. lemma OAI.SquareDifference.kernel_rate_second line 397
  27. lemma OAI.SquareDifference.kernel_rate_third line 415
  28. lemma OAI.SquareDifference.kernel_all_rates line 433
  29. lemma OAI.SquareDifference.kernel_parameter_bounds line 462
  30. lemma OAI.SquareDifference.exists_kernel_threshold line 504
  31. lemma OAI.SquareDifference.natural_sqrt_bounds line 515
  32. lemma OAI.SquareDifference.rootProduct_le_squareModulus line 534
  33. def OAI.SquareDifference.kernelAbsoluteConstant line 546
  34. lemma OAI.SquareDifference.actual_kernel_power_error line 548