Bias and mean squared error of estimators

DefinitionBias of an estimator#✓fully proved

Let \(S\) be a measurable space, \(W : S \to \mathbb{R}\) an estimator, \(\mu\) a probability measure on \(S\) for which \(W\) is integrable, and \(\theta \in \mathbb{R}\) a target. The bias of \(W\) under \(\mu\) at \(\theta\) is \(\int_S W \, d\mu - \theta\), the expected value of \(W\) under \(\mu\) minus \(\theta\).

Integrability of \(W\) is part of the input: it is the domain on which the expectation exists in the source (Chapter 2, Definition 2.2.1), so a nonintegrable estimator has no finite bias.

noncomputable def bias (W : S → ℝ) (μ : ProbabilityMeasure S) (θ : ℝ)
    (_hW : Integrable W (μ : Measure S)) : ℝ :=
  ∫ x, W x ∂(μ : Measure S) - θ

Sources

• blueprint af_723199a7ca6fb3e936a73618.

Used by 5

Used byBias as an integral · Family bias of an estimator · Bias–variance decomposition of the mean squared error · Mean squared error of an unbiased estimator · Bias–variance decomposition of the extended mean squared error

TheoremBias as an integral#✓fully proved

Let \(S\) be a measurable space, \(W : S \to \mathbb{R}\) an estimator, \(\mu\) a probability measure on \(S\) for which \(W\) is integrable, and \(\theta \in \mathbb{R}\) a target. Then the bias of \(W\) under \(\mu\) at \(\theta\) equals \(\int_S W \, d\mu - \theta\).

@[simp]
theorem bias_eq_integral (W : S → ℝ) (μ : ProbabilityMeasure S) (θ : ℝ)
    (hW : Integrable W (μ : Measure S)) :
    bias W μ θ hW = ∫ x, W x ∂(μ : Measure S) - θ

Sources

• blueprint af_723199a7ca6fb3e936a73618.

Uses 1

Statement usesBias of an estimator

DefinitionMean squared error#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(S\), let \(W : S \to \mathbb{R}\) be an estimator and \(\theta \in \mathbb{R}\) a target value, and suppose the squared error \(x \mapsto (W(x) - \theta)^2\) is \(\mu\)-integrable. The mean squared error of \(W\) at \(\theta\) under \(\mu\) is the real number \(\int_S (W(x) - \theta)^2 \, d\mu(x)\).

The integrability hypothesis is part of the definition: without it no finite mean squared error is defined.

noncomputable def meanSquaredError (W : S → ℝ) (μ : ProbabilityMeasure S)
    (θ : ℝ)
    (_hW2 : Integrable (fun x => (W x - θ) ^ 2) (μ : Measure S)) : ℝ :=
  ∫ x, (W x - θ) ^ 2 ∂(μ : Measure S)

Sources

• Casella–Berger, Definition 7.3.1; blueprint af_fd40353442120bd19166139d.

Used by 8

Used byThe mean minimizes the expected squared loss · Family mean squared error of an estimator · Mean squared error as an integral · Bias–variance decomposition of the mean squared error · Mean squared error as variance plus squared mean deviation · Mean squared error of an unbiased estimator · Finite and extended mean squared error agree · Bias–variance decomposition of the extended mean squared error

TheoremMean squared error as an integral#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(S\), let \(W : S \to \mathbb{R}\) and \(\theta \in \mathbb{R}\), and suppose the squared error \(x \mapsto (W(x) - \theta)^2\) is \(\mu\)-integrable. Then the mean squared error of \(W\) at \(\theta\) under \(\mu\) equals \(\int_S (W(x) - \theta)^2 \, d\mu(x)\).

@[simp]
theorem meanSquaredError_eq_integral (W : S → ℝ) (μ : ProbabilityMeasure S)
    (θ : ℝ)
    (hW2 : Integrable (fun x => (W x - θ) ^ 2) (μ : Measure S)) :
    meanSquaredError W μ θ hW2 = ∫ x, (W x - θ) ^ 2 ∂(μ : Measure S)

Sources

• blueprint af_fd40353442120bd19166139d.

Uses 1

Statement usesMean squared error

DefinitionExtended mean squared error#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(S\), let \(W : S \to \mathbb{R}\) be an estimator and let \(\theta \in \mathbb{R}\) be a target value. The extended mean squared error of \(W\) at \(\theta\) under \(\mu\) is the (lower) Lebesgue integral \(\int_S (W(x) - \theta)^2 \, d\mu(x)\) of the nonnegative squared error, computed in \([0, \infty]\). It is defined for every \(W\), with no integrability hypothesis.

