Actual posterior score and covariance identities

Fan Chen, Sinho Chewi, Jianfeng Lu, Matthew S. Zhang; ASTIS original mathematical restatement of equation4.1, with explicit arbitrary-probability and constant-prefactor generalizations.

Complete source statement (Samplinglib restatement)

At every observation y, R_y is a probability measure and the identity map belongs to L2(R_y). For every direction v, DU(y)[v]=inner(y-mean(R_y),v)/eta. For every v,w, D2U(y)[v,w]=inner(v,w)/eta-covarianceBilin(R_y)(v,w)/eta^2. These are actual first and second Frechet derivatives and actual finite posterior moments; the constant positive prefactor cancels exactly.

Actual Gaussian posterior derivative identities

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Actual posterior score and covariance identities

AutoSamplingTheory.TechnicalLemmas.Measure.GaussianConvolutionRegularity.gaussian_convolution_derivatives · theorem · Teaching coverage

Read this first

Mathematical statement

\[R_y(dx)=Z(y)^{-1}e^{-\|x-y\|^2/(2\eta)}\mu(dx),\quad X\in L^2(R_y),\quad DU(y)[v]=\eta^{-1}\langle y-\mathbb E_{R_y}X,v\rangle,\quad D^2U(y)[v,w]=\eta^{-1}\langle v,w\rangle-\eta^{-2}\operatorname{Cov}_{R_y}(\langle v,X\rangle,\langle w,X\rangle).\]

Lean statement · gaussian_convolution_derivatives

Actual selected posterior probability/L2 and all-direction first/second Frechet derivative identities using actual mean and covariance.

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 gaussian_convolution_derivatives (μ : Measure E) [IsProbabilityMeasure μ] {η C : ℝ} (hη : 0 < η)
    (hC : 0 < C) :
    let R := fun y : E => μ.tilted (fun x => -‖x-y‖^2/(2*η))
    let U := fun y : E => -Real.log (C*∫ x, Real.exp (-‖y-x‖^2/(2*η)) ∂μ)
    (∀ y, IsProbabilityMeasure (R y) ∧ MemLp (fun x : E => x) 2 (R y)) ∧
    (∀ y v, fderiv ℝ U y v = inner ℝ (y-∫ x, x ∂(R y)) v/η) ∧
    ∀ y v w, fderiv ℝ (fderiv ℝ U) y v w =
      inner ℝ v w/η - covarianceBilin (R y) v w/η^2

Exact module and namespace context

Proof roadmap

1Use genuine dominated Gaussian derivatives
Reuse the same canonical kernel calculus. Its positive weight has uniformly bounded first and second operator derivatives. Probability-integrable constants justify differentiating the actual normalizer twice. The existing private regularity proof now returns these proved derivative interfaces; they are not supplied hypotheses.
2Derive posterior probability and second moments
Gaussian damping gives w≤1 and w norm(x-y)^2≤2eta. The triangle inequality yields w norm(x)^2≤2 norm(y)^2+4eta. Both dominating constants are integrable against the probability input. Positive normalizer and the actual tilted integrability identity derive posterior probability and identity L2, even when the input has no moments.
3Identify normalized derivative moments
Insert the exact quadratic tilt into the Bochner integral and divide by the positive Gaussian normalizer. Continuous-linear-map evaluation commutes with integrable derivative integrals. The explicit kernel formulas produce actual posterior first and second uncentered moments; splitting the second derivative uses integrability, rather than undefined total integrals.
4Differentiate the negative log exactly
The positive normalizer justifies log differentiation and differentiating its reciprocal. Apply the product rule to the actual first derivative map. Evaluating the resulting second derivative gives the exact quotient, including its sign and eta powers.
5Center the actual finite moments
Posterior L2 implies an actual Bochner mean and L2 of every displacement projection. Integral linearity identifies the expected displacement with y minus the mean. The true L2 covariance identity subtracts the product of means; translation and two signs identify displacement covariance with covarianceBilin(R_y). Substitute the normalized moments in the log quotient.
6Keep the positive prefactor and source convention
For C>0 and Z>0, -log(CZ)=-log Z-log C. This fixed constant has zero derivatives. The genuine source Test uses the existing exact U_eta=V_eta+log Z_V, so the first and second directional identities apply to the source unnormalized V_eta and its same backward Gaussian kernel. The identities give no quantitative covariance inequality or Hessian curvature estimate.

