Order properties of the harmonic mean transform

The three parts of Corollary 1 in Korten (2026): concavity, decrease under revealing more coordinates, and the upper bound by the ordinary mean.

theorem Complexity.BooleanAnalysis.harmonicPair_le_midpoint_internal {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) : 2 * a * b / (a + b) ≤ (a + b) / 2

theorem Complexity.BooleanAnalysis.harmonicPair_mono_internal {a b c d : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hac : a ≤ c) (hbd : b ≤ d) : 2 * a * b / (a + b) ≤ 2 * c * d / (c + d)

theorem Complexity.BooleanAnalysis.harmonicTransform_concave_internal {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f g : (ι → Bool) → ℝ} (hf : ∀ (x : ι → Bool), 0 ≤ f x) (hg : ∀ (x : ι → Bool), 0 ≤ g x) {t : ℝ} (ht : 0 ≤ t) (ht' : t ≤ 1) (selected : ι → Bool) : t * harmonicTransform f selected + (1 - t) * harmonicTransform g selected ≤ harmonicTransform (fun (x : ι → Bool) => t * f x + (1 - t) * g x) selected

theorem Complexity.BooleanAnalysis.harmonicTransform_antitone_internal {n : ℕ} {f : (Fin n → Bool) → ℝ} (hf : ∀ (x : Fin n → Bool), 0 ≤ f x) {r s : Fin n → Bool} (hrs : ∀ (i : Fin n), r i = true → s i = true) : harmonicTransform f s ≤ harmonicTransform f r

theorem Complexity.BooleanAnalysis.harmonicTransform_empty_internal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) : (harmonicTransform f fun (x : ι) => false) = Finset.univ.expect fun (x : ι → Bool) => f x

theorem Complexity.BooleanAnalysis.harmonicTransform_full_internal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) : (harmonicTransform f fun (x : ι) => true) = harmonicMean f

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