OAI/Analysis/Triangular/Construction/ConcreteSchur.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AtomicTriangular.Construction.splitL line 11
  2. def OAI.AtomicTriangular.Construction.splitB line 13
  3. def OAI.AtomicTriangular.Construction.splitK line 15
  4. def OAI.AtomicTriangular.Construction.splitD line 17
  5. def OAI.AtomicTriangular.Construction.splitN line 19
  6. def OAI.AtomicTriangular.Construction.splitQ line 20
  7. lemma OAI.AtomicTriangular.Construction.splitL_norm line 21
  8. lemma OAI.AtomicTriangular.Construction.splitB_norm line 25
  9. lemma OAI.AtomicTriangular.Construction.splitK_norm line 28
  10. lemma OAI.AtomicTriangular.Construction.splitD_norm line 33
  11. lemma OAI.AtomicTriangular.Construction.splitN_nonneg line 37
  12. lemma OAI.AtomicTriangular.Construction.splitQ_nonneg line 38
  13. lemma OAI.AtomicTriangular.Construction.splitQ_lt line 39
  14. lemma OAI.AtomicTriangular.Construction.splitOperator_norm line 40
  15. def OAI.AtomicTriangular.Construction.correctionTail line 56
  16. def OAI.AtomicTriangular.Construction.correctionFinite line 58
  17. lemma OAI.AtomicTriangular.Construction.correctionTail_equation line 60
  18. lemma OAI.AtomicTriangular.Construction.correctionTail_norm line 64
  19. lemma OAI.AtomicTriangular.Construction.correctionFinite_norm line 83
  20. def OAI.AtomicTriangular.Construction.finiteResidualBound line 93
  21. def OAI.AtomicTriangular.Construction.tailResidualBound line 94
  22. def OAI.AtomicTriangular.Construction.tailErrorBound line 95
  23. def OAI.AtomicTriangular.Construction.finiteErrorBound line 96
  24. lemma OAI.AtomicTriangular.Construction.correctionTail_small line 97
  25. lemma OAI.AtomicTriangular.Construction.correctionFinite_small line 108