Geometric means under a measure on a finite type

The geometric mean of a function f under a measure μ on a finite type is the product of the values of f, each to the power of the mass of its atom. Under a probability measure it is the exponential of the expected logarithm of f, so it is the value itself when f is constant on the atoms of positive mass, and evaluation at a point under a point mass.

Main definitions

• MeasureTheory.Measure.geomMean: the geometric mean ∏ a, f a ^ μ.real {a}.

Main results

• MeasureTheory.Measure.geomMean_dirac: under a point mass the mean is evaluation.
• MeasureTheory.Measure.geomMean_prod: under a product measure the mean is the iterated mean.
• MeasureTheory.Measure.geomMean_of_forall_eq: the mean of a function constant on the atoms of positive mass is that constant.
• MeasureTheory.Measure.geomMean_eq_zero_iff: the mean vanishes exactly when the function vanishes at an atom of positive mass.
• MeasureTheory.Measure.geomMean_eq_ofReal_exp_sum_log: the mean is the exponential of the expected logarithm.

noncomputable def MeasureTheory.Measure.geomMean {α : Type u_1} [MeasurableSpace α] [Fintype α] (μ : Measure α) (f : α → ENNReal) : ENNReal

The geometric mean of a function on a finite type under a measure weights each value by the mass of its atom.

Equations

• μ.geomMean f = ∏ a : α, f a ^ μ.real {a}

theorem MeasureTheory.Measure.geomMean_mul {α : Type u_1} [MeasurableSpace α] [Fintype α] (μ : Measure α) (f g : α → ENNReal) : (μ.geomMean fun (a : α) => f a * g a) = μ.geomMean f * μ.geomMean g

theorem MeasureTheory.Measure.geomMean_rpow {α : Type u_1} [MeasurableSpace α] [Fintype α] (μ : Measure α) (f : α → ENNReal) {r : ℝ} (hr : 0 ≤ r) : (μ.geomMean fun (a : α) => f a ^ r) = μ.geomMean f ^ r

theorem MeasureTheory.Measure.geomMean_mono {α : Type u_1} [MeasurableSpace α] [Fintype α] {μ : Measure α} {f g : α → ENNReal} (h : ∀ (a : α), f a ≤ g a) : μ.geomMean f ≤ μ.geomMean g

theorem MeasureTheory.Measure.geomMean_congr {α : Type u_1} [MeasurableSpace α] [Fintype α] {μ : Measure α} {f g : α → ENNReal} (h : ∀ (a : α), μ {a} ≠ 0 → f a = g a) : μ.geomMean f = μ.geomMean g

The geometric mean depends on the function only at the atoms of positive mass.

theorem MeasureTheory.Measure.geomMean_ne_top {α : Type u_1} [MeasurableSpace α] [Fintype α] {μ : Measure α} {f : α → ENNReal} (h : ∀ (a : α), μ {a} ≠ 0 → f a ≠ ⊤) : μ.geomMean f ≠ ⊤

theorem MeasureTheory.Measure.geomMean_ne_zero {α : Type u_1} [MeasurableSpace α] [Fintype α] {μ : Measure α} {f : α → ENNReal} (h : ∀ (a : α), μ {a} ≠ 0 → f a ≠ 0) : μ.geomMean f ≠ 0

theorem MeasureTheory.Measure.geomMean_eq_zero_iff {α : Type u_1} [MeasurableSpace α] [Fintype α] {μ : Measure α} {f : α → ENNReal} [IsFiniteMeasure μ] : μ.geomMean f = 0 ↔ ∃ (a : α), μ {a} ≠ 0 ∧ f a = 0

The geometric mean vanishes exactly when the function vanishes at an atom of positive mass.

theorem MeasureTheory.Measure.geomMean_eq_ofReal_exp_sum_log {α : Type u_1} [MeasurableSpace α] [Fintype α] {μ : Measure α} {f : α → ENNReal} (h0 : ∀ (a : α), μ {a} ≠ 0 → f a ≠ 0) (htop : ∀ (a : α), μ {a} ≠ 0 → f a ≠ ⊤) : μ.geomMean f = ENNReal.ofReal (Real.exp (∑ a : α, μ.real {a} * Real.log (f a).toReal))

The geometric mean is the exponential of the expected logarithm, for a function that is positive and finite at the atoms of positive mass.

theorem MeasureTheory.Measure.geomMean_prod {α : Type u_1} [MeasurableSpace α] [Fintype α] {β : Type u_2} [MeasurableSpace β] [Fintype β] (μ : Measure α) (ν : Measure β) [SFinite ν] (f : α × β → ENNReal) : (μ.prod ν).geomMean f = μ.geomMean fun (a : α) => ν.geomMean fun (b : β) => f (a, b)

Under a product measure the geometric mean is the mean over the first factor of the means over the second.

@[simp]

theorem MeasureTheory.Measure.geomMean_const {α : Type u_1} [MeasurableSpace α] [Fintype α] [MeasurableSingletonClass α] (μ : Measure α) [IsProbabilityMeasure μ] (c : ENNReal) : (μ.geomMean fun (x : α) => c) = c

theorem MeasureTheory.Measure.geomMean_of_forall_eq {α : Type u_1} [MeasurableSpace α] [Fintype α] {μ : Measure α} {f : α → ENNReal} {c : ENNReal} [MeasurableSingletonClass α] [IsProbabilityMeasure μ] (h : ∀ (a : α), μ {a} ≠ 0 → f a = c) : μ.geomMean f = c

The geometric mean under a probability measure of a function constant on the atoms of positive mass is that constant.

@[simp]

theorem MeasureTheory.Measure.geomMean_dirac {α : Type u_1} [MeasurableSpace α] [Fintype α] [MeasurableSingletonClass α] (a : α) (f : α → ENNReal) : (dirac a).geomMean f = f a

Under a point mass the geometric mean is evaluation at the point.