Weak approximate counting -- proof internals

theorem Complexity.ApproximateCounting.Weak.estimate_lt_two_pow_add_four_internal {domainWidth : ℕ} (responses : Level domainWidth → Bool) : estimate responses < 2 ^ (domainWidth + 4)

theorem Complexity.ApproximateCounting.Weak.mem_trueLevels_iff_internal {domainWidth : ℕ} {responses : Level domainWidth → Bool} {level : Level domainWidth} : level ∈ trueLevels responses ↔ responses level = true

theorem Complexity.ApproximateCounting.Weak.selectedLevel_mem_trueLevels_internal {domainWidth : ℕ} {responses : Level domainWidth → Bool} (hnonempty : (trueLevels responses).Nonempty) : selectedLevel responses ∈ trueLevels responses

theorem Complexity.ApproximateCounting.Weak.le_selectedLevel_of_mem_internal {domainWidth : ℕ} {responses : Level domainWidth → Bool} {level : Level domainWidth} (hlevel : level ∈ trueLevels responses) : level ≤ selectedLevel responses

theorem Complexity.ApproximateCounting.Weak.response_selectedLevel_eq_true_of_nonempty_internal {domainWidth : ℕ} {responses : Level domainWidth → Bool} (hnonempty : (trueLevels responses).Nonempty) : responses (selectedLevel responses) = true

theorem Complexity.ApproximateCounting.Weak.estimate_eq_zero_of_cardinality_eq_zero_internal {domainWidth cardinality : ℕ} {responses : Level domainWidth → Bool} (haccurate : ResponsesAccurate responses) (hzero : cardinality = 0) : estimate responses = 0

theorem Complexity.ApproximateCounting.Weak.estimate_eq_pow_of_cardinality_pos_internal {domainWidth cardinality : ℕ} {responses : Level domainWidth → Bool} (haccurate : ResponsesAccurate responses) (hpositive : 0 < cardinality) : estimate responses = 2 ^ ↑(selectedLevel responses)

theorem Complexity.ApproximateCounting.Weak.selectedLevel_response_eq_true_of_cardinality_pos_internal {domainWidth cardinality : ℕ} {responses : Level domainWidth → Bool} (haccurate : ResponsesAccurate responses) (hpositive : 0 < cardinality) : responses (selectedLevel responses) = true

theorem Complexity.ApproximateCounting.Weak.estimate_le_sixteen_mul_internal {domainWidth cardinality : ℕ} {responses : Level domainWidth → Bool} (haccurate : ResponsesAccurate responses) : estimate responses ≤ 16 * cardinality

theorem Complexity.ApproximateCounting.Weak.cardinality_le_sixteen_mul_estimate_internal {domainWidth cardinality : ℕ} {responses : Level domainWidth → Bool} (hcardinality : cardinality ≤ 2 ^ domainWidth) (haccurate : ResponsesAccurate responses) : cardinality ≤ 16 * estimate responses

theorem Complexity.ApproximateCounting.Weak.estimate_isFactorApproximation_internal {domainWidth cardinality : ℕ} {responses : Level domainWidth → Bool} (hcardinality : cardinality ≤ 2 ^ domainWidth) (haccurate : ResponsesAccurate responses) : IsFactorApproximation 16 cardinality (estimate responses)