Harmonic means on finite types

The harmonic mean of a nonnegative function on a finite type (Cslib.harmonicMean), zero as soon as a value is zero, has a variational formula: it is the least energy 𝔼 (f w ^ 2) of a nonnegative weight w of mean one Korten, Lemma 11 (Cslib.harmonicMean_variational). Completing the square gives the lower bound (Cslib.harmonicMean_le_energy), and an explicit weight attains it, including when a value vanishes (Cslib.harmonicMean_exists_weight). Hence the harmonic mean is monotone (Cslib.harmonicMean_mono) and concave (Cslib.concaveOn_harmonicMean), and at most the arithmetic mean (Cslib.harmonicMean_le_expect).

Main definitions

• Cslib.harmonicMean: the uniform harmonic mean on a finite type, zero whenever an entry is zero.

Main results

• Cslib.harmonicMean_le_energy, Cslib.harmonicMean_exists_weight, Cslib.harmonicMean_variational: the variational formula for the harmonic mean.
• Cslib.harmonicMean_mono, Cslib.concaveOn_harmonicMean, Cslib.harmonicMean_le_expect, Cslib.expect_harmonicMean_le: monotonicity, concavity, comparison with the arithmetic mean, and Jensen's inequality.
• Cslib.harmonicMean_light_fraction_le: reciprocal-density Markov bound for small entries.
• Cslib.harmonicMean_pair: two-point harmonic mean decomposition on Bool × α.

References

• O. Korten, Top-Down Lower Bounds for All Depths

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

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

theorem Cslib.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: inside the average, 0⁻¹ counts as ∞ rather than as Lean's 0⁻¹ = 0.

theorem Cslib.harmonicMean_of_pos {α : Type u_1} [Fintype α] {f : α → ℝ} (hf : ∀ (x : α), 0 < f x) : harmonicMean f = (Finset.univ.expect fun (x : α) => (f x)⁻¹)⁻¹

The harmonic mean of positive entries is the reciprocal of the mean of their reciprocals.

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

Harmonic means of nonnegative entries are nonnegative.

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

An equivalence of finite types preserves harmonic means.

theorem Cslib.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 Cslib.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 Cslib.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}

The variational formula for the harmonic mean Korten, Lemma 11, on every nonempty finite type: the harmonic mean is the least energy 𝔼 (f w ^ 2) of a nonnegative weight w of mean one.

theorem Cslib.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 Cslib.concaveOn_harmonicMean {α : Type u_1} [Fintype α] [Nonempty α] : ConcaveOn ℝ (Set.Ici 0) harmonicMean

The harmonic mean is concave on nonnegative functions.

theorem Cslib.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 Cslib.expect_harmonicMean_le {α : 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

Jensen's inequality for the harmonic mean: the average of harmonic means is at most the harmonic mean of the average.

theorem Cslib.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 Cslib.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 Cslib.harmonicMean_pair {α : 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))

The harmonic mean of a function on Bool × α is the two-point harmonic mean 2 h₀ h₁ / (h₀ + h₁) of the harmonic means h₀, h₁ of its two halves.