OAI/Analysis/C0Absorption/Duality.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.C0Absorption.BoundedTest line 17
  2. theorem OAI.C0Absorption.class_pairing_bound line 20
  3. theorem OAI.C0Absorption.BoundedTest.continuous line 34
  4. theorem OAI.C0Absorption.BoundedTest.weak_null line 39
  5. theorem OAI.C0Absorption.pairing_add line 46
  6. theorem OAI.C0Absorption.pairing_smul line 52
  7. theorem OAI.C0Absorption.BoundedTest.add line 61
  8. theorem OAI.C0Absorption.BoundedTest.smul line 69
  9. theorem OAI.C0Absorption.completedPairing_add line 77
  10. theorem OAI.C0Absorption.completedPairing_smul line 93
  11. def OAI.C0Absorption.c0Origin line 110
  12. abbrev OAI.C0Absorption.SourceSpace line 111
  13. theorem OAI.C0Absorption.TClass_mono line 113
  14. theorem OAI.C0Absorption.VClass_mono line 117
  15. theorem OAI.C0Absorption.representation_mem_VClass line 121
  16. theorem OAI.C0Absorption.sourceClasses_lipschitz line 127
  17. theorem OAI.C0Absorption.TClass_pairing_bound line 134
  18. theorem OAI.C0Absorption.VClass_pairing_bound line 142
  19. theorem OAI.C0Absorption.TClass_bounded line 151
  20. theorem OAI.C0Absorption.VClass_bounded line 156
  21. def OAI.C0Absorption.flattenOperation line 169
  22. theorem OAI.C0Absorption.flattenOperation_scale line 172
  23. theorem OAI.C0Absorption.flattenOperation_act line 175
  24. theorem OAI.C0Absorption.flattenOperation_center line 178
  25. theorem OAI.C0Absorption.flattenOperation_plateau line 181
  26. theorem OAI.C0Absorption.flattenOperation_difference line 189
  27. theorem OAI.C0Absorption.GeneratedRepresentation.exists_flatten line 198
  28. theorem OAI.C0Absorption.GeneratedRepresentation.exists_flatten_T line 252