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

Pointwise gradient–variance bound for the actual reflected conditional mean

Printed Appendix C.1 A3.Ex7 smoothcompact pointwise gradient-variance ingredient. Real unit-direction argument is implemented equivalently by testing the derivative at its own gradient and zero-aware cancellation. Exact1356 StatementSeal and separately reviewed source-only representation overlay admitted before proof. Formula(C.2) outer integration, rough closed-domain extension and PBPS main remain separate.

PBPS arXiv2609.06905v1; Mathlib db584cd6; Lean4.33.0 · PBPS arXiv2609.06905v1 AppendixC.1 A3.Ex7 physical4646-4653; C.1 density/score/derivative A3.Ex1/Ex2/A3.E1; standing0<alpha<=beta C2 and betaeta<=1. · faithful paraphrase

Complete source statement (Samplinglib restatement)

Let E be a finite-dimensional real Hilbert space with its Borel structure, including rank zero. Let V be globally C2 and 0<alpha<=beta, with alpha norm(a)^2<=D²V(x)[a,a]<=beta norm(a)^2 for every x,a. For eta>0 with beta*eta<=1, form the literal normalized volume tilt mu and true Gaussian augmentation J. There exist Markov R and S with R a regular conditional kernel of swapped J, S(y) the reflection x->2x-y of R(y), and every-y explicit normalized reflected density. For every globally smooth compactly supported f, the true conditional mean T f(y)=integral f dS(y) is differentiable at every y and norm(gradient T f(y))²<=(1/eta-alpha)²/[4(alpha+1/eta)]*Var_{S(y)}(f). The probability laws, differentiability and integrability domains are internally produced. No kernel equality, covariance, Poincare or desired-bound certificate is a public premise.

  • Finite real Hilbert/Borel E including rank zero; finite-Hilbert/rank0 extension is explicitly authored.
  • Globally C2 V; 0<alpha<=beta and genuine evaluated Hessian bounds alpha||a||²<=D²V(x)[a,a]<=beta||a||² for every x,a.
  • eta>0 and beta*eta<=1, exact printed source step cap.
  • Observations are globally smooth and compactly supported. Every-y true Markov conditional laws, actual differentiability and centered L2 domains are outputs.

Pointwise gradient–variance bound for the actual reflected conditional mean

\[\|\nabla Tf(y)\|^2\le C_\eta\operatorname{Var}_{S_y}(f),\qquad C_\eta=\frac{(\eta^{-1}-\alpha)^2}{4(\alpha+\eta^{-1})}.\]

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Pointwise gradient–variance bound for the actual reflected conditional mean

AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGradientVariance.reflected_conditional_gradient_variance · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be a finite-dimensional real Hilbert space with its Borel structure, including rank zero. Let V be globally C2 and 0<alpha≤beta, with alpha norm(a)^2≤D²V(x)[a,a]≤beta norm(a)^2 for every x,a. For eta>0 with beta*eta≤1, form the literal normalized volume tilt mu and true Gaussian augmentation J. There exist Markov R and S with R a regular conditional kernel of swapped J, S(y) the reflection x→2x-y of R(y), and every-y explicit normalized reflected density. For every globally smooth compactly supported f, the true conditional mean T f(y)=integral f dS(y) is differentiable at every y and norm(gradient T f(y))²≤(1/eta-alpha)²/[4(alpha+1/eta)]*Var_{S(y)}(f). The probability laws, differentiability and integrability domains are internally produced. No kernel equality, covariance, Poincare or desired-bound certificate is a public premise.

\[\|\nabla Tf(y)\|^2\le C_\eta\operatorname{Var}_{S_y}(f),\qquad C_\eta=\frac{(\eta^{-1}-\alpha)^2}{4(\alpha+\eta^{-1})}.\]
Lean statement · reflected_conditional_gradient_variance

