OAI/Probability/LogConcave/Sampling/CoordinateRank.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.conditionalU_moments_sq line 18
  2. theorem OAI.LogConcaveSampling.conditionalU_joint_smooth line 34
  3. lemma OAI.LogConcaveSampling.jointU_timeSmooth line 56
  4. def OAI.LogConcaveSampling.coordinateRankOne line 77
  5. def OAI.LogConcaveSampling.conditionalFirstJet line 81
  6. lemma OAI.LogConcaveSampling.conditionalFirstJet_smooth line 91
  7. def OAI.LogConcaveSampling.terminalJacobian line 101
  8. lemma OAI.LogConcaveSampling.terminalJacobian_smooth line 106
  9. def OAI.LogConcaveSampling.steinIntegrand line 112
  10. lemma OAI.LogConcaveSampling.steinIntegrand_smooth line 118
  11. def OAI.LogConcaveSampling.centeringKernel line 129
  12. lemma OAI.LogConcaveSampling.centeringKernel_smooth line 133
  13. lemma OAI.LogConcaveSampling.covariance_field_synthesis line 152
  14. lemma OAI.LogConcaveSampling.conditionalFirstJet_inner line 169
  15. lemma OAI.LogConcaveSampling.conditionalFirstJet_norm_le line 204
  16. lemma OAI.LogConcaveSampling.conditionalFirstJet_deriv line 227
  17. lemma OAI.LogConcaveSampling.terminalJacobian_eq line 255
  18. lemma OAI.LogConcaveSampling.terminalJacobian_norm_le line 273
  19. lemma OAI.LogConcaveSampling.steinIntegrand_norm_le line 289
  20. theorem OAI.LogConcaveSampling.centeringKernel_norm_le line 306
  21. lemma OAI.LogConcaveSampling.eq_zero_of_continuous_pos line 331
  22. lemma OAI.LogConcaveSampling.JetCalculus.smooth_gadj_at line 343
  23. lemma OAI.LogConcaveSampling.extra_list_nodup line 349
  24. theorem OAI.LogConcaveSampling.material_jointU line 368
  25. lemma OAI.LogConcaveSampling.joint_score_transport_nonneg line 446
  26. theorem OAI.LogConcaveSampling.physical_material_adjoint_nonneg line 466