AutoSamplingTheory.TechnicalLemmas.Analysis.HilbertCorrectorPerturbation

Samplinglib mathematical lesson

Hilbert corrector perturbation identity

AutoSamplingTheory.TechnicalLemmas.Analysis.HilbertCorrectorPerturbation.quadratic_corrector_perturbation · theorem · Teaching coverage

Read this first

Mathematical statement

Let H be a complete real Hilbert space, allowing the zero space. Let A,G,Inv:H→H be bounded real-linear endomorphisms. Assume A,G,Inv are selfadjoint, A commutes with Inv, Inv G=G Inv=I, and A²+G²=I. Every one of these structural conditions is an explicit hypothesis of this auxiliary algebra theorem. For arbitrary u,v,r∈H define C(a,b)=(||a||²−||b||²)/2−⟨A(Inv a),b⟩. Then C(u+Gr,v−Ar)−C(u,v)=⟨u,Inv r⟩+||r||²/2. The half, plus sign, operator order and same three operators are exact. This is an ASTIS Hilbert-space auxiliary generalization of the algebra in Chen–Chewi–Lu–Zhang's PBPS B20 and Lemma B4 expansion Ex28–Ex34, rather than a claim that the paper states a theorem for arbitrary Hilbert operators. No positivity, finite dimension, spectral gap, surjectivity or probability hypothesis is needed by this algebra identity. The actual PBPS consumer constructs all seven operator facts internally on its same centered space. Arbitrary r is not yet the paper's r_rho; the actual H/K/B27 adapter and B4/B28 decay proof remain open.

\[C(u,v)=\frac{\|u\|^2-\|v\|^2}{2}-\langle A\operatorname{Inv}u,v\rangle,\quad C(u+Gr,v-Ar)-C(u,v)=\langle u,\operatorname{Inv}r\rangle+\frac{\|r\|^2}{2}.\]

Lean statement · quadratic_corrector_perturbation

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 quadratic_corrector_perturbation
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
    [CompleteSpace H]
    (A G Inv : H →L[ℝ] H)
    (hA : IsSelfAdjoint A) (hG : IsSelfAdjoint G)
    (hInv : IsSelfAdjoint Inv) (hAInv : Commute A Inv)
    (hInvG : Inv * G = 1) (hGInv : G * Inv = 1)
    (hSquares : A * A + G * G = 1)
    (u v r : H) :
    let C : H → H → ℝ := fun u v =>
      (‖u‖^2 - ‖v‖^2)/2 - inner ℝ (A (Inv u)) v
    C (u + G r) (v - A r) - C u v =
      inner ℝ u (Inv r) + ‖r‖^2/2

Exact module and namespace context

Proof roadmap

1Expose the exact functional and typed selfadjoint identities
Unfold only C. State each selfadjointness consequence as an equality of real inner products on the same H, avoiding coercion-sensitive rewrites. No mathematical assumption is added.
2Evaluate the inverse and square-sum operator equalities
Apply Inv G=I and A²+G²=I to an arbitrary vector x. These give vector equalities without dividing by a scalar or assuming a nonzero space.
3Obtain the energy identity
Take the inner product of the square-sum equality with x and move A and G across the inner product by selfadjointness. The two summands become squared norms.
4Recover the remaining linear operator
Use Inv(G(Gx))=Gx and linearity to write Inv(A(Ax))+Gx=Inv(A(Ax)+G(Gx))=Inv x. This avoids any additional A–G commutation hypothesis.
5Identify the mixed linear contribution
Move A and Inv through the inner products and apply the preceding vector identity with x=r. Thus the sum of the two surviving u-linear terms is exactly the claimed right-hand linear term.
6Expand and cancel the perturbation terms
Expand the two squared norms and C cross term. Since Inv Gr=r, the increment is ⟨u,Gr⟩+⟨v,Ar⟩+(||Gr||²−||Ar||²)/2+⟨A Inv u,Ar⟩−⟨Ar,v⟩+||Ar||². Real symmetry cancels the v terms, the energy identity reduces the quadratic terms to ||r||²/2, and the mixed identity gives ⟨u,Inv r⟩. The result retains the exact positive half.

Full assumptions and notation

All objects and hypotheses

H is a complete real Hilbert space, including the zero space; A,G,Inv are bounded real-linear endomorphisms.
A,G,Inv are selfadjoint; A commutes with Inv; Inv G=G Inv=I; A²+G²=I. All seven structural facts are explicit premises of this auxiliary algebra theorem.
u,v,r are arbitrary in H; C is the exact displayed local definition. No finite dimension, positivity, spectral gap, nontriviality or probability premise.

Mathematical proof

1. Expose the exact functional and typed selfadjoint identities

Unfold only C. State each selfadjointness consequence as an equality of real inner products on the same H, avoiding coercion-sensitive rewrites. No mathematical assumption is added.

\[\langle Ax,y\rangle=\langle x,Ay\rangle,\quad\langle Gx,y\rangle=\langle x,Gy\rangle,\quad\langle\operatorname{Inv}x,y\rangle=\langle x,\operatorname{Inv}y\rangle.\]

Corresponding Lean step

  dsimp only
  have ha (x y : H) : inner ℝ (A x) y=inner ℝ x (A y) := hA.isSymmetric x y
  have hg (x y : H) : inner ℝ (G x) y=inner ℝ x (G y) := hG.isSymmetric x y
  have hi (x y : H) : inner ℝ (Inv x) y=inner ℝ x (Inv y) := hInv.isSymmetric x y