OAI/Combinatorics/Progressions/Probability/CandidateFrontFactorMassBlockBudget.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.candidateFrontFactor_block_le_power line 9
2. theorem OAI.Erdos3.VectorPolynomial.exists_candidateFrontFactor_block_power_budget line 26
3. theorem OAI.Erdos3.VectorPolynomial.candidateFrontFactor_uniform_block_le_power line 35
4. theorem OAI.Erdos3.VectorPolynomial.candidateFrontFactor_massLog_le line 57