OAI/Combinatorics/Progressions/Lattices/ResidueSliceCountingCost.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.scalarResidue_card_mul_le line 11
  2. theorem OAI.Erdos3.scalarResidue_card_real_le line 36
  3. theorem OAI.Erdos3.scalarResidue_card_mul_ge line 56
  4. theorem OAI.Erdos3.scalarResidue_card_absolute_error line 78
  5. theorem OAI.Erdos3.scalarResidue_relative_count_error line 93
  6. theorem OAI.Erdos3.residue_constraints_iff_lcm line 115
  7. theorem OAI.Erdos3.exists_integer_coprime_residues line 124
  8. theorem OAI.Erdos3.coprime_refinement_preserves_compatibility line 139
  9. theorem OAI.Erdos3.refined_residue_constraints_iff line 152
  10. theorem OAI.Erdos3.compatible_residue_count_error line 162
  11. def OAI.Erdos3.residueIndexLower line 184
  12. def OAI.Erdos3.residueIndexLength line 187
  13. def OAI.Erdos3.residueAffineEmbedding line 190
  14. theorem OAI.Erdos3.residueIndexInterval_eq line 194
  15. theorem OAI.Erdos3.residueInterval_eq_map line 201
  16. def OAI.Erdos3.residueIntervalEquiv line 214
  17. theorem OAI.Erdos3.residueIntervalEquiv_val line 235
  18. theorem OAI.Erdos3.residueIndexLength_eq_card line 240
  19. theorem OAI.Erdos3.residueIndexLength_absolute_error line 246
  20. def OAI.Erdos3.integerResidueLabel line 259
  21. theorem OAI.Erdos3.integerResidueLabel_val line 265
  22. theorem OAI.Erdos3.integerResidueLabel_eq_iff line 270
  23. abbrev OAI.Erdos3.CompatibleAuxResidue line 278
  24. instance OAI.Erdos3.compatibleAuxResidueFintype line 281
  25. def OAI.Erdos3.compatibleAuxResidueOfPoint line 284
  26. theorem OAI.Erdos3.compatibleAuxResidueOfPoint_eq_iff line 288
  27. theorem OAI.Erdos3.compatibleAuxResidue_nonempty line 295
  28. def OAI.Erdos3.CompatibleAuxResidue.baseValue line 299
  29. theorem OAI.Erdos3.CompatibleAuxResidue.baseValue_spec line 302
  30. def OAI.Erdos3.CompatibleAuxResidue.refinedValue line 307
  31. theorem OAI.Erdos3.CompatibleAuxResidue.refinedValue_spec line 311
  32. theorem OAI.Erdos3.CompatibleAuxResidue.baseConstraint_iff line 318
  33. theorem OAI.Erdos3.refinement_modEq_iff line 324
  34. theorem OAI.Erdos3.CompatibleAuxResidue.refinedConstraint_iff line 331
  35. theorem OAI.Erdos3.residueIndexLength_ge_of_width line 350
  36. theorem OAI.Erdos3.residueIndexLength_half_width line 372
  37. theorem OAI.Erdos3.residueIndexLength_large_of_exp line 397
  38. theorem OAI.Erdos3.residueIndexLength_le_width line 428
  39. theorem OAI.Erdos3.residue_slice_counting_cost line 434