FiniteCoefficientTests.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Directed finite tests on arbitrary Hilbert spaces

Local approximations need not agree on overlapping tests. An ultrafilter extending the directed test filter produces the coefficient limits needed by the UCP criterion.

def OAI.KadisonKastler.FiniteCoefficientConjugations line 29
Source documentation
The finite coefficient condition supplied by separable restrictions in the manuscript. It asserts no global range inclusion for a local conjugacy.
```
def FiniteCoefficientConjugations (M N : VonNeumannAlgebra H) (a : ℝ) : Prop :=
…
```
theorem OAI.KadisonKastler.concrete_unitary_of_finite_coefficient_tests line 39
Source documentation
Assemble all finite tests, take the UCP limit, and apply the concrete correction theorem on the original ambient Hilbert space.
```
theorem concrete_unitary_of_finite_coefficient_tests
    (hCorrection : PublishedMultiplicationCorrection M)
    (hCommutant : PublishedBlockCommutantApproximation (Algebra M) H)
    {a g : ℝ} (ha : 0 ≤ a) (htests : FiniteCoefficientConjugations M N a)
    (hsmall : 2 * a < 1 / 1000) (hge : g + 2 * a < 1)
    (hgap : kkDistance M N < g) :
    ∃ u : unitary (H →L[ℂ] H), Conjugates u M N ∧
      ‖(u : H →L[ℂ] H) - 1‖ ≤ 256 * a := by
…
```
Mentions: OAI.KadisonKastler.PublishedMultiplicationCorrection, OAI.KadisonKastler.PublishedBlockCommutantApproximation, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteCoefficientConjugations, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.Conjugates