OAI/Probability/LogConcave/Numerics/RowTape.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.MeanTree.appendSlots_preserving line 14
2. lemma OAI.LogConcaveSampling.MeanTree.finPi_head_preserving line 31
3. abbrev OAI.LogConcaveSampling.MeanTree.RowTape line 37
4. def OAI.LogConcaveSampling.MeanTree.rowLaw line 40
5. instance OAI.LogConcaveSampling.MeanTree.(instance at line 44) line 44
6. def OAI.LogConcaveSampling.MeanTree.concatTerms line 47
7. lemma OAI.LogConcaveSampling.MeanTree.concatTerms_preserving line 55
8. lemma OAI.LogConcaveSampling.MeanTree.leftBlock_append line 83
9. lemma OAI.LogConcaveSampling.MeanTree.middleBlock_append line 86
10. lemma OAI.LogConcaveSampling.MeanTree.rightBlock_append line 91
11. lemma OAI.LogConcaveSampling.MeanTree.eval_concatTerms line 97