OAI/Combinatorics/Progressions/FixedDensity/Conclusions.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FixedDensity.HypergraphBundle.frozenProjectedEdgeOrderIso line 17
  2. def OAI.Erdos3.FixedDensity.HypergraphBundle.frozenOccurrenceOrderEquiv line 42
  3. def OAI.Erdos3.FixedDensity.HypergraphBundle.frozenBundleFaceTupleEquiv line 53
  4. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.frozenBundleFaceTupleEquiv_apply line 71
  5. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.frozenBundleFaceTupleEquiv_symm_apply line 88
  6. def OAI.Erdos3.FixedDensity.HypergraphBundle.frozenBundleMissingVertex line 102
  7. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.frozenBundleMissingVertex_not_mem line 118
  8. def OAI.Erdos3.FixedDensity.HypergraphBundle.frozenBundleMissingCoordinate line 133
  9. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.frozenOccurrenceOrder_missingCoordinate_not_mem line 145
  10. def OAI.Erdos3.FixedDensity.HypergraphBundle.frozenBundleInsertedSelectedTuple line 159
  11. def OAI.Erdos3.FixedDensity.HypergraphBundle.frozenBundleInsertedAssignment line 174
  12. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.splitEdgeEquiv_symm_apply_of_mem line 190
  13. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.splitEdgeEquiv_symm_apply_of_not_mem line 202
  14. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.edgeTuple_frozenBundleInsertedAssignment line 218
  15. def OAI.Erdos3.FixedDensity.HypergraphBundle.frozenBundleRemainderCutTest line 278
  16. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.frozenBundleRemainderCutTest_bounded line 302
  17. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.cutTestProduct_frozenBundleRemainderCutTest line 347
  18. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.hasOrderedConfigurationBundleFrozenCutRepresentation line 419
  19. theorem OAI.Erdos3.FixedDensity.orderedConfigurationBaseDensity_ge_of_sourceFullMixedGood line 455
  20. theorem OAI.Erdos3.FixedDensity.hasTaoBundleCountingStep_orderedConfiguration_of_sourceFull line 478
  21. theorem OAI.Erdos3.FixedDensity.abs_bundleCount_orderedConfiguration_sub_main_le_sourceFullEnvelope line 507
  22. theorem OAI.Erdos3.FixedDensity.one_sub_sourceFullEnvelope_mul_densityProduct_le_fullConfigurationCount line 558
  23. theorem OAI.Erdos3.FixedDensity.fullConfigurationCount_pos_of_sourceFullEnvelope_lt_half line 593
  24. theorem OAI.Erdos3.FixedDensity.orderedConfigurationInitialBundle_order_le line 635
  25. theorem OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.Certificate.isFullyMixedPreliminaryOrderedRegular_common line 644
  26. theorem OAI.Erdos3.FixedDensity.orderedConfigurationBaseDensity_ge_of_sourceFullMixedGood_rankwise line 661
  27. theorem OAI.Erdos3.FixedDensity.hasTaoBundleCountingStep_orderedConfiguration_of_sourceFull_rankwise line 689
  28. theorem OAI.Erdos3.FixedDensity.abs_bundleCount_orderedConfiguration_sub_main_le_rankwiseEnvelope line 716
  29. theorem OAI.Erdos3.FixedDensity.one_sub_rankwiseEnvelope_mul_densityProduct_le_fullConfigurationCount line 759
  30. theorem OAI.Erdos3.FixedDensity.half_rankwiseDensityProduct_le_fullConfigurationCount line 798
  31. theorem OAI.Erdos3.FixedDensity.half_rankwiseDensityProduct_le_fullConfigurationCount_of_rankBound line 866
  32. def OAI.Erdos3.FixedDensity.sourceBundleRemovalHorizon line 905
  33. def OAI.Erdos3.FixedDensity.sourceBundleRemovalDensityBudget line 909
  34. def OAI.Erdos3.FixedDensity.sourceBundleRemovalStep line 914
  35. def OAI.Erdos3.FixedDensity.sourceBundleRemovalKappa line 918
  36. theorem OAI.Erdos3.FixedDensity.sourceBundleRemovalDensityBudget_pos line 921
  37. theorem OAI.Erdos3.FixedDensity.sourceBundleRemovalDensityBudget_le_one line 927
  38. theorem OAI.Erdos3.FixedDensity.card_mul_two_sourceBundleRemovalDensityBudget_le line 941
  39. theorem OAI.Erdos3.FixedDensity.sourceBundleRemovalStep_pos line 965
  40. theorem OAI.Erdos3.FixedDensity.sourceBundleRemovalStep_le_one line 970
  41. theorem OAI.Erdos3.FixedDensity.sourceBundleRemovalKappa_pos line 980
  42. theorem OAI.Erdos3.FixedDensity.sourceBundleRemovalKappa_le_one line 985
  43. theorem OAI.Erdos3.FixedDensity.four_mul_sourceBundleRemovalKappa_le_step line 991
  44. theorem OAI.Erdos3.FixedDensity.sourceBundleRemovalKappa_sq_le_half_step line 997
  45. theorem OAI.Erdos3.FixedDensity.sourceBundleRemovalStep_total_le_quarter line 1005
  46. theorem OAI.Erdos3.FixedDensity.sourceBundleRemovalStep_total_le_one line 1023
  47. theorem OAI.Erdos3.FixedDensity.sourceBundleRemovalStep_total_lt_half line 1028
  48. def OAI.Erdos3.FixedDensity.sourceBundleRemovalCountThreshold line 1033
  49. theorem OAI.Erdos3.FixedDensity.sourceBundleRemovalCountThreshold_pos line 1039
  50. theorem OAI.Erdos3.FixedDensity.hasUniformOrderedPatternRemoval_sourceFull line 1046
  51. theorem OAI.Erdos3.FixedDensity.szemeredi line 1290