OAI/Probability/LogConcave/Sampling/NormalizedTensor.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.list_split_perm line 16
  2. def OAI.LogConcaveSampling.normalizedTensor line 35
  3. def OAI.LogConcaveSampling.normalizedTensorMajorant line 44
  4. lemma OAI.LogConcaveSampling.normalizedTensorMajorant_nonneg line 48
  5. lemma OAI.LogConcaveSampling.normalizedTensor_allSplit line 51
  6. lemma OAI.LogConcaveSampling.joint_laplace_as_conditional line 133
  7. lemma OAI.LogConcaveSampling.joint_laplace_shift line 142
  8. lemma OAI.LogConcaveSampling.joint_log_laplace_shift line 167
  9. lemma OAI.LogConcaveSampling.joint_log_laplace_smooth line 182
  10. def OAI.LogConcaveSampling.jointCumulant line 193
  11. lemma OAI.LogConcaveSampling.jointCumulant_shift line 198
  12. lemma OAI.LogConcaveSampling.jointCumulant_smooth line 225
  13. lemma OAI.LogConcaveSampling.jointCumulant_spatial_jet line 240
  14. lemma OAI.LogConcaveSampling.list_length_full line 282
  15. lemma OAI.LogConcaveSampling.normalizedTensor_smooth line 287
  16. lemma OAI.LogConcaveSampling.normalizedTensor_spatial_jet line 295