OAI/Analysis/MarkovType/SubdivisionProfileExpansion.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.MarkovSuperreflexivity.Subdivision.ofList_appendline 13 - theorem
OAI.MarkovSuperreflexivity.Subdivision.ofList_replicateline 27 - theorem
OAI.MarkovSuperreflexivity.Subdivision.pieces_ofFn_eqline 32 - theorem
OAI.MarkovSuperreflexivity.Subdivision.finiteSubdivision_eqline 59