OAI/Analysis/MarkovType/SubdivisionAverage.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MarkovSuperreflexivity.Subdivision.skip line 19
2. theorem OAI.MarkovSuperreflexivity.Subdivision.strictMono_skip line 21
3. def OAI.MarkovSuperreflexivity.Subdivision.blockArray line 26
4. def OAI.MarkovSuperreflexivity.Subdivision.blockVector line 30
5. theorem OAI.MarkovSuperreflexivity.Subdivision.place_blockArray line 33
6. theorem OAI.MarkovSuperreflexivity.Subdivision.blockVector_eq line 43
7. def OAI.MarkovSuperreflexivity.Subdivision.sample line 51
8. theorem OAI.MarkovSuperreflexivity.Subdivision.skip_in_block line 55
9. theorem OAI.MarkovSuperreflexivity.Subdivision.sample_eq line 68
10. theorem OAI.MarkovSuperreflexivity.Subdivision.sum_deletions line 89
11. theorem OAI.MarkovSuperreflexivity.Subdivision.block_nsmul line 104
12. theorem OAI.MarkovSuperreflexivity.Subdivision.sum_samples line 118
13. theorem OAI.MarkovSuperreflexivity.Subdivision.seminorm_sum_le line 131
14. theorem OAI.MarkovSuperreflexivity.Subdivision.sample_norm line 146
15. theorem OAI.MarkovSuperreflexivity.Subdivision.block_succ_le line 153
16. theorem OAI.MarkovSuperreflexivity.Subdivision.block_mono line 164