Basic.lean`

34 declarations, 0 contain sorry, 0 declared as axioms

The concrete Kadison–Kastler distance

The distance is the operator-norm Hausdorff distance between the closed unit balls of two concrete, unital von Neumann algebras. All Hilbert spaces are allowed, including the zero space. The elementary estimates belong to §2 of Universal strong Kadison–Kastler stability (2026).

def OAI.KadisonKastler.unitBall line 27
Source documentation
The operator-norm closed unit ball, as a subset of the ambient operators.
Also declared: ComparatorChallenges/StrongKadisonKastler.lean:16 (same declaration text).
```
def unitBall (M : VonNeumannAlgebra H) : Set (H →L[ℂ] H) :=
…
```
theorem OAI.KadisonKastler.mem_unitBall line 30
theorem OAI.KadisonKastler.zero_mem_unitBall line 33
theorem OAI.KadisonKastler.unitBall_nonempty line 36
theorem OAI.KadisonKastler.unitBall_bounded line 39
def OAI.KadisonKastler.kkDistance line 43
Source documentation
Kadison and Kastler's ordinary distance, without matrix amplification.
Also declared: ComparatorChallenges/StrongKadisonKastler.lean:19 (same declaration text).
```
noncomputable def kkDistance (M N : VonNeumannAlgebra H) : ℝ :=
…
```
theorem OAI.KadisonKastler.unitBall_hausdorffEDist_ne_top line 46
theorem OAI.KadisonKastler.kkDistance_nonneg line 51
theorem OAI.KadisonKastler.kkDistance_self line 54
theorem OAI.KadisonKastler.kkDistance_comm line 57
theorem OAI.KadisonKastler.kkDistance_triangle line 60
theorem OAI.KadisonKastler.kkDistance_le_one line 64
theorem OAI.KadisonKastler.exists_unitBall_approx line 72
Source documentation
A strict distance bound supplies a contractive approximant in the other algebra.
```
theorem exists_unitBall_approx {M N : VonNeumannAlgebra H} {x : H →L[ℂ] H}
    (hx : x ∈ unitBall M) {r : ℝ} (hr : kkDistance M N < r) :
    ∃ y ∈ unitBall N, ‖x - y‖ < r := by
…
```
Mentions: OAI.KadisonKastler.unitBall, OAI.KadisonKastler.kkDistance
def OAI.KadisonKastler.unitaryConj line 79
Source documentation
Conjugation by an ambient unitary operator.
Also declared: ComparatorChallenges/StrongKadisonKastler.lean:22 (same declaration text).
```
def unitaryConj (v : unitary (H →L[ℂ] H)) (x : H →L[ℂ] H) : H →L[ℂ] H :=
…
```
theorem OAI.KadisonKastler.unitaryConj_one line 82
theorem OAI.KadisonKastler.norm_unitaryConj line 85
theorem OAI.KadisonKastler.unitaryConj_sub line 89
theorem OAI.KadisonKastler.isometry_unitaryConj line 93
theorem OAI.KadisonKastler.unitaryConj_star_unitaryConj line 98
theorem OAI.KadisonKastler.unitaryConj_mul line 107
def OAI.KadisonKastler.Conjugates line 112
Source documentation
This expresses v M v* = N in the original Hilbert space.
Also declared: ComparatorChallenges/StrongKadisonKastler.lean:25 (same declaration text).
```
def Conjugates (v : unitary (H →L[ℂ] H)) (M N : VonNeumannAlgebra H) : Prop :=
…
```
def OAI.KadisonKastler.NearConjugacy line 116
Source documentation
The conclusion of strong stability, with a strict displacement bound.
Also declared: ComparatorChallenges/StrongKadisonKastler.lean:28 (same declaration text).
```
def NearConjugacy (M N : VonNeumannAlgebra H) (ε : ℝ) : Prop :=
…
```
theorem OAI.KadisonKastler.conjugates_one line 119
theorem OAI.KadisonKastler.Conjugates.symm line 122
theorem OAI.KadisonKastler.Conjugates.trans line 128
theorem OAI.KadisonKastler.nearConjugacy_self line 135
theorem OAI.KadisonKastler.unitaryConj_unitBall line 139
theorem OAI.KadisonKastler.norm_unitaryConj_sub_le line 156
Source documentation
The elementary displacement estimate used at every matrix level in §2.
```
theorem norm_unitaryConj_sub_le (v : unitary (H →L[ℂ] H)) (x : H →L[ℂ] H) :
    ‖unitaryConj v x - x‖ ≤ 2 * ‖(v : H →L[ℂ] H) - 1‖ * ‖x‖ := by
…
```
Mentions: OAI.KadisonKastler.unitaryConj
theorem OAI.KadisonKastler.kkDistance_le_of_conjugates line 177
theorem OAI.KadisonKastler.kkDistance_eq_of_conjugates line 195
Source documentation
The same unitary change of position leaves the distance unchanged.
```
theorem kkDistance_eq_of_conjugates {M N P Q : VonNeumannAlgebra H}
    {v : unitary (H →L[ℂ] H)} (hMN : Conjugates v M N) (hPQ : Conjugates v P Q) :
    kkDistance N Q = kkDistance M P := by
…
```
Mentions: OAI.KadisonKastler.Conjugates, OAI.KadisonKastler.kkDistance
theorem OAI.KadisonKastler.kkDistance_conjugate_le line 204
Source documentation
Moving one algebra by a small unitary increases its gap by at most twice the unitary displacement (the ordinary-distance part of equation (2.1)).
```
theorem kkDistance_conjugate_le {M N P : VonNeumannAlgebra H}
    {v : unitary (H →L[ℂ] H)} (hv : Conjugates v N P) :
    kkDistance M P ≤ kkDistance M N + 2 * ‖(v : H →L[ℂ] H) - 1‖ :=
…
```
Mentions: OAI.KadisonKastler.Conjugates, OAI.KadisonKastler.kkDistance

theorem OAI.KadisonKastler.norm_unitary_mul_sub_one_le line 210

Source documentation

Errors add when two unitary changes of position are composed.

theorem norm_unitary_mul_sub_one_le (v w : unitary (H →L[ℂ] H)) :
    ‖((v * w : unitary (H →L[ℂ] H)) : H →L[ℂ] H) - 1‖ ≤
      ‖(v : H →L[ℂ] H) - 1‖ + ‖(w : H →L[ℂ] H) - 1‖ := by
…

theorem OAI.KadisonKastler.NearConjugacy.symm line 220
theorem OAI.KadisonKastler.NearConjugacy.trans line 231