Bochner energy under the actual reflected conditional Gibbs kernel
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalBochner.conditional_bochner_energy · theorem · Teaching coverage
Mathematical statement
For the actual Gibbs-Gaussian augmentation there are common Markov kernels R,S: R disintegrates the swapped joint law and S_y is the reflected pushforward of R_y. Every S_y is normalized exp(-W_y) times volume, W_y(u)=V((y+u)/2)+norm(u-y)^2/(8 eta), with W_y C2 and finite strictly positive normalizer. For every smooth compactly supported f, the square of L_y f, squared gradient, coordinate Hessian-square term and genuine conditional curvature term are integrable under this same S_y. The exact normalized Bochner identity holds, and the square-generator energy bounds ((alpha+eta inverse)/4) times the gradient energy.
Lean statement · conditional_bochner_energy
Common actual kernels, density and finite positive normalizer precede the universal compact-test integrability, identity and exact energy inequality.
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 conditional_bochner_energy {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
{V : E → ℝ} {α β : NNReal} {η : ℝ}
(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) :
let μ := (volume : Measure E).tilted (fun x => -V x)
let J := Measure.map (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2)) (μ.prod (stdGaussian E))
let W := fun y u : E => V ((1/2:ℝ) • (y+u)) + ‖u-y‖^2/(8*η)
∃ R S : Kernel E E, IsMarkovKernel R ∧ IsMarkovKernel S ∧
(J.map Prod.swap).IsCondKernel R ∧
(∀ y, S y = (R y).map (fun x => (2:ℝ) • x-y)) ∧
∀ y, S y = (volume : Measure E).tilted (fun u => -W y u) ∧
ContDiff ℝ 2 (W y) ∧ Integrable (fun u => Real.exp (-W y u)) ∧
0 < (∫ u, Real.exp (-W y u)) ∧
∀ f : E → ℝ, ContDiff ℝ ∞ f → HasCompactSupport f →
let L := fun u => Laplacian.laplacian f u - inner ℝ (gradient (W y) u) (gradient f u)
let H := fun u => ∑ i, ‖gradient (fun z => fderiv ℝ f z ((stdOrthonormalBasis ℝ E) i)) u‖^2
let C := fun u => fderiv ℝ (fderiv ℝ (W y)) u (gradient f u) (gradient f u)
Integrable (fun u => (L u)^2) (S y) ∧
Integrable (fun u => ‖gradient f u‖^2) (S y) ∧
Integrable H (S y) ∧ Integrable C (S y) ∧
(∫ u, (L u)^2 ∂S y) = (∫ u, H u ∂S y) + ∫ u, C u ∂S y ∧
(((α:ℝ)+1/η)/4) * (∫ u, ‖gradient f u‖^2 ∂S y) ≤ ∫ u, (L u)^2 ∂S yProof roadmap
- 1Keep one actual conditional kernel
Use ConditionalScoreDomain to obtain common R,S, their Markov properties, disintegration and reflected pushforward. For each y it provides exactly S_y=volume tilted by -W_y, W_y C2 and the genuine lower curvature (alpha+eta inverse)/4. Do not replace S_y by an unrelated measure with an assumed curvature inequality.
- 2Prove the global normalizer is finite and positive
The shared compact-test identity alone cannot prove global weight integrability. Instead, S_y is already an actual probability measure and equals the tilt. If exp(-W_y) were not integrable, Mathlib tilt would be the zero measure, contradicting S_y(univ)=1. Thus the weight is integrable. Its pointwise strict positivity and nonzero volume make Z_y strictly positive. This rules out a totalized zero-measure normalization.
- 3Transport the full identity and every integral domain
Apply the actual shared Bochner theorem to W_y and f. It supplies all four weighted Integrable facts and the raw identity. The tilted-integrability equivalence transfers each fact to this same S_y. For every integrand g, the exact tilted integral equals Z_y inverse times the weighted volume integral, so multiplying the raw identity gives the normalized identity.
- 4Use the actual conditional curvature constant
Apply the shared curvature-energy consequence to the inherited genuine Hessian lower bound, then multiply by positive Z_y inverse. This yields precisely (alpha+eta inverse)/4 times the S_y gradient energy. It remains a compact-test square-generator estimate. Constructing a weighted closed core/range or resolvent and extending to noncompact scores are still necessary before claiming conditional Poincare or score variance.
Full assumptions and notation
All objects and hypotheses
- E is finite-dimensional real inner-product with Borel structure and canonical volume, including dimension zero. V:E→R is C2.
- Alpha,beta are finite nonnegative real parameters with explicit 0<alpha≤beta and genuine alpha/beta Hessian quadratic-form bounds on V.
- Eta>0 and beta eta≤1 are retained from the ConditionalScoreDomain parent interface. The upper scale and upper curvature restrictions are not needed by the abstract Bochner identity; they are not removed from this conditional consumer.
- Mu is volume tilted by -V; J is the law of (X,X+sqrt(eta)Z) from independent X~mu and standard Gaussian Z. The same constructed R,S work for every y and every smooth compactly supported f.
- No probability, conditional density, global normalizer, integrability, integration-by-parts or Poincare premise is silently added; they are derived where claimed.
Mathematical proof
1. Keep one actual conditional kernel
Use ConditionalScoreDomain to obtain common R,S, their Markov properties, disintegration and reflected pushforward. For each y it provides exactly S_y=volume tilted by -W_y, W_y C2 and the genuine lower curvature (alpha+eta inverse)/4. Do not replace S_y by an unrelated measure with an assumed curvature inequality.
Corresponding Lean step
conditional_curvature_and_score_domain supplies the same existential witnesses; the consumer retains hR,hS,hcond,hSR,hSy and hcurv.
2. Prove the global normalizer is finite and positive
The shared compact-test identity alone cannot prove global weight integrability. Instead, S_y is already an actual probability measure and equals the tilt. If exp(-W_y) were not integrable, Mathlib tilt would be the zero measure, contradicting S_y(univ)=1. Thus the weight is integrable. Its pointwise strict positivity and nonzero volume make Z_y strictly positive. This rules out a totalized zero-measure normalization.
Corresponding Lean step
hweight contradicts tilted_of_not_integrable using the Markov probability mass. integral_exp_pos gives hZ before any normalized inequality is transferred.
3. Transport the full identity and every integral domain
Apply the actual shared Bochner theorem to W_y and f. It supplies all four weighted Integrable facts and the raw identity. The tilted-integrability equivalence transfers each fact to this same S_y. For every integrand g, the exact tilted integral equals Z_y inverse times the weighted volume integral, so multiplying the raw identity gives the normalized identity.
Corresponding Lean step
integrated_bochner_identity is a genuine public shared theorem call. hI uses integrable_tilted_iff only after hweight; htilt uses integral_tilted and scalar integral algebra.
4. Use the actual conditional curvature constant
Apply the shared curvature-energy consequence to the inherited genuine Hessian lower bound, then multiply by positive Z_y inverse. This yields precisely (alpha+eta inverse)/4 times the S_y gradient energy. It remains a compact-test square-generator estimate. Constructing a weighted closed core/range or resolvent and extending to noncompact scores are still necessary before claiming conditional Poincare or score variance.
Corresponding Lean step
The final calc applies hbound to hcurv and uses inv_nonneg.mpr hZ.le; no variance or spectral-gap theorem is assumed.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · conditional_bochner_energy
Reuse the genuine conditional construction and the full shared Bochner identity; derive the normalizer from actual probability and transfer all integrals exactly.
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 conditional_bochner_energy {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
{V : E → ℝ} {α β : NNReal} {η : ℝ}
(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) :
let μ := (volume : Measure E).tilted (fun x => -V x)
let J := Measure.map (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2)) (μ.prod (stdGaussian E))
let W := fun y u : E => V ((1/2:ℝ) • (y+u)) + ‖u-y‖^2/(8*η)
∃ R S : Kernel E E, IsMarkovKernel R ∧ IsMarkovKernel S ∧
(J.map Prod.swap).IsCondKernel R ∧
(∀ y, S y = (R y).map (fun x => (2:ℝ) • x-y)) ∧
∀ y, S y = (volume : Measure E).tilted (fun u => -W y u) ∧
ContDiff ℝ 2 (W y) ∧ Integrable (fun u => Real.exp (-W y u)) ∧
0 < (∫ u, Real.exp (-W y u)) ∧
∀ f : E → ℝ, ContDiff ℝ ∞ f → HasCompactSupport f →
let L := fun u => Laplacian.laplacian f u - inner ℝ (gradient (W y) u) (gradient f u)
let H := fun u => ∑ i, ‖gradient (fun z => fderiv ℝ f z ((stdOrthonormalBasis ℝ E) i)) u‖^2
let C := fun u => fderiv ℝ (fderiv ℝ (W y)) u (gradient f u) (gradient f u)
Integrable (fun u => (L u)^2) (S y) ∧
Integrable (fun u => ‖gradient f u‖^2) (S y) ∧
Integrable H (S y) ∧ Integrable C (S y) ∧
(∫ u, (L u)^2 ∂S y) = (∫ u, H u ∂S y) + ∫ u, C u ∂S y ∧
(((α:ℝ)+1/η)/4) * (∫ u, ‖gradient f u‖^2 ∂S y) ≤ ∫ u, (L u)^2 ∂S y := by
obtain ⟨R,S,hR,hS,hcond,hSR,hfiber⟩ :=
ConditionalScoreDomain.conditional_curvature_and_score_domain hα hαβ hV hH hη hβη
let _ : IsMarkovKernel S := hS
dsimp only
refine ⟨R,S,hR,hS,hcond,hSR,?_⟩
intro y
let W := fun u : E => V ((1/2:ℝ) • (y+u)) + ‖u-y‖^2/(8*η)
obtain ⟨hSy,hWC,_,_,hcurv,_,_⟩ := hfiber y
change S y = (volume : Measure E).tilted (fun u => -W u) at hSy
have hweight : Integrable (fun u => Real.exp (-W u)) := by
by_contra hn
have hz : S y = 0 := hSy.trans (tilted_of_not_integrable hn)
have hu := measure_univ (μ := S y)
rw [hz] at hu
norm_num at hu
have hZ : 0 < ∫ u, Real.exp (-W u) := integral_exp_pos hweight
refine ⟨hSy,hWC,hweight,hZ,?_⟩
intro f hf hc
obtain ⟨hL,hG,hHess,hC,hidentity,hbound⟩ :=
WeightedBochner.integrated_bochner_identity W f hWC hf hc
have hI (g : E → ℝ) (hg : Integrable (fun u => Real.exp (-W u)*g u)) :
Integrable g (S y) := by
rw [hSy]
exact (integrable_tilted_iff hweight g).mpr (by simpa only [smul_eq_mul] using hg)
have htilt (g : E → ℝ) : (∫ u, g u ∂S y) =
(∫ u, Real.exp (-W u))⁻¹ * (∫ u, Real.exp (-W u)*g u) := by
rw [hSy, integral_tilted]
rw [← integral_const_mul]
apply integral_congr_ae
filter_upwards [] with u
change (Real.exp (-W u) / (∫ z, Real.exp (-W z))) • g u =
(∫ z, Real.exp (-W z))⁻¹ * (Real.exp (-W u) * g u)
simp only [smul_eq_mul, div_eq_mul_inv]
ring
refine ⟨hI _ hL,hI _ hG,hI _ hHess,hI _ hC,?_,?_⟩
· rw [htilt,htilt,htilt,hidentity,mul_add]
· rw [htilt,htilt]
calc
_ = (∫ u, Real.exp (-W u))⁻¹ *
((((α:ℝ)+1/η)/4) * (∫ u, Real.exp (-W u)*‖gradient f u‖^2)) := by ring
_ ≤ _ := mul_le_mul_of_nonneg_left (hbound _ hcurv) (inv_nonneg.mpr hZ.le)
end AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalBochnerSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Paper setting: Euclidean d>=1, V C2, 0<alpha<=beta and actual Hessian bounds alpha I<=D2V<=beta I, eta>0 with beta eta<=1. | E is finite-dimensional real inner-product with Borel structure and canonical volume, including dimension zero. V:E->R is C2. | generalization | Arbitrary finite-dimensional real inner-product spaces and zero dimension are allowed. The positive-dimensional Euclidean source is recovered by specialization; no full manifold result is claimed. |
| Appendix C.1 invokes conditional Poincare. | Actual conditional Bochner identity and square-generator energy lower bound on smooth compact tests. | API-limitation | This is an explicitly labeled analytic prerequisite, not proof of the source Poincare or variance conclusion. |
| Source strong-convexity/smoothness and step-size setting. | Explicit 0<alpha<=beta, C2 V, genuine Hessian bounds and beta eta<=1 retained via ConditionalScoreDomain. | same | The Bochner argument itself needs only the lower curvature; inherited upper restrictions are disclosed as parent-interface restrictions. |
| Actual conditional normalized Gibbs law. | One pair of common Markov R,S with disintegration and reflected pushforward, finite strictly positive normalizer, four integrability conclusions and normalized identity for every y. | source-implicit | Probability of the constructed S rules out the zero tilt before the exact normalized integral transfer. |
Compact-test Bochner identity and curvature-energy bound only. No curvature-to-Poincare theorem, closed weighted operator/core, dense range or resolvent construction, noncompact score extension, variance estimate, macro coercivity, process/mixing/error/cost or complete-paper result.
Encoder–denoiser: accepted · domain-mismatch
Detected semantic differences
- domains: Disclosed abstract finite-dimensional and zero-dimensional extension. — Explicitly disclosed domain extension.
- scopes: Authored analytic prerequisite, not an explicit PBPS C.1 theorem or proof of its Poincare conclusion. — No closed generator, noncompact score extension, variance or macro coercivity; missing core/range/resolvent explicit.
- assumptions: Inherited beta eta<=1 preserved although abstract Bochner does not need it. — Upper scale restriction retained from parent interface and distinguished from abstract Bochner needs.
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
- Compact-test Bochner identity and curvature-energy bound only. No curvature-to-Poincare theorem, closed weighted operator/core, dense range or resolvent construction, noncompact score extension, variance estimate, macro coercivity, process/mixing/error/cost or complete-paper result.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScoreDomain.conditional_curvature_and_score_domainAutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedBochner.integrated_bochner_identity
Mathlib API called (external library)
- MeasureTheory.tilted_of_not_integrable
- MeasureTheory.integral_exp_pos
- MeasureTheory.integrable_tilted_iff
- MeasureTheory.integral_tilted
Mathematical sources
- Chen, Chewi, Lu and Zhang, PBPS v1 Appendix C.1 — Analytic prerequisite for the invoked conditional Poincare inequality. The Bochner edge does not discharge that inequality.
- Kolesnikov and Milman, weighted Reilly identity, Theorem 1.1 (1.3) — Euclidean compact-test localized version proved directly; not the full compact manifold/boundary theorem. Zero dimension is an additional extension.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.