OAI/Analysis/Triangular/Construction/BlockOperators.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.AtomicTriangular.Construction.FiniteCoefficients line 11
  2. abbrev OAI.AtomicTriangular.Construction.TailCoefficients line 12
  3. lemma OAI.AtomicTriangular.Construction.sum_fin20_pairs line 13
  4. def OAI.AtomicTriangular.Construction.Bkernel line 18
  5. lemma OAI.AtomicTriangular.Construction.Bkernel_bound line 20
  6. def OAI.AtomicTriangular.Construction.Boperator line 24
  7. lemma OAI.AtomicTriangular.Construction.Boperator_norm line 26
  8. def OAI.AtomicTriangular.Construction.Ckernel line 27
  9. lemma OAI.AtomicTriangular.Construction.Ckernel_summable line 29
  10. lemma OAI.AtomicTriangular.Construction.Ckernel_bound line 31
  11. def OAI.AtomicTriangular.Construction.Coperator line 33
  12. lemma OAI.AtomicTriangular.Construction.Coperator_norm line 35
  13. def OAI.AtomicTriangular.Construction.Dkernel line 36
  14. lemma OAI.AtomicTriangular.Construction.Dkernel_summable line 38
  15. lemma OAI.AtomicTriangular.Construction.Dkernel_bound line 40
  16. def OAI.AtomicTriangular.Construction.Doperator line 42
  17. lemma OAI.AtomicTriangular.Construction.Doperator_norm line 44
  18. def OAI.AtomicTriangular.Construction.tailFixedColumn line 45
  19. lemma OAI.AtomicTriangular.Construction.tailFixedColumn_apply line 53
  20. lemma OAI.AtomicTriangular.Construction.tailFixedColumn_norm_finite line 55
  21. lemma OAI.AtomicTriangular.Construction.tailFixedColumn_norm_constant line 60
  22. def OAI.AtomicTriangular.Construction.Roperator line 67
  23. def OAI.AtomicTriangular.Construction.Lplus line 68
  24. def OAI.AtomicTriangular.Construction.Lminus line 69
  25. lemma OAI.AtomicTriangular.Construction.Lplus_norm line 70
  26. lemma OAI.AtomicTriangular.Construction.Lminus_norm line 72
  27. lemma OAI.AtomicTriangular.Construction.Lplus_left_inverse line 74
  28. lemma OAI.AtomicTriangular.Construction.Lminus_left_inverse line 77