LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-02

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 periodic conjugate square identity for real mean-zero polynomials

Statement

Let $g$ be a real-valued trigonometric polynomial on $T = R / Z$ with zero mean, and let $C$ be the conjugate function of Conjugate function on the circle. Then

$(C g)^{2} = g^{2} + 2 C (g C g) .$

The identity is asserted for trigonometric polynomials only; no extension to arbitrary $L^{p} (T)$ inputs is claimed here, and the mean-zero hypothesis is not removable: for the constant polynomial $g = 1$ one has $C g = 0$ and $C (g C g) = 0$ , so the right-hand side equals $1$ while the left-hand side vanishes.

Facts & Assumptions

Given: A real-valued trigonometric polynomial $g$ on $T$ with zero mean; the conjugate function $C$ on trigonometric polynomials.

[F1]

On trigonometric polynomials $C$ acts coefficientwise by $\hat{C f} (k) = - i sgn (k) \hat{f} (k)$ ; it is complex-linear, kills constants, and preserves real-valuedness, so $C g$ is real-valued for real $g$ . Conjugate function on the circle

[F2]

Characters satisfy $e_{k} e_{l} = e_{k + l}$ and a trigonometric polynomial is a finite complex linear combination of characters. Fourier coefficients and trigonometric polynomials on the torus

[F3]

If $p = \sum_{k \in F} c_{k} e_{k}$ is a trigonometric polynomial, then its Fourier coefficient at $j \in F$ is $\hat{p} (j) = c_{j}$ and $\hat{p} (j) = 0$ for $j \notin F$ . The trigonometric characters are orthonormal in $L^{2}$ of the torus

Proof

technique · direct

1.1F1F2F3

Write the finite expansion $g = \sum_{k \in F} c_{k} e_{k}$ given by [F2]. Since $g$ has mean zero and $0 \in F$ , [F3] gives $c_{0} = \hat{g} (0) = 0$ ; since $g$ is real-valued, [F1] makes $C g = \sum_{k \in F} (- i sgn (k)) c_{k} e_{k}$ real-valued, so $C g = \sum_{k \in F, 0 \neq k} (- i sgn k) c_{k} e_{k}$ has zero mean as well. Adding the two expansions and using complex-linearity of $C$ from [F1] gives $F : = g + i C g = \sum_{k \in F} c_{k} (1 + sgn k) e_{k} = \sum_{k > 0} 2 c_{k} e_{k}$ : a trigonometric polynomial whose only frequencies are strictly positive.

2.1step 1.1F1F2

By [F2], $e_{k} e_{l} = e_{k + l}$ , so expanding the finite square and collecting terms shows that $F^{2} = \sum_{k, l > 0} 4 c_{k} c_{l} e_{k + l}$ is a trigonometric polynomial whose only frequencies are strictly positive. On a polynomial carried by the characters $e_{k}$ with $k > 0$ , the coefficient rule of [F1] gives $C (e_{k}) = - i e_{k}$ , and complex-linearity gives $C (F^{2}) = - i F^{2}$ .

2.2step 1.1F1

Expanding, $F^{2} = (g + i C g)^{2} = g^{2} - (C g)^{2} + 2 i g C g$ ; by 1.1 both $u : = g^{2} - (C g)^{2}$ and $v : = 2 g C g$ are real-valued trigonometric polynomials with real-valued conjugate transforms, and $F^{2} = u + i v$ . By complex-linearity of $C$ , $C (F^{2}) = C u + i C v$ .

3.1step 2.1step 2.2

By 2.1 and 2.2, $C u + i C v = - i F^{2} = - i (u + i v) = v - i u$ . Taking real and imaginary parts of this identity of trigonometric polynomials, whose four real and imaginary parts are real-valued by 2.2, gives $C u = v$ and $C v = - u$ .

4.1step 3.1F1∎

Substituting $u = g^{2} - (C g)^{2}$ and $v = 2 g C g$ into $C v = - u$ gives $2 C (g C g) = (C g)^{2} - g^{2}$ , hence $(C g)^{2} = g^{2} + 2 C (g C g)$ , which is the asserted identity.

Depends on

Used by

The Marcel Riesz conjugate-function theorem on the circle Theorem

Dependency tree · two levels

24 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

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