OAI/Probability/LogConcave/Sampling/SpatialTensor.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LogConcaveSampling.spatialTensor line 15
  2. lemma OAI.LogConcaveSampling.fullList_perm line 20
  3. lemma OAI.LogConcaveSampling.spatialTensor_relabel line 26
  4. lemma OAI.LogConcaveSampling.spatialTensor_polySmooth line 39
  5. lemma OAI.LogConcaveSampling.spatialTensor_allSplit_relabel line 44
  6. def OAI.LogConcaveSampling.spatialEnvelope line 54
  7. lemma OAI.LogConcaveSampling.spatialEnvelope_nonneg line 58
  8. lemma OAI.LogConcaveSampling.spatialEnvelope_measurable line 62
  9. lemma OAI.LogConcaveSampling.spatialTensor_allSplit_envelope line 68
  10. def OAI.LogConcaveSampling.selectList line 94
  11. lemma OAI.LogConcaveSampling.map_selectList line 98
  12. lemma OAI.LogConcaveSampling.selectList_nodup line 104
  13. lemma OAI.LogConcaveSampling.selectList_full line 110
  14. lemma OAI.LogConcaveSampling.jet_selectList line 120
  15. lemma OAI.LogConcaveSampling.conditionalU_map line 139
  16. lemma OAI.LogConcaveSampling.jointU_map line 145
  17. def OAI.LogConcaveSampling.TensorAtom.jetList line 154
  18. lemma OAI.LogConcaveSampling.TensorAtom.jetList_weight line 160
  19. lemma OAI.LogConcaveSampling.TensorAtom.jetList_eval line 166
  20. def OAI.LogConcaveSampling.TensorAtom.swapLast line 189
  21. lemma OAI.LogConcaveSampling.TensorAtom.swapLast_left line 193
  22. lemma OAI.LogConcaveSampling.TensorAtom.swapLast_inner line 194
  23. lemma OAI.LogConcaveSampling.TensorAtom.swapLast_outer line 195
  24. def OAI.LogConcaveSampling.TensorAtom.extendedU line 197
  25. lemma OAI.LogConcaveSampling.TensorAtom.extendedU_weight line 201
  26. lemma OAI.LogConcaveSampling.TensorAtom.extendedU_eval line 205
  27. lemma OAI.LogConcaveSampling.jointU_selectList line 230
  28. lemma OAI.LogConcaveSampling.selectList_lengths line 237
  29. def OAI.LogConcaveSampling.TensorAtom.splitLabels line 246
  30. lemma OAI.LogConcaveSampling.TensorAtom.splitLabels_left line 249
  31. lemma OAI.LogConcaveSampling.TensorAtom.splitLabels_right line 251
  32. lemma OAI.LogConcaveSampling.TensorAtom.splitLabels_field line 253
  33. def OAI.LogConcaveSampling.TensorAtom.splitProduct line 258
  34. lemma OAI.LogConcaveSampling.TensorAtom.splitProduct_weight line 269
  35. lemma OAI.LogConcaveSampling.TensorAtom.splitProduct_eval line 283