OAI/Combinatorics/Progressions/Probability/AnisotropicSmoothPairLaw.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.independent_row_density_error line 11
  2. theorem OAI.Erdos3.product_masked_scalars line 32
  3. theorem OAI.Erdos3.independent_masked_row_density_error line 43
  4. def OAI.Erdos3.smoothPairCoefficientScale line 71
  5. theorem OAI.Erdos3.smoothPairCoefficientScale_pos line 74
  6. theorem OAI.Erdos3.affinePair_split_mulVec line 81
  7. theorem OAI.Erdos3.smooth_pair_input_law line 95
  8. theorem OAI.Erdos3.smooth_pair_row_law line 119
  9. theorem OAI.Erdos3.smooth_affinePairRowDensity_cap line 145
  10. theorem OAI.Erdos3.smooth_affinePairRowDensity_lipschitz line 170
  11. theorem OAI.Erdos3.centeredSmoothAffinePairRows_law line 218
  12. def OAI.Erdos3.smoothPairProbabilityError line 230
  13. def OAI.Erdos3.smoothPairProbabilityCap line 235
  14. theorem OAI.Erdos3.smooth_pair_actual_row_error line 239
  15. theorem OAI.Erdos3.smooth_pair_product_probability_law line 263
  16. theorem OAI.Erdos3.affine_pair_shift_divisibility line 330
  17. theorem OAI.Erdos3.shifted_smooth_pair_product_probability_law line 341
  18. theorem OAI.Erdos3.centeredSmoothAffinePairRows_variable line 388
  19. theorem OAI.Erdos3.smoothPairProbabilityError_nonneg line 398
  20. theorem OAI.Erdos3.anisotropic_smooth_pair_product_probability_law line 404
  21. theorem OAI.Erdos3.shifted_anisotropic_smooth_pair_product_probability_law line 461