Dense distributions and good coordinate projections

The first probability estimate in the proof of Korten's Lemma 10, before transference to a sparse coordinate set. We use a pointwise density bound B instead of writing it as 2 ^ k.

theorem Complexity.BooleanAnalysis.harmonicTransform_good_probability_internal {n : ℕ} {f : (Fin n → Bool) → ℝ} (hf : ∀ (x : Fin n → Bool), 0 ≤ f x) (hmean : (Finset.univ.expect fun (x : Fin n → Bool) => f x) = 1) {B : ℝ} (hB : 1 ≤ B) (hbound : ∀ (x : Fin n → Bool), f x ≤ B) : 1 / (2 * √B) ≤ bernoulliAverage (1 / 4) fun (selected : Fin n → Bool) => if 1 / (4 * B) ≤ harmonicTransform f selected then 1 else 0