OAI/Combinatorics/Progressions/Lattices/ResidueCellNormLengths.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.residuePrimeDensity_scaled_section_low_degree line 21
  2. theorem OAI.Erdos3.residuePrimeDensity_scaled_section_norm line 50
  3. theorem OAI.Erdos3.residuePrimeDensity_section_norm_le_three line 75
  4. theorem OAI.Erdos3.productSectionAverage_empty_fixed line 107
  5. theorem OAI.Erdos3.residuePrimeDensity_norm_le_three line 117
  6. theorem OAI.Erdos3.residuePrimeCoordinateMassRatio_nonneg line 145
  7. theorem OAI.Erdos3.residuePrimeCoordinateMassRatio_outside line 152
  8. theorem OAI.Erdos3.residuePrimeCoordinateDensity_conditional_outside line 185
  9. theorem OAI.Erdos3.retained_residue_marginals_of_lengths line 216
  10. def OAI.Erdos3.residueCellOutsideDensity line 263
  11. theorem OAI.Erdos3.residueCellOutsideDensity_lcm line 274
  12. theorem OAI.Erdos3.PrimeRefinementUpperBound.reference_density_upper line 302
  13. theorem OAI.Erdos3.PrimeRefinementUpperBound.reference_conditioned_upper line 341
  14. theorem OAI.Erdos3.residueCellOutsideDensity_norm_of_lengths line 377