The actual translated Gaussian likelihood and RN derivative

Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang; ASTIS expanded prerequisite proof, no author endorsement implied.

Complete source statement (Samplinglib restatement)

SPHMC Lemma6.3(ii) uses the heat-flow bound R_q(Pdag*gamma_tau || Q*gamma_tau)<=q Winfinity(Pdag,Q)^2/(2tau). The selected expanded Gaussian prerequisite, not the full mixture inequality, is the actual likelihood between equal-covariance translates: for G_a=Law(a+sqrt(tau)Z), tau>0, L(z)=exp(inner(x-y,z-y)/tau-norm(x-y)^2/(2tau)) satisfies G_x=G_y.withDensity(ofReal L), absolute continuity and a.e. RN identification under G_y. Measurability and the measure identity are proved rather than assumed.

Actual likelihood

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

The actual translated Gaussian likelihood and RN derivative

AutoSamplingTheory.TechnicalLemmas.Measure.GaussianLikelihood.translated_gaussian_likelihood · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be a finite-dimensional real inner-product Borel space, x,y in E and tau>0. Define G_a as the pushforward of standard Gaussian by z to a+sqrt(tau)z, and L(z)=exp(inner(x-y,z-y)/tau-norm(x-y)^2/(2tau)). Then L is measurable, G_x=G_y.withDensity(ofReal L), G_x is absolutely continuous with respect to G_y, and its RN derivative equals ofReal L almost everywhere under G_y.

\[G_a=\operatorname{Law}(a+\sqrt\tau Z),\quad L(z)=\exp\!\left(\frac{\langle x-y,z-y\rangle}{\tau}-\frac{\|x-y\|^2}{2\tau}\right),\quad \frac{dG_x}{dG_y}=L\quad G_y\text{-a.e.}\]

Lean statement · translated_gaussian_likelihood

