OAI/Combinatorics/SumProduct/Alignment/BooleanRough01.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BooleanRough.Raise line 23
  2. lemma OAI.BooleanRough.sum_raise_rank line 27
  3. lemma OAI.BooleanRough.sum_raise_rank_zero line 68
  4. lemma OAI.BooleanRough.alternating_powerset line 82
  5. lemma OAI.BooleanRough.powerset_sdiff_filter line 88
  6. lemma OAI.BooleanRough.complement_mobius line 95
  7. theorem OAI.BooleanRough.raise_injective_below_middle line 121
  8. def OAI.BooleanRough.WeightedRaise line 165
  9. lemma OAI.BooleanRough.weighted_raise_rescale line 168
  10. lemma OAI.BooleanRough.weighted_raise_injective line 180
  11. def OAI.BooleanRough.LinMul line 199
  12. def OAI.BooleanRough.DegreeLE line 202
  13. lemma OAI.BooleanRough.weighted_raise_top line 205
  14. theorem OAI.BooleanRough.linMul_injective_low_degree line 232
  15. lemma OAI.BooleanRough.map_linMul line 258
  16. lemma OAI.BooleanRough.intCast_linMul line 263
  17. lemma OAI.BooleanRough.linMul_scalar line 269
  18. def OAI.BooleanRough.Clears line 279
  19. def OAI.BooleanRough.IntegralCoeffs line 282
  20. lemma OAI.BooleanRough.clear_divide_prime line 287
  21. theorem OAI.BooleanRough.integral_of_linMul_integral line 342
  22. def OAI.BooleanRough.Eval line 366
  23. lemma OAI.BooleanRough.eval_weightedRaise line 369
  24. lemma OAI.BooleanRough.eval_linMul line 399
  25. lemma OAI.BooleanRough.eval_integral_of_coeffs line 416
  26. lemma OAI.BooleanRough.integral_coeffs_of_eval line 423
  27. lemma OAI.BooleanRough.degree_linMul line 449
  28. def OAI.BooleanRough.LinPow line 459
  29. lemma OAI.BooleanRough.eval_linPow line 463
  30. lemma OAI.BooleanRough.degree_linPow line 470
  31. lemma OAI.BooleanRough.clears_linMul line 477
  32. lemma OAI.BooleanRough.clears_linPow line 486
  33. theorem OAI.BooleanRough.integral_of_linPow_integral line 494
  34. theorem OAI.BooleanRough.integral_of_power_vertex_integral line 510
  35. lemma OAI.BooleanRough.sum_subset_incidence line 524
  36. def OAI.BooleanRough.Mobius line 559
  37. lemma OAI.BooleanRough.eval_mobius line 562
  38. lemma OAI.BooleanRough.eval_injective line 591
  39. lemma OAI.BooleanRough.mobius_eval line 610
  40. def OAI.BooleanRough.Interp line 616
  41. lemma OAI.BooleanRough.degree_interp line 619
  42. lemma OAI.BooleanRough.eval_interp_low line 623
  43. lemma OAI.BooleanRough.map_eval line 631
  44. lemma OAI.BooleanRough.map_mobius line 635
  45. lemma OAI.BooleanRough.map_interp line 639
  46. lemma OAI.BooleanRough.mobius_scalar line 644
  47. lemma OAI.BooleanRough.interp_sub line 652
  48. lemma OAI.BooleanRough.interp_eval_degree line 659
  49. lemma OAI.BooleanRough.clears_interp line 666
  50. lemma OAI.BooleanRough.abs_mobius_le line 680
  51. lemma OAI.BooleanRough.abs_interp_le line 690
  52. lemma OAI.BooleanRough.abs_eval_interp_le line 700
  53. lemma OAI.BooleanRough.eval_interp_error line 716
  54. lemma OAI.BooleanRough.clears_eval line 725
  55. lemma OAI.BooleanRough.denominator_clears_div line 732
  56. lemma OAI.BooleanRough.rational_exact_of_small line 745
  57. theorem OAI.BooleanRough.rough_rounding_local line 762
  58. theorem OAI.BooleanRough.rough_rounding line 875
  59. lemma OAI.BooleanRough.mobius_sub line 891
  60. lemma OAI.BooleanRough.eval_constant_coeff line 895
  61. lemma OAI.BooleanRough.mobius_const line 900
  62. theorem OAI.BooleanRough.constant_rounding line 908