RegularCoreModulus.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A uniform tolerance for regular-core descent

The tolerance is obtained from the proved continuous error functions at zero. It is chosen before the Hilbert space, the algebras, and the modular action. Both the original-space gap and the regular tensor gap remain explicit.

theorem OAI.KadisonKastler.exists_regularCore_tolerance line 22

Source documentation

One positive tolerance satisfies every numerical requirement of the regular-core descent and the prescribed final displacement.

theorem exists_regularCore_tolerance {ε : ℝ} (hε : 0 < ε) :
    ∃ t : ℝ, 0 < t ∧
      302 * t < 1 / 100 ∧
      302 * (302 * t) < 174 / 1000000000000000 ∧
      3 * 50948 * Real.sqrt (302 * (302 * t)) < 1 / 100000 ∧
      commonPositionError (302 * (302 * t)) < 1 / 4000000 ∧
      2 * matrixCornerError t < 1 / 1000 ∧
      t + 2 * matrixCornerError t < 1 ∧
      256 * matrixCornerError t < ε := by
…

Mentions: OAI.KadisonKastler.commonPositionError, OAI.KadisonKastler.matrixCornerError

theorem OAI.KadisonKastler.uniform_regularCore_strong_stability line 82

Source documentation

Uniform strong stability from a type II∞ source regular core. The original and tensor gaps are both hypotheses; no ordinary-gap amplification is asserted.

theorem uniform_regularCore_strong_stability
    (h : FiniteFactorPublishedInputs.{u})
    (hComm : PublishedRegularCommutant.{u})
    (hSpectral : PublishedRealSpectralCommutant.{u})
    (hDiagonal : PublishedRealDiagonalDecomposition.{u})
    (hCopies : PublishedProperInfiniteProjectionCopies.{u})
    {ε : ℝ} (hε : 0 < ε) :
    ∃ t : ℝ, 0 < t ∧ ∀ (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℂ H]
      [CompleteSpace H] [TopologicalSpace.SeparableSpace H]
      (M N : VonNeumannAlgebra H),
      PublishedMultiplicationCorrection M →
      PublishedBlockCommutantApproximation (Algebra M) H →
…

Mentions: OAI.KadisonKastler.PublishedMultiplicationCorrection, OAI.KadisonKastler.PublishedBlockCommutantApproximation, OAI.KadisonKastler.Algebra