OAI/Combinatorics/Progressions/FixedDensity/GeneratorCells.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos3.FixedDensity.BooleanCutTest line 13
  2. def OAI.Erdos3.FixedDensity.BooleanCutTest.eval line 18
  3. theorem OAI.Erdos3.FixedDensity.BooleanCutTest.eval_of_mem line 23
  4. theorem OAI.Erdos3.FixedDensity.BooleanCutTest.eval_of_not_mem line 29
  5. theorem OAI.Erdos3.FixedDensity.BooleanCutTest.eval_sq line 34
  6. theorem OAI.Erdos3.FixedDensity.BooleanCutTest.eval_nonneg line 39
  7. theorem OAI.Erdos3.FixedDensity.BooleanCutTest.eval_le_one line 44
  8. def OAI.Erdos3.FixedDensity.IsPartitionMeasurable line 50
  9. theorem OAI.Erdos3.FixedDensity.IsPartitionMeasurable.of_le line 55
  10. theorem OAI.Erdos3.FixedDensity.IsPartitionMeasurable.conditionalMean_eq line 61
  11. theorem OAI.Erdos3.FixedDensity.IsPartitionMeasurable.conditionalMean line 73
  12. theorem OAI.Erdos3.FixedDensity.booleanCut_measurable_generatedBy line 80
  13. structure OAI.Erdos3.FixedDensity.FaceRegularityState line 97
  14. abbrev OAI.Erdos3.FixedDensity.FaceRegularitySystem line 100
  15. def OAI.Erdos3.FixedDensity.FaceRegularityState.structured line 107
  16. def OAI.Erdos3.FixedDensity.FaceRegularityState.residual line 111
  17. def OAI.Erdos3.FixedDensity.FaceRegularityState.energy line 115
  18. def OAI.Erdos3.FixedDensity.FaceRegularityState.booleanCutCorrelation line 119
  19. def OAI.Erdos3.FixedDensity.FaceRegularityState.refineBy line 124
  20. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.partition_refineBy line 131
  21. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.refineBy_le line 138
  22. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.booleanCut_measurable_refineBy line 143
  23. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.complexity_refineBy_le line 151
  24. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.structured_nonneg line 173
  25. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.structured_le_one line 178
  26. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.conditionalMean_residual line 184
  27. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.mean_residual line 195
  28. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.conditionalMean_residual_refineBy line 203
  29. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.mean_mul_eq_mean_conditionalMean_mul line 217
  30. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.booleanCutCorrelation_eq_projection line 232
  31. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.mean_mul_sq_le_sq_mul_sq line 257
  32. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.mean_booleanCut_sq_le_one line 264
  33. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.energy_refineBy_sub_eq_mean_sq line 272
  34. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.booleanCutCorrelation_sq_le_energyIncrement line 282
  35. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.energy_increment_of_booleanCut line 310
  36. def OAI.Erdos3.FixedDensity.FaceRegularityState.IsRegularAgainst line 324
  37. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.exists_booleanCut_of_not_regular line 329
  38. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.energy_increment_budget line 342
  39. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.no_long_energy_increment_run line 386
  40. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.exists_regular_state_in_refinement_run line 400
  41. def OAI.Erdos3.FixedDensity.FaceRegularityState.chosenIrregularCut line 437
  42. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.chosenIrregularCut_mem line 448
  43. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.chosenIrregularCut_correlation line 458
  44. def OAI.Erdos3.FixedDensity.FaceRegularityState.regularityRun line 470
  45. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.regularityRun_zero line 480
  46. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.regularityRun_succ line 487
  47. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.regularityRun_partition_le line 497
  48. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.regularityRun_complexity_le line 513
  49. def OAI.Erdos3.FixedDensity.FaceRegularityState.regularityRunCuts line 542
  50. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.regularityRunCuts_zero line 553
  51. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.regularityRunCuts_succ line 560
  52. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.chosenIrregularCut_mem_of_empty_mem line 572
  53. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.regularityRunCuts_subset line 581
  54. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.regularityRun_partition_eq_join_generatedBy line 593
  55. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.exists_regular_run_index_before line 646
  56. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.exists_regular_refinement_before line 672
  57. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.exists_regular_refinement line 695
  58. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.exists_regular_refinement_allCuts line 723
  59. def OAI.Erdos3.FixedDensity.booleanFaceCutSupport line 758
  60. theorem OAI.Erdos3.FixedDensity.mem_booleanFaceCutSupport line 767
  61. theorem OAI.Erdos3.FixedDensity.booleanFaceCutSupport_eval line 774
  62. def OAI.Erdos3.FixedDensity.booleanFaceCutSupports line 803
  63. theorem OAI.Erdos3.FixedDensity.booleanFaceCutSupport_mem_supports line 809
  64. theorem OAI.Erdos3.FixedDensity.booleanFaceCutSupport_false line 817
  65. theorem OAI.Erdos3.FixedDensity.empty_mem_booleanFaceCutSupports line 835
  66. def OAI.Erdos3.FixedDensity.FaceRegularityState.faceCutCorrelation line 849
  67. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.faceCutCorrelation_boolean line 855
  68. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.faceCutCorrelation_eq_sum_boolean line 868
  69. def OAI.Erdos3.FixedDensity.FaceRegularityState.IsFaceCutRegular line 922
  70. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.isFaceCutRegular_of_regularAgainst_supports line 930
  71. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.exists_faceCutRegular_refinement line 973
  72. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.exists_faceCutRegular_refinement_with_generators_before line 997
  73. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.exists_faceCutRegular_refinement_with_generators line 1052
  74. def OAI.Erdos3.FixedDensity.representingBooleanFaceCutAssignment line 1100
  75. theorem OAI.Erdos3.FixedDensity.booleanFaceCutSupport_representing line 1116
  76. abbrev OAI.Erdos3.FixedDensity.GeneratorBranch line 1132
  77. theorem OAI.Erdos3.FixedDensity.card_generatorBranch line 1138
  78. def OAI.Erdos3.FixedDensity.lowerGeneratorCell line 1144
  79. theorem OAI.Erdos3.FixedDensity.mem_lowerGeneratorCell line 1160
  80. theorem OAI.Erdos3.FixedDensity.mem_generatedBy_part_iff_exists_lowerGeneratorCells line 1175