Full assumptions and notation

All objects and hypotheses

E is a finite-dimensional real inner-product space with its Borel measurable space, including dimension zero. mu is an arbitrary probability measure; eta>0 and C>0 are real numbers. No input density, finite input moments, input potential, smoothness, curvature, normalizer or conditional-version certificate is assumed.
Z(y)=integral exp(-norm(y-x)^2/(2eta))dmu(x), R_y=mu.tilted(-norm(x-y)^2/(2eta)), U(y)=-log(C Z(y)). C is an arbitrary positive constant prefactor; choosing the actual Gaussian C_eta gives its negative-log probability density. Other C values are not asserted to normalize a density.
R_y is the actual everywhere-selected posterior of the Gaussian augmentation, previously identified as a measurable Markov/disintegration kernel. Probability and finite second moments are derived here; mean is the Bochner integral, covarianceBilin is the true centered bilinear covariance. The new theorem concerns this selected version, never an arbitrary conditional representative.
For the source Gibbs input, the actual source unnormalized potential V_eta differs from the normalized density potential U_eta by the already-proved constant log Z_V. The genuine Test derives original Gibbs probability from C2 and positive lower Hessian, proves source V_eta directional derivative/covariance identities by this exact constant, and joins the same augmentation backward kernel. Source Hessian upper bound and eta upper cap are unnecessary for these identities.

Mathematical proof

1. Use genuine dominated Gaussian derivatives

Reuse the same canonical kernel calculus. Its positive weight has uniformly bounded first and second operator derivatives. Probability-integrable constants justify differentiating the actual normalizer twice. The existing private regularity proof now returns these proved derivative interfaces; they are not supplied hypotheses.

\[Dw_y[v]=-\eta^{-1}w_y\langle y-x,v\rangle,\quad D^2w_y[v,u]=-\eta^{-1}w_y\langle v,u\rangle+\eta^{-2}w_y\langle y-x,v\rangle\langle y-x,u\rangle,\quad\|Dw_y\|\le(1+2\eta)/\eta,\ \|D^2w_y\|\le3/\eta.\]

Corresponding Lean step

gaussianNormalizerRegularity; gaussianDeriv; gaussianFirstDeriv; hasFDerivAt_integral_of_dominated_of_fderiv_le; normalizerDerivatives

2. Derive posterior probability and second moments

Gaussian damping gives w≤1 and w norm(x-y)^2≤2eta. The triangle inequality yields w norm(x)^2≤2 norm(y)^2+4eta. Both dominating constants are integrable against the probability input. Positive normalizer and the actual tilted integrability identity derive posterior probability and identity L2, even when the input has no moments.

\[0<w\le1,\quad w\|x-y\|^2\le2\eta,\quad w\|x\|^2\le2\|y\|^2+4\eta\ \Longrightarrow\ R_y\text{ probability},\quad X\in L^2(R_y).\]

Corresponding Lean step

posteriorMoment; Real.mul_exp_neg_le_exp_neg_one; isProbabilityMeasure_tilted; integrable_tilted_iff; memLp_two_iff_integrable_sq_norm

3. Identify normalized derivative moments

Insert the exact quadratic tilt into the Bochner integral and divide by the positive Gaussian normalizer. Continuous-linear-map evaluation commutes with integrable derivative integrals. The explicit kernel formulas produce actual posterior first and second uncentered moments; splitting the second derivative uses integrability, rather than undefined total integrals.

\[DZ(y)[v]/Z(y)=-\eta^{-1}\mathbb E_{R_y}\langle y-X,v\rangle,\quad D^2Z(y)[v,w]/Z(y)=-\eta^{-1}\langle v,w\rangle+\eta^{-2}\mathbb E_{R_y}[\langle y-X,v\rangle\langle y-X,w\rangle].\]

Corresponding Lean step

posteriorIntegral; normalizedFirst; normalizedSecond; integral_tilted; integral_div; ContinuousLinearMap.integral_apply; Integrable.apply_continuousLinearMap; integral_add

4. Differentiate the negative log exactly

The positive normalizer justifies log differentiation and differentiating its reciprocal. Apply the product rule to the actual first derivative map. Evaluating the resulting second derivative gives the exact quotient, including its sign and eta powers.

\[D(-\log Z)[v]=-DZ[v]/Z,\quad D^2(-\log Z)[v,w]=DZ[v]DZ[w]/Z^2-D^2Z[v,w]/Z.\]

