OAI/Analysis/KadisonKastler/ConstructedFiniteFactorModulus.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.continuous_constructedFiniteFactorError line 14
2. theorem OAI.KadisonKastler.constructedFiniteFactorError_zero line 20
3. theorem OAI.KadisonKastler.constructedFiniteFactorError_monotone line 23
4. theorem OAI.KadisonKastler.exists_constructed_finiteFactor_tolerance line 32

   Source documentation

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

   theorem exists_constructed_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 / 4000000 ∧ constructedFiniteFactorError t < ε := by
   …

   Mentions: OAI.KadisonKastler.commonPositionError, OAI.KadisonKastler.constructedFiniteFactorError