ProximalPhaseStability actual source component
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProximalPhaseStability.source_phase_proximal_stability · theorem · Teaching coverage
Mathematical statement
Construct measurable exact p, actual stopped q and natural N for full0<eta<1, with p+eta gradientV(p)=id, ||q-p||≤eps and proximalQuery(g,eta,eps,y,N(y)+1,y)=some(q(y),N(y)+1). The exact p is nonexpansive. Construct Markov Kp and Kq as the full two-layer source Gaussian pushforwards. For every deterministic phase state s and finite real rho≥1, the Euclidean Wasserstein cost W_rho(Kq(s),Kp(s))≤3h Lambda eps. Moreover every measurable delta-accurate r has its true pushforward Markov Kr with W_rho(Kr(s),Kp(s))≤3h Lambda delta for all s and rho≥1, includingdelta0. Here W_rho is the 1/rho power of the infimum coupling integral of [sqrt(||DX||²+||DP||²)]^rho. It is not the default max-norm product metric.
Lean statement · source_phase_proximal_stability
Complete exact statement with all constructed source arrays, probability laws, terminal-query identities and Euclidean cost as applicable.
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 source_phase_proximal_stability {V : E → ℝ} {κ : ℝ≥0}
(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 eps : ℝ} (heta : 0 < eta) (heta1 : eta < 1) (heps : 0 < eps)
{J : ℕ} (hJ : 2 ≤ J) {h : ℝ} (hh : 0 < h) :
let t := fun i : Fin J => h/2*(1-Real.cos ((i : ℝ)/(J-1 : ℝ)*Real.pi))
let ell := fun j : Fin J => Lagrange.basis Finset.univ t j
let Lambda := sSup ((fun s : ℝ => ∑ j : Fin J, |(ell j).eval s|) '' Set.Icc 0 h)
let omega := fun i j : Fin J => ∫ s in 0..t i, (t i-s)*(ell j).eval s
let pw := omega ⟨J-1,by omega⟩
let bw := fun j : Fin J => ∫ s in 0..h, (ell j).eval s
h^2*Lambda ≤ 1 →
∃ p q : E → E, ∃ N : E → ℕ,
Measurable p ∧ Measurable q ∧ Measurable N ∧
(∀ y, p y + eta • gradient V (p y) = y ∧ ‖q y-p y‖ ≤ eps ∧
ApproximateProximalExecution.proximalQuery (gradient V) eta eps y (N y+1) y =
some (q y,N y+1)) ∧ LipschitzWith 1 p ∧
let γ := ((stdGaussian E).prod (stdGaussian E)).prod
((Measure.pi (fun _ : Fin J => stdGaussian E)).prod
(Measure.pi (fun _ : Fin J => stdGaussian E)))
let Φ := fun (f : E → E)
(w : (E × E) × ((E × E) × ((Fin J → E) × (Fin J → E)))) =>
let a := Real.exp (-h/2)
let sigma := Real.sqrt (1-Real.exp (-h))
let P0 := a • w.1.2 + sigma • w.2.1.1
let Y0 := fun i => w.1.1+t i • P0
let Z0 := fun j => gradient V (f (Y0 j)+Real.sqrt eta • w.2.2.1 j)
let Y1 := fun i => Y0 i-∑ j, omega i j • Z0 j
let Z1 := fun j => gradient V (f (Y1 j)+Real.sqrt eta • w.2.2.2 j)
(w.1.1+h • P0-∑ j, pw j • Z1 j,
a • (P0-∑ j, bw j • Z1 j)+sigma • w.2.1.2)
let W := fun (rho : ℝ) (μ ν : Measure (E × E)) =>
(TechnicalLemmas.Measure.Transport.transportCost
(fun z : (E × E) × (E × E) =>
(ENNReal.ofReal (Real.sqrt (‖z.1.1-z.2.1‖^2+‖z.1.2-z.2.2‖^2)))^rho)
μ ν)^(rho⁻¹)
∃ Kp Kq : Kernel (E × E) (E × E),
IsMarkovKernel Kp ∧ IsMarkovKernel Kq ∧
(∀ s, Kp s = γ.map (fun z => Φ p (s,z))) ∧
(∀ s, Kq s = γ.map (fun z => Φ q (s,z))) ∧
(∀ s rho, 1 ≤ rho → W rho (Kq s) (Kp s) ≤ ENNReal.ofReal (3*h*Lambda*eps)) ∧
(∀ (r : E → E), Measurable r → ∀ delta : ℝ, 0 ≤ delta →
(∀ y, ‖r y-p y‖ ≤ delta) →
∃ Kr : Kernel (E × E) (E × E), IsMarkovKernel Kr ∧
(∀ s, Kr s = γ.map (fun z => Φ r (s,z))) ∧
∀ s rho, 1 ≤ rho → W rho (Kr s) (Kp s) ≤
ENNReal.ofReal (3*h*Lambda*delta))Proof roadmap
- 1Construct and identify the actual proximal maps
Use the compiled full-range stopped execution kernel with contraction c=eta. It constructs one exact optimality solution p and its actual finite residual-stopped q,N. Derive gradient monotonicity and 1-Lipschitz gradient from the genuine C2 Hessian through the shared quadratic/first-order APIs, then apply the shared monotone-optimality implication. Strong convexity identifies this unique optimality solution with the source proximal minimizer; no p-nonexpansiveness premise or hidden eta≤1/2 restriction.
- 2Use the actual coefficients and preserve the same noise
Use the independent coefficient construction for Lambda≥1 and every omega row sum≤S=h²Lambda/2. Position weights are the final row. The new absolute momentum-integral prerequisite yields sum|b|≤hLambda. Set a=exp(-h/2), sigma=sqrt(1-exp(-h)); P0=aP+sigma*zeta0; both phases use the same P0 and independent G0,G1 arrays, and the same terminal zeta1.
- 3Propagate the two actual Picard layers
At Y0_i=X+t_iP0, common G0 cancels; gradient Lipschitz and ||r-p||≤delta give first gradient difference≤delta. Therefore ||Y1_r-Y1_p||≤S delta. In the second layer add and subtract p(Y1_r), use r accuracy and exact p nonexpansiveness, then cancel common G1 and use gradient Lipschitz. This works for delta=0 and does not assume r Lipschitz.
- 4Bound true Euclidean phase displacement
The full actual position difference is≤S(1+S)delta and momentum difference≤aB(1+S)delta. From Lambda≥1 and h²Lambda≤1 obtain h≤1, S≤1/2 and S≤B/2; also a≤1. The sum of these norms is≤9Bdelta/4≤3Bdelta. The Euclidean square-root norm is at most that sum by nonnegative cross product. Source prose uses momentum-weight positivity to give a sharper intermediate bound; this proof uses the independently derived absolute sum and keeps the same universal D2 scaling with explicit3, without adding an assumption.
- 5Construct actual kernels and a coupling for every finite rho
The product Gaussian law gamma contains both refreshes and both Fin J Gaussian arrays. Each full phase map is measurable by finite sums and composition. Map the product id/kernel-constant to construct each Markov kernel, retaining the existing actual Kq. For fixed s, gamma.map(z↦(Phi_r(s,z),Phi_p(s,z))) has exactly Kr(s) and Kp(s) marginals. The pointwise Euclidean displacement bounds its rho-cost integral by A^rho with A=3hLambda delta; probability normalization supplies the constant integral, so no incoming-state moment assumption is needed. Taking the monotone1/rho root gives the bound, for delta=0 as well.
Full assumptions and notation
All objects and hypotheses
- E is a complete finite-dimensional real inner-product space with its Borel sigma algebra; dimension zero is allowed. V:E→R is genuinely C2, kappa≥1 and kappa^-1||v||²≤D²V(x)[v,v]≤||v||² for every x,v (normalized beta=1).
- 0<eta<1, eps>0 for the actual stopped approximate program. J≥2, h>0; the actual nodes, cardinal polynomials, Lambda, omega and b are defined as in the coefficient prerequisite. Position weights are the last omega row, whose node equals h. The sole step condition is h² Lambda≤1.
- The abstract comparison oracle r is Borel measurable and uniformly satisfies ||r(y)-p(y)||≤delta for every y, with delta≥0 including0. No Lipschitz assumption on r, no state moment or integrability budget, no b positivity, no target-law approximation premise.
Mathematical proof
1. Construct and identify the actual proximal maps
Use the compiled full-range stopped execution kernel with contraction c=eta. It constructs one exact optimality solution p and its actual finite residual-stopped q,N. Derive gradient monotonicity and 1-Lipschitz gradient from the genuine C2 Hessian through the shared quadratic/first-order APIs, then apply the shared monotone-optimality implication. Strong convexity identifies this unique optimality solution with the source proximal minimizer; no p-nonexpansiveness premise or hidden eta≤1/2 restriction.
Corresponding Lean step
ImplementedPhaseKernel.implemented_phase_kernel; QuadraticRegularization; StrongConvexFirstOrder; MonotoneProximalMap
2. Use the actual coefficients and preserve the same noise
Use the independent coefficient construction for Lambda≥1 and every omega row sum≤S=h²Lambda/2. Position weights are the final row. The new absolute momentum-integral prerequisite yields sum|b|≤hLambda. Set a=exp(-h/2), sigma=sqrt(1-exp(-h)); P0=aP+sigma*zeta0; both phases use the same P0 and independent G0,G1 arrays, and the same terminal zeta1.
Corresponding Lean step
ChebyshevLobattoQuadrature.chebyshev_lobatto_coefficients; ChebyshevLobattoMomentum.momentum_absolute_sum_le; phaseMap
3. Propagate the two actual Picard layers
At Y0_i=X+t_iP0, common G0 cancels; gradient Lipschitz and ||r-p||≤delta give first gradient difference≤delta. Therefore ||Y1_r-Y1_p||≤S delta. In the second layer add and subtract p(Y1_r), use r accuracy and exact p nonexpansiveness, then cancel common G1 and use gradient Lipschitz. This works for delta=0 and does not assume r Lipschitz.
Corresponding Lean step
weighted_difference_le; phase_displacement_le hz0,hy1,hz1
4. Bound true Euclidean phase displacement
The full actual position difference is≤S(1+S)delta and momentum difference≤aB(1+S)delta. From Lambda≥1 and h²Lambda≤1 obtain h≤1, S≤1/2 and S≤B/2; also a≤1. The sum of these norms is≤9Bdelta/4≤3Bdelta. The Euclidean square-root norm is at most that sum by nonnegative cross product. Source prose uses momentum-weight positivity to give a sharper intermediate bound; this proof uses the independently derived absolute sum and keeps the same universal D2 scaling with explicit3, without adding an assumption.
Corresponding Lean step
phase_displacement_le hx,hm,hShalf,hSB,htotal; Real.sqrt_le_iff
5. Construct actual kernels and a coupling for every finite rho
The product Gaussian law gamma contains both refreshes and both Fin J Gaussian arrays. Each full phase map is measurable by finite sums and composition. Map the product id/kernel-constant to construct each Markov kernel, retaining the existing actual Kq. For fixed s, gamma.map(z↦(Phi_r(s,z),Phi_p(s,z))) has exactly Kr(s) and Kp(s) marginals. The pointwise Euclidean displacement bounds its rho-cost integral by A^rho with A=3hLambda delta; probability normalization supplies the constant integral, so no incoming-state moment assumption is needed. Taking the monotone1/rho root gives the bound, for delta=0 as well.
Corresponding Lean step
measurable_phase; kernel_from_phase; euclidean_transport_bound; Measure.fst_map_prodMk; Measure.snd_map_prodMk; Transport.transportCost_le_lintegral_of_isCoupling; lintegral_map; ENNReal.rpow_mul
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · source_phase_proximal_stability
Entire current module is covered, including private phase, finite weighted difference, measurability, actual kernel and transport helpers. Extraction carries no new mathematical credit.
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 source_phase_proximal_stability {V : E → ℝ} {κ : ℝ≥0}
(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 eps : ℝ} (heta : 0 < eta) (heta1 : eta < 1) (heps : 0 < eps)
{J : ℕ} (hJ : 2 ≤ J) {h : ℝ} (hh : 0 < h) :
let t := fun i : Fin J => h/2*(1-Real.cos ((i : ℝ)/(J-1 : ℝ)*Real.pi))
let ell := fun j : Fin J => Lagrange.basis Finset.univ t j
let Lambda := sSup ((fun s : ℝ => ∑ j : Fin J, |(ell j).eval s|) '' Set.Icc 0 h)
let omega := fun i j : Fin J => ∫ s in 0..t i, (t i-s)*(ell j).eval s
let pw := omega ⟨J-1,by omega⟩
let bw := fun j : Fin J => ∫ s in 0..h, (ell j).eval s
h^2*Lambda ≤ 1 →
∃ p q : E → E, ∃ N : E → ℕ,
Measurable p ∧ Measurable q ∧ Measurable N ∧
(∀ y, p y + eta • gradient V (p y) = y ∧ ‖q y-p y‖ ≤ eps ∧
ApproximateProximalExecution.proximalQuery (gradient V) eta eps y (N y+1) y =
some (q y,N y+1)) ∧ LipschitzWith 1 p ∧
let γ := ((stdGaussian E).prod (stdGaussian E)).prod
((Measure.pi (fun _ : Fin J => stdGaussian E)).prod
(Measure.pi (fun _ : Fin J => stdGaussian E)))
let Φ := fun (f : E → E)
(w : (E × E) × ((E × E) × ((Fin J → E) × (Fin J → E)))) =>
let a := Real.exp (-h/2)
let sigma := Real.sqrt (1-Real.exp (-h))
let P0 := a • w.1.2 + sigma • w.2.1.1
let Y0 := fun i => w.1.1+t i • P0
let Z0 := fun j => gradient V (f (Y0 j)+Real.sqrt eta • w.2.2.1 j)
let Y1 := fun i => Y0 i-∑ j, omega i j • Z0 j
let Z1 := fun j => gradient V (f (Y1 j)+Real.sqrt eta • w.2.2.2 j)
(w.1.1+h • P0-∑ j, pw j • Z1 j,
a • (P0-∑ j, bw j • Z1 j)+sigma • w.2.1.2)
let W := fun (rho : ℝ) (μ ν : Measure (E × E)) =>
(TechnicalLemmas.Measure.Transport.transportCost
(fun z : (E × E) × (E × E) =>
(ENNReal.ofReal (Real.sqrt (‖z.1.1-z.2.1‖^2+‖z.1.2-z.2.2‖^2)))^rho)
μ ν)^(rho⁻¹)
∃ Kp Kq : Kernel (E × E) (E × E),
IsMarkovKernel Kp ∧ IsMarkovKernel Kq ∧
(∀ s, Kp s = γ.map (fun z => Φ p (s,z))) ∧
(∀ s, Kq s = γ.map (fun z => Φ q (s,z))) ∧
(∀ s rho, 1 ≤ rho → W rho (Kq s) (Kp s) ≤ ENNReal.ofReal (3*h*Lambda*eps)) ∧
(∀ (r : E → E), Measurable r → ∀ delta : ℝ, 0 ≤ delta →
(∀ y, ‖r y-p y‖ ≤ delta) →
∃ Kr : Kernel (E × E) (E × E), IsMarkovKernel Kr ∧
(∀ s, Kr s = γ.map (fun z => Φ r (s,z))) ∧
∀ s rho, 1 ≤ rho → W rho (Kr s) (Kp s) ≤
ENNReal.ofReal (3*h*Lambda*delta)) := by
classical
dsimp only
intro hstep
let t := fun i : Fin J => h/2*(1-Real.cos ((i : ℝ)/(J-1 : ℝ)*Real.pi))
let ell := fun j : Fin J => Lagrange.basis Finset.univ t j
let Lambda := sSup ((fun s : ℝ => ∑ j : Fin J, |(ell j).eval s|) '' Set.Icc 0 h)
let omega := fun i j : Fin J => ∫ s in 0..t i, (t i-s)*(ell j).eval s
let pw := omega ⟨J-1,by omega⟩
let bw := fun j : Fin J => ∫ s in 0..h, (ell j).eval s
obtain ⟨p,q,N,hp,hq,hN,hall,_,hΦq,Kq,hKq,hKqpush⟩ :=
ImplementedPhaseKernel.implemented_phase_kernel hκ hV hH heta
(le_refl eta) heta1 heps h hh.le t omega pw bw
have hg : Measurable (gradient V) := by
unfold gradient
exact ((InnerProductSpace.toDual ℝ E).symm.continuous.comp
(hV.continuous_fderiv (by norm_num))).measurable
have hH' : ∀ x v : E, ((κ⁻¹ : ℝ≥0) : ℝ)*‖v‖^2 ≤
(fderiv ℝ (fderiv ℝ V) x v) v ∧
(fderiv ℝ (fderiv ℝ V) x v) v ≤ (1 : ℝ≥0)*‖v‖^2 := by
simpa only [NNReal.coe_inv,NNReal.coe_one,one_mul] using hH
have hreg :=
TechnicalLemmas.Analysis.QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadratic
(r := 0) hV hH' (0 : E)
have hLip : LipschitzWith 1 (gradient V) := by simpa using hreg.2
have hsc : StrongConvexOn Set.univ ((κ : ℝ)⁻¹) V := by simpa using hreg.1
have hmono (x y : E) : 0 ≤ inner ℝ (gradient V x-gradient V y) (x-y) := by
have hb :=
TechnicalLemmas.Analysis.StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOn hsc
(fun z _ => (hV.differentiable (by norm_num) z).hasGradientAt)
(x := y) (y := x) (Set.mem_univ _) (Set.mem_univ _)
exact (mul_nonneg (inv_nonneg.mpr (NNReal.coe_nonneg κ)) (sq_nonneg _)).trans hb
have hpLip := TechnicalLemmas.Analysis.MonotoneProximalMap.nonexpansive_of_monotone_optimality
heta.le hmono (fun y => (hall y).1)
have hcoeff := TechnicalLemmas.Analysis.ChebyshevLobattoQuadrature.chebyshev_lobatto_coefficients hJ hh
have hL : 1 ≤ Lambda := hcoeff.2.2.2.2.2.1
have hrow : ∀ i, (∑ j, |omega i j|) ≤ h^2/2*Lambda := fun i =>
(hcoeff.2.2.2.2.2.2.1 i).2
have hpw : (∑ j, |pw j|) ≤ h^2/2*Lambda := hrow _
have hbw : (∑ j, |bw j|) ≤ h*Lambda :=
TechnicalLemmas.Analysis.ChebyshevLobattoMomentum.momentum_absolute_sum_le hJ hh
let γ := ((stdGaussian E).prod (stdGaussian E)).prod
((Measure.pi (fun _ : Fin J => stdGaussian E)).prod
(Measure.pi (fun _ : Fin J => stdGaussian E)))
let Φ := fun f => phaseMap (gradient V) f eta h t omega pw bw
have hΦ (f : E → E) (hf : Measurable f) : Measurable (Φ f) :=
measurable_phase hg hf eta h t omega pw bw
obtain ⟨Kp,hKp,hKppush⟩ := kernel_from_phase γ (hΦ p hp)
refine ⟨p,q,N,hp,hq,hN,hall,hpLip,Kp,Kq,hKp,hKq,hKppush,hKqpush,?_,?_⟩
· intro state rho hrho
rw [hKqpush state,hKppush state]
apply euclidean_transport_bound γ ((hΦ q hq).comp (by fun_prop))
((hΦ p hp).comp (by fun_prop)) _ hrho
intro z
exact phase_displacement_le hLip hpLip heps.le hh hL hstep
(fun y => (hall y).2.1) eta t omega pw bw hrow hpw hbw (state,z)
· intro r hr delta hd herr
obtain ⟨Kr,hKr,hKrpush⟩ := kernel_from_phase γ (hΦ r hr)
refine ⟨Kr,hKr,hKrpush,fun state rho hrho => ?_⟩
rw [hKrpush state,hKppush state]
apply euclidean_transport_bound γ ((hΦ r hr).comp (by fun_prop))
((hΦ p hp).comp (by fun_prop)) _ hrho
intro z
exact phase_displacement_le hLip hpLip hd hh hL hstep herr
eta t omega pw bw hrow hpw hbw (state,z)
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProximalPhaseStabilityScope and omitted-condition boundaries
- Appendix D1/D2 one-phase proximal implementation stability only, explicit universal constant3. Both compared phases use the exact same two stochastic-gradient Gaussian arrays and two half-refresh Gaussian vectors; the exact phase uses exact proximal p, not a deterministic smoothed force. N(y)+1 is a noncomputable successful execution certificate, not free runtime fuel determination or expected-work evidence. Repeated-phase D3, weighted contraction, numerical D7/D8, invariant law, bias/concentration, Wp/proxy-warmness/init/PBPS/composition and both main results remain separate. No TV-to-unbounded-cost transfer.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ImplementedPhaseKernel.implemented_phase_kernelAutoSamplingTheory.TechnicalLemmas.Analysis.ChebyshevLobattoQuadrature.chebyshev_lobatto_coefficientsAutoSamplingTheory.TechnicalLemmas.Analysis.MonotoneProximalMap.nonexpansive_of_monotone_optimalityAutoSamplingTheory.TechnicalLemmas.Analysis.ChebyshevLobattoMomentum.momentum_absolute_sum_leAutoSamplingTheory.TechnicalLemmas.Measure.Transport.transportCost_le_lintegral_of_isCouplingAutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadraticAutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOn
Mathlib API called (external library)
- Measure.fst_map_prodMk
- Measure.snd_map_prodMk
- Kernel.IsMarkovKernel.map
- Measure.map_map
- lintegral_map
- ENNReal.rpow_le_rpow
- ENNReal.rpow_mul
- Real.sqrt_le_iff
Mathematical sources
- SPHMC proximal phase and coefficient prerequisites — Appendix D1/D2 one-phase proximal implementation stability only, explicit universal constant3. Both compared phases use the exact same two stochastic-gradient Gaussian arrays and two half-refresh Gaussian vectors; the exact phase uses exact proximal p, not a deterministic smoothed force. N(y)+1 is a noncomputable successful execution certificate, not free runtime fuel determination or expected-work evidence. Repeated-phase D3, weighted contraction, numerical D7/D8, invariant law, bias/concentration, Wp/proxy-warmness/init/PBPS/composition and both main results remain separate. No TV-to-unbounded-cost transfer.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.