SquareRootCompression.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Square roots in projection corners and the compression error

theorem OAI.KadisonKastler.sqrt_scalar_sub_one_sq_le line 19

theorem OAI.KadisonKastler.sqrt_projection_support line 32

Source documentation

A square root has the same two-sided projection support as the positive element.

theorem sqrt_projection_support (s e : B) (hs : 0 ≤ s) (he : IsStarProjection e)
    (hse : s * e = s) :
    CFC.sqrt s * e = CFC.sqrt s ∧ e * CFC.sqrt s = CFC.sqrt s := by
…

theorem OAI.KadisonKastler.traceTwoNorm_sqrt line 51
Source documentation
The tracial two-norm of a positive square root.
```
theorem traceTwoNorm_sqrt (τ : FaithfulTracialState B) (s : B) (hs : 0 ≤ s) :
    traceTwoNorm τ (CFC.sqrt s) = Real.sqrt ((τ.toLinearMap s).re) := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm
theorem OAI.KadisonKastler.traceTwoNorm_projection line 57
Source documentation
The tracial two-norm of a projection.
```
theorem traceTwoNorm_projection (τ : FaithfulTracialState B) (e : B)
    (he : IsStarProjection e) :
    traceTwoNorm τ e = Real.sqrt ((τ.toLinearMap e).re) := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm
theorem OAI.KadisonKastler.traceTwoNorm_sqrt_sub_projection_le line 64
Source documentation
Taking the positive square root improves the distance to the identity of the supporting projection corner.
```
theorem traceTwoNorm_sqrt_sub_projection_le (τ : FaithfulTracialState B)
    (s e : B) (hs : 0 ≤ s) (he : IsStarProjection e) (hse : s * e = s) :
    traceTwoNorm τ (CFC.sqrt s - e) ≤ traceTwoNorm τ (s - e) := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm

theorem OAI.KadisonKastler.CenteredProjectionMoments.sqrt_compression_sandwich_error line 110

Source documentation

The actual square-root compression error in the scalar recovery argument, from the two low-degree free moments.

theorem CenteredProjectionMoments.sqrt_compression_sandwich_error
    {τ : FaithfulTracialState B} {p e a : B} {n : ℕ} {η N : ℝ}
    (hn : 0 < n) (hp : IsStarProjection p) (he : IsStarProjection e)
    (hpτ : τ.toLinearMap p = (((n : ℝ)⁻¹ : ℝ) : ℂ))
    (heτ : τ.toLinearMap e = (η : ℂ))
    (h : CenteredProjectionMoments τ p e (n : ℝ)⁻¹ η) (hN : ‖a‖ ≤ N) :
    traceOneNorm τ (CFC.sqrt ((n : ℂ) • (e * p * e)) * a *
        CFC.sqrt ((n : ℂ) • (e * p * e)) - e * a * e) ≤
      2 * N * Real.sqrt ((n : ℝ) - 1) * η * Real.sqrt η := by
…

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