OAI/Analysis/MarkovType/FiniteMartingaleDuality.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MarkovSuperreflexivity.finite_l2_dual_pairing_bound line 20
2. theorem OAI.MarkovSuperreflexivity.lowerL2_dual_exponent_range line 32
3. theorem OAI.MarkovSuperreflexivity.finiteLowerL2_dual_upper line 41