OAI/Computability/MinUncut/Estimates/F2.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncut.BinaryFourier.F₂ line 16
  2. def OAI.MinUncut.BinaryFourier.sign line 18
  3. lemma OAI.MinUncut.BinaryFourier.sign_zero line 20
  4. lemma OAI.MinUncut.BinaryFourier.sign_one line 21
  5. lemma OAI.MinUncut.BinaryFourier.sign_sq line 22
  6. lemma OAI.MinUncut.BinaryFourier.sign_abs line 24
  7. lemma OAI.MinUncut.BinaryFourier.sign_add line 26
  8. lemma OAI.MinUncut.BinaryFourier.self_add line 33
  9. lemma OAI.MinUncut.BinaryFourier.neg_eq line 38
  10. lemma OAI.MinUncut.BinaryFourier.add_eq_zero_iff line 40
  11. def OAI.MinUncut.BinaryFourier.character line 43
  12. lemma OAI.MinUncut.BinaryFourier.character_zero line 45
  13. lemma OAI.MinUncut.BinaryFourier.character_at_zero line 47
  14. lemma OAI.MinUncut.BinaryFourier.character_sq line 49
  15. lemma OAI.MinUncut.BinaryFourier.character_abs line 51
  16. lemma OAI.MinUncut.BinaryFourier.character_add line 53
  17. lemma OAI.MinUncut.BinaryFourier.character_add_dual line 56
  18. lemma OAI.MinUncut.BinaryFourier.expect_translate line 63
  19. lemma OAI.MinUncut.BinaryFourier.character_mean line 66
  20. lemma OAI.MinUncut.BinaryFourier.character_orthogonality line 81
  21. lemma OAI.MinUncut.BinaryFourier.card_dual line 93
  22. lemma OAI.MinUncut.BinaryFourier.character_kernel line 101
  23. def OAI.MinUncut.BinaryFourier.coefficient line 120
  24. lemma OAI.MinUncut.BinaryFourier.inversion line 123
  25. lemma OAI.MinUncut.BinaryFourier.parseval_inner line 138
  26. lemma OAI.MinUncut.BinaryFourier.parseval line 157
  27. lemma OAI.MinUncut.BinaryFourier.add_add_cancel line 162
  28. lemma OAI.MinUncut.BinaryFourier.coefficient_translate line 165
  29. def OAI.MinUncut.BinaryFourier.convolution line 176
  30. lemma OAI.MinUncut.BinaryFourier.coefficient_convolution line 178
  31. lemma OAI.MinUncut.BinaryFourier.convolution_shifts line 203
  32. lemma OAI.MinUncut.BinaryFourier.square_fourier line 214
  33. lemma OAI.MinUncut.BinaryFourier.square_bound line 250
  34. lemma OAI.MinUncut.GaussianSmoothing.weighted_exp_derivative line 296
  35. lemma OAI.MinUncut.GaussianSmoothing.gaussianPDF_translate line 337
  36. lemma OAI.MinUncut.GaussianSmoothing.gaussian_translate_integral line 345
  37. lemma OAI.MinUncut.GaussianSmoothing.gaussian_translate_derivative line 361
  38. lemma OAI.MinUncut.GaussianSmoothing.gaussian_convolution_derivative line 374
  39. abbrev OAI.MinUncut.GaussianSmoothing.gamma line 395
  40. def OAI.MinUncut.GaussianSmoothing.split line 398
  41. lemma OAI.MinUncut.GaussianSmoothing.split_apply line 404
  42. lemma OAI.MinUncut.GaussianSmoothing.split_symm_apply line 408
  43. lemma OAI.MinUncut.GaussianSmoothing.split_measurePreserving line 412
  44. lemma OAI.MinUncut.GaussianSmoothing.integral_split line 420
  45. lemma OAI.MinUncut.GaussianSmoothing.split_affine_update line 428
  46. lemma OAI.MinUncut.GaussianSmoothing.product_convolution_derivative line 437
  47. lemma OAI.MinUncut.GaussianSmoothing.coordinate_memLp_two line 480
  48. lemma OAI.MinUncut.GaussianSmoothing.coordinate_second_moment line 484
  49. lemma OAI.MinUncut.GaussianSmoothing.integral_inner_toLp line 503
  50. lemma OAI.MinUncut.GaussianSmoothing.integral_bessel line 511
  51. lemma OAI.MinUncut.GaussianSmoothing.gaussian_score_energy line 528
  52. abbrev OAI.MinUncut.Inner.F₂ line 545
  53. abbrev OAI.MinUncut.Inner.Point line 549
  54. abbrev OAI.MinUncut.Inner.Row line 550
  55. def OAI.MinUncut.Inner.face line 552
  56. def OAI.MinUncut.Inner.faceSum line 554
  57. abbrev OAI.MinUncut.Inner.Code line 559
  58. instance OAI.MinUncut.Inner.codeFintype line 561
  59. instance OAI.MinUncut.Inner.codeDecidableEq line 562
  60. abbrev OAI.MinUncut.Inner.Forms line 566
  61. instance OAI.MinUncut.Inner.formsFintype line 569
  62. abbrev OAI.MinUncut.Inner.FaceArray line 573
  63. def OAI.MinUncut.Inner.labelCode line 576
  64. lemma OAI.MinUncut.Inner.labelCode_apply line 579
  65. structure OAI.MinUncut.Inner.FoldedProof line 582
  66. def OAI.MinUncut.Inner.bitSign line 586
  67. lemma OAI.MinUncut.Inner.bitSign_sq line 587
  68. lemma OAI.MinUncut.Inner.bitSign_abs line 588
  69. lemma OAI.MinUncut.Inner.bitSign_not line 589
  70. def OAI.MinUncut.Inner.query line 591
  71. def OAI.MinUncut.Inner.pullQuery line 595
  72. def OAI.MinUncut.Inner.gauss line 598
  73. instance OAI.MinUncut.Inner.gauss_probability line 601
  74. def OAI.MinUncut.Inner.smooth line 605
  75. def OAI.MinUncut.Inner.gradient line 611
  76. lemma OAI.MinUncut.Inner.measurable_query line 618
  77. lemma OAI.MinUncut.Inner.measurable_pullQuery line 630
  78. lemma OAI.MinUncut.Inner.measurable_answer line 636
  79. def OAI.MinUncut.Inner.tableSmooth line 643
  80. lemma OAI.MinUncut.Inner.measurable_tableSmooth line 647
  81. lemma OAI.MinUncut.Inner.tableSmooth_abs_le line 652
  82. lemma OAI.MinUncut.Inner.smooth_coordinate_derivative line 659
  83. lemma OAI.MinUncut.Inner.gradient_convolution line 667
  84. def OAI.MinUncut.Inner.spatialEnergy line 676
  85. lemma OAI.MinUncut.Inner.gradient_score line 679
  86. lemma OAI.MinUncut.Inner.gradient_spatialEnergy_le line 686
  87. lemma OAI.MinUncut.Inner.gradient_abs_le line 704