OAI/Analysis/PureInfiniteness/BoundedPairDiagonalization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The uniform two-entry step for the finite diagonalization in KR02 Lemma 5.7. The implementer bound depends on the diagonal tolerance and norm bound, but not on the off-diagonal entry or its requested error.

  1. theorem OAI.WeakPureInfiniteness.uniform_bounded_pair_diagonalization line 18