OAI/Combinatorics/Progressions/Lattices/RegularizedAffineComparison.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.nonprincipalDilation_width_pos line 12
  2. theorem OAI.Erdos3.nonprincipalDilation_width_lower line 18
  3. theorem OAI.Erdos3.nonprincipalDilation_profile_support line 26
  4. theorem OAI.Erdos3.affineAllowance_nonprincipal_sum_le line 34
  5. theorem OAI.Erdos3.affinePrincipal_sum_le line 42
  6. theorem OAI.Erdos3.affineConstantCoefficient_measurable line 47
  7. def OAI.Erdos3.canonicalAffineRawArray line 67
  8. theorem OAI.Erdos3.canonicalAffineRawArray_eq line 80
  9. theorem OAI.Erdos3.scaledAffinePolynomial_principal_coefficient line 93
  10. theorem OAI.Erdos3.canonicalAffineRawArray_eq_jointUnitMap line 116
  11. theorem OAI.Erdos3.canonicalAffineRawArray_normalized line 156
  12. theorem OAI.Erdos3.canonicalAffineRawArray_joint_law line 188
  13. theorem OAI.Erdos3.rawCanonicalJet_eq_smallAffineArray line 236
  14. def OAI.Erdos3.smallAffineSourceOutput line 275
  15. theorem OAI.Erdos3.rawSourceOutput_eq_smallAffineSource line 287
  16. theorem OAI.Erdos3.smallAffineSourceOutput_measurable line 311
  17. def OAI.Erdos3.regularizedAffineIdealDensity line 344
  18. theorem OAI.Erdos3.regularizedAffineIdealDensity_probability line 355
  19. theorem OAI.Erdos3.regularizedAffineIdealDensity_bounds line 367
  20. theorem OAI.Erdos3.regularizedAffineIdealDensity_measurable_comp line 380
  21. theorem OAI.Erdos3.smallAffineSourceOutput_zero_rescale line 416
  22. theorem OAI.Erdos3.exists_small_affine_source_tolerance_with_scale line 446
  23. theorem OAI.Erdos3.exists_small_affine_source_tolerance line 528
  24. theorem OAI.Erdos3.smallAffineSourceOutput_zero_integral line 582
  25. theorem OAI.Erdos3.exists_regularized_affine_comparison_with_parameters line 614
  26. theorem OAI.Erdos3.exists_regularized_affine_comparison line 691