OAI/Combinatorics/Progressions/Lattices/SmoothAffinePairLaw.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.affinePairMatrix line 13
  2. theorem OAI.Erdos3.affinePairMatrix_mulVec line 18
  3. def OAI.Erdos3.affinePairImage line 25
  4. theorem OAI.Erdos3.mem_affinePairImage_iff line 28
  5. theorem OAI.Erdos3.affinePairImage_iff_content_dvd line 45
  6. def OAI.Erdos3.pairDifferenceMod line 82
  7. theorem OAI.Erdos3.pairDifferenceMod_surjective line 87
  8. theorem OAI.Erdos3.pairDifferenceMod_ker line 93
  9. theorem OAI.Erdos3.affinePairImage_eq_congruence_kernel line 98
  10. theorem OAI.Erdos3.pairDifferenceMod_index line 105
  11. theorem OAI.Erdos3.affinePairImage_index line 111
  12. theorem OAI.Erdos3.integerResidueMatrix_fromCols line 123
  13. theorem OAI.Erdos3.integerMatrix_fromCols_range line 130
  14. theorem OAI.Erdos3.pivotFullImage_eq_range line 146
  15. theorem OAI.Erdos3.pivotFullImage_split line 151
  16. theorem OAI.Erdos3.pivotFullImage_eq_of_kernel_residues line 157
  17. theorem OAI.Erdos3.maskedIntegerImageDensity_eq_of_kernel_residues line 173
  18. def OAI.Erdos3.affinePairPivot line 194
  19. def OAI.Erdos3.affinePairFree line 197
  20. def OAI.Erdos3.affinePairColumnEquiv line 200
  21. theorem OAI.Erdos3.affinePairPivot_det line 217
  22. theorem OAI.Erdos3.affinePairPivot_columns line 221
  23. theorem OAI.Erdos3.affinePairPivot_image line 230
  24. theorem OAI.Erdos3.affinePairPivot_index line 250
  25. def OAI.Erdos3.latticeStarMask line 263
  26. theorem OAI.Erdos3.latticeStarMask_bound line 268
  27. theorem OAI.Erdos3.latticeStarMask_eval line 277
  28. theorem OAI.Erdos3.maskedIntegerImageDensity_star line 285
  29. def OAI.Erdos3.liftResidueMatrix line 305
  30. theorem OAI.Erdos3.liftResidueMatrix_residue line 308
  31. def OAI.Erdos3.residueSpatialWeight line 313
  32. theorem OAI.Erdos3.maskedIntegerImageDensity_eq_residueWeight line 318
  33. theorem OAI.Erdos3.residueSpatialWeight_factor_average line 328
  34. def OAI.Erdos3.affinePairScale line 349
  35. theorem OAI.Erdos3.affinePairScale_pos line 351
  36. theorem OAI.Erdos3.normalized_affinePairPivot line 358
  37. theorem OAI.Erdos3.normalized_affinePairFree line 366
  38. theorem OAI.Erdos3.normalized_affinePairPivot_det line 375
  39. theorem OAI.Erdos3.normalized_affinePairPivot_inverse line 382
  40. theorem OAI.Erdos3.normalized_affinePairFree_norm line 404
  41. theorem OAI.Erdos3.residueSpatialWeight_average_functional line 424
  42. theorem OAI.Erdos3.residueSpatialWeight_average_comparison line 451
  43. theorem OAI.Erdos3.weightedResidueSpatial_mixture_functional line 485
  44. theorem OAI.Erdos3.weightedResidueSpatial_mixture_comparison line 511
  45. theorem OAI.Erdos3.affinePair_mesh_bound line 542
  46. def OAI.Erdos3.affinePairRowDensity line 560
  47. theorem OAI.Erdos3.affinePair_probability_error line 567
  48. theorem OAI.Erdos3.affinePair_probability_law line 624
  49. def OAI.Erdos3.smoothPairRowLipschitz line 673
  50. theorem OAI.Erdos3.smooth_affinePair_probability_law line 676