LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

Local polynomial projections matching moments through order $s$

Statement

Assume Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $Q \subseteq R^{n}$ be a nondegenerate axis-parallel cube with centre $c_{Q}$ , side length $ℓ (Q)$ and volume $∣ Q ∣$ in the sense of Axis-parallel rectangles in $R^{m}$ and their volume. Fix $λ > 1$ and write $Q^{*} : = {x \in R^{n} : ∥ x - c_{Q} ∥_{\infty} < λ ℓ (Q) / 2}$ for its open concentric dilation. Let $N \in N \cup {0}$ , and let $ω_{Q} \in C_{c}^{\infty} (R^{n})$ be real, nonnegative, with $\int_{R^{n}} ω_{Q} > 0$ and $supp ω_{Q} \subset Q^{*}$ . Then for every tempered distribution $f \in S^{'} (R^{n})$ there is a unique moment-matching polynomial $P_{Q}$ of total degree at most $N$ such that $⟨ f - P_{Q}, x^{α} ω_{Q} ⟩ = 0 for every multi-index ∣ α ∣ \leq N .$ The polynomial $P_{Q}$ depends only on the restriction of $f$ to an open neighbourhood of $supp ω_{Q}$ : for every open $U \supseteq supp ω_{Q}$ , if $g \in S^{'}$ agrees with $f$ as a distribution on $U$ , then $P_{Q}^{g} = P_{Q}^{f}$ . When $f$ is represented by a function in $L^{2} (ω_{Q} (x) d x)$ , this is the orthogonal projection of $f$ onto the polynomials of degree at most $N$ in that weighted inner product space, with inner product $(P, R)_{ω_{Q}} = \int_{R^{n}} P (x) \overline{R (x)} ω_{Q} (x) d x$ . This inner product is positive definite on the polynomial subspace because $ω_{Q} \geq 0$ and $\int ω_{Q} > 0$ .

Facts & Assumptions

