OAI/NumberTheory/Jacobsthal/Estimates/UniformJointModel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.ErdosUniformMobiusRemainder.cutoffExponent line 13
2. theorem OAI.Erdos970.ErdosUniformMobiusRemainder.cutoffExponent_margin line 15
3. theorem OAI.Erdos970.ErdosUniformMobiusRemainder.source_sqrt_lower line 19
4. theorem OAI.Erdos970.ErdosUniformMobiusRemainder.remainder_scalar_bound line 28
5. theorem OAI.Erdos970.ErdosUniformMobiusRemainder.uniform_mobius_remainder line 52
6. theorem OAI.Erdos970.ErdosVarianceUniformMoments.zero_joint_model_mass line 94
7. theorem OAI.Erdos970.ErdosVarianceUniformMoments.uniform_joint_model_relative line 120