OAI/Combinatorics/Progressions/Lattices/AffineBoxTest.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.normalizedIntervalWindow_translate line 12
  2. theorem OAI.Erdos3.boxProbabilityWindow_translate line 21
  3. theorem OAI.Erdos3.boxAverage_eq_translate line 27
  4. def OAI.Erdos3.affineBoxAverage line 36
  5. theorem OAI.Erdos3.affineBoxAverage_eq line 40
  6. theorem OAI.Erdos3.affineBoxAverage_lipschitz line 50
  7. theorem OAI.Erdos3.affineBoxAverage_mem_Icc line 68
  8. def OAI.Erdos3.affineBoxIntegrand line 88
  9. theorem OAI.Erdos3.affineBoxIntegrand_integrable line 92
  10. theorem OAI.Erdos3.affineBoxAverage_integrable line 109
  11. theorem OAI.Erdos3.affineBoxAverage_mass line 114
  12. theorem OAI.Erdos3.affineBoxAverage_nonneg line 126
  13. theorem OAI.Erdos3.affineBoxAverage_probability_density line 131
  14. theorem OAI.Erdos3.affineBoxAverage_test_integral line 151