Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412

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

  1. The actual translated Gaussian likelihood and RN derivative
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.

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)) := 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

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