OAI/Topology/CoarseAssembly/HilbertHeadTail.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The head and tail decomposition used in finite-cycle telescoping

  1. def OAI.CoarseAssembly.Analytic.tailInsertVector line 13
  2. theorem OAI.CoarseAssembly.Analytic.tailInsertVector_norm line 21
  3. def OAI.CoarseAssembly.Analytic.tailInsert line 29
  4. theorem OAI.CoarseAssembly.Analytic.tailInsert_zero line 43
  5. theorem OAI.CoarseAssembly.Analytic.tailInsert_succ line 46
  6. theorem OAI.CoarseAssembly.Analytic.tailInsert_single line 49
  7. theorem OAI.CoarseAssembly.Analytic.tailInsert_adjoint_apply line 61
  8. theorem OAI.CoarseAssembly.Analytic.head_tail_orthogonal line 70
  9. theorem OAI.CoarseAssembly.Analytic.head_tail_exhaustive line 77