FreeProjectionMoments.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Two free-projection moments for scalar recovery

Only the degree-two and alternating degree-four centered moments are used. The identities below are proved from these explicit algebraic hypotheses; no free-probability theorem is assumed here.

structure OAI.KadisonKastler.CenteredProjectionMoments line 22
Source documentation
The two centered mixed moments needed for the compressed projection.
```
structure CenteredProjectionMoments (τ : FaithfulTracialState B) (p e : B)
    (t η : ℝ) : Prop where
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState
theorem OAI.KadisonKastler.centered_projection_square line 28
theorem OAI.KadisonKastler.expand_centered_sandwich line 35
theorem OAI.KadisonKastler.trace_sandwich_square line 42

theorem OAI.KadisonKastler.CenteredProjectionMoments.trace_compression line 56

Source documentation

The first mixed moment makes the trace of a compression the product of the projection traces.

theorem CenteredProjectionMoments.trace_compression
    {τ : FaithfulTracialState B} {p e : B} {t η : ℝ}
    (h : CenteredProjectionMoments τ p e t η)
    (he : e * e = e) (hpτ : τ.toLinearMap p = (t : ℂ))
    (heτ : τ.toLinearMap e = (η : ℂ)) :
    τ.toLinearMap (e * p * e) = ((t * η : ℝ) : ℂ) := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.CenteredProjectionMoments

theorem OAI.KadisonKastler.CenteredProjectionMoments.trace_centered_compression line 74

Source documentation

The alternating fourth moment determines the centered compressed second moment before any normalization by the corner trace.

theorem CenteredProjectionMoments.trace_centered_compression
    {τ : FaithfulTracialState B} {p e : B} {t η : ℝ}
    (h : CenteredProjectionMoments τ p e t η)
    (hp : p * p = p) (hpτ : τ.toLinearMap p = (t : ℂ))
    (heτ : τ.toLinearMap e = (η : ℂ)) :
    τ.toLinearMap ((p - (t : ℂ) • 1) * e * (p - (t : ℂ) • 1) * e) =
      (η : ℂ) ^ 2 * ((t : ℂ) - (t : ℂ) ^ 2) := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.CenteredProjectionMoments

theorem OAI.KadisonKastler.CenteredProjectionMoments.trace_scaled_compression line 105

Source documentation

The normalized positive compression has the same trace as e.

theorem CenteredProjectionMoments.trace_scaled_compression
    {τ : FaithfulTracialState B} {p e : B} {n : ℕ} {η : ℝ}
    (hn : 0 < n) (he : IsStarProjection e)
    (hpτ : τ.toLinearMap p = (((n : ℝ)⁻¹ : ℝ) : ℂ))
    (heτ : τ.toLinearMap e = (η : ℂ))
    (h : CenteredProjectionMoments τ p e (n : ℝ)⁻¹ η) :
    τ.toLinearMap ((n : ℂ) • (e * p * e)) = (η : ℂ) := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.CenteredProjectionMoments

theorem OAI.KadisonKastler.CenteredProjectionMoments.trace_scaled_compression_sub_sq line 120

Source documentation

With trace 1/n, the scaled compression has the exact variance (n-1)η². This is the scalar identity used in the recovery estimate.

theorem CenteredProjectionMoments.trace_scaled_compression_sub_sq
    {τ : FaithfulTracialState B} {p e : B} {n : ℕ} {η : ℝ}
    (hn : 0 < n) (hp : IsStarProjection p) (he : IsStarProjection e)
    (hpτ : τ.toLinearMap p = (((n : ℝ)⁻¹ : ℝ) : ℂ))
    (heτ : τ.toLinearMap e = (η : ℂ))
    (h : CenteredProjectionMoments τ p e (n : ℝ)⁻¹ η) :
    τ.toLinearMap (((n : ℂ) • (e * p * e) - e) ^ 2) =
      (((n : ℝ) - 1) * η ^ 2 : ℝ) := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.CenteredProjectionMoments

theorem OAI.KadisonKastler.CenteredProjectionMoments.traceTwoNorm_scaled_compression_sub_sq line 146

Source documentation

The preceding complex identity is the square of the tracial two-norm, because the scaled compression is selfadjoint.

theorem CenteredProjectionMoments.traceTwoNorm_scaled_compression_sub_sq
    {τ : FaithfulTracialState B} {p e : B} {n : ℕ} {η : ℝ}
    (hn : 0 < n) (hp : IsStarProjection p) (he : IsStarProjection e)
    (hpτ : τ.toLinearMap p = (((n : ℝ)⁻¹ : ℝ) : ℂ))
    (heτ : τ.toLinearMap e = (η : ℂ))
    (h : CenteredProjectionMoments τ p e (n : ℝ)⁻¹ η) :
    traceTwoNorm τ ((n : ℂ) • (e * p * e) - e) ^ 2 =
      ((n : ℝ) - 1) * η ^ 2 := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.CenteredProjectionMoments, OAI.KadisonKastler.traceTwoNorm