Corresponding Lean step

rawFirst; rawSecond; HasFDerivAt.log; hasDerivAt_inv; HasDerivAt.comp_hasFDerivAt; HasFDerivAt.smul; HasFDerivAt.neg

5. Center the actual finite moments

Posterior L2 implies an actual Bochner mean and L2 of every displacement projection. Integral linearity identifies the expected displacement with y minus the mean. The true L2 covariance identity subtracts the product of means; translation and two signs identify displacement covariance with covarianceBilin(R_y). Substitute the normalized moments in the log quotient.

\[\mathbb E\langle y-X,v\rangle=\langle y-\mathbb EX,v\rangle,\quad\operatorname{Cov}(y-X)=\operatorname{Cov}(X),\quad D^2(-\log Z)=\eta^{-1}I-\eta^{-2}\operatorname{Cov}(R_y).\]

Corresponding Lean step

MemLp.integrable; MemLp.inner_const; integral_inner; integral_sub; covariance_eq_sub; covariance_const_sub_left/right; covarianceBilin_apply_eq_cov

6. Keep the positive prefactor and source convention

For C>0 and Z>0, -log(CZ)=-log Z-log C. This fixed constant has zero derivatives. The genuine source Test uses the existing exact U_eta=V_eta+log Z_V, so the first and second directional identities apply to the source unnormalized V_eta and its same backward Gaussian kernel. The identities give no quantitative covariance inequality or Hessian curvature estimate.

\[U=-\log Z-\log C,\quad U_\eta=V_\eta+\log Z_V\ \Longrightarrow\ DU_\eta=DV_\eta,\quad D^2U_\eta=D^2V_\eta.\]

Corresponding Lean step

Real.log_mul; fderiv_sub_const; Tests.GaussianConvolutionDerivatives.actual_source_score_covariance; SmoothedGibbsPotential.smoothed_gibbs_potential; GaussianConditionalKernel.exists_tilted_isCondKernel

Lean verification

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

Lean proof · gaussian_convolution_derivatives

Canonical dominated Gaussian derivative integrals, true posterior L2, exact tilted normalized moments, log/reciprocal product derivative, actual centered covariance and positive constant cancellation.

Download module (.lean)

