Actual conditional curvature and the noncompact directional-score domain
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScoreDomain.conditional_curvature_and_score_domain · theorem · Teaching coverage
Statement
For the actual Gibbs-Gaussian augmentation J, there exist common Markov kernels R,S with R disintegrating the swapped joint law and S_y its reflected pushforward. Every S_y is the normalized tilt by -W_y, with W_y(u)=V((y+u)/2)+norm(u-y)^2/(8 eta). The theorem computes the genuine Hessian of W_y and derivative of the dual-valued score s_y(u)=-DV((y+u)/2)/2-inner(y-u,.)/(4 eta), proves the lower curvature (alpha+eta inverse)/4 and sharp score derivative norm bound L=(eta inverse-alpha)/4. Every directional score q_a(u)=s_y(u)(a) is C1 and lies in L2(S_y); its mean, centered square and gradient square are integrable, and its gradient norm is bounded by L norm(a), for every y,a,u.
All objects and hypotheses
- E is a finite-dimensional real inner-product space with its Borel structure and canonical volume. Dimension zero is allowed. V:E->R is C2.
- Alpha and beta are finite nonnegative reals with explicit 0<alpha<=beta. For every x,v the genuine second derivative satisfies alpha norm(v)^2<=D2V(x)[v,v]<=beta norm(v)^2.
- Eta is positive and beta eta<=1. The explicit alpha<=beta condition is retained even in dimension zero, where the Hessian inequalities alone do not imply it.
- Mu is normalized exponential weighting of volume by -V; J is the law of (X,X+sqrt(eta)Z) with X~mu and independent standard Gaussian Z. Kernels, normalization, tails and moment conditions are derived.
- The same R,S work for every y and every direction a. No compact support is imposed on q_a. All regularity, pointwise derivative bounds and fiber integrability conclusions are for the selected everywhere-defined conditional version.
Mathematical proof
1. Fix the actual reflected conditional law
Use the existing conditional-score construction to obtain Markov R and S. R disintegrates the actual swapped Gibbs-Gaussian augmentation; every S_y is the pushforward of R_y through x to 2x-y. The same S_y is volume tilted by minus W_y, where W_y(u)=V((y+u)/2)+norm(u-y)^2/(8 eta). Symmetry of the norm identifies this exponent with the earlier density. No abstract measure with assumed curvature or moments replaces this conditional law.
Corresponding Lean step
Final assembly retains R,S from reflected_conditional_covariance and rewrites hSnu using norm_sub_rev. All following estimates use that S.
2. Compute both genuine derivatives
The midpoint map has derivative one half times identity. Apply the chain rule twice to V composed with the midpoint, and differentiate the quadratic term. Its Hessian is the inner-product map divided by 4 eta. For the score, differentiating minus one half DV gives minus one quarter D2V, while differentiating minus inner(y-u,.)/(4 eta) gives plus the inner-product map divided by 4 eta. V being C2 yields W_y C2 and s_y C1. The Hessian lower bound of V therefore gives the displayed positive lower curvature for W_y.
Corresponding Lean step
conditional_derivatives proves both Frechet derivative identities and regularity by chain rules. The final lower bound substitutes the genuine hH lower inequality.
3. Obtain the sharp score derivative norm
The explicit inequalities alpha<=beta and beta eta<=1 imply beta<=eta inverse and L=(eta inverse-alpha)/4>=0. Use the real Riesz isometry to view D_us_y as an endomorphism of E. Symmetry follows from the symmetry of the genuine second derivative of V. Its quadratic forms lie between zero and L norm(v)^2; the Rayleigh quotient norm formula therefore gives operator norm at most L. The operator is positive semidefinite and may vanish at the endpoint. Transfer the bound back through the Riesz isometry. Keeping alpha<=beta explicitly is necessary when dimension zero is allowed.
Corresponding Lean step
sharp_score_norm uses ContDiffAt.isSymmSndFDerivAt and norm_eq_iSup_rayleighQuotient on the Riesz endomorphism, then opNorm_le_bound on the dual-valued map. No Hessian operator-norm premise is assumed.
4. Derive Gaussian tails and linear score growth
The existing quadratic-regularization theorem at zero regularization gives strong convexity and beta-Lipschitz continuity of the actual gradient. Write G=norm(gradient V(0)). The first-order lower bound and completing the square imply V>=m, with m=V(0)-G^2/(2 alpha), and norm(DV(x))<=G+beta norm(x). For fixed y, put R=norm(y), k=1/(16 eta), C=exp(-m+R^2/(8 eta)), and b=(beta+eta inverse)/4. The triangle inequality gives exp(-W_y(u))<=C exp(-k norm(u)^2) and norm(s_y(u))<=G/2+bR+b norm(u). For direction a, evaluation yields norm(q_a(u))<=A+B norm(u), where A=(G/2+bR)norm(a), B=b norm(a).
Corresponding Lean step
potential_controls, weight_envelope and score_envelope are local proved adapters, reusing public QuadraticRegularization and StrongConvexFirstOrder. They are not treated as publicly available helpers of ConditionalScore.
5. Prove second moments by absorbing the quadratic factor
The linear bound gives q_a(u)^2<=2A^2+2B^2 norm(u)^2. The elementary exponential inequality t<=exp(t), with t=k r^2/2, gives r^2 exp(-k r^2)<=(2/k) exp(-k r^2/2). Consequently the unnormalized squared-score integrand is bounded by C(2A^2+4B^2/k) exp(-k norm(u)^2/2), which is integrable on finite-dimensional E. The original Gaussian envelope also proves integrability of the normalizing weight. The tilted-integral equivalence then proves q_a in L2(S_y). No second-moment assumption is introduced.
Corresponding Lean step
absorb_quadratic and weighted_linear_memLp use the exponential lower bound, finite-dimensional Gaussian integrability, integrable_tilted_iff and memLp_two_iff_integrable_sq.
6. Verify the noncompact input domain
Evaluation at a is a continuous linear map, so q_a is C1 and its gradient has norm at most L norm(a). Its gradient is continuous and uniformly bounded, hence has integrable square under the probability S_y. The already proved L2 membership gives L1 integrability; subtracting the constant expectation preserves L2 and proves the centered square integrable. These are precisely the three clauses of the existing Poincare.Admissible domain. This supplies a valid noncompact directional-score input, but the curvature-to-Poincare theorem and its applicable test-domain extension are separate missing proofs.
Corresponding Lean step
directional_score proves C1 and the norm bound through continuous-linear evaluation. admissible_of_memLp_gradient_bound derives the Admissible clauses from MemLp, MemLp subtraction and bounded continuous gradient; it does not use Poincare.Satisfies or variance_le.
Lean statement · conditional_curvature_and_score_domain
One public theorem constructs actual compatible kernels and proves conditional curvature, the sharp score derivative bound and the full directional-score admissibility domain.
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_curvature_and_score_domain {E : Type u} [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*η)
let s := fun y u : E => -(1/2:ℝ) • fderiv ℝ V ((1/2:ℝ) • (y+u)) - (1/(4*η)) • innerSL ℝ (y-u)
∃ 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) ∧ ContDiff ℝ 1 (s y) ∧
(∀ u v w,
(fderiv ℝ (fderiv ℝ (W y)) u v) w =
(1/4:ℝ)*(fderiv ℝ (fderiv ℝ V) ((1/2:ℝ) • (y+u)) v) w + (1/(4*η))*inner ℝ v w ∧
(fderiv ℝ (s y) u v) w = (1/(4*η))*inner ℝ v w -
(1/4:ℝ)*(fderiv ℝ (fderiv ℝ V) ((1/2:ℝ) • (y+u)) v) w) ∧
(∀ u v, (((α:ℝ)+1/η)/4)*‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ (W y)) u v) v) ∧
(∀ u, ‖fderiv ℝ (s y) u‖ ≤ (1/η-(α:ℝ))/4) ∧
∀ a : E, ContDiff ℝ 1 (fun u => s y u a) ∧
MemLp (fun u => s y u a) 2 (S y) ∧
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.Admissible (S y) (fun u => s y u a) ∧
∀ u, ‖gradient (fun z => s y z a) u‖ ≤ ((1/η-(α:ℝ))/4)*‖a‖Lean proof · conditional_curvature_and_score_domain
Chain rules and symmetric Rayleigh quotients give exact derivatives and sharp norms; Gaussian domination derives L2 moments; continuous evaluation and bounded gradients give the noncompact input domain.
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_curvature_and_score_domain {E : Type u} [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*η)
let s := fun y u : E => -(1/2:ℝ) • fderiv ℝ V ((1/2:ℝ) • (y+u)) - (1/(4*η)) • innerSL ℝ (y-u)
∃ 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) ∧ ContDiff ℝ 1 (s y) ∧
(∀ u v w,
(fderiv ℝ (fderiv ℝ (W y)) u v) w =
(1/4:ℝ)*(fderiv ℝ (fderiv ℝ V) ((1/2:ℝ) • (y+u)) v) w + (1/(4*η))*inner ℝ v w ∧
(fderiv ℝ (s y) u v) w = (1/(4*η))*inner ℝ v w -
(1/4:ℝ)*(fderiv ℝ (fderiv ℝ V) ((1/2:ℝ) • (y+u)) v) w) ∧
(∀ u v, (((α:ℝ)+1/η)/4)*‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ (W y)) u v) v) ∧
(∀ u, ‖fderiv ℝ (s y) u‖ ≤ (1/η-(α:ℝ))/4) ∧
∀ a : E, ContDiff ℝ 1 (fun u => s y u a) ∧
MemLp (fun u => s y u a) 2 (S y) ∧
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.Admissible (S y) (fun u => s y u a) ∧
∀ u, ‖gradient (fun z => s y z a) u‖ ≤ ((1/η-(α:ℝ))/4)*‖a‖ := by
have conditional_derivatives {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
{V : E → ℝ} (hV : ContDiff ℝ 2 V) (η : ℝ) (y : E) :
let W := fun u : E => V ((1/2:ℝ) • (y+u)) + ‖u-y‖^2/(8*η)
let s := fun u : E => -(1/2:ℝ) • fderiv ℝ V ((1/2:ℝ) • (y+u)) -
(1/(4*η)) • innerSL ℝ (y-u)
ContDiff ℝ 2 W ∧ ContDiff ℝ 1 s ∧
∀ u v w : E,
(fderiv ℝ (fderiv ℝ W) u v) w =
(1/4:ℝ) * (fderiv ℝ (fderiv ℝ V) ((1/2:ℝ) • (y+u)) v) w +
(1/(4*η)) * inner ℝ v w ∧
(fderiv ℝ s u v) w =
(1/(4*η)) * inner ℝ v w -
(1/4:ℝ) * (fderiv ℝ (fderiv ℝ V) ((1/2:ℝ) • (y+u)) v) w := by
let mid := fun u : E => (1/2:ℝ) • (y+u)
let W := fun u : E => V (mid u) + ‖u-y‖^2/(8*η)
let s := fun u : E => -(1/2:ℝ) • fderiv ℝ V (mid u) -
(1/(4*η)) • innerSL ℝ (y-u)
let J : E →L[ℝ] (E →L[ℝ] ℝ) :=
{ toFun := fun v => innerSL ℝ v
map_add' := by intros; ext; simp
map_smul' := by intros; ext; simp
cont := (innerSL ℝ (E := E)).continuous }
have hmid (u : E) : HasFDerivAt mid ((1/2:ℝ) • ContinuousLinearMap.id ℝ E) u := by
convert ((hasFDerivAt_const (𝕜 := ℝ) y u).add (hasFDerivAt_id u)).const_smul (1/2:ℝ) using 1 <;> simp [mid] <;> rfl
have hVd := hV.differentiable (by norm_num)
have hVdd := (hV.fderiv_right (m := 1) (by norm_num)).differentiable_one
have hmidC : ContDiff ℝ 2 mid := by fun_prop
have hWC : ContDiff ℝ 2 W := hV.comp hmidC |>.add (((contDiff_id.sub contDiff_const).norm_sq (𝕜 := ℝ)).div_const _)
have hsC : ContDiff ℝ 1 s := by
apply ContDiff.sub
· exact ((hV.fderiv_right (m := 1) (by norm_num)).comp (hmidC.of_le (by norm_num))).const_smul _
· exact (J.contDiff.comp (contDiff_const.sub contDiff_id)).const_smul _
have hWfd (u : E) : fderiv ℝ W u =
(1/2:ℝ) • fderiv ℝ V (mid u) + (1/(4*η)) • J (u-y) := by
have hv := (hVd (mid u)).hasFDerivAt.comp u (hmid u)
have hq := (((hasFDerivAt_id u).sub_const y).norm_sq).const_mul (1/(8*η))
have hw : HasFDerivAt W ((1/2:ℝ) • fderiv ℝ V (mid u) + (1/(4*η)) • J (u-y)) u := by
convert hv.add hq using 1 <;> first | rfl | (ext v; simp [W,J,Function.comp_def]; ring)
exact hw.fderiv
have hWdd (u : E) : HasFDerivAt (fderiv ℝ W)
((1/4:ℝ) • fderiv ℝ (fderiv ℝ V) (mid u) + (1/(4*η)) • J) u := by
rw [show fderiv ℝ W = _ from funext hWfd]
convert (((hVdd (mid u)).hasFDerivAt.comp u (hmid u)).const_smul (1/2:ℝ)).add
((J.hasFDerivAt.comp u ((hasFDerivAt_id u).sub_const y)).const_smul (1/(4*η))) using 1 <;>
first | rfl | (ext v w; simp; ring)
have hsD (u : E) : HasFDerivAt s
((1/(4*η)) • J - (1/4:ℝ) • fderiv ℝ (fderiv ℝ V) (mid u)) u := by
convert (((hVdd (mid u)).hasFDerivAt.comp u (hmid u)).const_smul (-(1/2:ℝ))).sub
((J.hasFDerivAt.comp u ((hasFDerivAt_const (𝕜 := ℝ) y u).sub (hasFDerivAt_id u))).const_smul (1/(4*η))) using 1 <;>
first | rfl | (ext v w; simp; ring)
refine ⟨hWC,hsC,?_⟩
intro u v w
rw [(hWdd u).fderiv,(hsD u).fderiv]
constructor <;> rfl
have sharp_score_norm {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
{V : E → ℝ} (hV : ContDiff ℝ 2 V) {α β η : ℝ}
(hαβ : α ≤ β) (hη : 0 < η) (hβη : β*η ≤ 1)
(hH : ∀ x v : E, α*‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
(fderiv ℝ (fderiv ℝ V) x v) v ≤ β*‖v‖^2)
(x : E) (D : E →L[ℝ] (E →L[ℝ] ℝ))
(hD : ∀ v w, D v w = (1/(4*η))*inner ℝ v w -
(1/4:ℝ)*(fderiv ℝ (fderiv ℝ V) x v) w) :
‖D‖ ≤ (1/η-α)/4 := by
let R : (E →L[ℝ] ℝ) →L[ℝ] E :=
{ toFun := (toDual ℝ E).symm
map_add' := (toDual ℝ E).symm.map_add
map_smul' := by intros; simp
cont := (toDual ℝ E).symm.continuous }
let T := R.comp D
have hinner (v w : E) : inner ℝ (T v) w = D v w := toDual_symm_apply
have hsym : T.IsSymmetric := by
intro v w
change inner ℝ (T v) w = inner ℝ v (T w)
calc
_ = D v w := hinner v w
_ = D w v := by
rw [hD,hD,hV.contDiffAt.isSymmSndFDerivAt (by norm_num) v w,real_inner_comm w v]
_ = inner ℝ (T w) v := (hinner w v).symm
_ = inner ℝ v (T w) := real_inner_comm _ _
have hβ : β ≤ 1/η := (le_div_iff₀ hη).2 hβη
have hc : 0 ≤ (1/η-α)/4 := div_nonneg (sub_nonneg.mpr (hαβ.trans hβ)) (by norm_num)
have hdiag (v : E) : D v v = ((1/η)*‖v‖^2-(fderiv ℝ (fderiv ℝ V) x v) v)/4 := by
rw [hD,real_inner_self_eq_norm_sq]
ring
have hbounds (v : E) : 0 ≤ D v v ∧ D v v ≤ ((1/η-α)/4)*‖v‖^2 := by
rw [hdiag]
have hh := hH x v
have hb := mul_le_mul_of_nonneg_right hβ (sq_nonneg ‖v‖)
constructor <;> nlinarith
have hnormT : ‖T‖ ≤ (1/η-α)/4 := by
rw [T.norm_eq_iSup_rayleighQuotient hsym]
apply ciSup_le
intro v
change |inner ℝ (T v) v / ‖v‖^2| ≤ (1/η-α)/4
rw [hinner,abs_of_nonneg (div_nonneg (hbounds v).1 (sq_nonneg _))]
by_cases hv : v=0
· simpa [hv] using hc
· exact (div_le_iff₀ (sq_pos_of_pos (norm_pos_iff.mpr hv))).2 (hbounds v).2
apply D.opNorm_le_bound hc
intro v
calc
‖D v‖ = ‖T v‖ := ((toDual ℝ E).symm.norm_map (D v)).symm
_ ≤ ‖T‖ * ‖v‖ := T.le_opNorm v
_ ≤ ((1/η-α)/4)*‖v‖ := mul_le_mul_of_nonneg_right hnormT (norm_nonneg _)
have absorb_quadratic {a r : ℝ} (ha : 0 < a) :
r^2 * Real.exp (-a*r^2) ≤ (2/a)*Real.exp (-(a/2)*r^2) := by
have hx : (a/2)*r^2 ≤ Real.exp ((a/2)*r^2) := by
linarith [Real.add_one_le_exp ((a/2)*r^2)]
have hm := mul_le_mul_of_nonneg_right hx (Real.exp_nonneg (-a*r^2))
have he : Real.exp ((a/2)*r^2)*Real.exp (-a*r^2) = Real.exp (-(a/2)*r^2) := by
rw [← Real.exp_add]
congr 1
ring
rw [he] at hm
calc
r^2 * Real.exp (-a*r^2) ≤ Real.exp (-(a/2)*r^2)/(a/2) :=
(le_div_iff₀ (by positivity : 0 < a/2)).2 (by nlinarith [hm])
_ = (2/a)*Real.exp (-(a/2)*r^2) := by ring
have weighted_linear_memLp {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
(w q : E → ℝ) (hw : Continuous w) (hq : Continuous q)
{a C A B : ℝ} (ha : 0 < a) (hC : 0 ≤ C) (hA : 0 ≤ A) (hB : 0 ≤ B)
(hweight : ∀ u, Real.exp (w u) ≤ C*Real.exp (-a*‖u‖^2))
(hgrowth : ∀ u, ‖q u‖ ≤ A+B*‖u‖) :
Integrable (fun u => Real.exp (w u)) (volume : Measure E) ∧
MemLp q 2 ((volume : Measure E).tilted w) := by
have hwi : Integrable (fun u => Real.exp (w u)) (volume : Measure E) := by
apply ((AutoSamplingTheory.TechnicalLemmas.Analysis.Integrability.integrable_exp_neg_mul_norm_sq
(E := E) ha).const_mul C).mono' hw.rexp.aestronglyMeasurable
filter_upwards with u
simpa only [Real.norm_eq_abs,abs_of_pos (Real.exp_pos _)] using hweight u
refine ⟨hwi,?_⟩
apply (memLp_two_iff_integrable_sq hq.aestronglyMeasurable).2
apply (integrable_tilted_iff hwi (fun u => q u ^ 2)).2
have hdom := (AutoSamplingTheory.TechnicalLemmas.Analysis.Integrability.integrable_exp_neg_mul_norm_sq
(E := E) (show 0 < a/2 by positivity)).const_mul (C*(2*A^2+4*B^2/a))
apply hdom.mono' (hw.rexp.smul (hq.pow 2)).aestronglyMeasurable
filter_upwards with u
change ‖Real.exp (w u)*(q u)^2‖ ≤ C*(2*A^2+4*B^2/a)*Real.exp (-(a/2)*‖u‖^2)
simp only [smul_eq_mul,Real.norm_eq_abs,abs_of_nonneg (mul_nonneg (Real.exp_nonneg _) (sq_nonneg _))]
have hs : (q u)^2 ≤ 2*A^2+2*B^2*‖u‖^2 := by
have hh := (sq_le_sq₀ (norm_nonneg (q u)) (by positivity)).2 (hgrowth u)
rw [Real.norm_eq_abs,sq_abs] at hh
nlinarith [sq_nonneg (A-B*‖u‖)]
have he : Real.exp (-a*‖u‖^2) ≤ Real.exp (-(a/2)*‖u‖^2) := by
apply Real.exp_le_exp.mpr
nlinarith [mul_nonneg ha.le (sq_nonneg ‖u‖)]
calc
Real.exp (w u)*(q u)^2 ≤ (C*Real.exp (-a*‖u‖^2))*(2*A^2+2*B^2*‖u‖^2) :=
mul_le_mul (hweight u) hs (sq_nonneg _) (mul_nonneg hC (Real.exp_nonneg _))
_ = C*(2*A^2*Real.exp (-a*‖u‖^2)+2*B^2*(‖u‖^2*Real.exp (-a*‖u‖^2))) := by ring
_ ≤ C*(2*A^2*Real.exp (-(a/2)*‖u‖^2)+2*B^2*((2/a)*Real.exp (-(a/2)*‖u‖^2))) := by
apply mul_le_mul_of_nonneg_left _ hC
exact add_le_add (mul_le_mul_of_nonneg_left he (by positivity))
(mul_le_mul_of_nonneg_left (absorb_quadratic (r := ‖u‖) ha) (by positivity))
_ = C*(2*A^2+4*B^2/a)*Real.exp (-(a/2)*‖u‖^2) := by ring
have admissible_of_memLp_gradient_bound {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
(μ : Measure E) [IsFiniteMeasure μ] (q : E → ℝ)
(hq : ContDiff ℝ 1 q) (hLp : MemLp q 2 μ)
{M : ℝ} (hM : ∀ u, ‖gradient q u‖ ≤ M) :
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.Admissible μ q := by
have hgc : Continuous (gradient q) :=
(toDual ℝ E).symm.continuous.comp (hq.continuous_fderiv (by norm_num))
have hgLp : MemLp (gradient q) 2 μ :=
MemLp.of_bound hgc.aestronglyMeasurable M (Filter.Eventually.of_forall hM)
refine ⟨hLp.integrable (by norm_num),?_,?_⟩
· exact (hLp.sub (memLp_const _)).integrable_sq
· exact (memLp_two_iff_integrable_sq_norm hgc.aestronglyMeasurable).1 hgLp
have directional_score {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
(s : E → (E →L[ℝ] ℝ)) (hs : ContDiff ℝ 1 s) {c : ℝ} (hc : 0 ≤ c)
(hD : ∀ u, ‖fderiv ℝ s u‖ ≤ c) (a : E) :
ContDiff ℝ 1 (fun u => s u a) ∧ ∀ u,
‖gradient (fun z => s z a) u‖ ≤ c*‖a‖ := by
let ev := ContinuousLinearMap.apply' ℝ (RingHom.id ℝ) a
have hq : ContDiff ℝ 1 (fun u => s u a) := ev.contDiff.comp hs
refine ⟨hq,?_⟩
intro u
have hqD : HasFDerivAt (fun z => s z a) (ev.comp (fderiv ℝ s u)) u :=
ev.hasFDerivAt.comp u ((hs.differentiable (by norm_num)) u).hasFDerivAt
have hdn : ‖fderiv ℝ (fun z => s z a) u‖ ≤ c*‖a‖ := by
rw [hqD.fderiv]
apply ContinuousLinearMap.opNorm_le_bound _ (mul_nonneg hc (norm_nonneg _))
intro v
change ‖(fderiv ℝ s u v) a‖ ≤ (c*‖a‖)*‖v‖
calc
‖(fderiv ℝ s u v) a‖ ≤ ‖fderiv ℝ s u v‖*‖a‖ := (fderiv ℝ s u v).le_opNorm a
_ ≤ (‖fderiv ℝ s u‖*‖v‖)*‖a‖ := mul_le_mul_of_nonneg_right ((fderiv ℝ s u).le_opNorm v) (norm_nonneg _)
_ ≤ (c*‖v‖)*‖a‖ := mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_right (hD u) (norm_nonneg _)) (norm_nonneg _)
_ = (c*‖a‖)*‖v‖ := by ring
rw [← toDual_gradient,(toDual ℝ E).norm_map] at hdn
exact hdn
have potential_controls {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] {V : E → ℝ} {α β : ℝ≥0}
(hα : 0 < (α : ℝ)) (hV : ContDiff ℝ 2 V)
(hH : ∀ x v : E,
(α : ℝ)*‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
(fderiv ℝ (fderiv ℝ V) x v) v ≤ (β : ℝ)*‖v‖^2) :
(∀ x, V 0 - (α : ℝ)⁻¹/2*‖gradient V 0‖^2 ≤ V x) ∧
(∀ x, ‖fderiv ℝ V x‖ ≤ ‖gradient V 0‖ + (β : ℝ)*‖x‖) := by
have hd : Differentiable ℝ V := hV.differentiable (by norm_num)
have hreg := QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadratic
hV hH (r := 0) (0 : E)
simp only [NNReal.coe_zero, zero_div, zero_mul, add_zero] at hreg
constructor
· intro x
have hfirst := StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn hreg.1
(fun z _ => (hd z).hasGradientAt) (x := 0) (y := x)
(Set.mem_univ _) (Set.mem_univ _)
simp only [sub_zero] at hfirst
have hinner := (abs_le.mp (abs_real_inner_le_norm (gradient V 0) x)).1
have hyoung := two_mul_le_add_mul_sq (a := ‖x‖) (b := ‖gradient V 0‖) hα
nlinarith
· intro x
rw [← toDual_gradient]
rw [(toDual ℝ E).norm_map]
calc
‖gradient V x‖ ≤ ‖gradient V x - gradient V 0‖ + ‖gradient V 0‖ :=
norm_le_norm_sub_add _ _
_ ≤ (β : ℝ)*‖x‖ + ‖gradient V 0‖ := by
apply add_le_add _ (le_refl _)
simpa using hreg.2.norm_sub_le x 0
_ = _ := add_comm _ _
have weight_envelope {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
(V : E → ℝ) {m η R : ℝ} (hV : ∀ x, m ≤ V x) (hη : 0 < η)
(y u : E) (hy : ‖y‖ ≤ R) :
Real.exp (-V ((1/2:ℝ) • (y+u)) - ‖y-u‖^2/(8*η)) ≤
Real.exp (-m+R^2/(8*η)) * Real.exp (-(1/(16*η))*‖u‖^2) := by
have hR : 0 ≤ R := (norm_nonneg y).trans hy
have htri : ‖u‖ ≤ ‖y-u‖ + R := by
have h := norm_le_norm_sub_add u y
rw [norm_sub_rev u y] at h
linarith
have hsq : ‖u‖^2 ≤ 2*‖y-u‖^2 + 2*R^2 := by
have ht := (sq_le_sq₀ (norm_nonneg u) (by positivity)).mpr htri
nlinarith [sq_nonneg (‖y-u‖-R)]
have hq := div_le_div_of_nonneg_right hsq (by positivity : 0 ≤ 16*η)
have hdiv : ‖u‖^2/(16*η) ≤ ‖y-u‖^2/(8*η) + R^2/(8*η) := by
have heq : (2*‖y-u‖^2+2*R^2)/(16*η) = ‖y-u‖^2/(8*η)+R^2/(8*η) := by
field_simp
ring
rw [heq] at hq
exact hq
rw [← Real.exp_add]
apply Real.exp_le_exp.mpr
have hv := hV ((1/2:ℝ) • (y+u))
simp only [div_eq_mul_inv, one_mul] at hdiv ⊢
nlinarith
have score_envelope {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[CompleteSpace E] (V : E → ℝ) {G β η R : ℝ}
(hG : ∀ x, ‖fderiv ℝ V x‖ ≤ G+β*‖x‖) (hβ : 0 ≤ β) (hη : 0 < η)
(y u : E) (hy : ‖y‖ ≤ R) :
‖-(1/2:ℝ) • fderiv ℝ V ((1/2:ℝ) • (y+u)) -
(1/(4*η)) • innerSL ℝ (y-u)‖ ≤
G/2 + ((β+η⁻¹)/4)*R + ((β+η⁻¹)/4)*‖u‖ := by
have hmid : ‖(1/2:ℝ) • (y+u)‖ ≤ (R+‖u‖)/2 := by
rw [norm_smul, Real.norm_eq_abs]
norm_num
have h := norm_add_le y u
linarith
have hfd : ‖fderiv ℝ V ((1/2:ℝ) • (y+u))‖ ≤ G+β*((R+‖u‖)/2) :=
(hG _).trans (add_le_add (le_refl _) (mul_le_mul_of_nonneg_left hmid hβ))
have hdiff : ‖y-u‖ ≤ R+‖u‖ := (norm_sub_le _ _).trans (add_le_add hy (le_refl _))
calc
_ ≤ ‖-(1/2:ℝ) • fderiv ℝ V ((1/2:ℝ) • (y+u))‖ +
‖(1/(4*η)) • innerSL ℝ (y-u)‖ := norm_sub_le _ _
_ = (1/2:ℝ)*‖fderiv ℝ V ((1/2:ℝ) • (y+u))‖ + (1/(4*η))*‖y-u‖ := by
simp only [norm_smul, Real.norm_eq_abs, innerSL_apply_norm]
rw [abs_of_pos (by positivity : 0 < 1/(4*η))]
norm_num
_ ≤ (1/2:ℝ)*(G+β*((R+‖u‖)/2)) + (1/(4*η))*(R+‖u‖) := by
gcongr
_ = _ := by simp only [div_eq_mul_inv, mul_inv_rev]; ring
let W := fun y u : E => V ((1/2:ℝ) • (y+u)) + ‖u-y‖^2/(8*η)
let s := fun y u : E => -(1/2:ℝ) • fderiv ℝ V ((1/2:ℝ) • (y+u)) - (1/(4*η)) • innerSL ℝ (y-u)
obtain ⟨R,S,hR,hS,hcond,hSR,hSν,hder⟩ :=
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScore.reflected_conditional_covariance hα hV hH hη
let _ : IsMarkovKernel S := hS
obtain ⟨hmin,hgrad⟩ := potential_controls hα hV hH
have hαβr : (α:ℝ) ≤ β := hαβ
have hβInv : (β:ℝ) ≤ 1/η := (le_div_iff₀ hη).2 hβη
have hc : 0 ≤ (1/η-(α:ℝ))/4 := div_nonneg (sub_nonneg.mpr (hαβr.trans hβInv)) (by norm_num)
dsimp only
refine ⟨R,S,hR,hS,hcond,hSR,?_⟩
intro y
have hSy : S y = (volume : Measure E).tilted (fun u => -W y u) := by
rw [hSν y]
congr 1
funext u
dsimp [W]
rw [norm_sub_rev u y]
ring
obtain ⟨hWC,hsC,hcalc⟩ := conditional_derivatives hV η y
have hDn (u : E) : ‖fderiv ℝ (s y) u‖ ≤ (1/η-(α:ℝ))/4 :=
sharp_score_norm hV hαβr hη hβη hH ((1/2:ℝ) • (y+u)) (fderiv ℝ (s y) u)
(fun v w => (hcalc u v w).2)
refine ⟨hSy,hWC,hsC,hcalc,?_,hDn,?_⟩
· intro u v
rw [(hcalc u v v).1,real_inner_self_eq_norm_sq]
have hco : 1/(4*η) = (1/η)/4 := by ring
rw [hco]
nlinarith [(hH ((1/2:ℝ) • (y+u)) v).1]
· intro a
obtain ⟨hqC,hqG⟩ := directional_score (s y) hsC hc hDn a
let b := ((β:ℝ)+η⁻¹)/4
let A := ‖gradient V 0‖/2+b*‖y‖
let m := V 0 - (α:ℝ)⁻¹/2*‖gradient V 0‖^2
have hb : 0 ≤ b := by dsimp [b]; positivity
have hA : 0 ≤ A := by dsimp [A]; positivity
have hqgrowth (u : E) : ‖s y u a‖ ≤ (A*‖a‖)+(b*‖a‖)*‖u‖ := by
have hsg := score_envelope V hgrad (NNReal.coe_nonneg β) hη y u (le_refl ‖y‖)
calc
‖s y u a‖ ≤ ‖s y u‖*‖a‖ := (s y u).le_opNorm a
_ ≤ (A+b*‖u‖)*‖a‖ := mul_le_mul_of_nonneg_right hsg (norm_nonneg _)
_ = _ := by ring
have hweight (u : E) : Real.exp (-W y u) ≤
Real.exp (-m+‖y‖^2/(8*η))*Real.exp (-(1/(16*η))*‖u‖^2) := by
have hw := weight_envelope V hmin hη y u (le_refl ‖y‖)
convert hw using 1
dsimp [W]
rw [norm_sub_rev u y]
congr 1
ring
have hLp : MemLp (fun u => s y u a) 2 (S y) := by
rw [hSy]
exact (weighted_linear_memLp (fun u => -W y u) (fun u => s y u a)
hWC.continuous.neg hqC.continuous (by positivity) (Real.exp_nonneg _)
(mul_nonneg hA (norm_nonneg _)) (mul_nonneg hb (norm_nonneg _)) hweight hqgrowth).2
exact ⟨hqC,hLp,admissible_of_memLp_gradient_bound (S y) (fun u => s y u a) hqC hLp hqG,hqG⟩
end AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScoreDomainScope and omitted-condition boundaries
- Actual conditional curvature, sharp score derivative norm and noncompact directional-score domain only. No curvature-to-Poincare theorem, noncompact test extension of that inequality, conditional variance bound, general L2/H1 differentiation, macroscopic coercivity, process/mixing/implementation/error/query-cost or complete-paper theorem.
Source and reuse
ASTIS parents called
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScore.reflected_conditional_covarianceAutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadraticAutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOnAutoSamplingTheory.TechnicalLemmas.Analysis.Integrability.integrable_exp_neg_mul_norm_sqAutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.Admissible
Mathlib API called (external library)
- ContDiffAt.isSymmSndFDerivAt
- ContinuousLinearMap.norm_eq_iSup_rayleighQuotient
- Real.add_one_le_exp
- MeasureTheory.integrable_tilted_iff
- MeasureTheory.memLp_two_iff_integrable_sq
- MeasureTheory.MemLp.integrable_sq
Mathematical sources
- Chen, Chewi, Lu and Zhang, PBPS v1 Appendix C.1 — Conditional Hessian and score derivative estimates before conditional Poincare, with explicit noncompact test-domain proof.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.