OAI/Analysis/LipschitzEquivalence/WeakSums.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LipschitzCounterexample.WeakSequences.WeakCauchy.map line 16
  2. theorem OAI.LipschitzCounterexample.WeakSequences.WeakCauchy.bounded line 19
  3. theorem OAI.LipschitzCounterexample.WeakSequences.schur_cauchy line 29
  4. theorem OAI.LipschitzCounterexample.WeakSequences.wsc_realL1 line 49
  5. abbrev OAI.LipschitzCounterexample.WeakSequences.SumL1 line 54
  6. theorem OAI.LipschitzCounterexample.WeakSequences.sumL1_norm line 58
  7. theorem OAI.LipschitzCounterexample.WeakSequences.sumL1_summable line 62
  8. def OAI.LipschitzCounterexample.WeakSequences.coordinateTests line 65
  9. theorem OAI.LipschitzCounterexample.WeakSequences.coordinateTests_apply line 82
  10. def OAI.LipschitzCounterexample.WeakSequences.headL1 line 85
  11. def OAI.LipschitzCounterexample.WeakSequences.tailL1 line 88
  12. theorem OAI.LipschitzCounterexample.WeakSequences.headL1_eq_sum line 90
  13. theorem OAI.LipschitzCounterexample.WeakSequences.headL1_apply line 98
  14. theorem OAI.LipschitzCounterexample.WeakSequences.tailL1_apply line 103
  15. theorem OAI.LipschitzCounterexample.WeakSequences.tendsto_tailL1 line 110
  16. theorem OAI.LipschitzCounterexample.WeakSequences.norm_tailL1_le line 116
  17. theorem OAI.LipschitzCounterexample.WeakSequences.norm_tailL1_antitone line 123
  18. theorem OAI.LipschitzCounterexample.WeakSequences.uniform_tails_of_cauchy line 133
  19. theorem OAI.LipschitzCounterexample.WeakSequences.exists_common_functionals line 154
  20. theorem OAI.LipschitzCounterexample.WeakSequences.uniform_tails_of_weakCauchy line 178
  21. theorem OAI.LipschitzCounterexample.WeakSequences.finite_norm_le_of_weak_limits line 254
  22. theorem OAI.LipschitzCounterexample.WeakSequences.wsc_sumL1 line 270
  23. theorem OAI.LipschitzCounterexample.WeakSequences.weakLimit_mem line 337
  24. theorem OAI.LipschitzCounterexample.WeakSequences.wsc_submodule line 345
  25. theorem OAI.LipschitzCounterexample.WeakSequences.wsc_equiv line 354
  26. abbrev OAI.LipschitzCounterexample.WeakSequences.ScalarC0 line 361
  27. def OAI.LipschitzCounterexample.WeakSequences.initialOnes line 364
  28. theorem OAI.LipschitzCounterexample.WeakSequences.initialOnes_apply line 366
  29. theorem OAI.LipschitzCounterexample.WeakSequences.summable_c0_dual line 369
  30. theorem OAI.LipschitzCounterexample.WeakSequences.initialOnes_weakCauchy line 403
  31. theorem OAI.LipschitzCounterexample.WeakSequences.not_wsc_c0 line 410
  32. theorem OAI.LipschitzCounterexample.WeakSequences.no_c0_of_wsc line 428