OAI/NumberTheory/Jacobsthal/Estimates/PositionDensities.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosVarianceMoments.positionResidues line 13
  2. def OAI.Erdos970.ErdosVarianceMoments.forbiddenClasses line 15
  3. theorem OAI.Erdos970.ErdosVarianceMoments.affine_forbidden_injective line 18
  4. theorem OAI.Erdos970.ErdosVarianceMoments.forbiddenClasses_card line 25
  5. theorem OAI.Erdos970.ErdosVarianceMoments.mem_forbiddenClasses line 31
  6. theorem OAI.Erdos970.ErdosVarianceMoments.positionResidues_le_positions line 40
  7. theorem OAI.Erdos970.ErdosVarianceMoments.positionResidues_le_modulus line 43
  8. theorem OAI.Erdos970.ErdosVarianceMoments.forbiddenClasses_full_of_card line 47
  9. def OAI.Erdos970.ErdosVarianceMoments.positionDensity line 64
  10. def OAI.Erdos970.ErdosVarianceMoments.jointDensity line 67
  11. theorem OAI.Erdos970.ErdosVarianceMoments.positionDensity_bounds line 69
  12. theorem OAI.Erdos970.ErdosVarianceMoments.positionDensity_le_two line 76
  13. theorem OAI.Erdos970.ErdosVarianceMoments.positionResidues_singleton line 81
  14. theorem OAI.Erdos970.ErdosVarianceMoments.positionResidues_pair line 84
  15. theorem OAI.Erdos970.ErdosVarianceMoments.jointDensity_singleton line 98
  16. theorem OAI.Erdos970.ErdosVarianceMoments.jointDensity_pair line 102