LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)

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.

Real L2 multipliers and unitary transport

Statement

Assume countable choice. In complex $H = L^{2} (R^{n})$ use $⟨ f, g ⟩ = \int f \overline{g}$ . For finite real measurable $m$ , set $D (M) = {f \in H : m f \in H}$ and $M f = m f$ . This is well-defined on classes, densely defined and self-adjoint. Here $D (M^{*})$ consists of those $g \in H$ for which some $h \in H$ satisfies $⟨ M f, g ⟩ = ⟨ f, h ⟩$ for every $f \in D (M)$ , and $M^{*} g = h$ ; density makes this value unique.

The operators $V_{t} f = e^{i t m} f$ , $t \in R$ , form a strongly continuous unitary group. The norm derivative $\lim_{t \to 0} (V_{t} f - f) / t$ exists exactly for $f \in D (M)$ and then equals $i M f$ .

For a specified unitary $U : H \to H$ , the operator $P = U^{- 1} M U$ on $D (P) = U^{- 1} D (M)$ is self-adjoint. Define $e^{i t P} = U^{- 1} V_{t} U$ ; this group has derivative $i P$ exactly on $D (P)$ . Only this explicitly transported exponential is being defined.

Facts & Assumptions

Given: The Axiom of Countable Choice ( ${A C}_{ω}$ ), the stated $m$ and unitary $U$ (a surjective complex-linear pairing isometry). Almost-everywhere equality preserves integrals (Two integrable functions are equal almost everywhere exactly when all of their indefinite integrals agree).

[F1]

The complex pairing is definite, continuous and satisfies Cauchy–Schwarz (Complex completeness, density, and inner product: the consumer interface).

[F2]

Dominated convergence applies with an integrable majorant (Dominated convergence).

[F3]

Fatou bounds the integral of a nonnegative pointwise limit by the lower limit of its integrals (Fatou's lemma).

[F4]

A nonnegative function of integral zero vanishes a.e. (A nonnegative measurable function has integral $0$ exactly when it vanishes almost everywhere).

[F5]

The exponential addition and Euler identities give the group law and modulus one ( $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential, $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ ).

[F6]

The sine/cosine derivative formulas and the complex interval FTC give $∣ e^{i t s} - 1 ∣ \leq ∣ t s ∣$ for real $s, t$ , and derivative $i s$ at $t = 0$ (The derivatives of sine and cosine are cosine and minus sine, Complex integration by parts on intervals and decaying lines).

Proof

technique · direct

1.1

Null-equivalent finite representatives give null-equivalent products; this applies to changes of $m$ as well as $f$ , so domain and value are well-defined. The domain is a vector subspace. With $E_{N} = {∣ m ∣ \leq N}$ and $f_{N} = 1_{E_{N}} f$ , one has $∥ m f_{N} ∥_{2} \leq N ∥ f ∥_{2}$ , so $f_{N} \in D (M)$ . Finiteness of $m$ gives $E_{N} ↑ R^{n}$ , and [F2] applied to $1_{E_{N}^{c}} ∣ f ∣^{2} \leq ∣ f ∣^{2}$ gives $f_{N} \to f$ in norm. This proves density. If $h, h^{'}$ both satisfy the adjoint identity for $g$ , then $⟨ f, h - h^{'} ⟩ = 0$ on this dense domain; continuity in [F1] extends it to every $f \in H$ , including $h - h^{'}$ , forcing $h = h^{'}$ .

F1F2given

1.2

By [F5], $V_{t} V_{s} = V_{t + s}$ , $V_{0} = I$ , $V_{- t} = V_{t}^{- 1}$ and $⟨ V_{t} f, V_{t} g ⟩ = ⟨ f, g ⟩$ . For fixed $f$ , $∣ e^{i t m} - 1 ∣^{2} ∣ f ∣^{2} \to 0$ pointwise as $t \to 0$ , with majorant $4 ∣ f ∣^{2}$ . [F2] gives strong continuity at zero; the isometry and group law give it at every $t$ . Countable choice permits the sequential criterion for these real-parameter norm limits.

F1F2F5given

2.1

Real-valuedness of $m$ and [F1] give $⟨ M f, g ⟩ = ⟨ f, M g ⟩$ for $f, g \in D (M)$ , with both integrals absolutely convergent. Thus $D (M) \subseteq D (M^{*})$ with the same value. Conversely let $M^{*} g = h$ . On $E_{N}$ , $w_{N} = 1_{E_{N}} (m g - h)$ is in $H$ , and $m w_{N} \in H$ because $∣ m ∣ \leq N$ there, so $w_{N} \in D (M)$ . Inserting $f = w_{N}$ into the adjoint identity gives $0 = ⟨ M w_{N}, g ⟩ - ⟨ w_{N}, h ⟩ = \int_{E_{N}} ∣ m g - h ∣^{2}$ . By [F4], $m g = h$ a.e. on each $E_{N}$ . Their countable union is the whole space, so $m g = h$ a.e. globally; in particular $m g \in H$ . Thus $D (M^{*}) = D (M)$ and the operators agree.

step 1.1F1F4given

2.2

If $m f \in H$ , [F6] gives pointwise $(e^{i t m} - 1) f / t \to i m f$ and the squared error is at most $4 ∣ m f ∣^{2}$ . [F2] proves norm convergence to $i M f$ . Conversely, if the norm derivative exists, the quotients at $t = 1 / (N + 1)$ have bounded norms for $N \in N$ . Their squared moduli tend pointwise to $∣ m f ∣^{2}$ by [F6]. [F3] gives $\int ∣ m f ∣^{2} \leq {lim inf}_{N} ∥ (V_{1 / (N + 1)} f - f) / (1 / (N + 1)) ∥_{2}^{2} < \infty$ . Thus $f \in D (M)$ , and the forward part identifies the derivative. This proves both directions, including points where $m = 0$ .

step 1.2F2F3F6

3.1

Since $U$ and $U^{- 1}$ preserve norms and pairings, $U^{- 1} D (M)$ is dense. For $g, h \in H$ , the assertion $⟨ P f, g ⟩ = ⟨ f, h ⟩$ for every $f \in D (P)$ is equivalent, by writing $v = U f$ , to $⟨ M v, U g ⟩ = ⟨ v, U h ⟩$ for every $v \in D (M)$ . By step 2.1 this holds exactly when $U g \in D (M)$ and $U h = M U g$ . Therefore $D (P^{*}) = D (P)$ and $P^{*} = P$ . Conjugating the group identities and norm limits of steps 1.2 and 2.2 by $U$ proves the asserted unitary group, continuity, and both directions of the transported derivative-domain criterion. No spectral theorem or choice of a basis is used.

step 1.1step 2.1step 1.2step 2.2given∎

Depends on

Used by

Momentum operator under the Fourier transform Example

Dependency tree · two levels

51 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

Gerald Teschl, Mathematical Methods in Quantum Mechanics, 2nd edition (standard reference, not scraped)