OAI/Combinatorics/Progressions/Estimates/AllocatedGenuineNativePartner.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.allocatedRecenteredContinuousSiteFactor line 47
2. theorem OAI.Erdos3.VectorPolynomial.nonneg_exp_sum_le_exp_add_one line 54
3. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredContinuousSiteFactor_pre_bounds line 64
4. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredNormalizedSiteFactor_continuous line 127
5. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredNormalizedSiteFactor_norm_le line 145
6. theorem OAI.Erdos3.VectorPolynomial.allocated_genuine_cube_expansion line 232
7. theorem OAI.Erdos3.VectorPolynomial.allocated_genuine_cube_native_partner line 360