OAI/Combinatorics/Progressions/Lattices/AffineSampleAlphabet.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.residueColumnMap line 16
  2. theorem OAI.Erdos3.residueColumnMap_single line 22
  3. theorem OAI.Erdos3.additiveCharacter_zmod_smul line 26
  4. theorem OAI.Erdos3.residueColumn_character_zero_iff line 31
  5. theorem OAI.Erdos3.residueColumn_character_mean line 44
  6. def OAI.Erdos3.residueColumnAverage line 50
  7. theorem OAI.Erdos3.finiteFourierCoeff_residueColumnAverage line 55
  8. theorem OAI.Erdos3.residueColumn_survival_probability line 83
  9. theorem OAI.Erdos3.residueColumnAverage_energy line 108
  10. theorem OAI.Erdos3.residueColumnAverage_mean_energy line 118
  11. theorem OAI.Erdos3.primeAffine_contraction_sq line 129
  12. theorem OAI.Erdos3.primeAffine_contraction line 150
  13. theorem OAI.Erdos3.primePowerResidue_contraction_sq line 181
  14. theorem OAI.Erdos3.primePowerResidue_contraction line 191
  15. def OAI.Erdos3.residueColumnRealAverage line 214
  16. theorem OAI.Erdos3.residueColumnAverage_ofReal line 217
  17. theorem OAI.Erdos3.residueColumnRealAverage_mean line 225
  18. theorem OAI.Erdos3.primeAffine_real_contraction_sq line 233
  19. def OAI.Erdos3.residueAffineSource line 257
  20. def OAI.Erdos3.residueAffineKernel line 260
  21. theorem OAI.Erdos3.residueAffineKernel_mean line 264
  22. theorem OAI.Erdos3.residueAffineKernel_preserves_mean line 269
  23. def OAI.Erdos3.residueAffineCoupling line 275
  24. theorem OAI.Erdos3.residueAffineKernel_centered_sq line 280
  25. theorem OAI.Erdos3.affineCoupling_level_abs_le line 306
  26. theorem OAI.Erdos3.affineCoupling_tail_abs_le line 321
  27. theorem OAI.Erdos3.productAffine_centered_contraction_sq line 345
  28. theorem OAI.Erdos3.productAffine_centered_pairing_sq line 362
  29. theorem OAI.Erdos3.productAffine_uniform_centered_sq line 381
  30. theorem OAI.Erdos3.primeCoordinateCell_mono line 411
  31. def OAI.Erdos3.primeCoordinateMean line 419
  32. theorem OAI.Erdos3.primeCoordinateMean_eq_physical line 424
  33. def OAI.Erdos3.PrimeCoordinateStable line 433
  34. theorem OAI.Erdos3.primeCoordinateStable_of_empty line 440
  35. theorem OAI.Erdos3.exists_prime_cell_physical_comparison line 450
  36. def OAI.Erdos3.primeCoordinateObservation line 497
  37. def OAI.Erdos3.primeCoordinateReference line 500
  38. theorem OAI.Erdos3.primeCoordinateReference_weight_pos line 504
  39. def OAI.Erdos3.primeCoordinateLaw line 510
  40. def OAI.Erdos3.primeCoordinateDensity line 517
  41. theorem OAI.Erdos3.primeCoordinateDensity_nonneg line 525
  42. theorem OAI.Erdos3.primeCoordinateDensity_one line 537
  43. abbrev OAI.Erdos3.ResiduePrimeCoordinateCell line 555
  44. def OAI.Erdos3.residuePrimeCoordinateMean line 561
  45. def OAI.Erdos3.ResiduePrimeCoordinateStable line 568
  46. def OAI.Erdos3.primeCoordinateCell_subtypeEquiv line 577
  47. def OAI.Erdos3.affineSampleAlphabetEquiv line 598
  48. theorem OAI.Erdos3.affineSampleAlphabet_weight line 605
  49. theorem OAI.Erdos3.affineSampleAlphabet_mean line 615
  50. def OAI.Erdos3.affinePrimeCoordinateObservation line 622
  51. theorem OAI.Erdos3.affinePrimeCoordinateObservation_apply line 626