When the squared error is \(\mu\)-integrable, this value is finite and equals the mean squared error; when the squared error is almost everywhere strongly measurable but not \(\mu\)-integrable, it equals \(\infty\).

noncomputable def meanSquaredErrorENN (W : S → ℝ) (μ : ProbabilityMeasure S)
    (θ : ℝ) : ℝ≥0∞ :=
  ∫⁻ x, ENNReal.ofReal ((W x - θ) ^ 2) ∂(μ : Measure S)

Sources

• blueprint af_fd40353442120bd19166139d.

Used by 3

Used byExtended mean squared error of a measurable non-integrable squared error is infinite · Finite and extended mean squared error agree · Bias–variance decomposition of the extended mean squared error

TheoremFinite and extended mean squared error agree#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(S\), let \(W : S \to \mathbb{R}\) and \(\theta \in \mathbb{R}\), and suppose the squared error \(x \mapsto (W(x) - \theta)^2\) is \(\mu\)-integrable. Then the extended mean squared error \(\int_S (W(x) - \theta)^2 \, d\mu(x)\), computed in \([0, \infty]\), is finite and equals the mean squared error of \(W\) at \(\theta\) under \(\mu\).

theorem ofReal_meanSquaredError {W : S → ℝ} {μ : ProbabilityMeasure S}
    {θ : ℝ}
    (h : Integrable (fun x => (W x - θ) ^ 2) (μ : Measure S)) :
    ENNReal.ofReal (meanSquaredError W μ θ h) = meanSquaredErrorENN W μ θ

Sources

• blueprint af_fd40353442120bd19166139d.

Uses 2 · Used by 1

Statement usesMean squared error · Extended mean squared error

Used byBias–variance decomposition of the extended mean squared error

TheoremExtended mean squared error of a measurable non-integrable squared error is infinite#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(S\), \(W : S \to \mathbb{R}\) an estimator and \(\theta \in \mathbb{R}\). If the squared error \(x \mapsto (W(x) - \theta)^2\) is almost everywhere strongly measurable with respect to \(\mu\) but not \(\mu\)-integrable, then the extended mean squared error \(\int_S (W(x) - \theta)^2 \, d\mu(x) \in [0, \infty]\) of \(W\) at \(\theta\) equals \(\infty\).

theorem meanSquaredErrorENN_eq_top_of_not_finite {W : S → ℝ}
    {μ : ProbabilityMeasure S} {θ : ℝ}
    (hm : AEStronglyMeasurable (fun x => (W x - θ) ^ 2) (μ : Measure S))
    (h : ¬ Integrable (fun x => (W x - θ) ^ 2) (μ : Measure S)) :
    meanSquaredErrorENN W μ θ = ∞

Sources

• blueprint af_fd40353442120bd19166139d.

Uses 1

Statement usesExtended mean squared error

DefinitionFamily bias of an estimator#✓fully proved

Let \(S\) be a measurable space, \(W : S \to \mathbb{R}\) an estimator, \((P_\theta)_{\theta \in \Theta}\) a family of probability measures on \(S\) such that \(W\) is integrable for every \(P_\theta\), and \(\tau : \Theta \to \mathbb{R}\) a target function. The family bias of \(W\) is the function on \(\Theta\) whose value at \(\theta\) is the bias of \(W\) under \(P_\theta\) at the target \(\tau(\theta)\), that is, \(\int_S W \, dP_\theta - \tau(\theta)\).

The estimator \(W\) is fixed before the family and does not depend on \(\theta\).

noncomputable def familyBias {Θ : Type*} (W : S → ℝ)
    (P : Θ → ProbabilityMeasure S) (τ : Θ → ℝ)
    (h : ∀ θ, Integrable W ((P θ) : Measure S)) : Θ → ℝ :=
  fun θ => bias W (P θ) (τ θ) (h θ)

Sources

• blueprint af_723199a7ca6fb3e936a73618.

Uses 1 · Used by 4

Statement usesBias of an estimator

Used byFamily bias as an integral · An unbiased estimator has mean squared error equal to its variance · Bias–variance decomposition for a parametric family · An estimator is unbiased exactly when its bias vanishes

TheoremFamily bias as an integral#✓fully proved

