OAI/Combinatorics/Progressions/FixedDensity/OrderedConfigurationCounting.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.FixedDensity.PositiveOrderedFace line 11
  2. def OAI.Erdos3.FixedDensity.PositiveOrderedFace.equivSigma line 18
  3. instance OAI.Erdos3.FixedDensity.PositiveOrderedFace.instFintype line 26
  4. def OAI.Erdos3.FixedDensity.PositiveOrderedFace.rank line 32
  5. theorem OAI.Erdos3.FixedDensity.PositiveOrderedFace.rank_pos line 36
  6. def OAI.Erdos3.FixedDensity.PositiveOrderedFace.boundary line 40
  7. theorem OAI.Erdos3.FixedDensity.PositiveOrderedFace.boundary_lowerRank line 56
  8. theorem OAI.Erdos3.FixedDensity.PositiveOrderedFace.boundary_rank_lt line 65
  9. theorem OAI.Erdos3.FixedDensity.PositiveOrderedFace.orderedFaceTuple_boundary line 74
  10. def OAI.Erdos3.FixedDensity.IsDownwardClosedPositiveFaces line 98
  11. theorem OAI.Erdos3.FixedDensity.downwardClosed_empty line 106
  12. theorem OAI.Erdos3.FixedDensity.downwardClosed_univ line 113
  13. theorem OAI.Erdos3.FixedDensity.exists_maxRank_mem line 120
  14. theorem OAI.Erdos3.FixedDensity.IsDownwardClosedPositiveFaces.erase_maxRank line 154
  15. theorem OAI.Erdos3.FixedDensity.exists_positiveFace_coordinate_not_mem_range line 172
  16. def OAI.Erdos3.FixedDensity.positiveFaceMissingCoordinate line 214
  17. theorem OAI.Erdos3.FixedDensity.positiveFaceMissingCoordinate_not_mem_range line 223
  18. theorem OAI.Erdos3.FixedDensity.orderedFaceTuple_split_update_eq_of_missing line 233
  19. theorem OAI.Erdos3.FixedDensity.orderedFaceTuple_split_insertErased_eq_of_missing line 284
  20. def OAI.Erdos3.FixedDensity.configurationFaceWeight line 305
  21. theorem OAI.Erdos3.FixedDensity.configurationFaceWeight_nonneg line 316
  22. theorem OAI.Erdos3.FixedDensity.configurationFaceWeight_le_one line 326
  23. def OAI.Erdos3.FixedDensity.partialConfigurationWeight line 336
  24. def OAI.Erdos3.FixedDensity.partialConfigurationCount line 347
  25. def OAI.Erdos3.FixedDensity.fullConfigurationCount line 355
  26. theorem OAI.Erdos3.FixedDensity.partialConfigurationWeight_empty line 363
  27. theorem OAI.Erdos3.FixedDensity.partialConfigurationCount_empty line 373
  28. theorem OAI.Erdos3.FixedDensity.partialConfigurationWeight_nonneg line 382
  29. theorem OAI.Erdos3.FixedDensity.partialConfigurationWeight_le_one line 394
  30. theorem OAI.Erdos3.FixedDensity.orderedFaceTuple_split_insertNth_erase_eq_of_missing line 409
  31. def OAI.Erdos3.FixedDensity.configurationMissingCoordinate line 425
  32. theorem OAI.Erdos3.FixedDensity.configurationMissingCoordinate_not_mem_range line 438
  33. def OAI.Erdos3.FixedDensity.configurationRemainderCutTest line 453
  34. theorem OAI.Erdos3.FixedDensity.configurationRemainderCutTest_bounded line 475
  35. theorem OAI.Erdos3.FixedDensity.cutTestProduct_configurationRemainderCutTest line 507
  36. def OAI.Erdos3.FixedDensity.positiveFaceLowerLayer line 575
  37. def OAI.Erdos3.FixedDensity.configurationCoarseDensity line 583
  38. def OAI.Erdos3.FixedDensity.configurationFineDensity line 597
  39. def OAI.Erdos3.FixedDensity.configurationDefect line 612
  40. def OAI.Erdos3.FixedDensity.configurationUniform line 622
  41. def OAI.Erdos3.FixedDensity.configurationBoundaryIndicator line 632
  42. theorem OAI.Erdos3.FixedDensity.configurationCoarseDensity_nonneg line 647
  43. theorem OAI.Erdos3.FixedDensity.configurationCoarseDensity_le_one line 657
  44. theorem OAI.Erdos3.FixedDensity.configurationBoundaryIndicator_nonneg line 667
  45. theorem OAI.Erdos3.FixedDensity.configurationBoundaryIndicator_le_one line 677
  46. theorem OAI.Erdos3.FixedDensity.configurationFaceWeight_decompose line 687
  47. theorem OAI.Erdos3.FixedDensity.coarse_boundary_mem_of_boundary_weight_ne_zero line 701
  48. theorem OAI.Erdos3.FixedDensity.configurationBoundaryIndicator_mul_remainder line 765
  49. def OAI.Erdos3.FixedDensity.configurationContribution line 832
  50. theorem OAI.Erdos3.FixedDensity.partialConfigurationWeight_eq_face_mul_erase line 844
  51. theorem OAI.Erdos3.FixedDensity.partialConfigurationCount_decompose line 863
  52. theorem OAI.Erdos3.FixedDensity.configurationFace_isFaceCutRegular line 897
  53. theorem OAI.Erdos3.FixedDensity.ClosedOrderedAtomConfiguration.IsGood.atPositiveFace line 920
  54. theorem OAI.Erdos3.FixedDensity.configurationContribution_uniform_eq_mean_faceCutCorrelation line 939
  55. theorem OAI.Erdos3.FixedDensity.abs_configurationContribution_uniform_le line 974
  56. theorem OAI.Erdos3.FixedDensity.configurationDefect_mul_boundaryIndicator line 1025
  57. theorem OAI.Erdos3.FixedDensity.mean_sq_configurationDefect_mul_boundaryIndicator line 1079
  58. theorem OAI.Erdos3.FixedDensity.orderedBoundaryAtomMass_le_one line 1109
  59. theorem OAI.Erdos3.FixedDensity.mean_sq_partialConfigurationWeight_le_one line 1120
  60. theorem OAI.Erdos3.FixedDensity.configurationContribution_defect_eq_localized line 1134
  61. theorem OAI.Erdos3.FixedDensity.configurationContribution_defect_sq_le line 1157
  62. theorem OAI.Erdos3.FixedDensity.abs_configurationContribution_defect_le line 1259
  63. theorem OAI.Erdos3.FixedDensity.abs_partialConfigurationCount_sub_coarseDensity_mul_le line 1290
  64. def OAI.Erdos3.FixedDensity.extendedConfigurationCount line 1349
  65. theorem OAI.Erdos3.FixedDensity.extendedConfigurationCount_empty line 1363
  66. theorem OAI.Erdos3.FixedDensity.extendedConfigurationCount_univ line 1373
  67. theorem OAI.Erdos3.FixedDensity.configurationCoarseDensity_lower line 1384
  68. theorem OAI.Erdos3.FixedDensity.extendedConfigurationCount_step line 1395
  69. theorem OAI.Erdos3.FixedDensity.fullConfigurationCount_lower_bound line 1498
  70. theorem OAI.Erdos3.FixedDensity.fullConfigurationCount_pos line 1558