Samplinglib mathematical lesson

Integrate the quadratic potential before taking the remainder

AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticFeatureRisk.quadratic_feature_mean_calculus · theorem · Teaching coverage

Read this first

Mathematical statement

Let W be measurable and H a complete real inner-product space. Let mu and nu be arbitrary measures, feature:W→H Bochner integrable under each, and y in H. Put m=integral feature dmu, n=integral feature dnu and V(q)=2 inner(m-y,feature(q)). Then V is integrable under both measures. With D=integral V dnu-integral V dmu, one has D=2 inner(m-y,n-m), ||n-y||²-||m-y||²-D=||n-m||², and ||m-y||²+D≤||n-y||². The real function t↦||m+t(n-m)-y||² has derivative D at zero. No probability, finite-mass or equal-mass hypothesis is imposed: m and n are unnormalized integrals.

\[D=\int Vd\nu-\int Vd\mu=2\langle m-y,n-m\rangle,\qquad \|n-y\|^2-\|m-y\|^2-D=\|n-m\|^2.\]

Lean statement · quadratic_feature_mean_calculus

Let W be measurable and H a complete real inner-product space. Let mu and nu be arbitrary measures, feature:W->H Bochner integrable under each, and y in H. Put m=integral feature dmu, n=integral feature dnu and V(q)=2 inner(m-y,feature(q)). Then V is integrable under both measures. With D=integral V dnu-integral V dmu, one has D=2 inner(m-y,n-m), ||n-y||²-||m-y||²-D=||n-m||², and ||m-y||²+D<=||n-y||². The real function t↦||m+t(n-m)-y||² has derivative D at zero. No probability, finite-mass or equal-mass hypothesis is imposed: m and n are unnormalized integrals.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)

