Korten's harmonic mean inequality: proof internals

Lemma 12 of Top-Down Lower Bounds for All Depths (2026). The scalar inequality is followed by induction on dimension using concavity of the harmonic mean. No strict-positivity assumption is needed.

theorem Complexity.BooleanAnalysis.harmonicMean_sqrt_pair_internal {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) : (√a + √b) / 2 ≤ 3 / 4 * √((a + b) / 2) + 1 / 4 * √(2 * a * b / (a + b))

theorem Complexity.BooleanAnalysis.expect_sqrt_le_bernoulliAverage_sqrt_harmonicTransform_internal {n : ℕ} {f : (Fin n → Bool) → ℝ} (hf : ∀ (x : Fin n → Bool), 0 ≤ f x) : (Finset.univ.expect fun (x : Fin n → Bool) => √(f x)) ≤ bernoulliAverage (1 / 4) fun (selected : Fin n → Bool) => √(harmonicTransform f selected)