Let \(S\) be a measurable space, \(W : S \to \mathbb{R}\) an estimator, \((P_\theta)_{\theta \in \Theta}\) a family of probability measures on \(S\) such that \(W\) is integrable for every \(P_\theta\), and \(\tau : \Theta \to \mathbb{R}\) a target function. Then for every \(\theta \in \Theta\) the family bias of \(W\) at \(\theta\) equals \(\int_S W \, dP_\theta - \tau(\theta)\).

@[simp]
theorem familyBias_apply {Θ : Type*} (W : S → ℝ)
    (P : Θ → ProbabilityMeasure S) (τ : Θ → ℝ)
    (h : ∀ θ, Integrable W ((P θ) : Measure S)) (θ : Θ) :
    familyBias W P τ h θ = ∫ x, W x ∂((P θ) : Measure S) - τ θ

Sources

• blueprint af_723199a7ca6fb3e936a73618.

Uses 1

Statement usesFamily bias of an estimator

DefinitionFamily mean squared error of an estimator#✓fully proved

Let \(S\) be a measurable space, \(W : S \to \mathbb{R}\) an estimator, \((P_\theta)_{\theta \in \Theta}\) a family of probability measures on \(S\) and \(\tau : \Theta \to \mathbb{R}\) a target function such that \((W - \tau(\theta))^2\) is integrable for \(P_\theta\) for every \(\theta \in \Theta\). The family mean squared error of \(W\) is the function on \(\Theta\) whose value at \(\theta\) is the mean squared error of \(W\) under \(P_\theta\) at the target \(\tau(\theta)\), that is, \(\int_S (W(x) - \tau(\theta))^2 \, dP_\theta(x)\).

The estimator \(W\) is fixed before the family and does not depend on \(\theta\).

noncomputable def familyMeanSquaredError {Θ : Type*} (W : S → ℝ)
    (P : Θ → ProbabilityMeasure S) (τ : Θ → ℝ)
    (h : ∀ θ, Integrable (fun x => (W x - τ θ) ^ 2) ((P θ) : Measure S)) :
    Θ → ℝ :=
  fun θ => meanSquaredError W (P θ) (τ θ) (h θ)

Sources

• blueprint af_fd40353442120bd19166139d.

Uses 1 · Used by 4

Statement usesMean squared error

Used byFamily mean squared error as an integral · An unbiased estimator has mean squared error equal to its variance · Bias–variance decomposition for a parametric family · Mean squared error is frequentist risk under squared-error loss

TheoremFamily mean squared error as an integral#✓fully proved

Let \(S\) be a measurable space, \(W : S \to \mathbb{R}\) an estimator, \((P_\theta)_{\theta \in \Theta}\) a family of probability measures on \(S\) and \(\tau : \Theta \to \mathbb{R}\) a target function such that \((W - \tau(\theta))^2\) is integrable for \(P_\theta\) for every \(\theta \in \Theta\). Then for every \(\theta \in \Theta\) the family mean squared error of \(W\) at \(\theta\) equals \(\int_S (W(x) - \tau(\theta))^2 \, dP_\theta(x)\).

@[simp]
theorem familyMeanSquaredError_apply {Θ : Type*} (W : S → ℝ)
    (P : Θ → ProbabilityMeasure S) (τ : Θ → ℝ)
    (h : ∀ θ, Integrable (fun x => (W x - τ θ) ^ 2) ((P θ) : Measure S))
    (θ : Θ) :
    familyMeanSquaredError W P τ h θ =
      ∫ x, (W x - τ θ) ^ 2 ∂((P θ) : Measure S)

Sources

• blueprint af_fd40353442120bd19166139d.

Uses 1

Statement usesFamily mean squared error of an estimator

DefinitionUnbiased estimator#✓fully proved

Let \((P_\theta)_{\theta \in \Theta}\) be a family of probability measures on a measurable space \(S\) and \(\tau : \Theta \to \mathbb{R}\) a target function. An estimator \(W : S \to \mathbb{R}\) is unbiased for \(\tau\) if for every \(\theta \in \Theta\) the function \(W\) is \(P_\theta\)-integrable and \(\int_S W \, dP_\theta = \tau(\theta)\).

Integrability is part of the definition, so a non-integrable estimator is never unbiased. The estimator \(W\) is fixed and does not depend on \(\theta\).

def IsUnbiased {Θ : Type*} (W : S → ℝ) (P : Θ → ProbabilityMeasure S)
    (τ : Θ → ℝ) : Prop :=
  ∀ θ, Integrable W ((P θ) : Measure S) ∧
    ∫ x, W x ∂((P θ) : Measure S) = τ θ

