ExampleConstruction: Literature-sourcedVerification: 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.

Transform of an interval indicator

Example

Assume countable choice and $a \leq b$ . For $f = 1_{[a, b]}$ on $R$ , $\hat{f} (ξ) = \frac{e^{- 2 π i a ξ} - e^{- 2 π i b ξ}}{2 π i ξ} (ξ \neq 0), \hat{f} (0) = b - a .$ In particular for $[a, b] = [- 1 / 2, 1 / 2]$ the transform is $\sin (π ξ) / (π ξ)$ with value one at zero.

Facts & Assumptions

Given: $a \leq b$ and The Axiom of Countable Choice ( ${A C}_{ω}$ ), with the integral convention of Fourier transform on complex L1 classes.

[F1]

Complex FTC evaluates continuous derivatives on intervals (Complex integration by parts on intervals and decaying lines).

[F2]

Euler's formula and the real sine/cosine derivatives give the exponential derivative ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ , The derivatives of sine and cosine are cosine and minus sine).

[F3]

The transform of an integrable function is continuous (The L1 transform is bounded and uniformly continuous).

Verification

1.1

The interval indicator is integrable with norm $b - a$ . For $a < b$ and $ξ \neq 0$ , F2 gives the antiderivative $- e^{- 2 π i x ξ} / (2 π i ξ)$ . F1 at a and b gives the displayed quotient. If $a = b$ the indicator is null almost everywhere and both the numerator and transform vanish.

F1F2given

2.1

At zero frequency the integral is the interval length $b - a$ ; F3 shows this is the continuous extension of the quotient. For the symmetric interval its numerator is $e^{π i ξ} - e^{- π i ξ} = 2 i \sin (π ξ)$ by F2, giving the sinc formula and value one. Countable choice is inherited from the interval Lebesgue measure and FTC bridge.

F1F2F3step 1.1∎

Depends on

Used by

An L1 transform need not be integrable Counterexample
Triangle function and squared sinc Example

Dependency tree · two levels

38 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, Topics in Real and Functional Analysis (2017) (standard reference, not scraped)