ASTIS mathematical exposition
Actual reflected conditional expectation and its score derivative
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScore.reflected_conditional_covariance · theorem · Teaching coverage
Statement
There exist Markov kernels R and S such that R disintegrates the actual law of (Y,X), S_y is the pushforward of R_y by x↦2x−y, and every S_y has the normalized density proportional to exp(−V((y+u)/2)−‖y−u‖²/(8η)). For every smooth compactly supported real f and every y, both s_y and f s_y are S_y-integrable, and the Fréchet derivative of T_f(y)=∫f dS_y is ∫f s_y dS_y−T_f(y)∫s_y dS_y. Here s_y(u)=−DV((y+u)/2)/2−⟨y−u,·⟩/(4η) is a continuous linear functional, the derivative of the unnormalized log weight.
\[DT_f(y)=\mathbb E_{S_y}[f\,s_y]-\mathbb E_{S_y}[f]\,\mathbb E_{S_y}[s_y].\]
All objects and hypotheses
- E is a finite-dimensional real inner-product space with its Borel measurable structure; dimension zero is allowed. The potential V:E→R is C².
- Constants α and β are finite nonnegative reals, α>0, and the actual second Fréchet derivative satisfies α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v. The scale η is positive. No upper bound βη≤1 is needed for this differentiation step.
- μ is volume tilted by −V and J is the law of (X,X+sqrt(η)Z), where X has law μ and Z is an independent standard Gaussian. Normalization and all integrability used in the proof are derived from the curvature assumptions.
- The public conclusion quantifies over every C∞ compactly supported real test f and every parameter y. The internally proved differentiation argument works for bounded continuous f, including the noncompact test f≡1 needed for the normalizer.
Mathematical proof
1. Push the actual backward conditional kernel through reflection
Positive curvature gives a positive finite Gibbs normalizer. The existing Gaussian conditional-kernel theorem therefore supplies a Markov kernel R disintegrating (Y,X), with R_y equal to μ tilted by −‖x−y‖²/(2η). Tilting twice adds the exponents. The affine change of variables u=2x−y has inverse x=(u+y)/2 and sends volume to 2^(−dim E) times volume. A constant positive factor cancels from a normalized tilt. Substituting the inverse yields W(y,u)=−V((y+u)/2)−‖y−u‖²/(8η). To obtain joint measurability, define S by mapping the product kernel id×R through (y,x)↦2x−y; its fibers are exactly these pushforwards.
\[S_y=(x\mapsto2x-y)_\#R_y=\frac{e^{W(y,u)}\,du}{Z(y)},\qquad Z(y)=\int e^{W(y,u)}\,du.\]
Corresponding Lean step
actual_reflected_density combines normalized_augmentation_density, exists_tilted_isCondKernel, tilted_tilted, an affine measurable equivalence and the Haar scaling formula. reflected_kernel uses Kernel.prod and Kernel.map to construct the measurable Markov kernel.
2. Extract a potential lower bound and linear gradient growth
Apply the existing quadratic-regularization theorem with regularization parameter zero. Its strong-convexity conclusion gives V(x)≥V(0)+⟨∇V(0),x⟩+α‖x‖²/2. Completing the square gives the global lower bound m=V(0)−‖∇V(0)‖²/(2α). The same theorem's β-Lipschitz gradient gives ‖DV(x)‖≤G+β‖x‖, where G=‖∇V(0)‖. These estimates are consequences of the supplied genuine Hessian inequalities, not new premises.
\[V(x)\ge m:=V(0)-\frac{\|\nabla V(0)\|^2}{2\alpha},\qquad\|DV(x)\|\le G+\beta\|x\|.\]
Corresponding Lean step
potential_controls specializes strongConvexOn_and_lipschitzWith_gradient_add_quadratic at r=0, uses its first-order lower bound, and identifies gradient and derivative norms through the Riesz isometry.
3. Derive an integrable local envelope, including the normalizer
Fix y₀ and put R=‖y₀‖+1. On the unit ball around y₀, ‖y‖≤R. The triangle inequality gives ‖u‖²≤2‖y−u‖²+2R². Thus w=e^W is bounded by C exp(−a‖u‖²), where a=1/(16η) and C=exp(−m+R²/(8η)). The derivative score obeys ‖s_y(u)‖≤A+b‖u‖ with b=(β+η⁻¹)/4 and A=G/2+bR. Absorb this linear factor into a weaker Gaussian: (A+br)exp(−ar²)≤(A+b(1+2/a))exp(−ar²/2). Consequently C(A+b(1+2/a))exp(−a‖u‖²/2) dominates ‖D_yw(y,u)‖ uniformly in that ball and is integrable on E. A fixed-y version also proves integrability of w itself.
\[\|D_yw(y,u)\|\le C\bigl(A+b(1+2/a)\bigr)e^{-a\|u\|^2/2}.\]
Corresponding Lean step
weight_envelope, score_envelope and absorb_linear feed local_controls. Gaussian integrability is reused from integrable_exp_neg_mul_norm_sq; no domination hypothesis is accepted by the public theorem.
4. Differentiate the numerator and the noncompact normalizer
The ordinary chain rule gives D_yw=w s_y. For a continuous test f with |f|≤M, multiply the local envelope by M. Continuity of f, V and DV provides the required measurability, so dominated differentiation proves DN_f(y)=∫f(u)w(y,u)s_y(u)du for N_f=∫fw. Apply the same argument separately to f≡1 to obtain DZ(y)=∫w(y,u)s_y(u)du. This second use is essential: compact support of the original test cannot justify differentiating Z. Positivity of the exponential and its already proved integrability give Z(y)>0.
\[DN_f(y)=\int fws_y\,du,\qquad DZ(y)=\int ws_y\,du,\qquad Z(y)>0.\]
Corresponding Lean step
weight_derivative proves the chain-rule formula. unnormalized_derivative applies hasFDerivAt_integral_of_dominated_of_fderiv_le with the derived neighborhood envelope. normalized_covariance invokes it both for f and for the constant one.
5. Normalize and center the derivative
Integration against a tilt is division by Z. The quotient rule gives D(N_f/Z)=Z⁻¹DN_f−(N_f/Z)Z⁻¹DZ. Each weighted volume integral becomes an expectation under S_y. This gives the stated covariance and proves that the score and f times the score are integrable under S_y. The unnormalized score s_y is not itself the derivative of log of the normalized density: that derivative is s_y−E_{S_y}s_y. Under the real Riesz identification, the continuous-linear-functional formula is the source's vector gradient formula.
\[D(N_f/Z)=Z^{-1}DN_f-(N_f/Z)Z^{-1}DZ.\]
Corresponding Lean step
quotient_derivative uses the derivative of inversion and multiplication. integral_tilted and integrable_tilted_iff convert the derivative and its integrability to the actual normalized conditional measure.
6. Recover the smooth compactly supported source inputs
A continuous compactly supported f has bounded norm, so every source test satisfies the bounded-continuous premise used internally. Substitute the everywhere fiber identity for S into both the parameterized expectation and the derivative. This uses the same constructed R and S for all tests and all y. The result supplies the differentiation input to Appendix C.1's conditional gradient–variance estimate; the quantitative variance estimate and its subsequent Sobolev extension are separate obligations.
\[f\in C_c^\infty(E)\Longrightarrow\sup_u|f(u)|<\infty.\]
Corresponding Lean step
The final assembly obtains the norm bound from bddAbove_range_of_hasCompactSupport and rewrites normalized_covariance through hSν.
Lean statement · reflected_conditional_covariance
One public theorem constructs both Markov kernels from the genuine Gibbs/Gaussian law, identifies every reflected fiber and differentiates every smooth compactly supported test expectation at every parameter.
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 reflected_conditional_covariance {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace 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) (hη : 0 < η) :
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 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 => -V ((1/2:ℝ) • (y+u)) - ‖y-u‖^2/(8*η))) ∧
∀ (f : E → ℝ), ContDiff ℝ ∞ f → HasCompactSupport f →
∀ y, Integrable (s y) (S y) ∧ Integrable (fun u => f u • s y u) (S y) ∧
HasFDerivAt (fun z => ∫ u, f u ∂S z)
((∫ u, f u • s y u ∂S y) -
(∫ u, f u ∂S y) • (∫ u, s y u ∂S y)) yLean proof · reflected_conditional_covariance
Local helpers derive normalization, the affine pushforward density, Gaussian domination, both unnormalized derivatives and the normalized covariance. The public theorem assumes none of those conclusions.
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 reflected_conditional_covariance {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace 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) (hη : 0 < η) :
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 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 => -V ((1/2:ℝ) • (y+u)) - ‖y-u‖^2/(8*η))) ∧
∀ (f : E → ℝ), ContDiff ℝ ∞ f → HasCompactSupport f →
∀ y, Integrable (s y) (S y) ∧ Integrable (fun u => f u • s y u) (S y) ∧
HasFDerivAt (fun z => ∫ u, f u ∂S z)
((∫ u, f u • s y u ∂S y) -
(∫ u, f u ∂S y) • (∫ u, s y u ∂S y)) y := by
have map_tilt {E F : Type u} [MeasurableSpace E] [MeasurableSpace F]
(μ : Measure E) (e : E ≃ᵐ F) (f : E → ℝ) (hf : Measurable f) :
(μ.tilted f).map e = (μ.map e).tilted (f ∘ e.symm) := by
unfold Measure.tilted
rw [AutoSamplingTheory.TechnicalLemmas.Measure.RadonNikodym.measurableEquiv_map_withDensity e _ (by fun_prop)]
congr 1
funext y
have hi : (∫ y, Real.exp (f (e.symm y)) ∂(μ.map e)) = ∫ x, Real.exp (f x) ∂μ := by
rw [integral_map_equiv e]
simp only [e.symm_apply_apply]
simp only [Function.comp_apply, hi]
have smul_tilt {E : Type u} [MeasurableSpace E] (μ : Measure E) (f : E → ℝ)
(hf : Measurable f) {c : ℝ} (hc : 0 < c) :
(ENNReal.ofReal c • μ).tilted f = μ.tilted f := by
unfold Measure.tilted
rw [integral_smul_measure, ENNReal.toReal_ofReal hc.le, smul_eq_mul,
withDensity_smul_measure, ← withDensity_smul _ (by fun_prop)]
congr 1
funext x
simp only [Pi.smul_apply, smul_eq_mul]
rw [← ENNReal.ofReal_mul hc.le]
congr 1
by_cases hz : (∫ x, Real.exp (f x) ∂μ) = 0
· simp [hz]
· field_simp
have reflection_affine {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (y : E) :
∃ e : E ≃ᵐ E,
(∀ x, e x = (2:ℝ) • x-y) ∧
(∀ u, e.symm u = (1/2:ℝ) • (u+y)) ∧
Measure.map e (volume : Measure E) =
ENNReal.ofReal (abs ((2:ℝ)^Module.finrank ℝ E)⁻¹) • volume := by
let e : E ≃ᵐ E :=
{ toFun := fun x => (2:ℝ) • x-y
invFun := fun u => (1/2:ℝ) • (u+y)
left_inv := by intro x; simp [smul_smul]
right_inv := by intro u; simp [smul_smul]
measurable_toFun := by
change Measurable (fun x : E => (2:ℝ) • x-y)
fun_prop
measurable_invFun := by
change Measurable (fun u : E => (1/2:ℝ) • (u+y))
fun_prop }
refine ⟨e, fun _ => rfl, fun _ => rfl, ?_⟩
change Measure.map (fun x : E => (2:ℝ) • x-y) volume = _
simp only [sub_eq_add_neg]
change Measure.map ((fun x : E => x + -y) ∘ (fun x : E => (2:ℝ) • x)) volume = _
rw [← Measure.map_map (by fun_prop) (by fun_prop),
Measure.map_addHaar_smul volume (by norm_num : (2:ℝ) ≠ 0),
Measure.map_smul, map_add_right_eq_self]
have reflected_exponent {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
(V : E → ℝ) (η : ℝ) (y u : E) :
-V ((1/2:ℝ) • (u+y)) - ‖(1/2:ℝ) • (u+y)-y‖^2/(2*η) =
-V ((1/2:ℝ) • (y+u)) - ‖y-u‖^2/(8*η) := by
rw [show (1/2:ℝ) • (u+y)-y = (1/2:ℝ) • (u-y) by module]
rw [norm_smul, Real.norm_eq_abs, norm_sub_rev u y, add_comm u y]
norm_num
simp only [div_eq_mul_inv, mul_inv_rev]
ring
have actual_reflected_density {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
{V : E → ℝ} {α η : ℝ} (hα : 0 < α) (hV : ContDiff ℝ 2 V)
(hH : ∀ x v : E, α*‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v)
(hη : 0 < η) :
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 : Kernel E E, IsMarkovKernel R ∧ (J.map Prod.swap).IsCondKernel R ∧
∀ y, Measure.map (fun x => (2:ℝ) • x-y) (R y) =
(volume : Measure E).tilted
(fun u => -V ((1/2:ℝ) • (y+u)) - ‖y-u‖^2/(8*η)) := by
have density := AutoSamplingTheory.ExampleCases.ProximalBPS.GibbsAugmentation.normalized_augmentation_density
hα hV hH hη
have hi : Integrable (fun x => Real.exp (-V x)) (volume : Measure E) := by
by_contra hn
exact (ne_of_gt density.1) (integral_undef hn)
have : IsProbabilityMeasure ((volume : Measure E).tilted (fun x => -V x)) :=
isProbabilityMeasure_tilted hi
have hVm : Measurable V := hV.continuous.measurable
obtain ⟨R,hR,hRf,hcond⟩ :=
AutoSamplingTheory.TechnicalLemmas.Probability.GaussianConditionalKernel.exists_tilted_isCondKernel
((volume : Measure E).tilted (fun x => -V x)) hη
refine ⟨R,hR,hcond,?_⟩
intro y
rw [hRf y, tilted_tilted hi]
obtain ⟨e,he,heinv,hemap⟩ := reflection_affine y
rw [show (fun x => (2:ℝ) • x-y) = e from (funext he).symm]
rw [map_tilt _ e _ (by fun_prop), hemap,
smul_tilt _ _ (by fun_prop) (by positivity)]
congr 1
funext u
simp only [Function.comp_apply, Pi.add_apply, heinv]
simpa only [neg_div, sub_eq_add_neg] using reflected_exponent V η y u
have reflected_kernel {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (R : Kernel E E) [IsMarkovKernel R] :
∃ S : Kernel E E, IsMarkovKernel S ∧
∀ y, S y = (R y).map (fun x => (2:ℝ) • x-y) := by
let F := fun p : E × E => (2:ℝ) • p.2-p.1
have hF : Measurable F := by fun_prop
let S := (Kernel.id ×ₖ R).map F
have : IsMarkovKernel S := Kernel.IsMarkovKernel.map _ hF
refine ⟨S, inferInstance, ?_⟩
intro y
change ((Kernel.id ×ₖ R).map F) y = _
rw [Kernel.map_apply _ hF, Kernel.prod_apply, Kernel.id_apply,
Measure.dirac_prod, Measure.map_map hF (by fun_prop)]
rfl
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
have absorb_linear {a A b r : ℝ} (ha : 0 < a) (hA : 0 ≤ A) (hb : 0 ≤ b) (hr : 0 ≤ r) :
(A+b*r)*Real.exp (-a*r^2) ≤
(A+b*(1+2/a))*Real.exp (-(a/2)*r^2) := by
let t := a/2*r^2
have ht : 0 ≤ t := by dsimp [t]; positivity
have he1 : 1 ≤ Real.exp t := Real.one_le_exp_iff.mpr ht
have he2 : t ≤ Real.exp t := by linarith [Real.add_one_le_exp t]
have hr2 : r^2 ≤ (2/a)*Real.exp t := by
have hh : r^2*a ≤ 2*Real.exp t := by dsimp [t] at he2; nlinarith
calc
r^2 ≤ (2*Real.exp t)/a := (le_div_iff₀ ha).2 hh
_ = _ := by ring
have hrb : r ≤ (1+2/a)*Real.exp t := by
nlinarith [sq_nonneg (r-1)]
have hcoef : A+b*r ≤ (A+b*(1+2/a))*Real.exp t := by
have h1 := mul_le_mul_of_nonneg_left he1 hA
have h2 := mul_le_mul_of_nonneg_left hrb hb
nlinarith
have h := mul_le_mul_of_nonneg_right hcoef (Real.exp_nonneg (-a*r^2))
rw [mul_assoc, ← Real.exp_add] at h
have heq : t + -a*r^2 = -(a/2)*r^2 := by dsimp [t]; ring
rw [heq] at h
exact h
have weight_derivative {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] {V : E → ℝ} (hV : Differentiable ℝ V)
(η : ℝ) (y u : E) :
HasFDerivAt
(fun z => Real.exp (-V ((1/2:ℝ) • (z+u)) - ‖z-u‖^2/(8*η)))
(Real.exp (-V ((1/2:ℝ) • (y+u)) - ‖y-u‖^2/(8*η)) •
(-(1/2:ℝ) • fderiv ℝ V ((1/2:ℝ) • (y+u)) -
(1/(4*η)) • innerSL ℝ (y-u))) y := by
have hv := (hV ((1/2:ℝ) • (y+u))).hasFDerivAt.comp y
(((hasFDerivAt_id y).add_const u).const_smul (1/2:ℝ))
have hq := (((hasFDerivAt_id y).sub_const u).norm_sq).const_mul (8*η)⁻¹
convert (hv.neg.sub hq).exp using 1 <;>
first | (congr 1; ext z; simp [div_eq_mul_inv]; ring) |
(ext v; simp [div_eq_mul_inv, mul_inv_rev]; ring)
have quotient_derivative {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E]
{N Z : E → ℝ} {DN DZ : E →L[ℝ] ℝ} {y : E}
(hN : HasFDerivAt N DN y) (hZ : HasFDerivAt Z DZ y) (hz : Z y ≠ 0) :
HasFDerivAt (fun z => N z/Z z)
((Z y)⁻¹ • DN - (N y/Z y) • ((Z y)⁻¹ • DZ)) y := by
have hi := (hasFDerivAt_inv hz).comp y hZ
have hp := hN.mul hi
convert! hp using 1
ext v
simp [div_eq_mul_inv, pow_two]
ring
have local_controls {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace 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) (hη : 0 < η) :
let w := fun y u : E => Real.exp (-V ((1/2:ℝ) • (y+u)) - ‖y-u‖^2/(8*η))
let dw := fun y u : E => w y u •
(-(1/2:ℝ) • fderiv ℝ V ((1/2:ℝ) • (y+u)) - (1/(4*η)) • innerSL ℝ (y-u))
(∀ y, Integrable (w y) (volume : Measure E)) ∧
∀ y₀, ∃ bound : E → ℝ, Integrable bound (volume : Measure E) ∧
(∀ u, 0 ≤ bound u) ∧
∀ y ∈ Metric.ball y₀ 1, ∀ u, ‖dw y u‖ ≤ bound u := by
let w := fun y u : E => Real.exp (-V ((1/2:ℝ) • (y+u)) - ‖y-u‖^2/(8*η))
let dw := fun y u : E => w y u •
(-(1/2:ℝ) • fderiv ℝ V ((1/2:ℝ) • (y+u)) - (1/(4*η)) • innerSL ℝ (y-u))
let m := V 0 - (α : ℝ)⁻¹/2*‖gradient V 0‖^2
let G := ‖gradient V 0‖
let a := 1/(16*η)
have ha : 0 < a := by dsimp [a]; positivity
obtain ⟨hlower,hgrowth⟩ := potential_controls hα hV hH
have hVc : Continuous V := hV.continuous
have hgauss : Integrable (fun u : E => Real.exp (-a*‖u‖^2)) volume :=
Integrability.integrable_exp_neg_mul_norm_sq ha
constructor
· intro y
refine (hgauss.const_mul (Real.exp (-m+‖y‖^2/(8*η)))).mono' (by dsimp [w]; fun_prop) ?_
filter_upwards with u
rw [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)]
exact weight_envelope V hlower hη y u (le_refl _)
· intro y₀
let R := ‖y₀‖+1
let b := ((β : ℝ)+η⁻¹)/4
let A := G/2+b*R
let C := Real.exp (-m+R^2/(8*η))
let bound := fun u : E => C*(A+b*(1+2/a))*Real.exp (-(a/2)*‖u‖^2)
have hR : 0 ≤ R := by dsimp [R]; positivity
have hb : 0 ≤ b := by dsimp [b]; positivity
have hA : 0 ≤ A := by dsimp [A,G]; positivity
have hC : 0 ≤ C := Real.exp_nonneg _
refine ⟨bound, (Integrability.integrable_exp_neg_mul_norm_sq
(E := E) (a := a/2) (by positivity)).const_mul _, ?_, ?_⟩
· intro u
dsimp [bound]
positivity
· intro y hy u
have hyR : ‖y‖ ≤ R := by
have ht := norm_le_norm_sub_add y y₀
have hd : ‖y-y₀‖ < 1 := by simpa only [Metric.mem_ball, dist_eq_norm] using hy
dsimp [R]
linarith
have hw : w y u ≤ C*Real.exp (-a*‖u‖^2) := weight_envelope V hlower hη y u hyR
have hs : ‖-(1/2:ℝ) • fderiv ℝ V ((1/2:ℝ) • (y+u)) -
(1/(4*η)) • innerSL ℝ (y-u)‖ ≤ A+b*‖u‖ :=
score_envelope V hgrowth β.coe_nonneg hη y u hyR
have hp := absorb_linear ha hA hb (norm_nonneg u)
change ‖dw y u‖ ≤ bound u
dsimp only [dw]
rw [norm_smul, Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)]
calc
_ ≤ w y u*(A+b*‖u‖) := mul_le_mul_of_nonneg_left hs (Real.exp_nonneg _)
_ ≤ (C*Real.exp (-a*‖u‖^2))*(A+b*‖u‖) :=
mul_le_mul_of_nonneg_right hw (by positivity)
_ = C*((A+b*‖u‖)*Real.exp (-a*‖u‖^2)) := by ring
_ ≤ C*((A+b*(1+2/a))*Real.exp (-(a/2)*‖u‖^2)) :=
mul_le_mul_of_nonneg_left hp hC
_ = bound u := by dsimp [bound]; ring
have unnormalized_derivative {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace 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) (hη : 0 < η)
(f : E → ℝ) (hf : Continuous f) {M : ℝ} (hM : 0 ≤ M) (hMf : ∀ u, ‖f u‖ ≤ M) :
let w := fun y u : E => Real.exp (-V ((1/2:ℝ) • (y+u)) - ‖y-u‖^2/(8*η))
let dw := fun y u : E => w y u •
(-(1/2:ℝ) • fderiv ℝ V ((1/2:ℝ) • (y+u)) - (1/(4*η)) • innerSL ℝ (y-u))
∀ y, Integrable (fun u => f u*w y u) (volume : Measure E) ∧
Integrable (fun u => f u • dw y u) (volume : Measure E) ∧
HasFDerivAt (fun z => ∫ u, f u*w z u ∂(volume : Measure E))
(∫ u, f u • dw y u ∂(volume : Measure E)) y := by
let w := fun y u : E => Real.exp (-V ((1/2:ℝ) • (y+u)) - ‖y-u‖^2/(8*η))
let dw := fun y u : E => w y u •
(-(1/2:ℝ) • fderiv ℝ V ((1/2:ℝ) • (y+u)) - (1/(4*η)) • innerSL ℝ (y-u))
have hVc : Continuous V := hV.continuous
have hVdc : Continuous (fderiv ℝ V) := (hV.fderiv_right (m := 1) (by norm_num)).continuous
have hVd : Differentiable ℝ V := hV.differentiable (by norm_num)
obtain ⟨hwI,hcontrols⟩ := local_controls hα hV hH hη
have hfwI (y : E) : Integrable (fun u => f u*w y u) (volume : Measure E) := by
refine ((hwI y).const_mul M).mono' (by dsimp [w]; fun_prop) ?_
filter_upwards with u
rw [norm_mul, Real.norm_eq_abs (w y u), abs_of_pos (Real.exp_pos _)]
exact mul_le_mul_of_nonneg_right (hMf u) (Real.exp_nonneg _)
dsimp only
intro y
obtain ⟨B,hBI,hB0,hB⟩ := hcontrols y
have hbound : ∀ u, ∀ z ∈ Metric.ball y 1, ‖f u • dw z u‖ ≤ M*B u := by
intro u z hz
rw [norm_smul]
exact mul_le_mul (hMf u) (hB z hz u) (norm_nonneg _) hM
have hfdI : Integrable (fun u => f u • dw y u) (volume : Measure E) := by
refine (hBI.const_mul M).mono' (by dsimp [dw,w]; fun_prop) ?_
exact ae_of_all _ (fun u => hbound u y (Metric.mem_ball_self zero_lt_one))
refine ⟨hfwI y,hfdI,?_⟩
apply hasFDerivAt_integral_of_dominated_of_fderiv_le
(F' := fun z u => f u • dw z u) (bound := fun u => M*B u)
(Metric.ball_mem_nhds y zero_lt_one)
· exact Filter.Eventually.of_forall (fun z => by fun_prop)
· exact hfwI y
· exact hfdI.aestronglyMeasurable
· exact ae_of_all _ hbound
· exact hBI.const_mul M
· filter_upwards with u
intro z _
exact (weight_derivative hVd η z u).const_mul (f u)
have normalized_tilt_integral {E F : Type u} [MeasurableSpace E]
[NormedAddCommGroup F] [NormedSpace ℝ F] (μ : Measure E) (W : E → ℝ) (g : E → F) :
∫ u, g u ∂(μ.tilted W) = (∫ u, Real.exp (W u) ∂μ)⁻¹ •
∫ u, Real.exp (W u) • g u ∂μ := by
rw [integral_tilted]
simp only [div_eq_inv_mul, mul_smul]
rw [integral_smul]
have normalized_covariance {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace 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) (hη : 0 < η)
(f : E → ℝ) (hf : Continuous f) {M : ℝ} (hM : 0 ≤ M) (hMf : ∀ u, ‖f u‖ ≤ M) :
let ν := fun y : E => (volume : Measure E).tilted
(fun u => -V ((1/2:ℝ) • (y+u)) - ‖y-u‖^2/(8*η))
let s := fun y u : E => -(1/2:ℝ) • fderiv ℝ V ((1/2:ℝ) • (y+u)) -
(1/(4*η)) • innerSL ℝ (y-u)
∀ y, Integrable (s y) (ν y) ∧ Integrable (fun u => f u • s y u) (ν y) ∧
HasFDerivAt (fun z => ∫ u, f u ∂ν z)
((∫ u, f u • s y u ∂ν y) - (∫ u, f u ∂ν y) • (∫ u, s y u ∂ν y)) y := by
let ν := fun y : E => (volume : Measure E).tilted
(fun u => -V ((1/2:ℝ) • (y+u)) - ‖y-u‖^2/(8*η))
let s := fun y u : E => -(1/2:ℝ) • fderiv ℝ V ((1/2:ℝ) • (y+u)) -
(1/(4*η)) • innerSL ℝ (y-u)
let w := fun y u : E => Real.exp (-V ((1/2:ℝ) • (y+u)) - ‖y-u‖^2/(8*η))
let dw := fun y u : E => w y u • s y u
let Z := fun y => ∫ u, w y u ∂(volume : Measure E)
let N := fun y => ∫ u, f u*w y u ∂(volume : Measure E)
let DZ := fun y => ∫ u, dw y u ∂(volume : Measure E)
let DN := fun y => ∫ u, f u • dw y u ∂(volume : Measure E)
have hN := unnormalized_derivative hα hV hH hη f hf hM hMf
have hZraw := unnormalized_derivative hα hV hH hη (fun _ : E => (1:ℝ))
continuous_const (M := 1) (by norm_num) (fun _ => by norm_num)
have hZ : ∀ y, Integrable (w y) (volume : Measure E) ∧
Integrable (dw y) (volume : Measure E) ∧ HasFDerivAt Z (DZ y) y := by
intro y
simpa only [one_mul, one_smul] using hZraw y
have hTf (y : E) : (∫ u, f u ∂ν y) = N y/Z y := by
have hscalar (μ : Measure E) (W g : E → ℝ) :
∫ u, g u ∂(μ.tilted W) = (∫ u, Real.exp (W u) ∂μ)⁻¹ •
∫ u, Real.exp (W u) • g u ∂μ := by
rw [integral_tilted]
simp only [div_eq_inv_mul, mul_smul]
rw [integral_smul]
rw [hscalar]
change (Z y)⁻¹ * (∫ u, w y u * f u ∂(volume : Measure E)) = N y / Z y
rw [div_eq_mul_inv, mul_comm (N y)]
congr 1
apply integral_congr_ae
filter_upwards with u
exact mul_comm _ _
have hTs (y : E) : (∫ u, s y u ∂ν y) = (Z y)⁻¹ • DZ y := by
exact normalized_tilt_integral _ _ _
have hTfs (y : E) : (∫ u, f u • s y u ∂ν y) = (Z y)⁻¹ • DN y := by
rw [normalized_tilt_integral]
congr 1
apply integral_congr_ae
filter_upwards with u
simp only [dw, smul_smul]
rw [mul_comm]
dsimp only
intro y
have hsI : Integrable (s y) (ν y) := by
rw [integrable_tilted_iff (hZ y).1]
exact (hZ y).2.1
have hfsI : Integrable (fun u => f u • s y u) (ν y) := by
rw [integrable_tilted_iff (hZ y).1]
apply (hN y).2.1.congr
filter_upwards with u
simp only [smul_smul]
rw [mul_comm]
refine ⟨hsI,hfsI,?_⟩
change HasFDerivAt (fun z => ∫ u, f u ∂ν z)
((∫ u, f u • s y u ∂ν y) - (∫ u, f u ∂ν y) • (∫ u, s y u ∂ν y)) y
rw [show (fun z => ∫ u, f u ∂ν z) = (fun z => N z/Z z) from funext hTf,
hTf y,hTs y,hTfs y]
exact quotient_derivative (hN y).2.2 (hZ y).2.2 (ne_of_gt (integral_exp_pos (hZ y).1))
dsimp only
obtain ⟨R,hR,hcond,hν⟩ := actual_reflected_density hα hV (fun x v => (hH x v).1) hη
let : IsMarkovKernel R := hR
obtain ⟨S,hS,hSR⟩ := reflected_kernel R
have hSν (y : E) : S y = (volume : Measure E).tilted
(fun u => -V ((1/2:ℝ) • (y+u)) - ‖y-u‖^2/(8*η)) :=
(hSR y).trans (hν y)
refine ⟨R,S,hR,hS,hcond,hSR,hSν,?_⟩
intro f hf hfc y
obtain ⟨M,hM⟩ := hf.continuous.norm.bddAbove_range_of_hasCompactSupport hfc.norm
have hMf (u : E) : ‖f u‖ ≤ M := hM (Set.mem_range_self u)
have hM0 : 0 ≤ M := (norm_nonneg (f 0)).trans (hMf 0)
simpa only [hSν] using normalized_covariance hα hV hH hη f hf.continuous hM0 hMf y
end AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScoreScope and omitted-condition boundaries
- Actual reflected conditional-kernel density and smooth-test derivative only. The transformed joint law's IsCondKernel interface and its identification with the existing L² PUP representative are not yet exposed. Conditional Poincare, score variance, the L²/H¹ extension, macroscopic coercivity, half-turn/process semantics, invariance/nonexplosion, mixing/error/cost and full-paper completion remain open.
Source and reuse
ASTIS parents called
AutoSamplingTheory.ExampleCases.ProximalBPS.GibbsAugmentation.normalized_augmentation_densityAutoSamplingTheory.TechnicalLemmas.Probability.GaussianConditionalKernel.exists_tilted_isCondKernelAutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadraticAutoSamplingTheory.TechnicalLemmas.Measure.RadonNikodym.measurableEquiv_map_withDensityAutoSamplingTheory.TechnicalLemmas.Analysis.Integrability.integrable_exp_neg_mul_norm_sq
Mathlib API called (external library)
- Measure.map_addHaar_smul
- tilted_tilted
- integral_tilted
- integrable_tilted_iff
- hasFDerivAt_integral_of_dominated_of_fderiv_le
- Continuous.bddAbove_range_of_hasCompactSupport
Mathematical sources
- Chen, Chewi, Lu and Zhang, PBPS v1 Appendix C.1 — Conditional density and differentiated conditional expectation only; expanded normalization and domination 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.