Given: Countable Choice and a nondegenerate axis-parallel cube $Q$ , an integer $N \geq 0$ , a test function $ω_{Q}$ as in the statement, $f \in S^{'} (R^{n})$ , and multi-indices with the conventions of $C^{k}$ maps and multi-index derivative notation in Euclidean space.

[L1]

A nonnegative continuous function on an open set with positive integral is positive at some point, hence positive on a nonempty open subset of that set; a polynomial vanishing on a nonempty open set is zero: at an interior point all its partial derivatives vanish, and its finite expansion about that point, obtained by the binomial formula for each monomial, has precisely those derivatives as coefficients (The spaces $C_{c} (R^{n})$ and $C_{c}^{\infty} (R^{n})$ fixes the support convention).

[F1]

$x^{α} ω_{Q} \in C_{c}^{\infty} (R^{n}) \subseteq S (R^{n})$ , so the pairings $⟨ f, x^{α} ω_{Q} ⟩$ and, for polynomials $P$ , the regular-distribution pairings $⟨ P, x^{α} ω_{Q} ⟩ = \int P x^{α} ω_{Q}$ are defined; polynomials are locally integrable and $P x^{α} ω_{Q} \in S$ (Schwartz space and its seminorms, Tempered distribution, Regular distribution from a locally integrable function).

[F2]

The space $P_{N}$ of polynomials of total degree at most $N$ has finite dimension $d = (\binom{N + n}{n})$ , and the monomials $x^{α}$ , $∣ α ∣ \leq N$ , form a basis ( $C^{k}$ maps and multi-index derivative notation in Euclidean space). A finite-dimensional linear system with invertible matrix has a unique solution.

[F3]

If two distributions agree on an open set $U$ , then their pairings with every test function supported in $U$ agree: this is the definition of agreement of distributions on $U$ (Distribution). In particular, if $h \in C_{c}^{\infty} (R^{n})$ is supported in $U$ and $f = 0$ on $U$ , then $⟨ f, h ⟩ = 0$ .

[F4]

Since $ω_{Q}$ is measurable and nonnegative, $d μ_{Q} = ω_{Q} (x) d x$ is the measure with density $ω_{Q}$ relative to Lebesgue measure (The measure with density $f$ relative to $μ$ ).

[F5]

On the measure space $(R^{n}, μ_{Q})$ the pairing $([u], [v]) \mapsto \int u \overline{v} d μ_{Q}$ is the well-defined complex $L^{2}$ inner product (The complex $L^{2}$ pairing is well-defined and satisfies Cauchy–Schwarz).

Proof technique: positive-definite Gram matrix on the finite-dimensional polynomial space.

Proof

technique · direct

1.1L1F1F2algebra

The Gram matrix. Set $G_{α β} = \int_{R^{n}} x^{α + β} ω_{Q} (x) d x$ for $∣ α ∣, ∣ β ∣ \leq N$ . If $P = \sum_{∣ α ∣ \leq N} c_{α} x^{α}$ satisfies $\int ∣ P ∣^{2} ω_{Q} = 0$ , then $∣ P ∣^{2} ω_{Q} = 0$ Lebesgue-a.e.; since $∣ P ∣^{2}$ is continuous and $ω_{Q}$ is continuous and positive on a nonempty open set by [L1] (using $\int ω_{Q} > 0$ and $ω_{Q} \geq 0$ ), $P$ vanishes on that open set, hence $P = 0$ and all $c_{α} = 0$ by [L1] and [F2]. Writing $\int ∣ P ∣^{2} ω_{Q} = \sum_{α, β} \overline{c_{α}} c_{β} G_{α β}$ , positive definiteness follows, so $G$ is invertible.

2.1step 1.1F1F2F4F5algebra

Existence and uniqueness. The vector $b = (⟨ f, x^{α} ω_{Q} ⟩)_{∣ α ∣ \leq N} \in C^{d}$ is well defined by [F1], so [F2] gives a unique coefficient vector $c = G^{- 1} b$ and a polynomial $P_{Q} = \sum_{∣ α ∣ \leq N} c_{α} x^{α}$ with $⟨ P_{Q}, x^{β} ω_{Q} ⟩ = \sum_{α} c_{α} G_{α β} = b_{β} = ⟨ f, x^{β} ω_{Q} ⟩$ for every $∣ β ∣ \leq N$ ; that is, $⟨ f - P_{Q}, x^{β} ω_{Q} ⟩ = 0$ . If $f$ is represented by an element of $L^{2} (μ_{Q})$ , then for every polynomial $R$ of degree at most $N$ its conjugate is a linear combination of the real monomials $x^{α}$ , and the moment equations give $(f - P_{Q}, R)_{ω_{Q}} = \int (f - P_{Q}) \overline{R} d μ_{Q} = 0$ by [F4, F5]. Thus $P_{Q}$ is the orthogonal projection onto the polynomial subspace in the weighted $L^{2}$ inner product space. If $P^{'}, P^{''}$ both satisfy the moment equations, then $R = P^{'} - P^{''}$ satisfies $⟨ R, x^{α} ω_{Q} ⟩ = 0$ for $∣ α ∣ \leq N$ , so $\int ∣ R ∣^{2} ω_{Q} = \sum \overline{c_{α}} ⟨ R, x^{α} ω_{Q} ⟩ = 0$ with $c_{α}$ the coefficients of $R$ , because $\overline{R} = \sum \overline{c_{α}} x^{α}$ , and step 1.1 gives $R = 0$ . This proves existence and uniqueness.

3.1step 2.1F3given

Locality. Let $U$ be the given neighbourhood of $supp ω_{Q}$ on which $f$ and $g$ agree as distributions. For every $∣ α ∣ \leq N$ , the test function $x^{α} ω_{Q}$ is supported in $supp ω_{Q} \subset U$ , so [F3] gives $⟨ f - g, x^{α} ω_{Q} ⟩ = 0$ . Hence $f$ and $g$ produce the same vector $b$ in step 2.1, and therefore the same $P_{Q} = G^{- 1} b$ . This proves the locality statement.

4.1step 1.1step 2.1step 3.1∎

Conclusion. Step 1.1 shows that the Gram matrix is positive definite, step 2.1 constructs the unique moment-matching polynomial and identifies it as the weighted $L^{2}$ orthogonal projection when that interpretation applies, and step 3.1 records dependence only on the distribution near the support of the weight. This proves the lemma.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

41 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

Mitsuo Izuki, Eiichi Nakai, Yoshihiro Sawano, Hardy spaces with variable exponents, RIMS Kokyuroku Bessatsu B42 (2014), 123-136 (standard reference, not scraped)
Stefano Meda, Peter Sjogren, Maria Vallarino, Atomic decompositions and operators on Hardy spaces, Revista de la Union Matematica Argentina 50 (2009), no. 2, 15-22 (standard reference, not scraped)

Local polynomial projections matching moments through order ss