ComputedCoarseWidthCost.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The actual coarse array counter has a common source-width overhead. Its exponent is sublinear in the computed logarithmic height.

def OAI.EditApproximation.computedCoarseWidthOverhead line 13
theorem OAI.EditApproximation.coarse_width_overhead_le_power line 17
theorem OAI.EditApproximation.computedCoarseWidthOverhead_le line 35
theorem OAI.EditApproximation.computedCoarseWidthOverhead_exp_le line 47
theorem OAI.EditApproximation.coarse_array_bound_mono line 60

theorem OAI.EditApproximation.computed_coarse_expected_source_width line 74

Source documentation

The common overhead dominates the actual expected coarse array work at every source/target interval, including the direct long-target branch.

theorem computed_coarse_expected_source_width {α : Type*} [DecidableEq α]
    (N B : ℕ) [NeZero B] [MeasurableSpace (Fin B)] [MeasurableSingletonClass (Fin B)]
    (hB : B = (integerParameters N).B) (hN : 0 < N) (hell : 200 ≤ inputSmallLog N)
    (hinverse : coarseInverseAllowanceFactor B (initialThresholdQ N) (initialLambda N) ≤
      (inputHeight N : ℝ) ^ 8)
    (x y : List α) (D : ℕ) (hDcomputed : D = computedCoarseDepth N (coarseEntryWidth x y))
    (hsize : coarseEntryWidth x y ≤ N) :
    (∫ draw, (coarseInitialArrayWork B D
      (initialThresholdQ N) (initialLambda N) x y draw : ℝ)
      ∂coarseInitialMeasure B D (coarseEntryWidth x y)) ≤
      (x.length : ℝ) * computedCoarseWidthOverhead N := by
…

Mentions: OAI.EditApproximation.integerParameters, OAI.EditApproximation.inputSmallLog, OAI.EditApproximation.coarseInverseAllowanceFactor, OAI.EditApproximation.initialThresholdQ, OAI.EditApproximation.initialLambda, OAI.EditApproximation.inputHeight, OAI.EditApproximation.computedCoarseDepth, OAI.EditApproximation.coarseEntryWidth, OAI.EditApproximation.coarseInitialArrayWork, OAI.EditApproximation.coarseInitialMeasure, OAI.EditApproximation.computedCoarseWidthOverhead