Harmonic means and coordinate projections

Definitions for Section 4 of Oliver Korten, Top-Down Lower Bounds for All Depths, ECCC TR26-221 (2026), https://eccc.weizmann.ac.il/report/2026/221/.

The harmonic mean is zero if any value is zero. This implements the paper's extended-real convention without using the real-number convention 0⁻¹ = 0 inside the average. Theorems assume nonnegative inputs.

A coordinate set is its Boolean membership function. Projections are represented on the full cube: their value depends only on the selected coordinates. Averaging on the full cube gives each projected pattern the same multiplicity, so this is the uniform average over projected patterns. All expectations are finite sums.

noncomputable def Complexity.BooleanAnalysis.harmonicMean {α : Type u_1} [Fintype α] (f : α → ℝ) : ℝ

The uniform harmonic mean, with value zero whenever an entry is zero.

Equations

• Complexity.BooleanAnalysis.harmonicMean f = if ∃ (x : α), f x = 0 then 0 else (Finset.univ.expect fun (x : α) => (f x)⁻¹)⁻¹

noncomputable def Complexity.BooleanAnalysis.projectionAverage {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) (selected x : ι → Bool) : ℝ

Average over the unselected coordinates, keeping the selected bits of x.

Equations

• Complexity.BooleanAnalysis.projectionAverage f selected x = Finset.univ.expect fun (y : ι → Bool) => f fun (i : ι) => if selected i = true then x i else y i

noncomputable def Complexity.BooleanAnalysis.coordinateMarginal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) (selected : ι → Bool) (pattern : { i : ι // selected i = true } → Bool) : ℝ

The marginal on actual selected-coordinate patterns, obtained by uniformly averaging over their completions. For a normalized density f, this is the normalized density of its coordinate projection.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.BooleanAnalysis.harmonicTransform {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) (selected : ι → Bool) : ℝ

Korten's harmonic mean transform (Definition 5), represented on the full cube.

Equations

• Complexity.BooleanAnalysis.harmonicTransform f selected = Complexity.BooleanAnalysis.harmonicMean (Complexity.BooleanAnalysis.projectionAverage f selected)