OAI/Probability/LogConcave/Sampling/JointSpace.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.tensorAdjoint_scalar line 12
  2. lemma OAI.LogConcaveSampling.conditionalU_one_eq_dir line 28
  3. lemma OAI.LogConcaveSampling.material_score_algebra line 45
  4. theorem OAI.LogConcaveSampling.material_interpolation_score line 81
  5. def OAI.LogConcaveSampling.jointSpace line 116
  6. def OAI.LogConcaveSampling.jointMean line 119
  7. def OAI.LogConcaveSampling.jointScore line 123
  8. lemma OAI.LogConcaveSampling.jointMean_smooth_at line 127
  9. lemma OAI.LogConcaveSampling.jointScore_smooth_at line 134
  10. lemma OAI.LogConcaveSampling.joint_gadj_slice line 141
  11. lemma OAI.LogConcaveSampling.joint_score_transport line 166
  12. theorem OAI.LogConcaveSampling.physical_material_adjoint line 188