Median of a distribution

DefinitionMedian of a measure on the real line#✓fully proved

Let \(\nu\) be a measure on \(\mathbb{R}\), typically a probability measure. A real number \(m\) is a median of \(\nu\) when \(\nu((-\infty, m]) \ge 1/2\) and \(\nu([m, \infty)) \ge 1/2\), where a set of infinite measure counts as having measure \(0\).

def IsMedian (ν : Measure ℝ) (m : ℝ) : Prop :=
  1 / 2 ≤ ν.real (Iic m) ∧ 1 / 2 ≤ ν.real (Ici m)

Used by 4

Used byA posterior median is a Bayes estimator for absolute loss · Measurable choices of posterior medians · The expected absolute loss is minimized at every median · A median minimizes the expected absolute loss

TheoremAbsolute deviations are integrable exactly when the mean exists#✓fully proved

Let \(\nu\) be a finite measure on \(\mathbb{R}\) and let \(c \in \mathbb{R}\). Then \(\theta \mapsto |\theta - c|\) is \(\nu\)-integrable if and only if \(\theta \mapsto \theta\) is \(\nu\)-integrable.

theorem integrable_abs_sub_iff (ν : Measure ℝ) [IsFiniteMeasure ν] (c : ℝ) :
    Integrable (fun θ => |θ - c|) ν ↔ Integrable (fun θ : ℝ => θ) ν

Used by 2

Used byThe expected absolute loss is minimized at every median · A median minimizes the expected absolute loss

TheoremA median minimizes the expected absolute loss#✓fully proved

Let \(\nu\) be a probability measure on \(\mathbb{R}\) and let \(m\) be a median of \(\nu\). Then for every \(y \in \mathbb{R}\),

\[ \int |\theta - m| \, d\nu(\theta) \le \int |\theta - y| \, d\nu(\theta). \]

When \(\nu\) has no first moment, neither integrand is integrable and both integrals are \(0\) by the convention for non-integrable functions.

theorem integral_abs_sub_le_of_isMedian (ν : Measure ℝ) [IsProbabilityMeasure ν] {m : ℝ}
    (hm : IsMedian ν m) (y : ℝ) : ∫ θ, |θ - m| ∂ν ≤ ∫ θ, |θ - y| ∂ν

Uses 2 · Used by 1

Statement usesMedian of a measure on the real line

Proof usesAbsolute deviations are integrable exactly when the mean exists

Used byThe expected absolute loss is minimized at every median

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.