OAI/Analysis/MarkovType/FiniteTailAmplification.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MarkovSuperreflexivity.one_sub_pow_le_reciprocal_linear line 12
2. theorem OAI.MarkovSuperreflexivity.le_inv_nat_of_half_le_one_sub_pow line 27
3. theorem OAI.MarkovSuperreflexivity.tail_bound_of_nat_scale_bound line 40
4. theorem OAI.MarkovSuperreflexivity.tail_bound_of_half_power_scale line 81