Sources

• Casella–Berger Definition 7.3.2 is the case \(\tau(\theta) = \theta\) on real parameters; the general target follows section 7.3.2. Blueprint af_95118d196fd6478105a6eb43.

Used by 4

Used byAn unbiased estimator has the target as its expectation · An unbiased estimator has mean squared error equal to its variance · Unbiased estimators are integrable · An estimator is unbiased exactly when its bias vanishes

TheoremUnbiased estimators are integrable#✓fully proved

Let \((P_\theta)_{\theta \in \Theta}\) be a family of probability measures on \(S\) and \(\tau : \Theta \to \mathbb{R}\) a target function. If an estimator \(W : S \to \mathbb{R}\) is unbiased for \(\tau\), then \(W\) is \(P_\theta\)-integrable for every \(\theta \in \Theta\).

theorem IsUnbiased.integrable {Θ : Type*} {W : S → ℝ}
    {P : Θ → ProbabilityMeasure S} {τ : Θ → ℝ} (h : IsUnbiased W P τ)
    (θ : Θ) : Integrable W ((P θ) : Measure S)

Uses 1

Statement usesUnbiased estimator

TheoremAn unbiased estimator has the target as its expectation#✓fully proved

Let \(S\) be a measurable space, \(W : S \to \mathbb{R}\) an estimator, \((P_\theta)_{\theta \in \Theta}\) a family of probability measures on \(S\) and \(\tau : \Theta \to \mathbb{R}\) a target function. If \(W\) is unbiased for \(\tau\) under the family \((P_\theta)\), then \(\int_S W \, dP_\theta = \tau(\theta)\) for every \(\theta \in \Theta\).

theorem IsUnbiased.expect_eq {Θ : Type*} {W : S → ℝ}
    {P : Θ → ProbabilityMeasure S} {τ : Θ → ℝ} (h : IsUnbiased W P τ)
    (θ : Θ) : ∫ x, W x ∂((P θ) : Measure S) = τ θ

Uses 1 · Used by 1

Statement usesUnbiased estimator

Used byAn unbiased estimator has mean squared error equal to its variance

TheoremAn estimator is unbiased exactly when its bias vanishes#✓fully proved

Let \((P_\theta)_{\theta \in \Theta}\) be a family of probability measures on \(S\), \(\tau : \Theta \to \mathbb{R}\) a target function, and \(W : S \to \mathbb{R}\) an estimator that is \(P_\theta\)-integrable for every \(\theta \in \Theta\). Then \(W\) is unbiased for \(\tau\) if and only if its family bias \(\int_S W \, dP_\theta - \tau(\theta)\) is zero for every \(\theta \in \Theta\).

theorem isUnbiased_iff_forall_familyBias_eq_zero {Θ : Type*} {W : S → ℝ}
    {P : Θ → ProbabilityMeasure S} {τ : Θ → ℝ}
    (h : ∀ θ, Integrable W ((P θ) : Measure S)) :
    IsUnbiased W P τ ↔ ∀ θ, familyBias W P τ h θ = 0

Uses 2

Statement usesUnbiased estimator · Family bias of an estimator

TheoremA finite second moment makes the squared error integrable#✓fully proved

Let \(\mu\) be a probability measure on \(S\) and \(W : S \to \mathbb{R}\) an estimator in \(L^2(\mu)\). Then for every \(\theta \in \mathbb{R}\) the squared error \(x \mapsto (W(x) - \theta)^2\) is \(\mu\)-integrable.

theorem integrable_sq_sub_of_memLp_two {W : S → ℝ} {μ : ProbabilityMeasure S}
    {θ : ℝ} (hW : MemLp W 2 ((μ : Measure S))) :
    Integrable (fun x => (W x - θ) ^ 2) ((μ : Measure S))

Used by 5

Used byThe mean minimizes the expected squared loss · Bias–variance decomposition of the mean squared error · Mean squared error as variance plus squared mean deviation · Mean squared error of an unbiased estimator · Bias–variance decomposition of the extended mean squared error

TheoremBias–variance decomposition of the mean squared error#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(S\), let \(\theta \in \mathbb{R}\), and let \(W : S \to \mathbb{R}\) be square-integrable with respect to \(\mu\), that is, \(W \in L^2(\mu)\). Then the mean squared error of \(W\) at \(\theta\) under \(\mu\) equals \(\operatorname{Var}_\mu(W) + b^2\), where \(b = \int_S W \, d\mu - \theta\) is the bias of \(W\) at \(\theta\) under \(\mu\).