Let E be a finite-dimensional real Hilbert space with its Borel structure, including rank zero. Let V be globally C2 and 0<alpha<=beta, with alpha norm(a)^2<=D²V(x)[a,a]<=beta norm(a)^2 for every x,a. For eta>0 with beta*eta<=1, form the literal normalized volume tilt mu and true Gaussian augmentation J. There exist Markov R and S with R a regular conditional kernel of swapped J, S(y) the reflection x->2x-y of R(y), and every-y explicit normalized reflected density. For every globally smooth compactly supported f, the true conditional mean T f(y)=integral f dS(y) is differentiable at every y and norm(gradient T f(y))²<=(1/eta-alpha)²/[4(alpha+1/eta)]*Var_{S(y)}(f). The probability laws, differentiability and integrability domains are internally produced. No kernel equality, covariance, Poincare or desired-bound certificate is a public premise.

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 reflected_conditional_gradient_variance
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x a : E,
      (α : ℝ) * ‖a‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x a) a ∧
      (fderiv ℝ (fderiv ℝ V) x a) a ≤ (β : ℝ) * ‖a‖^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))
    ∃ 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 => -V ((1/2 : ℝ) • (y+u)) - ‖y-u‖^2/(8*η))) ∧
      ∀ (f : E → ℝ), ContDiff ℝ ∞ f → HasCompactSupport f →
        ∀ y, DifferentiableAt ℝ (fun z => ∫ u, f u ∂S z) y ∧
          ‖gradient (fun z => ∫ u, f u ∂S z) y‖^2 ≤
            (1/η-(α : ℝ))^2/(4*((α : ℝ)+1/η)) *
              AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance
                (S y) f

Exact module and namespace context

Proof roadmap

  1. 1Produce one actual reflected conditional law

    The normalized derivative parent supplies the literal Gaussian augmentation, conditional R, reflected Markov S and every-y normalized density. Its derivative acts on globally smooth compactly supported observations.

  2. 2Identify the score-variance law internally

    The score-variance parent returns its own S prime. Its density agrees at every y because ||u-y||=||y-u|| and -(a+b)=-a-b. Kernel extensionality and subst transport the complete dependent variance/domain package. Equality of R witnesses is neither claimed nor needed.

  3. 3Retain the true covariance derivative

    The score is the actual parameter derivative of the log weight. Normalization centers it. Evaluate this genuine Frechet derivative at the genuine Riesz gradient G of T f, not at a caller-supplied derivative.

  4. 4Produce centered L2 domains and apply Cauchy–Schwarz

    Compact continuity makes f bounded and L2 under the actual probability S_y. Actual score Admissible supplies its integrability and centered-square integrability; the Mathlib L2 equivalence supplies the centered L2 element, with constants restoring score L2. Centered representatives and the real inner-product inequality then give covariance squared ≤ product of actual variances.

  5. 5Use directional variance and cancel with the zero case retained

    Use the actual parent inequality at a=G. If ||G||² is positive, cancel it from ||G||⁴≤Var(f) C_eta ||G||². If it is zero, positivity of the coefficient and variance closes the bound. This keeps rank zero without assuming a unit direction exists.

  6. 6Check the exact Gaussian precision boundary

    For the actual potential V(x)=||x||²/2, alpha=beta=eta=1, the coefficient is zero, so the true differentiable conditional mean has zero gradient. The same actual-kernel test specializes to the zero-dimensional Hilbert space. Outer integration and rough-domain extension are still separate.

Full assumptions and notation

All objects and hypotheses

  • Finite real Hilbert/Borel E including rank zero; finite-Hilbert/rank0 extension is explicitly authored.
  • Globally C2 V; 0<alpha≤beta and genuine evaluated Hessian bounds alpha||a||²≤D²V(x)[a,a]≤beta||a||² for every x,a.
  • eta>0 and beta*eta≤1, exact printed source step cap.
  • Observations are globally smooth and compactly supported. Every-y true Markov conditional laws, actual differentiability and centered L2 domains are outputs.

Mathematical proof

1. Produce one actual reflected conditional law

The normalized derivative parent supplies the literal Gaussian augmentation, conditional R, reflected Markov S and every-y normalized density. Its derivative acts on globally smooth compactly supported observations.

\[\mu(dx)\propto e^{-V(x)}dx,\quad J=\mathcal L(X,X+\sqrt\eta G),\quad S_y(du)\propto e^{-V((y+u)/2)-\|y-u\|^2/(8\eta)}du.\]
Corresponding Lean step

