Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
Samplinglib mathematical lesson

Actual PBPS phase Gibbs normalization

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseNormalization.actual_phase_gibbs_normalization · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be a finite-dimensional real inner-product space equipped with its Borel sigma algebra and canonical Lebesgue measure, including dimension d=0. Let V:E→R be C2. Let alpha,beta≥0 with alpha>0 and alpha≤beta, and assume alpha||v||^2 ≤ D2 V(x)[v,v] ≤ beta||v||^2 for every x,v in E, where D2 is the genuine second Frechet derivative. Let eta>0 and beta*eta≤1. For each y in E define Vy(x)=V(x)+||x-y||^2/(2 eta), U_y(x,p)=Vy(x)+||p||^2/2, w_y=exp(-U_y), and ell=volume_E times volume_E in position-momentum order. Define the real position partition Zx(y)=integral exp(-Vy(x)) dx, C_E=(sqrt(2 pi))^d using the natural-number power, and the extended nonnegative phase partition Zphase(y)=integral ofReal(w_y(z)) d ell(z). Let pi_y=volume_E.tilted(-Vy), meaning volume_E.withDensity(x → ofReal(exp(-Vy(x))/Zx(y))). Let nu_y=ell.withDensity(z → Zphase(y)^(-1)*ofReal(w_y(z))) and let gamma be the centered Gaussian on E with identity covariance. Then for every y, all seven assertions hold: exp(-Vy) is integrable; Zx(y)>0; Zphase(y)=ofReal(Zx(y)*C_E); Zphase(y)>0; Zphase(y)<infinity; nu_y is a probability measure; and nu_y=pi_y times gamma exactly as measures on E times E. The real and extended-real integrals are therefore finite before normalization is justified. This identifies the actual phase law rather than a supplied density or normalizer. In dimension zero C_E=1 and the normalized measure is the unit atom on the singleton phase space. No minimizer, critical point, Gaussian envelope, measurability, integrability or finite-mass premise is added. Upper curvature, alpha≤beta and beta*eta≤1 remain as original source assumptions even though this analytic normalization proof needs only the lower curvature, C2 and eta>0. This result does not assert a process law, stationary averaging, countable sector assembly, invariance, a Markov property, hypocoercivity, simulation error, expected oracle cost or whole-paper/composition completion.

\[\frac{e^{-U_y(x,p)}}{Z_x(y)C_E}=\frac{e^{-V_y(x)}}{Z_x(y)}\frac{e^{-\|p\|^2/2}}{C_E},\qquad\nu_y=\pi_y\otimes\gamma.\]
Lean statement · actual_phase_gibbs_normalization

Let E be a finite-dimensional real inner-product space equipped with its Borel sigma algebra and canonical Lebesgue measure, including dimension d=0. Let V:E->R be C2. Let alpha,beta>=0 with alpha>0 and alpha<=beta, and assume alpha||v||^2 <= D2 V(x)[v,v] <= beta||v||^2 for every x,v in E, where D2 is the genuine second Frechet derivative. Let eta>0 and beta*eta<=1. For each y in E define Vy(x)=V(x)+||x-y||^2/(2 eta), U_y(x,p)=Vy(x)+||p||^2/2, w_y=exp(-U_y), and ell=volume_E times volume_E in position-momentum order. Define the real position partition Zx(y)=integral exp(-Vy(x)) dx, C_E=(sqrt(2 pi))^d using the natural-number power, and the extended nonnegative phase partition Zphase(y)=integral ofReal(w_y(z)) d ell(z). Let pi_y=volume_E.tilted(-Vy), meaning volume_E.withDensity(x -> ofReal(exp(-Vy(x))/Zx(y))). Let nu_y=ell.withDensity(z -> Zphase(y)^(-1)*ofReal(w_y(z))) and let gamma be the centered Gaussian on E with identity covariance. Then for every y, all seven assertions hold: exp(-Vy) is integrable; Zx(y)>0; Zphase(y)=ofReal(Zx(y)*C_E); Zphase(y)>0; Zphase(y)<infinity; nu_y is a probability measure; and nu_y=pi_y times gamma exactly as measures on E times E. The real and extended-real integrals are therefore finite before normalization is justified. This identifies the actual phase law rather than a supplied density or normalizer. In dimension zero C_E=1 and the normalized measure is the unit atom on the singleton phase space. No minimizer, critical point, Gaussian envelope, measurability, integrability or finite-mass premise is added. Upper curvature, alpha<=beta and beta*eta<=1 remain as original source assumptions even though this analytic normalization proof needs only the lower curvature, C2 and eta>0. This result does not assert a process law, stationary averaging, countable sector assembly, invariance, a Markov property, hypocoercivity, simulation error, expected oracle cost or whole-paper/composition completion.

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 actual_phase_gibbs_normalization
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E,
      (α : ℝ) * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β : ℝ) * ‖v‖ ^ 2)
    (hη : 0 < η) (hβη : (β : ℝ) * η ≤ 1) : actual_phase_normalization_statement hα hαβ hV hH hη hβη

