OAI/Probability/LogConcave/JetEstimates/Growth.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LogConcaveSampling.Appell.HasGrowth line 23
  2. lemma OAI.LogConcaveSampling.Appell.pow_le_one_add_pow_add line 26
  3. lemma OAI.LogConcaveSampling.Appell.HasGrowth.const line 36
  4. lemma OAI.LogConcaveSampling.Appell.HasGrowth.add line 39
  5. lemma OAI.LogConcaveSampling.Appell.HasGrowth.smul line 51
  6. lemma OAI.LogConcaveSampling.Appell.HasGrowth.mul line 67
  7. lemma OAI.LogConcaveSampling.Appell.HasGrowth.norm line 70
  8. lemma OAI.LogConcaveSampling.Appell.HasGrowth.pow line 73
  9. lemma OAI.LogConcaveSampling.Appell.HasGrowth.sum line 79
  10. lemma OAI.LogConcaveSampling.Appell.HasGrowth.prod line 89
  11. lemma OAI.LogConcaveSampling.Appell.HasGrowth.linear line 99
  12. lemma OAI.LogConcaveSampling.Appell.HasGrowth.lipschitz line 104
  13. def OAI.LogConcaveSampling.Appell.HasMoments line 113
  14. lemma OAI.LogConcaveSampling.Appell.HasGrowth.integrable line 115
  15. lemma OAI.LogConcaveSampling.Appell.HasGrowth.memLp line 121
  16. def OAI.LogConcaveSampling.Appell.inverseMoment line 135
  17. lemma OAI.LogConcaveSampling.Appell.inverseMoment_empty line 144
  18. lemma OAI.LogConcaveSampling.Appell.inverseMoment_convolution line 148
  19. lemma OAI.LogConcaveSampling.Appell.inverseMoment_nonempty line 169
  20. lemma OAI.LogConcaveSampling.Appell.inverseMoment_image line 182
  21. def OAI.LogConcaveSampling.Appell.polynomial line 204
  22. lemma OAI.LogConcaveSampling.Appell.polynomial_empty line 207
  23. lemma OAI.LogConcaveSampling.Appell.polynomial_image line 210
  24. def OAI.LogConcaveSampling.Appell.moments line 221
  25. lemma OAI.LogConcaveSampling.Appell.moments_empty line 225
  26. lemma OAI.LogConcaveSampling.Appell.moments_image line 229
  27. lemma OAI.LogConcaveSampling.Appell.polynomial_integrable line 239
  28. lemma OAI.LogConcaveSampling.Appell.integral_polynomial line 247
  29. lemma OAI.LogConcaveSampling.Appell.sum_powerset_sdiff line 256
  30. lemma OAI.LogConcaveSampling.Appell.polynomial_contDiff line 275
  31. lemma OAI.LogConcaveSampling.Appell.hasFDerivAt_polynomial line 285
  32. def OAI.LogConcaveSampling.Appell.coordinate line 318
  33. lemma OAI.LogConcaveSampling.Appell.coordinate_basis line 321
  34. def OAI.LogConcaveSampling.Appell.slotPolynomial line 325
  35. def OAI.LogConcaveSampling.Appell.tensorPolynomial line 329
  36. lemma OAI.LogConcaveSampling.Appell.growth_polynomial line 334
  37. lemma OAI.LogConcaveSampling.Appell.slotPolynomial_growth line 341
  38. lemma OAI.LogConcaveSampling.Appell.tensorPolynomial_growth line 347
  39. lemma OAI.LogConcaveSampling.Appell.slotPolynomial_smooth line 352
  40. lemma OAI.LogConcaveSampling.Appell.tensorPolynomial_smooth line 357
  41. lemma OAI.LogConcaveSampling.Appell.integral_slotPolynomial line 362
  42. lemma OAI.LogConcaveSampling.Appell.integral_tensorPolynomial line 371
  43. lemma OAI.LogConcaveSampling.Appell.slotPolynomial_erase line 383
  44. def OAI.LogConcaveSampling.Appell.slice line 401
  45. lemma OAI.LogConcaveSampling.Appell.hasFDerivAt_tensorPolynomial line 405
  46. lemma OAI.LogConcaveSampling.Appell.derivative_tensorPolynomial_basis line 412
  47. lemma OAI.LogConcaveSampling.Appell.tensorPolynomial_memLp line 438
  48. lemma OAI.LogConcaveSampling.Appell.tensorPolynomial_derivative_growth line 446
  49. lemma OAI.LogConcaveSampling.Appell.tensorPolynomial_derivative_integrable line 453
  50. lemma OAI.LogConcaveSampling.Appell.sq_sum_le_card_mul_sum_sq line 462
  51. lemma OAI.LogConcaveSampling.Appell.tensorPolynomial_derivative_bound line 467
  52. lemma OAI.LogConcaveSampling.Appell.tensorPolynomial_one_step line 478
  53. lemma OAI.LogConcaveSampling.Appell.slice_energy line 499
  54. theorem OAI.LogConcaveSampling.Appell.tensorPolynomial_L2_aux line 506
  55. theorem OAI.LogConcaveSampling.Appell.tensorPolynomial_L2 line 550