OAI/Analysis/LipschitzEquivalence/Schur.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LipschitzCounterexample.WeakSequences.WeakNull line 16
  2. def OAI.LipschitzCounterexample.WeakSequences.CompletelyContinuous line 19
  3. def OAI.LipschitzCounterexample.WeakSequences.WeakCauchy line 22
  4. def OAI.LipschitzCounterexample.WeakSequences.WeakSequentiallyComplete line 25
  5. theorem OAI.LipschitzCounterexample.WeakSequences.WeakNull.map line 29
  6. theorem OAI.LipschitzCounterexample.WeakSequences.WeakNull.subseq line 32
  7. abbrev OAI.LipschitzCounterexample.WeakSequences.RealL1 line 35
  8. theorem OAI.LipschitzCounterexample.WeakSequences.summable_norm line 37
  9. theorem OAI.LipschitzCounterexample.WeakSequences.summable_pair line 40
  10. def OAI.LipschitzCounterexample.WeakSequences.pairing line 48
  11. theorem OAI.LipschitzCounterexample.WeakSequences.pairing_apply line 70
  12. theorem OAI.LipschitzCounterexample.WeakSequences.norm_pairing_le_one line 73
  13. def OAI.LipschitzCounterexample.WeakSequences.trunc line 76
  14. theorem OAI.LipschitzCounterexample.WeakSequences.trunc_eq_sum line 81
  15. theorem OAI.LipschitzCounterexample.WeakSequences.trunc_apply line 89
  16. theorem OAI.LipschitzCounterexample.WeakSequences.tendsto_trunc line 94
  17. theorem OAI.LipschitzCounterexample.WeakSequences.WeakNull.trunc line 98
  18. theorem OAI.LipschitzCounterexample.WeakSequences.exists_common_sign line 110
  19. theorem OAI.LipschitzCounterexample.WeakSequences.schur line 140