OAI/Probability/LogConcave/JetEstimates/NormalizedLaplace.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.Appell.dir_laplace line 25
  2. lemma OAI.LogConcaveSampling.Appell.jet_laplace line 36
  3. lemma OAI.LogConcaveSampling.Appell.laplace_zero line 57
  4. lemma OAI.LogConcaveSampling.Appell.jet_laplace_zero line 60
  5. lemma OAI.LogConcaveSampling.Appell.filter_toFinset_of_subset line 67
  6. lemma OAI.LogConcaveSampling.Appell.filter_not_toFinset line 73
  7. lemma OAI.LogConcaveSampling.Appell.jet_inverse_laplace_zero line 78
  8. lemma OAI.LogConcaveSampling.JetCalculus.dir_comp_affine line 137
  9. lemma OAI.LogConcaveSampling.JetCalculus.jet_comp_affine line 146
  10. lemma OAI.LogConcaveSampling.JetCalculus.jet_map line 155
  11. lemma OAI.LogConcaveSampling.JetCalculus.dir_zero line 161
  12. lemma OAI.LogConcaveSampling.JetCalculus.jet_zero line 163
  13. def OAI.LogConcaveSampling.Appell.normalizedLaplace line 179
  14. lemma OAI.LogConcaveSampling.Appell.smooth_normalizedLaplace line 182
  15. lemma OAI.LogConcaveSampling.Appell.growth_polynomial_inner line 189
  16. lemma OAI.LogConcaveSampling.Appell.continuous_polynomial_inner line 198
  17. lemma OAI.LogConcaveSampling.Appell.jet_shift_laplace line 202
  18. lemma OAI.LogConcaveSampling.Appell.jet_normalized_at_zero line 213
  19. lemma OAI.LogConcaveSampling.Appell.jet_normalizedLaplace_zero line 249
  20. def OAI.LogConcaveSampling.JetCalculus.logTrunc line 266
  21. lemma OAI.LogConcaveSampling.JetCalculus.smooth_logTrunc line 269
  22. lemma OAI.LogConcaveSampling.JetCalculus.hasDerivAt_logTrunc line 274
  23. lemma OAI.LogConcaveSampling.JetCalculus.logTrunc_one line 287
  24. lemma OAI.LogConcaveSampling.JetCalculus.dir_log_remainder line 292
  25. lemma OAI.LogConcaveSampling.JetCalculus.jet_logTrunc line 322
  26. def OAI.LogConcaveSampling.JetCalculus.mixedJet line 354
  27. lemma OAI.LogConcaveSampling.JetCalculus.jet_right_slice line 357
  28. lemma OAI.LogConcaveSampling.JetCalculus.jet_left_slice line 364
  29. lemma OAI.LogConcaveSampling.JetCalculus.mixedJet_eq_joint line 371
  30. lemma OAI.LogConcaveSampling.JetCalculus.mixedJet_sub line 382
  31. lemma OAI.LogConcaveSampling.JetCalculus.mixedJet_sum line 388
  32. lemma OAI.LogConcaveSampling.JetCalculus.mixedJet_const_mul line 397
  33. lemma OAI.LogConcaveSampling.JetCalculus.mixedJet_const line 402
  34. lemma OAI.LogConcaveSampling.JetCalculus.nodup_sum_append line 408
  35. lemma OAI.LogConcaveSampling.JetCalculus.mixedJet_logTrunc line 418
  36. def OAI.LogConcaveSampling.Appell.crossMGF line 442
  37. lemma OAI.LogConcaveSampling.Appell.smooth_crossMGF line 446
  38. lemma OAI.LogConcaveSampling.Appell.crossMGF_pos line 454
  39. lemma OAI.LogConcaveSampling.Appell.crossMGF_zero line 460
  40. lemma OAI.LogConcaveSampling.Appell.crossMGF_left_zero line 464
  41. lemma OAI.LogConcaveSampling.Appell.crossMGF_right_zero line 471
  42. lemma OAI.LogConcaveSampling.Appell.mixedJet_crossMGF line 477
  43. lemma OAI.LogConcaveSampling.Appell.mixedJet_reduced_unmixed line 498
  44. lemma OAI.LogConcaveSampling.Appell.mixedJet_reduced line 509
  45. def OAI.LogConcaveSampling.JetCalculus.assignments line 530
  46. lemma OAI.LogConcaveSampling.JetCalculus.length_assignments line 536
  47. lemma OAI.LogConcaveSampling.JetCalculus.assignments_default line 545
  48. lemma OAI.LogConcaveSampling.JetCalculus.mem_assignments line 557
  49. lemma OAI.LogConcaveSampling.JetCalculus.filter_update line 577
  50. lemma OAI.LogConcaveSampling.JetCalculus.differentiable_list_sum line 584
  51. lemma OAI.LogConcaveSampling.JetCalculus.dir_list_sum line 593
  52. lemma OAI.LogConcaveSampling.JetCalculus.smooth_list_sum line 608
  53. lemma OAI.LogConcaveSampling.JetCalculus.jet_list_sum line 618
  54. lemma OAI.LogConcaveSampling.JetCalculus.list_sum_flatMap line 628
  55. lemma OAI.LogConcaveSampling.JetCalculus.sum_eq_list line 635
  56. lemma OAI.LogConcaveSampling.JetCalculus.dir_prod line 641
  57. theorem OAI.LogConcaveSampling.JetCalculus.jet_prod line 656