Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
Samplinglib mathematical lesson

Differentiate a moving feature and scale the risk

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

Read this first

Mathematical statement

Let H be a real inner-product normed space, with no completeness assumption. Let N be a positive natural number, lambda any real number, phi:R→H, and a,y,v in H. At a real time t assume the genuine derivative of phi is v. Then s↦||(a+phi(s))/N-y||² has derivative (2/N) inner((a+phi(t))/N-y,v) at t. Multiplying that risk by N/lambda gives derivative (2/lambda) times the same inner product. All divisions are real totalized divisions; lambda=0 is an algebraic zero-scaling case, not a temperature model.

\[R(s)=\|N^{-1}(a+\phi(s))-y\|^2,\quad R\prime(t)=\frac2N\langle N^{-1}(a+\phi(t))-y,v\rangle,\quad (NR/\lambda)\prime(t)=\frac2\lambda\langle N^{-1}(a+\phi(t))-y,v\rangle.\]
Lean statement · empirical_squared_feature_risk_derivatives

Let H be a real inner-product normed space, with no completeness assumption. Let N be a positive natural number, lambda any real number, phi:R->H, and a,y,v in H. At a real time t assume the genuine derivative of phi is v. Then s↦||(a+phi(s))/N-y||² has derivative (2/N) inner((a+phi(t))/N-y,v) at t. Multiplying that risk by N/lambda gives derivative (2/lambda) times the same inner product. All divisions are real totalized divisions; lambda=0 is an algebraic zero-scaling case, not a temperature model.

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 empirical_squared_feature_risk_derivatives
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
    {N : ℕ} (hN : 0 < N) (lambda : ℝ)
    {phi : ℝ → H} {v a y : H} {t : ℝ} (hphi : HasDerivAt phi v t) :
    HasDerivAt (fun s => ‖(N : ℝ)⁻¹ • (a + phi s) - y‖ ^ 2)
      ((2 / (N : ℝ)) * ⟪(N : ℝ)⁻¹ • (a + phi t) - y, v⟫_ℝ) t ∧
    HasDerivAt (fun s => ((N : ℝ) / lambda) * ‖(N : ℝ)⁻¹ • (a + phi s) - y‖ ^ 2)
      ((2 / lambda) * ⟪(N : ℝ)⁻¹ • (a + phi t) - y, v⟫_ℝ) t

Exact module and namespace context

Proof roadmap

  1. 1Differentiate the actual mean

    The derivative of N^{-1}(a+phi(s))-y is N^{-1}v; translations by fixed vectors contribute zero.

  2. 2Differentiate the squared norm

    Apply the real Hilbert squared-norm chain rule to this residual, yielding its inner product with the derived derivative.

  3. 3Cancel the genuine nonzero particle count

    Multiply by N/lambda and use N>0 to cancel N. This does not require lambda to be nonzero; totalized zero scaling remains valid.

Full assumptions and notation

All objects and hypotheses

  • N>0; phi has actual scalar-parameter derivative v at t.
  • H is a real inner-product normed space; a and y are fixed arbitrary vectors; lambda is any real number.

Mathematical proof

1. Differentiate the actual mean

The derivative of N^{-1}(a+phi(s))-y is N^{-1}v; translations by fixed vectors contribute zero.

\[\frac{d}{ds}(N^{-1}(a+\phi(s))-y)_{s=t}=N^{-1}v.\]
Corresponding Lean step

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

2. Differentiate the squared norm

Apply the real Hilbert squared-norm chain rule to this residual, yielding its inner product with the derived derivative.

\[R\prime(t)=2\langle N^{-1}(a+\phi(t))-y,N^{-1}v\rangle.\]
Corresponding Lean step

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

3. Cancel the genuine nonzero particle count

Multiply by N/lambda and use N>0 to cancel N. This does not require lambda to be nonzero; totalized zero scaling remains valid.

\[\frac N\lambda\frac2N=\frac2\lambda.\]
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 · empirical_squared_feature_risk_derivatives

See the adjacent exact Lean and the mathematical proof steps.

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 empirical_squared_feature_risk_derivatives
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
    {N : ℕ} (hN : 0 < N) (lambda : ℝ)
    {phi : ℝ → H} {v a y : H} {t : ℝ} (hphi : HasDerivAt phi v t) :
    HasDerivAt (fun s => ‖(N : ℝ)⁻¹ • (a + phi s) - y‖ ^ 2)
      ((2 / (N : ℝ)) * ⟪(N : ℝ)⁻¹ • (a + phi t) - y, v⟫_ℝ) t ∧
    HasDerivAt (fun s => ((N : ℝ) / lambda) * ‖(N : ℝ)⁻¹ • (a + phi s) - y‖ ^ 2)
      ((2 / lambda) * ⟪(N : ℝ)⁻¹ • (a + phi t) - y, v⟫_ℝ) t := by
  have hNr : (N : ℝ) ≠ 0 := by exact_mod_cast hN.ne'
  have hsum : HasDerivAt (fun s => a + phi s) v t := hphi.const_add a
  have hmean : HasDerivAt (fun s => (N : ℝ)⁻¹ • (a + phi s)) ((N : ℝ)⁻¹ • v) t :=
    HasDerivAt.const_smul (N : ℝ)⁻¹ hsum
  have hcurve : HasDerivAt (fun s => (N : ℝ)⁻¹ • (a + phi s) - y) ((N : ℝ)⁻¹ • v) t :=
    hmean.sub_const y
  have hsq : HasDerivAt (fun s => ‖(N : ℝ)⁻¹ • (a + phi s) - y‖ ^ 2)
      ((2 / (N : ℝ)) * ⟪(N : ℝ)⁻¹ • (a + phi t) - y, v⟫_ℝ) t := by
    simpa only [real_inner_smul_right, div_eq_mul_inv, mul_assoc] using hcurve.norm_sq
  have hcancel : ((N : ℝ) / lambda) *
        ((2 / (N : ℝ)) * ⟪(N : ℝ)⁻¹ • (a + phi t) - y, v⟫_ℝ) =
      (2 / lambda) * ⟪(N : ℝ)⁻¹ • (a + phi t) - y, v⟫_ℝ := by
    simp only [div_eq_mul_inv]
    calc
      (N : ℝ) * lambda⁻¹ * (2 * (N : ℝ)⁻¹ * ⟪(N : ℝ)⁻¹ • (a + phi t) - y, v⟫_ℝ) =
          ((N : ℝ) * (N : ℝ)⁻¹) *
            (2 * lambda⁻¹ * ⟪(N : ℝ)⁻¹ • (a + phi t) - y, v⟫_ℝ) := by ring
      _ = 2 * lambda⁻¹ * ⟪(N : ℝ)⁻¹ • (a + phi t) - y, v⟫_ℝ := by
        rw [mul_inv_cancel₀ hNr, one_mul]
  have hscaled := HasDerivAt.const_mul ((N : ℝ) / lambda) hsq
  rw [hcancel] at hscaled
  exact ⟨hsq, hscaled⟩

Exact module and namespace context

Scope and omitted-condition boundaries
  • No actual parameter-feature differentiability is constructed.
  • The algebraic lambda=0 case is not a statistical or dynamical interpretation.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

    Mathlib API called (external library)

    • HasDerivAt.const_smul
    • HasDerivAt.norm_sq
    • HasDerivAt.const_mul
    • mul_inv_cancel₀

    Mathematical sources

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