OAI/Combinatorics/Progressions/Linear/CountingKernelOuter.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.countingFeature line 12
  2. def OAI.Erdos3.countingKernel line 15
  3. def OAI.Erdos3.positiveCountingKernel line 18
  4. theorem OAI.Erdos3.countingFeature_pair line 20
  5. theorem OAI.Erdos3.countingFeature_opposite line 27
  6. theorem OAI.Erdos3.countingFeature_same line 34
  7. theorem OAI.Erdos3.countingFeature_sqrt_opposite line 42
  8. theorem OAI.Erdos3.countingFeature_sqrt_same line 47
  9. theorem OAI.Erdos3.countingKernel_one line 52
  10. theorem OAI.Erdos3.countingKernel_quarter line 56
  11. theorem OAI.Erdos3.positiveCountingKernel_nonneg line 61
  12. def OAI.Erdos3.countingFeatureProduct line 75
  13. def OAI.Erdos3.countingKernelProductAverage line 79
  14. def OAI.Erdos3.positiveKernelGram line 83
  15. theorem OAI.Erdos3.countingFeatureProduct_pair line 86
  16. theorem OAI.Erdos3.countingFeatureProduct_mean_pair line 95
  17. theorem OAI.Erdos3.countingKernelProductAverage_factorization line 111
  18. theorem OAI.Erdos3.countingFeatureProduct_square line 120
  19. theorem OAI.Erdos3.positiveKernelGram_nonneg line 126
  20. theorem OAI.Erdos3.countingKernelProductAverage_sq_le line 131
  21. theorem OAI.Erdos3.countingKernelProductAverage_abs_le line 145
  22. def OAI.Erdos3.countingBernoulli line 164
  23. theorem OAI.Erdos3.countingBernoulli_mean line 170
  24. theorem OAI.Erdos3.countingBernoulli_product line 174
  25. theorem OAI.Erdos3.positiveKernelGram_le_of_boolean_products line 182
  26. theorem OAI.Erdos3.countingKernelProductAverage_abs_le_of_boolean_products line 199
  27. theorem OAI.Erdos3.countingKernelProductAverage_outer_sq_le line 219
  28. theorem OAI.Erdos3.mean_positiveKernelGram_le_of_boolean_products line 242
  29. theorem OAI.Erdos3.countingKernelProductAverage_outer_abs_le line 261