theorem gaussian_convolution_derivatives (μ : Measure E) [IsProbabilityMeasure μ] {η C : ℝ} (hη : 0 < η)
    (hC : 0 < C) :
    let R := fun y : E => μ.tilted (fun x => -‖x-y‖^2/(2*η))
    let U := fun y : E => -Real.log (C*∫ x, Real.exp (-‖y-x‖^2/(2*η)) ∂μ)
    (∀ y, IsProbabilityMeasure (R y) ∧ MemLp (fun x : E => x) 2 (R y)) ∧
    (∀ y v, fderiv ℝ U y v = inner ℝ (y-∫ x, x ∂(R y)) v/η) ∧
    ∀ y v w, fderiv ℝ (fderiv ℝ U) y v w =
      inner ℝ v w/η - covarianceBilin (R y) v w/η^2 := by
  let Z := fun y : E => ∫ x, gaussianWeight η y x ∂μ
  let D := fun y : E => ∫ x, gaussianFirst η y x ∂μ
  let H := fun y : E => ∫ x, gaussianSecond η y x ∂μ
  let R := fun y : E => μ.tilted (fun x => -‖x-y‖^2/(2*η))
  let U0 := fun y : E => -Real.log (Z y)
  have hU : (fun y : E => -Real.log (C*Z y)) = fun y => U0 y-Real.log C := by
    funext y
    have hZ := (normalizerDerivatives μ hη).1 y
    rw [Real.log_mul hC.ne' hZ.ne']
    dsimp only [U0]
    ring
  have hDU : fderiv ℝ (fun y : E => -Real.log (C*Z y)) = fderiv ℝ U0 := by
    rw [hU]
    funext y
    exact fderiv_sub_const _
  refine ⟨fun y => posteriorMoment μ hη y, ?_, ?_⟩
  · intro y v
    change fderiv ℝ (fun y : E => -Real.log (C*Z y)) y v = _
    rw [hDU]
    obtain ⟨hR,hLp⟩ := posteriorMoment μ hη y
    haveI : IsProbabilityMeasure (R y) := hR
    have hi : Integrable (fun x : E => x) (R y) := hLp.integrable (by norm_num)
    have hm : (∫ x, inner ℝ (y-x) v ∂(R y)) = inner ℝ (y-∫ x, x ∂(R y)) v := by
      have he : (fun x : E => inner ℝ (y-x) v) = fun x => inner ℝ v (y-x) := by
        funext x
        exact real_inner_comm _ _
      rw [he]
      have hmean : (∫ x, inner ℝ v (y-x) ∂(R y)) =
          inner ℝ v (∫ x, y-x ∂(R y)) := by
        simpa only [Pi.sub_apply] using
          (integral_inner (𝕜 := ℝ) ((integrable_const y).sub hi) v)
      have hdiff : (∫ x, y-x ∂(R y)) = y-∫ x, x ∂(R y) := by
        simpa only [Pi.sub_apply, integral_const, probReal_univ, one_smul] using
          integral_sub (integrable_const y) hi
      rw [hmean,hdiff]
      exact real_inner_comm _ _
    calc
      _ = -(D y v/Z y) := by simpa only [neg_div] using rawFirst μ hη y v
      _ = (∫ x, inner ℝ (y-x) v ∂(R y))/η := by
        rw [normalizedFirst μ hη y v]; ring
      _ = _ := by rw [hm]
  · intro y v w
    change fderiv ℝ (fderiv ℝ (fun y : E => -Real.log (C*Z y))) y v w = _
    rw [hDU]
    obtain ⟨hR,hLp⟩ := posteriorMoment μ hη y
    haveI : IsProbabilityMeasure (R y) := hR
    have hi : Integrable (fun x : E => x) (R y) := hLp.integrable (by norm_num)
    have hξ : MemLp (fun x : E => y-x) 2 (R y) := (memLp_const y).sub hLp
    have hv := hξ.inner_const (𝕜 := ℝ) v
    have hw := hξ.inner_const (𝕜 := ℝ) w
    have hc : covarianceBilin (R y) v w =
        (∫ x, inner ℝ (y-x) v*inner ℝ (y-x) w ∂(R y)) -
          (∫ x, inner ℝ (y-x) v ∂(R y))*(∫ x, inner ℝ (y-x) w ∂(R y)) := by
      have hcenter : covariance (fun x => inner ℝ (y-x) v)
          (fun x => inner ℝ (y-x) w) (R y) = covarianceBilin (R y) v w := by
        simp_rw [inner_sub_left]
        rw [covariance_const_sub_left (hi.inner_const (𝕜 := ℝ) v),
          covariance_const_sub_right (hi.inner_const (𝕜 := ℝ) w), neg_neg]
        rw [covarianceBilin_apply_eq_cov hLp]
        simp_rw [real_inner_comm v, real_inner_comm w]
        rfl
      exact hcenter.symm.trans (by simpa only [Pi.mul_apply] using covariance_eq_sub hv hw)
    rw [rawSecond μ hη y v w]
    change D y v*D y w/Z y^2 - H y v w/Z y = _
    rw [show D y v*D y w/Z y^2 = (D y v/Z y)*(D y w/Z y) by ring]
    rw [normalizedFirst μ hη y v, normalizedFirst μ hη y w,
      normalizedSecond μ hη y v w, hc]
    ring

