OAI/Combinatorics/Progressions/Lattices/RetainedPhysicalCRT.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.affineSampleKernel line 17
  2. theorem OAI.Erdos3.affineSampleKernel_mean line 20
  3. theorem OAI.Erdos3.affineSampleKernel_preserves_mean line 32
  4. def OAI.Erdos3.affineSampleCoupling line 40
  5. theorem OAI.Erdos3.affineSampleKernel_centered_sq line 45
  6. theorem OAI.Erdos3.affinePrimeCoordinateObservation_site line 57
  7. theorem OAI.Erdos3.affineSampleFixedParameter_mean line 79
  8. def OAI.Erdos3.affineSampleParameterKernel line 94
  9. theorem OAI.Erdos3.affineSampleParameterKernel_mean line 99
  10. theorem OAI.Erdos3.affineSampleParameterKernel_preserves_mean line 106
  11. def OAI.Erdos3.affineSampleParameterCoupling line 115
  12. theorem OAI.Erdos3.affineSampleParameterKernel_uniform line 121
  13. theorem OAI.Erdos3.inverse_prime_power_le_square line 134
  14. theorem OAI.Erdos3.affineSampleKernel_centered_sq_of_inverse_le line 143
  15. theorem OAI.Erdos3.residue_function_alphabet_card_le_exp line 154
  16. def OAI.Erdos3.affineSampleProductCoupling line 170
  17. def OAI.Erdos3.affineResidueTruncatedPairing line 177
  18. def OAI.Erdos3.affinePeriodParameterLaw line 195
  19. theorem OAI.Erdos3.affinePeriodParameterLaw_mean line 200
  20. theorem OAI.Erdos3.affinePeriodParameterLaw_uniform line 207
  21. theorem OAI.Erdos3.affinePeriodParameterLaw_integer line 225
  22. theorem OAI.Erdos3.affineSampleParameterKernel_centered_bound line 242
  23. theorem OAI.Erdos3.affine_leaf_source_assignments_card_le_exp line 271
  24. def OAI.Erdos3.affineParameterProductCoupling line 303
  25. theorem OAI.Erdos3.affineSampleParameterCoupling_uniform line 310
  26. theorem OAI.Erdos3.affineSampleParameterKernel_sq line 314
  27. theorem OAI.Erdos3.affineParameterProductCoupling_pairing line 327
  28. theorem OAI.Erdos3.affineParameterProductCoupling_outside line 352
  29. def OAI.Erdos3.affineParameterCRTequiv line 376
  30. theorem OAI.Erdos3.affineParameterCRTequiv_apply line 382
  31. theorem OAI.Erdos3.affineParameterCRT_mean line 387
  32. theorem OAI.Erdos3.affinePeriodParameterLaw_CRT line 401
  33. theorem OAI.Erdos3.affineParameterCRTequiv_integer line 416
  34. theorem OAI.Erdos3.affinePeriodParameterLaw_CRT_integer line 423
  35. def OAI.Erdos3.affinePeriodProductCoupling line 444
  36. theorem OAI.Erdos3.affinePeriodProductCoupling_outside line 450
  37. theorem OAI.Erdos3.affinePeriodProductCoupling_pairing line 459
  38. theorem OAI.Erdos3.affinePeriodParameterKernel_centered_sq line 480
  39. def OAI.Erdos3.affinePeriodResidueSample line 511
  40. theorem OAI.Erdos3.affinePeriodResidueSample_integer line 519
  41. theorem OAI.Erdos3.affinePeriodResidueSample_depends line 529
  42. theorem OAI.Erdos3.affinePeriodProductCoupling_observed line 541
  43. theorem OAI.Erdos3.affinePeriodTruncatedPairing_observed line 553
  44. theorem OAI.Erdos3.affinePeriodProductCoupling_pairing_CRT line 581
  45. theorem OAI.Erdos3.affinePeriodParameterLaw_physical_site line 598
  46. theorem OAI.Erdos3.affinePeriodTruncatedPairing_comparison line 627
  47. theorem OAI.Erdos3.affinePeriodTruncation_sample_comparison line 661
  48. theorem OAI.Erdos3.residuePrimeCoordinateDensity_component_cap line 695
  49. def OAI.Erdos3.residueAffineTruncationError line 736
  50. theorem OAI.Erdos3.residueAffineTruncation_comparison line 746
  51. theorem OAI.Erdos3.residueAffineTruncation_comparison_of_lengths line 781
  52. theorem OAI.Erdos3.physicalBoxTruncation_of_classify_some line 814
  53. theorem OAI.Erdos3.physicalBoxTruncation_of_classify_none line 828
  54. theorem OAI.Erdos3.retained_physical_truncation_crt line 838