OAI/Analysis/MarkovType/SequenceL2JConvex.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.MarkovSuperreflexivity.sequenceL2ExponentAtLeastOne line 16
2. abbrev OAI.MarkovSuperreflexivity.SequenceL2 line 18
3. theorem OAI.MarkovSuperreflexivity.sequenceL2_completeSpace line 23
4. theorem OAI.MarkovSuperreflexivity.sequenceL2_norm_sq line 27
5. theorem OAI.MarkovSuperreflexivity.sequenceL2_hasSum_norm_sq line 33
6. theorem OAI.MarkovSuperreflexivity.sequenceL2_cutSum_apply line 38
7. theorem OAI.MarkovSuperreflexivity.squareAverage_sequenceL2 line 50
8. theorem OAI.MarkovSuperreflexivity.AmbientJConvex.sequenceL2 line 71