OAI/Analysis/KadisonKastler/RecoveryParameters.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Choosing the finite degrees before the recovery randomization

  1. theorem OAI.KadisonKastler.exists_recovery_degrees line 11

    Source documentation

    The polynomial degree meets the scalar-recovery bound, and the finite phase order exceeds twice that degree, as required by the word expansions.

    theorem exists_recovery_degrees (n : ℕ) :
    ∃ N q : ℕ, 0 < N ∧ 2 * N < q ∧
      100 * (n : ℝ) * (100 * Real.pi) ^ 3 ≤ N := by
…