OAI/Analysis/KadisonKastler/SpatialTensorModulus.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KadisonKastler.spatialDescentTolerance line 22

   Source documentation

   The auxiliary tolerance used before choosing any representation or algebra.

   def spatialDescentTolerance (ε : ℝ) : ℝ := min (ε / 512) (1 / 4000)

2. theorem OAI.KadisonKastler.spatialDescentTolerance_pos line 24
3. theorem OAI.KadisonKastler.nearConjugacy_of_spatial_product line 31

   Source documentation

   A sufficiently small spatial-product conjugacy gives a conjugacy of the original pair, with the prescribed strict displacement.

   theorem nearConjugacy_of_spatial_product
       {M N : VonNeumannAlgebra H} (D : VonNeumannAlgebra K)
       (hCorrection : PublishedMultiplicationCorrection M)
       (hCommutant : PublishedBlockCommutantApproximation (Algebra M) H)
       (ξ : K) (hξ : ‖ξ‖ = 1) {ε : ℝ} (hε : 0 < ε)
       (hgap : kkDistance M N < 1 / 4)
       (h : NearConjugacy (spatialProductAlgebra M D) (spatialProductAlgebra N D)
         (spatialDescentTolerance ε)) : NearConjugacy M N ε := by
   …

   Mentions: OAI.KadisonKastler.PublishedMultiplicationCorrection, OAI.KadisonKastler.PublishedBlockCommutantApproximation, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.NearConjugacy, OAI.KadisonKastler.spatialProductAlgebra, OAI.KadisonKastler.spatialDescentTolerance