end
end AutoSamplingTheory.TechnicalLemmas.Measure.GaussianConvolutionRegularity

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Section4.1 equation4.1 uses the actual Gibbs posterior and source unnormalized V_eta.	E is a finite-dimensional real inner-product space with its Borel measurable space, including dimension zero. mu is an arbitrary probability measure; eta>0 and C>0 are real numbers. No input density, finite input moments, input potential, smoothness, curvature, normalizer or conditional-version certificate is assumed. Z(y)=integral exp(-norm(y-x)^2/(2eta))dmu(x), R_y=mu.tilted(-norm(x-y)^2/(2eta)), U(y)=-log(C Z(y)). C is an arbitrary positive constant prefactor; choosing the actual Gaussian C_eta gives its negative-log probability density. Other C values are not asserted to normalize a density. R_y is the actual everywhere-selected posterior of the Gaussian augmentation, previously identified as a measurable Markov/disintegration kernel. Probability and finite second moments are derived here; mean is the Bochner integral, covarianceBilin is the true centered bilinear covariance. The new theorem concerns this selected version, never an arbitrary conditional representative. For the source Gibbs input, the actual source unnormalized potential V_eta differs from the normalized density potential U_eta by the already-proved constant log Z_V. The genuine Test derives original Gibbs probability from C2 and positive lower Hessian, proves source V_eta directional derivative/covariance identities by this exact constant, and joins the same augmentation backward kernel. Source Hessian upper bound and eta upper cap are unnecessary for these identities.	generalization	Arbitrary probability input includes the derived source Gibbs law. Every selected posterior moment and derivative is proved; no moment/density/regularity premise is added. The source Test explicitly transports the exact potential constant. Positive C is only a constant-prefactor generalization, not an arbitrary probability-density certificate.
Equation4.1 states gradient and Hessian matrix identities.	At every observation y, R_y is a probability measure and the identity map belongs to L2(R_y). For every direction v, DU(y)[v]=inner(y-mean(R_y),v)/eta. For every v,w, D2U(y)[v,w]=inner(v,w)/eta-covarianceBilin(R_y)(v,w)/eta^2. These are actual first and second Frechet derivatives and actual finite posterior moments; the constant positive prefactor cancels exactly.	same	The real Hilbert directional first derivative for every v and bilinear second derivative for every v,w are exactly the gradient/Hessian representation in the induced inner product. covarianceBilin is genuine L2 centered covariance.
Lemma4.1 obtains quantitative curvature using Brascamp-Lieb and Cramer-Rao.	No covariance inequalities or quantitative source Hessian bounds are asserted.	unresolved	Actual everywhere-selected quadratic Gaussian posterior has probability and finite second moments, without input moments; true first/second derivatives of negative log of the Gaussian normalizer equal posterior mean and covariance, including the positive constant prefactor and dimension zero. No Brascamp-Lieb/Cramer-Rao covariance inequalities, source Hessian bounds/higher cumulants, stationarity/algorithm accuracy/history/expected work, PBPS process or either complete main/composition. TV never transfers unbounded expected cost.

Actual everywhere-selected quadratic Gaussian posterior has probability and finite second moments, without input moments; true first/second derivatives of negative log of the Gaussian normalizer equal posterior mean and covariance, including the positive constant prefactor and dimension zero. No Brascamp-Lieb/Cramer-Rao covariance inequalities, source Hessian bounds/higher cumulants, stationarity/algorithm accuracy/history/expected work, PBPS process or either complete main/composition. TV never transfers unbounded expected cost.

Encoder–denoiser: accepted · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

Actual everywhere-selected quadratic Gaussian posterior has probability and finite second moments, without input moments; true first/second derivatives of negative log of the Gaussian normalizer equal posterior mean and covariance, including the positive constant prefactor and dimension zero. No Brascamp-Lieb/Cramer-Rao covariance inequalities, source Hessian bounds/higher cumulants, stationarity/algorithm accuracy/history/expected work, PBPS process or either complete main/composition. TV never transfers unbounded expected cost.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

hasFDerivAt_integral_of_dominated_of_fderiv_le
integral_tilted
integrable_tilted_iff
isProbabilityMeasure_tilted
memLp_two_iff_integrable_sq_norm
ContinuousLinearMap.integral_apply
Integrable.apply_continuousLinearMap
HasFDerivAt.log
hasDerivAt_inv
HasDerivAt.comp_hasFDerivAt
integral_inner
covariance_eq_sub
covarianceBilin_apply_eq_cov
Real.log_mul
fderiv_sub_const

Mathematical sources

SPHMC equation4.1 actual posterior score/covariance — Actual everywhere-selected quadratic Gaussian posterior has probability and finite second moments, without input moments; true first/second derivatives of negative log of the Gaussian normalizer equal posterior mean and covariance, including the positive constant prefactor and dimension zero. No Brascamp-Lieb/Cramer-Rao covariance inequalities, source Hessian bounds/higher cumulants, stationarity/algorithm accuracy/history/expected work, PBPS process or either complete main/composition. TV never transfers unbounded expected cost.

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

Actual posterior score and covariance identities

Complete source statement (Samplinglib restatement)

Actual Gaussian posterior derivative identities

Read the formalized proofs

Actual posterior score and covariance identities

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Use genuine dominated Gaussian derivatives

2. Derive posterior probability and second moments

3. Identify normalized derivative moments

4. Differentiate the negative log exactly

5. Center the actual finite moments

6. Keep the positive prefactor and source convention

Lean verification

Source assumptions versus formal assumptions

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?