OAI/Analysis/KadisonKastler/FiniteFactorModulus.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.continuous_commonPositionError line 13
2. theorem OAI.KadisonKastler.commonPositionError_zero line 17
3. theorem OAI.KadisonKastler.continuous_finiteFactorError line 20
4. theorem OAI.KadisonKastler.finiteFactorError_zero line 26
5. theorem OAI.KadisonKastler.commonPositionError_monotone line 29
6. theorem OAI.KadisonKastler.finiteFactorError_monotone line 34
7. theorem OAI.KadisonKastler.exists_finiteFactor_tolerance line 43

   Source documentation

   All smallness requirements hold at one positive tolerance, uniformly in the factors and the Hilbert space.

   theorem exists_finiteFactor_tolerance {ε : ℝ} (hε : 0 < ε) :
       ∃ t : ℝ, 0 < t ∧ t < 1 / 100 ∧
         302 * t < 174 / 1000000000000000 ∧
         3 * 50948 * Real.sqrt (302 * t) < 1 / 100000 ∧
         commonPositionError (302 * t) < 1 / 2400 ∧ finiteFactorError t < ε := by
   …

   Mentions: OAI.KadisonKastler.commonPositionError, OAI.KadisonKastler.finiteFactorError