RelativeOneStep.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The relative-domain form of KR02 Proposition 7.14 needed for the nuclear subalgebra of the ultrapower. The witnesses lie in the ambient algebra.

def OAI.WeakPureInfiniteness.ApproximatelyInnerAlong line 16
Source documentation
Finite inner approximation relative to the specified inclusion.
```
def ApproximatelyInnerAlong (φ : B →⋆ₙₐ[ℂ] D) (T : B → D) : Prop :=
…
```
def OAI.WeakPureInfiniteness.ApproximatelyOneStepAlong line 22
Source documentation
One-coefficient approximation relative to the specified inclusion.
```
def ApproximatelyOneStepAlong (φ : B →⋆ₙₐ[ℂ] D) (T : B → D) : Prop :=
…
```
lemma OAI.WeakPureInfiniteness.ApproximatelyOneStepAlong.of_pointNorm_approximation line 26
theorem OAI.WeakPureInfiniteness.approximately_oneStepAlong_of_abelian_range line 49
Source documentation
The finite one-step reduction applies to any subalgebra inclusion, without requiring the whole ambient ultrapower to be nuclear or separable.
```
theorem approximately_oneStepAlong_of_abelian_range (hP : MainGap.PropertyP A)
    (φ : B →⋆ₙₐ[ℂ] N) (T : B →L[ℂ] N) (hT : ApproximatelyInnerAlong φ T)
    (hpos : ∀ b, 0 ≤ b → 0 ≤ T b) (hcomm : ∀ b c, Commute (T b) (T c)) :
    ApproximatelyOneStepAlong φ T := by
…
```
Mentions: OAI.MainGap.PropertyP, OAI.WeakPureInfiniteness.ApproximatelyInnerAlong, OAI.WeakPureInfiniteness.ApproximatelyOneStepAlong