OAI/Combinatorics/Progressions/FixedDensity/BoundaryBernoulli.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos3.FixedDensity.BoundaryBooleanCutAssignment line 11
  2. def OAI.Erdos3.FixedDensity.boundaryBooleanComponentCut line 15
  3. theorem OAI.Erdos3.FixedDensity.mem_boundaryBooleanComponentCut line 25
  4. def OAI.Erdos3.FixedDensity.boundaryBooleanCutSupport line 34
  5. theorem OAI.Erdos3.FixedDensity.mem_boundaryBooleanCutSupport line 44
  6. def OAI.Erdos3.FixedDensity.orderedBoundaryComponentCuts line 53
  7. theorem OAI.Erdos3.FixedDensity.boundaryBooleanComponentCut_mem_orderedBoundaryComponentCuts line 66
  8. def OAI.Erdos3.FixedDensity.refineOrderedFacePartitionsByBoundaryCut line 80
  9. theorem OAI.Erdos3.FixedDensity.refineOrderedFacePartitionsByBoundaryCut_refines line 92
  10. theorem OAI.Erdos3.FixedDensity.refineOrderedFacePartitionsByBoundaryCut_le_component line 103
  11. theorem OAI.Erdos3.FixedDensity.boundaryComponentBit_eq_of_mem_refined_part line 125
  12. theorem OAI.Erdos3.FixedDensity.orderedBoundaryPartition_refined_le_generatedSupport line 154
  13. theorem OAI.Erdos3.FixedDensity.orderedBoundaryPartition_refined_le_refineBy line 196
  14. def OAI.Erdos3.FixedDensity.orderedLayerAtomEnergy line 214
  15. theorem OAI.Erdos3.FixedDensity.orderedLayerAtomEnergy_nonneg line 222
  16. theorem OAI.Erdos3.FixedDensity.orderedLayerAtomEnergy_le_card line 232
  17. theorem OAI.Erdos3.FixedDensity.orderedLayerAtomEnergy_mono line 250
  18. theorem OAI.Erdos3.FixedDensity.orderedLayerAtomEnergy_increment_of_boundaryCut line 263
  19. def OAI.Erdos3.FixedDensity.IsPreliminaryOrderedRegular line 414
  20. theorem OAI.Erdos3.FixedDensity.exists_boundaryCut_of_not_preliminaryRegular line 429
  21. structure OAI.Erdos3.FixedDensity.PreliminaryIrregularWitness line 451
  22. def OAI.Erdos3.FixedDensity.chosenPreliminaryIrregularWitness line 468
  23. def OAI.Erdos3.FixedDensity.preliminaryOrderedRegularityStep line 488
  24. theorem OAI.Erdos3.FixedDensity.preliminaryOrderedRegularityStep_refines line 505
  25. theorem OAI.Erdos3.FixedDensity.preliminaryOrderedRegularityStep_energy_increment line 525
  26. def OAI.Erdos3.FixedDensity.preliminaryOrderedRegularityRun line 544
  27. theorem OAI.Erdos3.FixedDensity.preliminaryOrderedRegularityRun_zero line 558
  28. theorem OAI.Erdos3.FixedDensity.preliminaryOrderedRegularityRun_succ line 569
  29. theorem OAI.Erdos3.FixedDensity.preliminaryOrderedRegularityRun_refines line 581
  30. theorem OAI.Erdos3.FixedDensity.exists_preliminaryOrderedRegularityRun_index_before line 600
  31. theorem OAI.Erdos3.FixedDensity.exists_preliminaryOrderedRegular_refinement_before line 718
  32. theorem OAI.Erdos3.FixedDensity.card_orderedBoundaryComponentCuts_le line 744
  33. theorem OAI.Erdos3.FixedDensity.complexity_refineOrderedFacePartitionsByBoundaryCut_le line 764
  34. theorem OAI.Erdos3.FixedDensity.complexity_preliminaryOrderedRegularityStep_le line 802
  35. theorem OAI.Erdos3.FixedDensity.complexity_preliminaryOrderedRegularityRun_le line 826
  36. theorem OAI.Erdos3.FixedDensity.exists_preliminaryOrderedRegular_refinement_with_complexity_before line 865
  37. def OAI.Erdos3.FixedDensity.boundaryBooleanAssignmentOfBoolean line 907
  38. def OAI.Erdos3.FixedDensity.booleanAssignmentOfBoundary line 913
  39. theorem OAI.Erdos3.FixedDensity.booleanAssignmentOfBoundary_ofBoolean line 920
  40. theorem OAI.Erdos3.FixedDensity.boundaryBooleanAssignmentOfBoolean_ofBoundary line 930
  41. def OAI.Erdos3.FixedDensity.booleanBoundaryAssignmentEquiv line 938
  42. theorem OAI.Erdos3.FixedDensity.booleanAssignmentOfBoundary_equiv_apply line 948
  43. def OAI.Erdos3.FixedDensity.boundaryBernoulliWeight line 955
  44. theorem OAI.Erdos3.FixedDensity.sum_boundaryBernoulliWeight line 963
  45. theorem OAI.Erdos3.FixedDensity.boundaryBernoulliWeight_nonneg line 990
  46. theorem OAI.Erdos3.FixedDensity.boundaryBooleanComponentCut_eval line 1004
  47. theorem OAI.Erdos3.FixedDensity.eraseBoundaryCoordinate_eq_eraseCoordinate line 1024
  48. theorem OAI.Erdos3.FixedDensity.boundaryBooleanCutSupport_eq_booleanFaceCutSupport line 1030
  49. theorem OAI.Erdos3.FixedDensity.boundaryBooleanCutSupport_eval line 1043
  50. theorem OAI.Erdos3.FixedDensity.boundaryFactor_eq_sum_boolean line 1055
  51. theorem OAI.Erdos3.FixedDensity.boundaryCutProduct_eq_sum_boolean line 1091
  52. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.faceCutCorrelation_eq_sum_boundaryBoolean line 1119
  53. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.abs_faceCutCorrelation_le_of_boundaryBoolean line 1149
  54. def OAI.Erdos3.FixedDensity.IsPreliminaryOrderedBoundedRegular line 1188
  55. theorem OAI.Erdos3.FixedDensity.IsPreliminaryOrderedRegular.toBounded line 1200