U-statistics

DefinitionU-statistic#✓fully proved

The U-statistic with kernel h of degree m on a sample x of size n: the average of h (x ∘ f) over the n.descFactorial m injective maps f : Fin m ↪ Fin n. For m > n there are no such maps and the value is 0 (Lean's a / 0 = 0).

noncomputable def uStatistic {m n : ℕ} (h : (Fin m → α) → ℝ) (x : Fin n → α) : ℝ :=
  (∑ f : Fin m ↪ Fin n, h (x ∘ f)) / n.descFactorial m

Used by 3

Used byHoeffding's central limit theorem · Unbiasedness · Hoeffding's variance formula

DefinitionHoeffding projection of a kernel#✓fully proved

Hoeffding's c-th projection of a kernel h of degree m under μ: h_c(y) = E h(y₁, …, y_c, X_{c+1}, …, X_m) with X_{c+1}, …, X_m i.i.d. μ.

noncomputable def hoeffdingProj (μ : Measure α) {m : ℕ} (h : (Fin m → α) → ℝ) (c : ℕ)
    (y : Fin c → α) : ℝ :=
  ∫ z : Fin (m - c) → α,
    h (fun j => if hj : (j : ℕ) < c then y ⟨j, hj⟩ else z ⟨j - c, by have := j.isLt; omega⟩)
    ∂(Measure.pi fun _ => μ)

Used by 2

Used byHoeffding's central limit theorem · Hoeffding's variance formula

TheoremUnbiasedness#✓fully proved

For an i.i.d. sample of size n ≥ m and an integrable kernel, the U-statistic has mean E h(X₁, …, X_m).

theorem integral_uStatistic {m n : ℕ} (hmn : m ≤ n) (μ : Measure α) [IsProbabilityMeasure μ]
    {h : (Fin m → α) → ℝ} (hh : Integrable h (Measure.pi fun _ => μ)) :
    ∫ x, uStatistic h x ∂(Measure.pi fun _ : Fin n => μ) =
      ∫ y, h y ∂(Measure.pi fun _ => μ)

Uses 1

Statement usesU-statistic

TheoremHoeffding's variance formula#✓fully proved

Hoeffding's variance formula (1948, §5): for an i.i.d. sample of size n ≥ m and a symmetric square-integrable kernel h of degree m, Var U = C(n, m)⁻¹ ∑_{c=1}^{m} C(m, c) C(n - m, m - c) Var h_c.

theorem variance_uStatistic {m n : ℕ} (hmn : m ≤ n) (μ : Measure α) [IsProbabilityMeasure μ]
    {h : (Fin m → α) → ℝ} (hsymm : ∀ (σ : Equiv.Perm (Fin m)) y, h (y ∘ σ) = h y)
    (hh : MemLp h 2 (Measure.pi fun _ => μ)) :
    Var[uStatistic h; Measure.pi fun _ : Fin n => μ] =
      (∑ c ∈ Finset.Icc 1 m, (m.choose c : ℝ) * ((n - m).choose (m - c) : ℝ) *
        Var[hoeffdingProj μ h c; Measure.pi fun _ : Fin c => μ]) / n.choose m

Uses 2

Statement usesHoeffding projection of a kernel · U-statistic

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.