Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

SharpCorrectorEnergy: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. Actual PBPS sharp first-corrector bound and Lemma B.3 consumer
Samplinglib mathematical lesson

Actual PBPS sharp first-corrector bound and Lemma B.3 consumer

AutoSamplingTheory.ExampleCases.ProximalBPS.SharpCorrectorEnergy.actual_sharp_corrector_bound · 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 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 SAME coefficient K=A_0 Inv is selfadjoint and I+K²=Inv². Define C(u,v)=(‖u‖²−‖v‖²)/2−⟨Ku,v⟩ on the SAME centered Hilbert space H_P^0. For every u,v in H_P^0, |C(u,v)|≤(‖u‖²+‖v‖²)/(2γ). For every actual f∈L²(J;ℝ) with ∫f dJ=0, the SAME f_P,f_perp,f_V and all preceding identities persist, and ‖f_P‖²+‖f_V‖²≤‖f‖² and |C(f_P,f_V)|≤‖f‖²/(2γ). All coefficient identities, domains and bounds are conclusions from the original potential and step inputs. The genuine original-input Test then proves, for every real 0<omegaWeight≤γ and L=‖f‖²+omegaWeight C(f_P,f_V), that ‖f‖²/2≤L≤3‖f‖²/2 and |L−‖f‖²|≤omegaWeight ‖f‖²/(2γ)≤‖f‖²/2. These are the first-corrector bound and Lemma B.3 energy equivalence. B21 rotation, weak H1/B2, B4 dynamics, mixing, nonexplosion, implementation error, expected costs and actual-input composition remain separate. One private literal Prop per actual module stores the full sealed statement and adds no proof provider or premise.

