InjectiveStability.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Strong stability when the source algebra is injective

The one-sided amenable embedding gives a nearby conjugate subalgebra of the neighbor. Riesz's lemma forces this inclusion to be equality once the unit-ball gap is below one. No second perturbation or injectivity of the neighbor is required.

theorem OAI.KadisonKastler.eq_of_le_of_kkDistance_lt_one line 26
Source documentation
A proper closed linear subspace cannot approximate the entire unit ball with uniform error less than one. Applied inside the larger algebra, this turns a sufficiently close inclusion into equality.
```
theorem eq_of_le_of_kkDistance_lt_one {P Q : VonNeumannAlgebra H}
    (hPQ : P ≤ Q) (hgap : kkDistance P Q < 1) : P = Q := by
…
```
Mentions: OAI.KadisonKastler.kkDistance
theorem OAI.KadisonKastler.exists_injective_conjugacy_of_kkDistance_lt line 52
Source documentation
The one-sided embedding already gives equality for an injective source at a sufficiently small ordinary distance.
```
theorem exists_injective_conjugacy_of_kkDistance_lt
    (hpub : PublishedAmenableEmbedding (H := H))
…
```
Mentions: OAI.KadisonKastler.PublishedAmenableEmbedding
theorem OAI.KadisonKastler.uniform_injective_strong_stability line 73
Source documentation
The tolerance is independent of the Hilbert space and the two algebras. Only the source must be injective.
```
theorem uniform_injective_strong_stability {ε : ℝ} (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧
      ∀ (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H],
      PublishedAmenableEmbedding (H := H) →
…
```
Mentions: OAI.KadisonKastler.PublishedAmenableEmbedding