NormUltraproductDerivation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Innerness in the norm ultraproduct gives uniform commutator control

This proves the analytic core of the infinitesimal-normalizer contradiction. The hypotheses are simplicity of the type III ultraproduct and invariance under the commutator.

def OAI.KadisonKastler.commutatorAlong line 26
Source documentation
A spatial commutator along a star representation, as a bounded map.
```
def commutatorAlong (φ : A →⋆ₐ[ℂ] E) (T : E) : A →L[ℂ] E :=
…
```
theorem OAI.KadisonKastler.commutatorAlong_apply line 32
theorem OAI.KadisonKastler.normUltraproduct_commutator_in_range line 39

theorem OAI.KadisonKastler.exists_uniform_commutator_correction line 60

Source documentation

Equality of the two derivations gives a single bounded self-adjoint coordinate correction whose commutator norms converge uniformly to zero.

theorem exists_uniform_commutator_correction
    (hPublished : PublishedSimpleDerivationInner.{u})
    (φ : ∀ j, B j →⋆ₐ[ℂ] C j) (hφ : ∀ j, Function.Injective (φ j))
    (ω : Ultrafilter ℕ) (hSimple : CStarSimple (NormUltraproduct B ω))
    (T : VaryingBoundedSequence C) (hT : IsSelfAdjoint T)
    (hrange : ∀ x : VaryingBoundedSequence B,
      ∃ y : VaryingBoundedSequence B,
        NormNullSequence C ω (T * normProductMap φ x - normProductMap φ x * T -
          normProductMap φ y)) :
    ∃ a : VaryingBoundedSequence B, IsSelfAdjoint a ∧
      Tendsto (fun j => ‖commutatorAlong (φ j) (T j - φ j (a j))‖)
        (ω : Filter ℕ) (𝓝 0) := by
…

Mentions: OAI.KadisonKastler.CStarSimple, OAI.KadisonKastler.NormUltraproduct, OAI.KadisonKastler.VaryingBoundedSequence, OAI.KadisonKastler.NormNullSequence, OAI.KadisonKastler.normProductMap, OAI.KadisonKastler.commutatorAlong