Bochner energy under the actual reflected conditional Gibbs kernel
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalBochner.conditional_bochner_energy · theorem · Teaching coverage
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.
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 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 yLean 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.ConditionalBochnerScope 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.
Source and reuse
ASTIS 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.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.