ASTIS mathematical exposition

The actual translated Gaussian likelihood and RN derivative

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

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.}\]

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

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

Lean proof · translated_gaussian_likelihood

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

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

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.

Source and reuse

ASTIS 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.

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