OAI/Combinatorics/Progressions/Geometry/TwoBoxSmoothingComplex.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.twoBoxDifferenceDensity line 14
  2. theorem OAI.Erdos3.twoBoxDifferenceDensity_mem_Icc line 18
  3. theorem OAI.Erdos3.twoBoxDifferenceDensity_lipschitz line 25
  4. theorem OAI.Erdos3.twoBoxDifferenceDensity_integrable line 35
  5. theorem OAI.Erdos3.twoBoxDifferenceDensity_mass line 40
  6. theorem OAI.Erdos3.twoBoxDifferenceDensity_test_integral line 47
  7. theorem OAI.Erdos3.affineBoxAverage_preserves_lipschitz line 74
  8. theorem OAI.Erdos3.affineBoxAverage_preserves_cap line 90
  9. theorem OAI.Erdos3.integral_comp_inverse_linear_complex line 118
  10. theorem OAI.Erdos3.linearDensityPullback_complex_test_integral line 127
  11. theorem OAI.Erdos3.affineBoxAverage_complex_test_integral line 141
  12. theorem OAI.Erdos3.twoBoxDifferenceDensity_complex_test_integrable line 172
  13. theorem OAI.Erdos3.twoBoxDifferenceDensity_complex_test_integral line 179