RecoveryExpectation.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The affine expectation of the scalar recovery observable

def OAI.KadisonKastler.recoveryObservable line 19
Source documentation
The expression averaged over the finite random choices in the scalar recovery argument.
```
def recoveryObservable (n N : ℕ) (p : B) (u : unitary B) : B :=
…
```
theorem OAI.KadisonKastler.norm_recoveryObservable_le line 23
theorem OAI.KadisonKastler.recoveryObservable_mem_projectionHaarClosedAlgebra line 42
theorem OAI.KadisonKastler.FreeHaarMoments.recoveryExpectation_affine line 48

theorem OAI.KadisonKastler.freeHaar_recoveryObservable_pairings_eq line 63

Source documentation

The two determining trace values of the recovery observable are independent of the free pair, with the projection trace fixed.

theorem freeHaar_recoveryObservable_pairings_eq
    (τ : FaithfulTracialState B) (σ : FaithfulTracialState C)
    {A : StarSubalgebra ℂ B} {D : StarSubalgebra ℂ C}
    {u : unitary B} {v : unitary C}
    (hu : FreeHaarMoments τ A u) (hv : FreeHaarMoments σ D v)
    {p : B} {q : C} (hp : IsStarProjection p) (hq : IsStarProjection q)
    (hpA : p ∈ A) (hqD : q ∈ D) {t : ℂ}
    (hpτ : τ.toLinearMap p = t) (hqσ : σ.toLinearMap q = t)
    {n : ℕ} (hn : 0 < n) (N : ℕ) :
    τ.toLinearMap (recoveryObservable n N p u) =
      σ.toLinearMap (recoveryObservable n N q v) ∧
    τ.toLinearMap (p * recoveryObservable n N p u) =
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.recoveryObservable

theorem OAI.KadisonKastler.finiteAverage_recoveryExpectation line 85

Source documentation

The actual recovery observables have scalar averaged expectation. The averaging premise refers only to the finite family of projections.

theorem finiteAverage_recoveryExpectation
    {ι : Type*} [Fintype ι] [Nonempty ι]
    (τ : FaithfulTracialState B) (A : StarSubalgebra ℂ B)
    (E : B →L[ℂ] B) (hE : ∀ x, E x ∈ A)
    (hpair : ∀ b ∈ A, ∀ x, τ.toLinearMap (b * E x) = τ.toLinearMap (b * x))
    (p : ι → B) (u : ι → unitary B)
    (hp : ∀ i, IsStarProjection (p i)) (hpA : ∀ i, p i ∈ A)
    (hfree : ∀ i, FreeHaarMoments τ A (u i)) {t : ℂ}
    (hptrace : ∀ i, τ.toLinearMap (p i) = t) (ht0 : t ≠ 0) (ht1 : t ≠ 1)
    (hpavg : finiteAverage p = t • (1 : B))
    {n : ℕ} (hn : 0 < n) (N : ℕ) (i₀ : ι) :
    finiteAverage (fun i => E (recoveryObservable n N (p i) (u i))) =
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.finiteAverage, OAI.KadisonKastler.recoveryObservable

theorem OAI.KadisonKastler.expectation_finiteAverage_recoveryObservable line 112