TraceCompressionPolar.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Trace-one compression identities from explicit polar data

theorem OAI.KadisonKastler.traceOneNorm_smul_nonneg line 19
Source documentation
Positive real homogeneity of the tracial one-norm.
```
theorem traceOneNorm_smul_nonneg (τ : FaithfulTracialState B) {r : ℝ} (hr : 0 ≤ r)
    (x : B) : traceOneNorm τ (r • x) = r * traceOneNorm τ x := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceOneNorm
theorem OAI.KadisonKastler.traceOneNorm_nat_smul line 26
Source documentation
Natural scalar homogeneity, stated with complex algebra scalars.
```
theorem traceOneNorm_nat_smul (τ : FaithfulTracialState B) (n : ℕ) (x : B) :
    traceOneNorm τ ((n : ℂ) • x) = (n : ℝ) * traceOneNorm τ x := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceOneNorm
theorem OAI.KadisonKastler.traceOneNorm_neg line 32

theorem OAI.KadisonKastler.traceOneNorm_selfAdjoint_polar_compression line 38

Source documentation

The algebraic polar compression identity. Only the displayed factorization and final-projection support are used.

theorem traceOneNorm_selfAdjoint_polar_compression (τ : FaithfulTracialState B)
    (x b a w : B) (hb : IsSelfAdjoint b) (hx : x = b * w)
    (hw : IsStarProjection (w * star w))
    (hL : (w * star w) * b = b) (hR : b * (w * star w) = b) :
    traceOneNorm τ (star x * a * x) = traceOneNorm τ (b * a * b) := by
…

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

theorem OAI.KadisonKastler.traceOneNorm_polar_compression line 61

Source documentation

The compression identity for the positive part of a polar factorization.

theorem traceOneNorm_polar_compression (τ : FaithfulTracialState B)
    (x a w : B) (hx : x = CFC.sqrt (x * star x) * w)
    (hw : IsStarProjection (w * star w))
    (hL : (w * star w) * CFC.sqrt (x * star x) = CFC.sqrt (x * star x))
    (hR : CFC.sqrt (x * star x) * (w * star w) = CFC.sqrt (x * star x)) :
    traceOneNorm τ (star x * a * x) =
      traceOneNorm τ (CFC.sqrt (x * star x) * a * CFC.sqrt (x * star x)) :=
…

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

theorem OAI.KadisonKastler.scaled_projection_product_mul_star line 73

Source documentation

The positive square of the scaled projection product is the normalized compression.

theorem scaled_projection_product_mul_star (n : ℕ) (p e : B)
    (hp : IsStarProjection p) (he : IsStarProjection e) :
    ((Real.sqrt (n : ℝ)) • (e * p)) * star ((Real.sqrt (n : ℝ)) • (e * p)) =
      (n : ℂ) • (e * p * e) := by
…

theorem OAI.KadisonKastler.traceOneNorm_scaled_projection_compression line 91

Source documentation

Compression by sqrt n • ep, in the exact form needed in scalar recovery. The hypotheses describe the polar factor, not its existence.

theorem traceOneNorm_scaled_projection_compression (τ : FaithfulTracialState B)
    (n : ℕ) (p e a w : B) (hp : IsStarProjection p) (he : IsStarProjection e)
    (hx : (Real.sqrt (n : ℝ)) • (e * p) = CFC.sqrt ((n : ℂ) • (e * p * e)) * w)
    (hw : IsStarProjection (w * star w))
    (hL : (w * star w) * CFC.sqrt ((n : ℂ) • (e * p * e)) =
      CFC.sqrt ((n : ℂ) • (e * p * e)))
    (hR : CFC.sqrt ((n : ℂ) • (e * p * e)) * (w * star w) =
      CFC.sqrt ((n : ℂ) • (e * p * e))) :
    (n : ℝ) * traceOneNorm τ (p * e * a * e * p) =
      traceOneNorm τ (CFC.sqrt ((n : ℂ) • (e * p * e)) * a *
        CFC.sqrt ((n : ℂ) • (e * p * e))) := by
…

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