Sampling facts for top-down initializations

Coordinate marginals, the empty-mask probability, and an elementary bound on that probability. These are shared by the parity and majority proofs.

theorem Complexity.BooleanAnalysis.bernoulliAverage_coordinate_internal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) (i : ι) : (bernoulliAverage p fun (s : ι → Bool) => if s i = true then 1 else 0) = p

theorem Complexity.BooleanAnalysis.bernoulliAverage_nonempty_internal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) : (bernoulliAverage p fun (P : ι → Bool) => if ∃ (i : ι), P i = true then 1 else 0) = 1 - (1 - p) ^ Fintype.card ι

theorem Complexity.BooleanAnalysis.one_sub_pow_bound_internal {p : ℝ} (hp' : p ≤ 1) (n : ℕ) : (1 - p) ^ n * (1 + ↑n * p) ≤ 1