Exact module and namespace context

Full Lean proposition (definition) · actual_phase_normalization_statement

This literal definition stores the complete proposition asserted above. It supplies no mathematical proof or additional hypothesis; the theorem proof must establish its value.

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)
private def actual_phase_normalization_statement
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E,
      (α : ℝ) * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β : ℝ) * ‖v‖ ^ 2)
    (hη : 0 < η) (hβη : (β : ℝ) * η ≤ 1) : Prop := by
  classical
  exact
    let d : ℕ := Module.finrank ℝ E
    let Vy : E → E → ℝ := fun y x => V x + ‖x - y‖ ^ 2 / (2 * η)
    let U : E → E × E → ℝ := fun y z =>
      V z.1 + ‖z.1 - y‖ ^ 2 / (2 * η) + ‖z.2‖ ^ 2 / 2
    let w : E → E × E → ℝ := fun y z => Real.exp (-U y z)
    let ell : Measure (E × E) := (volume : Measure E).prod (volume : Measure E)
    let Zx : E → ℝ := fun y => ∫ x : E, Real.exp (-Vy y x) ∂volume
    let C : ℝ := (Real.sqrt (2 * Real.pi)) ^ d
    let Zphase : E → ℝ≥0∞ := fun y => ∫⁻ z, ENNReal.ofReal (w y z) ∂ell
    let piY : E → Measure E := fun y => (volume : Measure E).tilted (fun x => -Vy y x)
    let nu : E → Measure (E × E) := fun y =>
      ell.withDensity (fun z => (Zphase y)⁻¹ * ENNReal.ofReal (w y z))
    let gamma : Measure E := ProbabilityTheory.stdGaussian E
    ∀ y : E,
      Integrable (fun x => Real.exp (-Vy y x)) (volume : Measure E) ∧
      0 < Zx y ∧
      Zphase y = ENNReal.ofReal (Zx y * C) ∧
      0 < Zphase y ∧
      Zphase y < ⊤ ∧
      IsProbabilityMeasure (nu y) ∧
      nu y = (piY y).prod gamma

Exact module and namespace context

Proof roadmap

  1. 1Obtain the integrable Gibbs tail

    The genuine Hessian lower bound and C2 regularity imply alpha-strong convexity. The existing positive-modulus Gibbs integrability theorem uses a quadratic envelope and requires no supplied minimizing or critical point.

  2. 2Control every conditional position partition

    For each y, eta>0 makes the proximal quadratic nonnegative, hence 0<exp(-Vy)≤exp(-V). Continuity yields measurability; domination proves integrability. Strict positivity of the exponential and nonzero canonical volume then give Zx>0, including dimension zero.

  3. 3Evaluate the Gaussian momentum factor

    Apply the canonical Gaussian integral with coefficient 1/2. Convert its real power to the natural-number power of sqrt(2 pi). The resulting positive factor is C_E; no variance eta appears in momentum.

  4. 4Factor the actual phase partition

    The target energy is additive in position and momentum. Exponentiation factors its weight, and nonnegative product integration separates the two factors in position-first order. Integrability of the position factor permits the real-to-ENNReal integral conversion.

  5. 5Normalize only after positivity and finiteness

    Both real factors are positive, and ofReal of a real number is finite. The existing Gibbs withDensity theorem now proves that the reciprocal-partition density has total mass one. No finite-mass premise was supplied.

  6. 6Identify standard Gaussian momentum

    Specialize the existing isotropic Gaussian density theorem to variance one. Scaling by sqrt(1) is the identity map, so the Gaussian density is C_E inverse times exp(-||p||^2/2). This also covers d=0.

  7. 7Match the normalized product density

    Expand the tilted position measure and use product-withDensity for the two measurable densities. Substitute the exact phase partition and factorized energy. Positivity and finite ofReal factors justify division and inversion; commutativity then identifies the densities pointwise and hence the measures.

