Amenable.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Conditional strong stability for injective represented algebras

The hypothesis ChristensenMutual is the mutual near-inclusion consequence of Cameron–Christensen–Sinclair–Smith–White–Wiggins, Kadison–Kastler stable factors, Duke Math. J. 163 (2014), Theorem 3.3(i), building on Christensen, Near inclusions of C-algebras* (1980). The stability theorem is conditional on this near-inclusion property.

def OAI.KadisonKastler.IsInjective line 25
Source documentation
Injectivity in the given representation, expressed as a contractive linear projection of the ambient bounded operators onto the algebra. Normality of the projection is not required.
```
def IsInjective (M : VonNeumannAlgebra H) : Prop :=
…
```
def OAI.KadisonKastler.NearInclusion line 31
Source documentation
The strict near-inclusion convention of the published input. Approximants belong to the algebra, but need not lie in its unit ball.
```
def NearInclusion (M N : VonNeumannAlgebra H) (γ : ℝ) : Prop :=
…
```
theorem OAI.KadisonKastler.nearInclusion_of_kkDistance_lt line 35
def OAI.KadisonKastler.ChristensenMutual line 47
Source documentation
Precise published input: the mutual case of CCSSWW (2014), Theorem 3.3(i). The location of the unitary in (M ∪ N)'' is omitted because this application does not use it. The equality conclusion applies for γ < 1/101.
```
def ChristensenMutual : Prop :=
…
```
theorem OAI.KadisonKastler.injective_nearConjugacy_of_kkDistance_lt line 56
Source documentation
The concrete tolerance used in conditional injective-class stability. It depends only on the requested displacement, not on the represented algebras or on their Hilbert space.
```
theorem injective_nearConjugacy_of_kkDistance_lt
    (hChristensen : ChristensenMutual (H := H)) {ε : ℝ} (hε : 0 < ε)
…
```
Mentions: OAI.KadisonKastler.ChristensenMutual
theorem OAI.KadisonKastler.injective_strong_stability line 73
Source documentation
Conditional injective strong stability in a fixed representation.
```
theorem injective_strong_stability (hChristensen : ChristensenMutual (H := H))
…
```
Mentions: OAI.KadisonKastler.ChristensenMutual
theorem OAI.KadisonKastler.universal_injective_strong_stability line 83
Source documentation
Conditional strong stability uniformly over the injective class and all Hilbert-space representations. The tolerance is chosen before the Hilbert space.
```
theorem universal_injective_strong_stability
    (hChristensen : ∀ (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℂ H]
      [CompleteSpace H], ChristensenMutual (H := H)) :
…
```
Mentions: OAI.KadisonKastler.ChristensenMutual