OAI/Probability/SwitchChain/InitialTVGraph.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem315.tvDistanceFrom_zero_eq line 10
2. theorem OAI.Problem315.mixedAt_zero_of_stateCount_one line 23
3. theorem OAI.Problem315.mixingTime_zero_of_mixedAt_zero line 29
4. theorem OAI.Problem315.singleton_mixing_conclusion line 35
5. theorem OAI.Problem315.mixedAt_zero_iff_stateCount_le_one line 41