Full assumptions and notation

All objects and hypotheses

  • Finite-dimensional real inner-product Borel E with canonical volume, including dimension zero.
  • alpha,beta≥0; alpha>0; alpha≤beta; V is C2; alpha||v||^2≤D2V(x)[v,v]≤beta||v||^2 for every x,v.
  • eta>0 and beta*eta≤1. All conclusions hold for every y in E.
  • Literal conditional and phase energies, real Zx, ENNReal Zphase, C_E=(sqrt(2 pi))^d, tilted position law and standard Gaussian momentum. No extra integrability, normalizer, minimizing point or regularity premise.

Mathematical proof

1. Obtain the integrable Gibbs tail

The genuine Hessian lower bound and C2 regularity imply alpha-strong convexity. The existing positive-modulus Gibbs integrability theorem uses a quadratic envelope and requires no supplied minimizing or critical point.

\[D^2V\succeq\alpha I,\quad\alpha>0\quad\Longrightarrow\quad e^{-V}\in L^1(dx).\]
Corresponding Lean step
  have hsc := AutoSamplingTheory.TechnicalLemmas.Analysis.HessianStrongConvexity.strongConvexOn_univ_of_fderiv2_lower hV (fun x v => (hH x v).1)
  have hbase := AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexGibbsIntegrability.integrable_exp_neg_of_strongConvexOn hα (hV.differentiable (by norm_num)) hsc

ASTIS completion of the phase-law proportionality. Exact compiled region; every analytic ingredient is derived from the original assumptions.

2. Control every conditional position partition

For each y, eta>0 makes the proximal quadratic nonnegative, hence 0<exp(-Vy)≤exp(-V). Continuity yields measurability; domination proves integrability. Strict positivity of the exponential and nonzero canonical volume then give Zx>0, including dimension zero.

\[V_y\ge V,\qquad 0<e^{-V_y}\le e^{-V},\qquad 0<Z_x(y)=\int e^{-V_y(x)}\,dx<\infty.\]
Corresponding Lean step
  have hVy : Continuous Vy := hV.continuous.add (((continuous_id.sub continuous_const).norm.pow 2).div_const (2 * η))
  have hfc : Continuous f := Real.continuous_exp.comp hVy.neg
  have hgc : Continuous g := Real.continuous_exp.comp ((continuous_norm.pow 2).neg.div_const 2)
  have hf : Integrable f (volume : Measure E) := by
    refine hbase.mono' hfc.aestronglyMeasurable ?_
    filter_upwards with x
    rw [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)]
    apply Real.exp_le_exp.mpr
    dsimp [Vy]
    have : 0 ≤ ‖x - y‖ ^ 2 / (2 * η) := by positivity
    linarith
  have hZ : 0 < Z := integral_exp_pos hf

ASTIS completion of the phase-law proportionality. Exact compiled region; every analytic ingredient is derived from the original assumptions.

3. Evaluate the Gaussian momentum factor

Apply the canonical Gaussian integral with coefficient 1/2. Convert its real power to the natural-number power of sqrt(2 pi). The resulting positive factor is C_E; no variance eta appears in momentum.

\[\int e^{-\|p\|^2/2}\,dp=(2\pi)^{d/2}=(\sqrt{2\pi})^d=C_E>0.\]
Corresponding Lean step
  have hC : 0 < C := by dsimp [C]; positivity
  have hCg : (∫⁻ p : E, ENNReal.ofReal (g p) ∂volume) = ENNReal.ofReal C := by
    have h := AutoSamplingTheory.TechnicalLemmas.Analysis.Integrability.lintegral_exp_neg_mul_norm_sq_eq (E := E) (a := (1 / 2 : ℝ)) (by norm_num)
    have hn : (Real.pi / (1 / 2 : ℝ)) ^ ((Module.finrank ℝ E : ℝ) / 2) = C := by
      dsimp [C]
      rw [Real.sqrt_eq_rpow, ← Real.rpow_mul_natCast (by positivity)]
      congr 1 <;> ring
    rw [hn] at h
    convert h using 1
    congr 1
    funext p
    congr 2
    dsimp [g]
    ring

ASTIS completion of the phase-law proportionality. Exact compiled region; every analytic ingredient is derived from the original assumptions.

4. Factor the actual phase partition

The target energy is additive in position and momentum. Exponentiation factors its weight, and nonnegative product integration separates the two factors in position-first order. Integrability of the position factor permits the real-to-ENNReal integral conversion.

