OAI/Combinatorics/SquareDifference/DualCoordinates.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SquareDifference.cyclicChar line 19
  2. lemma OAI.SquareDifference.cyclicChar_sub_right line 21
  3. lemma OAI.SquareDifference.cyclicChar_neg line 26
  4. lemma OAI.SquareDifference.cyclicChar_symm line 29
  5. lemma OAI.SquareDifference.cyclicChar_expect line 32
  6. lemma OAI.SquareDifference.cyclicChar_orthogonal line 41
  7. def OAI.SquareDifference.cyclicPolynomial line 51
  8. def OAI.SquareDifference.cyclicFourier line 54
  9. lemma OAI.SquareDifference.cyclicPolynomial_parseval line 57
  10. lemma OAI.SquareDifference.cyclicFourier_reconstruction line 74
  11. lemma OAI.SquareDifference.cyclicFourier_parseval line 97
  12. lemma OAI.SquareDifference.cyclicFourier_neg line 102
  13. lemma OAI.SquareDifference.cyclic_bilinear_fourier line 106
  14. lemma OAI.SquareDifference.cyclic_bilinear_multiplier line 120
  15. lemma OAI.SquareDifference.cyclic_bilinear_counting line 144
  16. lemma OAI.SquareDifference.cyclic_bilinear_normalized line 173
  17. lemma OAI.SquareDifference.cyclicChar_nat line 194
  18. def OAI.SquareDifference.cyclicPush line 204
  19. lemma OAI.SquareDifference.cyclicPush_transform line 207
  20. lemma OAI.SquareDifference.cyclicPush_point line 218
  21. lemma OAI.SquareDifference.cyclicPush_bilinear_zero line 230
  22. lemma OAI.SquareDifference.cyclic_interval_injective line 243
  23. lemma OAI.SquareDifference.cyclic_interval_point line 253
  24. def OAI.SquareDifference.intervalFourier line 275
  25. def OAI.SquareDifference.intervalModelWeight line 278
  26. lemma OAI.SquareDifference.intervalModel_bilinear line 282
  27. lemma OAI.SquareDifference.cyclic_square_transform line 350
  28. lemma OAI.SquareDifference.cyclic_model_transform line 364
  29. lemma OAI.SquareDifference.ordered_square_kernel_bilinear line 389
  30. lemma OAI.SquareDifference.actual_kernel_ordered_bilinear line 437
  31. def OAI.SquareDifference.standardCharEquiv line 477
  32. lemma OAI.SquareDifference.standardCharEquiv_apply line 486
  33. lemma OAI.SquareDifference.standardCharEquiv_symm_apply line 489
  34. lemma OAI.SquareDifference.standardCharEquiv_zero line 493
  35. lemma OAI.SquareDifference.rationalGrid_char line 497
  36. def OAI.SquareDifference.dualCRTCoordinates line 528
  37. lemma OAI.SquareDifference.dualCRTCoordinates_char line 533
  38. lemma OAI.SquareDifference.dualCRTCoordinates_product line 539
  39. lemma OAI.SquareDifference.dualCRTCoordinates_injective line 546
  40. def OAI.SquareDifference.dualCRTEquiv line 555
  41. lemma OAI.SquareDifference.dualCRT_nat line 560
  42. def OAI.SquareDifference.smallDualEquiv line 588
  43. lemma OAI.SquareDifference.smallCoordinateChar_grid line 592
  44. lemma OAI.SquareDifference.smallDual_active line 601
  45. lemma OAI.SquareDifference.smallDual_support line 620
  46. lemma OAI.SquareDifference.kernelModelCoefficient_dual line 632