ConditionalScore.reflected_conditional_covariance; hSd; hder

2. Identify the score-variance law internally

The score-variance parent returns its own S prime. Its density agrees at every y because ||u-y||=||y-u|| and -(a+b)=-a-b. Kernel extensionality and subst transport the complete dependent variance/domain package. Equality of R witnesses is neither claimed nor needed.

\[S'_y=S_y\quad\text{for every }y,\qquad \operatorname{Var}_{S_y}(s_y[a])\le C_\eta\|a\|^2.\]
Corresponding Lean step

ConditionalScoreVariance.conditional_centered_domain_and_score_variance; hSS; subst S'; hscore

3. Retain the true covariance derivative

The score is the actual parameter derivative of the log weight. Normalization centers it. Evaluate this genuine Frechet derivative at the genuine Riesz gradient G of T f, not at a caller-supplied derivative.

\[s_y(u)=-\tfrac12 DV((y+u)/2)-\tfrac1{4\eta}\langle y-u,\cdot\rangle,\quad D(Tf)(y)[a]=\operatorname{Cov}_{S_y}(f,s_y[a]),\quad D(Tf)(y)[G]=\|G\|^2.\]
Corresponding Lean step

hfd.differentiableAt; hfd.fderiv; ContinuousLinearMap.integral_apply; inner_gradient_left; hcov

4. Produce centered L2 domains and apply Cauchy–Schwarz

Compact continuity makes f bounded and L2 under the actual probability S_y. Actual score Admissible supplies its integrability and centered-square integrability; the Mathlib L2 equivalence supplies the centered L2 element, with constants restoring score L2. Centered representatives and the real inner-product inequality then give covariance squared ≤ product of actual variances.

\[f-\mathbb E_{S_y}f,\ s_y[G]-\mathbb E_{S_y}s_y[G]\in L^2(S_y),\qquad |\operatorname{Cov}_{S_y}(f,s_y[G])|^2\le\operatorname{Var}_{S_y}(f)\operatorname{Var}_{S_y}(s_y[G]).\]
Corresponding Lean step

MemLp.of_bound; memLp_two_iff_integrable_sq; covariance_eq_sub; MemLp.coeFn_toLp; L2.inner_def; real_inner_mul_inner_self_le

5. Use directional variance and cancel with the zero case retained

Use the actual parent inequality at a=G. If ||G||² is positive, cancel it from ||G||⁴≤Var(f) C_eta ||G||². If it is zero, positivity of the coefficient and variance closes the bound. This keeps rank zero without assuming a unit direction exists.

\[\|G\|^4\le C_\eta\operatorname{Var}_{S_y}(f)\|G\|^2\Longrightarrow\|G\|^2\le C_\eta\operatorname{Var}_{S_y}(f).\]
Corresponding Lean step

hYvar; variance_nonneg; mul_le_mul_of_nonneg_left; hz; mul_le_mul_iff_right₀

6. Check the exact Gaussian precision boundary

For the actual potential V(x)=||x||²/2, alpha=beta=eta=1, the coefficient is zero, so the true differentiable conditional mean has zero gradient. The same actual-kernel test specializes to the zero-dimensional Hilbert space. Outer integration and rough-domain extension are still separate.

\[V(x)=\tfrac12\|x\|^2,\quad\alpha=\beta=\eta=1\Longrightarrow C_\eta=0,\quad\nabla Tf(y)=0.\]
Corresponding Lean step

Tests.ProximalBPSConditionalGradientVariance.gaussian_precision_step; rank_zero_actual_kernel

Lean verification

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

Lean proof · reflected_conditional_gradient_variance

Produce one actual reflected conditional law; Identify the score-variance law internally; Retain the true covariance derivative; Produce centered L2 domains and apply Cauchy–Schwarz; Use directional variance and cancel with the zero case retained; Check the exact Gaussian precision boundary

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 reflected_conditional_gradient_variance
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x a : E,
      (α : ℝ) * ‖a‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x a) a ∧
      (fderiv ℝ (fderiv ℝ V) x a) a ≤ (β : ℝ) * ‖a‖^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))
    ∃ 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 => -V ((1/2 : ℝ) • (y+u)) - ‖y-u‖^2/(8*η))) ∧
      ∀ (f : E → ℝ), ContDiff ℝ ∞ f → HasCompactSupport f →
        ∀ y, DifferentiableAt ℝ (fun z => ∫ u, f u ∂S z) y ∧
          ‖gradient (fun z => ∫ u, f u ∂S z) y‖^2 ≤
            (1/η-(α : ℝ))^2/(4*((α : ℝ)+1/η)) *
              AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance
                (S y) f := by
  dsimp only
  obtain ⟨R, S, hR, hS, hcond, hSR, hSd, hder⟩ :=
    ConditionalScore.reflected_conditional_covariance hα hV hH hη
  obtain ⟨R', S', _, _, _, _, hvar⟩ :=
    ConditionalScoreVariance.conditional_centered_domain_and_score_variance
      hα hαβ hV hH hη hβη
  have hSS : S' = S := by
    ext y : 1
    rw [(hvar y).1, hSd y]
    congr 1
    funext u
    simp only [norm_sub_rev u y, neg_add_rev]
    ring
  subst S'
  let : IsMarkovKernel S := hS
  refine ⟨R, S, hR, hS, hcond, hSR, hSd, ?_⟩
  intro f hf hfc y
  obtain ⟨hsI, hfsI, hfd⟩ := hder f hf hfc y
  refine ⟨hfd.differentiableAt, ?_⟩
  let s := fun u : E => -(1/2:ℝ) • fderiv ℝ V ((1/2:ℝ) • (y+u)) -
    (1/(4*η)) • innerSL ℝ (y-u)
  let G := gradient (fun z => ∫ u, f u ∂S z) y
  let Y := fun u => s u G
  obtain ⟨_, _, _, _, D, _, _, _, _, _, hscore⟩ := hvar y
  obtain ⟨hYad, hYvar⟩ := hscore G
  obtain ⟨M, hM⟩ := hf.continuous.norm.bddAbove_range_of_hasCompactSupport hfc.norm
  have hf2 : MemLp f 2 (S y) := MemLp.of_bound
    hf.continuous.aestronglyMeasurable M (Filter.Eventually.of_forall
      (fun u => hM (Set.mem_range_self u)))
  let Xc := fun u => f u - ∫ v, f v ∂S y
  let Yc := fun u => Y u - ∫ v, Y v ∂S y
  have hXc2 : MemLp Xc 2 (S y) := hf2.sub (memLp_const _)
  have hYc2 : MemLp Yc 2 (S y) :=
    (memLp_two_iff_integrable_sq
      (hYad.1.aestronglyMeasurable.sub aestronglyMeasurable_const)).mpr hYad.2.1
  have hY2 : MemLp Y 2 (S y) := by
    convert hYc2.add (memLp_const (∫ v, Y v ∂S y)) using 1
    funext u
    simp [Yc]
  have hpair (a b : E → ℝ) (ha : MemLp a 2 (S y)) (hb : MemLp b 2 (S y)) :
      ⟪ha.toLp a, hb.toLp b⟫_ℝ = ∫ u, a u * b u ∂S y := by
    rw [L2.inner_def]
    apply integral_congr_ae
    filter_upwards [ha.coeFn_toLp, hb.coeFn_toLp] with u hua hub
    simp [hua, hub, mul_comm]
  have hcs := real_inner_mul_inner_self_le (hXc2.toLp Xc) (hYc2.toLp Yc)
  rw [hpair Xc Yc hXc2 hYc2, hpair Xc Xc hXc2 hXc2,
    hpair Yc Yc hYc2 hYc2] at hcs
  have hcov : ProbabilityTheory.covariance f Y (S y) = ‖G‖^2 := by
    rw [covariance_eq_sub hf2 hY2]
    have hg := congrArg (fun L : E →L[ℝ] ℝ => L G) hfd.fderiv
    have hgG : fderiv ℝ (fun z => ∫ u, f u ∂S z) y G = ‖G‖^2 := by
      rw [← inner_gradient_left, real_inner_self_eq_norm_sq]
    rw [hgG] at hg
    simp only [sub_apply, smul_apply,
      smul_eq_mul, ContinuousLinearMap.integral_apply hfsI G,
      ContinuousLinearMap.integral_apply hsI G] at hg
    exact hg.symm
  have hnorm : (‖G‖^2)^2 ≤
      AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance (S y) f *
      AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance (S y) Y := by
    have he : (∫ u, Xc u * Yc u ∂S y) = ‖G‖^2 := hcov
    rw [he] at hcs
    simpa only [← pow_two, Xc, Yc,
      AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance] using hcs
  have hbound := hnorm.trans (mul_le_mul_of_nonneg_left hYvar
    (AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance_nonneg))
  change ‖G‖^2 ≤ _
  by_cases hz : ‖G‖^2 = 0
  · rw [hz]
    exact mul_nonneg (by positivity)
      AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance_nonneg
  · have hp : 0 < ‖G‖^2 := lt_of_le_of_ne (sq_nonneg _) (Ne.symm hz)
    apply (mul_le_mul_iff_right₀ hp).mp
    simpa only [pow_two, mul_assoc, mul_comm, mul_left_comm] using hbound

end AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGradientVariance

Exact module and namespace context

Source assumptions versus formal assumptions

SourceActual LeanDifference kindWhy it matters
Finite Euclidean standing C2/positivealpha<=beta/Hessian/eta cap assumptions.Finite real Hilbert/Borel including rank zero with exact genuine Hessian and beta*eta<=1 premises.generalizationFiniteHilbert/rank0 authored extension explicitly disclosed; no source premise removed or extra certificate added.
Unit-direction covariance CauchySchwarz followed by norm supremum.Actual derivative evaluated at G, actual centeredL2 covarianceCS and zero-aware positive norm² cancellation.sameSame pointwise inequality and exact quarter coefficient without requiring a unit vector in rank zero.
Outer integrated(C.2), B.13, rough extension and main/cost boundaries.Printed smooth-compact pointwise gradient-variance ingredient, exact quarter coefficient. FiniteHilbert/rank0 explicitly authored extension. Formula(C.2) outer integration/B.13 and rough-domain density/closedgradient extension remain separate, as do full PBPS/SPHMC/kernel runtime/error/cost/composition/main/live/PURIFIED. Actual focused3886PASS; independent wholeproof/blind/source/exactcommit/shared admission pending.unresolvedPointwise smoothcompact edge alone supplies no outer integration, rough-domain closure, sampler convergence or unbounded-cost transfer.

