ComputedCoarseCandidateWork.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.EditApproximation.BinaryFraction.coarseGuess_le line 12
theorem OAI.EditApproximation.BinaryFraction.coarseCandidate_scalar line 23
theorem OAI.EditApproximation.BinaryFraction.computedCoarseRoot_for_candidate line 46
theorem OAI.EditApproximation.BinaryFraction.coarseCandidate_k_bits line 95

theorem OAI.EditApproximation.BinaryFraction.computedCoarseCandidate_bounds line 108

Source documentation

Every executed dyadic candidate has a short binary value and its complete arithmetic cost is bounded by a fixed height power times its active-array work.

theorem computedCoarseCandidate_bounds :
    ∀ᶠ N : ℕ in atTop, ∀ B d : ℕ, ∀ x y : List ℕ,
      B = (integerParameters N).B → d = computedCoarseDepth N (coarseEntryWidth x y) →
      coarseEntryWidth x y ≤ N → ∀ (hB : 0 < B) (hq : 0 < inputHeight N ^ 4)
      (hL : 0 < 64 * inputHeight N)
      (i : CoarseGuessIndex (coarseEntryWidth x y)) (draws : CoarseThresholdDraws B d),
      (coarseCandidateWithWork (inputHeight N ^ 4) (64 * inputHeight N) hB hq hL x y i draws).1.width ≤
        inputHeight N ^ 4 ∧
      (coarseCandidateWithWork (inputHeight N ^ 4) (64 * inputHeight N) hB hq hL x y i draws).2 ≤
        inputHeight N ^ 32 * (coarseActiveArrayWork (coarseGuess (coarseEntryWidth x y) i)
          (initialThresholdQ N) (initialLambda N) (coarseEntryTree B d x y) draws
          (coarseGuess (coarseEntryWidth x y) i) + 1) := by
…