The integrability that the mean squared error and the bias require follows from \(W \in L^2(\mu)\).

theorem meanSquaredError_eq_variance_add_sq_bias {W : S → ℝ}
    {μ : ProbabilityMeasure S} {θ : ℝ} (hW : MemLp W 2 ((μ : Measure S))) :
    meanSquaredError W μ θ (integrable_sq_sub_of_memLp_two hW) =
      ProbabilityTheory.variance W ((μ : Measure S)) +
        (bias W μ θ (hW.integrable one_le_two)) ^ 2

Sources

• Casella–Berger, equation (7.3.1); blueprint af_3a1bafba0b7dff99554b01f0.

Uses 3 · Used by 4

Statement usesBias of an estimator · A finite second moment makes the squared error integrable · Mean squared error

Used byBias–variance decomposition for a parametric family · Mean squared error as variance plus squared mean deviation · Mean squared error of an unbiased estimator · Bias–variance decomposition of the extended mean squared error

TheoremMean squared error as variance plus squared mean deviation#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(S\), let \(\theta \in \mathbb{R}\), and let \(W : S \to \mathbb{R}\) be square-integrable with respect to \(\mu\), that is, \(W \in L^2(\mu)\). Then the mean squared error of \(W\) at \(\theta\) under \(\mu\) equals \(\operatorname{Var}_\mu(W) + \left(\int_S W \, d\mu - \theta\right)^2\).

theorem meanSquaredError_eq_variance_add_sq_expectation_sub {W : S → ℝ}
    {μ : ProbabilityMeasure S} {θ : ℝ} (hW : MemLp W 2 ((μ : Measure S))) :
    meanSquaredError W μ θ (integrable_sq_sub_of_memLp_two hW) =
      ProbabilityTheory.variance W ((μ : Measure S)) +
        ((∫ x, W x ∂((μ : Measure S))) - θ) ^ 2

Sources

• Casella–Berger, equation (7.3.1) in expectation form; blueprint af_3a1bafba0b7dff99554b01f0.

Uses 3 · Used by 1

Statement usesA finite second moment makes the squared error integrable · Mean squared error

Proof usesBias–variance decomposition of the mean squared error

Used byThe mean minimizes the expected squared loss

TheoremBias–variance decomposition of the extended mean squared error#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(S\), let \(\theta \in \mathbb{R}\), and let \(W : S \to \mathbb{R}\) be square-integrable with respect to \(\mu\), that is, \(W \in L^2(\mu)\). Then the extended mean squared error \(\int_S (W(x) - \theta)^2 \, d\mu(x)\), computed in \([0, \infty]\), is finite and equals \(\operatorname{Var}_\mu(W) + b^2\), where \(b = \int_S W \, d\mu - \theta\) is the bias of \(W\) at \(\theta\) under \(\mu\).

theorem ofReal_variance_add_sq_bias {W : S → ℝ} {μ : ProbabilityMeasure S}
    {θ : ℝ} (hW : MemLp W 2 ((μ : Measure S))) :
    ENNReal.ofReal (ProbabilityTheory.variance W ((μ : Measure S)) +
          (bias W μ θ (hW.integrable one_le_two)) ^ 2) =
      meanSquaredErrorENN W μ θ

Uses 6

Statement usesBias of an estimator · Extended mean squared error

Proof usesA finite second moment makes the squared error integrable · Mean squared error · Bias–variance decomposition of the mean squared error · Finite and extended mean squared error agree

TheoremBias–variance decomposition for a parametric family#✓fully proved

Let \(S\) be a measurable space, \(W : S \to \mathbb{R}\) an estimator, \((P_\theta)_{\theta \in \Theta}\) a family of probability measures on \(S\) and \(\tau : \Theta \to \mathbb{R}\) a target function. Suppose that for every \(\theta \in \Theta\), \(W\) has a finite second moment under \(P_\theta\), and \(W\) and \((W - \tau(\theta))^2\) are integrable for \(P_\theta\). Then for every \(\theta \in \Theta\) the family mean squared error of \(W\) at \(\theta\) equals the variance \(\operatorname{Var}_{P_\theta}(W)\) of \(W\) under \(P_\theta\) plus the square of the family bias of \(W\) at \(\theta\).

