PublishedCommonPosition.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The published common tracial position input

This is the application-specific part of Cameron--Christensen--Sinclair-- Smith--White--Wiggins, Kadison--Kastler stable factors, Duke Math. J. 163 (2014), Lemma 4.10(i)--(iv),(vii), printed pp. 20--21, arXiv:1209.4116v3. The constant is 50948 * sqrt g and the hypothesis is g < 1.74 * 10^(-13).

We specialize their amenable subalgebra hypothesis to a scalar relative commutant, which is the only case used here. The output records algebraic equivalences onto the represented images and their actual vector traces. No isomorphism between the two nearby factors is assumed.

structure OAI.KadisonKastler.CommonTracialPositionData line 37

Source documentation

Common-position data retaining only the conclusions used in the finite-factor application.

structure CommonTracialPositionData
    (M N R : VonNeumannAlgebra H) (hRM : R ≤ M) (hRN : R ≤ N) (g : ℝ)
    (K : Type u) [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] where
…

def OAI.KadisonKastler.PublishedCommonTracialPosition line 73
Source documentation
Precise published input, specialized to the common irreducible amenable subalgebra needed by the finite-factor argument.
```
def PublishedCommonTracialPosition : Prop :=
…
```
theorem OAI.KadisonKastler.CommonTracialPositionData.left_isII1 line 94
theorem OAI.KadisonKastler.CommonTracialPositionData.right_isII1 line 99

theorem OAI.KadisonKastler.CommonTracialPositionData.irreducible_left line 106

Source documentation

The original relative commutant transfers through the faithful representations and the common restriction.

theorem irreducible_left
    (hirr : ∀ a : Algebra M,
      (∀ r : Algebra R, coordinateInclusion hRM r * a = a * coordinateInclusion hRM r) →
      ∃ c : ℂ, a = c • (1 : Algebra M))
    (x : Algebra d.left)
    (hx : ∀ r : Algebra d.common,
      coordinateInclusion d.common_le_left r * x = x * coordinateInclusion d.common_le_left r) :
    ∃ c : ℂ, x = c • (1 : Algebra d.left) := by
…

Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.CommonTracialPositionData.distance_le line 134

theorem OAI.KadisonKastler.CommonTracialPositionData.conjugations_sub_le line 139

Source documentation

The common-position output supplies the full tracial-conjugation estimate and its module structure.

theorem conjugations_sub_le
    (hirr : ∀ a : Algebra M,
      (∀ r : Algebra R, coordinateInclusion hRM r * a = a * coordinateInclusion hRM r) →
      ∃ c : ℂ, a = c • (1 : Algebra M))
    {b : ℝ} (hb : 2 * d.tolerance < b) :
    ‖(d.leftPosition.conjugation : K →L⋆[ℂ] K) -
      (d.rightPosition.conjugation : K →L⋆[ℂ] K)‖ ≤ 768 * b := by
…

Mentions: OAI.KadisonKastler.Algebra