OAI/Combinatorics/EditApproximation/Coarse/CoarseWorkAsymptotics.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The depth-dependent scalar overhead of the actual initial estimator. The expected array-counter bound includes every pruning outcome.

  1. def OAI.EditApproximation.computedMaxCoarseDepth line 15
  2. theorem OAI.EditApproximation.computedCoarseDepth_le_max line 17
  3. theorem OAI.EditApproximation.coarse_depth_mul_exponent_bound line 22
  4. theorem OAI.EditApproximation.scalar_coarse_depth_log_bound line 40
  5. theorem OAI.EditApproximation.coarse_depth_log_height_div_height_tendsto line 55
  6. def OAI.EditApproximation.computedCoarseOverheadExponent line 84
  7. theorem OAI.EditApproximation.computedCoarseOverheadExponent_tendsto line 88
  8. theorem OAI.EditApproximation.coarse_branching_log_div_height_tendsto line 98
  9. theorem OAI.EditApproximation.coarse_inverse_allowance_le_height_eight_eventually line 113

    Source documentation

    The literal coarse threshold law has the paper's H^8 inverse-allowance factor, for all sufficiently large inputs and without any accuracy event.

    theorem coarse_inverse_allowance_le_height_eight_eventually :
    ∀ᶠ N in atTop, coarseInverseAllowanceFactor (integerParameters N).B
      (initialThresholdQ N) (initialLambda N) ≤ (inputHeight N : ℝ) ^ 8 := by
…

    Mentions: OAI.EditApproximation.coarseInverseAllowanceFactor, OAI.EditApproximation.integerParameters, OAI.EditApproximation.initialThresholdQ, OAI.EditApproximation.initialLambda, OAI.EditApproximation.inputHeight