theorem familyMeanSquaredError_eq_variance_add_sq_familyBias {Θ : Type*}
    {W : S → ℝ} {P : Θ → ProbabilityMeasure S} {τ : Θ → ℝ}
    (hMem : ∀ θ, MemLp W 2 (((P θ)) : Measure S))
    (h2 : ∀ θ, Integrable (fun x => (W x - τ θ) ^ 2) (((P θ)) : Measure S))
    (h1 : ∀ θ, Integrable W (((P θ)) : Measure S)) (θ : Θ) :
    familyMeanSquaredError W P τ h2 θ =
      ProbabilityTheory.variance W (((P θ)) : Measure S) +
        (familyBias W P τ h1 θ) ^ 2

Sources

• equation 7.3.1, in family form for a single fixed estimator.

Uses 3 · Used by 1

Statement usesFamily bias of an estimator · Family mean squared error of an estimator

Proof usesBias–variance decomposition of the mean squared error

Used byAn unbiased estimator has mean squared error equal to its variance

TheoremMean squared error of an unbiased estimator#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(S\), let \(\theta \in \mathbb{R}\), and let \(W : S \to \mathbb{R}\) be square-integrable with respect to \(\mu\) (that is, \(W \in L^2(\mu)\)) and satisfy \(\int_S W \, d\mu = \theta\). Then the mean squared error of \(W\) at \(\theta\) under \(\mu\) equals \(\operatorname{Var}_\mu(W)\).

theorem meanSquaredError_eq_variance_of_expect_eq {W : S → ℝ}
    {μ : ProbabilityMeasure S} {θ : ℝ} (hW : MemLp W 2 ((μ : Measure S)))
    (hunb : ∫ x, W x ∂((μ : Measure S)) = θ) :
    meanSquaredError W μ θ (integrable_sq_sub_of_memLp_two hW) =
      ProbabilityTheory.variance W ((μ : Measure S))

Sources

• the display following Definition 7.3.2.

Uses 4

Statement usesA finite second moment makes the squared error integrable · Mean squared error

Proof usesBias of an estimator · Bias–variance decomposition of the mean squared error

TheoremAn unbiased estimator has mean squared error equal to its variance#✓fully proved

Let \(S\) be a measurable space, \(W : S \to \mathbb{R}\) an estimator, \((P_\theta)_{\theta \in \Theta}\) a family of probability measures on \(S\) and \(\tau : \Theta \to \mathbb{R}\) a target function. Suppose that \(W\) is unbiased for \(\tau\) under the family, and that for every \(\theta \in \Theta\), \(W\) has a finite second moment under \(P_\theta\) and \((W - \tau(\theta))^2\) is integrable for \(P_\theta\). Then for every \(\theta \in \Theta\) the family mean squared error of \(W\) at \(\theta\) equals the variance \(\operatorname{Var}_{P_\theta}(W)\) of \(W\) under \(P_\theta\).

theorem IsUnbiased.familyMeanSquaredError_eq_variance {Θ : Type*} {W : S → ℝ}
    {P : Θ → ProbabilityMeasure S} {τ : Θ → ℝ} (hunb : IsUnbiased W P τ)
    (hMem : ∀ θ, MemLp W 2 (((P θ)) : Measure S))
    (h2 : ∀ θ, Integrable (fun x => (W x - τ θ) ^ 2) (((P θ)) : Measure S))
    (θ : Θ) :
    familyMeanSquaredError W P τ h2 θ =
      ProbabilityTheory.variance W (((P θ)) : Measure S)

Uses 5

Statement usesUnbiased estimator · Family mean squared error of an estimator

Proof usesAn unbiased estimator has the target as its expectation · Family bias of an estimator · Bias–variance decomposition for a parametric family

DefinitionFrequentist risk#✓fully proved

Let \(S\) be a measurable space, \(\delta : S \to A\) a decision rule, \((P_\theta)_{\theta \in \Theta}\) a family of probability measures on \(S\), and \(\ell : \Theta \times A \to [0, \infty)\) a loss such that \(x \mapsto \ell(\theta, \delta(x))\) is \(P_\theta\)-integrable for every \(\theta \in \Theta\). The frequentist risk of \(\delta\) is the function \(\Theta \to \mathbb{R}\) given by \(R(\theta, \delta) = \int_S \ell(\theta, \delta(x)) \, dP_\theta(x)\).

