Samuelson’s outlier bound

Paper

How Deviant Can You Be?, 1968. Journal of the American Statistical Association 63(324), pp. 1522–1525. Read Goroncy and Rychlik’s later treatment.

The result

In any finite nonempty dataset, every squared deviation from the sample mean is at most N − 1 times the population variance of that same dataset. The bound is attained when all other observations coincide.

μ = Σᵢxᵢ/N, σ² = Σᵢ(xᵢ − μ)²/N (xₖ − μ)² ≤ (N − 1)σ²

Scope & assumptions

4 checked theorems. Centering, a zero-sum inequality, the deviation bound, and equality when all other centered observations coincide. No probabilistic tail estimate or simultaneous order-statistic bounds.

A finite set of indices, arbitrary real observations, and an index k in that set. Variance uses N, not N − 1. The squared version includes zero variance and a singleton dataset, without dividing by the standard deviation.

Prior work

No matching named formalization was located in the bounded search of two Mathlib revisions and indexed web results on 2026-09-10. Related library ingredients already exist. First-formalization status is unconfirmed; this does not establish priority.

Lean proof

Lean + Mathlib 4.33.1 · 4 checked theorems

import Mathlib.Algebra.Order.BigOperators.Ring.Finset
import Mathlib.Data.Real.Basic
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Ring
import Mathlib.Tactic.Linarith

/-! Samuelson (1968), How Deviant Can You Be?
The single-observation bound for a finite deterministic population.
Variance uses divisor N, not the unbiased sample-estimator divisor N - 1. -/
namespace PaperToLean.Samuelson
noncomputable section
open scoped BigOperators
variable {ι : Type*}

def mean (I : Finset ι) (x : ι → ℝ) : ℝ := (∑ i ∈ I, x i) / I.card
def variance (I : Finset ι) (x : ι → ℝ) : ℝ :=
  (∑ i ∈ I, (x i - mean I x) ^ 2) / I.card

theorem centered_sum (I : Finset ι) (x : ι → ℝ) (hI : I.Nonempty) :
    ∑ i ∈ I, (x i - mean I x) = 0 := by
  have hn : (I.card : ℝ) ≠ 0 := by exact_mod_cast (ne_of_gt hI.card_pos)
  simp only [Finset.sum_sub_distrib, Finset.sum_const, nsmul_eq_mul, mean]
  field_simp
  ring

theorem zero_sum_bound (I : Finset ι) (d : ι → ℝ) (k : ι) (hk : k ∈ I)
    (hd : ∑ i ∈ I, d i = 0) :
    (I.card : ℝ) * (d k) ^ 2 ≤ (I.card - 1 : ℝ) * ∑ i ∈ I, (d i) ^ 2 := by
  classical
  have hc := Finset.sum_mul_sq_le_sq_mul_sq (I.erase k) (fun _ => (1 : ℝ)) d
  simp only [one_mul, one_pow, Finset.sum_const, nsmul_eq_mul, mul_one,
    Finset.sum_erase_eq_sub hk, hd, zero_sub, neg_sq] at hc
  nlinarith

theorem deviation_bound (I : Finset ι) (x : ι → ℝ) (k : ι) (hk : k ∈ I) :
    (x k - mean I x) ^ 2 ≤ (I.card - 1 : ℝ) * variance I x := by
  have hn : (0 : ℝ) < I.card := by exact_mod_cast (Finset.card_pos.mpr ⟨k, hk⟩)
  have h := zero_sum_bound I (fun i => x i - mean I x) k hk (centered_sum I x ⟨k, hk⟩)
  unfold variance
  rw [← mul_div_assoc]
  apply (le_div_iff₀ hn).mpr
  nlinarith

/-- If all other centered observations agree, the bound is an equality. -/
theorem equality_when_others_equal (I : Finset ι) (d : ι → ℝ) (k : ι)
    (hk : k ∈ I) (c : ℝ) (hothers : ∀ i ∈ I, i ≠ k → d i = c)
    (hd : ∑ i ∈ I, d i = 0) :
    (I.card : ℝ) * (d k) ^ 2 = (I.card - 1 : ℝ) * ∑ i ∈ I, (d i) ^ 2 := by
  classical
  have hn : 1 ≤ I.card := Nat.succ_le_of_lt (Finset.card_pos.mpr ⟨k, hk⟩)
  have he : ∑ i ∈ I.erase k, d i = (I.card - 1 : ℝ) * c := by
    rw [Finset.sum_congr rfl (fun i hi => hothers i (Finset.mem_erase.mp hi).2 (Finset.mem_erase.mp hi).1)]
    simp [Finset.card_erase_of_mem hk, Nat.cast_sub hn]
  have he2 : ∑ i ∈ I.erase k, (d i) ^ 2 = (I.card - 1 : ℝ) * c ^ 2 := by
    rw [Finset.sum_congr rfl (fun i hi => congrArg (· ^ 2)
      (hothers i (Finset.mem_erase.mp hi).2 (Finset.mem_erase.mp hi).1))]
    simp [Finset.card_erase_of_mem hk, Nat.cast_sub hn]
  have hz := Finset.sum_erase_add I d hk
  rw [he, hd] at hz
  have hs := Finset.sum_erase_add I (fun i => (d i) ^ 2) hk
  rw [he2] at hs
  have hdk : d k = -((I.card - 1 : ℝ) * c) := by linarith
  rw [← hs, hdk]
  ring

#print axioms centered_sum
#print axioms zero_sum_bound
#print axioms deviation_bound
#print axioms equality_when_others_equal
end
end PaperToLean.Samuelson

Lean 4.33.1
Dependencies: Mathlib 4.33.1 (see bundled lake-manifest.json)
File: Samuelson.lean
SHA-256: 3ef63aaa63fb8c1ea6b6af91111ca1a9a3eaa7c53cf7b0e097f5d211d620f43f
Result: passed

'PaperToLean.Samuelson.centered_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Samuelson.zero_sum_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Samuelson.deviation_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Samuelson.equality_when_others_equal' depends on axioms: [propext, Classical.choice, Quot.sound]

Run it

Install Lean with elan and Git. Download the project ZIP, extract it, and run these commands in that folder. The first command downloads the pinned Mathlib dependencies.

python3 prepare.py
lake env lean -DwarningAsError=true Samuelson.lean

A successful check prints the axiom dependencies and exits without errors.