ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generated

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.

Two separated dyadic frequency packets add in Euclidean square

Example

Assume Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $0 \leq j < k$ be integers with $k \geq j + 3$ , and let $f_{1}, f_{2} \in S (R^{n})$ have Fourier transforms supported in ${2^{j - 1} \leq ∣ ξ ∣ \leq 2^{j + 1}}$ and ${2^{k - 1} \leq ∣ ξ ∣ \leq 2^{k + 1}}$ respectively; put $f : = f_{1} + f_{2}$ . Then for every $i \geq 0$ at most one of $Δ_{i} f_{1}$ , $Δ_{i} f_{2}$ is nonzero, so $S f^{2} = S f_{1}^{2} + S f_{2}^{2}, ∥ S f ∥_{2}^{2} = ∥ S f_{1} ∥_{2}^{2} + ∥ S f_{2} ∥_{2}^{2} .$ Moreover $⟨ f_{1}, f_{2} ⟩ = 0$ by Plancherel, so $∥ f ∥_{2}^{2} = ∥ f_{1} ∥_{2}^{2} + ∥ f_{2} ∥_{2}^{2}$ and the square function of the sum has the Euclidean-square size of the two packets rather than the sum of their absolute sizes. This is the finite two-packet instance of L2 almost orthogonality of the dyadic pieces.

Verification

Given: Countable Choice and integers $0 \leq j < k$ with $k \geq j + 3$ and $f_{1}, f_{2} \in S (R^{n})$ with $supp \hat{f_{1}} \subset {2^{j - 1} \leq ∣ ξ ∣ \leq 2^{j + 1}}$ and $supp \hat{f_{2}} \subset {2^{k - 1} \leq ∣ ξ ∣ \leq 2^{k + 1}}$ ; $f = f_{1} + f_{2}$ .

[L1] For every $i \geq 0$ one has $\hat{Δ_{i} f_{t}} = φ_{i} \hat{f_{t}}$ for $t = 1, 2$ , and $φ_{i}$ vanishes for $∣ ξ ∣ \leq 2^{i - 1}$ (when $i \geq 1$ ) and for $∣ ξ ∣ \geq 2^{i + 1}$ , with the nonzero set of $φ_{i}$ contained in the open annulus $2^{i - 1} < ∣ ξ ∣ < 2^{i + 1}$ for $i \geq 1$ and in ${∣ ξ ∣ < 2}$ for $i = 0$ (The inhomogeneous dyadic frequency partition and its Littlewood-Paley operators, Existence of a smooth inhomogeneous dyadic frequency partition).

[L2] For every $h \in L^{2}$ the square function satisfies $∥ S h ∥_{2}^{2} = \sum_{i \geq 0} ∥ Δ_{i} h ∥_{2}^{2}$ with the two-sided $L^{2}$ bound of L2 almost orthogonality of the dyadic pieces, in particular the sum is finite for Schwartz $h$ ; and $∥ h ∥_{2}^{2} = \int ∣ \hat{h} ∣^{2}$ (Plancherel theorem, The Littlewood-Paley square function).

1.1L1givenalgebra

Disjointness of the active levels. Suppose first that $i \geq 1$ and $Δ_{i} f_{1} \neq 0$ . Since $\hat{Δ_{i} f_{1}} = φ_{i} \hat{f_{1}}$ by [L1] and the Fourier transform is injective, there is $ξ$ with $φ_{i} (ξ) \neq 0$ and $2^{j - 1} \leq ∣ ξ ∣ \leq 2^{j + 1}$ . By [L1], $φ_{i} (ξ) \neq 0$ forces $2^{i - 1} < ∣ ξ ∣ < 2^{i + 1}$ , so $2^{j - 1} < 2^{i + 1}$ and $2^{i - 1} < 2^{j + 1}$ , which imply $j - 1 \leq i \leq j + 1$ . If instead $i = 0$ and $Δ_{0} f_{1} \neq 0$ , then some $ξ$ in the packet support also lies in $supp φ_{0} \subset {∣ ξ ∣ < 2}$ ; since $2^{j - 1} \leq ∣ ξ ∣ < 2$ , this forces $j \leq 1$ , and therefore $0 \in {j - 1, j, j + 1}$ . Thus every active $i$ for $f_{1}$ belongs to ${j - 1, j, j + 1} \cap {0, 1, 2, \dots}$ . The same argument shows every active $i$ for $f_{2}$ belongs to ${k - 1, k, k + 1}$ ; because $k \geq j + 3$ , the two nonnegative index sets are disjoint. Hence for every $i$ at most one of $Δ_{i} f_{1}$ , $Δ_{i} f_{2}$ is nonzero.

2.1L1step 1.1algebra

Pointwise Euclidean-square identity. For every $x$ and every $i$ , step 1.1 gives $∣ Δ_{i} f (x) ∣^{2} = ∣ Δ_{i} f_{1} (x) + Δ_{i} f_{2} (x) ∣^{2} = ∣ Δ_{i} f_{1} (x) ∣^{2} + ∣ Δ_{i} f_{2} (x) ∣^{2}$ (the cross term vanishes because one of the two numbers is zero), hence $S f (x)^{2} = \sum_{i} ∣ Δ_{i} f (x) ∣^{2} = S f_{1} (x)^{2} + S f_{2} (x)^{2}$ ; the rearrangement is legitimate because each packet has at most three active levels by step 1.1, so only finitely many indices contribute.

3.1L2step 2.1algebra∎

Norms and orthogonality of the packets. Because $f_{1}, f_{2} \in S$ , both square functions lie in $L^{2}$ by [L2], and integrating the identity of step 2.1 gives $∥ S f ∥_{2}^{2} = ∥ S f_{1} ∥_{2}^{2} + ∥ S f_{2} ∥_{2}^{2}$ ; the $L^{2}$ almost orthogonality [L2] identifies each side with the sum of the squared dyadic-piece norms. Finally, $\hat{f_{1}} \hat{f_{2}} = 0$ pointwise because the two Fourier supports are disjoint, so Plancherel gives $⟨ f_{1}, f_{2} ⟩ = \int \hat{f_{1}} \overline{\hat{f_{2}}} = 0$ and $∥ f ∥_{2}^{2} = ∥ f_{1} ∥_{2}^{2} + ∥ f_{2} ∥_{2}^{2}$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

45 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, 3rd ed. (Springer GTM 249) (standard reference, not scraped)