OAI/Analysis/KadisonKastler/ScalarRecoveryBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.recovery_compression_error_le line 14

   Source documentation

   The cubic-root error estimate is expressed using only square roots, as in the tracial Cauchy–Schwarz calculation.

   theorem recovery_compression_error_le {n N η : ℝ}
       (hn : 0 ≤ n) (hN : 0 < N) (hη : 0 ≤ η) (hNη : N * η = 100)
       (hsize : 100000000 * n ≤ N) :
       2 * N * Real.sqrt n * η * Real.sqrt η ≤ 1 / 5 := by
   …

2. theorem OAI.KadisonKastler.recovered_scalar_lower_bound line 33

   Source documentation

   The manuscript's choice N ≥ 100 n (100π)^3 makes the recovered scalar uniformly larger than one half.

   theorem recovered_scalar_lower_bound {n N : ℕ} (hn : 1 ≤ n)
       (hsize : 100 * (n : ℝ) * (100 * Real.pi) ^ 3 ≤ N)
       {c : ℝ}
       (hc : 9 / 10 - 2 * Real.pi / (100 * Real.pi) -
         2 * N * Real.sqrt ((n : ℝ) - 1) * (100 / N) * Real.sqrt (100 / N) ≤ c) :
       1 / 2 ≤ c := by
   …