OAI/Analysis/MarkovType/MarkedLetters.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MarkovSuperreflexivity.markedLettersline 15 - theorem
OAI.MarkovSuperreflexivity.markedLetters_snocline 19 - theorem
OAI.MarkovSuperreflexivity.markedExpect_constline 27 - theorem
OAI.MarkovSuperreflexivity.sum_outgoing_letterline 31 - theorem
OAI.MarkovSuperreflexivity.markedExpect_uniform_lettersline 47 - theorem
OAI.MarkovSuperreflexivity.markedProb_uniform_letter_wordline 100