Korten's harmonic mean transform

This module formalizes Definition 5, Lemmas 11--12, and Corollary 1 of Oliver Korten, Top-Down Lower Bounds for All Depths, ECCC TR26-221 (2026), https://eccc.weizmann.ac.il/report/2026/221/.

harmonicMean_variational works on any nonempty finite type. The coordinate transform uses Boolean membership functions for sets and real nonnegative densities. harmonicTransform_eq_harmonicMean_coordinateMarginal identifies the convenient full-cube representation with the harmonic mean over actual projected patterns. Zero entries give harmonic mean zero, as in the paper.

expect_sqrt_le_bernoulliAverage_sqrt_harmonicTransform is Lemma 12, including dimension zero. harmonicTransform_good_probability supplies the intermediate 1/4-sampling estimate in the proof of Lemma 10, using a density bound B in place of 2 ^ k. The sparse-sampling conclusion and pattern count of Lemma 10 are proved in Complexitylib.BooleanAnalysis.LightPatterns, which feeds the mirror-set argument of Complexitylib.BooleanAnalysis.MirrorSets. The top-down communication and circuit lower bounds of Theorem 3 are Complexity.KarchmerWigderson.parity_communication_lower_bound and Complexity.Circuit.parity_wire_lower_bound in Complexitylib.Circuits.KarchmerWigderson.TopDown.

theorem Complexity.BooleanAnalysis.harmonicMean_eq_zero_of_exists {α : Type u_1} [Fintype α] {f : α → ℝ} (hf : ∃ (x : α), f x = 0) : harmonicMean f = 0

A zero entry makes the harmonic mean zero, implementing 0⁻¹ = ∞ inside the average rather than Lean's real inverse at zero.

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

Harmonic means of nonnegative entries are nonnegative.

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

The harmonic mean of a constant on a nonempty finite set is that constant.

theorem Complexity.BooleanAnalysis.harmonicMean_le_energy {α : 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

Every weight with mean one bounds the harmonic mean by its quadratic energy. The weight need not be nonnegative for this direction.

theorem Complexity.BooleanAnalysis.harmonicMean_exists_weight {α : 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

A nonnegative weight of mean one attains the variational minimum, including when an entry of f is zero.

theorem Complexity.BooleanAnalysis.harmonicMean_variational {α : 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}

Korten's Lemma 11, generalized to every nonempty finite type.

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

Harmonic means are monotone in their nonnegative entries.

theorem Complexity.BooleanAnalysis.harmonicMean_concave {α : 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

Harmonic means are concave on nonnegative functions.

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

The harmonic mean is at most the arithmetic mean.

theorem Complexity.BooleanAnalysis.harmonicMean_light_fraction_le {α : 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

A positive harmonic-mean lower bound controls the fraction of small entries. This is the reciprocal-density Markov step used for light patterns.

theorem Complexity.BooleanAnalysis.projectionAverage_eq_coordinateMarginal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) (selected x : ι → Bool) : projectionAverage f selected x = coordinateMarginal f selected fun (i : { i : ι // selected i = true }) => x ↑i

The full-cube projection depends exactly on the selected input pattern.

theorem Complexity.BooleanAnalysis.expect_coordinateMarginal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) (selected : ι → Bool) : (Finset.univ.expect fun (z : { i : ι // selected i = true } → Bool) => coordinateMarginal f selected z) = Finset.univ.expect fun (x : ι → Bool) => f x

Marginalization preserves the uniform mean, hence also density normalization.

theorem Complexity.BooleanAnalysis.harmonicTransform_eq_harmonicMean_coordinateMarginal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) (selected : ι → Bool) : harmonicTransform f selected = harmonicMean (coordinateMarginal f selected)

The transform agrees with Definition 5 on the actual projected cube; repeating each pattern on the full cube does not change its harmonic mean.

theorem Complexity.BooleanAnalysis.harmonicTransform_variational {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → ℝ} (hf : ∀ (x : ι → Bool), 0 ≤ f x) (selected : ι → Bool) : harmonicTransform f selected = sInf {a : ℝ | ∃ (w : ({ i : ι // selected i = true } → Bool) → ℝ), (∀ (z : { i : ι // selected i = true } → Bool), 0 ≤ w z) ∧ (Finset.univ.expect fun (z : { i : ι // selected i = true } → Bool) => w z) = 1 ∧ (Finset.univ.expect fun (z : { i : ι // selected i = true } → Bool) => coordinateMarginal f selected z * w z ^ 2) = a}

Lemma 11 on the selected-coordinate cube, with nonnegative weights of mean one.

theorem Complexity.BooleanAnalysis.coordinateMarginal_light_fraction_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → ℝ} (hf : ∀ (x : ι → Bool), 0 ≤ f x) (selected : ι → Bool) {a b : ℝ} (ha : 0 < a) (ha' : a ≤ harmonicTransform f selected) (hb : 0 ≤ b) : (Finset.univ.expect fun (z : { i : ι // selected i = true } → Bool) => if coordinateMarginal f selected z ≤ b then 1 else 0) ≤ b / a

A positive transform lower bound bounds the fraction of light projected patterns. The expectation ranges over the actual selected-coordinate cube.

theorem Complexity.BooleanAnalysis.harmonicTransform_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → ℝ} (hf : ∀ (x : ι → Bool), 0 ≤ f x) (selected : ι → Bool) : 0 ≤ harmonicTransform f selected

The harmonic transform is nonnegative on nonnegative functions.

theorem Complexity.BooleanAnalysis.harmonicTransform_concave {ι : 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

Corollary 1(1): the transform is pointwise concave in its input function.

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

Selecting no coordinates gives the ordinary mean.

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

Selecting all coordinates gives the harmonic mean of the original function.

theorem Complexity.BooleanAnalysis.harmonicTransform_const {ι : Type u_1} [Fintype ι] [DecidableEq ι] (c : ℝ) (selected : ι → Bool) : harmonicTransform (fun (x : ι → Bool) => c) selected = c

Constants are fixed by the harmonic transform.

theorem Complexity.BooleanAnalysis.harmonicTransform_antitone {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

Corollary 1(2): revealing more coordinates decreases the harmonic transform. The hypothesis is inclusion of the two sets represented by Boolean masks.

theorem Complexity.BooleanAnalysis.harmonicTransform_le_expect {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

Corollary 1(3): the harmonic transform is at most the ordinary mean.

theorem Complexity.BooleanAnalysis.expect_sqrt_le_bernoulliAverage_sqrt_harmonicTransform {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)

Korten's Lemma 12: on the 1/4-biased coordinate cube, the mean square root of the harmonic transform dominates the uniform mean square root of f.

theorem Complexity.BooleanAnalysis.harmonicTransform_good_probability {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

Intermediate estimate in the proof of Lemma 10: a normalized density bounded by B has harmonic transform at least 1 / (4 * B) with probability at least 1 / (2 * sqrt B) under 1/4-coordinate sampling. The LightPatterns module transfers this estimate to sparse sampling.