OAI/Combinatorics/Progressions/Estimates/BooleanCubeModeWitness.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.booleanCoefficient line 15
  2. theorem OAI.Erdos3.sum_powerset_neg_one_pow_card_ring line 19
  3. theorem OAI.Erdos3.boolean_interval_alternating_sum line 24
  4. theorem OAI.Erdos3.booleanCoefficient_monomial line 64
  5. theorem OAI.Erdos3.booleanCoefficient_sum line 80
  6. theorem OAI.Erdos3.booleanCoefficient_const_mul line 87
  7. theorem OAI.Erdos3.booleanCoefficient_map line 95
  8. theorem OAI.Erdos3.booleanCoefficient_add line 110
  9. theorem OAI.Erdos3.booleanCoefficient_const line 115
  10. theorem OAI.Erdos3.booleanCoefficient_div line 122
  11. abbrev OAI.Erdos3.BooleanCubeKernel.Variable line 138
  12. inductive OAI.Erdos3.BooleanCubeKernel.Form line 140
  13. def OAI.Erdos3.BooleanCubeKernel.site line 144
  14. def OAI.Erdos3.BooleanCubeKernel.formPolynomial line 150
  15. def OAI.Erdos3.BooleanCubeKernel.formProduct line 155
  16. theorem OAI.Erdos3.BooleanCubeKernel.formProduct_nil line 159
  17. theorem OAI.Erdos3.BooleanCubeKernel.formProduct_cons line 162
  18. theorem OAI.Erdos3.BooleanCubeKernel.formPolynomial_homogeneous line 166
  19. theorem OAI.Erdos3.BooleanCubeKernel.formProduct_homogeneous line 172
  20. def OAI.Erdos3.BooleanCubeKernel.vanishingSpan line 180
  21. theorem OAI.Erdos3.BooleanCubeKernel.formProduct_mem_vanishingSpan line 185
  22. theorem OAI.Erdos3.BooleanCubeKernel.vanishingSpan_eval_zero line 190
  23. theorem OAI.Erdos3.BooleanCubeKernel.vanishingSpan_mul_form line 199
  24. theorem OAI.Erdos3.booleanCoefficient_sub_bound line 226
  25. def OAI.Erdos3.booleanSiteJets line 243
  26. theorem OAI.Erdos3.booleanSiteJets_lipschitz line 247
  27. def OAI.Erdos3.BooleanCubeKernel.normalMonomial line 278
  28. def OAI.Erdos3.BooleanCubeKernel.normalWord line 281
  29. theorem OAI.Erdos3.BooleanCubeKernel.normalWord_length line 285
  30. theorem OAI.Erdos3.BooleanCubeKernel.normalWord_product line 291
  31. theorem OAI.Erdos3.BooleanCubeKernel.normalMonomial_eval line 298
  32. theorem OAI.Erdos3.BooleanCubeKernel.normalMonomial_jet line 308
  33. theorem OAI.Erdos3.BooleanCubeKernel.normalMonomial_homogeneous line 315
  34. def OAI.Erdos3.BooleanCubeKernel.normalSpan line 320
  35. theorem OAI.Erdos3.BooleanCubeKernel.normalMonomial_mem line 324
  36. theorem OAI.Erdos3.BooleanCubeKernel.normalMonomial_mul_root line 329
  37. theorem OAI.Erdos3.BooleanCubeKernel.normalMonomial_mul_new line 335
  38. theorem OAI.Erdos3.BooleanCubeKernel.normalMonomial_mul_coordinate line 342
  39. def OAI.Erdos3.polynomialLinearRow line 396
  40. def OAI.Erdos3.rowPolynomial line 399
  41. theorem OAI.Erdos3.homogeneous_eq_rowPolynomial line 402
  42. theorem OAI.Erdos3.rowPolynomial_eval line 425
  43. theorem OAI.Erdos3.homogeneous_eval_eq_row line 429
  44. theorem OAI.Erdos3.BooleanCubeKernel.normalSpan_mul_coordinate line 448
  45. theorem OAI.Erdos3.BooleanCubeKernel.reductionSpace_mul_coordinate line 463
  46. theorem OAI.Erdos3.BooleanCubeKernel.reductionSpace_mul_linear line 472
  47. theorem OAI.Erdos3.BooleanCubeKernel.homogeneous_mem_reductionSpace line 491
  48. def OAI.Erdos3.BooleanCubeKernel.siteEvaluation line 529
  49. def OAI.Erdos3.BooleanCubeKernel.coefficientLinear line 535
  50. def OAI.Erdos3.BooleanCubeKernel.interpolation line 540
  51. theorem OAI.Erdos3.BooleanCubeKernel.interpolation_apply line 543
  52. theorem OAI.Erdos3.BooleanCubeKernel.interpolation_normalMonomial line 554
  53. theorem OAI.Erdos3.BooleanCubeKernel.interpolation_eq_of_mem_normalSpan line 568
  54. theorem OAI.Erdos3.BooleanCubeKernel.normalSpan_eq_zero_of_eval_zero line 578
  55. theorem OAI.Erdos3.BooleanCubeKernel.homogeneous_vanishing_mem_span line 583
  56. theorem OAI.Erdos3.BooleanCubeKernel.remainder_mem_vanishingSpan line 609
  57. theorem OAI.Erdos3.BooleanCubeKernel.map_vanishingSpan_eq_zero line 617
  58. theorem OAI.Erdos3.BooleanCubeKernel.factor_through_sites_of_kills_products line 629
  59. theorem OAI.Erdos3.BooleanCubeKernel.exists_vanishing_product_of_nonfactor line 639
  60. theorem OAI.Erdos3.BooleanCubeKernel.exists_vector_vanishing_product line 652