OAI/Analysis/Nuclearity/UnitizedCoefficientOneStep.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The finite coefficient estimate and one-step implementation remain valid for unitization coefficients. All implementing elements remain in D.

  1. lemma OAI.WeakPureInfiniteness.unitizedCoefficientEnlargement_error_le line 16
  2. lemma OAI.WeakPureInfiniteness.ApproximatelyOneStepAlong.unitizedCoefficientEnlargement line 27