OAI/Combinatorics/Progressions/FixedDensity/CoarseTargetRegularity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Erdos3.FixedDensity.CoarseTargetOrderedComplexRegularityCertificate line 11
2. def OAI.Erdos3.FixedDensity.CoarseTargetOrderedComplexRegularityCertificate.toCoarseFine line 73
3. theorem OAI.Erdos3.FixedDensity.CoarseTargetOrderedComplexRegularityCertificate.fine_refines_initial line 87
4. theorem OAI.Erdos3.FixedDensity.CoarseTargetOrderedComplexRegularityCertificate.nonempty line 102
5. def OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.totalCoarseUpperAtomEnergyGap line 488
6. theorem OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.totalCoarseUpperAtomEnergyGap_nonneg line 494
7. theorem OAI.Erdos3.FixedDensity.CoarseTargetOrderedComplexRegularityCertificate.totalCoarseUpperAtomEnergyGap_le_sum_div line 510
8. theorem OAI.Erdos3.FixedDensity.CoarseTargetOrderedComplexRegularityCertificate.totalCoarseUpperAtomEnergyGap_nonneg line 529
9. theorem OAI.Erdos3.FixedDensity.exists_coarseTargetOrderedComplexRegularity line 543