OAI/NumberTheory/Jacobsthal/Analysis/JointModelDensity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.ErdosVarianceMoments.jointDensity_nonneg line 16
2. theorem OAI.Erdos970.ErdosVarianceMoments.odd_position_density_lower line 23
3. theorem OAI.Erdos970.ErdosVarianceMoments.nonzero_jointDensity_lower line 35
4. def OAI.Erdos970.ErdosVarianceUniformMoments.densityInverseConstant line 71
5. theorem OAI.Erdos970.ErdosVarianceUniformMoments.densityInverseConstant_pos line 73
6. theorem OAI.Erdos970.ErdosVarianceUniformMoments.actual_sieveProduct line 77
7. theorem OAI.Erdos970.ErdosVarianceUniformMoments.uniform_density_inverse line 81
8. theorem OAI.Erdos970.ErdosVarianceMoments.jointDensity_le_one line 126
9. theorem OAI.Erdos970.ErdosVarianceMoments.jointDensity_split line 136
10. theorem OAI.Erdos970.ErdosVarianceMoments.model_normalization_identity line 142