OAI/Probability/LogConcave/JetEstimates/Bound.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LogConcaveSampling.TensorEnergy.Bound line 22
  2. lemma OAI.LogConcaveSampling.TensorEnergy.energy_nonneg line 25
  3. lemma OAI.LogConcaveSampling.TensorEnergy.dot_sq line 28
  4. lemma OAI.LogConcaveSampling.TensorEnergy.bound_of_bilinear line 32
  5. lemma OAI.LogConcaveSampling.TensorEnergy.Bound.bilinear line 52
  6. lemma OAI.LogConcaveSampling.TensorEnergy.Bound.transpose line 58
  7. lemma OAI.LogConcaveSampling.TensorEnergy.Bound.kronecker line 73
  8. lemma OAI.LogConcaveSampling.TensorEnergy.Bound.reindex line 93
  9. lemma OAI.LogConcaveSampling.TensorEnergy.prod_split line 101
  10. lemma OAI.LogConcaveSampling.TensorEnergy.bound_pi_aux line 108
  11. lemma OAI.LogConcaveSampling.TensorEnergy.Bound.pi line 140
  12. lemma OAI.LogConcaveSampling.TensorEnergy.Bound.fibers line 147
  13. lemma OAI.LogConcaveSampling.TensorEnergy.Bound.mono line 159
  14. lemma OAI.LogConcaveSampling.TensorEnergy.Bound.smul line 163
  15. lemma OAI.LogConcaveSampling.TensorEnergy.Bound.sum line 169
  16. def OAI.LogConcaveSampling.Appell.splitConstant line 198
  17. lemma OAI.LogConcaveSampling.Appell.splitConstant_nonneg line 202
  18. theorem OAI.LogConcaveSampling.Appell.crossMoment_energy line 205
  19. def OAI.LogConcaveSampling.Appell.reducedCrossMoment line 216
  20. lemma OAI.LogConcaveSampling.Appell.reducedCrossMoment_energy line 220
  21. lemma OAI.LogConcaveSampling.Appell.card_fibers line 232
  22. lemma OAI.LogConcaveSampling.Appell.prod_fiber_factorial_le line 237
  23. lemma OAI.LogConcaveSampling.Appell.prod_splitConstant_le line 246
  24. def OAI.LogConcaveSampling.Appell.crossBlockProduct line 257
  25. lemma OAI.LogConcaveSampling.Appell.crossBlockProduct_energy line 263
  26. abbrev OAI.LogConcaveSampling.Appell.LogTerms line 273
  27. def OAI.LogConcaveSampling.Appell.logCoefficient line 276
  28. lemma OAI.LogConcaveSampling.Appell.logCoefficient_sq_le line 279
  29. def OAI.LogConcaveSampling.Appell.mixedCumulant line 288
  30. lemma OAI.LogConcaveSampling.Appell.card_logTerms_le line 293
  31. theorem OAI.LogConcaveSampling.Appell.mixedCumulant_energy line 303
  32. def OAI.LogConcaveSampling.Appell.HasExpMoments line 335
  33. def OAI.LogConcaveSampling.Appell.laplace line 339
  34. lemma OAI.LogConcaveSampling.Appell.growth_exp_bound line 344
  35. lemma OAI.LogConcaveSampling.Appell.HasExpMoments.integrable_laplace line 355
  36. lemma OAI.LogConcaveSampling.Appell.HasExpMoments.hasMoments line 370
  37. def OAI.LogConcaveSampling.Appell.inserted line 377
  38. lemma OAI.LogConcaveSampling.Appell.continuous_inserted line 380
  39. lemma OAI.LogConcaveSampling.Appell.growth_inserted line 384
  40. lemma OAI.LogConcaveSampling.Appell.hasFDerivAt_laplace line 396
  41. lemma OAI.LogConcaveSampling.Appell.contDiff_laplace line 428
  42. lemma OAI.LogConcaveSampling.Appell.laplace_one_pos line 445
  43. def OAI.LogConcaveSampling.JetCalculus.dir line 462
  44. def OAI.LogConcaveSampling.JetCalculus.jet line 464
  45. lemma OAI.LogConcaveSampling.JetCalculus.smooth_dir line 468
  46. lemma OAI.LogConcaveSampling.JetCalculus.smooth_jet line 472
  47. lemma OAI.LogConcaveSampling.JetCalculus.dir_add line 478
  48. lemma OAI.LogConcaveSampling.JetCalculus.dir_mul line 485
  49. lemma OAI.LogConcaveSampling.JetCalculus.dir_sum line 493
  50. lemma OAI.LogConcaveSampling.JetCalculus.jet_add line 500
  51. lemma OAI.LogConcaveSampling.JetCalculus.jet_sum line 510
  52. lemma OAI.LogConcaveSampling.JetCalculus.jet_const line 519
  53. lemma OAI.LogConcaveSampling.JetCalculus.filter_insert_of_not_mem line 529
  54. lemma OAI.LogConcaveSampling.JetCalculus.filter_not_insert_of_not_mem line 536
  55. theorem OAI.LogConcaveSampling.JetCalculus.jet_mul line 543
  56. lemma OAI.LogConcaveSampling.JetCalculus.jet_append line 578
  57. lemma OAI.LogConcaveSampling.JetCalculus.dir_const_mul line 584
  58. lemma OAI.LogConcaveSampling.JetCalculus.jet_const_mul line 591
  59. lemma OAI.LogConcaveSampling.JetCalculus.jet_sub line 600
  60. lemma OAI.LogConcaveSampling.JetCalculus.filter_length_add line 607
  61. lemma OAI.LogConcaveSampling.JetCalculus.jet_pow_zero line 618
  62. lemma OAI.LogConcaveSampling.JetCalculus.jet_pow_mul_zero line 641