OAI/Analysis/Unitarizability/FrameParameters.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Ceiling dimensions and finite union-bound arithmetic for frames.

  1. def OAI.Dixmier.FrameParameters.dimension line 11
  2. def OAI.Dixmier.FrameParameters.subfamilySize line 12
  3. theorem OAI.Dixmier.FrameParameters.bounds line 14
  4. theorem OAI.Dixmier.FrameParameters.failure_bound_lt_one line 40

    Source documentation

    The frame failure probability is strictly below one.

    theorem failure_bound_lt_one {n k p : ℕ} (hn : 2 ≤ n) (hk : 1 ≤ k)
    (hp : p ≤ k) (hplog : (p : ℝ) * Real.log n ≤ k) :
    2 * (n : ℝ)^p * 9^(k+p) * Real.exp (-25*(k : ℝ)/2) < 1 := by
…
  5. theorem OAI.Dixmier.FrameParameters.exact_failure_bound line 70