\[|C(u,v)|\le\frac{\|u\|^2+\|v\|^2}{2\gamma},\quad |C(f_P,f_V)|\le\frac{\|f\|^2}{2\gamma},\quad\tfrac12\|f\|^2\le L\le\tfrac32\|f\|^2.\]
Lean statement · actual_sharp_corrector_bound

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 SAME coefficient K=A_0 Inv is selfadjoint and I+K²=Inv². Define C(u,v)=(‖u‖²−‖v‖²)/2−⟨Ku,v⟩ on the SAME centered Hilbert space H_P^0. For every u,v in H_P^0, |C(u,v)|≤(‖u‖²+‖v‖²)/(2γ). For every actual f∈L²(J;ℝ) with ∫f dJ=0, the SAME f_P,f_perp,f_V and all preceding identities persist, and ‖f_P‖²+‖f_V‖²≤‖f‖² and |C(f_P,f_V)|≤‖f‖²/(2γ). All coefficient identities, domains and bounds are conclusions from the original potential and step inputs. The genuine original-input Test then proves, for every real 0<omegaWeight≤γ and L=‖f‖²+omegaWeight C(f_P,f_V), that ‖f‖²/2≤L≤3‖f‖²/2 and |L−‖f‖²|≤omegaWeight ‖f‖²/(2γ)≤‖f‖²/2. These are the first-corrector bound and Lemma B.3 energy equivalence. B21 rotation, weak H1/B2, B4 dynamics, mixing, nonexplosion, implementation error, expected costs and actual-input composition remain separate. One private literal Prop per actual module stores the full sealed statement and adds no proof provider or premise.

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_sharp_corrector_bound
    {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_sharp_corrector_bound_statement (E := E) (V := V) (α := α) (β := β) (η := η) hα hαβ hV hH hη hβη

Exact module and namespace context

Proof roadmap

  1. 1Retain the exact actual input and witnesses

    Call the production parent at the unchanged potential and step assumptions; fix the same laws, kernel, centered spaces, inverse and global centered-observable geometry.

  2. 2Produce the coefficient identity inside production

    Commuting selfadjoint A0 and Inv give selfadjoint K. Multiply A0²+Γ0²=I by the SAME Inv² and use the right inverse identity twice.

  3. 3Apply the sharp Hilbert estimate on the actual centered space

    Take D=Inv and c=1/γ. Positivity of γ and the existing norm bound discharge all leaf hypotheses without a new public premise.

  4. 4Use the actual norm budget

    Pythagoras and the adjoint contraction give the sum-of-squares budget. Apply the pair bound to the SAME actual fP,fV. An explicitly typed local have proves exactly this final conclusion before the outer witnesses are reconstructed.

  5. 5Preserve every preceding actual conclusion

    Reassemble the same witnesses with the new internally proved coefficient, pair bound and exact local actual-input conclusion. The literal statement retains each original probability and domain conclusion.

  6. 6Consume the sharp bound in Lemma B.3

    The Test calls production at the original inputs. For every 0<omegaWeight≤γ, bound the perturbation by half of the squared norm and use both sides of the absolute-value inequality. Its local have proves the exact final Test tail, then retains all original witnesses.

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 input and witnesses

Call the production parent at the unchanged potential and step assumptions; fix the same laws, kernel, centered spaces, inverse and global centered-observable geometry.

\[H_P^0=\ker\langle q_P,\cdot\rangle,\quad\Gamma_0^{-1}=\mathrm{Inv},\quad f_V=V_0^*Rf.\]
Corresponding Lean step
  classical
  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.ActualRootCommutation.actual_same_root_inverse_commutation
    (E:=E) (V:=V) (α:=α) (β:=β) (η:=η) hα hαβ hV hH hη hβη
  have parentSlice0 := hBase
  have hμ := parentSlice0.1
  have parentSlice1 := parentSlice0.2
  have hJ := parentSlice1.1
  have parentSlice2 := parentSlice1.2
  have hν := parentSlice2.1
  have parentSlice3 := parentSlice2.2
  have hRange := parentSlice3.1
  have parentSlice4 := parentSlice3.2
  have hPf := parentSlice4.1
  have parentSlice5 := parentSlice4.2
  obtain ⟨S, parentSlice6⟩ := parentSlice5
  have hS := parentSlice6.1
  have parentSlice7 := parentSlice6.2
  have hSd := parentSlice7.1
  have parentSlice8 := parentSlice7.2
  have hSc := parentSlice8.1
  have parentSlice9 := parentSlice8.2
  have hSf := parentSlice9.1
  have parentSlice10 := parentSlice9.2
  have hSs := parentSlice10.1
  have parentSlice11 := parentSlice10.2
  obtain ⟨e, parentSlice12⟩ := parentSlice11
  have he := parentSlice12.1
  have parentSlice13 := parentSlice12.2
  obtain ⟨U, parentSlice14⟩ := parentSlice13
  have hU := parentSlice14.1
  have parentSlice15 := parentSlice14.2
  have hUi := parentSlice15.1
  have parentSlice16 := parentSlice15.2
  have hUs := parentSlice16.1
  have parentSlice17 := parentSlice16.2
  obtain ⟨T, parentSlice18⟩ := parentSlice17
  have hTs := parentSlice18.1
  have parentSlice19 := parentSlice18.2
  have hAll := parentSlice19.1
  have parentSlice20 := parentSlice19.2
  have hAeq := parentSlice20.1
  have parentSlice21 := parentSlice20.2
  have hAs := parentSlice21.1
  have parentSlice22 := parentSlice21.2
  have hAn := parentSlice22.1
  have parentSlice23 := parentSlice22.2
  have hPB := parentSlice23.1
  have parentSlice24 := parentSlice23.2
  obtain ⟨Γ, parentSlice25⟩ := parentSlice24
  have hΓ := parentSlice25.1
  have parentSlice26 := parentSlice25.2
  have hΓSq := parentSlice26.1
  have parentSlice27 := parentSlice26.2
  have hCommRoot := parentSlice27.1
  have parentSlice28 := parentSlice27.2
  have hΓP := parentSlice28.1
  have parentSlice29 := parentSlice28.2
  have hΓPSq := parentSlice29.1
  have parentSlice30 := parentSlice29.2
  have hCommP := parentSlice30.1
  have parentSlice31 := parentSlice30.2
  have hGram := parentSlice31.1
  have parentSlice32 := parentSlice31.2
  obtain ⟨q, parentSlice33⟩ := parentSlice32
  have hqa := parentSlice33.1
  have parentSlice34 := parentSlice33.2
  have hTq := parentSlice34.1
  have parentSlice35 := parentSlice34.2
  have hq := parentSlice35.1
  have parentSlice36 := parentSlice35.2
  have hCenter := parentSlice36.1
  have parentSlice37 := parentSlice36.2
  have hΓPq := parentSlice37.1
  have parentSlice38 := parentSlice37.2
  have hγ := parentSlice38.1
  have parentSlice39 := parentSlice38.2
  obtain ⟨ΓP0, parentSlice40⟩ := parentSlice39
  have hΓP0 := parentSlice40.1
  have parentSlice41 := parentSlice40.2
  have hPos0 := parentSlice41.1
  have parentSlice42 := parentSlice41.2
  have hOrder0 := parentSlice42.1
  have parentSlice43 := parentSlice42.2
  have hUnit := parentSlice43.1
  have parentSlice44 := parentSlice43.2
  obtain ⟨Inv, parentSlice45⟩ := parentSlice44
  have hLeft := parentSlice45.1
  have parentSlice46 := parentSlice45.2
  have hRight := parentSlice46.1
  have parentSlice47 := parentSlice46.2
  have hNormInv := parentSlice47.1
  have parentSlice48 := parentSlice47.2
  have hInvSelf := parentSlice48.1
  have parentSlice49 := parentSlice48.2
  obtain ⟨A0, parentSlice50⟩ := parentSlice49
  have hA0 := parentSlice50.1
  have parentSlice51 := parentSlice50.2
  have hA0self := parentSlice51.1
  have parentSlice52 := parentSlice51.2
  have hComm0 := parentSlice52.1
  have parentSlice53 := parentSlice52.2
  have hSquare0 := parentSlice53.1
  have parentSlice54 := parentSlice53.2
  have hCommInv := parentSlice54.1
  have parentSlice55 := parentSlice54.2
  obtain ⟨B0, parentSlice56⟩ := parentSlice55
  have hB0 := parentSlice56.1
  have parentSlice57 := parentSlice56.2
  obtain ⟨V0, parentSlice58⟩ := parentSlice57
  have hVdef := parentSlice58.1
  have parentSlice59 := parentSlice58.2
  have hFactor := parentSlice59.1
  have parentSlice60 := parentSlice59.2
  have hVadj := parentSlice60.1
  have parentSlice61 := parentSlice60.2
  have hVnorm := parentSlice61.1
  have parentSlice62 := parentSlice61.2
  obtain ⟨R, parentSlice63⟩ := parentSlice62
  have hR := parentSlice63.1
  have parentSlice64 := parentSlice63.2
  have hAmbient := parentSlice64.1
  have parentSlice65 := parentSlice64.2
  have hGlobal := parentSlice65
  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 A0
  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 the coefficient identity inside production

Commuting selfadjoint A0 and Inv give selfadjoint K. Multiply A0²+Γ0²=I by the SAME Inv² and use the right inverse identity twice.

\[K=A_0\mathrm{Inv}=K^*,\quad I+K^2=(\Gamma_0^2+A_0^2)\mathrm{Inv}^2=\mathrm{Inv}^2.\]
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.

3. Apply the sharp Hilbert estimate on the actual centered space

Take D=Inv and c=1/γ. Positivity of γ and the existing norm bound discharge all leaf hypotheses without a new public premise.

\[\|\mathrm{Inv}\|\le1/\gamma\quad\Longrightarrow\quad |C(u,v)|\le\frac{\|u\|^2+\|v\|^2}{2\gamma}.\]
Corresponding Lean step
  let γ : ℝ := 2*Real.sqrt ((α : ℝ)*η)/(1+(α : ℝ)*η)
  change 0 < γ at hγ
  change ‖Inv‖ ≤ 1/γ at hNormInv
  let C : HP0 → HP0 → ℝ := fun u v =>
    (1/2 : ℝ)*(‖u‖^2-‖v‖^2)-inner ℝ ((A0*Inv) u) v
  have hPair (u v : HP0) : |C u v| ≤ (‖u‖^2+‖v‖^2)/(2*γ) := by
    have h := AutoSamplingTheory.TechnicalLemmas.Analysis.HilbertCorrectorBound.quadratic_corrector_bound_of_square_identity
      (A0*Inv) Inv hKself hInvSelf hCoefficient (1/γ) (by positivity) hNormInv u v
    change |C u v| ≤ ((1/γ)/2)*(‖u‖^2+‖v‖^2) at h
    calc
      |C u v| ≤ ((1/γ)/2)*(‖u‖^2+‖v‖^2) := h
      _ = (‖u‖^2+‖v‖^2)/(2*γ) := by
        field_simp

Literal compiled BODY span; exact preceding locals remain in scope.

4. Use the actual norm budget

Pythagoras and the adjoint contraction give the sum-of-squares budget. Apply the pair bound to the SAME actual fP,fV. An explicitly typed local have proves exactly this final conclusion before the outer witnesses are reconstructed.

\[\|f_P\|^2+\|f_V\|^2\le\|f\|^2\quad\Longrightarrow\quad |C(f_P,f_V)|\le\frac{\|f\|^2}{2\gamma}.\]
Corresponding Lean step
  have hFinal : ∀ 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‖ ∧
        ‖fP‖^2+‖fV‖^2≤‖f‖^2 ∧ |C fP fV|≤‖f‖^2/(2*γ) := by
    intro f hf
    obtain ⟨fP,hGlobalFields⟩ := hGlobal f hf
    have hfP := hGlobalFields.1
    have hBf := hGlobalFields.2.1
    have hΓf := hGlobalFields.2.2.1
    have hPyth := hGlobalFields.2.2.2.1
    have hNormV := hGlobalFields.2.2.2.2
    let fperp : Hperp := R f
    let fV : HP0 := V0.adjoint fperp
    have hBudget : ‖fP‖^2+‖fV‖^2 ≤ ‖f‖^2 := by
      have hs := (sq_le_sq₀ (norm_nonneg fV) (norm_nonneg fperp)).2 hNormV
      nlinarith only [hPyth, hs]
    refine ⟨fP,hfP,hBf,hΓf,hPyth,hNormV,hBudget,?_⟩
    exact (hPair fP fV).trans (div_le_div_of_nonneg_right hBudget (by positivity))

Literal compiled BODY span; exact preceding locals remain in scope.

5. Preserve every preceding actual conclusion

Reassemble the same witnesses with the new internally proved coefficient, pair bound and exact local actual-input conclusion. The literal statement retains each original probability and domain conclusion.

\[\text{same }\mu,J,\nu,S,e,U,T,\Gamma,\Gamma_0,\mathrm{Inv},A_0,B_0,V_0,R.\]
Corresponding Lean step
  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,hKself,hCoefficient,hPair,?_⟩
  refine ⟨B0, ?_⟩
  refine ⟨hB0, ?_⟩
  refine ⟨V0, ?_⟩
  refine ⟨hVdef, ?_⟩
  refine ⟨hFactor, ?_⟩
  refine ⟨hVadj, ?_⟩
  refine ⟨hVnorm, ?_⟩
  refine ⟨R, ?_⟩
  refine ⟨hR, ?_⟩
  refine ⟨hAmbient, ?_⟩
  exact hFinal

Literal compiled BODY span; exact preceding locals remain in scope.

6. Consume the sharp bound in Lemma B.3

The Test calls production at the original inputs. For every 0<omegaWeight≤γ, bound the perturbation by half of the squared norm and use both sides of the absolute-value inequality. Its local have proves the exact final Test tail, then retains all original witnesses.

\[|L-\|f\|^2|\le\frac{\omega}{2\gamma}\|f\|^2\le\frac12\|f\|^2,\quad\frac12\|f\|^2\le L\le\frac32\|f\|^2.\]
Corresponding Lean step
  have hFinal : ∀ 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‖ ∧
        ‖fP‖^2+‖fV‖^2≤‖f‖^2 ∧
        |C fP fV|≤‖f‖^2/(2*γ) ∧
        (∀ omegaWeight : ℝ, 0<omegaWeight → omegaWeight≤γ →
          let L : ℝ := ‖f‖^2+omegaWeight*C fP fV
          (1/2 : ℝ)*‖f‖^2≤L ∧ L≤(3/2 : ℝ)*‖f‖^2 ∧
          |L-‖f‖^2|≤(omegaWeight/(2*γ))*‖f‖^2 ∧
          (omegaWeight/(2*γ))*‖f‖^2≤(1/2 : ℝ)*‖f‖^2) := by
    intro f hf
    obtain ⟨fP,hGlobalFields⟩ := hGlobal f hf
    have hfP := hGlobalFields.1
    have hBf := hGlobalFields.2.1
    have hΓf := hGlobalFields.2.2.1
    have hPyth := hGlobalFields.2.2.2.1
    have hNormV := hGlobalFields.2.2.2.2.1
    have hBudget := hGlobalFields.2.2.2.2.2.1
    have hCorrector := hGlobalFields.2.2.2.2.2.2
    let fperp : Hperp := R f
    let fV : HP0 := V0.adjoint fperp
    refine ⟨fP,hfP,hBf,hΓf,hPyth,hNormV,hBudget,hCorrector,?_⟩
    intro omegaWeight hWeight hWeightGamma
    let L : ℝ := ‖f‖^2+omegaWeight*C fP fV
    have hPerturbation : |L-‖f‖^2| ≤ (omegaWeight/(2*γ))*‖f‖^2 := by
      have hId : L-‖f‖^2=omegaWeight*C fP fV := by dsimp only [L]; ring
      rw [hId,abs_mul,abs_of_pos hWeight]
      calc
        omegaWeight*|C fP fV| ≤ omegaWeight*(‖f‖^2/(2*γ)) :=
          mul_le_mul_of_nonneg_left hCorrector hWeight.le
        _ = (omegaWeight/(2*γ))*‖f‖^2 := by ring
    have hWeightBound : omegaWeight/(2*γ) ≤ (1/2 : ℝ) := by
      apply (div_le_iff₀ (by positivity : 0 < 2*γ)).2
      nlinarith only [hWeightGamma]
    have hHalf : (omegaWeight/(2*γ))*‖f‖^2 ≤ (1/2 : ℝ)*‖f‖^2 :=
      mul_le_mul_of_nonneg_right hWeightBound (sq_nonneg _)
    have hBoth := abs_le.mp (hPerturbation.trans hHalf)
    refine ⟨?_,?_,hPerturbation,hHalf⟩ <;> linarith only [hBoth.1,hBoth.2]
  unfold genuine_actual_modified_energy_equivalence_statement
  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,hKself,hCoefficient,hPair,?_⟩
  refine ⟨B0, ?_⟩
  refine ⟨hB0, ?_⟩
  refine ⟨V0, ?_⟩
  refine ⟨hVdef, ?_⟩
  refine ⟨hFactor, ?_⟩
  refine ⟨hVadj, ?_⟩
  refine ⟨hVnorm, ?_⟩
  refine ⟨R, ?_⟩
  refine ⟨hR, ?_⟩
  refine ⟨hAmbient, ?_⟩
  exact hFinal

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_sharp_corrector_bound

Retain the exact actual input and witnesses; Produce the coefficient identity inside production; Apply the sharp Hilbert estimate on the actual centered space; Use the actual norm budget; Preserve every preceding actual conclusion; Consume the sharp bound in Lemma B.3

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_sharp_corrector_bound
    {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_sharp_corrector_bound_statement (E := E) (V := V) (α := α) (β := β) (η := η) hα hαβ hV hH hη hβη := by
  classical
  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.ActualRootCommutation.actual_same_root_inverse_commutation
    (E:=E) (V:=V) (α:=α) (β:=β) (η:=η) hα hαβ hV hH hη hβη
  have parentSlice0 := hBase
  have hμ := parentSlice0.1
  have parentSlice1 := parentSlice0.2
  have hJ := parentSlice1.1
  have parentSlice2 := parentSlice1.2
  have hν := parentSlice2.1
  have parentSlice3 := parentSlice2.2
  have hRange := parentSlice3.1
  have parentSlice4 := parentSlice3.2
  have hPf := parentSlice4.1
  have parentSlice5 := parentSlice4.2
  obtain ⟨S, parentSlice6⟩ := parentSlice5
  have hS := parentSlice6.1
  have parentSlice7 := parentSlice6.2
  have hSd := parentSlice7.1
  have parentSlice8 := parentSlice7.2
  have hSc := parentSlice8.1
  have parentSlice9 := parentSlice8.2
  have hSf := parentSlice9.1
  have parentSlice10 := parentSlice9.2
  have hSs := parentSlice10.1
  have parentSlice11 := parentSlice10.2
  obtain ⟨e, parentSlice12⟩ := parentSlice11
  have he := parentSlice12.1
  have parentSlice13 := parentSlice12.2
  obtain ⟨U, parentSlice14⟩ := parentSlice13
  have hU := parentSlice14.1
  have parentSlice15 := parentSlice14.2
  have hUi := parentSlice15.1
  have parentSlice16 := parentSlice15.2
  have hUs := parentSlice16.1
  have parentSlice17 := parentSlice16.2
  obtain ⟨T, parentSlice18⟩ := parentSlice17
  have hTs := parentSlice18.1
  have parentSlice19 := parentSlice18.2
  have hAll := parentSlice19.1
  have parentSlice20 := parentSlice19.2
  have hAeq := parentSlice20.1
  have parentSlice21 := parentSlice20.2
  have hAs := parentSlice21.1
  have parentSlice22 := parentSlice21.2
  have hAn := parentSlice22.1
  have parentSlice23 := parentSlice22.2
  have hPB := parentSlice23.1
  have parentSlice24 := parentSlice23.2
  obtain ⟨Γ, parentSlice25⟩ := parentSlice24
  have hΓ := parentSlice25.1
  have parentSlice26 := parentSlice25.2
  have hΓSq := parentSlice26.1
  have parentSlice27 := parentSlice26.2
  have hCommRoot := parentSlice27.1
  have parentSlice28 := parentSlice27.2
  have hΓP := parentSlice28.1
  have parentSlice29 := parentSlice28.2
  have hΓPSq := parentSlice29.1
  have parentSlice30 := parentSlice29.2
  have hCommP := parentSlice30.1
  have parentSlice31 := parentSlice30.2
  have hGram := parentSlice31.1
  have parentSlice32 := parentSlice31.2
  obtain ⟨q, parentSlice33⟩ := parentSlice32
  have hqa := parentSlice33.1
  have parentSlice34 := parentSlice33.2
  have hTq := parentSlice34.1
  have parentSlice35 := parentSlice34.2
  have hq := parentSlice35.1
  have parentSlice36 := parentSlice35.2
  have hCenter := parentSlice36.1
  have parentSlice37 := parentSlice36.2
  have hΓPq := parentSlice37.1
  have parentSlice38 := parentSlice37.2
  have hγ := parentSlice38.1
  have parentSlice39 := parentSlice38.2
  obtain ⟨ΓP0, parentSlice40⟩ := parentSlice39
  have hΓP0 := parentSlice40.1
  have parentSlice41 := parentSlice40.2
  have hPos0 := parentSlice41.1
  have parentSlice42 := parentSlice41.2
  have hOrder0 := parentSlice42.1
  have parentSlice43 := parentSlice42.2
  have hUnit := parentSlice43.1
  have parentSlice44 := parentSlice43.2
  obtain ⟨Inv, parentSlice45⟩ := parentSlice44
  have hLeft := parentSlice45.1
  have parentSlice46 := parentSlice45.2
  have hRight := parentSlice46.1
  have parentSlice47 := parentSlice46.2
  have hNormInv := parentSlice47.1
  have parentSlice48 := parentSlice47.2
  have hInvSelf := parentSlice48.1
  have parentSlice49 := parentSlice48.2
  obtain ⟨A0, parentSlice50⟩ := parentSlice49
  have hA0 := parentSlice50.1
  have parentSlice51 := parentSlice50.2
  have hA0self := parentSlice51.1
  have parentSlice52 := parentSlice51.2
  have hComm0 := parentSlice52.1
  have parentSlice53 := parentSlice52.2
  have hSquare0 := parentSlice53.1
  have parentSlice54 := parentSlice53.2
  have hCommInv := parentSlice54.1
  have parentSlice55 := parentSlice54.2
  obtain ⟨B0, parentSlice56⟩ := parentSlice55
  have hB0 := parentSlice56.1
  have parentSlice57 := parentSlice56.2
  obtain ⟨V0, parentSlice58⟩ := parentSlice57
  have hVdef := parentSlice58.1
  have parentSlice59 := parentSlice58.2
  have hFactor := parentSlice59.1
  have parentSlice60 := parentSlice59.2
  have hVadj := parentSlice60.1
  have parentSlice61 := parentSlice60.2
  have hVnorm := parentSlice61.1
  have parentSlice62 := parentSlice61.2
  obtain ⟨R, parentSlice63⟩ := parentSlice62
  have hR := parentSlice63.1
  have parentSlice64 := parentSlice63.2
  have hAmbient := parentSlice64.1
  have parentSlice65 := parentSlice64.2
  have hGlobal := parentSlice65
  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 A0
  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 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]
  let γ : ℝ := 2*Real.sqrt ((α : ℝ)*η)/(1+(α : ℝ)*η)
  change 0 < γ at hγ
  change ‖Inv‖ ≤ 1/γ at hNormInv
  let C : HP0 → HP0 → ℝ := fun u v =>
    (1/2 : ℝ)*(‖u‖^2-‖v‖^2)-inner ℝ ((A0*Inv) u) v
  have hPair (u v : HP0) : |C u v| ≤ (‖u‖^2+‖v‖^2)/(2*γ) := by
    have h := AutoSamplingTheory.TechnicalLemmas.Analysis.HilbertCorrectorBound.quadratic_corrector_bound_of_square_identity
      (A0*Inv) Inv hKself hInvSelf hCoefficient (1/γ) (by positivity) hNormInv u v
    change |C u v| ≤ ((1/γ)/2)*(‖u‖^2+‖v‖^2) at h
    calc
      |C u v| ≤ ((1/γ)/2)*(‖u‖^2+‖v‖^2) := h
      _ = (‖u‖^2+‖v‖^2)/(2*γ) := by
        field_simp
  have hFinal : ∀ 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‖ ∧
        ‖fP‖^2+‖fV‖^2≤‖f‖^2 ∧ |C fP fV|≤‖f‖^2/(2*γ) := by
    intro f hf
    obtain ⟨fP,hGlobalFields⟩ := hGlobal f hf
    have hfP := hGlobalFields.1
    have hBf := hGlobalFields.2.1
    have hΓf := hGlobalFields.2.2.1
    have hPyth := hGlobalFields.2.2.2.1
    have hNormV := hGlobalFields.2.2.2.2
    let fperp : Hperp := R f
    let fV : HP0 := V0.adjoint fperp
    have hBudget : ‖fP‖^2+‖fV‖^2 ≤ ‖f‖^2 := by
      have hs := (sq_le_sq₀ (norm_nonneg fV) (norm_nonneg fperp)).2 hNormV
      nlinarith only [hPyth, hs]
    refine ⟨fP,hfP,hBf,hΓf,hPyth,hNormV,hBudget,?_⟩
    exact (hPair fP fV).trans (div_le_div_of_nonneg_right hBudget (by positivity))
  unfold actual_sharp_corrector_bound_statement
  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,hKself,hCoefficient,hPair,?_⟩
  refine ⟨B0, ?_⟩
  refine ⟨hB0, ?_⟩
  refine ⟨V0, ?_⟩
  refine ⟨hVdef, ?_⟩
  refine ⟨hFactor, ?_⟩
  refine ⟨hVadj, ?_⟩
  refine ⟨hVnorm, ?_⟩
  refine ⟨R, ?_⟩
  refine ⟨hR, ?_⟩
  refine ⟨hAmbient, ?_⟩
  exact hFinal


end
end AutoSamplingTheory.ExampleCases.ProximalBPS.SharpCorrectorEnergy

#print axioms AutoSamplingTheory.ExampleCases.ProximalBPS.SharpCorrectorEnergy.actual_sharp_corrector_bound

Exact module and namespace context

Scope and omitted-condition boundaries
  • Sharp first-corrector energy/LemmaB.3 only. B21 rotation,B2/weakH1,B4 dynamics,hypocoercivity/main,invariance/nonexplosion,errors,caps,expectedquery costs and actual-input composition remain independent. All original finite real Hilbert/Borel/C2/two Hessians/positive capped eta callers retained; no new provider/coercivity/strict endpoint/Nontrivial premise. Rank0 and alphaeta1 legal.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • IsSelfAdjoint.commute_iff
  • Commute.eq
  • sq_le_sq₀
  • div_le_div_of_nonneg_right
  • abs_le
  • div_le_iff₀

Mathematical sources

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.