GaussianConvolutionRegularity: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

Actual Gaussian convolution density and C2 normalized potential
Actual posterior score and covariance identities

Samplinglib mathematical lesson

Actual Gaussian convolution density and C2 normalized potential

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

Read this first

Mathematical statement

The actual Gaussian add-noise probability law equals volume.withDensity(ofReal(C_eta Z_eta)). Its density is strictly positive at every y, Z_eta is globally C2, and the exact negative-log density U_eta=-log(C_eta Z_eta) is globally C2. The input law may be singular and may lack moments.

\[\pi_\eta=(x+\sqrt\eta\,g)_\#(\mu\otimes\gamma)=C_\eta Z_\eta\,dx,\quad Z_\eta(y)=\int e^{-\|y-x\|^2/(2\eta)}\mu(dx)>0,\quad Z_\eta,U_\eta=-\log(C_\eta Z_\eta)\in C^2.\]

Lean statement · gaussian_convolution_potential_c2

Actual Gaussian pushforward equals explicit volume density, with everywhere-positive normalizer and genuine C2 negative-log density.

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_potential_c2 (μ : Measure E) [IsProbabilityMeasure μ]
    {η : ℝ} (hη : 0 < η) :
    let C := ((Real.sqrt (2*Real.pi*η))⁻¹)^Module.finrank ℝ E
    let Z := fun y : E => ∫ x, Real.exp (-‖y-x‖^2/(2*η)) ∂μ
    (μ.prod (stdGaussian E)).map (fun p => p.1+Real.sqrt η • p.2) =
      (volume : Measure E).withDensity (fun y => ENNReal.ofReal (C*Z y)) ∧
    (∀ y, 0 < C*Z y) ∧ ContDiff ℝ 2 Z ∧
      ContDiff ℝ 2 (fun y => -Real.log (C*Z y))

Exact module and namespace context

Proof roadmap

1Differentiate the actual Gaussian weight
For u=y-x, w=exp(-norm(u)^2/(2eta)), differentiate the squared norm and exponential as Frechet maps. D_yw[v]=-eta^-1 w inner(u,v), and D_y²w[v,t]=w(eta^-2 inner(u,v)inner(u,t)-eta^-1 inner(v,t)). These are the explicit kernel derivatives, not derivatives of an assumed regularized potential.
2Derive probability-integrable domination
The Gaussian weight lies in (0,1]. With q=norm(u)^2/(2eta), q exp(-q)≤exp(-1)≤1 gives w norm(u)^2≤2eta. Since norm(u)≤1+norm(u)^2, the first derivative norm is at most (1+2eta)/eta. The second derivative operator norm is at most w norm(u)^2/eta²+w/eta≤3/eta. These constants are uniform in x and y, so the probability input integrates them without any moment condition.
3Differentiate the actual normalizer twice
Continuity of the displayed derivatives gives their Borel/strong measurability. Apply the dominated parametric-integral Frechet theorem first to w and then to Dw. Dominated continuity of the integral of D²w makes the first derivative C1, hence Z is C2. Probability mass one and everywhere w>0 imply Z(y)>0 at every observation, not merely almost everywhere.
4Identify the actual smoothed density
Project the existing genuine GaussianAugmentation joint density to its observation coordinate. For any measurable nonnegative test, the pushforward integral and nonnegative Fubini put the x-integral inside the y-integral. The established Bochner integrability identifies integral ofReal(C_eta w) with ofReal(C_eta Z). Equality against all such tests proves the exact volume density of the actual Gaussian add-noise law.
5Form the exact normalized potential and expose the source convention
The finite-dimensional Gaussian prefactor C_eta is strictly positive for eta>0, including dimension zero. Compose the C2 positive function C_eta Z with log and negate. This yields C2 of the actual normalized negative-log density, with its normalization constant retained. Source Hessian bounds require additional posterior covariance inequalities and are not inferred from C2 regularity. Source Section3.1 defines the unnormalized convolution exp(-V_eta)=exp(-V)*Gaussian. This theorem constructs the exact normalized density potential U_eta=-log(C_eta Z_mu). For Gibbs mu=exp(-V) volume/Z_V, U_eta=V_eta+log Z_V; formalizing that Gibbs specialization and constant-shift adapter remains separate. This normalization difference does not change derivatives, but the two chosen potentials are not asserted literally identical.

Full assumptions and notation

All objects and hypotheses

E is a finite-dimensional real inner-product space equipped with its Borel measurable space, including dimension zero. eta is a strictly positive real. mu is an arbitrary probability measure on E, possibly singular and without finite moments.
C_eta=((sqrt(2*pi*eta))^-1)^dim E and Z_eta(y)=integral exp(-norm(y-x)^2/(2*eta)) dmu(x). The actual smoothed law is the measurable pushforward of mu×standard Gaussian by (x,g)→x+sqrt(eta)g. The potential is exactly -log(C_eta Z_eta), not Gaussian averaging of an input potential.
All first/second Gaussian derivative domination, Bochner integrability, measurability and strictly positive normalizers are derived. The local CLM dual instances choose existing canonical normed structures and add no mathematical premises. No input density, moment, curvature or supplied regularity certificate is assumed.
Source Section3.1 defines the unnormalized convolution exp(-V_eta)=exp(-V)*Gaussian. This theorem constructs the exact normalized density potential U_eta=-log(C_eta Z_mu). For Gibbs mu=exp(-V) volume/Z_V, U_eta=V_eta+log Z_V; formalizing that Gibbs specialization and constant-shift adapter remains separate. This normalization difference does not change derivatives, but the two chosen potentials are not asserted literally identical.

Mathematical proof

1. Differentiate the actual Gaussian weight

For u=y-x, w=exp(-norm(u)^2/(2eta)), differentiate the squared norm and exponential as Frechet maps. D_yw[v]=-eta^-1 w inner(u,v), and D_y²w[v,t]=w(eta^-2 inner(u,v)inner(u,t)-eta^-1 inner(v,t)). These are the explicit kernel derivatives, not derivatives of an assumed regularized potential.

\[Dw=-\eta^{-1}w\,u^\flat,\qquad D^2w=w(\eta^{-2}u^\flat\otimes u^\flat-\eta^{-1}I).\]

Corresponding Lean step

gaussianDeriv; gaussianFirstDeriv; realDual; innerSL

2. Derive probability-integrable domination

The Gaussian weight lies in (0,1]. With q=norm(u)^2/(2eta), q exp(-q)≤exp(-1)≤1 gives w norm(u)^2≤2eta. Since norm(u)≤1+norm(u)^2, the first derivative norm is at most (1+2eta)/eta. The second derivative operator norm is at most w norm(u)^2/eta²+w/eta≤3/eta. These constants are uniform in x and y, so the probability input integrates them without any moment condition.

\[0<w\le1,\quad w\|u\|^2\le2\eta,\quad\|Dw\|\le(1+2\eta)/\eta,\quad\|D^2w\|\le3/\eta.\]

Corresponding Lean step

weight_bounds; first_bound; second_bound; integrable_const

3. Differentiate the actual normalizer twice

Continuity of the displayed derivatives gives their Borel/strong measurability. Apply the dominated parametric-integral Frechet theorem first to w and then to Dw. Dominated continuity of the integral of D²w makes the first derivative C1, hence Z is C2. Probability mass one and everywhere w>0 imply Z(y)>0 at every observation, not merely almost everywhere.

\[DZ(y)=\int Dw(y,x)\,\mu(dx),\quad D^2Z(y)=\int D^2w(y,x)\,\mu(dx),\quad Z(y)>0.\]

Corresponding Lean step

gaussianNormalizerRegularity; hdZ; hdD; hHC; hDC; hZC; integral_exp_pos; hasFDerivAt_integral_of_dominated_of_fderiv_le; continuous_of_dominated

4. Identify the actual smoothed density

Project the existing genuine GaussianAugmentation joint density to its observation coordinate. For any measurable nonnegative test, the pushforward integral and nonnegative Fubini put the x-integral inside the y-integral. The established Bochner integrability identifies integral ofReal(C_eta w) with ofReal(C_eta Z). Equality against all such tests proves the exact volume density of the actual Gaussian add-noise law.

\[\int f\,d\pi_\eta=\int\!\int f(y)C_\eta w(y,x)\,dy\,\mu(dx)=\int f(y)C_\eta Z_\eta(y)\,dy.\]

Corresponding Lean step

gaussianDensity; GaussianAugmentation.augmentation_eq_withDensity; Measure.ext_of_lintegral; lintegral_prod_symm; ofReal_integral_eq_lintegral_ofReal

5. Form the exact normalized potential and expose the source convention

The finite-dimensional Gaussian prefactor C_eta is strictly positive for eta>0, including dimension zero. Compose the C2 positive function C_eta Z with log and negate. This yields C2 of the actual normalized negative-log density, with its normalization constant retained. Source Hessian bounds require additional posterior covariance inequalities and are not inferred from C2 regularity. Source Section3.1 defines the unnormalized convolution exp(-V_eta)=exp(-V)*Gaussian. This theorem constructs the exact normalized density potential U_eta=-log(C_eta Z_mu). For Gibbs mu=exp(-V) volume/Z_V, U_eta=V_eta+log Z_V; formalizing that Gibbs specialization and constant-shift adapter remains separate. This normalization difference does not change derivatives, but the two chosen potentials are not asserted literally identical.

\[U_\eta(y)=-\log(C_\eta Z_\eta(y)),\qquad C_\eta Z_\eta(y)>0,\qquad U_\eta\in C^2.\]

Corresponding Lean step

gaussian_convolution_potential_c2; hC; ContDiff.log; ContDiff.neg

Lean verification

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

Lean proof · gaussian_convolution_potential_c2

Explicit Gaussian derivative domination, two genuine parametric integral derivatives, dominated continuity, exact augmentation marginal and positive logarithm.

Download module (.lean)

theorem gaussian_convolution_potential_c2 (μ : Measure E) [IsProbabilityMeasure μ]
    {η : ℝ} (hη : 0 < η) :
    let C := ((Real.sqrt (2*Real.pi*η))⁻¹)^Module.finrank ℝ E
    let Z := fun y : E => ∫ x, Real.exp (-‖y-x‖^2/(2*η)) ∂μ
    (μ.prod (stdGaussian E)).map (fun p => p.1+Real.sqrt η • p.2) =
      (volume : Measure E).withDensity (fun y => ENNReal.ofReal (C*Z y)) ∧
    (∀ y, 0 < C*Z y) ∧ ContDiff ℝ 2 Z ∧
      ContDiff ℝ 2 (fun y => -Real.log (C*Z y)) := by
  let C := ((Real.sqrt (2*Real.pi*η))⁻¹)^Module.finrank ℝ E
  have hC : 0 < C := by dsimp [C]; positivity
  obtain ⟨hZ,hZC,hV,_hdZ,_hdD⟩ := gaussianNormalizerRegularity μ hη
  exact ⟨gaussianDensity μ hη,fun y => mul_pos hC (hZ y),hZC,hV C hC⟩

Exact module and namespace context

Scope and omitted-condition boundaries

Closes the genuine Gaussian-smoothed density and global C2 normalizer/negative-log potential prerequisite, for arbitrary probability input and eta>0. It does not yet prove the score/posterior-covariance identities (4.1), Lemma4.1 curvature via Brascamp-Lieb/Cramer-Rao, higher derivative/cumulant estimates, target invariance, numerical bias/history/expected costs, PBPS process, either complete main result or composition. TV proximity does not transfer unbounded cost. Source Section3.1 defines the unnormalized convolution exp(-V_eta)=exp(-V)*Gaussian. This theorem constructs the exact normalized density potential U_eta=-log(C_eta Z_mu). For Gibbs mu=exp(-V) volume/Z_V, U_eta=V_eta+log Z_V; formalizing that Gibbs specialization and constant-shift adapter remains separate. This normalization difference does not change derivatives, but the two chosen potentials are not asserted literally identical.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.ExampleCases.ProximalBPS.GaussianAugmentation.augmentation_eq_withDensity

Mathlib API called (external library)

hasFDerivAt_integral_of_dominated_of_fderiv_le
continuous_of_dominated
ContDiff.log
contDiff_succ_iff_fderiv
contDiff_one_iff_fderiv
Real.mul_exp_neg_le_exp_neg_one
integral_exp_pos
Measure.ext_of_lintegral
lintegral_map
lintegral_prod_symm
lintegral_withDensity_eq_lintegral_mul
ofReal_integral_eq_lintegral_ofReal
ContinuousLinearMap.toNormedAddCommGroup
ContinuousLinearMap.toNormedSpace

Mathematical sources

SPHMC actual Gaussian smoothing analytic prerequisite — Closes the genuine Gaussian-smoothed density and global C2 normalizer/negative-log potential prerequisite, for arbitrary probability input and eta>0. It does not yet prove the score/posterior-covariance identities (4.1), Lemma4.1 curvature via Brascamp-Lieb/Cramer-Rao, higher derivative/cumulant estimates, target invariance, numerical bias/history/expected costs, PBPS process, either complete main result or composition. TV proximity does not transfer unbounded 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.

Samplinglib mathematical lesson

Actual posterior score and covariance identities

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

Read this first

Mathematical statement

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.

\[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.

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

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.