OAI/Analysis/MarkovType/ScalarPowerRemainder.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MarkovSuperreflexivity.rpow_add_le_tangent_add_rpow line 11
2. theorem OAI.MarkovSuperreflexivity.rpow_sub_le_tangent_add_rpow line 44
3. theorem OAI.MarkovSuperreflexivity.rpow_le_tangent_add_abs_rpow line 79
4. theorem OAI.MarkovSuperreflexivity.symmetric_rpow_le_of_sum_bound line 104