OAI/Combinatorics/Progressions/Estimates/FiniteSectionPermutation.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.finiteWeightedLp line 14
  2. theorem OAI.Erdos3.finiteWeightedMoment_nonneg line 17
  3. theorem OAI.Erdos3.finiteWeightedLp_nonneg line 21
  4. theorem OAI.Erdos3.finiteWeightedLp_mono line 25
  5. theorem OAI.Erdos3.finiteWeightedLp_smul line 34
  6. theorem OAI.Erdos3.finiteWeightedLp_rpow line 49
  7. theorem OAI.Erdos3.finiteWeightedLp_two line 61
  8. def OAI.Erdos3.finiteMixedLp line 75
  9. theorem OAI.Erdos3.finiteMixedLp_nonneg line 81
  10. theorem OAI.Erdos3.finiteMixedLp_mono line 87
  11. theorem OAI.Erdos3.finiteMixedLp_smul line 101
  12. theorem OAI.Erdos3.finiteMixedLp_rpow line 114
  13. def OAI.Erdos3.finiteSectionIntegral line 141
  14. def OAI.Erdos3.finiteSectionL2Norm line 152
  15. def OAI.Erdos3.finiteSectionCount line 156
  16. theorem OAI.Erdos3.finiteSectionCount_succ line 159
  17. theorem OAI.Erdos3.finiteSectionIntegral_nonneg line 164
  18. theorem OAI.Erdos3.finiteSectionL2Norm_zero line 177
  19. theorem OAI.Erdos3.finiteSectionL2Norm_fix line 182
  20. theorem OAI.Erdos3.finiteSectionL2Norm_integrate line 190
  21. theorem OAI.Erdos3.finiteWeightedLp_interpolate_two line 215
  22. def OAI.Erdos3.finiteWeightedL2Map line 257
  23. theorem OAI.Erdos3.norm_finiteWeightedL2Map line 268
  24. theorem OAI.Erdos3.finiteWeightedLp_two_sum_le line 277
  25. theorem OAI.Erdos3.finiteWeightedLp_rpow_self line 299
  26. theorem OAI.Erdos3.finiteWeightedLp_zero_support line 305
  27. theorem OAI.Erdos3.finiteWeightedLp_abs line 316
  28. def OAI.Erdos3.finiteMaskedLpStep line 330
  29. def OAI.Erdos3.finiteMaskedMixedLp line 334
  30. theorem OAI.Erdos3.finiteMaskedMixedLp_nonneg line 339
  31. theorem OAI.Erdos3.finiteMaskedMixedLp_all line 346
  32. def OAI.Erdos3.finiteSectionL2Control line 365
  33. theorem OAI.Erdos3.finiteSectionL2Control_pointwise line 374
  34. theorem OAI.Erdos3.finiteSectionL2Control_norm line 387
  35. theorem OAI.Erdos3.finiteSectionCount_eq_card line 404
  36. theorem OAI.Erdos3.finiteSection_free_card line 409
  37. def OAI.Erdos3.finiteSectionFreeOrder line 413
  38. def OAI.Erdos3.finiteSectionFill line 417
  39. theorem OAI.Erdos3.finiteSectionFill_fixed line 422
  40. theorem OAI.Erdos3.finiteSectionFill_free line 427
  41. def OAI.Erdos3.finiteSectionWeight line 445
  42. theorem OAI.Erdos3.finiteSectionWeight_false line 450
  43. theorem OAI.Erdos3.finiteSectionWeight_sum_true line 454
  44. theorem OAI.Erdos3.finiteSectionIntegral_eq_product line 459
  45. theorem OAI.Erdos3.FiniteProbabilityWeights.familyL2_eq line 488
  46. theorem OAI.Erdos3.FiniteProbabilityWeights.sqrt_sum_mean_sq_triangle line 496
  47. theorem OAI.Erdos3.finiteSectionCount_permute line 517
  48. theorem OAI.Erdos3.finiteSectionIntegral_permute line 522
  49. theorem OAI.Erdos3.finiteSectionL2Norm_permute line 531
  50. theorem OAI.Erdos3.finiteSectionL2Bounds_permute line 538