Documentation

Complexitylib.Metacomplexity.MCSP.AntiChecker.Approximation.Internal

Relative survivor-count approximation -- proof internals #

source
theorem Complexity.AntiChecker.isRelativeApproximation_exact_internal {precision actual : ℕ} (hprecision : 0 < precision) :
IsRelativeApproximation precision actual actual
source
theorem Complexity.AntiChecker.IsRelativeApproximation.estimate_eq_zero_of_actual_eq_zero_internal {precision actual estimate : ℕ} (happrox : IsRelativeApproximation precision actual estimate) (hactual : actual = 0) :
estimate = 0
source
theorem Complexity.AntiChecker.IsRelativeApproximation.actual_eq_zero_of_estimate_eq_zero_internal {precision actual estimate : ℕ} (hprecision : 1 < precision) (happrox : IsRelativeApproximation precision actual estimate) (hestimate : estimate = 0) :
actual = 0
source
theorem Complexity.AntiChecker.IsRelativeApproximation.estimate_eq_zero_iff_actual_eq_zero_internal {precision actual estimate : ℕ} (hprecision : 1 < precision) (happrox : IsRelativeApproximation precision actual estimate) :
estimate = 0 ↔ actual = 0
source
theorem Complexity.AntiChecker.IsRelativeApproximation.actual_le_scaled_of_estimate_le_internal {precision firstActual firstEstimate secondActual secondEstimate : ℕ} (hfirst : IsRelativeApproximation precision firstActual firstEstimate) (hsecond : IsRelativeApproximation precision secondActual secondEstimate) (hestimate : firstEstimate ≤ secondEstimate) :
(precision - 1) * firstActual ≤ (precision + 1) * secondActual
source
theorem Complexity.AntiChecker.approximatesCandidateSurvivorCount_exact_internal {arity precision threshold : ℕ} (hprecision : 0 < precision) (target : BitString arity → Bool) (inputs : List (BitString arity)) :
ApproximatesCandidateSurvivorCount precision target threshold inputs (candidateSurvivorCount target threshold inputs)
source
theorem Complexity.AntiChecker.estimate_eq_zero_iff_isFor_internal {arity precision threshold estimate : ℕ} [NeZero arity] (hprecision : 1 < precision) (target : BitString arity → Bool) (inputs : List (BitString arity)) (happrox : ApproximatesCandidateSurvivorCount precision target threshold inputs estimate) :
estimate = 0 ↔ IsFor target threshold inputs