RecoveryWeakLimit.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The recovery average converges weakly to its scalar expectation

The average is formed from actual bounded coordinate sequences. Its quotient is computed by continuous functional calculus; the constructed expectation and free-word trace identities then identify its weak limit.

theorem OAI.KadisonKastler.map_recoveryObservable line 24

Source documentation

Naturality of the whole observable, including its continuous cutoff.

theorem map_recoveryObservable (π : B →⋆ₐ[ℂ] C) {n : ℕ} (hn : 0 < n)
    (N : ℕ) (p : B) (u : unitary B) (v : unitary C)
    (huv : π (u : B) = (v : C)) :
    π (recoveryObservable n N p u) = recoveryObservable n N (π p) v := by
…

Mentions: OAI.KadisonKastler.recoveryObservable

theorem OAI.KadisonKastler.map_complex_smul_one line 32
Source documentation
Scalar identities are preserved without any choice of representation.
```
theorem map_complex_smul_one (π : B →⋆ₐ[ℂ] C) (c : ℂ) :
    π (c • (1 : B)) = c • (1 : C) := by
…
```
theorem OAI.KadisonKastler.map_finiteAverage line 37
Source documentation
A star homomorphism commutes with the finite uniform average.
```
theorem map_finiteAverage {ι : Type*} [Fintype ι]
    (π : B →⋆ₐ[ℂ] C) (x : ι → B) :
    π (finiteAverage x) = finiteAverage (fun i => π (x i)) := by
…
```
Mentions: OAI.KadisonKastler.finiteAverage
def OAI.KadisonKastler.sequenceUnitaryEval line 43
Source documentation
The unitary represented by one coordinate of a bounded unitary sequence.
```
def sequenceUnitaryEval (v : unitary (BoundedSequence B)) (j : ℕ) : unitary B :=
…
```
Mentions: OAI.KadisonKastler.BoundedSequence
theorem OAI.KadisonKastler.sequenceUnitaryEval_coe line 47
theorem OAI.KadisonKastler.recoveryObservable_sequence_apply line 52
Source documentation
The sequence-level continuous cutoff evaluates to the actual coordinate contraction.
```
theorem recoveryObservable_sequence_apply {n : ℕ} (hn : 0 < n) (N : ℕ)
    (p : B) (v : unitary (BoundedSequence B)) (j : ℕ) :
    recoveryObservable n N (boundedSequenceConst p) v j =
      recoveryObservable n N p (sequenceUnitaryEval v j) :=
…
```
Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.recoveryObservable, OAI.KadisonKastler.boundedSequenceConst, OAI.KadisonKastler.sequenceUnitaryEval

theorem OAI.KadisonKastler.recoveryAverage_sequence_apply line 59

Source documentation

Evaluation also respects the actual finite averaging operation.

theorem recoveryAverage_sequence_apply {ι : Type*} [Fintype ι]
    {n : ℕ} (hn : 0 < n) (N : ℕ) (p : ι → B)
    (v : ι → unitary (BoundedSequence B)) (j : ℕ) :
    (finiteAverage (fun i => recoveryObservable n N (boundedSequenceConst (p i)) (v i))) j =
      finiteAverage (fun i => recoveryObservable n N (p i) (sequenceUnitaryEval (v i) j)) := by
…

Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.finiteAverage, OAI.KadisonKastler.recoveryObservable, OAI.KadisonKastler.boundedSequenceConst, OAI.KadisonKastler.sequenceUnitaryEval

theorem OAI.KadisonKastler.TraceQuotientMap.weak_scalar_limit line 79
Source documentation
Scalar expectation determines the weak operator limit in the given representation, rather than only in the tracial representation.
```
theorem weak_scalar_limit (s : BoundedSequence (Algebra M)) (c : ℂ)
    (hs : D.baseExpectationCLM hτ (D.quotient s) = c • (1 : C)) :
    WeakOperatorConverges (ω : Filter ℕ)
      (fun j => (s j : H →L[ℂ] H)) (c • ContinuousLinearMap.id ℂ H) := by
…
```
Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.WeakOperatorConverges

theorem OAI.KadisonKastler.TraceQuotientMap.recovery_average_weak_limit line 97

Source documentation

The weak scalar limit of the actual sequence-level recovery average.

theorem recovery_average_weak_limit
    {ι : Type*} [Fintype ι] [Nonempty ι]
    (p : ι → Algebra M) (v : ι → unitary (BoundedSequence (Algebra M)))
    (u : ι → unitary C)
    (hu : ∀ i, D.quotient (v i : BoundedSequence (Algebra M)) = (u i : C))
    (hp : ∀ i, IsStarProjection (p i))
    (hfree : ∀ i, FreeHaarMoments σ D.constant.range (u i))
    {t : ℂ} (hptrace : ∀ i, τ.toLinearMap (p i) = t)
    (ht0 : t ≠ 0) (ht1 : t ≠ 1)
    (hpavg : finiteAverage p = t • (1 : Algebra M))
    {n : ℕ} (hn : 0 < n) (N : ℕ) (i₀ : ι) :
    WeakOperatorConverges (ω : Filter ℕ)
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.finiteAverage, OAI.KadisonKastler.WeakOperatorConverges