OAI/Analysis/PureInfiniteness/RectangularReturnDefect.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A multiplicative-defect bound for the concrete finite return map G* X G. Only a contractive column and square roots in a finite matrix algebra are used.

  1. def OAI.WeakPureInfiniteness.columnReturn line 15
  2. lemma OAI.WeakPureInfiniteness.columnReturn_multiplicative_defect line 18