AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalBochner

- Actual conditional normalized Bochner identity and curvature-energy bound. The displayed Hessian square term uses genuine directional derivatives in an orthonormal basis, not an assumed operator or a spectral-gap premise.

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⟩ :=
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/ExampleCases/ProximalBPS/ConditionalBochner.lean:25published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.