Measurability, actual withDensity equality, absolute continuity and RN a.e. equality for the explicitly defined Gaussian laws.

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 translated_gaussian_likelihood {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (x y : E) (τ : ℝ) (hτ : 0 < τ) :
    let G := fun a : E => (stdGaussian E).map (fun z => a + Real.sqrt τ • z)
    let L := fun z : E => Real.exp (inner ℝ (x-y) (z-y) / τ - ‖x-y‖ ^ 2 / (2*τ))
    Measurable L ∧ G x = (G y).withDensity (fun z => ENNReal.ofReal (L z)) ∧
      G x ≪ G y ∧ (G x).rnDeriv (G y) =ᵐ[G y] (fun z => ENNReal.ofReal (L z))

Exact module and namespace context

Proof roadmap

1Translate the existing actual Gaussian density
Apply the existing canonical-volume density theorem for sqrt(tau)Z. Push that measure through the measurable equivalence z to a+z. Translation preserves Haar volume and the inverse map is z-a, giving the normalized density centered at a.
2Prove actual multiplication of densities
The norm identity norm(z-x)^2=norm(z-y)^2-2 inner(x-y,z-y)+norm(x-y)^2 shows the x-density equals the y-density times L. Measurability permits withDensity multiplication, proving equality of the actual measures.
3Identify absolute continuity and the RN version
The explicit density is measurable and finite everywhere. Actual withDensity equality gives absolute continuity. G_y is a probability, so the standard RN identification theorem applies and yields the equality almost everywhere in the correct direction.

Full assumptions and notation

All objects and hypotheses

Finite-dimensional real inner-product space with its Borel measurable structure, including dimension zero.
Tau>0 and arbitrary centers x,y. The covariance is tau I, not sqrt(tau) I.
Both Gaussian laws are actual scaled/translated standard Gaussian pushforwards, not arbitrary laws assumed to have a density ratio.
The source states reverse transport on Euclidean probabilities. This coordinate-free Gaussian ingredient is an explicit expanded prerequisite, not the mixture theorem.

Mathematical proof

1. Translate the existing actual Gaussian density

Apply the existing canonical-volume density theorem for sqrt(tau)Z. Push that measure through the measurable equivalence z to a+z. Translation preserves Haar volume and the inverse map is z-a, giving the normalized density centered at a.

\[G_a(dz)=C_\tau e^{-\|z-a\|^2/(2\tau)}\,dz,\qquad C_\tau=(\sqrt{2\pi\tau})^{-\dim E}.\]

Corresponding Lean step

Local translated_density uses map_map, IsotropicGaussianDensity, measurableEquiv_map_withDensity and map_add_left_eq_self.

2. Prove actual multiplication of densities

The norm identity norm(z-x)^2=norm(z-y)^2-2 inner(x-y,z-y)+norm(x-y)^2 shows the x-density equals the y-density times L. Measurability permits withDensity multiplication, proving equality of the actual measures.

\[C_\tau e^{-\|z-x\|^2/(2\tau)}=C_\tau e^{-\|z-y\|^2/(2\tau)}L(z).\]

Corresponding Lean step

norm_sub_sq_real and real_inner_comm establish the exponent identity; withDensity_mul identifies actual measures, not merely exponent expressions.

3. Identify absolute continuity and the RN version

The explicit density is measurable and finite everywhere. Actual withDensity equality gives absolute continuity. G_y is a probability, so the standard RN identification theorem applies and yields the equality almost everywhere in the correct direction.

\[G_x\ll G_y,\qquad (G_x).\operatorname{rnDeriv}(G_y)=L\quad G_y\text{-a.e.}\]

Corresponding Lean step

withDensity_absolutelyContinuous and Measure.rnDeriv_withDensity after deriving the probability instance for G_y.

Lean verification

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

Lean proof · translated_gaussian_likelihood

The actual translated density helper is local; the public proof derives the likelihood equality and genuine RN identity.

Download module (.lean)

theorem translated_gaussian_likelihood {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (x y : E) (τ : ℝ) (hτ : 0 < τ) :
    let G := fun a : E => (stdGaussian E).map (fun z => a + Real.sqrt τ • z)
    let L := fun z : E => Real.exp (inner ℝ (x-y) (z-y) / τ - ‖x-y‖ ^ 2 / (2*τ))
    Measurable L ∧ G x = (G y).withDensity (fun z => ENNReal.ofReal (L z)) ∧
      G x ≪ G y ∧ (G x).rnDeriv (G y) =ᵐ[G y] (fun z => ENNReal.ofReal (L z)) := by
  have translated_density
      (a : E) (τ : ℝ) (hτ : 0 < τ) :
      (stdGaussian E).map (fun z => a + Real.sqrt τ • z) =
        (volume : Measure E).withDensity (fun z => ENNReal.ofReal
          (((Real.sqrt (2 * Real.pi * τ))⁻¹) ^ Module.finrank ℝ E *
            Real.exp (-‖z-a‖ ^ 2 / (2 * τ)))) := by
    have hmap : (stdGaussian E).map (fun z => a + Real.sqrt τ • z) =
        ((stdGaussian E).map (fun z : E => Real.sqrt τ • z)).map (MeasurableEquiv.addLeft a) := by
      rw [Measure.map_map (by fun_prop) (by fun_prop)]
      rfl
    rw [hmap,IsotropicGaussianDensity.map_sqrt_smul_stdGaussian_eq_withDensity τ hτ,
      RadonNikodym.measurableEquiv_map_withDensity (MeasurableEquiv.addLeft a) _ (by fun_prop)]
    have hvol : (volume : Measure E).map (MeasurableEquiv.addLeft a) = volume :=
      Measure.IsAddLeftInvariant.map_add_left_eq_self a
    rw [hvol]
    congr 1
    funext z
    simp [MeasurableEquiv.addLeft,sub_eq_add_neg,add_comm]
  let G := fun a : E => (stdGaussian E).map (fun z => a + Real.sqrt τ • z)
  let L := fun z : E => Real.exp (inner ℝ (x-y) (z-y) / τ - ‖x-y‖ ^ 2 / (2*τ))
  have hL : Measurable L := by fun_prop
  have heq : G x = (G y).withDensity (fun z => ENNReal.ofReal (L z)) := by
    dsimp only [G]
    rw [translated_density x τ hτ,translated_density y τ hτ,
      ← withDensity_mul _ (by fun_prop) (by fun_prop)]
    congr 1
    funext z
    change ENNReal.ofReal (_ * Real.exp _) = ENNReal.ofReal (_ * Real.exp _) * ENNReal.ofReal (L z)
    rw [← ENNReal.ofReal_mul (by positivity)]
    congr 1
    dsimp only [L]
    simp only [mul_assoc]
    rw [← Real.exp_add]
    congr 2
    have hnorm : ‖z-x‖ ^ 2 = ‖z-y‖ ^ 2 - 2 * inner ℝ (x-y) (z-y) + ‖x-y‖ ^ 2 := by
      have hz : z-x = (z-y)-(x-y) := by abel
      rw [hz,norm_sub_sq_real,real_inner_comm]
    rw [hnorm]
    field_simp
    ring
  let : IsProbabilityMeasure (G y) := Measure.isProbabilityMeasure_map (by fun_prop)
  refine ⟨hL,heq,?_,?_⟩
  · change G x ≪ G y
    rw [heq]
    exact withDensity_absolutelyContinuous _ _
  · change (G x).rnDeriv (G y) =ᵐ[G y] (fun z => ENNReal.ofReal (L z))
    rw [heq]
    exact Measure.rnDeriv_withDensity _ (by fun_prop)

end AutoSamplingTheory.TechnicalLemmas.Measure.GaussianLikelihood

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Euclidean probabilities and Gaussian heat kernel.	Finite-dimensional real inner-product Borel spaces, including zero dimension.	generalization	Explicit coordinate-free finite-dimensional extension.
Lemma6.3(ii) invokes reverse transport for mixed Gaussian laws.	Actual equal-covariance Gaussian likelihood	API-limitation	Expanded Gaussian prerequisite; mixing/data-processing, general reverse transport and full divergence API remain separate.
Gaussian heat covariance tau I with positive heat time; q>1 for Renyi.	Actual law of a+sqrt(tau)Z, tau>0; real q>1 in power consumer.	same	The covariance, derivative direction and source coefficient are retained.
Gaussian likelihood and high-order integrability implicit in the standard Gaussian ingredient.	Actual volume-density multiplication, RN identity and integrability derived from existing Gaussian facts.	source-implicit	No supplied likelihood, finite moment or nonzero-displacement premise.

Actual equal-covariance Gaussian likelihood/RN and power-moment prerequisite only. No mixture/data-processing inequality, general reverse transport, proxy-warmness, sampler error or query-cost guarantee. The explicit normalized log-moment is not a new packaged divergence API.

Encoder–denoiser: accepted · domain-mismatch

Detected semantic differences

domains: Coordinate-free finite-dimensional and zero-dimensional extension. — Positive dimension omitted; extension explicitly disclosed.
scopes: Expanded Gaussian prerequisite, not the full mixed reverse-transport assertion in Lemma6.3(ii). — Source contract and binding retain independent mixture/data-processing boundary.

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 equal-covariance Gaussian likelihood/RN and power-moment prerequisite only. No mixture/data-processing inequality, general reverse transport, proxy-warmness, sampler error or query-cost guarantee. The explicit normalized log-moment is not a new packaged divergence API.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MeasureTheory.Measure.rnDeriv_withDensity
MeasureTheory.withDensity_mul

Mathematical sources

Chen, Chewi, Lu and Zhang, SPHMC v1 Lemma6.3(ii) — Expanded actual Gaussian ingredient of the stated Winfinity reverse-transport inequality; mixture step separate.

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

The actual translated Gaussian likelihood and RN derivative

Complete source statement (Samplinglib restatement)

Actual likelihood

Read the formalized proofs

The actual translated Gaussian likelihood and RN derivative

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Translate the existing actual Gaussian density

2. Prove actual multiplication of densities

3. Identify absolute continuity and the RN version

Lean verification

Source assumptions versus formal assumptions

Detected semantic differences

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?