OAI/Algebra/Determinantal/AmbientNumerical.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PermanentBorder.Polar.ambient_count_numerical_bound line 9

   Source documentation

   The binomial count implies a numerical lower bound for the matrix size. No positivity assumption on D or n is needed.

   theorem ambient_count_numerical_bound (n K D : ℕ)
       (hcount : D ≤ 2 ^ K * (2 * n - 1).choose (K + 1)) :
       ((K + 1 : ℕ) : ℝ) / (4 * Real.exp 1) *
         Real.rpow (D : ℝ) (1 / ((K + 1 : ℕ) : ℝ)) ≤ (n : ℝ) := by
   …