OAI/Analysis/MarkovType/FiniteDualNorming.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MarkovSuperreflexivity.exists_unit_test_ge_norm_sub line 20
2. theorem OAI.MarkovSuperreflexivity.exists_weighted_dual_l2_test line 30
3. theorem OAI.MarkovSuperreflexivity.weighted_norm_rpow_root line 116
4. theorem OAI.MarkovSuperreflexivity.exists_weighted_dual_norming line 125