Samplinglib mathematical lesson

Actual PBPS ambient adjoint and globally centered corrector

AutoSamplingTheory.ExampleCases.ProximalBPS.AmbientAdjointCorrector.actual_ambient_adjoint_centered_decomposition · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be a finite-dimensional real Hilbert Borel space with canonical volume, including the explicit rank-zero extension. Let V:E→ℝ be C², 0<α≤β, and assume α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v. Assume η>0 and βη≤1. Define μ(dx) proportional to exp(−V(x))dx, J as the law of (X,X+√η Z) for independent X~μ and Z~N(0,I), ν=J.snd, and Λ as the law of (Y,2X−Y) under J. These are probability laws. Put mY=comap(snd), H_P=L² classes measurable with respect to mY, P=i∘E[·|Y] and the canonical M:u↦u∘snd. Then H_P=ran(P), P is identity on H_P, and there exists an onto linear isometry e:L²(ν;ℝ)≃H_P with i e=M. There is a Markov kernel S whose every-state normalized law is S(y)=volume.tilted(x↦−V((y+x)/2)−‖y−x‖²/(8η)); Λ.IsCondKernel S and both Λ marginals equal ν. The same joint reflection F(x,y)=(x,2x−y) gives the involutive selfadjoint isometry U, with Uf=f∘F J-almost everywhere for every f. There is a bounded selfadjoint T on the full real L²(ν), with ‖Tu‖≤‖u‖, Tu(y)=∫u(x)S(y,dx) ν-almost everywhere for each u, and preserved integral. On H_P put A=PUP restricted via i and orthogonal projection, and B=(I_J−P)UPi:H_P→L²(J). Then A=eTe⁻¹ is selfadjoint and contractive, PB=0. There is a bounded positive operator Γ on the real scalar-valued L² space with Γ²=I−T². For the SAME transported Γ_P=eΓe⁻¹, positivity holds and Γ_P²=I_H_P−A²=B*B. There is q∈L²(ν;ℝ) equal to one ν-almost everywhere, with Tq=q and ⟨q,u⟩=∫u dν for every u. Set q_P=e q and H_P^0=ker⟨q_P,·⟩, with its inherited Hilbert structure. Membership is exactly zero ν-mean after e⁻¹. The SAME Γ_P annihilates q_P. Put γ=2√(αη)/(1+αη)>0. There exists Γ_0:H_P^0→H_P^0 equal under inclusion to the restriction of Γ_P, positive with Γ_0−γ I positive. Γ_0 is a unit in the algebra of bounded real operators. There exists a bounded real Inv on this SAME centered space with Inv Γ_0=Γ_0 Inv=I and ‖Inv‖≤1/γ. All probability, normalization, range, root, centering, spectral-gap, unit and inverse facts are internally derived from the original inputs; none is an additional public premise. αη=1 and rank-zero E remain legal. No inverse on full H_P is asserted. Define the actual closed conditional-mean-zero space H_perp=ker P in L²(J;ℝ), with its inherited complete Hilbert structure; this is not merely the globally zero-mean joint space. There exists B_0:H_P^0→H_perp whose inclusion equals B i_0. There exists V_0:H_P^0→H_perp with V_0=B_0 Inv, B_0=V_0 Γ_0, V_0* V_0=I and ‖V_0 f‖=‖f‖ for every f∈H_P^0. All these objects and identities are conclusions from the same original inputs. There exists the canonical bounded residual map R:L²(J;ℝ)→H_perp with i_perp Rg=g−Pg for every joint g. The SAME ambient adjoint satisfies B* g=i_0 B_0* Rg for every joint g; the printed intrinsic block adjoint is recovered on H_perp. For every actual joint f∈L²(J;ℝ) with ∫f dJ=0, there exists f_P∈H_P^0 whose inclusion is E[f|Y]. Put f_perp=Rf and f_V=V_0* f_perp∈the SAME H_P^0. Then B* i_perp f_perp=i_0 Γ_0 f_V=Γ_P i_0 f_V, ‖f‖²=‖f_P‖²+‖f_perp‖² and ‖f_V‖≤‖f_perp‖. The genuine original-input Test derives f=i i_0 f_P+i_perp f_perp, B* f=Γ_P i_0 f_V and ‖f_V‖²≤‖f‖²−‖f_P‖². The global zero-mean condition is a quantified input restriction to this concluded implication, not an extra assumption on the potential or an operator certificate. One private proposition definition per file stores exactly the original full statement solely to stage dependent elaboration; it assumes and proves no mathematics. No onto/coisometry,full modified-energy bound or later dynamics/cost/composition result is asserted.

