OAI/Combinatorics/EditApproximation/Queries/QueryProgramPolynomial.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.queryPrimitiveBitDegree line 10
2. def OAI.EditApproximation.queryLocalProgramBitDegree line 14
3. theorem OAI.EditApproximation.queryLocalProgramBitBudget_shell_cap line 16
4. theorem OAI.EditApproximation.queryLocalProgramBitBudget_uniform_cap line 64

   Source documentation

   A uniform cap absorbs the finite counts before applying the cost polynomial.

   theorem queryLocalProgramBitBudget_uniform_cap (M N P F exponent eM eF B S t W X : ℕ)
       (hX : 64 ≤ X) (hN : Nat.size N ≤ B)
       (hM : M ≤ X) (hP : P ≤ X) (hF : F ≤ X) (he : exponent ≤ X)
       (heM : eM ≤ X) (heF : eF ≤ X) (hB : B ≤ X) (hS : S ≤ X) (ht : t ≤ X) (hW : W ≤ X)
       (hTheta : 2 ^ exponent ≤ X) (hV : (40 * P + 2) ^ (2 * M) ≤ X)
       (hCart : ((40 * P + 2) ^ 2 + 1) ^ (M + 1) ≤ X) :
       BinaryFraction.queryLocalProgramBitBudget M N P F exponent eM eF B S t W ≤
         X ^ (16 * queryLocalProgramBitDegree) := by
   …

   Mentions: OAI.EditApproximation.BinaryFraction.queryLocalProgramBitBudget, OAI.EditApproximation.queryLocalProgramBitDegree