The rule \(\delta\) does not depend on \(\theta\), and the action space \(A\) may differ from \(\Theta\). No prior, kernel or optimality criterion enters.

noncomputable def frequentistRisk {Θ A : Type*} (δ : S → A)
    (P : Θ → ProbabilityMeasure S) (ℓ : Θ → A → NNReal)
    (_h : ∀ θ, Integrable (fun x => (ℓ θ (δ x) : ℝ)) ((P θ) : Measure S)) :
    Θ → ℝ :=
  fun θ => ∫ x, (ℓ θ (δ x) : ℝ) ∂((P θ) : Measure S)

Sources

• Casella–Berger equation 7.3.16; the integrability hypothesis is the expectation domain of Chapter 2 Definition 2.2.1. Blueprint af_36871388da7326a07a5e4f71.

Used by 4

Used byFrequentist risk as an integral · Frequentist risk is nonnegative · Mean squared error is frequentist risk under squared-error loss · Finite and extended frequentist risk agree

TheoremFrequentist risk as an integral#✓fully proved

Let \(S\) be a measurable space, \(\delta : S \to A\) a decision rule, \((P_\theta)_{\theta \in \Theta}\) a family of probability measures on \(S\) and \(\ell : \Theta \times A \to [0, \infty)\) a loss function such that \(x \mapsto \ell(\theta, \delta(x))\) is integrable for \(P_\theta\) for every \(\theta \in \Theta\). Then for every \(\theta \in \Theta\) the frequentist risk of \(\delta\) at \(\theta\) equals \(\int_S \ell(\theta, \delta(x)) \, dP_\theta(x)\).

theorem frequentistRisk_apply {Θ A : Type*} {δ : S → A}
    {P : Θ → ProbabilityMeasure S} {ℓ : Θ → A → NNReal}
    {h : ∀ θ, Integrable (fun x => (ℓ θ (δ x) : ℝ)) ((P θ) : Measure S)}
    (θ : Θ) :
    frequentistRisk δ P ℓ h θ =
      ∫ x, (ℓ θ (δ x) : ℝ) ∂((P θ) : Measure S)

Uses 1

Statement usesFrequentist risk

TheoremFrequentist risk is nonnegative#✓fully proved

Let \(\delta : S \to A\) be a decision rule, \((P_\theta)_{\theta \in \Theta}\) a family of probability measures on \(S\), and \(\ell : \Theta \times A \to [0, \infty)\) a loss such that \(x \mapsto \ell(\theta, \delta(x))\) is \(P_\theta\)-integrable for every \(\theta \in \Theta\). Then the frequentist risk \(R(\theta, \delta)\) of \(\delta\) at \(\theta\) is nonnegative for every \(\theta \in \Theta\).

theorem frequentistRisk_nonneg {Θ A : Type*} {δ : S → A}
    {P : Θ → ProbabilityMeasure S} {ℓ : Θ → A → NNReal}
    {h : ∀ θ, Integrable (fun x => (ℓ θ (δ x) : ℝ)) ((P θ) : Measure S)}
    (θ : Θ) : 0 ≤ frequentistRisk δ P ℓ h θ

Uses 1

Statement usesFrequentist risk

DefinitionExtended frequentist risk#✓fully proved

Let \(S\) be a measurable space, \(\delta : S \to A\) a decision rule, \((P_\theta)_{\theta \in \Theta}\) a family of probability measures on \(S\), and \(\ell : \Theta \times A \to [0, \infty)\) a loss. The extended frequentist risk of \(\delta\) at \(\theta \in \Theta\) is the Lebesgue integral \(\int_S \ell(\theta, \delta(x)) \, dP_\theta(x)\), taken in \([0, \infty]\).

When the loss is \(P_\theta\)-integrable for every \(\theta\), this is the frequentist risk; when it is measurable but not integrable at \(\theta\), it equals \(\infty\).

noncomputable def frequentistRiskENN {Θ A : Type*} (δ : S → A)
    (P : Θ → ProbabilityMeasure S) (ℓ : Θ → A → NNReal) (θ : Θ) : ℝ≥0∞ :=
  ∫⁻ x, ℓ θ (δ x) ∂((P θ) : Measure S)

Sources

• blueprint af_36871388da7326a07a5e4f71.

Used by 2

Used byExtended frequentist risk of a measurable non-integrable loss is infinite · Finite and extended frequentist risk agree

TheoremFinite and extended frequentist risk agree#✓fully proved

