OAI/Probability/LogConcave/Sampling/TerminalMean.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LogConcaveSampling.terminalMean line 18
  2. lemma OAI.LogConcaveSampling.terminalMean_smooth line 22
  3. lemma OAI.LogConcaveSampling.terminalBackward_deriv line 35
  4. lemma OAI.LogConcaveSampling.terminalMean_direction line 55
  5. lemma OAI.LogConcaveSampling.conditionalFieldMean_zero line 78
  6. lemma OAI.LogConcaveSampling.terminalMean_initial line 86
  7. lemma OAI.LogConcaveSampling.terminalMean_final line 90
  8. lemma OAI.LogConcaveSampling.conditionalFirstJet_symmetric_pos line 112
  9. lemma OAI.LogConcaveSampling.conditionalFirstJet_symmetric line 131
  10. lemma OAI.LogConcaveSampling.terminalForward_slice_smooth line 169
  11. lemma OAI.LogConcaveSampling.terminalBackward_slice_smooth line 173
  12. def OAI.LogConcaveSampling.terminalHomeomorph line 177
  13. lemma OAI.LogConcaveSampling.terminal_integral_pushforward line 185
  14. lemma OAI.LogConcaveSampling.firstJet_pairing_sum line 193
  15. lemma OAI.LogConcaveSampling.stein_pairing_integrand line 212
  16. lemma OAI.LogConcaveSampling.tensorAdjoint_continuous_C1 line 242
  17. lemma OAI.LogConcaveSampling.stein_weak_derivative line 256