SpectralRecovery.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Turning scalar spectral tails into compressed recovery estimates

def OAI.KadisonKastler.ProjectionTraceIndependent line 17
Source documentation
The degree-two consequence of freeness used for the tail estimate.
```
def ProjectionTraceIndependent (τ : FaithfulTracialState B) (p : B)
    (A : StarSubalgebra ℂ B) : Prop :=
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState
theorem OAI.KadisonKastler.traceTwoNorm_projection_left_sq line 21
theorem OAI.KadisonKastler.traceTwoNorm_projection_right_sq line 36

theorem OAI.KadisonKastler.spectral_tail_factor_norms line 53

Source documentation

The left and right factors in the tail Hölder estimate have the same squared two-norm, equal to the scalar tail divided by the matrix size.

theorem spectral_tail_factor_norms (τ : FaithfulTracialState B)
    {A : StarSubalgebra ℂ B} {p f e : B} {n : ℕ}
    (hp : IsStarProjection p) (he : IsStarProjection e)
    (hf : f ∈ A) (heA : e ∈ A) (hfe : Commute f e)
    (hpτ : τ.toLinearMap p = (((n : ℝ)⁻¹ : ℝ) : ℂ))
    (hind : ProjectionTraceIndependent τ p A) :
    traceTwoNorm τ (p * f * (1 - e)) ^ 2 =
        (n : ℝ)⁻¹ * (τ.toLinearMap (star f * f * (1 - e))).re ∧
    traceTwoNorm τ ((1 - e) * f * p) ^ 2 =
        (n : ℝ)⁻¹ * (τ.toLinearMap (star f * f * (1 - e))).re := by
…

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

theorem OAI.KadisonKastler.compressed_spectral_tail_le line 98

Source documentation

Freeness removes the factor n from the one-norm tail of the compressed square. Only the scalar Haar tail remains.

theorem compressed_spectral_tail_le (τ : FaithfulTracialState B)
    {A : StarSubalgebra ℂ B} {p f e : B} {n : ℕ} (hn : 0 < n)
    (hp : IsStarProjection p) (he : IsStarProjection e)
    (hf : f ∈ A) (heA : e ∈ A) (hfe : Commute f e)
    (hpτ : τ.toLinearMap p = (((n : ℝ)⁻¹ : ℝ) : ℂ))
    (hind : ProjectionTraceIndependent τ p A) :
    (n : ℝ) * traceOneNorm τ
      (recoveryCompression p f - p * e * (f * f) * e * p) ≤
        (τ.toLinearMap (star f * f * (1 - e))).re := by
…

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

theorem OAI.KadisonKastler.normal_compressed_square_mass line 122
Source documentation
For a normal polynomial the absolute value of its compressed square is precisely the compressed energy.
```
theorem normal_compressed_square_mass (τ : FaithfulTracialState B)
    {f e : B} (hf : IsStarNormal f) (he : IsStarProjection e) (hfe : Commute f e) :
    traceOneNorm τ (e * (f * f) * e) = (τ.toLinearMap (star f * f * e)).re := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceOneNorm

theorem OAI.KadisonKastler.normal_compressed_square_mass_lower line 138

Source documentation

Unit total energy and a scalar tail bound give the mass hypothesis in scalar recovery, without another analytic estimate.

theorem normal_compressed_square_mass_lower (τ : FaithfulTracialState B)
    {f e : B} {tail : ℝ} (hf : IsStarNormal f) (he : IsStarProjection e)
    (hfe : Commute f e) (hunit : τ.toLinearMap (star f * f) = 1)
    (htail : (τ.toLinearMap (star f * f * (1 - e))).re ≤ tail) :
    1 - tail ≤ traceOneNorm τ (e * (f * f) * e) := by
…

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