Printed smooth-compact pointwise gradient-variance ingredient, exact quarter coefficient. FiniteHilbert/rank0 explicitly authored extension. Formula(C.2) outer integration/B.13 and rough-domain density/closedgradient extension remain separate, as do full PBPS/SPHMC/kernel runtime/error/cost/composition/main/live/PURIFIED. Actual focused3886PASS; independent wholeproof/blind/source/exactcommit/shared admission pending.

Encoder–denoiser: accepted · equivalent-after-elaboration

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
  • Printed smooth-compact pointwise gradient-variance ingredient, exact quarter coefficient. FiniteHilbert/rank0 explicitly authored extension. Formula(C.2) outer integration/B.13 and rough-domain density/closedgradient extension remain separate, as do full PBPS/SPHMC/kernel runtime/error/cost/composition/main/live/PURIFIED. Actual focused3886PASS; independent wholeproof/blind/source/exactcommit/shared admission pending.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • ProbabilityTheory.covariance_eq_sub
  • MeasureTheory.L2.inner_def
  • real_inner_mul_inner_self_le
  • MeasureTheory.memLp_two_iff_integrable_sq
  • ContinuousLinearMap.integral_apply
  • inner_gradient_left

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.

Which proof obligations and prerequisites are covered?

  • Formalized proof edge; source adapter/review separate Actual smoothcompact pointwise true-gradient bound
  • TODO — not closed by these contributions Outer(C.2)/B.13/roughdomain/bothmain/errors/work/expectedcost remain open