OAI/Probability/SwitchChain/SwitchTV.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem315.kernelPow_eq_matrix_pow line 14
2. theorem OAI.Problem315.switch_tv_bound_of_gap line 29
3. lemma OAI.Problem315.switch_gap_parameter_le_one line 62
4. theorem OAI.Problem315.switch_chain_tv_bound_of_stochastic_and_gap line 72
5. theorem OAI.Problem315.switch_chain_tv_bound_of_spectralGap line 85