OAI/Combinatorics/Progressions/FixedDensity/OrderedGoodAtoms.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FixedDensity.partitionAtomAt line 11
  2. theorem OAI.Erdos3.FixedDensity.partitionAtomAt_val line 18
  3. theorem OAI.Erdos3.FixedDensity.partitionAtomAt_eq_iff_mem line 25
  4. theorem OAI.Erdos3.FixedDensity.partitionAtomAt_eq_iff_mem_part line 37
  5. theorem OAI.Erdos3.FixedDensity.partitionAtomIndicator_measurable line 45
  6. def OAI.Erdos3.FixedDensity.partitionAtomUnion line 71
  7. theorem OAI.Erdos3.FixedDensity.mem_partitionAtomUnion line 78
  8. theorem OAI.Erdos3.FixedDensity.mem_partitionAtomUnion_iff_atomAt_mem line 85
  9. theorem OAI.Erdos3.FixedDensity.selectedPartitionAtoms_pairwiseDisjoint line 104
  10. theorem OAI.Erdos3.FixedDensity.card_partitionAtomUnion line 114
  11. theorem OAI.Erdos3.FixedDensity.finsetIndicator_partitionAtomUnion line 122
  12. theorem OAI.Erdos3.FixedDensity.mean_finsetIndicator_partitionAtomUnion line 152
  13. theorem OAI.Erdos3.FixedDensity.partitionAtomUnion_indicator_measurable line 168
  14. theorem OAI.Erdos3.FixedDensity.mean_mul_partitionAtomIndicator line 191
  15. theorem OAI.Erdos3.FixedDensity.mean_mul_partitionAtomIndicator_le line 215
  16. def OAI.Erdos3.FixedDensity.smallAverageBaseAtoms line 227
  17. def OAI.Erdos3.FixedDensity.smallAverageBaseSupport line 235
  18. theorem OAI.Erdos3.FixedDensity.mem_smallAverageBaseSupport line 242
  19. theorem OAI.Erdos3.FixedDensity.mean_indicator_inter_smallAverageBaseSupport_le line 260
  20. def OAI.Erdos3.FixedDensity.largeAverageBaseAtoms line 305
  21. def OAI.Erdos3.FixedDensity.largeAverageBaseSupport line 313
  22. theorem OAI.Erdos3.FixedDensity.mem_largeAverageBaseSupport line 320
  23. theorem OAI.Erdos3.FixedDensity.mul_mean_indicator_largeAverageBaseSupport_le line 338
  24. theorem OAI.Erdos3.FixedDensity.mean_indicator_largeAverageBaseSupport_le line 362
  25. def OAI.Erdos3.FixedDensity.atomBoundaryDefect line 375
  26. def OAI.Erdos3.FixedDensity.atomBoundaryDefectSq line 382
  27. theorem OAI.Erdos3.FixedDensity.atomBoundaryDefectSq_nonneg line 388
  28. def OAI.Erdos3.FixedDensity.largeDefectBaseAtoms line 395
  29. def OAI.Erdos3.FixedDensity.largeDefectBaseSupport line 403
  30. theorem OAI.Erdos3.FixedDensity.mem_largeDefectBaseSupport line 412
  31. theorem OAI.Erdos3.FixedDensity.mean_atomBoundaryDefectSq_le_atomEnergy_sub line 424
  32. theorem OAI.Erdos3.FixedDensity.mul_mean_indicator_largeDefectBaseSupport_le_atomEnergy_sub line 445
  33. theorem OAI.Erdos3.FixedDensity.mean_indicator_largeDefectBaseSupport_le_atomEnergy_sub_div line 463
  34. def OAI.Erdos3.FixedDensity.atomBadBaseSupport line 478
  35. theorem OAI.Erdos3.FixedDensity.mean_indicator_inter_union_le_add line 487
  36. theorem OAI.Erdos3.FixedDensity.mean_indicator_atom_inter_badBaseSupport_le line 516
  37. def OAI.Erdos3.FixedDensity.orderedFaceAtomAt line 551
  38. theorem OAI.Erdos3.FixedDensity.orderedFaceAtomAt_val line 560
  39. theorem OAI.Erdos3.FixedDensity.orderedBoundaryAtomAt_eq_iff line 568
  40. def OAI.Erdos3.FixedDensity.orderedAtomBoundaryDefect line 608
  41. def OAI.Erdos3.FixedDensity.orderedBoundaryAtomMass line 620
  42. def OAI.Erdos3.FixedDensity.orderedLocalizedAtomDefectSq line 630
  43. theorem OAI.Erdos3.FixedDensity.orderedLocalizedAtomDefectSq_eq line 643
  44. theorem OAI.Erdos3.FixedDensity.orderedLocalizedAtomDefectSq_le line 665
  45. def OAI.Erdos3.FixedDensity.orderedLargeDefectBaseAtoms line 690
  46. def OAI.Erdos3.FixedDensity.orderedLargeDefectBaseSupport line 703
  47. def OAI.Erdos3.FixedDensity.orderedAtomBadBaseSupport line 716
  48. theorem OAI.Erdos3.FixedDensity.mul_mean_indicator_orderedLargeDefectBaseSupport_le line 729
  49. theorem OAI.Erdos3.FixedDensity.mean_indicator_orderedAtom_inter_badBaseSupport_le line 748
  50. def OAI.Erdos3.FixedDensity.OrderedAtomIsGoodAtBoundary line 768
  51. theorem OAI.Erdos3.FixedDensity.orderedAtomIsGoodAtBoundary_of_not_mem_badBase line 784
  52. theorem OAI.Erdos3.FixedDensity.OrderedAtomIsGoodAtBoundary.localized_defect line 822
  53. structure OAI.Erdos3.FixedDensity.ClosedOrderedAtomConfiguration line 857
  54. def OAI.Erdos3.FixedDensity.ClosedOrderedAtomConfiguration.ofTuple line 871
  55. theorem OAI.Erdos3.FixedDensity.ClosedOrderedAtomConfiguration.atom_eq_partitionAtomAt line 884
  56. def OAI.Erdos3.FixedDensity.ClosedOrderedAtomConfiguration.IsGoodAt line 897
  57. def OAI.Erdos3.FixedDensity.ClosedOrderedAtomConfiguration.IsGood line 915
  58. theorem OAI.Erdos3.FixedDensity.ClosedOrderedAtomConfiguration.isGoodAt_of_not_mem_badBase line 924
  59. theorem OAI.Erdos3.FixedDensity.ClosedOrderedAtomConfiguration.isGood_of_avoids_badBases line 953