OAI/Combinatorics/Progressions/Lattices/ResidueSliceUpperFailure.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.affineStabilityTolerance line 11
  2. def OAI.Erdos3.affineIncrementTolerance line 13
  3. theorem OAI.Erdos3.affineComparisonTolerance_bounds line 15
  4. theorem OAI.Erdos3.modEq_nat_lcm_iff line 41
  5. theorem OAI.Erdos3.residuePrimeCoordinate_constraints_lcm line 50
  6. def OAI.Erdos3.residuePrimeCoordinateCell_lcmEquiv line 78
  7. theorem OAI.Erdos3.residuePrimeCoordinateMean_lcm line 101
  8. theorem OAI.Erdos3.primeCoordinateProduct_le_exp line 122
  9. theorem OAI.Erdos3.residuePrimeModulus_le_exp line 132
  10. theorem OAI.Erdos3.residuePrimeCell_log_cost line 147
  11. def OAI.Erdos3.residuePrimeCoordinateOutsideEquiv line 177
  12. theorem OAI.Erdos3.residuePrimeCoordinateMean_outside line 210
  13. def OAI.Erdos3.ResidueSliceUpperComparison line 234
  14. theorem OAI.Erdos3.ResidueSliceUpperComparison.on_prime_cell line 240
  15. theorem OAI.Erdos3.ResiduePrimeCoordinateStable.refinement_upper_bound line 259
  16. theorem OAI.Erdos3.ResiduePrimeCoordinateStable.of_outside line 292
  17. theorem OAI.Erdos3.ResiduePrimeCoordinateStable.lift_outside line 341
  18. theorem OAI.Erdos3.primeCoordinate_error_le_exp line 374
  19. theorem OAI.Erdos3.residuePrimeDensity_close_of_lengths line 407
  20. theorem OAI.Erdos3.ResidueSliceUpperComparison.restrict_budget_and_error line 435
  21. theorem OAI.Erdos3.ResidueSliceUpperComparison.from_exponential_budget line 444
  22. theorem OAI.Erdos3.not_residueSliceUpperComparison_iff_exists_residue_slice line 462
  23. theorem OAI.Erdos3.exists_residue_slice_of_not_upper line 478
  24. theorem OAI.Erdos3.ResidueSliceLogCostLE.lengths_pos line 488
  25. theorem OAI.Erdos3.ResidueSliceLogCostLE.nonempty line 497
  26. theorem OAI.Erdos3.exists_nonempty_residue_slice_of_not_upper line 511