\[e^{-U_y(x,p)}=e^{-V_y(x)}e^{-\|p\|^2/2},\qquad Z_{\rm phase}(y)=\operatorname{ofReal}(Z_x(y)C_E).\]
Corresponding Lean step
  have hw (z : E × E) : Real.exp (-U z) = f z.1 * g z.2 := by
    dsimp [U, f, g, Vy]
    rw [← Real.exp_add]
    congr 1
    ring
  have hphase : Zp = ENNReal.ofReal (Z * C) := by
    calc
      Zp = ∫⁻ z : E × E, ENNReal.ofReal (f z.1) * ENNReal.ofReal (g z.2) ∂ell := by
        apply lintegral_congr
        intro z
        rw [hw, ENNReal.ofReal_mul (Real.exp_nonneg _)]
      _ = (∫⁻ x : E, ENNReal.ofReal (f x) ∂volume) * ∫⁻ p : E, ENNReal.ofReal (g p) ∂volume :=
        lintegral_prod_mul hfc.measurable.ennreal_ofReal.aemeasurable hgc.measurable.ennreal_ofReal.aemeasurable
      _ = ENNReal.ofReal (Z * C) := by
        rw [← ofReal_integral_eq_lintegral_ofReal hf (ae_of_all _ (fun x => Real.exp_nonneg _)), hCg, ← ENNReal.ofReal_mul hZ.le]

ASTIS completion of the phase-law proportionality. Exact compiled region; every analytic ingredient is derived from the original assumptions.

5. Normalize only after positivity and finiteness

Both real factors are positive, and ofReal of a real number is finite. The existing Gibbs withDensity theorem now proves that the reciprocal-partition density has total mass one. No finite-mass premise was supplied.

\[0<Z_{\rm phase}(y)<\infty,\qquad \nu_y=\ell\mathbin{.}\mathrm{withDensity}(Z_{\rm phase}(y)^{-1}e^{-U_y}),\quad\nu_y(E\times E)=1.\]
Corresponding Lean step
  have hpos : 0 < Zp := by rw [hphase]; exact ENNReal.ofReal_pos.mpr (mul_pos hZ hC)
  have hfin : Zp < ⊤ := by rw [hphase]; exact ENNReal.ofReal_lt_top
  have hprob : IsProbabilityMeasure (ell.withDensity (fun z => Zp⁻¹ * ENNReal.ofReal (Real.exp (-U z)))) :=
    AutoSamplingTheory.TechnicalLemmas.Measure.Gibbs.isProbabilityMeasure_withDensity_normalized_gibbs ell U hpos.ne' hfin.ne
  refine ⟨hf, hZ, hphase, hpos, hfin, hprob, ?_⟩

ASTIS completion of the phase-law proportionality. Exact compiled region; every analytic ingredient is derived from the original assumptions.

6. Identify standard Gaussian momentum

Specialize the existing isotropic Gaussian density theorem to variance one. Scaling by sqrt(1) is the identity map, so the Gaussian density is C_E inverse times exp(-||p||^2/2). This also covers d=0.

\[\gamma=dp\mathbin{.}\mathrm{withDensity}\bigl(\operatorname{ofReal}(C_E^{-1}e^{-\|p\|^2/2})\bigr).\]
Corresponding Lean step
  have hgamma : stdGaussian E = (volume : Measure E).withDensity (fun p => ENNReal.ofReal (C⁻¹ * g p)) := by
    have h := AutoSamplingTheory.TechnicalLemmas.Measure.IsotropicGaussianDensity.map_sqrt_smul_stdGaussian_eq_withDensity (E := E) 1 (by norm_num)
    have hid : (fun z : E => Real.sqrt 1 • z) = id := by funext z; simp
    rw [hid, Measure.map_id] at h
    simpa only [mul_one, inv_pow, C, g] using h

ASTIS completion of the phase-law proportionality. Exact compiled region; every analytic ingredient is derived from the original assumptions.

7. Match the normalized product density

Expand the tilted position measure and use product-withDensity for the two measurable densities. Substitute the exact phase partition and factorized energy. Positivity and finite ofReal factors justify division and inversion; commutativity then identifies the densities pointwise and hence the measures.