\[R=I-P:\mathfrak H\to\ker P,\quad B_{\rm amb}^*g=i_0B_0^*Rg;\quad f_\perp=Rf,\quad f_V=V_0^*f_\perp\in H_P^0,\quad B_{\rm amb}^*f=\Gamma_Pi_0f_V,\quad\|f_V\|^2\le\|f\|^2-\|f_P\|^2.\]

Lean statement · actual_ambient_adjoint_centered_decomposition

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)

theorem actual_ambient_adjoint_centered_decomposition
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (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) : actual_ambient_adjoint_centered_decomposition_statement (E := E) (V := V) (α := α) (β := β) (η := η) hα hαβ hV hH hη hβη

Exact module and namespace context

Proof roadmap

1Keep the actual spaces and construct the conditional residual
Reuse the SAME actual65 laws,normalized conditional kernel,reflection,root,inverse and polar witnesses. P is conditional expectation given Y. Idempotence gives P(g−Pg)=0, so the canonical bounded map R has exact codomain ker P; R is identity there.
2Eliminate the constant direction and recover the ambient adjoint
The SAME Gram/root identities and Γ_Pq_P=0 imply Bq_P=0. Adjoint pairing therefore puts B* g in H_P^0. Pair against each centered vector, use PB=0 and selfadjointness of P to remove Pg, and obtain the canonical extension of the intrinsic block adjoint.
3Use the same polar map for the first corrector
Taking adjoints of B_0=V_0Γ_0 and positivity of Γ_0 give B_0*=Γ_0V_0*. Isometry gives operator norm at most one, hence the adjoint contraction, including the zero-dimensional case.
4Identify actual joint mean with the transported constant
Pull the ν-almost-everywhere constant q back by the actual measure-preserving second coordinate. Thus i q_P is exactly the constant-one L²(J) class, and its pairing is the Bochner integral of every joint L² observable. No representative or integrability assumption is added.
5Construct centered macroscopic input and its exact norm decomposition
For every globally centered f, selfadjoint conditional expectation and Pq_P=q_P give E[f|Y]∈H_P^0. Apply the ambient identity to Rf and its idempotence, then the SAME restricted-root relation. Orthogonal projection gives the Pythagorean norm identity.
6Consume the result at every actual globally centered input
The Test starts from the original potential,Hessian and step inputs and extracts the same witnesses. R is identity on ker P,so the ambient adjoint on f equals its value on f_perp. Together with contraction and Pythagoras this yields the actual-input corrector norm budget needed before B.20.

Full assumptions and notation

All objects and hypotheses

Finite-dimensional real Hilbert Borel base E with canonical volume, including the disclosed rank-zero extension; V is C²; 0<α≤β; both global Hessian bounds; η>0 and βη≤1.
Canonical normalized laws/kernel, onto pullback e, SAME U/T, full and centered roots, exact centering, gap, unit and bounded inverse are conclusions. Conditional actions are per-observable AE. L² is not assumed finite-dimensional.
γ=2√(αη)/(1+αη); the inverse acts only on H_P^0=ker⟨e1,·⟩ with inherited Hilbert structure; the legal endpoint αη=1 is retained.
H_perp is exactly ker P (conditional expectation given Y), while H_P^0 is the zero ν-mean macroscopic space. Their complete Hilbert structures, B_0 and V_0 are internally constructed; no onto-kerP or coisometry assumption is introduced.
The concluded global-input implication quantifies every f∈L²(J) with integral zero. R,conditional centering,constant annihilation,adjoint range and norm decomposition are derived internally. Private statement definitions expand literally to the original sealed propositions and add no premise.

Mathematical proof

1. Keep the actual spaces and construct the conditional residual

Reuse the SAME actual65 laws,normalized conditional kernel,reflection,root,inverse and polar witnesses. P is conditional expectation given Y. Idempotence gives P(g−Pg)=0, so the canonical bounded map R has exact codomain ker P; R is identity there.

