Exact integrable Gaussian RN power moment and normalized logarithm
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianPowerMoment.gaussian_power_moment · theorem · Teaching coverage
Statement
For the same actual G_x,G_y on a finite-dimensional real inner-product Borel space, tau>0 and real q>1, retain the measurable likelihood L, actual withDensity equality, absolute continuity and RN identity. The qth power of the real-valued RN derivative is integrable under G_y, its integral is exp(q(q-1)norm(x-y)^2/(2tau)), and the logarithm of this integral divided by q-1 equals q norm(x-y)^2/(2tau).
All objects and hypotheses
- Same actual translated/scaled Gaussian laws, finite-dimensional real inner-product Borel E including dimension zero, tau>0 and arbitrary x,y.
- Real q>1, not just natural q. No nonzero displacement or positive dimension is assumed.
- No likelihood, Gaussian moment formula or integrability hypothesis is supplied. The RN toReal use is justified by equality to a finite explicit density a.e.
- The raw normalized log-moment is the equal-covariance Gaussian quantity needed for the source argument; mixing over a coupling and data processing remain separate.
Mathematical proof
1. Obtain a genuine one-dimensional projection law
For h=x-y, the continuous linear functional ell(z)=inner(h,z) sends standard Gaussian to a real Gaussian of mean zero and variance norm(h)^2. The existing one-dimensional exponential integrability and MGF theorem yield both an integrability fact and the exact integral.
Corresponding Lean step
Local linear_exp uses IsGaussian.map_eq_gaussianReal, integral_strongDual_stdGaussian, variance_dual_stdGaussian, integrable_exp_mul_gaussianReal and mgf_gaussianReal.
2. Pull the actual likelihood power back to standard Gaussian
Set s=sqrt(tau), a=q/s and b=-q norm(h)^2/(2tau). Under the actual map z=y+sZ, real exponentiation gives L(z)^q=exp(b) exp(a inner(h,Z)). The map is measurable and the projected exponential is integrable, so the actual pushed-forward power is integrable.
Corresponding Lean step
Real.exp_mul, inner_smul_right, s^2=tau and integrable_map_measure establish the exact pullback and integrability.
3. Compute the exact power moment
Use integral_map, take out exp(b), and substitute the one-dimensional MGF. The exponent b+a^2 norm(h)^2/2 simplifies to q(q-1)norm(h)^2/(2tau). Strictly positive tau justifies all reciprocal square-root operations.
Corresponding Lean step
Local power_moment returns integrability and equality together, with no assumed moment budget.
4. Transfer the result to the genuine RN derivative
Apply the shared likelihood theorem to the same x,y,tau. Its a.e. RN equality and finite exponential density identify the qth powers after toReal. Transfer integrability and the integral by a.e. congruence.
Corresponding Lean step
ENNReal.toReal_ofReal, Integrable.congr and integral_congr_ae use the actual RN equality, avoiding any inference from totalized infinite values.
5. Take the normalized logarithm without changing constants
The exact integral is a positive exponential. Its logarithm equals the computed exponent; q>1 makes q-1 nonzero, yielding the exact Gaussian reverse-transport coefficient. Zero displacement or dimension gives moment one and logarithm zero.
Corresponding Lean step
Real.log_exp and positive-order cancellation. No marginal mixture or sampler assertion is returned.
Lean statement · gaussian_power_moment
Actual RN power integrability, exact integral and normalized log-moment, together with the same genuine Gaussian likelihood certificate.
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 gaussian_power_moment {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
(x y : E) (τ q : ℝ) (hτ : 0 < τ) (hq : 1 < q) :
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)) ∧
Integrable (fun z => ((G x).rnDeriv (G y) z).toReal ^ q) (G y) ∧
(∫ z, ((G x).rnDeriv (G y) z).toReal ^ q ∂G y) =
Real.exp (q*(q-1)*‖x-y‖^2/(2*τ)) ∧
Real.log (∫ z, ((G x).rnDeriv (G y) z).toReal ^ q ∂G y) / (q-1) =
q*‖x-y‖^2/(2*τ)Lean proof · gaussian_power_moment
The one-dimensional projection/MGF and actual power integration helpers are local; the shared public likelihood theorem provides the RN identification.
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 gaussian_power_moment {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
(x y : E) (τ q : ℝ) (hτ : 0 < τ) (hq : 1 < q) :
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)) ∧
Integrable (fun z => ((G x).rnDeriv (G y) z).toReal ^ q) (G y) ∧
(∫ z, ((G x).rnDeriv (G y) z).toReal ^ q ∂G y) =
Real.exp (q*(q-1)*‖x-y‖^2/(2*τ)) ∧
Real.log (∫ z, ((G x).rnDeriv (G y) z).toReal ^ q ∂G y) / (q-1) =
q*‖x-y‖^2/(2*τ) := by
have linear_exp
(h : E) (a : ℝ) :
Integrable (fun z : E => Real.exp (a * inner ℝ h z)) (stdGaussian E) ∧
(∫ z : E, Real.exp (a * inner ℝ h z) ∂stdGaussian E) =
Real.exp (a^2 * ‖h‖^2 / 2) := by
let l : StrongDual ℝ E := innerSL ℝ h
have hmap : (stdGaussian E).map l = gaussianReal 0 (‖h‖^2).toNNReal := by
rw [IsGaussian.map_eq_gaussianReal l,integral_strongDual_stdGaussian,
variance_dual_stdGaussian]
simp only [l,innerSL_apply_norm]
have hI := integrable_exp_mul_gaussianReal (μ := 0) (v := (‖h‖^2).toNNReal) a
rw [← hmap] at hI
have hI' := (integrable_map_measure (by fun_prop) (by fun_prop : AEMeasurable l (stdGaussian E))).mp hI
refine ⟨hI',?_⟩
have hm := mgf_gaussianReal hmap a
simpa [mgf,l,Real.toNNReal_of_nonneg (sq_nonneg ‖h‖),mul_comm] using hm
have power_moment
(x y : E) (τ q : ℝ) (hτ : 0 < τ) (hq : 1 < q) :
let G := (stdGaussian E).map (fun z => y + Real.sqrt τ • z)
let L := fun z : E => Real.exp (inner ℝ (x-y) (z-y) / τ - ‖x-y‖ ^ 2 / (2*τ))
Integrable (fun z => L z ^ q) G ∧
(∫ z, L z ^ q ∂G) = Real.exp (q*(q-1)*‖x-y‖^2/(2*τ)) := by
let G := (stdGaussian E).map (fun z => y + Real.sqrt τ • z)
let L := fun z : E => Real.exp (inner ℝ (x-y) (z-y) / τ - ‖x-y‖ ^ 2 / (2*τ))
let s := Real.sqrt τ
have hs : 0 < s := Real.sqrt_pos.mpr hτ
have hs2 : s^2 = τ := Real.sq_sqrt hτ.le
let a := q / s
let b := -q * ‖x-y‖^2 / (2*τ)
have hq0 : 0 ≤ q := by linarith
have hfunc : (fun z : E => L (y + Real.sqrt τ • z)^q) =
(fun z => Real.exp b * Real.exp (a * inner ℝ (x-y) z)) := by
funext z
dsimp only [L]
rw [← Real.exp_mul,← Real.exp_add]
congr 1
simp only [add_sub_cancel_left,inner_smul_right]
change (s * inner ℝ (x-y) z / τ - ‖x-y‖^2/(2*τ))*q = b + a * inner ℝ (x-y) z
dsimp only [a,b]
rw [← hs2]
field_simp
ring
obtain ⟨hI,hm⟩ := linear_exp (x-y) a
have hpull : Integrable (fun z : E => L (y + Real.sqrt τ • z)^q) (stdGaussian E) := by
rw [hfunc]
exact hI.const_mul _
have hLG : Integrable (fun z : E => L z ^ q) G :=
(integrable_map_measure (by fun_prop) (by fun_prop)).mpr hpull
refine ⟨hLG,?_⟩
change (∫ z, L z ^ q ∂G) = _
dsimp only [G]
rw [integral_map (by fun_prop) (by fun_prop)]
change (∫ z : E, L (y + Real.sqrt τ • z)^q ∂stdGaussian E) = _
rw [hfunc,integral_const_mul,hm,← Real.exp_add]
congr 1
dsimp only [a,b]
rw [← hs2]
field_simp
ring
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*τ))
obtain ⟨hL,heq,hAC,hRN⟩ := GaussianLikelihood.translated_gaussian_likelihood x y τ hτ
change (G x).rnDeriv (G y) =ᵐ[G y] (fun z => ENNReal.ofReal (L z)) at hRN
obtain ⟨hI,hm⟩ := power_moment x y τ q hτ hq
have hpow : (fun z => ((G x).rnDeriv (G y) z).toReal ^ q) =ᵐ[G y] (fun z => L z ^ q) := by
filter_upwards [hRN] with z hz
rw [hz,ENNReal.toReal_ofReal (Real.exp_nonneg _)]
have hIRN : Integrable (fun z => ((G x).rnDeriv (G y) z).toReal ^ q) (G y) := hI.congr hpow.symm
have hval : (∫ z, ((G x).rnDeriv (G y) z).toReal ^ q ∂G y) =
Real.exp (q*(q-1)*‖x-y‖^2/(2*τ)) := (integral_congr_ae hpow).trans hm
refine ⟨hL,heq,hAC,hRN,hIRN,hval,?_⟩
change Real.log (∫ z, ((G x).rnDeriv (G y) z).toReal ^ q ∂G y) / (q-1) = _
rw [hval,Real.log_exp]
have hq1 : q-1 ≠ 0 := by linarith
field_simp
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianPowerMomentScope 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)
- ProbabilityTheory.IsGaussian.map_eq_gaussianReal
- ProbabilityTheory.mgf_gaussianReal
- ProbabilityTheory.integrable_exp_mul_gaussianReal
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.