LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck 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.

Bessel and Slobodeckij norms agree at order one half

Statement

Assume Countable Choice. For $f \in S (R^{2})$ , define $[f]_{1 / 2, 2}^{2} = \int_{R^{2}} \int_{R^{2}} \frac{∣ f (x) - f (y) ∣^{2}}{∣ x - y ∣^{3}} d x d y .$ There is a finite constant $c_{*} > 0$ such that $[f]_{1 / 2, 2}^{2} = c_{*} \int_{R^{2}} ∣ ξ ∣ ∣ \hat{f} (ξ) ∣^{2} d ξ .$ Consequently, the norm $∥ f ∥_{2}^{2} + [f]_{1 / 2, 2}^{2}$ is equivalent on $S (R^{2})$ to the Bessel-potential norm $\int_{R^{2}} (1 + 4 π^{2} ∣ ξ ∣^{2})^{1 / 2} ∣ \hat{f} (ξ) ∣^{2} d ξ$ . The two completions therefore define the same $H^{1 / 2} (R^{2})$ space with equivalent norms.

Facts & Assumptions

Given: Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )) and a Schwartz function $f$ on $R^{2}$ .

[A1]

Countable Choice is assumed for the Fourier and product-measure suppliers (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

The Fourier transform agrees with its unitary Plancherel extension on $L^{2}$ , and translations transform into multiplication by $e^{2 π i ξ \cdot h}$ (Fourier transform agrees with l one and plancherel transforms).

[F2]

Lebesgue measure is translation invariant, and the $L^{1}$ Fourier transform of $f (\cdot + h)$ is $e^{2 π i ξ \cdot h} \hat{f} (ξ)$ (Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation, Translation, modulation, linear dilation and reflection laws).

[F3]

Nonnegative measurable functions on product measure spaces may be integrated in either order (Tonelli and Fubini for the completed product, with only almost-everywhere section measurability).

[F4]

Use the equivalent Hilbert renorming of the Bessel-potential $H^{1 / 2} (R^{2})$ completion with Fourier weight $(1 + 4 π^{2} ∣ ξ ∣^{2})^{1 / 2}$ : it is between the published weight $(1 + ∣ ξ ∣^{2})^{1 / 2}$ and $2 π$ times that weight (Real-order H^s as weighted Fourier distributions).

[F5]

An invertible linear map changes Lebesgue measure by the absolute determinant (A linear map $T$ of $R^{n}$ sends Lebesgue measurable sets to Lebesgue measurable sets, with $λ_{n} (T [E]) = ∣ \det T ∣ λ_{n} (E)$ when $T$ is invertible and $T [E]$ Lebesgue null when it is not).

[F90]

Polar integration uses the published radial formula, not a linear substitution: $d x = r^{n - 1} d r d σ (ω)$ . The sphere measure agrees with graph-chart surface measure and scales by $R^{n - 1}$ . (Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma, Agreement with the existing polar sphere measure)

[F91]

The complex exponential has derivative itself and $∣ e^{i t} ∣ = 1$ for real $t$ . The finite-dimensional FTC, applied to real and imaginary parts along $t \mapsto i t$ , gives $∣ e^{i t} - 1 ∣ \leq ∣ t ∣$ . (The complex exponential is entire and its complex derivative is itself, $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ , If $f : [a, b] \to R^{m}$ is differentiable with integrable $f^{'}$ then $\int_{a}^{b} f^{'} = f (b) - f (a)$ ; and a bounded derivative makes $f$ Lipschitz)

Proof

1.1A1F1F2F3givenalgebra

Set $h = x - y$ and use translation invariance in [F2] and Tonelli [F3] on the nonnegative integrand. This gives $[f]_{1 / 2, 2}^{2} = \int_{R^{2}} \frac{∥ f (\cdot + h) - f (\cdot) ∥_{2}^{2}}{∣ h ∣^{3}} d h .$ For each $h$ , Plancherel and the translation formula [F1]–[F2] express the squared norm in the integrand as $\int_{R^{2}} ∣ e^{2 π i ξ \cdot h} - 1 ∣^{2} ∣ \hat{f} (ξ) ∣^{2} d ξ$ .

2.1A1F1F2F3F5F90F91step 1.1algebra

Tonelli [F3] now yields $[f]_{1 / 2, 2}^{2} = \int_{R^{2}} ∣ \hat{f} (ξ) ∣^{2} J (ξ) d ξ, J (ξ) = \int_{R^{2}} \frac{∣ e^{2 π i ξ \cdot h} - 1 ∣^{2}}{∣ h ∣^{3}} d h .$ If $ξ = 0$ , then $J (ξ) = 0$ . If $ξ \neq 0$ , rotate $h$ so that $ξ \cdot h = ∣ ξ ∣ h_{1}$ , then substitute $z = ∣ ξ ∣ h$ using [F5]; the Jacobian is $∣ ξ ∣^{- 2}$ and $∣ h ∣^{- 3} = ∣ ξ ∣^{3} ∣ z ∣^{- 3}$ , so $J (ξ) = c_{*} ∣ ξ ∣$ with $c_{*} = \int_{R^{2}} ∣ e^{2 π i z_{1}} - 1 ∣^{2} ∣ z ∣^{- 3} d z$ . This constant is finite: for $∣ z ∣ \leq 1$ , $∣ e^{2 π i z_{1}} - 1 ∣ \leq 2 π ∣ z ∣$ , and for $∣ z ∣ > 1$ it is at most $2$ ; polar integration gives finite bounds $C \int_{0}^{1} d r$ and $C \int_{1}^{\infty} r^{- 2} d r$ . It is positive because the numerator is positive on a nonempty open set.

3.1F4step 2.1algebra∎

Substitution of $J (ξ) = c_{*} ∣ ξ ∣$ into step 2.1 gives the exact seminorm identity. By [F4], the Bessel norm is the weighted Fourier norm; for every $r \geq 0$ , $(1 + 4 π^{2} r^{2})^{1 / 2}$ is bounded above and below by positive constants times $1 + r$ . Hence that norm is equivalent to $∥ f ∥_{2}^{2} + \int ∣ ξ ∣ ∣ \hat{f} (ξ) ∣^{2} d ξ$ , and step 2.1 proves the asserted equivalence. Equivalent norms have the same Cauchy sequences and completion classes, proving the final claim.

Depends on

Used by

Dependency tree · two levels

119 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

Martin Costabel, Boundary Integral Operators on Lipschitz Domains: Elementary Results (1988) (standard reference, not scraped)
Francisco-Javier Sayas, First Steps in the Boundary Element Method (2015 lecture notes) (standard reference, not scraped)