OAI/Analysis/OInfinity/FiniteRowDefect.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Exact defects of the finite row isometry

The explicit finite sum gives both forward and adjoint intertwining errors. Its range projection is almost central and has small compression of the source vacuum. These estimates do not discard either complementary corner.

  1. lemma OAI.WeakPureInfiniteness.row_forward_square line 20
  2. lemma OAI.WeakPureInfiniteness.row_backward_square line 39
  3. lemma OAI.WeakPureInfiniteness.finiteRow_ratio_sub line 59
  4. def OAI.WeakPureInfiniteness.finiteRowRange line 66

    Source documentation

    The actual range projection of the finite isometry.

    def finiteRowRange (s t : I → E) (r q : E) (m : ℕ) : E :=
…
  5. lemma OAI.WeakPureInfiniteness.finiteRowRange_star line 70
  6. lemma OAI.WeakPureInfiniteness.finiteRow_target_left line 83
  7. lemma OAI.WeakPureInfiniteness.finiteRowIsometry_forward_square line 94
  8. lemma OAI.WeakPureInfiniteness.finiteRowIsometry_backward_square line 110
  9. lemma OAI.WeakPureInfiniteness.finiteRowIsometry_vacuum_compression line 122
  10. lemma OAI.WeakPureInfiniteness.finiteRowIsometry_norm_le line 136
  11. lemma OAI.WeakPureInfiniteness.finiteRowIsometry_forward_norm_sq line 142
  12. lemma OAI.WeakPureInfiniteness.finiteRowIsometry_backward_norm_sq line 152
  13. lemma OAI.WeakPureInfiniteness.finiteRowRange_sq line 169
  14. lemma OAI.WeakPureInfiniteness.finiteRowRange_vacuum line 179
  15. lemma OAI.WeakPureInfiniteness.finiteRowRange_vacuum_norm line 194
  16. lemma OAI.WeakPureInfiniteness.finiteRowRange_commutator_bound line 205