ScalarRecovery.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Combining the tracial estimates for the recovered scalar

theorem OAI.KadisonKastler.traceOneNorm_le_sub_add line 20
Source documentation
Reverse triangle inequality in the form needed to restore a spectral compression.
```
theorem traceOneNorm_le_sub_add (τ : FaithfulTracialState B) (x y : B) :
    traceOneNorm τ x ≤ traceOneNorm τ (x - y) + traceOneNorm τ y := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceOneNorm
theorem OAI.KadisonKastler.compression_square_tail_factor line 26
Source documentation
The complement of a commuting spectral projection factors the tail of the compressed square into the two factors used by Hölder.
```
theorem compression_square_tail_factor (p f e : B)
    (he : IsStarProjection e) (hfe : Commute f e) :
    recoveryCompression p f - p * e * (f * f) * e * p =
      (p * f * (1 - e)) * ((1 - e) * f * p) := by
…
```
Mentions: OAI.KadisonKastler.recoveryCompression
theorem OAI.KadisonKastler.compression_square_tail_one_le line 51
Source documentation
The two-norm tail estimate supplies the one-norm tail of the compressed square.
```
theorem compression_square_tail_one_le (τ : FaithfulTracialState B)
    (p f e : B) (he : IsStarProjection e) (hfe : Commute f e) :
    traceOneNorm τ (recoveryCompression p f - p * e * (f * f) * e * p) ≤
      traceTwoNorm τ (p * f * (1 - e)) * traceTwoNorm τ ((1 - e) * f * p) := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceOneNorm, OAI.KadisonKastler.recoveryCompression, OAI.KadisonKastler.traceTwoNorm

theorem OAI.KadisonKastler.recovery_scalar_lower_from_compression line 61

Source documentation

All analytic losses in scalar recovery are now explicit: the tail occurs twice, and the square-root compression contributes its variance error. The recovered scalar uses the actual continuous contraction.

theorem recovery_scalar_lower_from_compression
    (τ : FaithfulTracialState B) {n : ℕ} (hn : 0 < n)
    (p f e : B) (hp : IsStarProjection p) (he : IsStarProjection e)
    {η N tail : ℝ}
    (hpτ : τ.toLinearMap p = (((n : ℝ)⁻¹ : ℝ) : ℂ))
    (heτ : τ.toLinearMap e = (η : ℂ))
    (hmom : CenteredProjectionMoments τ p e (n : ℝ)⁻¹ η)
    (hf : ‖f * f‖ ≤ N)
    (htail : (n : ℝ) * traceOneNorm τ
      (recoveryCompression p f - p * e * (f * f) * e * p) ≤ tail)
    (hmass : 1 - tail ≤ traceOneNorm τ (e * (f * f) * e))
    (hpolar : (n : ℝ) * traceOneNorm τ (p * e * (f * f) * e * p) =
…

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

theorem OAI.KadisonKastler.recovery_scalar_at_least_half line 104

Source documentation

With the manuscript's explicit choice of the power count, the constructed contraction recovers a scalar at least one half.

theorem recovery_scalar_at_least_half
    (τ : FaithfulTracialState B) {n N : ℕ} (hn : 0 < n)
    (hsize : 100 * (n : ℝ) * (100 * Real.pi) ^ 3 ≤ N)
    (p f e : B) (hp : IsStarProjection p) (he : IsStarProjection e)
    (hpτ : τ.toLinearMap p = (((n : ℝ)⁻¹ : ℝ) : ℂ))
    (heτ : τ.toLinearMap e = ((100 / (N : ℝ) : ℝ) : ℂ))
    (hmom : CenteredProjectionMoments τ p e (n : ℝ)⁻¹ (100 / N))
    (hf : ‖f * f‖ ≤ N)
    (htail : (n : ℝ) * traceOneNorm τ
      (recoveryCompression p f - p * e * (f * f) * e * p) ≤
        Real.pi / (100 * Real.pi))
    (hmass : 1 - Real.pi / (100 * Real.pi) ≤ traceOneNorm τ (e * (f * f) * e))
…

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