RecoveryContraction.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

An explicit corner contraction for scalar recovery

def OAI.KadisonKastler.recoveryCutoff line 19
Source documentation
The cutoff whose scaled trace loss is exactly one tenth.
```
def recoveryCutoff (n : ℕ) : ℝ := (10 * (n : ℝ))⁻¹
```
def OAI.KadisonKastler.recoveryCompression line 22
Source documentation
The compressed square used by the scalar recovery argument.
```
def recoveryCompression (p f : B) : B := p * f * f * p
```
def OAI.KadisonKastler.recoveryContraction line 26
Source documentation
A concrete contraction obtained from the adjoint of the clipped polar approximation inside the projection corner.
```
def recoveryContraction (n : ℕ) (p f : B) : B :=
…
```
theorem OAI.KadisonKastler.recoveryCutoff_pos line 29
theorem OAI.KadisonKastler.recoveryCutoff_mul line 33
theorem OAI.KadisonKastler.recoveryContraction_norm_le line 40
Source documentation
The formula has norm at most one.
```
theorem recoveryContraction_norm_le {n : ℕ} (hn : 0 < n) (p f : B) :
    ‖recoveryContraction n p f‖ ≤ 1 := by
…
```
Mentions: OAI.KadisonKastler.recoveryContraction
theorem OAI.KadisonKastler.recoveryContraction_support line 50
Source documentation
The contraction belongs algebraically to the original projection corner, without any approximation in the support identities.
```
theorem recoveryContraction_support {n : ℕ} (hn : 0 < n)
    (p f : B) (hp : IsStarProjection p) :
    p * recoveryContraction n p f = recoveryContraction n p f ∧
      recoveryContraction n p f * p = recoveryContraction n p f := by
…
```
Mentions: OAI.KadisonKastler.recoveryContraction
theorem OAI.KadisonKastler.trace_corner_recovery line 76
theorem OAI.KadisonKastler.spectralClip_continuous line 90
Source documentation
Fixed positive cutoffs depend continuously on the input element.
```
theorem spectralClip_continuous {ε : ℝ} (hε : 0 < ε) :
    Continuous (fun x : B => spectralClip ε x) := by
…
```
Mentions: OAI.KadisonKastler.spectralClip
theorem OAI.KadisonKastler.recoveryContraction_continuous line 100
Source documentation
For each fixed corner dimension, the recovery contraction is a continuous function of the Fourier-polynomial element.
```
theorem recoveryContraction_continuous {n : ℕ} (hn : 0 < n) (p : B) :
    Continuous (recoveryContraction n p) := by
…
```
Mentions: OAI.KadisonKastler.recoveryContraction
theorem OAI.KadisonKastler.recoveryContraction_trace_lower_bound line 109
Source documentation
The continuous cutoff recovers the compressed one-norm with loss at most 1/10 after scaling by the corner dimension.
```
theorem recoveryContraction_trace_lower_bound (τ : FaithfulTracialState B)
    {n : ℕ} (hn : 0 < n) (p f : B) (hp : IsStarProjection p) :
    (n : ℝ) * traceOneNorm τ (recoveryCompression p f) - 1 / 10 ≤
      (τ.toLinearMap ((n : ℂ) • (f * recoveryContraction n p f * f))).re := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceOneNorm, OAI.KadisonKastler.recoveryCompression, OAI.KadisonKastler.recoveryContraction