OAI/Probability/LogConcave/JetEstimates/Mdir.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.JetCalculus.jet_dir line 15
  2. def OAI.LogConcaveSampling.JetCalculus.mdir line 23
  3. lemma OAI.LogConcaveSampling.JetCalculus.smooth_mdir line 26
  4. lemma OAI.LogConcaveSampling.JetCalculus.mdir_sum line 31
  5. lemma OAI.LogConcaveSampling.JetCalculus.mdir_add line 41
  6. lemma OAI.LogConcaveSampling.JetCalculus.mdir_const_mul line 50
  7. lemma OAI.LogConcaveSampling.JetCalculus.mdir_mul line 64
  8. theorem OAI.LogConcaveSampling.JetCalculus.mdir_jet line 80
  9. lemma OAI.LogConcaveSampling.JetCalculus.mdir_dir line 123
  10. def OAI.LogConcaveSampling.JetCalculus.cadj line 134
  11. def OAI.LogConcaveSampling.JetCalculus.gadj line 136
  12. lemma OAI.LogConcaveSampling.JetCalculus.smooth_cadj line 138
  13. lemma OAI.LogConcaveSampling.JetCalculus.gadj_sum line 142
  14. lemma OAI.LogConcaveSampling.JetCalculus.gadj_mul line 152
  15. theorem OAI.LogConcaveSampling.JetCalculus.mdir_cadj line 163
  16. theorem OAI.LogConcaveSampling.JetCalculus.mdir_gadj line 185