LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)

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.

Elementary Fourier ray and derivative L2 bounds

Statement

Assume Countable Choice. Let $U$ be bounded and open, $ϕ \in C_{c}^{\infty} (R^{d})$ , and $ρ > 0$ . For every $ξ \in R^{d}$ and coordinate $j$ , $\int_{0}^{\infty} 2 π ∣ ξ_{j} ∣ ∣ \hat{ϕ} (t ξ) ∣ d t \leq ρ^{- 1} ∥ ϕ ∥_{1} + ρ ∥ \partial_{j}^{2} ϕ ∥_{1} .$ If $T_{ϕ, j}$ is the distributional operator of Truncated Fourier formula for derivatives of the Bogovskii operator, then for every $f \in C_{c}^{\infty} (U)$ its restriction to $U$ is in $L^{2} (U)$ and $∥ T_{ϕ, j} f ∥_{L^{2} (U)} \leq A_{j} (ϕ) ∥ f ∥_{L^{2} (U)}, A_{j} (ϕ) = 2^{(d - 1) / 2} (ρ^{- 1} ∥ ϕ ∥_{1} + ρ ∥ \partial_{j}^{2} ϕ ∥_{1}) + 2^{d} ∣ U ∣ ∥ \partial_{j} ϕ ∥_{\infty} .$ By density, this restriction has a unique bounded extension $L^{2} (U) \to L^{2} (U)$ with the same bound.

Facts & Assumptions

Given: Countable Choice; bounded $U$ , $ϕ \in C_{c}^{\infty}$ , $ρ > 0$ , and the truncated Fourier formula for $T_{ϕ, j}$ .

[A1]

Countable Choice is assumed by the Plancherel/Fourier-multiplier interfaces and is used for the $L^{2}$ density extension. (The Axiom of Countable Choice ( ${A C}_{ω}$ ))

[F1]

For $0 < t < 1 / 2$ , $\hat{T_{ϕ, j}^{<} f} (ξ) = 2 π i ξ_{j} \int_{0}^{1 / 2} \hat{ϕ} (t ξ) \hat{f} ((1 - t) ξ) d t$ . (Truncated Fourier formula for derivatives of the Bogovskii operator)

[F2]

Plancherel identifies the Fourier and $L^{2}$ norms, and $\hat{\partial_{j}^{2} ϕ} (η) = (2 π i η_{j})^{2} \hat{ϕ} (η)$ . (Fourier transform agrees with l one and plancherel transforms, Distributional derivatives are polynomial Fourier multipliers)

[F3]

Tonelli permits integrating the nonnegative Fourier bound in $(t, ξ)$ , and Countable Choice gives density of $C_{c}^{\infty} (U)$ in $L^{2} (U)$ . (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product, Smooth compactly supported functions of an open set are dense in $L^{2}$ , The Axiom of Countable Choice ( ${A C}_{ω}$ ))

[F4]

The L2 Cauchy--Schwarz inequality gives $\int ∣ f g ∣ \leq ∥ f ∥_{2} ∥ g ∥_{2}$ . (Cauchy-Schwarz inequality for $L^{2}$ )

Proof

1.1givenalgebra

If $ξ_{j} = 0$ , the left side of the ray estimate is zero. Otherwise put $t_{0} = (2 π ρ ∣ ξ_{j} ∣)^{- 1}$ . On $[0, t_{0}]$ , use $∣ \hat{ϕ} ∣ \leq ∥ ϕ ∥_{1}$ to bound the integral by $2 π ∣ ξ_{j} ∣ t_{0} ∥ ϕ ∥_{1} = ρ^{- 1} ∥ ϕ ∥_{1}$ .

2.1A1F2algebrastep 1.1

On $[t_{0}, \infty)$ , [F2] gives $∣ \hat{ϕ} (t ξ) ∣ \leq (4 π^{2} t^{2} ξ_{j}^{2})^{- 1} ∥ \partial_{j}^{2} ϕ ∥_{1}$ . Integrating $2 π ∣ ξ_{j} ∣ t^{- 2} / (4 π^{2} ξ_{j}^{2})$ from $t_{0}$ to infinity gives $ρ ∥ \partial_{j}^{2} ϕ ∥_{1}$ . Adding the intervals proves the ray bound.

3.1A1F1F2F3F4step 2.1

Write $m (t, ξ) = 2 π ∣ ξ_{j} ∣ ∣ \hat{ϕ} (t ξ) ∣$ . Cauchy–Schwarz in $t$ and step 2.1 yield $∣ \hat{T^{<} f} (ξ) ∣^{2} \leq R_{j} (ϕ) \int_{0}^{1 / 2} m (t, ξ) ∣ \hat{f} ((1 - t) ξ) ∣^{2} d t,$ where $R_{j} (ϕ) = ρ^{- 1} ∥ ϕ ∥_{1} + ρ ∥ \partial_{j}^{2} ϕ ∥_{1}$ . Integrate in $ξ$ , set $η = (1 - t) ξ$ , and then $s = t / (1 - t)$ . Since $(1 - t)^{- (d + 1)} d t = (1 + s)^{d - 1} d s \leq 2^{d - 1} d s$ for $0 \leq s \leq 1$ , the inner integral is at most $2^{d - 1} R_{j} (ϕ) ∥ f ∥_{2}^{2}$ by the ray bound and [F2]. Plancherel [F2] then gives $∥ T_{ϕ, j}^{<} f ∥_{2} \leq 2^{(d - 1) / 2} R_{j} (ϕ) ∥ f ∥_{2}$ .

4.1A1F1givenF4step 3.1

For $1 / 2 \leq t \leq 1$ , the kernel $t^{- d} \partial_{x_{j}} [ϕ (y + (x - y) / t)]$ has absolute value at most $2^{d + 1} ∥ \partial_{j} ϕ ∥_{\infty}$ ; integrating the sharper factor $t^{- d - 1}$ over this interval gives at most $2^{d} ∥ \partial_{j} ϕ ∥_{\infty}$ . On $U \times U$ its integral operator has $L^{2} (U)$ norm at most $2^{d} ∣ U ∣ ∥ \partial_{j} ϕ ∥_{\infty}$ by Cauchy–Schwarz in $y$ and then $x$ . Add this to the short-range bound of step 3.1, which was proved on all of $R^{d}$ and hence also holds after restriction to $U$ .

5.1A1F1F3step 3.1step 4.1∎

The estimates hold first for $f \in C_{c}^{\infty} (U)$ . Density in $L^{2} (U)$ extends the restriction of the distributional operator uniquely to all $L^{2} (U)$ inputs and preserves the same bound. Convergence in $L^{2} (U)$ implies convergence against every test function in $C_{c}^{\infty} (U)$ , so this extension agrees on $U$ with the distributional limit from the definition.

Depends on

Used by

Bounded Bogovskii right inverse on a star-shaped domain Theorem

Dependency tree · two levels

58 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

Ricardo G. Durán, An elementary proof of the continuity from L2_0(Omega) to H1_0(Omega)^n of Bogovskii’s right inverse of the divergence (standard reference, not scraped)
Daniele Boffi, Franco Brezzi, Michel Fortin, Mixed Finite Element Methods and Applications (complete textbook) (standard reference, not scraped)