Let \(\Theta\) and \(A\) be sets, let \((P_\vartheta)_{\vartheta \in \Theta}\) be a family of probability measures on a measurable space \(S\), let \(\delta : S \to A\) be a decision rule and \(\ell : \Theta \times A \to [0, \infty)\) a loss, and suppose \(x \mapsto \ell(\vartheta, \delta(x))\) is \(P_\vartheta\)-integrable for every \(\vartheta \in \Theta\). Then for every \(\theta \in \Theta\) the extended frequentist risk \(\int_S \ell(\theta, \delta(x)) \, dP_\theta(x)\), computed in \([0, \infty]\), is finite and equals the frequentist risk of \(\delta\) at \(\theta\).

theorem ofReal_frequentistRisk {Θ A : Type*} {δ : S → A}
    {P : Θ → ProbabilityMeasure S} {ℓ : Θ → A → NNReal}
    {h : ∀ θ, Integrable (fun x => (ℓ θ (δ x) : ℝ)) ((P θ) : Measure S)}
    (θ : Θ) :
    ENNReal.ofReal (frequentistRisk δ P ℓ h θ) =
      frequentistRiskENN δ P ℓ θ

Sources

• blueprint af_36871388da7326a07a5e4f71.

Uses 2

Statement usesFrequentist risk · Extended frequentist risk

TheoremExtended frequentist risk of a measurable non-integrable loss is infinite#✓fully proved

Let \(S\) be a measurable space, \(\delta : S \to A\) a decision rule, \((P_\theta)_{\theta \in \Theta}\) a family of probability measures on \(S\), \(\ell : \Theta \times A \to [0, \infty)\) a loss, and \(\theta \in \Theta\). If the function \(x \mapsto \ell(\theta, \delta(x))\) is almost everywhere strongly measurable with respect to \(P_\theta\) but not \(P_\theta\)-integrable, then the extended frequentist risk \(\int_S \ell(\theta, \delta(x)) \, dP_\theta(x) \in [0, \infty]\) of \(\delta\) at \(\theta\) equals \(\infty\).

So a measurable non-integrable loss is never assigned a finite extended risk.

theorem frequentistRiskENN_eq_top_of_not_integrable {Θ A : Type*}
    {δ : S → A} {P : Θ → ProbabilityMeasure S} {ℓ : Θ → A → NNReal}
    {θ : Θ}
    (hm : AEStronglyMeasurable (fun x => (ℓ θ (δ x) : ℝ))
      ((P θ) : Measure S))
    (h : ¬ Integrable (fun x => (ℓ θ (δ x) : ℝ)) ((P θ) : Measure S)) :
    frequentistRiskENN δ P ℓ θ = ∞

Sources

• blueprint af_36871388da7326a07a5e4f71.

Uses 1

Statement usesExtended frequentist risk

TheoremMean squared error is frequentist risk under squared-error loss#✓fully proved

Let \((P_\theta)_{\theta \in \Theta}\) be a family of probability measures on \(S\), \(W : S \to \mathbb{R}\) an estimator and \(\tau : \Theta \to \mathbb{R}\) a target function such that \(x \mapsto (W(x) - \tau(\theta))^2\) is \(P_\theta\)-integrable for every \(\theta \in \Theta\). Then for every \(\theta\), the frequentist risk at \(\theta\) of \(W\), as a decision rule with actions in \(\mathbb{R}\), under the squared-error loss \(\ell(\theta, a) = (a - \tau(\theta))^2\) equals the family mean squared error of \(W\) for \(\tau\) at \(\theta\).

theorem frequentistRisk_squared_eq_familyMeanSquaredError {Θ : Type*}
    {W : S → ℝ} {P : Θ → ProbabilityMeasure S} {τ : Θ → ℝ}
    (hRisk : ∀ θ, Integrable
      (fun x => ((⟨(W x - τ θ) ^ 2, sq_nonneg _⟩ : NNReal) : ℝ))
      (((P θ)) : Measure S))
    (hMSE : ∀ θ, Integrable (fun x => (W x - τ θ) ^ 2) (((P θ)) : Measure S)) :
    frequentistRisk W P (fun θ a => ⟨(a - τ θ) ^ 2, sq_nonneg _⟩) hRisk =
      familyMeanSquaredError W P τ hMSE

Sources

• blueprint af_36871388da7326a07a5e4f71.

Uses 2

Statement usesFamily mean squared error of an estimator · Frequentist risk

29 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.