DenseUnitBallGap.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Passing unit-ball approximation through weakly dense tests

A bounded target family has a weak operator ultralimit. The same uniform approximation bound survives this limit, allowing bounds on weakly dense unit-ball tests to control the full Kadison--Kastler gap.

theorem OAI.KadisonKastler.exists_unitBall_approx_of_weak_limit line 23

Source documentation

A uniform approximation by the target unit ball survives an arbitrary nontrivial coefficientwise convergent net.

theorem exists_unitBall_approx_of_weak_limit
    {ι : Type*} {l : Filter ι} [l.NeBot] (N : VonNeumannAlgebra H)
    (T : ι → H →L[ℂ] H) (a : H →L[ℂ] H)
    (hlim : ∀ x y, Tendsto (fun i => inner ℂ y (T i x)) l
      (𝓝 (inner ℂ y (a x))))
    {r : ℝ} (hr : 0 ≤ r)
    (hnear : ∀ i, ∃ b ∈ unitBall N, ‖T i - b‖ ≤ r) :
    ∃ b ∈ unitBall N, ‖a - b‖ ≤ r := by
…

Mentions: OAI.KadisonKastler.unitBall

def OAI.KadisonKastler.WeakUnitBallDense line 46
Source documentation
A family of contractions whose coefficientwise limits cover the whole unit ball. No metrizability or choice of a sequence is required.
```
def WeakUnitBallDense {ι : Type*} (T : ι → H →L[ℂ] H) (M : VonNeumannAlgebra H) : Prop :=
…
```
theorem OAI.KadisonKastler.exists_unitBall_approx_of_weakly_dense_tests line 51

theorem OAI.KadisonKastler.kkDistance_le_of_weakly_dense_tests line 62

Source documentation

Two weakly dense test families suffice to bound the full gap.

theorem kkDistance_le_of_weakly_dense_tests
    {ι κ : Type*} (M N : VonNeumannAlgebra H)
    (T : ι → H →L[ℂ] H) (S : κ → H →L[ℂ] H)
    (hT : WeakUnitBallDense T M) (hS : WeakUnitBallDense S N)
    {r : ℝ} (hr : 0 ≤ r)
    (hTN : ∀ i, ∃ b ∈ unitBall N, ‖T i - b‖ ≤ r)
    (hSM : ∀ j, ∃ a ∈ unitBall M, ‖S j - a‖ ≤ r) :
    kkDistance M N ≤ r := by
…

Mentions: OAI.KadisonKastler.WeakUnitBallDense, OAI.KadisonKastler.unitBall, OAI.KadisonKastler.kkDistance