Finite harmonic mean: proof internals

The variational formula of Korten (2026), Lemma 11, is proved for every nonempty finite type. Completing the square gives the lower bound, and an explicit weight attains it, including when an entry vanishes.

theorem Complexity.BooleanAnalysis.harmonicMean_nonneg_internal {α : Type u_1} [Fintype α] {f : α → ℝ} (hf : ∀ (x : α), 0 ≤ f x) : 0 ≤ harmonicMean f

theorem Complexity.BooleanAnalysis.harmonicMean_le_energy_internal {α : Type u_1} [Fintype α] [Nonempty α] {f w : α → ℝ} (hf : ∀ (x : α), 0 ≤ f x) (hw : (Finset.univ.expect fun (x : α) => w x) = 1) : harmonicMean f ≤ Finset.univ.expect fun (x : α) => f x * w x ^ 2

theorem Complexity.BooleanAnalysis.harmonicMean_exists_weight_internal {α : Type u_1} [Fintype α] [Nonempty α] {f : α → ℝ} (hf : ∀ (x : α), 0 ≤ f x) : ∃ (w : α → ℝ), (∀ (x : α), 0 ≤ w x) ∧ (Finset.univ.expect fun (x : α) => w x) = 1 ∧ (Finset.univ.expect fun (x : α) => f x * w x ^ 2) = harmonicMean f

theorem Complexity.BooleanAnalysis.harmonicMean_variational_internal {α : Type u_1} [Fintype α] [Nonempty α] {f : α → ℝ} (hf : ∀ (x : α), 0 ≤ f x) : harmonicMean f = sInf {a : ℝ | ∃ (w : α → ℝ), (∀ (x : α), 0 ≤ w x) ∧ (Finset.univ.expect fun (x : α) => w x) = 1 ∧ (Finset.univ.expect fun (x : α) => f x * w x ^ 2) = a}

theorem Complexity.BooleanAnalysis.harmonicMean_mono_internal {α : Type u_1} [Fintype α] [Nonempty α] {f g : α → ℝ} (hf : ∀ (x : α), 0 ≤ f x) (hfg : ∀ (x : α), f x ≤ g x) : harmonicMean f ≤ harmonicMean g

theorem Complexity.BooleanAnalysis.harmonicMean_concave_internal {α : Type u_1} [Fintype α] [Nonempty α] {f g : α → ℝ} (hf : ∀ (x : α), 0 ≤ f x) (hg : ∀ (x : α), 0 ≤ g x) {t : ℝ} (ht : 0 ≤ t) (ht' : t ≤ 1) : t * harmonicMean f + (1 - t) * harmonicMean g ≤ harmonicMean fun (x : α) => t * f x + (1 - t) * g x

theorem Complexity.BooleanAnalysis.harmonicMean_le_expect_internal {α : Type u_1} [Fintype α] [Nonempty α] {f : α → ℝ} (hf : ∀ (x : α), 0 ≤ f x) : harmonicMean f ≤ Finset.univ.expect fun (x : α) => f x

theorem Complexity.BooleanAnalysis.harmonicMean_const_internal {α : Type u_1} [Fintype α] [Nonempty α] (c : ℝ) : (harmonicMean fun (x : α) => c) = c

theorem Complexity.BooleanAnalysis.harmonicMean_equiv_internal {α : Type u_1} [Fintype α] {β : Type u_2} [Fintype β] (e : α ≃ β) (f : β → ℝ) : (harmonicMean fun (x : α) => f (e x)) = harmonicMean f

theorem Complexity.BooleanAnalysis.harmonicMean_average_internal {α : Type u_1} [Fintype α] [Nonempty α] {β : Type u_2} [Fintype β] {f : β → α → ℝ} (hf : ∀ (y : β) (x : α), 0 ≤ f y x) : (Finset.univ.expect fun (y : β) => harmonicMean (f y)) ≤ harmonicMean fun (x : α) => Finset.univ.expect fun (y : β) => f y x

theorem Complexity.BooleanAnalysis.expect_pair_internal {α : Type u_1} [Fintype α] {β : Type u_2} [Fintype β] (f : α × β → ℝ) : (Finset.univ.expect fun (x : α × β) => f x) = Finset.univ.expect fun (a : α) => Finset.univ.expect fun (b : β) => f (a, b)

theorem Complexity.BooleanAnalysis.expect_bool_internal (f : Bool → ℝ) : (Finset.univ.expect fun (b : Bool) => f b) = (f false + f true) / 2

theorem Complexity.BooleanAnalysis.harmonicMean_pair_internal {α : Type u_1} [Fintype α] [Nonempty α] {f : Bool → α → ℝ} (hf : ∀ (b : Bool) (x : α), 0 ≤ f b x) : (harmonicMean fun (x : Bool × α) => f x.1 x.2) = 2 * harmonicMean (f false) * harmonicMean (f true) / (harmonicMean (f false) + harmonicMean (f true))

theorem Complexity.BooleanAnalysis.harmonicMean_light_fraction_le_internal {α : Type u_1} [Fintype α] [Nonempty α] {f : α → ℝ} (hf : ∀ (x : α), 0 ≤ f x) {a b : ℝ} (ha : 0 < a) (ha' : a ≤ harmonicMean f) (hb : 0 ≤ b) : (Finset.univ.expect fun (x : α) => if f x ≤ b then 1 else 0) ≤ b / a