OAI/Analysis/MarkovType/FiniteL2IsometryTransport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MarkovSuperreflexivity.finiteDifference_map line 18
2. theorem OAI.MarkovSuperreflexivity.HasZeroConditionalSum.map line 26
3. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.IsMartingaleUpTo.map line 39
4. theorem OAI.MarkovSuperreflexivity.finiteL2Norm_linearIsometry line 55
5. theorem OAI.MarkovSuperreflexivity.FiniteUpperL2.pullback_isometry line 60
6. theorem OAI.MarkovSuperreflexivity.FiniteLowerL2.pullback_isometry line 76