OAI/Probability/LogConcave/JetEstimates/SpaceBasis.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.PolySmooth.linear line 17
  2. lemma OAI.LogConcaveSampling.growth_potential_of_gradient_lipschitz line 33
  3. lemma OAI.LogConcaveSampling.interpolationPotential_polySmooth line 56
  4. lemma OAI.LogConcaveSampling.JetCalculus.dir_right_slice_at line 96
  5. lemma OAI.LogConcaveSampling.JetCalculus.dir_left_slice_at line 105
  6. lemma OAI.LogConcaveSampling.joint_mdir_eq_material line 114
  7. lemma OAI.LogConcaveSampling.dir_inner_map line 130
  8. theorem OAI.LogConcaveSampling.conditionalFieldMean_directional_symm line 138
  9. abbrev OAI.LogConcaveSampling.JetCalculus.spaceBasis line 175
  10. def OAI.LogConcaveSampling.JetCalculus.linearScore line 177
  11. def OAI.LogConcaveSampling.JetCalculus.euler line 179
  12. lemma OAI.LogConcaveSampling.JetCalculus.linearScore_smooth line 182
  13. lemma OAI.LogConcaveSampling.JetCalculus.dir_linearScore line 185
  14. lemma OAI.LogConcaveSampling.JetCalculus.smooth_euler line 191
  15. lemma OAI.LogConcaveSampling.JetCalculus.dir_euler line 195
  16. lemma OAI.LogConcaveSampling.JetCalculus.jet_euler line 208
  17. lemma OAI.LogConcaveSampling.JetCalculus.gadj_linearScore line 222
  18. lemma OAI.LogConcaveSampling.JetCalculus.jet_gadj_linearScore line 228
  19. lemma OAI.LogConcaveSampling.JetCalculus.gadj_perturb line 245
  20. theorem OAI.LogConcaveSampling.JetCalculus.jet_gadj_gradient line 256
  21. lemma OAI.LogConcaveSampling.JetCalculus.smooth_dir_at line 297
  22. lemma OAI.LogConcaveSampling.JetCalculus.dir_dir_at line 301
  23. lemma OAI.LogConcaveSampling.JetCalculus.dir_add_at line 316
  24. lemma OAI.LogConcaveSampling.JetCalculus.dir_sub_at line 323
  25. lemma OAI.LogConcaveSampling.JetCalculus.dir_mul_at line 330
  26. lemma OAI.LogConcaveSampling.JetCalculus.dir_const_mul_at line 338
  27. lemma OAI.LogConcaveSampling.JetCalculus.dir_sum_at line 344
  28. lemma OAI.LogConcaveSampling.JetCalculus.smooth_mdir_at line 349
  29. lemma OAI.LogConcaveSampling.JetCalculus.mdir_sum_at line 355
  30. lemma OAI.LogConcaveSampling.JetCalculus.mdir_add_at line 363
  31. lemma OAI.LogConcaveSampling.JetCalculus.mdir_const_mul_at line 371
  32. lemma OAI.LogConcaveSampling.JetCalculus.mdir_mul_at line 384
  33. lemma OAI.LogConcaveSampling.JetCalculus.mdir_dir_at line 399
  34. lemma OAI.LogConcaveSampling.JetCalculus.smooth_cadj_at line 421
  35. lemma OAI.LogConcaveSampling.JetCalculus.gadj_mul_at line 426
  36. lemma OAI.LogConcaveSampling.JetCalculus.gadj_sum_at line 436
  37. theorem OAI.LogConcaveSampling.JetCalculus.mdir_cadj_at line 445
  38. theorem OAI.LogConcaveSampling.JetCalculus.mdir_gadj_at line 466
  39. lemma OAI.LogConcaveSampling.JetCalculus.dir_eventuallyEq line 499
  40. lemma OAI.LogConcaveSampling.JetCalculus.jet_eventuallyEq line 504
  41. lemma OAI.LogConcaveSampling.JetCalculus.mdir_eventuallyEq line 510
  42. lemma OAI.LogConcaveSampling.JetCalculus.gadj_eventuallyEq line 520
  43. lemma OAI.LogConcaveSampling.JetCalculus.smooth_jet_at line 530
  44. def OAI.LogConcaveSampling.JetCalculus.TimeSmooth line 536
  45. lemma OAI.LogConcaveSampling.JetCalculus.TimeSmooth.localize line 539
  46. theorem OAI.LogConcaveSampling.JetCalculus.mdir_jet_time line 548