OAI/Combinatorics/Progressions/FixedDensity/CoarseAtomBridge.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.FixedDensity.coarseAtomOfFineAtom line 12
2. def OAI.Erdos3.FixedDensity.fineAtomsInCoarseAtom line 20
3. theorem OAI.Erdos3.FixedDensity.mem_fineAtomsInCoarseAtom line 31
4. theorem OAI.Erdos3.FixedDensity.fineAtom_subset_coarseAtomOfFineAtom line 40
5. theorem OAI.Erdos3.FixedDensity.coarseAtomOfFineAtom_partitionAtomAt line 53
6. theorem OAI.Erdos3.FixedDensity.partitionAtomUnion_fineAtomsInCoarseAtom line 73
7. theorem OAI.Erdos3.FixedDensity.partitionAtomIndicator_eq_sum_fineAtomsInCoarseAtom line 110
8. theorem OAI.Erdos3.FixedDensity.partitionAtomIndicator_eq_sum_fineAtomsInCoarseAtom_fun line 126
9. theorem OAI.Erdos3.FixedDensity.card_fineAtomsInCoarseAtom_le_complexity line 140
10. theorem OAI.Erdos3.FixedDensity.conditionalMean_finset_sum line 155
11. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.faceCutCorrelation_finset_sum line 166
12. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.booleanCutCorrelation_finset_sum line 203
13. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.abs_coarseAtom_faceCutCorrelation_le_card_mul line 236
14. theorem OAI.Erdos3.FixedDensity.FaceRegularityState.abs_coarseAtom_booleanCutCorrelation_le_card_mul line 277
15. theorem OAI.Erdos3.FixedDensity.abs_orderedCoarseUpperAtom_faceCutCorrelation_le_card_mul line 316
16. theorem OAI.Erdos3.FixedDensity.abs_orderedCoarseUpperAtom_faceCutCorrelation_le_complexity_mul line 345
17. theorem OAI.Erdos3.FixedDensity.IsPreliminaryOrderedRegular.coarseUpper line 373
18. theorem OAI.Erdos3.FixedDensity.atomBoundaryDefect_coarseAtom_eq_sum_fineAtoms line 405
19. theorem OAI.Erdos3.FixedDensity.atomBoundaryDefect_coarseAtom_sq_le_card_mul_sum line 425
20. theorem OAI.Erdos3.FixedDensity.mean_atomBoundaryDefect_coarseAtom_sq_le_card_mul_sum line 450
21. theorem OAI.Erdos3.FixedDensity.sum_fineAtomsInCoarseAtom line 500
22. theorem OAI.Erdos3.FixedDensity.partitionAtomEnergy_sub_coarseUpper_le_complexity_mul_fineUpper line 514
23. theorem OAI.Erdos3.FixedDensity.orderedAtomEnergy_sub_coarseUpper_le_complexity_mul_fineUpper line 580
24. def OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.coarseUpperFaceAtomEnergyGap line 602
25. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.coarseUpperFaceAtomEnergyGap_nonneg line 614
26. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.coarseUpperFaceAtomEnergyGap_le line 625
27. def OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.coarseUpperLayerAtomEnergyGap line 639
28. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.coarseUpperLayerAtomEnergyGap_eq_sum_face line 651
29. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.coarseUpperLayerAtomEnergyGap_le_sum_complexity_mul line 665
30. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.coarseUpperLayerAtomEnergyGap_le line 679
31. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.preliminaryRegular_coarseUpper line 712