OAI/Combinatorics/Progressions/FixedDensity/OrderedAtomEnergy.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FixedDensity.FaceRegularityState.familyEnergy line 16
  2. def OAI.Erdos3.FixedDensity.FaceRegularityState.IsFamilyRegularAgainst line 20
  3. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.familyEnergy_nonneg line 25
  4. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.familyEnergy_le_card line 32
  5. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.familyEnergy_mono line 46
  6. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.familyEnergy_refineBy_increment line 56
  7. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.exists_index_booleanCut_of_not_familyRegular line 94
  8. structure OAI.Erdos3.FixedDensity.FaceRegularityState.FamilyIrregularWitness line 107
  9. def OAI.Erdos3.FixedDensity.FaceRegularityState.chosenFamilyIrregularWitness line 116
  10. def OAI.Erdos3.FixedDensity.FaceRegularityState.chosenFamilyIrregularCut line 133
  11. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.chosenFamilyIrregularCut_mem line 142
  12. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.exists_chosenFamilyIrregularCut_correlation line 151
  13. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.familyEnergy_increment_chosenFamilyCut line 164
  14. def OAI.Erdos3.FixedDensity.FaceRegularityState.familyRegularityRun line 179
  15. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.familyRegularityRun_zero line 189
  16. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.familyRegularityRun_succ line 196
  17. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.familyRegularityRun_partition_le line 205
  18. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.familyRegularityRun_complexity_le line 219
  19. def OAI.Erdos3.FixedDensity.FaceRegularityState.familyRegularityRunCuts line 246
  20. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.familyRegularityRunCuts_zero line 256
  21. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.familyRegularityRunCuts_succ line 263
  22. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.chosenFamilyIrregularCut_mem_of_empty_mem line 274
  23. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.familyRegularityRunCuts_subset line 284
  24. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.familyRegularityRun_partition_eq_join_generatedBy line 295
  25. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.exists_familyRegular_run_index_before line 347
  26. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.exists_familyRegular_refinement_with_generators_before line 422
  27. def OAI.Erdos3.FixedDensity.FaceRegularityState.IsFaceCutRegularFamily line 456
  28. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.isFaceCutRegularFamily_of_familyRegularAgainst_supports line 462
  29. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.exists_faceCutRegularFamily_refinement_with_generators_before line 474
  30. def OAI.Erdos3.FixedDensity.partitionAtomIndicator line 521
  31. theorem OAI.Erdos3.FixedDensity.partitionAtomIndicator_of_mem line 528
  32. theorem OAI.Erdos3.FixedDensity.partitionAtomIndicator_of_not_mem line 536
  33. theorem OAI.Erdos3.FixedDensity.partitionAtomIndicator_nonneg line 543
  34. theorem OAI.Erdos3.FixedDensity.partitionAtomIndicator_le_one line 549
  35. theorem OAI.Erdos3.FixedDensity.partitionAtomIndicator_sq line 555
  36. theorem OAI.Erdos3.FixedDensity.sum_partitionAtomIndicator line 562
  37. theorem OAI.Erdos3.FixedDensity.conditionalMean_fintype_sum line 584
  38. theorem OAI.Erdos3.FixedDensity.sum_conditionalMean_partitionAtomIndicator line 595
  39. def OAI.Erdos3.FixedDensity.partitionAtomEnergy line 606
  40. theorem OAI.Erdos3.FixedDensity.partitionAtomEnergy_nonneg line 613
  41. theorem OAI.Erdos3.FixedDensity.partitionAtomEnergy_le_one line 622
  42. theorem OAI.Erdos3.FixedDensity.partitionAtomEnergy_mono line 661
  43. theorem OAI.Erdos3.FixedDensity.partitionAtomEnergy_sub_eq_sum_mean_sq line 672
  44. def OAI.Erdos3.FixedDensity.orderedAtomEnergy line 688
  45. theorem OAI.Erdos3.FixedDensity.orderedAtomEnergy_nonneg line 696
  46. theorem OAI.Erdos3.FixedDensity.orderedAtomEnergy_le_one line 705
  47. theorem OAI.Erdos3.FixedDensity.orderedAtomEnergy_mono line 714
  48. theorem OAI.Erdos3.FixedDensity.orderedAtomEnergy_sub_eq_sum_mean_sq line 726