theorem quadratic_feature_mean_calculus
    {W H : Type*} [MeasurableSpace W]
    [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (μ ν : Measure W) (feature : W → H) (label : H)
    (hμ : Integrable feature μ) (hν : Integrable feature ν) :
    let m : H := ∫ w, feature w ∂μ
    let n : H := ∫ w, feature w ∂ν
    let potential : W → ℝ := fun w => 2 * ⟪m - label, feature w⟫_ℝ
    Integrable potential μ ∧ Integrable potential ν ∧
    ((∫ w, potential w ∂ν) - (∫ w, potential w ∂μ) =
      2 * ⟪m - label, n - m⟫_ℝ) ∧
    (‖n - label‖ ^ 2 - ‖m - label‖ ^ 2 -
      ((∫ w, potential w ∂ν) - (∫ w, potential w ∂μ)) = ‖n - m‖ ^ 2) ∧
    (‖m - label‖ ^ 2 + ((∫ w, potential w ∂ν) - (∫ w, potential w ∂μ)) ≤
      ‖n - label‖ ^ 2) ∧
    HasDerivAt (fun t : ℝ => ‖m + t • (n - m) - label‖ ^ 2)
      ((∫ w, potential w ∂ν) - (∫ w, potential w ∂μ)) 0

Exact module and namespace context

Proof roadmap

1Produce scalar potential integrability
Pairing the actual feature with a fixed Hilbert vector is a continuous linear functional. It preserves Bochner integrability under either measure.
2Commute each integral with the linear pairing
Subtract the two actual finite scalar integrals and use linearity in the second inner-product argument. Here eta is restricted to mu or nu, precisely the two supplied integrability domains.
3Expand the loss and use positivity
Expand n-y=(m-y)+(n-m); the leftover squared norm is nonnegative and yields the support inequality.
4Differentiate the literal affine Hilbert curve
Its residual derivative is n-m. The squared-norm chain rule gives precisely D at zero.

Full assumptions and notation

All objects and hypotheses

H is complete; the H-valued feature is genuinely Bochner integrable under both measures.
The fixed label is any vector. The measures may have unequal or infinite total mass.

Mathematical proof

1. Produce scalar potential integrability

Pairing the actual feature with a fixed Hilbert vector is a continuous linear functional. It preserves Bochner integrability under either measure.

\[V(q)=2\langle m-y,\Phi(q)\rangle\in L^1(\mu)\cap L^1(\nu).\]

Corresponding Lean step

The exact statement and proof are extracted from the adjacent compiled module; the mathematical step is explained here.

2. Commute each integral with the linear pairing

Subtract the two actual finite scalar integrals and use linearity in the second inner-product argument. Here eta is restricted to mu or nu, precisely the two supplied integrability domains.

\[\eta\in\{\mu,\nu\}:\quad\int Vd\eta=2\langle m-y,\int\Phi d\eta\rangle,\qquad D=2\langle m-y,n-m\rangle.\]

Corresponding Lean step

The exact statement and proof are extracted from the adjacent compiled module; the mathematical step is explained here.

3. Expand the loss and use positivity

Expand n-y=(m-y)+(n-m); the leftover squared norm is nonnegative and yields the support inequality.

\[\|n-y\|^2=\|m-y\|^2+D+\|n-m\|^2.\]

Corresponding Lean step

The exact statement and proof are extracted from the adjacent compiled module; the mathematical step is explained here.

4. Differentiate the literal affine Hilbert curve

Its residual derivative is n-m. The squared-norm chain rule gives precisely D at zero.

\[\frac d{dt}\|m+t(n-m)-y\|^2\big|_{t=0}=D.\]

Corresponding Lean step

The exact statement and proof are extracted from the adjacent compiled module; the mathematical step is explained here.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · quadratic_feature_mean_calculus

See the adjacent exact Lean and the mathematical proof steps.

Download module (.lean)

theorem quadratic_feature_mean_calculus
    {W H : Type*} [MeasurableSpace W]
    [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (μ ν : Measure W) (feature : W → H) (label : H)
    (hμ : Integrable feature μ) (hν : Integrable feature ν) :
    let m : H := ∫ w, feature w ∂μ
    let n : H := ∫ w, feature w ∂ν
    let potential : W → ℝ := fun w => 2 * ⟪m - label, feature w⟫_ℝ
    Integrable potential μ ∧ Integrable potential ν ∧
    ((∫ w, potential w ∂ν) - (∫ w, potential w ∂μ) =
      2 * ⟪m - label, n - m⟫_ℝ) ∧
    (‖n - label‖ ^ 2 - ‖m - label‖ ^ 2 -
      ((∫ w, potential w ∂ν) - (∫ w, potential w ∂μ)) = ‖n - m‖ ^ 2) ∧
    (‖m - label‖ ^ 2 + ((∫ w, potential w ∂ν) - (∫ w, potential w ∂μ)) ≤
      ‖n - label‖ ^ 2) ∧
    HasDerivAt (fun t : ℝ => ‖m + t • (n - m) - label‖ ^ 2)
      ((∫ w, potential w ∂ν) - (∫ w, potential w ∂μ)) 0 := by
  dsimp only
  let m : H := ∫ w, feature w ∂μ
  let n : H := ∫ w, feature w ∂ν
  let potential : W → ℝ := fun w => 2 * ⟪m - label, feature w⟫_ℝ
  change Integrable potential μ ∧ Integrable potential ν ∧ _
  have hpotμ : Integrable potential μ :=
    (Integrable.const_inner (m - label) hμ).const_mul 2
  have hpotν : Integrable potential ν :=
    (Integrable.const_inner (m - label) hν).const_mul 2
  have hpμ : (∫ w, potential w ∂μ) = 2 * ⟪m - label, m⟫_ℝ := by
    dsimp only [potential, m]
    rw [integral_const_mul, integral_inner hμ]
  have hpν : (∫ w, potential w ∂ν) = 2 * ⟪m - label, n⟫_ℝ := by
    dsimp only [potential, n]
    rw [integral_const_mul, integral_inner hν]
  have hpair : (∫ w, potential w ∂ν) - (∫ w, potential w ∂μ) =
      2 * ⟪m - label, n - m⟫_ℝ := by
    rw [hpν, hpμ, inner_sub_right]
    ring
  have hbre : ‖n - label‖ ^ 2 - ‖m - label‖ ^ 2 -
      ((∫ w, potential w ∂ν) - (∫ w, potential w ∂μ)) = ‖n - m‖ ^ 2 := by
    rw [hpair]
    have hsplit : n - label = (m - label) + (n - m) := by abel
    rw [hsplit, norm_add_sq_real]
    ring
  refine ⟨hpotμ, hpotν, hpair, hbre, ?_, ?_⟩
  · linarith [sq_nonneg ‖n - m‖]
  · rw [hpair]
    have hcurve : HasDerivAt (fun t : ℝ => m + t • (n - m) - label) (n - m) 0 := by
      have hsmul : HasDerivAt (fun t : ℝ => t • (n - m)) (n - m) 0 := by
        simpa only [one_smul, id_eq] using (hasDerivAt_id (0 : ℝ)).smul_const (n - m)
      have hadd : HasDerivAt (fun t : ℝ => m + t • (n - m)) (n - m) 0 :=
        hsmul.const_add m
      exact hadd.sub_const label
    simpa only [zero_smul, add_zero] using hcurve.norm_sq

Exact module and namespace context

Scope and omitted-condition boundaries

No identification of a pointwise statistical predictor with this Bochner mean is supplied.
The affine Hilbert derivative is not by itself a probability-measure-segment first variation.
For arbitrary measures, adding a constant to V need not preserve D.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Integrable.const_inner
Integrable.const_mul
integral_const_mul
integral_inner
inner_sub_right
norm_add_sq_real
HasDerivAt.norm_sq

Mathematical sources

Samplinglib quadratic feature-risk supplement, version1 (2026-10-20) (historical source) — Original library derivation from the explicitly listed Mathlib facts; not attributed to a theorem of the chapter source.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.