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.

Separated frequency blocks do not disturb earlier partial sum maxima

Statement

Let $P = \sum_{k = 0}^{d} c_{k} e_{k}$ , $m \geq 1$ an integer, $a \in C$ , and $Q = a e_{m} P$ . Its Fourier support is contained in $[m, m + d]$ , $A_{N} Q = 0$ for $N < m$ , and $A_{m + r} Q = a e_{m} A_{r} P$ for $0 \leq r \leq d$ . Thus disjoint later blocks leave earlier cutoffs unchanged, and internal maxima scale by $∣ a ∣$ . Pointwise $∣ Q ∣ = ∣ a ∣ ∣ P ∣$ ; for any set E, a separate bound $∣ a ∣ ∣ P (x) ∣ \leq ε$ for all $x \in E$ implies $∣ Q (x) ∣ \leq ε$ there. When the supremum of $∣ P ∣$ on E is finite, this is equivalently the stated bound $∣ a ∣ \sup_{E} ∣ P ∣ \leq ε$ . Modulation alone gives no magnitude reduction.

Facts & Assumptions

[F1]

Analytic cutoff and finite maximal-function conventions are fixed Kolmogorov analytic partial sum maximal function.

[F2]

$e_{k} e_{m} = e_{k + m}$ and Fourier coefficients use normalized period-one integration Period-one Fourier coefficients, partial sums, and convolution on the torus.

Proof

Given: The polynomial P, scalar a and integer m in the statement.

1.1

Multiplying the finite sum gives $Q = \sum_{k = 0}^{d} a c_{k} e_{m + k}$ . Orthogonality of the characters, verified in F1, identifies the coefficient at $m + k$ with $a c_{k}$ and all other coefficients with zero. Thus the claimed support containment holds, even when some coefficients vanish. At $N < m$ the cutoff contains no supported frequency, so $A_{N} Q = 0$ .

F1F2

2.1

At $N = m + r$ , $0 \leq r \leq d$ , exactly the terms with $k \leq r$ occur, so $A_{m + r} Q = \sum_{k = 0}^{r} a c_{k} e_{m + k} = a e_{m} A_{r} P$ . Taking absolute values and the finite maximum gives $\max_{0 \leq r \leq d} ∣ A_{m + r} Q ∣ = ∣ a ∣ A_{*}^{d} P$ . By linearity of a finite coefficient sum, adding any polynomial supported strictly beyond a cutoff leaves that cutoff unchanged; the same conclusion applies to any finite list of later separated blocks.

F1F2step 1.1

3.1

Since $∣ e_{m} (x) ∣ = 1$ for every x, $∣ Q (x) ∣ = ∣ a ∣ ∣ P (x) ∣$ at every point, and every separately supplied amplitude bound on E transfers unchanged. If $a = 0$ , Q is zero regardless of E; for E empty the pointwise bound is vacuous (use supremum zero for nonnegative functions on the empty set). In particular $a = 1$ , $P = 1$ gives $∣ Q ∣ = 1$ for every m, so frequency shifts cannot make it smaller than one on a nonempty set. These are finite algebraic identities and use no choice axiom.

F2step 2.1∎

Depends on

Used by

Dependency tree · one level

2 results within one dependency step 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

Grafakos, Classical Fourier Analysis, third edition (standard reference, not scraped)