RemoteScalingLimit.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Coisometries with a prescribed asymptotic modular ratio

The finite-site constructions give genuine coisometries. Their modular ratios converge to an arbitrary number in the open unit interval, and their conjugations converge strongly to the identity.

theorem OAI.KadisonKastler.PointedMatrixSites.exists_remote_scaling_conjugations line 28

theorem OAI.KadisonKastler.scaling_vector_limit line 61

Source documentation

A converging state ratio gives the corresponding approximate modular vector equation for every uniformly contractive coisometry sequence.

theorem scaling_vector_limit (J : H ≃ₗᵢ⋆[ℂ] H)
    (hsep : Function.Injective (algebraVectorMap M Ω))
    (hcyc : DenseRange (algebraVectorMap M Ω))
    (s : ℕ → ℝ) (v : ℕ → Algebra M) {r : ℝ}
    (hs : Tendsto s atTop (𝓝 r)) (hpos : ∀ n, 0 < s n)
    (hv : ∀ n, v n*star (v n)=1)
    (hscale : ∀ n, StateScales M Ω (s n) (v n).val) :
    Tendsto (fun n => (v n).val Ω - (Real.sqrt r : ℂ) •
      tomitaPolarConjugation J Ω hsep hcyc (star (v n).val Ω)) atTop (𝓝 0) := by
…

Mentions: OAI.KadisonKastler.algebraVectorMap, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.StateScales, OAI.KadisonKastler.tomitaPolarConjugation