\[\frac{e^{-U_y(x,p)}}{Z_x(y)C_E}=\frac{e^{-V_y(x)}}{Z_x(y)}\frac{e^{-\|p\|^2/2}}{C_E},\qquad\nu_y=\pi_y\otimes\gamma.\]
Corresponding Lean step
  rw [hgamma, Measure.tilted, prod_withDensity ((hfc.measurable.div_const Z).ennreal_ofReal) ((hgc.measurable.const_mul C⁻¹).ennreal_ofReal)]
  apply withDensity_congr_ae
  filter_upwards with z
  rw [hphase, hw, ENNReal.ofReal_mul hZ.le, ENNReal.ofReal_mul (Real.exp_nonneg _), ENNReal.ofReal_div_of_pos hZ, ENNReal.ofReal_mul (inv_nonneg.mpr hC.le), ENNReal.ofReal_inv_of_pos hC]
  rw [ENNReal.mul_inv (Or.inr ENNReal.ofReal_ne_top) (Or.inl ENNReal.ofReal_ne_top)]
  simp only [div_eq_mul_inv, f]
  ac_rfl

ASTIS completion of the phase-law proportionality. Exact compiled region; every analytic ingredient is derived from the original assumptions.

Lean verification

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

Lean proof · actual_phase_gibbs_normalization

