OAI/Combinatorics/Progressions/Estimates/FlatWeightedComparison.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.finiteSetLp line 12
  2. theorem OAI.Erdos3.finiteSetLp_of_pos line 15
  3. theorem OAI.Erdos3.finiteSetLp_nonneg line 19
  4. theorem OAI.Erdos3.finiteSetLp_pow line 26
  5. theorem OAI.Erdos3.finiteSetLp_eq_sum line 33
  6. theorem OAI.Erdos3.finiteSetLp_const line 39
  7. theorem OAI.Erdos3.finiteSetLp_mono_abs line 44
  8. theorem OAI.Erdos3.finiteSetLp_le_of_bound line 52
  9. theorem OAI.Erdos3.finiteSetLp_add_le line 59
  10. theorem OAI.Erdos3.finiteSetLp_le_of_uniform_error line 68
  11. def OAI.Erdos3.LocalConvolution.convolution line 86
  12. def OAI.Erdos3.LocalConvolution.correlation line 89
  13. def OAI.Erdos3.LocalConvolution.sumMoment line 92
  14. def OAI.Erdos3.LocalConvolution.differenceMoment line 95
  15. def OAI.Erdos3.LocalConvolution.momentVector line 98
  16. def OAI.Erdos3.LocalConvolution.plusMomentVector line 101
  17. theorem OAI.Erdos3.LocalConvolution.convolution_add line 104
  18. theorem OAI.Erdos3.LocalConvolution.correlation_sub line 115
  19. theorem OAI.Erdos3.LocalConvolution.plusMomentVector_eq_neg line 127
  20. theorem OAI.Erdos3.LocalConvolution.sum_momentVector_mul line 131
  21. theorem OAI.Erdos3.LocalConvolution.sum_momentVector_mul_plus line 145
  22. theorem OAI.Erdos3.LocalConvolution.sum_sq_plusMomentVector line 159
  23. theorem OAI.Erdos3.LocalConvolution.differenceMoment_correlation_eq line 165
  24. theorem OAI.Erdos3.LocalConvolution.sumMoment_convolution_eq line 172
  25. theorem OAI.Erdos3.LocalConvolution.differenceMoment_self_nonneg line 179
  26. theorem OAI.Erdos3.LocalConvolution.sumMoment_convolution_sq_le line 184
  27. theorem OAI.Erdos3.expect_tail_mul_pow_le line 203
  28. theorem OAI.Erdos3.finiteSetLp_tail_le line 213
  29. theorem OAI.Erdos3.finiteSetLp_double_tail_le line 224
  30. def OAI.Erdos3.LocalConvolution.momentAmplificationFactor line 238
  31. def OAI.Erdos3.LocalConvolution.momentAmplificationGain line 240
  32. theorem OAI.Erdos3.LocalConvolution.momentAmplificationFactor_pos line 243
  33. theorem OAI.Erdos3.LocalConvolution.momentAmplificationGain_pos line 247
  34. theorem OAI.Erdos3.LocalConvolution.momentAmplificationGain_le_one line 254
  35. theorem OAI.Erdos3.LocalConvolution.momentAmplificationGain_pow line 264
  36. theorem OAI.Erdos3.LocalConvolution.finiteSetLp_unbalance line 270
  37. def OAI.Erdos3.LocalConvolution.sumLp line 315
  38. def OAI.Erdos3.LocalConvolution.differenceLp line 318
  39. theorem OAI.Erdos3.LocalConvolution.sumLp_nonneg line 321
  40. theorem OAI.Erdos3.LocalConvolution.differenceLp_nonneg line 324
  41. theorem OAI.Erdos3.LocalConvolution.sumLp_pow line 327
  42. theorem OAI.Erdos3.LocalConvolution.differenceLp_pow line 332
  43. theorem OAI.Erdos3.LocalConvolution.sumLp_le_of_uniform_error line 337
  44. theorem OAI.Erdos3.LocalConvolution.differenceLp_le_of_uniform_error line 346
  45. theorem OAI.Erdos3.LocalConvolution.convolution_sumLp_sq_le line 355
  46. theorem OAI.Erdos3.flat_weighted_pointwise_le line 383
  47. theorem OAI.Erdos3.flat_weighted_average_le line 407