OAI/Combinatorics/EditApproximation/Refinement/ComputedPreevaluation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.guard_scalar line 10
2. theorem OAI.EditApproximation.physicalLargeInputWithWork_le_height line 22
3. theorem OAI.EditApproximation.setup_scalar line 33

   Source documentation

   All input scans, index construction, parameter arithmetic and the bounded accuracy/word-cap decision occur before sampling.

   private theorem setup_scalar (N H a b c : ℕ) (hH : 1000000 ≤ H)
       (ha : a ≤ (N + 2) * H ^ 4) (hb : b ≤ 2000 * (H + 1)) (hc : c ≤ H ^ 4) :
       a + b + c ≤ (N + 2) * H ^ 5 := by
   …

4. theorem OAI.EditApproximation.integerPreevaluationWork_near_linear line 46