Same actual PBPS root and centered inverse commutation
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualRootCommutation.actual_same_root_inverse_commutation · 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. 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 preceding independently reviewed ambient-adjoint 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. The SAME root commutes with T and its transport commutes with A. The SAME Inv on H_P^0 is selfadjoint. There exists an internally constructed A_0:H_P^0→H_P^0 whose inclusion equals A after inclusion; it is selfadjoint,commutes with Γ_0,satisfies A_0²+Γ_0²=I,and commutes with the SAME Inv. The genuine original-input Test proves K=A_0 Inv selfadjoint and I+K²=Inv². All old ambient-adjoint/global-centered-observable conclusions persist. These are ingredients for sharp B23 and B21;neither estimate/rotation nor full dynamics,expected costs or composition is asserted. Private literal proposition definitions store the complete original statements and add no premise or provider.
Lean statement · actual_same_root_inverse_commutation
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 preceding independently reviewed ambient-adjoint 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. The SAME root commutes with T and its transport commutes with A. The SAME Inv on H_P^0 is selfadjoint. There exists an internally constructed A_0:H_P^0→H_P^0 whose inclusion equals A after inclusion; it is selfadjoint,commutes with Γ_0,satisfies A_0²+Γ_0²=I,and commutes with the SAME Inv. The genuine original-input Test proves K=A_0 Inv selfadjoint and I+K²=Inv². All old ambient-adjoint/global-centered-observable conclusions persist. These are ingredients for sharp B23 and B21;neither estimate/rotation nor full dynamics,expected costs or composition is asserted. Private literal proposition definitions store the complete original statements and add no premise or provider.
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_same_root_inverse_commutation
{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_same_root_inverse_commutation_statement (E := E) (V := V) (α := α) (β := β) (η := η) hα hαβ hV hH hη hβηProof roadmap
- 1Retain the exact actual witnesses
Reuse the original-input parent and SAME laws,kernel,operators,roots,inverse,polar and centered geometry;fix their exact spaces.
- 2Produce positivity and root commutation internally
Selfadjoint contraction and Cauchy-Schwarz give I+T positive. Γ²=I−T² commutes with I+T. The reusable leaf then yields Γ commuting with T.
- 3Transport and construct the exact centered restriction
Conjugate commutation. Tq=q implies AqP=qP;symmetry preserves the exact zero-mean kernel. Construct A0 by codomain restriction and prove selfadjointness.
- 4Restrict the square identity and commutation
Use exact inclusion identities and injectivity of the centered subspace inclusion.
- 5Cancel with the same inverse
Taking adjoints gives Γ0 Inv*=I. Both inverse identities imply Inv selfadjoint;commutation of A0 with Γ0 passes to Inv by cancellation.
- 6Consume the B23 coefficient identity at original inputs
The Test starts from the original potential and step inputs. The product of commuting selfadjoint operators is selfadjoint;multiplying the exact square identity by Inv² gives the coefficient identity.
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. Retain the exact actual witnesses
Reuse the original-input parent and SAME laws,kernel,operators,roots,inverse,polar and centered geometry;fix their exact spaces.
Corresponding Lean step
classical
unfold actual_same_root_inverse_commutation_statement
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.AmbientAdjointCorrector.actual_ambient_adjoint_centered_decomposition
(E:=E) (V:=V) (α:=α) (β:=β) (η:=η) hα hαβ hV hH hη hβη
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,R,hR,hAmbient,hGlobal⟩
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
change Lp ℝ 2 J →L[ℝ] Hperp at R
change (∀ g : Lp ℝ 2 J, (R g : Lp ℝ 2 J)=g-P g) at hR
change (∀ g : Lp ℝ 2 J,
B.adjoint g=HP0.subtypeL (B0.adjoint (R g))) at hAmbient
change (∀ f : Lp ℝ 2 J, (∫ z, f z ∂J)=0 →
∃ fP : HP0,
HP0.subtypeL fP=condExpL2 ℝ ℝ (μ:=J) measurable_snd.comap_le f ∧
let fperp : Hperp := R f
let fV : HP0 := V0.adjoint fperp
B.adjoint (fperp : Lp ℝ 2 J)=HP0.subtypeL (ΓP0 fV) ∧
HP0.subtypeL (ΓP0 fV)=ΓP (HP0.subtypeL fV) ∧
‖f‖^2=‖fP‖^2+‖fperp‖^2 ∧ ‖fV‖≤‖fperp‖) at hGlobal
Literal compiled BODY span;exact preceding locals remain in scope.
2. Produce positivity and root commutation internally
Selfadjoint contraction and Cauchy-Schwarz give I+T positive. Γ²=I−T² commutes with I+T. The reusable leaf then yields Γ commuting with T.
Corresponding Lean step
have hAeqLocal : A=e.conjStarAlgEquiv T := hAeq
have hAsLocal : IsSelfAdjoint A := hAs
have hLeftLocal : Inv*ΓP0=(1 : HP0 →L[ℝ] HP0) := hLeft
have hPosLocal : ΓP0.IsPositive := hPos0
have hDpos : ((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)+T).IsPositive := by
refine ⟨((IsSelfAdjoint.one (Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)).add hTs).isSymmetric,?_⟩
intro u
change 0 ≤ inner ℝ (u+T u) u
rw [inner_add_left,real_inner_self_eq_norm_sq]
have hn : ‖T u‖≤‖u‖ := (hAll u).1
have hi := (abs_le.mp (abs_real_inner_le_norm (T u) u)).1
nlinarith only [hn,hi,norm_nonneg u]
have hCommSquare : Commute (Γ*Γ) ((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)+T) := by
rw [hΓSq]
show (1-T*T)*(1+T)=(1+T)*(1-T*T)
noncomm_ring
have hCommRootPlus := AutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareCommute.positive_square_commutation
ν Γ (1+T) hΓ hDpos hCommSquare
have hCommRoot : Commute Γ T := by
have h := hCommRootPlus.eq
simp only [mul_add,add_mul,mul_one,one_mul] at h
exact add_left_cancel h
Literal compiled BODY span;exact preceding locals remain in scope.
3. Transport and construct the exact centered restriction
Conjugate commutation. Tq=q implies AqP=qP;symmetry preserves the exact zero-mean kernel. Construct A0 by codomain restriction and prove selfadjointness.
Corresponding Lean step
have hCommP : Commute ΓP A := by
change ΓP*A=A*ΓP
change (e.conjStarAlgEquiv Γ)*A=A*(e.conjStarAlgEquiv Γ)
rw [hAeqLocal,← map_mul,← map_mul,hCommRoot.eq]
have hAq : A qP=qP := by
rw [hAeqLocal]
change e (T (e.symm (e q)))=e q
rw [e.symm_apply_apply,hTq]
have hAPreserves (u : HP0) : A (u : HP) ∈ HP0 := by
change inner ℝ qP (A (u : HP))=0
calc
inner ℝ qP (A (u : HP))=inner ℝ (A qP) (u : HP) :=
(hAsLocal.isSymmetric qP (u : HP)).symm
_ = inner ℝ qP (u : HP) := by rw [hAq]
_ = 0 := u.property
let A0 : HP0 →L[ℝ] HP0 := (A.comp HP0.subtypeL).codRestrict HP0 hAPreserves
have hA0 (u : HP0) : (A0 u : HP)=A (u : HP) := rfl
have hA0self : IsSelfAdjoint A0 := by
apply ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric.mpr
intro u v
exact hAsLocal.isSymmetric (u : HP) (v : HP)
Literal compiled BODY span;exact preceding locals remain in scope.
4. Restrict the square identity and commutation
Use exact inclusion identities and injectivity of the centered subspace inclusion.
Corresponding Lean step
have hComm0 : Commute A0 ΓP0 := by
apply ContinuousLinearMap.ext
intro u
apply Subtype.ext
change (A0 (ΓP0 u) : HP)=(ΓP0 (A0 u) : HP)
rw [hA0,hΓP0,hΓP0,hA0]
exact congrArg (fun D : HP →L[ℝ] HP => D (u : HP)) hCommP.eq.symm
have hSquare0 : A0*A0+ΓP0*ΓP0=(1 : HP0 →L[ℝ] HP0) := by
apply ContinuousLinearMap.ext
intro u
apply Subtype.ext
change (A0 (A0 u) : HP)+(ΓP0 (ΓP0 u) : HP)=(u : HP)
rw [hA0,hA0,hΓP0,hΓP0]
have h : ΓP (ΓP (u : HP))=(u : HP)-A (A (u : HP)) :=
congrArg (fun D : HP →L[ℝ] HP => D (u : HP)) hΓPSq
rw [h]
abel
Literal compiled BODY span;exact preceding locals remain in scope.
5. Cancel with the same inverse
Taking adjoints gives Γ0 Inv*=I. Both inverse identities imply Inv selfadjoint;commutation of A0 with Γ0 passes to Inv by cancellation.
Corresponding Lean step
have hStarInv : ΓP0*star Inv=(1 : HP0 →L[ℝ] HP0) := by
have h := congrArg (fun D : HP0 →L[ℝ] HP0 => star D) hLeftLocal
simpa only [star_mul,hPosLocal.isSelfAdjoint.star_eq,star_one] using h
have hInvSelf : IsSelfAdjoint Inv := by
change star Inv=Inv
calc
star Inv=(Inv*ΓP0)*star Inv := by rw [hLeft,one_mul]
_ = Inv*(ΓP0*star Inv) := mul_assoc _ _ _
_ = Inv := by rw [hStarInv,mul_one]
have hCommInv : Commute A0 Inv := by
change A0*Inv=Inv*A0
calc
A0*Inv=(Inv*ΓP0)*(A0*Inv) := by rw [hLeft,one_mul]
_ = Inv*((ΓP0*A0)*Inv) := by noncomm_ring
_ = Inv*((A0*ΓP0)*Inv) := by rw [hComm0.eq.symm]
_ = Inv*A0 := by simp only [mul_assoc,hRight,mul_one]
Literal compiled BODY span;exact preceding locals remain in scope.
6. Consume the B23 coefficient identity at original inputs
The Test starts from the original potential and step inputs. The product of commuting selfadjoint operators is selfadjoint;multiplying the exact square identity by Inv² gives the coefficient identity.
Corresponding Lean step
have hKself : IsSelfAdjoint (A0*Inv) := (hA0self.commute_iff hInvSelf).mp hCommInv
have hCoefficient : (1 : HP0 →L[ℝ] HP0)+(A0*Inv)*(A0*Inv)=Inv*Inv := by
have hFirst : (ΓP0*ΓP0)*(Inv*Inv)=(1 : HP0 →L[ℝ] HP0) := by
calc
(ΓP0*ΓP0)*(Inv*Inv)=ΓP0*((ΓP0*Inv)*Inv) := by noncomm_ring
_ = (1 : HP0 →L[ℝ] HP0) := by rw [hRight,one_mul,hRight]
have hSecond : (A0*Inv)*(A0*Inv)=(A0*A0)*(Inv*Inv) := by
calc
(A0*Inv)*(A0*Inv)=A0*((Inv*A0)*Inv) := by noncomm_ring
_ = A0*((A0*Inv)*Inv) := by rw [hCommInv.eq.symm]
_ = (A0*A0)*(Inv*Inv) := by noncomm_ring
calc
(1 : HP0 →L[ℝ] HP0)+(A0*Inv)*(A0*Inv)=
(ΓP0*ΓP0)*(Inv*Inv)+(A0*A0)*(Inv*Inv) := by rw [hFirst,hSecond]
_ = (ΓP0*ΓP0+A0*A0)*(Inv*Inv) := by rw [add_mul]
_ = Inv*Inv := by rw [add_comm,hSquare0,one_mul]
Literal compiled BODY span;exact preceding locals 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_same_root_inverse_commutation
Retain the exact actual witnesses; Produce positivity and root commutation internally; Transport and construct the exact centered restriction; Restrict the square identity and commutation; Cancel with the same inverse; Consume the B23 coefficient identity at original inputs
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_same_root_inverse_commutation
{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_same_root_inverse_commutation_statement (E := E) (V := V) (α := α) (β := β) (η := η) hα hαβ hV hH hη hβη := by
classical
unfold actual_same_root_inverse_commutation_statement
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.AmbientAdjointCorrector.actual_ambient_adjoint_centered_decomposition
(E:=E) (V:=V) (α:=α) (β:=β) (η:=η) hα hαβ hV hH hη hβη
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,R,hR,hAmbient,hGlobal⟩
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
change Lp ℝ 2 J →L[ℝ] Hperp at R
change (∀ g : Lp ℝ 2 J, (R g : Lp ℝ 2 J)=g-P g) at hR
change (∀ g : Lp ℝ 2 J,
B.adjoint g=HP0.subtypeL (B0.adjoint (R g))) at hAmbient
change (∀ f : Lp ℝ 2 J, (∫ z, f z ∂J)=0 →
∃ fP : HP0,
HP0.subtypeL fP=condExpL2 ℝ ℝ (μ:=J) measurable_snd.comap_le f ∧
let fperp : Hperp := R f
let fV : HP0 := V0.adjoint fperp
B.adjoint (fperp : Lp ℝ 2 J)=HP0.subtypeL (ΓP0 fV) ∧
HP0.subtypeL (ΓP0 fV)=ΓP (HP0.subtypeL fV) ∧
‖f‖^2=‖fP‖^2+‖fperp‖^2 ∧ ‖fV‖≤‖fperp‖) at hGlobal
have hAeqLocal : A=e.conjStarAlgEquiv T := hAeq
have hAsLocal : IsSelfAdjoint A := hAs
have hLeftLocal : Inv*ΓP0=(1 : HP0 →L[ℝ] HP0) := hLeft
have hPosLocal : ΓP0.IsPositive := hPos0
have hDpos : ((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)+T).IsPositive := by
refine ⟨((IsSelfAdjoint.one (Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)).add hTs).isSymmetric,?_⟩
intro u
change 0 ≤ inner ℝ (u+T u) u
rw [inner_add_left,real_inner_self_eq_norm_sq]
have hn : ‖T u‖≤‖u‖ := (hAll u).1
have hi := (abs_le.mp (abs_real_inner_le_norm (T u) u)).1
nlinarith only [hn,hi,norm_nonneg u]
have hCommSquare : Commute (Γ*Γ) ((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)+T) := by
rw [hΓSq]
show (1-T*T)*(1+T)=(1+T)*(1-T*T)
noncomm_ring
have hCommRootPlus := AutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareCommute.positive_square_commutation
ν Γ (1+T) hΓ hDpos hCommSquare
have hCommRoot : Commute Γ T := by
have h := hCommRootPlus.eq
simp only [mul_add,add_mul,mul_one,one_mul] at h
exact add_left_cancel h
have hCommP : Commute ΓP A := by
change ΓP*A=A*ΓP
change (e.conjStarAlgEquiv Γ)*A=A*(e.conjStarAlgEquiv Γ)
rw [hAeqLocal,← map_mul,← map_mul,hCommRoot.eq]
have hAq : A qP=qP := by
rw [hAeqLocal]
change e (T (e.symm (e q)))=e q
rw [e.symm_apply_apply,hTq]
have hAPreserves (u : HP0) : A (u : HP) ∈ HP0 := by
change inner ℝ qP (A (u : HP))=0
calc
inner ℝ qP (A (u : HP))=inner ℝ (A qP) (u : HP) :=
(hAsLocal.isSymmetric qP (u : HP)).symm
_ = inner ℝ qP (u : HP) := by rw [hAq]
_ = 0 := u.property
let A0 : HP0 →L[ℝ] HP0 := (A.comp HP0.subtypeL).codRestrict HP0 hAPreserves
have hA0 (u : HP0) : (A0 u : HP)=A (u : HP) := rfl
have hA0self : IsSelfAdjoint A0 := by
apply ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric.mpr
intro u v
exact hAsLocal.isSymmetric (u : HP) (v : HP)
have hComm0 : Commute A0 ΓP0 := by
apply ContinuousLinearMap.ext
intro u
apply Subtype.ext
change (A0 (ΓP0 u) : HP)=(ΓP0 (A0 u) : HP)
rw [hA0,hΓP0,hΓP0,hA0]
exact congrArg (fun D : HP →L[ℝ] HP => D (u : HP)) hCommP.eq.symm
have hSquare0 : A0*A0+ΓP0*ΓP0=(1 : HP0 →L[ℝ] HP0) := by
apply ContinuousLinearMap.ext
intro u
apply Subtype.ext
change (A0 (A0 u) : HP)+(ΓP0 (ΓP0 u) : HP)=(u : HP)
rw [hA0,hA0,hΓP0,hΓP0]
have h : ΓP (ΓP (u : HP))=(u : HP)-A (A (u : HP)) :=
congrArg (fun D : HP →L[ℝ] HP => D (u : HP)) hΓPSq
rw [h]
abel
have hStarInv : ΓP0*star Inv=(1 : HP0 →L[ℝ] HP0) := by
have h := congrArg (fun D : HP0 →L[ℝ] HP0 => star D) hLeftLocal
simpa only [star_mul,hPosLocal.isSelfAdjoint.star_eq,star_one] using h
have hInvSelf : IsSelfAdjoint Inv := by
change star Inv=Inv
calc
star Inv=(Inv*ΓP0)*star Inv := by rw [hLeft,one_mul]
_ = Inv*(ΓP0*star Inv) := mul_assoc _ _ _
_ = Inv := by rw [hStarInv,mul_one]
have hCommInv : Commute A0 Inv := by
change A0*Inv=Inv*A0
calc
A0*Inv=(Inv*ΓP0)*(A0*Inv) := by rw [hLeft,one_mul]
_ = Inv*((ΓP0*A0)*Inv) := by noncomm_ring
_ = Inv*((A0*ΓP0)*Inv) := by rw [hComm0.eq.symm]
_ = Inv*A0 := by simp only [mul_assoc,hRight,mul_one]
refine ⟨hμ, ?_⟩
refine ⟨hJ, ?_⟩
refine ⟨hν, ?_⟩
refine ⟨hRange, ?_⟩
refine ⟨hPf, ?_⟩
refine ⟨S, ?_⟩
refine ⟨hS, ?_⟩
refine ⟨hSd, ?_⟩
refine ⟨hSc, ?_⟩
refine ⟨hSf, ?_⟩
refine ⟨hSs, ?_⟩
refine ⟨e, ?_⟩
refine ⟨he, ?_⟩
refine ⟨U, ?_⟩
refine ⟨hU, ?_⟩
refine ⟨hUi, ?_⟩
refine ⟨hUs, ?_⟩
refine ⟨T, ?_⟩
refine ⟨hTs, ?_⟩
refine ⟨hAll, ?_⟩
refine ⟨hAeq, ?_⟩
refine ⟨hAs, ?_⟩
refine ⟨hAn, ?_⟩
refine ⟨hPB, ?_⟩
refine ⟨Γ, ?_⟩
refine ⟨hΓ, ?_⟩
refine ⟨hΓSq, ?_⟩
refine ⟨hCommRoot, ?_⟩
refine ⟨hΓP, ?_⟩
refine ⟨hΓPSq, ?_⟩
refine ⟨hCommP, ?_⟩
refine ⟨hGram, ?_⟩
refine ⟨q, ?_⟩
refine ⟨hqa, ?_⟩
refine ⟨hTq, ?_⟩
refine ⟨hq, ?_⟩
refine ⟨hCenter, ?_⟩
refine ⟨hΓPq, ?_⟩
refine ⟨hγ, ?_⟩
refine ⟨ΓP0, ?_⟩
refine ⟨hΓP0, ?_⟩
refine ⟨hPos0, ?_⟩
refine ⟨hOrder0, ?_⟩
refine ⟨hUnit, ?_⟩
refine ⟨Inv, ?_⟩
refine ⟨hLeft, ?_⟩
refine ⟨hRight, ?_⟩
refine ⟨hNormInv, ?_⟩
refine ⟨hInvSelf,A0,hA0,hA0self,hComm0,hSquare0,hCommInv,?_⟩
refine ⟨B0, ?_⟩
refine ⟨hB0, ?_⟩
refine ⟨V0, ?_⟩
refine ⟨hVdef, ?_⟩
refine ⟨hFactor, ?_⟩
refine ⟨hVadj, ?_⟩
refine ⟨hVnorm, ?_⟩
refine ⟨R, ?_⟩
refine ⟨hR, ?_⟩
refine ⟨hAmbient, ?_⟩
exact hGlobal
end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualRootCommutation
#print axioms AutoSamplingTheory.ExampleCases.ProximalBPS.ActualRootCommutation.actual_same_root_inverse_commutationScope and omitted-condition boundaries
- Same-root and actual centered inverse commutation plus B23 coefficient square identity only. Sharp B23 norm estimate/B21 rotation/full energy/H1/dynamics/errors/cost/composition not yet proved. All original finite Hilbert/Borel/C2/both Hessians/positive capped eta callers preserved. D=I+T positivity and all commutations are internally proved, never extra public paper premises.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.ProximalBPS.AmbientAdjointCorrector.actual_ambient_adjoint_centered_decompositionAutoSamplingTheory.TechnicalLemmas.Measure.L2RealComplexOperator.exists_positive_complex_liftAutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareCommute.positive_square_commutation
Mathlib API called (external library)
- Commute.cfcₙ_nnreal
- CFC.sqrt_unique
- ContinuousLinearMap.ext
- ContinuousLinearMap.codRestrict
- ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric
- IsSelfAdjoint.commute_iff
- LinearIsometryEquiv.conjStarAlgEquiv
- abs_real_inner_le_norm
Mathematical sources
- PBPS2609.06905v1 Appendix B3: B20 corrector definition, Lemma B.3 sharp B23 estimate and B21 rotation. Same spectral square root, actual centered restriction and inverse commutation; ASTIS positive-square commutation background adapter. — Same-root and actual centered inverse commutation plus B23 coefficient square identity only. Sharp B23 norm estimate/B21 rotation/full energy/H1/dynamics/errors/cost/composition not yet proved. All original finite Hilbert/Borel/C2/both Hessians/positive capped eta callers preserved. D=I+T positivity and all commutations are internally proved, never extra public paper premises.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.