ExpectedModularPreparation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Modular preparation from an expected finite subalgebra

The trace used here is only on the finite subalgebra. Its composition with an actual bimodular expectation is represented by the supplied vector. The modular conjugation data then give precisely the common right-vector identity used by matrix averaging and graph comparison. The corrected neighbor is proved cyclic and separating when the two ordinary gaps are small; these properties are not supplied as preparation assumptions.

theorem OAI.KadisonKastler.ModularConjugationData.common_vector_of_expectation line 32

Source documentation

Bimodularity of an expectation onto a finite algebra supplies the centralizer hypothesis required by modular conjugation.

theorem common_vector_of_expectation
    (d : ModularConjugationData M Ω) (hRM : R ≤ M)
    (τ : FaithfulTracialState (Algebra R))
    (P : Algebra M →L[ℂ] Algebra R)
    (hleft : ∀ (r : Algebra R) (x : Algebra M),
      P (StarSubalgebra.inclusion hRM r * x) = r * P x)
    (hright : ∀ (r : Algebra R) (x : Algebra M),
      P (x * StarSubalgebra.inclusion hRM r) = P x * r)
    (hΩ : ∀ x : Algebra M, expectedTrace τ P x = inner ℂ Ω (x.val Ω))
    (r : Algebra R) :
    conjugationOperator d.conjugation (star r.val) Ω = r.val Ω :=
…

Mentions: OAI.KadisonKastler.ModularConjugationData, OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.expectedTrace, OAI.KadisonKastler.conjugationOperator

theorem OAI.KadisonKastler.ModularConjugationData.expected_right_data line 48

Source documentation

The expected-state vector has unit norm, and its common right action has the exact membership and vector identities needed in preparation.

theorem expected_right_data
    (d : ModularConjugationData M Ω) (hRM : R ≤ M)
    (τ : FaithfulTracialState (Algebra R))
    (P : Algebra M →L[ℂ] Algebra R) (hP : P 1 = 1)
    (hleft : ∀ (r : Algebra R) (x : Algebra M),
      P (StarSubalgebra.inclusion hRM r * x) = r * P x)
    (hright : ∀ (r : Algebra R) (x : Algebra M),
      P (x * StarSubalgebra.inclusion hRM r) = P x * r)
    (hΩ : ∀ x : Algebra M, expectedTrace τ P x = inner ℂ Ω (x.val Ω)) :
    ‖Ω‖ = 1 ∧
      (∀ r ∈ R, conjugationOperator d.conjugation r ∈ M.commutant) ∧
      (∀ r ∈ R, conjugationOperator d.conjugation (star r) Ω = r Ω) := by
…

Mentions: OAI.KadisonKastler.ModularConjugationData, OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.expectedTrace, OAI.KadisonKastler.conjugationOperator

theorem OAI.KadisonKastler.unitaryConjugateAlgebra_commutant line 70
Source documentation
Conjugation transports the actual commutant, so the same elementary movement bound applies to the second gap in preparation.
```
theorem unitaryConjugateAlgebra_commutant
    (w : unitary (H →L[ℂ] H)) (N : VonNeumannAlgebra H) :
    (unitaryConjugateAlgebra w N).commutant =
      unitaryConjugateAlgebra w N.commutant := by
…
```
Mentions: OAI.KadisonKastler.unitaryConjugateAlgebra
theorem OAI.KadisonKastler.preparedPair_second_correction_commutant_gap line 93
theorem OAI.KadisonKastler.exists_expected_modular_graph_comparison line 111
Source documentation
An expected finite common algebra and actual modular conjugation supply the graph estimate without separate right-action assumptions.
```
theorem exists_expected_modular_graph_comparison
    (hpub : PublishedLocalizedAmenableEmbedding (H := H))
…
```
Mentions: OAI.KadisonKastler.PublishedLocalizedAmenableEmbedding

theorem OAI.KadisonKastler.expected_modular_corrected_cyclic_separating line 158

Source documentation

The same expected vector is cyclic and separating for the corrected neighbor. Smallness of the commutant gap is stated independently of the left gap and transported through the actual chosen correction.

theorem expected_modular_corrected_cyclic_separating
    (M N R : VonNeumannAlgebra H) (hRM : R ≤ M)
    (τ : FaithfulTracialState (Algebra R))
    (P : Algebra M →L[ℂ] Algebra R) (hP : P 1 = 1)
    (hleft : ∀ (r : Algebra R) (x : Algebra M),
      P (StarSubalgebra.inclusion hRM r * x) = r * P x)
    (hright : ∀ (r : Algebra R) (x : Algebra M),
      P (x * StarSubalgebra.inclusion hRM r) = P x * r)
    (Ω : H) (hΩ : ∀ x : Algebra M, expectedTrace τ P x = inner ℂ Ω (x.val Ω))
    (d : ModularConjugationData M Ω)
    (s : ℕ → ℕ) (E : ∀ n, MatrixUnitSystem (Fin (s n)) (H →L[ℂ] H))
    (hmono : Monotone (fun n => (E n).algebra))
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.expectedTrace, OAI.KadisonKastler.ModularConjugationData