OAI/Combinatorics/Progressions/Estimates/StableReferenceMean.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.residuePrimeCoordinateCell_lcm_nonempty line 11
2. theorem OAI.Erdos3.selectedCombined_coprime_outside line 20
3. theorem OAI.Erdos3.PrimeRefinementUpperBound.outside line 31
4. theorem OAI.Erdos3.ResiduePrimeCoordinateStable.outside_mean_close line 80
5. theorem OAI.Erdos3.ResiduePrimeCoordinateStable.reference_density_close line 129