Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The elliptic resolvent identity

Statement

Assume the Axiom of Choice and Countable Choice. In the symmetric case of The L2 operator associated with a symmetric elliptic form, let the scalar field be K∈{R,C} and let Ω be bounded and open. Define H~:=L2(Ω;C) and L~=L if K=C; if K=R, use the canonical isometric identification L2(Ω;R)C≅L2(Ω;C) and set L~=LC, the complexification LC(u+iv)=Lu+iLv on D(L)+iD(L) (The complex L2 pairing on equivalence classes, Complex Lp classes and Euclidean test-function conventions, Complexification as C⊗RV with its canonical real-linear embedding, Complexification of a real-linear map, The symmetric elliptic form operator is self-adjoint with compact resolvent). Write σ(L~) for its complex spectrum as in Resolvent and spectrum of an unbounded operator. For z∉σ(L~) put Rz:=(L~−z)−1 in the adopted L~−z convention, so that Rz:H~→D(L~) is bijective onto D(L~) with (L~−z)Rz=I on H~ and Rz(L~−z)=I on D(L~). Then for all z,w∉σ(L~) Rz−Rw=(z−w)RzRw=(z−w)RwRz, the identities holding on all of H~; in particular RzRw=RwRz. Each Rz is compact on H~.

Facts & Assumptions

Given: the Axiom of Choice and Countable Choice; a bounded open set Ω⊆Rn; the symmetric-case operator L and its complex realization L~ with its complex spectrum σ(L~); complex numbers z,w∉σ(L~); and the resolvents Rz,Rw.

[F1]

Resolvent data: for z∉σ(L~) the operator L~−z:D(L~)→H~ is bijective with bounded inverse Rz, Rz maps H~ into D(L~), (L~−z)Rz=I on H~ and Rz(L~−z)=I on D(L~) (Resolvent and spectrum of an unbounded operator).

[F2]

Compact resolvent: each Rz is compact on H~ (The symmetric elliptic form operator is self-adjoint with compact resolvent, Compact linear operator, The Axiom of Choice).

[F3]

Composition conventions: products of the resolvents in either order are defined on all of H~ because Rz,Rw map H~ into D(L~), on which the other resolvent is defined; a general second-resolvent identity for closed operators is available for comparison (Second resolvent identity for a closed perturbation, The L2 operator associated with a symmetric elliptic form, Resolvent and spectrum of an unbounded operator).

Proof

technique · direct
1.1F1F3givenalgebra

The identity. On H~ insert the two inverse relations of [F1]: Rz−Rw=Rz(L~−w)Rw−Rz(L~−z)Rw=Rz[(L~−w)−(L~−z)]Rw=(z−w)RzRw, where the first equality uses (L~−w)Rw=I and Rz(L~−z)=I; all products are everywhere defined by [F3]. Exchanging z,w gives Rz−Rw=(z−w)RwRz; comparing the two expressions gives (z−w)RzRw=(z−w)RwRz. If z≠w, divide by z−w; if z=w, the products are identical.

2.1F2step 1.1given∎

Compactness. Each Rz is compact on H~ by [F2]; the resolvent identity itself is an operator identity on all of H~ and involves no compactness, and no choice beyond [F1] and [F2] is used.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

80 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources