OAI/Analysis/PureInfiniteness/TailCancellationRows.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Literal row identities for removing the full tail in the absorption construction. The complementary subcorner is fixed, not estimated away.

  1. def OAI.WeakPureInfiniteness.TailCancellation.full line 12
  2. def OAI.WeakPureInfiniteness.TailCancellation.rest line 13
  3. def OAI.WeakPureInfiniteness.TailCancellation.support line 14
  4. def OAI.WeakPureInfiniteness.TailCancellation.sourceRow line 16
  5. def OAI.WeakPureInfiniteness.TailCancellation.targetRow line 19
  6. structure OAI.WeakPureInfiniteness.TailCancellation.Geometry line 21
  7. lemma OAI.WeakPureInfiniteness.TailCancellation.geometry line 37
  8. lemma OAI.WeakPureInfiniteness.TailCancellation.support_ne_zero line 87
  9. lemma OAI.WeakPureInfiniteness.TailCancellation.rest_commute line 94
  10. lemma OAI.WeakPureInfiniteness.TailCancellation.support_commute line 98
  11. lemma OAI.WeakPureInfiniteness.TailCancellation.orthogonal_sum_gram line 101
  12. lemma OAI.WeakPureInfiniteness.TailCancellation.source_gram line 132
  13. lemma OAI.WeakPureInfiniteness.TailCancellation.target_gram line 143
  14. lemma OAI.WeakPureInfiniteness.TailCancellation.source_support line 152
  15. lemma OAI.WeakPureInfiniteness.TailCancellation.target_support line 168
  16. lemma OAI.WeakPureInfiniteness.TailCancellation.conjugate_fixed_corner line 179
  17. lemma OAI.WeakPureInfiniteness.TailCancellation.recombination_norm line 189