OAI/Probability/LogConcave/Sampling/FinSnocSlots.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.physicalBase_envelope line 13
2. lemma OAI.LogConcaveSampling.physicalBase_envelope_budget line 27
3. theorem OAI.LogConcaveSampling.physicalBase_tame line 67
4. def OAI.LogConcaveSampling.finSnocSlots line 90
5. lemma OAI.LogConcaveSampling.finSnocSlots_castSucc line 93
6. lemma OAI.LogConcaveSampling.finSnocSlots_last line 96
7. lemma OAI.LogConcaveSampling.snoc_through_slots line 99
8. def OAI.LogConcaveSampling.TensorExpression.profileConstant line 108
9. lemma OAI.LogConcaveSampling.TensorExpression.profileConstant_ge line 115
10. theorem OAI.LogConcaveSampling.TensorExpression.eval_tame line 124
11. lemma OAI.LogConcaveSampling.physicalScale_one_le line 197
12. theorem OAI.LogConcaveSampling.TensorExpression.physical_tame line 204
13. lemma OAI.LogConcaveSampling.TameAt.eLpNorm line 238
14. theorem OAI.LogConcaveSampling.TensorExpression.physical_split_Lp line 273