Obtain the integrable Gibbs tail; Control every conditional position partition; Evaluate the Gaussian momentum factor; Factor the actual phase partition; Normalize only after positivity and finiteness; Identify standard Gaussian momentum; Match the normalized product density

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 actual_phase_gibbs_normalization
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E,
      (α : ℝ) * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β : ℝ) * ‖v‖ ^ 2)
    (hη : 0 < η) (hβη : (β : ℝ) * η ≤ 1) : actual_phase_normalization_statement hα hαβ hV hH hη hβη := by

  dsimp only [actual_phase_normalization_statement]
  intro y
  let Vy : E → ℝ := fun x => V x + ‖x - y‖ ^ 2 / (2 * η)
  let U : E × E → ℝ := fun z => V z.1 + ‖z.1 - y‖ ^ 2 / (2 * η) + ‖z.2‖ ^ 2 / 2
  let f : E → ℝ := fun x => Real.exp (-Vy x)
  let g : E → ℝ := fun p => Real.exp (-‖p‖ ^ 2 / 2)
  let C : ℝ := (Real.sqrt (2 * Real.pi)) ^ Module.finrank ℝ E
  let Z : ℝ := ∫ x, f x ∂(volume : Measure E)
  let ell : Measure (E × E) := (volume : Measure E).prod (volume : Measure E)
  let Zp : ℝ≥0∞ := ∫⁻ z, ENNReal.ofReal (Real.exp (-U z)) ∂ell
  change Integrable f volume ∧ 0 < Z ∧ Zp = ENNReal.ofReal (Z * C) ∧
    0 < Zp ∧ Zp < ⊤ ∧
    IsProbabilityMeasure (ell.withDensity (fun z => Zp⁻¹ * ENNReal.ofReal (Real.exp (-U z)))) ∧
    ell.withDensity (fun z => Zp⁻¹ * ENNReal.ofReal (Real.exp (-U z))) =
      ((volume : Measure E).tilted (fun x => -Vy x)).prod (stdGaussian E)
  have hsc := AutoSamplingTheory.TechnicalLemmas.Analysis.HessianStrongConvexity.strongConvexOn_univ_of_fderiv2_lower hV (fun x v => (hH x v).1)
  have hbase := AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexGibbsIntegrability.integrable_exp_neg_of_strongConvexOn hα (hV.differentiable (by norm_num)) hsc
  have hVy : Continuous Vy := hV.continuous.add (((continuous_id.sub continuous_const).norm.pow 2).div_const (2 * η))
  have hfc : Continuous f := Real.continuous_exp.comp hVy.neg
  have hgc : Continuous g := Real.continuous_exp.comp ((continuous_norm.pow 2).neg.div_const 2)
  have hf : Integrable f (volume : Measure E) := by
    refine hbase.mono' hfc.aestronglyMeasurable ?_
    filter_upwards with x
    rw [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)]
    apply Real.exp_le_exp.mpr
    dsimp [Vy]
    have : 0 ≤ ‖x - y‖ ^ 2 / (2 * η) := by positivity
    linarith
  have hZ : 0 < Z := integral_exp_pos hf
  have hC : 0 < C := by dsimp [C]; positivity
  have hCg : (∫⁻ p : E, ENNReal.ofReal (g p) ∂volume) = ENNReal.ofReal C := by
    have h := AutoSamplingTheory.TechnicalLemmas.Analysis.Integrability.lintegral_exp_neg_mul_norm_sq_eq (E := E) (a := (1 / 2 : ℝ)) (by norm_num)
    have hn : (Real.pi / (1 / 2 : ℝ)) ^ ((Module.finrank ℝ E : ℝ) / 2) = C := by
      dsimp [C]
      rw [Real.sqrt_eq_rpow, ← Real.rpow_mul_natCast (by positivity)]
      congr 1 <;> ring
    rw [hn] at h
    convert h using 1
    congr 1
    funext p
    congr 2
    dsimp [g]
    ring
  have hw (z : E × E) : Real.exp (-U z) = f z.1 * g z.2 := by
    dsimp [U, f, g, Vy]
    rw [← Real.exp_add]
    congr 1
    ring
  have hphase : Zp = ENNReal.ofReal (Z * C) := by
    calc
      Zp = ∫⁻ z : E × E, ENNReal.ofReal (f z.1) * ENNReal.ofReal (g z.2) ∂ell := by
        apply lintegral_congr
        intro z
        rw [hw, ENNReal.ofReal_mul (Real.exp_nonneg _)]
      _ = (∫⁻ x : E, ENNReal.ofReal (f x) ∂volume) * ∫⁻ p : E, ENNReal.ofReal (g p) ∂volume :=
        lintegral_prod_mul hfc.measurable.ennreal_ofReal.aemeasurable hgc.measurable.ennreal_ofReal.aemeasurable
      _ = ENNReal.ofReal (Z * C) := by
        rw [← ofReal_integral_eq_lintegral_ofReal hf (ae_of_all _ (fun x => Real.exp_nonneg _)), hCg, ← ENNReal.ofReal_mul hZ.le]
  have hpos : 0 < Zp := by rw [hphase]; exact ENNReal.ofReal_pos.mpr (mul_pos hZ hC)
  have hfin : Zp < ⊤ := by rw [hphase]; exact ENNReal.ofReal_lt_top
  have hprob : IsProbabilityMeasure (ell.withDensity (fun z => Zp⁻¹ * ENNReal.ofReal (Real.exp (-U z)))) :=
    AutoSamplingTheory.TechnicalLemmas.Measure.Gibbs.isProbabilityMeasure_withDensity_normalized_gibbs ell U hpos.ne' hfin.ne
  refine ⟨hf, hZ, hphase, hpos, hfin, hprob, ?_⟩
  have hgamma : stdGaussian E = (volume : Measure E).withDensity (fun p => ENNReal.ofReal (C⁻¹ * g p)) := by
    have h := AutoSamplingTheory.TechnicalLemmas.Measure.IsotropicGaussianDensity.map_sqrt_smul_stdGaussian_eq_withDensity (E := E) 1 (by norm_num)
    have hid : (fun z : E => Real.sqrt 1 • z) = id := by funext z; simp
    rw [hid, Measure.map_id] at h
    simpa only [mul_one, inv_pow, C, g] using h
  rw [hgamma, Measure.tilted, prod_withDensity ((hfc.measurable.div_const Z).ennreal_ofReal) ((hgc.measurable.const_mul C⁻¹).ennreal_ofReal)]
  apply withDensity_congr_ae
  filter_upwards with z
  rw [hphase, hw, ENNReal.ofReal_mul hZ.le, ENNReal.ofReal_mul (Real.exp_nonneg _), ENNReal.ofReal_div_of_pos hZ, ENNReal.ofReal_mul (inv_nonneg.mpr hC.le), ENNReal.ofReal_inv_of_pos hC]
  rw [ENNReal.mul_inv (Or.inr ENNReal.ofReal_ne_top) (Or.inl ENNReal.ofReal_ne_top)]
  simp only [div_eq_mul_inv, f]
  ac_rfl

#print axioms actual_phase_gibbs_normalization
end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseNormalization

Exact module and namespace context

Scope and omitted-condition boundaries
  • Exact phase probability normalization and product-law identity only; no process invariance, countable sector assembly, Markov property, hypocoercivity, implementation error, cost or main theorem completion.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • Integrable.mono'
  • integral_exp_pos
  • lintegral_prod_mul
  • ofReal_integral_eq_lintegral_ofReal
  • Real.rpow_mul_natCast
  • Measure.tilted
  • prod_withDensity
  • withDensity_congr_ae
  • ENNReal.mul_inv

Mathematical sources

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