Exact integrable Gaussian RN power moment and normalized logarithm
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianPowerMoment.gaussian_power_moment · theorem · Teaching coverage
Mathematical 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).
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*τ)Proof roadmap
- 1Obtain 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.
- 2Pull 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.
- 3Compute 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.
- 4Transfer 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.
- 5Take 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.
Full assumptions and notation
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 verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
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.GaussianPowerMomentSource 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 Gaussian RN power integral and normalized log-moment | 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. — No positive dimension; degenerate scalar Gaussian projection handled by existing APIs.
- scopes: Expanded Gaussian prerequisite, not the full mixed reverse-transport assertion in Lemma6.3(ii). — No mixture/data-processing or packaged divergence identification returned.
- conclusion: Explicit normalized log integral, not a newly proved full divergence API. — Finite explicit RN density a.e. justifies toReal; integrability/integral transfer by a.e. congruence.
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)
- 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.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.