OAI/Combinatorics/Progressions/FixedDensity/SourceFullOrderedRemoval.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FixedDensity.topPositiveOrderedFace line 9
  2. theorem OAI.Erdos3.FixedDensity.topPositiveOrderedFace_rank line 16
  3. theorem OAI.Erdos3.FixedDensity.topPositiveOrderedFace_lowerRank_succ line 22
  4. theorem OAI.Erdos3.FixedDensity.partialConfigurationWeight_univ_eq_zero_of_not_occurrence line 29
  5. theorem OAI.Erdos3.FixedDensity.partialConfigurationWeight_univ_le_patternWeight line 65
  6. theorem OAI.Erdos3.FixedDensity.fullConfigurationCount_le_patternCount line 85
  7. theorem OAI.Erdos3.FixedDensity.orderedBadBaseDeletionFamily_isCover_of_good_count line 102
  8. theorem OAI.Erdos3.FixedDensity.orderedBadBaseDeletionFamily_isCover line 145
  9. def OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.sourceFullAtomDefectSq line 197
  10. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.sourceFullAtomDefectSq_nonneg line 212
  11. def OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.sourceFullLargeDefectBaseSupport line 223
  12. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.mem_sourceFullLargeDefectBaseSupport line 236
  13. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.mul_mean_indicator_sourceFullLargeDefectBaseSupport_le line 254
  14. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.mul_mean_indicator_sourceFullLargeDefectBaseSupport_le_atomEnergy_sub line 272
  15. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.mean_indicator_sourceFullLargeDefectBaseSupport_le line 309
  16. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.orderedAtomEnergy_sub_eq_sum_mean_sourceFullAtomDefectSq line 325
  17. def OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.sourceFullAtomBadBaseSupport line 344
  18. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.mem_sourceFullAtomBadBaseSupport line 359
  19. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.mean_indicator_atom_inter_sourceFullAtomBadBaseSupport_le line 380
  20. def OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.sourceFullOwnAtomBadBaseSupport line 423
  21. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.mem_sourceFullOwnAtomBadBaseSupport line 437
  22. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.mean_indicator_sourceFullOwnAtomBadBaseSupport_le line 469
  23. def OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.sourceFullCoarseOwnAtomBadBaseSupport line 521
  24. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.mem_sourceFullCoarseOwnAtomBadBaseSupport line 532
  25. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.mean_indicator_sourceFullCoarseOwnAtomBadBaseSupport_le line 548
  26. theorem OAI.Erdos3.FixedDensity.sourceFullMixedDefect_eq_orderedAtomBoundaryDefect_of_mem line 568
  27. theorem OAI.Erdos3.FixedDensity.conditionalMean_sourceFullMixedDefect_sq_eq line 604
  28. def OAI.Erdos3.FixedDensity.ClosedOrderedAtomConfiguration.AvoidsSourceFullBadBases line 629
  29. theorem OAI.Erdos3.FixedDensity.ClosedOrderedAtomConfiguration.sourceFullMixedGoodAtFace_of_not_mem_badBase line 640
  30. theorem OAI.Erdos3.FixedDensity.ClosedOrderedAtomConfiguration.isSourceFullMixedGood_of_avoids_badBases line 716
  31. def OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.sourceFullTopBadBaseDeletion line 743
  32. def OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.sourceFullBadBaseDeletionFamily line 761
  33. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.mean_indicator_sourceFullTopBadBaseDeletion_le line 769
  34. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.faceDeletionDensity_sourceFullBadBaseDeletionFamily_le line 828
  35. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.faceDeletionDensity_sourceFullBadBaseDeletionFamily_le_fineGap line 858
  36. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.faceDeletionDensity_sourceFullBadBaseDeletionFamily_constant_le line 911
  37. theorem OAI.Erdos3.FixedDensity.ClosedOrderedAtomConfiguration.isSourceFullMixedGood_of_avoids_sourceFullTopBadBaseDeletion line 988
  38. theorem OAI.Erdos3.FixedDensity.sourceFullBadBaseDeletionFamily_isCover_of_sourceFullMixedGood_count line 1024