OAI/Combinatorics/SquareDifference/RationalApproximation.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SquareDifference.sum_square_cells line 10
  2. lemma OAI.SquareDifference.square_cell_card line 19
  3. lemma OAI.SquareDifference.square_phase_cell line 23
  4. lemma OAI.SquareDifference.square_phase_riemann line 59
  5. def OAI.SquareDifference.normalizedLinearSum line 69
  6. lemma OAI.SquareDifference.squareWeight_riemann line 72
  7. lemma OAI.SquareDifference.rational_quadratic_sum line 108
  8. lemma OAI.SquareDifference.quadratic_sum_shift line 123
  9. lemma OAI.SquareDifference.norm_linear_weighted_sum line 130
  10. lemma OAI.SquareDifference.rational_weighted_quadratic_sum line 160
  11. lemma OAI.SquareDifference.periodic_square_main line 183
  12. lemma OAI.SquareDifference.quadratic_fourier_weight line 211
  13. lemma OAI.SquareDifference.dirichlet_fraction line 240
  14. lemma OAI.SquareDifference.rational_weighted_quadratic_uniform line 252
  15. lemma OAI.SquareDifference.rational_difference_lower line 280
  16. lemma OAI.SquareDifference.normalizedLinearSum_norm line 303
  17. lemma OAI.SquareDifference.normalizedLinearSum_distance line 311
  18. lemma OAI.SquareDifference.normalizedLinearSum_add_int line 321
  19. lemma OAI.SquareDifference.rational_approximation_separation line 332
  20. lemma OAI.SquareDifference.normalizedLinearSum_rational_bound line 349
  21. def OAI.SquareDifference.modelCenterCoefficient line 367
  22. lemma OAI.SquareDifference.rational_model_approximation line 372
  23. lemma OAI.SquareDifference.modelCenterCoefficient_zero line 400
  24. lemma OAI.SquareDifference.expPhase_rat_square_periodic line 413
  25. lemma OAI.SquareDifference.periodic_rational_quadratic line 427
  26. lemma OAI.SquareDifference.rational_kernel_major line 436
  27. lemma OAI.SquareDifference.rational_kernel_major_uniform line 462
  28. lemma OAI.SquareDifference.quadratic_fourier_weight_uniform line 496