Actual PBPS typed polar isometry and adjoint corrector
AutoSamplingTheory.ExampleCases.ProximalBPS.PolarIsometry.actual_centered_polar_isometry · theorem · Teaching coverage
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. The genuine original-input consumer proves B_0* g=Γ_0 V_0* g, ‖V_0* g‖≤‖g‖ and V_0*(g−V_0 V_0* g)=0 for every g∈H_perp. No surjectivity onto H_perp or equality V_0 V_0*=I on that entire space is claimed.
Lean statement · actual_centered_polar_isometry
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. The genuine original-input consumer proves B_0* g=Γ_0 V_0* g, ‖V_0* g‖≤‖g‖ and V_0*(g−V_0 V_0* g)=0 for every g∈H_perp. No surjectivity onto H_perp or equality V_0 V_0*=I on that entire space is claimed.
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 actual_centered_polar_isometry
{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) :
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 Λ := J.map (fun p : E × E => (p.2,(2 : ℝ) • p.1-p.2))
let F := fun p : E × E => (p.1,(2 : ℝ) • p.1-p.2)
let mY := 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
let P : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J :=
HP.subtypeL ∘L condExpL2 ℝ ℝ (μ := J) measurable_snd.comap_le
let hp : MeasurePreserving (Prod.snd : E × E → E) J ν := ⟨measurable_snd,rfl⟩
let M : Lp ℝ 2 ν →ₗᵢ[ℝ] Lp ℝ 2 J := Lp.compMeasurePreservingₗᵢ ℝ Prod.snd hp
IsProbabilityMeasure μ ∧ IsProbabilityMeasure J ∧ IsProbabilityMeasure ν ∧
HP = P.toLinearMap.range ∧
(∀ f : HP, P (f : Lp ℝ 2 J) = f) ∧
∃ S : Kernel E E, IsMarkovKernel S ∧
(∀ y, S y = (volume : Measure E).tilted
(fun x => -V ((1/2 : ℝ) • (y+x)) - ‖y-x‖^2/(8*η))) ∧
Λ.IsCondKernel S ∧ Λ.fst = ν ∧ Λ.snd = ν ∧
∃ e : Lp ℝ 2 ν ≃ₗᵢ[ℝ] HP,
(∀ u : Lp ℝ 2 ν, (e u : Lp ℝ 2 J) = M u) ∧
∃ U : Lp ℝ 2 J →ₗᵢ[ℝ] Lp ℝ 2 J,
(∀ g : Lp ℝ 2 J, (U g : E × E → ℝ) =ᵐ[J] g ∘ F) ∧
Function.Involutive U ∧ IsSelfAdjoint U.toContinuousLinearMap ∧
∃ T : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν,
IsSelfAdjoint T ∧
(∀ u : Lp ℝ 2 ν,
‖T u‖ ≤ ‖u‖ ∧
(T u : E → ℝ) =ᵐ[ν] (fun y => ∫ x, u x ∂S y) ∧
(∫ y, T u y ∂ν) = ∫ y, u y ∂ν) ∧
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
A = e.conjStarAlgEquiv T ∧ IsSelfAdjoint A ∧
(∀ f : HP, ‖A f‖ ≤ ‖f‖) ∧
(∀ f : HP, P (B f) = 0) ∧
∃ Γ : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν,
Γ.IsPositive ∧ Γ*Γ=(1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)-T*T ∧
let ΓP : HP →L[ℝ] HP := e.conjStarAlgEquiv Γ
ΓP.IsPositive ∧ ΓP*ΓP=(1 : HP →L[ℝ] HP)-A*A ∧
B.adjoint ∘L B = ΓP*ΓP ∧
∃ q : Lp ℝ 2 ν,
(q : E → ℝ) =ᵐ[ν] (fun _ => (1 : ℝ)) ∧ T q = q ∧
(∀ u : Lp ℝ 2 ν, inner ℝ q u = ∫ y, u y ∂ν) ∧
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 γ : ℝ := 2*Real.sqrt ((α : ℝ)*η)/(1+(α : ℝ)*η)
(∀ f : HP, f ∈ HP0 ↔ (∫ y, (e.symm f) y ∂ν) = 0) ∧
ΓP qP = 0 ∧ 0 < γ ∧
∃ ΓP0 : HP0 →L[ℝ] HP0,
(∀ f : HP0, (ΓP0 f : HP) = ΓP (f : HP)) ∧
ΓP0.IsPositive ∧ (ΓP0-γ • (1 : HP0 →L[ℝ] HP0)).IsPositive ∧
IsUnit ΓP0 ∧
∃ Inv : HP0 →L[ℝ] HP0,
Inv*ΓP0=(1 : HP0 →L[ℝ] HP0) ∧
ΓP0*Inv=(1 : HP0 →L[ℝ] HP0) ∧ ‖Inv‖ ≤ 1/γ ∧
let Hperp := P.ker
letI : NormedAddCommGroup Hperp := Hperp.normedAddCommGroup
letI : InnerProductSpace ℝ Hperp := Hperp.innerProductSpace
letI : CompleteSpace Hperp := P.isClosed_ker.completeSpace_coe
∃ B0 : HP0 →L[ℝ] Hperp,
(∀ f : HP0, (B0 f : Lp ℝ 2 J) = B (f : HP)) ∧
∃ V0 : HP0 →L[ℝ] Hperp,
V0 = B0 ∘L Inv ∧ B0 = V0 ∘L ΓP0 ∧
V0.adjoint ∘L V0 = (1 : HP0 →L[ℝ] HP0) ∧
(∀ f : HP0, ‖V0 f‖ = ‖f‖)Proof roadmap
- 1Restrict actual leakage to the exact closed conditional kernel
Reuse the same accepted actual laws, normalized kernel, reflection, macroscopic equivalence, centered root and bounded inverse. Since PB=0, codRestrict produces B_0 with codomain ker P. The centered domain and conditional kernel inherit completeness internally; no range or completeness premise is supplied.
- 2Normalize by the same centered inverse
Set V_0=B_0 Inv. The SAME Gram equality B*B=Γ_P² and positivity give ‖B i_0 u‖=‖Γ_P i_0 u‖. The exact restricted-root relation and Γ_0 Inv=I turn this into ‖V_0 f‖=‖f‖ for every centered f.
- 3Prove factorization and the isometric adjoint identity
The other cancellation Inv Γ_0=I gives B_0=V_0 Γ_0 by application to each vector. Norm preservation gives V_0*V_0=I on H_P^0. It does not make V_0 onto ker P.
- 4Consume the factorization in the actual adjoint corrector
The Test starts from the original potential, Hessian and step inputs and extracts these same witnesses. Taking adjoints of B_0=V_0 Γ_0 and using the positivity, hence selfadjointness, of Γ_0 gives the exact first-corrector action.
- 5Retain contraction and the orthogonal residual
Norm preservation bounds ‖V_0‖≤1, hence ‖V_0*‖≤1, including the zero-dimensional case. Evaluating V_0*V_0=I at V_0*g proves that the residual g−V_0V_0*g is annihilated by V_0*. The Test does not replace contraction by norm equality on all ker P.
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.
Mathematical proof
1. Restrict actual leakage to the exact closed conditional kernel
Reuse the same accepted actual laws, normalized kernel, reflection, macroscopic equivalence, centered root and bounded inverse. Since PB=0, codRestrict produces B_0 with codomain ker P. The centered domain and conditional kernel inherit completeness internally; no range or completeness premise is supplied.
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.CenteredRootOrderInverse.actual_centered_root_order_inverse
(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⟩
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
let B0 : HP0 →L[ℝ] Hperp :=
(B ∘L HP0.subtypeL).codRestrict Hperp (by intro f; exact hPB (f : HP))
have hB0 (f : HP0) : (B0 f : Lp ℝ 2 J)=B (f : HP) := rfl
Literal compiled BODY excerpt; preceding exact local definitions and derived facts remain in scope.
2. Normalize by the same centered inverse
Set V_0=B_0 Inv. The SAME Gram equality B*B=Γ_P² and positivity give ‖B i_0 u‖=‖Γ_P i_0 u‖. The exact restricted-root relation and Γ_0 Inv=I turn this into ‖V_0 f‖=‖f‖ for every centered f.
Corresponding Lean step
let V0 : HP0 →L[ℝ] Hperp := B0 ∘L Inv
have hGramLocal : B.adjoint ∘L B=ΓP*ΓP := hGram
have hPosLocal : ΓP.IsPositive := hΓP
have hVnorm (f : HP0) : ‖V0 f‖=‖f‖ := by
let g : HP0 := Inv f
have hg : ΓP0 g=f := congrArg (fun C : HP0 →L[ℝ] HP0 => C f) hRight
have hb := B.apply_norm_sq_eq_inner_adjoint_right (g : HP)
have hr := ΓP.apply_norm_sq_eq_inner_adjoint_right (g : HP)
rw [hGramLocal] at hb
rw [hPosLocal.isSelfAdjoint.adjoint_eq] at hr
have hNorm : ‖B (g : HP)‖=‖ΓP (g : HP)‖ :=
(sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)).mp (hb.trans hr.symm)
calc
‖V0 f‖=‖B (g : HP)‖ := rfl
_ = ‖ΓP (g : HP)‖ := hNorm
_ = ‖ΓP0 g‖ := congrArg (fun z : HP => ‖z‖) (hΓP0 g).symm
_ = ‖f‖ := congrArg (fun z : HP0 => ‖z‖) hg
Literal compiled BODY excerpt; preceding exact local definitions and derived facts remain in scope.
3. Prove factorization and the isometric adjoint identity
The other cancellation Inv Γ_0=I gives B_0=V_0 Γ_0 by application to each vector. Norm preservation gives V_0*V_0=I on H_P^0. It does not make V_0 onto ker P.
Corresponding Lean step
have hFactor : B0=V0 ∘L ΓP0 := by
apply ContinuousLinearMap.ext
intro f
change B0 f=B0 (Inv (ΓP0 f))
have hf : Inv (ΓP0 f)=f := congrArg (fun C : HP0 →L[ℝ] HP0 => C f) hLeft
rw [hf]
have hVadj : V0.adjoint ∘L V0=(1 : HP0 →L[ℝ] HP0) :=
(ContinuousLinearMap.norm_map_iff_adjoint_comp_self V0).mp hVnorm
Literal compiled BODY excerpt; preceding exact local definitions and derived facts remain in scope.
4. Consume the factorization in the actual adjoint corrector
The Test starts from the original potential, Hessian and step inputs and extracts these same witnesses. Taking adjoints of B_0=V_0 Γ_0 and using the positivity, hence selfadjointness, of Γ_0 gives the exact first-corrector action.
Corresponding Lean step
have hBAdj : B0.adjoint=ΓP0 ∘L V0.adjoint := by
calc
B0.adjoint = (V0 ∘L ΓP0).adjoint :=
congrArg (fun C : HP0 →L[ℝ] Hperp => C.adjoint) hFactor
_ = ΓP0.adjoint ∘L V0.adjoint := ContinuousLinearMap.adjoint_comp V0 ΓP0
_ = ΓP0 ∘L V0.adjoint :=
congrArg (fun C : HP0 →L[ℝ] HP0 => C ∘L V0.adjoint)
hPosLocal.isSelfAdjoint.adjoint_eq
Literal compiled BODY excerpt; preceding exact local definitions and derived facts remain in scope.
5. Retain contraction and the orthogonal residual
Norm preservation bounds ‖V_0‖≤1, hence ‖V_0*‖≤1, including the zero-dimensional case. Evaluating V_0*V_0=I at V_0*g proves that the residual g−V_0V_0*g is annihilated by V_0*. The Test does not replace contraction by norm equality on all ker P.
Corresponding Lean step
have hNormV : ‖V0‖ ≤ (1 : ℝ) :=
ContinuousLinearMap.opNorm_le_bound _ zero_le_one (by intro f; rw [hVnorm f,one_mul])
have hNormAdj : ‖V0.adjoint‖ ≤ (1 : ℝ) :=
(ContinuousLinearMap.adjoint.norm_map V0).trans_le hNormV
refine ⟨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,?_,?_,?_⟩
· intro g
exact congrArg (fun C : Hperp →L[ℝ] HP0 => C g) hBAdj
· intro g
calc
‖V0.adjoint g‖ ≤ ‖V0.adjoint‖*‖g‖ := V0.adjoint.le_opNorm g
_ ≤ 1*‖g‖ := mul_le_mul_of_nonneg_right hNormAdj (norm_nonneg _)
_ = ‖g‖ := one_mul _
· intro g
have hf : V0.adjoint (V0 (V0.adjoint g))=V0.adjoint g :=
congrArg (fun C : HP0 →L[ℝ] HP0 => C (V0.adjoint g)) hVadj
exact (map_sub V0.adjoint g (V0 (V0.adjoint g))).trans (sub_eq_zero.mpr hf.symm)
Literal compiled BODY excerpt; preceding exact local definitions and derived facts remain in scope.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · actual_centered_polar_isometry
Restrict actual leakage to the exact closed conditional kernel; Normalize by the same centered inverse; Prove factorization and the isometric adjoint identity; Consume the factorization in the actual adjoint corrector; Retain contraction and the orthogonal residual
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 actual_centered_polar_isometry
{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) :
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 Λ := J.map (fun p : E × E => (p.2,(2 : ℝ) • p.1-p.2))
let F := fun p : E × E => (p.1,(2 : ℝ) • p.1-p.2)
let mY := 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
let P : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J :=
HP.subtypeL ∘L condExpL2 ℝ ℝ (μ := J) measurable_snd.comap_le
let hp : MeasurePreserving (Prod.snd : E × E → E) J ν := ⟨measurable_snd,rfl⟩
let M : Lp ℝ 2 ν →ₗᵢ[ℝ] Lp ℝ 2 J := Lp.compMeasurePreservingₗᵢ ℝ Prod.snd hp
IsProbabilityMeasure μ ∧ IsProbabilityMeasure J ∧ IsProbabilityMeasure ν ∧
HP = P.toLinearMap.range ∧
(∀ f : HP, P (f : Lp ℝ 2 J) = f) ∧
∃ S : Kernel E E, IsMarkovKernel S ∧
(∀ y, S y = (volume : Measure E).tilted
(fun x => -V ((1/2 : ℝ) • (y+x)) - ‖y-x‖^2/(8*η))) ∧
Λ.IsCondKernel S ∧ Λ.fst = ν ∧ Λ.snd = ν ∧
∃ e : Lp ℝ 2 ν ≃ₗᵢ[ℝ] HP,
(∀ u : Lp ℝ 2 ν, (e u : Lp ℝ 2 J) = M u) ∧
∃ U : Lp ℝ 2 J →ₗᵢ[ℝ] Lp ℝ 2 J,
(∀ g : Lp ℝ 2 J, (U g : E × E → ℝ) =ᵐ[J] g ∘ F) ∧
Function.Involutive U ∧ IsSelfAdjoint U.toContinuousLinearMap ∧
∃ T : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν,
IsSelfAdjoint T ∧
(∀ u : Lp ℝ 2 ν,
‖T u‖ ≤ ‖u‖ ∧
(T u : E → ℝ) =ᵐ[ν] (fun y => ∫ x, u x ∂S y) ∧
(∫ y, T u y ∂ν) = ∫ y, u y ∂ν) ∧
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
A = e.conjStarAlgEquiv T ∧ IsSelfAdjoint A ∧
(∀ f : HP, ‖A f‖ ≤ ‖f‖) ∧
(∀ f : HP, P (B f) = 0) ∧
∃ Γ : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν,
Γ.IsPositive ∧ Γ*Γ=(1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)-T*T ∧
let ΓP : HP →L[ℝ] HP := e.conjStarAlgEquiv Γ
ΓP.IsPositive ∧ ΓP*ΓP=(1 : HP →L[ℝ] HP)-A*A ∧
B.adjoint ∘L B = ΓP*ΓP ∧
∃ q : Lp ℝ 2 ν,
(q : E → ℝ) =ᵐ[ν] (fun _ => (1 : ℝ)) ∧ T q = q ∧
(∀ u : Lp ℝ 2 ν, inner ℝ q u = ∫ y, u y ∂ν) ∧
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 γ : ℝ := 2*Real.sqrt ((α : ℝ)*η)/(1+(α : ℝ)*η)
(∀ f : HP, f ∈ HP0 ↔ (∫ y, (e.symm f) y ∂ν) = 0) ∧
ΓP qP = 0 ∧ 0 < γ ∧
∃ ΓP0 : HP0 →L[ℝ] HP0,
(∀ f : HP0, (ΓP0 f : HP) = ΓP (f : HP)) ∧
ΓP0.IsPositive ∧ (ΓP0-γ • (1 : HP0 →L[ℝ] HP0)).IsPositive ∧
IsUnit ΓP0 ∧
∃ Inv : HP0 →L[ℝ] HP0,
Inv*ΓP0=(1 : HP0 →L[ℝ] HP0) ∧
ΓP0*Inv=(1 : HP0 →L[ℝ] HP0) ∧ ‖Inv‖ ≤ 1/γ ∧
let Hperp := P.ker
letI : NormedAddCommGroup Hperp := Hperp.normedAddCommGroup
letI : InnerProductSpace ℝ Hperp := Hperp.innerProductSpace
letI : CompleteSpace Hperp := P.isClosed_ker.completeSpace_coe
∃ B0 : HP0 →L[ℝ] Hperp,
(∀ f : HP0, (B0 f : Lp ℝ 2 J) = B (f : HP)) ∧
∃ V0 : HP0 →L[ℝ] Hperp,
V0 = B0 ∘L Inv ∧ B0 = V0 ∘L ΓP0 ∧
V0.adjoint ∘L V0 = (1 : HP0 →L[ℝ] HP0) ∧
(∀ f : HP0, ‖V0 f‖ = ‖f‖) := by
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.CenteredRootOrderInverse.actual_centered_root_order_inverse
(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⟩
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
let B0 : HP0 →L[ℝ] Hperp :=
(B ∘L HP0.subtypeL).codRestrict Hperp (by intro f; exact hPB (f : HP))
have hB0 (f : HP0) : (B0 f : Lp ℝ 2 J)=B (f : HP) := rfl
let V0 : HP0 →L[ℝ] Hperp := B0 ∘L Inv
have hGramLocal : B.adjoint ∘L B=ΓP*ΓP := hGram
have hPosLocal : ΓP.IsPositive := hΓP
have hVnorm (f : HP0) : ‖V0 f‖=‖f‖ := by
let g : HP0 := Inv f
have hg : ΓP0 g=f := congrArg (fun C : HP0 →L[ℝ] HP0 => C f) hRight
have hb := B.apply_norm_sq_eq_inner_adjoint_right (g : HP)
have hr := ΓP.apply_norm_sq_eq_inner_adjoint_right (g : HP)
rw [hGramLocal] at hb
rw [hPosLocal.isSelfAdjoint.adjoint_eq] at hr
have hNorm : ‖B (g : HP)‖=‖ΓP (g : HP)‖ :=
(sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)).mp (hb.trans hr.symm)
calc
‖V0 f‖=‖B (g : HP)‖ := rfl
_ = ‖ΓP (g : HP)‖ := hNorm
_ = ‖ΓP0 g‖ := congrArg (fun z : HP => ‖z‖) (hΓP0 g).symm
_ = ‖f‖ := congrArg (fun z : HP0 => ‖z‖) hg
have hFactor : B0=V0 ∘L ΓP0 := by
apply ContinuousLinearMap.ext
intro f
change B0 f=B0 (Inv (ΓP0 f))
have hf : Inv (ΓP0 f)=f := congrArg (fun C : HP0 →L[ℝ] HP0 => C f) hLeft
rw [hf]
have hVadj : V0.adjoint ∘L V0=(1 : HP0 →L[ℝ] HP0) :=
(ContinuousLinearMap.norm_map_iff_adjoint_comp_self V0).mp hVnorm
exact ⟨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,rfl,
hFactor,hVadj,hVnorm⟩
end
end AutoSamplingTheory.ExampleCases.ProximalBPS.PolarIsometryScope and omitted-condition boundaries
- Only exact B16 typed polar/factorization/isometry and first adjoint-corrector consumer. No onto ker P or V V.adjoint=I on all ker P, no new H1/B13/B14-floor/small-step/root/gap/unit premise. Rank0/alphaeta1 retained. B17 quantitative contraction, remaining H1/operator inequalities,dynamics/invariance/nonexplosion/hypocoercivity/main/errors/actual-input expected query costs and composition remain open.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- ContinuousLinearMap.codRestrict
- ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_right
- ContinuousLinearMap.norm_map_iff_adjoint_comp_self
- ContinuousLinearMap.adjoint_comp
- ContinuousLinearMap.opNorm_le_bound
- ContinuousLinearMap.adjoint.norm_map
Mathematical sources
- PBPS arXiv2609.06905v1 Appendix B16, inherited B11/B15 and first corrector f_V=V.adjoint f_perp; exact original finite-dimensional C2/two Hessian/positive capped eta inputs. — Only exact B16 typed polar/factorization/isometry and first adjoint-corrector consumer. No onto ker P or V V.adjoint=I on all ker P, no new H1/B13/B14-floor/small-step/root/gap/unit premise. Rank0/alphaeta1 retained. B17 quantitative contraction, remaining H1/operator inequalities,dynamics/invariance/nonexplosion/hypocoercivity/main/errors/actual-input expected query costs and composition remain open.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.