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.

The Sobolev weight on a single dyadic annulus

Example

Assume Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $0 < ε < 1$ and let $(φ_{j})$ be an admissible partition, in the sense of Existence of a smooth inhomogeneous dyadic frequency partition, whose cutoff satisfies $ψ = 1$ on ${∣ ξ ∣ \leq 1}$ and $supp ψ \subset {∣ ξ ∣ \leq 1 + ε}$ . Set $A_{0} : = {∣ ξ ∣ \leq 1}, A_{j} : = {2^{j - 1} (1 + ε) < ∣ ξ ∣ \leq 2^{j}} (j \geq 1) .$ Then $A_{0}$ is the nonempty unit ball and each $A_{j}$ , $j \geq 1$ , is a nonempty annulus (because $(1 + ε) / 2 < 1$ , so $2^{j - 1} (1 + ε) < 2^{j}$ ), on which $φ_{j} = 1$ and $φ_{i} = 0$ for all $i \neq j$ . For $f \in S (R^{n})$ with $supp \hat{f} \subset A_{j}$ one has $Δ_{j} f = f$ and $Δ_{i} f = 0$ for $i \neq j$ , and for every real $s$ $∥ f ∥_{H^{s}} ≍_{s} 2^{j s} ∥ f ∥_{L^{2}},$ the comparison constants depending only on $n, s$ and the fixed partition. For $j = 0$ the same formula reads $∥ f ∥_{H^{s}} ≍_{s} ∥ f ∥_{2}$ , the correct low-frequency weight and not an exception to be excluded.

Verification

Given: Countable Choice and $0 < ε < 1$ , the admissible partition $(φ_{j})$ with $ψ = 1$ on ${∣ ξ ∣ \leq 1}$ and $ψ = 0$ for $∣ ξ ∣ \geq 1 + ε$ ; a real $s$ ; $j \geq 0$ ; $f \in S$ with $supp \hat{f} \subset A_{j}$ .

[L1] The pieces are $φ_{0} = ψ$ and $φ_{j} (ξ) = ψ (2^{- j} ξ) - ψ (2^{- (j - 1)} ξ)$ for $j \geq 1$ , with $ψ = 1$ on ${∣ ξ ∣ \leq 1}$ and $ψ = 0$ on ${∣ ξ ∣ \geq 1 + ε}$ (Existence of a smooth inhomogeneous dyadic frequency partition).

[L2] For every $U$ in the image of the canonical embedding $E_{s}$ the Littlewood-Paley characterisation gives $∥ U ∥_{H^{s}}^{2} ≍ \sum_{i \geq 0} 2^{2 i s} ∥ Δ_{i} U ∥_{L^{2}}^{2}$ , with constants depending only on $n, s$ and the partition; Schwartz functions lie in that image and $Δ_{i} u_{f} = u_{Δ_{i} f}$ for $f \in S$ (Littlewood-Paley characterisation of the Hilbert-Sobolev spaces, The inhomogeneous dyadic frequency partition and its Littlewood-Paley operators, Real-order Bessel-potential completion H^s, Real-order H^s as weighted Fourier distributions).

[L3] Plancherel: $∥ f ∥_{L^{2}} = ∥ \hat{f} ∥_{L^{2}}$ for Schwartz $f$ (Plancherel theorem).

1.1L1givenalgebra

The values of the pieces on $A_{j}$ . Let $ξ \in A_{j}$ . If $j = 0$ then $∣ ξ ∣ \leq 1$ and $φ_{0} (ξ) = ψ (ξ) = 1$ ; if $j \geq 1$ then $∣ ξ ∣ \leq 2^{j}$ gives $ψ (2^{- j} ξ) = 1$ , while $∣ ξ ∣ > 2^{j - 1} (1 + ε)$ gives $∣ 2^{- (j - 1)} ξ ∣ > 1 + ε$ , hence $ψ (2^{- (j - 1)} ξ) = 0$ and $φ_{j} (ξ) = 1$ . For $i \neq j$ : if $1 \leq i \leq j - 1$ then the smaller argument has $∣ 2^{- i} ξ ∣ \geq ∣ 2^{- (j - 1)} ξ ∣ > 1 + ε$ , and so does the larger argument, so both $ψ$ values vanish and $φ_{i} (ξ) = 0$ ; for $i = 0 < j$ , $∣ ξ ∣ > 1 + ε$ gives $φ_{0} (ξ) = ψ (ξ) = 0$ ; if $i \geq j + 1$ then the larger argument has $∣ 2^{- (i - 1)} ξ ∣ \leq 2^{- j} ∣ ξ ∣ \leq 1$ , so both $ψ$ values are $1$ and again $φ_{i} (ξ) = 0$ .

2.1L1step 1.1algebra

The pieces of $f$ . By step 1.1, $\hat{Δ_{j} f} = φ_{j} \hat{f} = \hat{f}$ and $\hat{Δ_{i} f} = φ_{i} \hat{f} = 0$ for $i \neq j$ ; since the Fourier transform is injective on tempered distributions, $Δ_{j} f = f$ and $Δ_{i} f = 0$ for $i \neq j$ .

3.1L2L3step 1.1step 2.1algebra

The Sobolev comparison. Applying the characterisation [L2] to the regular distribution $u_{f}$ of $f$ , whose $Δ_{i}$ -images are $u_{Δ_{i} f}$ by [L2], and using step 2.1, gives $∥ f ∥_{H^{s}}^{2} ≍ \sum_{i \geq 0} 2^{2 i s} ∥ Δ_{i} f ∥_{2}^{2} = 2^{2 j s} ∥ f ∥_{2}^{2}$ ; moreover on $A_{j}$ the Japanese bracket satisfies $⟨ ξ ⟩ ≍ 2^{j}$ for $j \geq 1$ (as $2^{j - 1} (1 + ε) < ∣ ξ ∣ \leq 2^{j}$ ) and $⟨ ξ ⟩ ≍ 1 = 2^{0}$ for $j = 0$ , so the weight implicit in the comparison is exactly the dyadic weight $2^{j s}$ . Taking square roots gives $∥ f ∥_{H^{s}} ≍_{s} 2^{j s} ∥ f ∥_{2}$ with constants depending only on $n, s$ and the fixed partition (through $ε$ ).

4.1step 1.1step 2.1step 3.1∎

Conclusion. Steps 1.1 to 3.1 verify the asserted values of the pieces, the identities $Δ_{j} f = f$ , $Δ_{i} f = 0$ ( $i \neq j$ ), and the two-sided Sobolev comparison, including the low-frequency case $j = 0$ where the weight $2^{0} = 1$ is the correct one.

Existence of the partition. For completeness, such a cutoff exists for every $0 < ε < 1$ : putting $q (ξ) : = ((1 + ε)^{2} - ∣ ξ ∣^{2}) / ((1 + ε)^{2} - 1)$ and $ψ : = σ \circ q$ with the standard smooth step $σ$ gives a radial smooth cutoff with $ψ = 1$ exactly on ${∣ ξ ∣ \leq 1}$ and $ψ = 0$ for $∣ ξ ∣ \geq 1 + ε$ (The standard smooth step function); the conclusions above hold for the resulting partition.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

50 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

Mark Williams, Notes on Harmonic Analysis (January 11, 2022) (standard reference, not scraped)