\[Rg=g-Pg\in\ker P,\quad R i_\perp=I_{\ker P}.\]

Corresponding Lean step

  classical
  dsimp only
  let μ := (volume : Measure E).tilted (fun x => -V x)
  let J := (μ.prod (stdGaussian E)).map
    (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2))
  let ν := J.snd
  let mY : MeasurableSpace (E × E) := MeasurableSpace.comap Prod.snd (inferInstance : MeasurableSpace E)
  letI : MeasurableSpace (E × E) := Prod.instMeasurableSpace
  letI : Fact (mY ≤ (inferInstance : MeasurableSpace (E × E))) := ⟨measurable_snd.comap_le⟩
  let HP := lpMeas ℝ ℝ mY 2 J
  letI : NormedAddCommGroup HP := HP.normedAddCommGroup
  letI : InnerProductSpace ℝ HP := HP.innerProductSpace
  let P : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J :=
    HP.subtypeL ∘L condExpL2 ℝ ℝ (μ := J) measurable_snd.comap_le
  have hBase := AutoSamplingTheory.ExampleCases.ProximalBPS.PolarIsometry.actual_centered_polar_isometry
    (E:=E) (V:=V) (α:=α) (β:=β) (η:=η) hα hαβ hV hH hη hβη
  dsimp only at hBase
  rcases hBase with
    ⟨hμ,hJ,hν,hRange,hPf,S,hS,hSd,hSc,hSf,hSs,e,he,U,hU,hUi,hUs,
      T,hTs,hAll,hAeq,hAs,hAn,hPB,Γ,hΓ,hΓSq,hΓP,hΓPSq,hGram,
      q,hqa,hTq,hq,hCenter,hΓPq,hγ,ΓP0,hΓP0,hPos0,hOrder0,hUnit,
      Inv,hLeft,hRight,hNormInv,B0,hB0,V0,hVdef,hFactor,hVadj,hVnorm⟩
  let A : HP →L[ℝ] HP := HP.orthogonalProjectionOnto ∘L U.toContinuousLinearMap ∘L HP.subtypeL
  let B : HP →L[ℝ] Lp ℝ 2 J :=
    (((1 : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J)-P)*U.toContinuousLinearMap*P) ∘L HP.subtypeL
  let ΓP : HP →L[ℝ] HP := e.conjStarAlgEquiv Γ
  let qP : HP := e q
  let HP0 := (innerSL ℝ qP).ker
  letI : NormedAddCommGroup HP0 := HP0.normedAddCommGroup
  letI : InnerProductSpace ℝ HP0 := HP0.innerProductSpace
  letI : CompleteSpace HP0 := (innerSL ℝ qP).isClosed_ker.completeSpace_coe
  let Hperp := P.ker
  letI : NormedAddCommGroup Hperp := Hperp.normedAddCommGroup
  letI : InnerProductSpace ℝ Hperp := Hperp.innerProductSpace
  letI : CompleteSpace Hperp := P.isClosed_ker.completeSpace_coe
  change HP0 →L[ℝ] Hperp at B0 V0
  change HP0 →L[ℝ] HP0 at ΓP0 Inv
  letI : IsProbabilityMeasure J := hJ
  letI : IsProbabilityMeasure ν := hν
  let C : Lp ℝ 2 J →L[ℝ] HP := condExpL2 ℝ ℝ (μ:=J) measurable_snd.comap_le
  have hPself (g k : Lp ℝ 2 J) : inner ℝ (P g) k=inner ℝ g (P k) :=
    inner_condExpL2_left_eq_right measurable_snd.comap_le
  have hPid (g : Lp ℝ 2 J) : P (P g)=P g := hPf (C g)
  let R : Lp ℝ 2 J →L[ℝ] Hperp :=
    ((1 : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J)-P).codRestrict Hperp (by
      intro g
      change P (g-P g)=0
      rw [map_sub,hPid,sub_self])
  have hR (g : Lp ℝ 2 J) : (R g : Lp ℝ 2 J)=g-P g := rfl
  have hRself (g : Hperp) : R (g : Lp ℝ 2 J)=g := by
    apply Subtype.ext
    change (g : Lp ℝ 2 J)-P g=g
    rw [show P (g : Lp ℝ 2 J)=0 from g.property,sub_zero]