Cartesian powers for approximate counting -- proof internals

theorem Complexity.ApproximateCounting.mem_cartesianPower_iff_internal {domainWidth copies : ℕ} {set : Finset (BitString domainWidth)} {input : BitString (copies * domainWidth)} : input ∈ cartesianPower set copies ↔ ∀ (copy : Fin copies), (blocksEquiv copies domainWidth) input copy ∈ set

theorem Complexity.ApproximateCounting.card_cartesianPower_internal {domainWidth : ℕ} (set : Finset (BitString domainWidth)) (copies : ℕ) : (cartesianPower set copies).card = set.card ^ copies

theorem Complexity.ApproximateCounting.relativeCopies_separates_sixteen_internal (precision : ℕ) (hprecision : 0 < precision) : 16 ^ 2 * precision ^ relativeCopies precision ≤ (precision + 1) ^ relativeCopies precision

theorem Complexity.ApproximateCounting.upperRootEstimate_isRelativeApproximation_internal {factor copies precision actual weakEstimate : ℕ} (hcopies : 0 < copies) (hprecision : 0 < precision) (hseparation : factor ^ 2 * precision ^ copies ≤ (precision + 1) ^ copies) (hweak : IsFactorApproximation factor (actual ^ copies) weakEstimate) : IsRelativeApproximation precision actual (upperRootEstimate factor copies weakEstimate)

theorem Complexity.ApproximateCounting.boostedEstimate_isRelativeApproximation_internal {precision actual weakEstimate : ℕ} (hprecision : 0 < precision) (hweak : IsFactorApproximation 16 (actual ^ relativeCopies precision) weakEstimate) : IsRelativeApproximation precision actual (boostedEstimate precision weakEstimate)

theorem Complexity.ApproximateCounting.boostedEstimate_cartesianPower_isRelativeApproximation_internal {domainWidth precision weakEstimate : ℕ} (set : Finset (BitString domainWidth)) (hprecision : 0 < precision) (hweak : IsFactorApproximation 16 (cartesianPower set (relativeCopies precision)).card weakEstimate) : IsRelativeApproximation precision set.card (boostedEstimate precision weakEstimate)