OAI/Analysis/PureInfiniteness/OneStepAbelianRange.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The finite approximation consequence of KR02 Proposition 7.14. Positive commuting targets and finite inner approximation suffice; the proof constructs the single coefficient rather than assuming one-step innerness.

  1. lemma OAI.WeakPureInfiniteness.norm_apply_le_fourPositiveParts line 19
  2. theorem OAI.WeakPureInfiniteness.approximately_oneStep_of_abelian_range line 36