OAI/Probability/LogConcave/Sampling/ScoreSlots.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.natural_moment_root_product line 16
  2. theorem OAI.LogConcaveSampling.adjoint_eLpNorm line 32
  3. lemma OAI.LogConcaveSampling.scoreAugmented_allSplit line 75
  4. def OAI.LogConcaveSampling.scoreSlots line 109
  5. lemma OAI.LogConcaveSampling.scorePosition_allSplit line 131
  6. def OAI.LogConcaveSampling.contractSpatialSlots line 163
  7. lemma OAI.LogConcaveSampling.contractSpatialSlots_ll line 168
  8. lemma OAI.LogConcaveSampling.contractSpatialSlots_lr line 170
  9. lemma OAI.LogConcaveSampling.contractSpatialSlots_rl line 172
  10. lemma OAI.LogConcaveSampling.contractSpatialSlots_rr line 174
  11. def OAI.LogConcaveSampling.extendedSpatial line 177
  12. lemma OAI.LogConcaveSampling.extendedSpatial_allSplit line 182
  13. def OAI.LogConcaveSampling.spatialContractTerm line 188
  14. lemma OAI.LogConcaveSampling.spatialContractTerm_eq line 195
  15. lemma OAI.LogConcaveSampling.spatialContractTerm_allSplit line 213
  16. lemma OAI.LogConcaveSampling.spatialTensor_singleContract line 224
  17. def OAI.LogConcaveSampling.spatialInside line 251
  18. def OAI.LogConcaveSampling.spatialAdjointLeading line 257
  19. lemma OAI.LogConcaveSampling.spatialTensor_adjoint line 262
  20. def OAI.LogConcaveSampling.spatialFieldSlots line 276
  21. lemma OAI.LogConcaveSampling.fieldPosition_spatialInside line 283
  22. lemma OAI.LogConcaveSampling.fieldPosition_spatialInside_allSplit line 302
  23. lemma OAI.LogConcaveSampling.spatialInside_polySmooth line 316
  24. def OAI.LogConcaveSampling.scoreField line 334
  25. lemma OAI.LogConcaveSampling.scoreField_polySmooth line 337
  26. def OAI.LogConcaveSampling.lastSlot line 340
  27. def OAI.LogConcaveSampling.scoreSpatialSlots line 346
  28. lemma OAI.LogConcaveSampling.scoreSpatial_eq line 349
  29. lemma OAI.LogConcaveSampling.scoreField_spatial_allSplit line 357
  30. lemma OAI.LogConcaveSampling.scoreField_spatial_arbitrary line 372
  31. lemma OAI.LogConcaveSampling.spatialContractTerm_allSplit_nonempty line 390