TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Influence function for a regular M-location functional

Statement

Let $F$ be a Borel probability law on $R$ , let $ψ : R \to R$ be $C^{1}$ , and let $θ \in R$ satisfy

$J (θ) : = \int ψ (y - θ) d F (y) = 0.$

Assume $\int ∣ ψ (y - θ) ∣ d F (y) < \infty$ and that there is an open interval $I$ containing $θ$ and a nonnegative $g \in L^{1} (F)$ such that $∣ ψ^{'} (y - t) ∣ \leq g (y)$ for $F$ -almost every $y$ and every $t \in I$ . Put $A : = \int ψ^{'} (y - θ) d F (y)$ and assume $A \neq 0$ . For each fixed $x \in R$ , let $θ_{x} (ϵ)$ be the locally unique root near $θ$ of

$\int ψ (y - t) d F_{ϵ, x} (y) = 0, F_{ϵ, x} = (1 - ϵ) F + ϵ δ_{x} .$

Then, for all sufficiently small $ϵ \geq 0$ , this local root exists and

$IF (x; T, F) = \lim_{ϵ ↓ 0} \frac{θ_{x} (ϵ) - θ}{ϵ} = \frac{ψ (x - θ)}{A} .$

Here $T (F_{ϵ, x})$ denotes this local root. In the special case $ψ (u) = u$ and $F$ has a finite first absolute moment, $θ = μ : = \int y d F (y)$ and $IF (x; T, F) = x - μ$ .

Facts & Assumptions

Given: The law $F$ , the function $ψ$ , the root $θ$ , the open interval $I$ , the integrable derivative majorant $g$ , and $A \neq 0$ as in the Statement. Fix one contamination point $x \in R$ .

[F1]

Gross-error contamination path: for $0 \leq ϵ \leq 1$ , $F_{ϵ, x} = (1 - ϵ) F + ϵ δ_{x}$ is the point-contamination specialization of the gross-error path.

[F2]

Dominated convergence: pointwise almost-everywhere convergence under one integrable majorant permits passing limits through the integral.

[F3]

The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ : for a differentiable real function, a difference quotient over an interval equals a derivative at an intermediate point.

[F4]

The Euclidean implicit function theorem with derivative formula: if $H (e, t)$ is $C^{1}$ , $H (0, θ) = 0$ , and $\partial_{t} H (0, θ) \neq 0$ , then a unique local $C^{1}$ root $t = θ (e)$ exists and $θ^{'} (0) = - \partial_{e} H (0, θ) / \partial_{t} H (0, θ)$ .

[F5]

Statistical functionals and gross-error influence functions: the gross-error influence function is the right derivative of $T (F_{ϵ, x})$ at $ϵ = 0$ , when finite.

[A1]

For the mean specialization, $\int ∣ y ∣ d F (y) < \infty$ .

Proof

technique · direct

1.1givenF2F3

For $t \in I$ , the mean value theorem [F3] gives $∣ ψ (y - t) - ψ (y - θ) ∣ \leq ∣ t - θ ∣ g (y)$ for $F$ -almost every $y$ , so $J (t)$ is finite. For any $t \in I$ and nonzero $h$ with $t + h \in I$ , the difference quotient of $ψ (y - t)$ in $t$ converges pointwise to $- ψ^{'} (y - t)$ and is bounded in absolute value by $g (y)$ , again by [F3]. Dominated convergence [F2] therefore gives $J^{'} (t) = - \int ψ^{'} (y - t) d F (y)$ . If $t_{j} \to t$ in $I$ , continuity of $ψ^{'}$ gives pointwise convergence of $ψ^{'} (y - t_{j})$ to $ψ^{'} (y - t)$ , and the same majorant with [F2] shows $J^{'} (t_{j}) \to J^{'} (t)$ . Thus $J$ is $C^{1}$ on $I$ .

2.1givenF1F4step 1.1

Define $H_{x} (e, t) : = (1 - e) J (t) + e ψ (x - t)$ for real $e$ near $0$ and $t \in I$ . By step 1.1 and $ψ \in C^{1}$ , $H_{x}$ is $C^{1}$ ; also $H_{x} (0, θ) = 0$ and $\partial_{t} H_{x} (0, θ) = J^{'} (θ) = - A \neq 0$ . Applying [F4] gives a unique local $C^{1}$ root $t = θ_{x} (e)$ through $(0, θ)$ . For $e \geq 0$ small, [F1] identifies its equation with the stated M-location equation under $F_{e, x}$ .

3.1F4F5givenstep 2.1algebra

At $(0, θ)$ , $\partial_{e} H_{x} = ψ (x - θ) - J (θ) = ψ (x - θ)$ and $\partial_{t} H_{x} = - A$ . The derivative formula in [F4] therefore yields $θ_{x}^{'} (0) = ψ (x - θ) / A$ . Since a two-sided derivative implies the same right derivative, [F5] identifies this value with $IF (x; T, F)$ .

4.1A1step 3.1algebra∎

If $ψ (u) = u$ , then $J (t) = \int y d F (y) - t = μ - t$ , so its unique root is $θ = μ$ and $A = \int 1 d F = 1$ . Substitution in step 3.1 gives $IF (x; T, F) = x - μ$ .

Remarks

The argument is pointwise in $x$ : the implicit-function neighborhood and the remainder are not asserted to be uniform over contamination points. No Axiom of Choice is used.

Depends on

Used by

The mean has unbounded influence and 1/n breakdown Example

Dependency tree · two levels

32 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

P. B. Stark, Statistics 240 Lecture Notes, Part 9: Robustness and Related Topics, §1.4, PDF pp. 17–19 (standard reference, not scraped)
Elvezio Ronchetti, Introduction to Robust Statistics, slides 24–25 (standard reference, not scraped)