Approximate-count selection -- proof internals #
theorem
Complexity.AntiChecker.exists_isEstimateMinimizer_internal
{arity : ℕ}
(estimate : BitString arity → ℕ)
:
∃ (chosen : BitString arity), IsEstimateMinimizer estimate chosen
theorem
Complexity.AntiChecker.IsEstimateMinimizer.candidateSurvivorCount_le_scaled_internal
{arity precision threshold : ℕ}
{target : BitString arity → Bool}
{inputs : List (BitString arity)}
{estimate : BitString arity → ℕ}
{chosen other : BitString arity}
(happrox : ApproximatesAllExtensions precision target threshold inputs estimate)
(hminimum : IsEstimateMinimizer estimate chosen)
:
(precision - 1) * candidateSurvivorCount target threshold (chosen :: inputs) ≤ (precision + 1) * candidateSurvivorCount target threshold (other :: inputs)
theorem
Complexity.AntiChecker.IsEstimateMinimizer.scaledShrink_of_hasShrinkExtension_internal
{arity precision denominator threshold : ℕ}
{target : BitString arity → Bool}
{inputs : List (BitString arity)}
{estimate : BitString arity → ℕ}
{chosen : BitString arity}
(happrox : ApproximatesAllExtensions precision target threshold inputs estimate)
(hminimum : IsEstimateMinimizer estimate chosen)
(hgood : HasShrinkExtension denominator target threshold inputs)
:
theorem
Complexity.AntiChecker.IsEstimateMinimizer.isShrinkExtension_double_internal
{arity precision denominator threshold : ℕ}
{target : BitString arity → Bool}
{inputs : List (BitString arity)}
{estimate : BitString arity → ℕ}
{chosen : BitString arity}
(hprecision : 1 < precision)
(hdenominator : 0 < denominator)
(hbound : 4 * denominator ≤ precision + 3)
(happrox : ApproximatesAllExtensions precision target threshold inputs estimate)
(hminimum : IsEstimateMinimizer estimate chosen)
(hgood : HasShrinkExtension denominator target threshold inputs)
:
IsShrinkExtension (2 * denominator) target threshold inputs chosen