OAI/Combinatorics/EditApproximation/Coarse/CoarseInitialScalar.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.BinaryFraction.coarseInitial_aggregate_scalar line 9

   Source documentation

   Scalar envelope used only after summing the executed dyadic roots.

   theorem coarseInitial_aggregate_scalar (H x a g roots work : ℕ) (hH : 100 ≤ H)
       (hg : g ≤ H + 1)
       (hr : roots ≤ H ^ 32 * (a + g))
       (hw : work ≤ roots + (3 * x + 1) * (8 * H ^ 3 + 4) +
         10000 * (g + 1) * (H ^ 4 + 2) ^ 2) :
       work ≤ H ^ 36 * (a + x + 1) := by
   …