Actual proximal Gaussian oracle with sharp centered concentration
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.FullRangeProximalGaussianOracle.full_range_proximal_gaussian_oracle · theorem · Teaching coverage
Mathematical statement
Produce a measurable exact proximal selector p satisfying p+eta*gradientV(p)=y, the quantitative quadratic minimum and uniqueness, and equal-eta nonexpansivity. The literal G(s,z)=gradientV(p_s+sqrt(eta_s)*z) is jointly measurable and has equal-eta input/noise Lipschitz constants 1 and sqrteta. Produce the genuine Markov law K_s=G(s,-)_#stdGaussian with vector first Bochner moment. For its own mean m_s, every a and signed t have an integrable exponential and integral ≤exp(eta_s*t^2*norm(a)^2/2). This covers (3.2) and (4.3)-(4.5), without identifying K with the RGO posterior or HMC transition.
Lean statement · full_range_proximal_gaussian_oracle
Produce a measurable exact proximal selector p satisfying p+eta*gradientV(p)=y, the quantitative quadratic minimum and uniqueness, and equal-eta nonexpansivity. The literal G(s,z)=gradientV(p_s+sqrt(eta_s)*z) is jointly measurable and has equal-eta input/noise Lipschitz constants 1 and sqrteta. Produce the genuine Markov law K_s=G(s,-)_#stdGaussian with vector first Bochner moment. For its own mean m_s, every a and signed t have an integrable exponential and integral <=exp(eta_s*t^2*norm(a)^2/2). This covers (3.2) and (4.3)-(4.5), without identifying K with the RGO posterior or HMC transition.
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 full_range_proximal_gaussian_oracle
{E S : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
[MeasurableSpace S] {V : E → ℝ} {κ : ℝ}
(hκ : 1 ≤ κ) (hV : ContDiff ℝ 2 V)
(hH : ∀ x v : E, κ⁻¹*‖v‖^2 ≤ fderiv ℝ (fderiv ℝ V) x v v ∧
fderiv ℝ (fderiv ℝ V) x v v ≤ ‖v‖^2)
{eta : S → ℝ} {y : S → E} (heta : Measurable eta) (hy : Measurable y)
(hpos : ∀ s, 0 < eta s) :
let F := fun s x => V x + (eta s)⁻¹/2*‖x-y s‖^2
∃ p : S → E, Measurable p ∧
(∀ s, p s + eta s • gradient V (p s) = y s) ∧
(∀ s z, F s (p s) + (κ⁻¹+(eta s)⁻¹)/2*‖z-p s‖^2 ≤ F s z ∧
(F s z ≤ F s (p s) ↔ z=p s)) ∧
(∀ s t, eta s = eta t → ‖p s-p t‖ ≤ ‖y s-y t‖) ∧
let G := fun q : S × E => gradient V (p q.1+Real.sqrt (eta q.1) • q.2)
Measurable G ∧
(∀ s t z w, eta s = eta t →
‖G (s,z)-G (t,w)‖ ≤ ‖y s-y t‖+Real.sqrt (eta s)*‖z-w‖) ∧
∃ K : ProbabilityTheory.Kernel S E, ProbabilityTheory.IsMarkovKernel K ∧
(∀ s, K s = (ProbabilityTheory.stdGaussian E).map (fun z => G (s,z))) ∧
∀ s, MeasureTheory.Integrable (fun w : E => w) (K s) ∧
∀ (a : E) (t : ℝ), MeasureTheory.Integrable
(fun w => Real.exp (t * inner ℝ a (w - ∫ v, v ∂K s))) (K s) ∧
(∫ w, Real.exp (t * inner ℝ a (w - ∫ v, v ∂K s)) ∂K s) ≤
Real.exp (eta s * t^2 * ‖a‖^2 / 2)Proof roadmap
- 1Derive the real gradient estimates
Reuse the actual C2 Hessian-to-gradient and strong-convexity APIs. The source upper bound supplies gradientV Lipschitz1. The convex gradient-step theorem supplies id-gradientV Lipschitz1, and convexity supplies monotonicity. None is a theorem premise.
- 2Construct the actual pointwise damped map
For each actual positive eta, T_s contracts with its own coefficient eta_s/(1+eta_s)<1. The coefficients may approach one over the parameter space. Banach fixed-point construction is pointwise and makes no uniform-parameter contraction or runtime assumption.
- 3Obtain joint measurability from actual iterates
Every iterate T_s^n(0) is measurable in s from actual measurable eta/y and the continuous id-minus-gradient map. Pointwise Banach convergence with the actual c_s and measurable-limit theorem give a measurable p. Uniform convergence and an upper eta cap are unnecessary; no measurable selector is supplied.
- 4Recover the exact source equation
Multiply the actual fixed-point equation by positive 1+eta and cancel the scalar inverse. The resulting equality is the literal proximal first-order condition for the source quadratic potential.
- 5Prove the genuine minimum and uniqueness
Differentiate the true quadratic regularization. Its gradient vanishes at the constructed p. Existing strong-convexity and first-order bounds give the exact coefficient (kappa^-1+eta^-1)/2. Positivity forces norm(z-p)^2=0 for any competing lower point.
- 6Keep nonexpansivity at fixed eta
Subtract the two literal proximal equations only when eta_s=eta_t. Monotonicity bounds the inner product below by the squared proximal distance. Cauchy-Schwarz and positive-norm cancellation give nonexpansivity; a zero-distance branch is handled separately.
- 7Use the literal Gaussian gradient evaluator
The actual measurable p, eta square root and noise coordinate give a jointly measurable input to the continuous gradient. No posterior identification or oracle witness is used.
- 8Prove the exact input and noise constants
Apply the true gradient Lipschitz bound, split the input difference with the triangle inequality and use proximal nonexpansivity at equal eta. The literal square-root coefficient stays outside the noise norm. This supplies both source inequalities (4.4)-(4.5).
- 9Realize the actual Markov kernel
Take the product of the identity kernel and the constant standard Gaussian kernel, then map it by G. Joint measurability proves it Markov; dirac-product and map-map give the exact pointwise pushforward. This gradient-output law is distinct from the RGO posterior and HMC transitions.
- 10Produce the actual vector first moment
For fixed s the already produced noise Lipschitz bound yields normG(s,z)≤sqrt(eta_s) norm(z)+normG(s,0). Genuine Gaussian norm L1 and measurability imply vector Bochner integrability. Pushforward integrability proves the identity observable is integrable under the same actual output law K_s.
- 11Apply the canonical domain leaf to the actual direction
For every actual vector a, Cauchy-Schwarz and the true noise bound give the scalar observable z→inner(a,G(s,z)) Lipschitz with constant norm(a)sqrt(eta_s). Apply the shared Fernique-domain theorem for every real t, including negative t and zero direction.
- 12Identify the actual center and pull back the law
The Bochner pushforward identity gives m_s=int G(s,z)d gamma. Integral commutation with the continuous inner-product functional gives int f_s,a d gamma=inner(a,m_s). The integrability pushforward equivalence then yields every actual centered directional exponential under K_s. This is the output own mean; no equality with a smoothed gradient is assumed or proved.
- 13Apply sharp concentration at the actual own mean
Push the genuine vector mean back through the same actual Gaussian gradient law, commute inner product with its Bochner integral and apply the canonical sharp concentration theorem to f_s,a(z)=inner(a,G(s,z)). Its internally established Lipschitz constant is norm(a)sqrteta. Positivity of eta gives (norm(a)sqrteta)^2=eta norm(a)^2; the coefficient is exactly one half for every signed t, with no step cap or smoothed-gradient mean substitution.
Full assumptions and notation
All objects and hypotheses
- Source beta=1, alpha=kappa^-1, real kappa≥1; actual C2 V with kappa^-1*normv^2 ≤ D2V(x)[v,v] ≤ normv^2 for every x,v.
- Finite real complete Hilbert/Borel full space E, including dimension zero; arbitrary measurable parameter space S; actual measurable eta:S→R and y:S→E with eta(s)>0 for every s. These coordinate-free/parameter-space extensions are disclosed. Printed Lemma4.2 inherits eta>0 from Section3.1; the eta≤1 premise of neighboring Lemma4.1 is not consumed.
- No supplied proximal point, minimizer, measurable selector, gradient estimate, Lipschitz bound, probability kernel, mean or concentration certificate. Exact witnesses, first moments, signed Laplace domains and sharp coefficient are produced internally. The numerical proximal call cap eta≤1/(2 beta) remains a separate computational contract.
Mathematical proof
1. Derive the real gradient estimates
Reuse the actual C2 Hessian-to-gradient and strong-convexity APIs. The source upper bound supplies gradientV Lipschitz1. The convex gradient-step theorem supplies id-gradientV Lipschitz1, and convexity supplies monotonicity. None is a theorem premise.
Corresponding Lean step
actual_gradient_bounds; QuadraticRegularization; SmoothnessEquivalences; GradientDescentContraction; StrongConvexFirstOrder
2. Construct the actual pointwise damped map
For each actual positive eta, T_s contracts with its own coefficient eta_s/(1+eta_s)<1. The coefficients may approach one over the parameter space. Banach fixed-point construction is pointwise and makes no uniform-parameter contraction or runtime assumption.
Corresponding Lean step
parameterized_damped_point; ContractingWith
3. Obtain joint measurability from actual iterates
Every iterate T_s^n(0) is measurable in s from actual measurable eta/y and the continuous id-minus-gradient map. Pointwise Banach convergence with the actual c_s and measurable-limit theorem give a measurable p. Uniform convergence and an upper eta cap are unnecessary; no measurable selector is supplied.
Corresponding Lean step
ContractingWith.fixedPoint; tendsto_iterate_fixedPoint; measurable_of_tendsto_metrizable
4. Recover the exact source equation
Multiply the actual fixed-point equation by positive 1+eta and cancel the scalar inverse. The resulting equality is the literal proximal first-order condition for the source quadratic potential.
Corresponding Lean step
ContractingWith.fixedPoint_isFixedPt; smul_smul; mul_inv_cancel₀
5. Prove the genuine minimum and uniqueness
Differentiate the true quadratic regularization. Its gradient vanishes at the constructed p. Existing strong-convexity and first-order bounds give the exact coefficient (kappa^-1+eta^-1)/2. Positivity forces norm(z-p)^2=0 for any competing lower point.
Corresponding Lean step
actual_quadratic_minimum; HasFDerivAt.norm_sq; QuadraticRegularization; StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn
6. Keep nonexpansivity at fixed eta
Subtract the two literal proximal equations only when eta_s=eta_t. Monotonicity bounds the inner product below by the squared proximal distance. Cauchy-Schwarz and positive-norm cancellation give nonexpansivity; a zero-distance branch is handled separately.
Corresponding Lean step
gradient_inner_lower_bound_of_strongConvexOn; real_inner_le_norm; norm_nonneg
7. Use the literal Gaussian gradient evaluator
The actual measurable p, eta square root and noise coordinate give a jointly measurable input to the continuous gradient. No posterior identification or oracle witness is used.
Corresponding Lean step
Measurable.comp; Measurable.sqrt; Measurable.smul; LipschitzWith.continuous
8. Prove the exact input and noise constants
Apply the true gradient Lipschitz bound, split the input difference with the triangle inequality and use proximal nonexpansivity at equal eta. The literal square-root coefficient stays outside the noise norm. This supplies both source inequalities (4.4)-(4.5).
Corresponding Lean step
LipschitzWith.dist_le_mul; norm_add_le; norm_smul; Real.sqrt_nonneg
9. Realize the actual Markov kernel
Take the product of the identity kernel and the constant standard Gaussian kernel, then map it by G. Joint measurability proves it Markov; dirac-product and map-map give the exact pointwise pushforward. This gradient-output law is distinct from the RGO posterior and HMC transitions.
Corresponding Lean step
Kernel.id; Kernel.const; Kernel.prod; Kernel.IsMarkovKernel.map; Measure.dirac_prod; Measure.map_map
10. Produce the actual vector first moment
For fixed s the already produced noise Lipschitz bound yields normG(s,z)≤sqrt(eta_s) norm(z)+normG(s,0). Genuine Gaussian norm L1 and measurability imply vector Bochner integrability. Pushforward integrability proves the identity observable is integrable under the same actual output law K_s.
Corresponding Lean step
IsGaussian.integrable_id; Integrable.mono'; integrable_map_measure
11. Apply the canonical domain leaf to the actual direction
For every actual vector a, Cauchy-Schwarz and the true noise bound give the scalar observable z→inner(a,G(s,z)) Lipschitz with constant norm(a)sqrt(eta_s). Apply the shared Fernique-domain theorem for every real t, including negative t and zero direction.
Corresponding Lean step
AutoSamplingTheory.TechnicalLemmas.Probability.GaussianLipschitzExponential.integrable_and_integrable_exp_centered_of_lipschitz; abs_real_inner_le_norm; LipschitzWith.of_dist_le_mul
12. Identify the actual center and pull back the law
The Bochner pushforward identity gives m_s=int G(s,z)d gamma. Integral commutation with the continuous inner-product functional gives int f_s,a d gamma=inner(a,m_s). The integrability pushforward equivalence then yields every actual centered directional exponential under K_s. This is the output own mean; no equality with a smoothed gradient is assumed or proved.
Corresponding Lean step
integral_map; integral_inner; inner_sub_right; integrable_map_measure
13. Apply sharp concentration at the actual own mean
Push the genuine vector mean back through the same actual Gaussian gradient law, commute inner product with its Bochner integral and apply the canonical sharp concentration theorem to f_s,a(z)=inner(a,G(s,z)). Its internally established Lipschitz constant is norm(a)sqrteta. Positivity of eta gives (norm(a)sqrteta)^2=eta norm(a)^2; the coefficient is exactly one half for every signed t, with no step cap or smoothed-gradient mean substitution.
Corresponding Lean step
integral_map; integral_inner; inner_sub_right; AutoSamplingTheory.TechnicalLemmas.Probability.GaussianLipschitzExponential.integral_exp_centered_le_stdGaussian_of_lipschitz; Real.sq_sqrt
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · full_range_proximal_gaussian_oracle
Derive the real gradient estimates; Construct the actual pointwise damped map; Obtain joint measurability from actual iterates; Recover the exact source equation; Prove the genuine minimum and uniqueness; Keep nonexpansivity at fixed eta; Use the literal Gaussian gradient evaluator; Prove the exact input and noise constants; Realize the actual Markov kernel; Produce the actual vector first moment; Apply the canonical domain leaf to the actual direction; Identify the actual center and pull back the law; Apply sharp concentration at the actual own mean
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 full_range_proximal_gaussian_oracle
{E S : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
[MeasurableSpace S] {V : E → ℝ} {κ : ℝ}
(hκ : 1 ≤ κ) (hV : ContDiff ℝ 2 V)
(hH : ∀ x v : E, κ⁻¹*‖v‖^2 ≤ fderiv ℝ (fderiv ℝ V) x v v ∧
fderiv ℝ (fderiv ℝ V) x v v ≤ ‖v‖^2)
{eta : S → ℝ} {y : S → E} (heta : Measurable eta) (hy : Measurable y)
(hpos : ∀ s, 0 < eta s) :
let F := fun s x => V x + (eta s)⁻¹/2*‖x-y s‖^2
∃ p : S → E, Measurable p ∧
(∀ s, p s + eta s • gradient V (p s) = y s) ∧
(∀ s z, F s (p s) + (κ⁻¹+(eta s)⁻¹)/2*‖z-p s‖^2 ≤ F s z ∧
(F s z ≤ F s (p s) ↔ z=p s)) ∧
(∀ s t, eta s = eta t → ‖p s-p t‖ ≤ ‖y s-y t‖) ∧
let G := fun q : S × E => gradient V (p q.1+Real.sqrt (eta q.1) • q.2)
Measurable G ∧
(∀ s t z w, eta s = eta t →
‖G (s,z)-G (t,w)‖ ≤ ‖y s-y t‖+Real.sqrt (eta s)*‖z-w‖) ∧
∃ K : ProbabilityTheory.Kernel S E, ProbabilityTheory.IsMarkovKernel K ∧
(∀ s, K s = (ProbabilityTheory.stdGaussian E).map (fun z => G (s,z))) ∧
∀ s, MeasureTheory.Integrable (fun w : E => w) (K s) ∧
∀ (a : E) (t : ℝ), MeasureTheory.Integrable
(fun w => Real.exp (t * inner ℝ a (w - ∫ v, v ∂K s))) (K s) ∧
(∫ w, Real.exp (t * inner ℝ a (w - ∫ v, v ∂K s)) ∂K s) ≤
Real.exp (eta s * t^2 * ‖a‖^2 / 2) := by
let F := fun s x => V x+(eta s)⁻¹/2*‖x-y s‖^2
obtain ⟨hLip,hMinus,_hsc,hmono⟩ := actual_gradient_bounds hκ hV hH
obtain ⟨p,hp,heq⟩ := parameterized_damped_point hMinus heta hy hpos
have hmin := actual_quadratic_minimum hκ hV hH hpos heq
have hnexp : ∀ s t, eta s=eta t → ‖p s-p t‖ ≤ ‖y s-y t‖ := by
intro s t ht
have hsub : y s-y t=(p s-p t)+eta s • (gradient V (p s)-gradient V (p t)) := by
rw [← heq s,← heq t,← ht]
module
have hpair : ‖p s-p t‖^2 ≤ inner ℝ (y s-y t) (p s-p t) := by
calc
_ ≤ ‖p s-p t‖^2+eta s*inner ℝ (gradient V (p s)-gradient V (p t)) (p s-p t) :=
le_add_of_nonneg_right (mul_nonneg (hpos s).le (hmono (p s) (p t)))
_ = _ := by
rw [hsub,inner_add_left,real_inner_smul_left,real_inner_self_eq_norm_sq]
have hb := hpair.trans (real_inner_le_norm (y s-y t) (p s-p t))
by_cases hz : ‖p s-p t‖=0
· simpa only [hz] using norm_nonneg (y s-y t)
· have hpositive : 0 < ‖p s-p t‖ := lt_of_le_of_ne (norm_nonneg _) (Ne.symm hz)
nlinarith
refine ⟨p,hp,heq,hmin,hnexp,?_⟩
let G := fun q : S × E => gradient V (p q.1+Real.sqrt (eta q.1) • q.2)
have hG : Measurable G := hLip.continuous.measurable.comp
((hp.comp measurable_fst).add ((heta.comp measurable_fst).sqrt.smul measurable_snd))
have hGLip : ∀ s t z w, eta s=eta t →
‖G (s,z)-G (t,w)‖ ≤ ‖y s-y t‖+Real.sqrt (eta s)*‖z-w‖ := by
intro s t z w ht
have h := hLip.dist_le_mul (p s+Real.sqrt (eta s) • z) (p t+Real.sqrt (eta t) • w)
simp only [NNReal.coe_one,one_mul,dist_eq_norm] at h
have hdiff : (p s+Real.sqrt (eta s) • z)-(p t+Real.sqrt (eta t) • w) =
(p s-p t)+Real.sqrt (eta s) • (z-w) := by rw [← ht]; module
calc
_ ≤ ‖(p s+Real.sqrt (eta s) • z)-(p t+Real.sqrt (eta t) • w)‖ := h
_ = ‖(p s-p t)+Real.sqrt (eta s) • (z-w)‖ := by rw [hdiff]
_ ≤ ‖p s-p t‖+‖Real.sqrt (eta s) • (z-w)‖ := norm_add_le _ _
_ ≤ ‖y s-y t‖+Real.sqrt (eta s)*‖z-w‖ := by
rw [norm_smul,Real.norm_eq_abs,abs_of_nonneg (Real.sqrt_nonneg _)]
exact add_le_add (hnexp s t ht) le_rfl
let K := (Kernel.id ×ₖ Kernel.const S (stdGaussian E)).map G
have hK : IsMarkovKernel K := Kernel.IsMarkovKernel.map _ hG
have hKs (s : S) : K s=(stdGaussian E).map (fun z => G (s,z)) := by
dsimp only [K]
rw [Kernel.map_apply _ hG,Kernel.prod_apply,Kernel.id_apply,Kernel.const_apply,
Measure.dirac_prod,Measure.map_map hG (by fun_prop)]
rfl
have hGm (s : S) : Measurable (fun z => G (s,z)) :=
hG.comp (measurable_const.prodMk measurable_id)
have hGi (s : S) : Integrable (fun z => G (s,z)) (stdGaussian E) := by
apply (((IsGaussian.integrable_id (μ := stdGaussian E)).norm.const_mul
(Real.sqrt (eta s))).add (integrable_const ‖G (s,0)‖)).mono'
(hGm s).aestronglyMeasurable
filter_upwards with z
have hd := hGLip s s z 0 rfl
simp only [sub_self,norm_zero,zero_add,sub_zero] at hd
calc
‖G (s,z)‖ = ‖(G (s,z)-G (s,0))+G (s,0)‖ := by rw [sub_add_cancel]
_ ≤ ‖G (s,z)-G (s,0)‖+‖G (s,0)‖ := norm_add_le _ _
_ ≤ Real.sqrt (eta s)*‖z‖+‖G (s,0)‖ := add_le_add hd le_rfl
_ = _ := rfl
refine ⟨hG,hGLip,K,hK,hKs,fun s => ⟨?_,fun a t => ?_⟩⟩
· rw [hKs s]
exact (integrable_map_measure (by fun_prop) (hGm s).aemeasurable).mpr (hGi s)
· have hf : LipschitzWith (Real.toNNReal (‖a‖*Real.sqrt (eta s)))
(fun z => inner ℝ a (G (s,z))) := by
apply LipschitzWith.of_dist_le_mul
intro z w
rw [dist_eq_norm,Real.norm_eq_abs,← inner_sub_right,
Real.coe_toNNReal _ (mul_nonneg (norm_nonneg _) (Real.sqrt_nonneg _)),dist_eq_norm]
have hd := hGLip s s z w rfl
simp only [sub_self,norm_zero,zero_add] at hd
calc
|inner ℝ a (G (s,z)-G (s,w))| ≤ ‖a‖*‖G (s,z)-G (s,w)‖ :=
abs_real_inner_le_norm _ _
_ ≤ ‖a‖*(Real.sqrt (eta s)*‖z-w‖) :=
mul_le_mul_of_nonneg_left hd (norm_nonneg _)
_ = (‖a‖*Real.sqrt (eta s))*‖z-w‖ := by ring
have he :=
(AutoSamplingTheory.TechnicalLemmas.Probability.GaussianLipschitzExponential.integrable_and_integrable_exp_centered_of_lipschitz
(μ := stdGaussian E) hf).2 t
refine ⟨?_,?_⟩
· rw [hKs s,integral_map (hGm s).aemeasurable (by fun_prop)]
apply (integrable_map_measure (by fun_prop) (hGm s).aemeasurable).mpr
convert he using 1
funext z
rw [Function.comp_apply,inner_sub_right,integral_inner (hGi s) a]
· have hm : (∫ v, v ∂K s) = ∫ z, G (s,z) ∂stdGaussian E := by
rw [hKs s]
exact integral_map (hGm s).aemeasurable (by fun_prop)
rw [hm,hKs s,integral_map (hGm s).aemeasurable (by fun_prop)]
calc
_ = ∫ z, Real.exp (t * (inner ℝ a (G (s,z)) -
∫ v, inner ℝ a (G (s,v)) ∂stdGaussian E)) ∂stdGaussian E := by
apply integral_congr_ae
filter_upwards with z
rw [inner_sub_right,integral_inner (hGi s) a]
_ ≤ Real.exp (((Real.toNNReal (‖a‖*Real.sqrt (eta s)) : ℝ≥0) : ℝ)^2*t^2/2) :=
AutoSamplingTheory.TechnicalLemmas.Probability.GaussianLipschitzExponential.integral_exp_centered_le_stdGaussian_of_lipschitz hf t
_ = _ := by
congr 1
rw [Real.coe_toNNReal _ (mul_nonneg (norm_nonneg _) (Real.sqrt_nonneg _)),
mul_pow,Real.sq_sqrt (hpos s).le]
ring
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.FullRangeProximalGaussianOracle
endSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Euclidean d-dimensional source beta1/alpha=kappa^-1 and eta>0; exact argmin and Gaussian gradient definition. | Source beta=1, alpha=kappa^-1, real kappa>=1; actual C2 V with kappa^-1*normv^2 <= D2V(x)[v,v] <= normv^2 for every x,v. Finite real complete Hilbert/Borel full space E, including dimension zero; arbitrary measurable parameter space S; actual measurable eta:S->R and y:S->E with eta(s)>0 for every s. These coordinate-free/parameter-space extensions are disclosed. Printed Lemma4.2 inherits eta>0 from Section3.1; the eta<=1 premise of neighboring Lemma4.1 is not consumed. No supplied proximal point, minimizer, measurable selector, gradient estimate, Lipschitz bound, probability kernel, mean or concentration certificate. Exact witnesses, first moments, signed Laplace domains and sharp coefficient are produced internally. The numerical proximal call cap eta<=1/(2 beta) remains a separate computational contract. | generalization | Finite Hilbert/Borel including0 and arbitrary measurable parameter space disclose a representation extension; no mathematical source estimate or witness becomes an added premise. |
| Actual proximal existence/uniqueness/optimality are implicit and source uses fixed-eta nonexpansivity. | The constructed pointwise damped fixed point supplies measurable selector, true equation and unique quadratic minimum internally. | source-implicit | Authored sufficient construction fills implicit existence/measurability. It does not certify a finite-query numerical proximal algorithm or transfer source computational bounds. |
| Actual estimator (3.2), sharp centered concentration (4.3), input/noise Lipschitz (4.4)-(4.5). | Produce a measurable exact proximal selector p satisfying p+eta*gradientV(p)=y, the quantitative quadratic minimum and uniqueness, and equal-eta nonexpansivity. The literal G(s,z)=gradientV(p_s+sqrt(eta_s)*z) is jointly measurable and has equal-eta input/noise Lipschitz constants 1 and sqrteta. Produce the genuine Markov law K_s=G(s,-)_#stdGaussian with vector first Bochner moment. For its own mean m_s, every a and signed t have an integrable exponential and integral <=exp(eta_s*t^2*norm(a)^2/2). This covers (3.2) and (4.3)-(4.5), without identifying K with the RGO posterior or HMC transition. | same | The combined pair bound at equal eta implies the two source components with exact constants; the law is the literal gradient-output pushforward. |
| Bias, first W2 bound, posterior/HMC semantics, higher algorithms and main/work/composition. | Locally compiled sharp centered Gaussian-output estimate (4.3), retained exact positive-step proximal/evaluator and (4.4)-(4.5), genuine first Bochner moments and all signed exponential domains. Independent mathematics/blind/source/publication/exact-commit/integration admission pending. Bias (4.2), first W2 inequality in (4.6), LSI/T2 adapter, full Lemma4.2, higher smoothing/Picard/Wp/proxy-warmness/initialization, PBPS invariance/nonexplosion/hypocoercivity/implementation/work, both main results and actual-input precision/expected-query-cost composition remain open. Centers are actual Gaussian output means. TV proximity does not transfer unbounded expected cost. | unresolved | No posterior identity, query work or full-Lemma/main completion is asserted; TV proximity cannot transfer unbounded expected cost. |
| Section3.1 eta>0 and Lemma4.2 have no upper eta bound; neighboring Lemma4.1 alone requires eta<=1. | Every eta>0 and all original C2/Hessian/parameter binders retained; signed domain and exact sharp bound are derived outputs. | same | The prior bounded analytic slice is preserved in immutable snapshots, but its cap is removed by a real internal allpositive measurable proximal producer. No producer estimate becomes a public premise. |
| Actual centered Gaussian-gradient noise (4.3), xi=G-EgammaG, any direction u; no finite-mean/Laplace hypotheses printed. | Actual own-mean Bochner/Laplace domains internally produced; coefficient eta*t^2*norm(a)^2/2 independently established by actual standard-Gaussian background. | source-implicit | Internal domain obligations and sharp bound preserve actual output center; equality with a smoothed gradient or bias bound is not claimed. |
Locally compiled sharp centered Gaussian-output estimate (4.3), retained exact positive-step proximal/evaluator and (4.4)-(4.5), genuine first Bochner moments and all signed exponential domains. Independent mathematics/blind/source/publication/exact-commit/integration admission pending. Bias (4.2), first W2 inequality in (4.6), LSI/T2 adapter, full Lemma4.2, higher smoothing/Picard/Wp/proxy-warmness/initialization, PBPS invariance/nonexplosion/hypocoercivity/implementation/work, both main results and actual-input precision/expected-query-cost composition remain open. Centers are actual Gaussian output means. TV proximity does not transfer unbounded expected cost.
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
- Locally compiled sharp centered Gaussian-output estimate (4.3), retained exact positive-step proximal/evaluator and (4.4)-(4.5), genuine first Bochner moments and all signed exponential domains. Independent mathematics/blind/source/publication/exact-commit/integration admission pending. Bias (4.2), first W2 inequality in (4.6), LSI/T2 adapter, full Lemma4.2, higher smoothing/Picard/Wp/proxy-warmness/initialization, PBPS invariance/nonexplosion/hypocoercivity/implementation/work, both main results and actual-input precision/expected-query-cost composition remain open. Centers are actual Gaussian output means. TV proximity does not transfer unbounded expected cost.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadraticAutoSamplingTheory.TechnicalLemmas.Analysis.HessianStrongConvexity.strongConvexOn_univ_of_fderiv2_lowerAutoSamplingTheory.TechnicalLemmas.Analysis.SmoothnessEquivalences.upper_model_iff_fderiv2_upperAutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentContraction.gradient_step_contractionAutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOnAutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOnAutoSamplingTheory.TechnicalLemmas.Probability.GaussianLipschitzExponential.integrable_and_integrable_exp_centered_of_lipschitzAutoSamplingTheory.TechnicalLemmas.Probability.GaussianLipschitzExponential.integral_exp_centered_le_stdGaussian_of_lipschitz
Mathlib API called (external library)
- ContractingWith.fixedPoint
- ContractingWith.tendsto_iterate_fixedPoint
- measurable_of_tendsto_metrizable
- real_inner_le_norm
- HasFDerivAt.norm_sq
- Kernel.id
- Kernel.const
- Kernel.prod
- Kernel.IsMarkovKernel.map
- Measure.dirac_prod
- Measure.map_map
- ProbabilityTheory.IsGaussian.integrable_id
- integrable_map_measure
- integral_map
- integral_inner
- abs_real_inner_le_norm
- Real.sq_sqrt
- Real.coe_toNNReal
Mathematical sources
- SPHMC actual evaluator and (4.3)-(4.5) — Locally compiled sharp centered Gaussian-output estimate (4.3), retained exact positive-step proximal/evaluator and (4.4)-(4.5), genuine first Bochner moments and all signed exponential domains. Independent mathematics/blind/source/publication/exact-commit/integration admission pending. Bias (4.2), first W2 inequality in (4.6), LSI/T2 adapter, full Lemma4.2, higher smoothing/Picard/Wp/proxy-warmness/initialization, PBPS invariance/nonexplosion/hypocoercivity/implementation/work, both main results and actual-input precision/expected-query-cost composition remain open. Centers are actual Gaussian output means. TV proximity does not transfer unbounded expected cost.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.