OAI/Probability/SKGap/Stability/Ordinary.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.Noncrossing.WordSeries.ordinary line 30
2. def OAI.SKGap.Noncrossing.WordSeries.chain line 31
3. def OAI.SKGap.Noncrossing.WordSeries.inverseCoefficient line 33
4. lemma OAI.SKGap.Noncrossing.WordSeries.chain_nil line 36
5. lemma OAI.SKGap.Noncrossing.WordSeries.chain_append line 37
6. lemma OAI.SKGap.Noncrossing.WordSeries.chain_true line 39
7. lemma OAI.SKGap.Noncrossing.WordSeries.chain_false line 41
8. lemma OAI.SKGap.Noncrossing.WordSeries.blocks_zero line 44
9. instance OAI.SKGap.Noncrossing.WordSeries.blocksZeroUnique line 47
10. lemma OAI.SKGap.Noncrossing.WordSeries.inverseCoefficient_zero line 51
11. lemma OAI.SKGap.Noncrossing.WordSeries.inverseCoefficient_empty line 56
12. lemma OAI.SKGap.Noncrossing.WordSeries.mean_inverseCoefficient line 67
13. lemma OAI.SKGap.Noncrossing.WordSeries.sum_marked_chain line 74
14. lemma OAI.SKGap.Noncrossing.WordSeries.inverse_partner_right line 93
15. lemma OAI.SKGap.Noncrossing.WordSeries.ordinary_cut_right line 118
16. theorem OAI.SKGap.Noncrossing.WordSeries.inverseCoefficient_right line 131