OAI/Combinatorics/Progressions/Sampling/PreparedEarlyLateSamplerGeometry.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.RankPreparationFamily.PreparedHeights.exists_bounded_sampler_geometry line 14
2. theorem OAI.Erdos3.RankPreparationFamily.PreparedHeights.exists_bounded_sampler_geometry_of_sized line 43
3. theorem OAI.Erdos3.RankPreparationFamily.PreparedHeights.mono_parameter line 89
4. theorem OAI.Erdos3.RankPreparationFamily.PreparedHeights.basisAxisScale_le_exp line 101
5. theorem OAI.Erdos3.RankPreparationFamily.PreparedHeights.exists_early_late_sampler_geometry line 132
6. theorem OAI.Erdos3.RankPreparationFamily.PreparedHeights.exists_early_late_sampler_geometry_at_sum line 176