Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge 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.

Well-definedness of the Slobodeckij seminorm and norm

Statement

Assume Countable Choice. Let d≥1, 0<s<1 and 1≤p<∞.

(i) If g=h almost everywhere on Rd, then [g]s,p=[h]s,p, both possibly infinite.

(ii) The extended quantity [⋅]s,p is a seminorm: [λg]s,p=∣λ∣ [g]s,p and [f+g]s,p≤[f]s,p+[g]s,p for all measurable f,g and all λ∈K.

(iii) If g∈Lp(Rd) and [g]s,p=0, then g=0 almost everywhere; hence ∥⋅∥Ws,p is a norm and Ws,p(Rd) is a vector space. On a set of finite measure the seminorm vanishes on constants, so it is only definite modulo constants there; adding the Lp term removes that ambiguity, and on Rd with p<∞ no nonzero constant is in Lp.

Facts & Assumptions

Given: Countable Choice; d≥1, 0<s<1, 1≤p<∞; the seminorm [g]s,p of The Gagliardo--Slobodeckij space on Euclidean space, an extended nonnegative integral over the completed product measure on Rd×Rd of the integrand ∣g(x)−g(y)∣p∣x−y∣−d−sp, read as 0 on the diagonal.

[F1]

The seminorm is defined by the completed-product integral ∫Rd∫Rd∣g(x)−g(y)∣p∣x−y∣−d−spdx dy, raised to the power 1/p; the diagonal is a null set and the integrand is measurable and nonnegative, so the integral is an element of [0,∞]. (The Gagliardo--Slobodeckij space on Euclidean space)

[F2]

Assume Countable Choice. Tonelli's and Fubini's theorems hold for the completed product of sigma-finite measure spaces: for a nonnegative measurable h the double integral equals both iterated integrals with the section integrals as in the statement, and the section-integral functions are measurable. (Tonelli and Fubini for the completed product, with only almost-everywhere section measurability, The Axiom of Countable Choice (ACω))

[F3]

For a nonnegative measurable u, ∫u dμ=0 if and only if u=0 almost everywhere. (A nonnegative measurable function has integral 0 exactly when it vanishes almost everywhere)

[F4]

Minkowski's integral inequality: for sigma-finite (X,μ), (Y,ν), 1≤r<∞ and measurable F:X×Y→C with ∫Y∥F(⋅,y)∥Lr(X)dν(y)<∞, the function x↦∫Y∣F(x,y)∣dν(y) lies in Lr(X) with norm at most ∫Y∥F(⋅,y)∥Lr(X)dν(y). (Minkowski's integral inequality)

[F5]

Every box between its open and closed forms is Lebesgue measurable with measure the product of the side lengths; in particular λd([0,R]d)=Rd. (A box in Rn with parameters ai≤bi is Lebesgue measurable of measure ∏i<n(bi−ai), whichever of its faces are included)

[F6]

For 1≤p<∞ the quotient Lp norm is well defined on classes and makes Lp a normed space for real scalars, with ∥[f]∥p=∥f∥p. (The Lp norm descends to the quotient and makes Lp a normed space for 1≤p≤∞, The space Lp(μ) as the quotient by null functions)

[F7]

On any measure space, complex Lp classes carry well-defined vector operations and the norm ∥[f]∥p=Np(f) satisfies the triangle inequality. (Complex Holder, Minkowski, and the quotient norm)

Proof

technique · direct
1.1F1F2algebra

Representative independence (i). Let g=h almost everywhere and let N:={x:g(x)≠h(x)}, a Lebesgue-null set. The difference ∣g(x)−g(y)∣p−∣h(x)−h(y)∣p vanishes whenever x∉N and y∉N, so the two integrands differ at most on E:=(N×Rd)∪(Rd×N). Tonelli [F2] applied to the indicator of N×Rd gives (λd×λd)(N×Rd)=∫Rdλd(Rd)1N(x) dx=0, because 1N vanishes off the null set N; the second piece is handled the same way, and λd is sigma-finite. Hence E is null and the two integrals coincide, possibly both infinite, so [g]s,p=[h]s,p.

1.2F1algebra

Homogeneity (ii). For λ∈K one has ∣(λg)(x)−(λg)(y)∣p=∣λ∣p∣g(x)−g(y)∣p pointwise, so the integrals are related by the factor ∣λ∣p and [λg]s,p=∣λ∣[g]s,p; at λ=0 both sides are 0 while for [g]s,p=+∞ and λ≠0 both sides are +∞.

1.3F1F4algebra

Triangle inequality (ii). Put Δg(x,y):=g(x)−g(y). Then [Δf+g](x,y)=Δf(x,y)+Δg(x,y) pointwise, and [⋅]s,p is the Lp norm of Δ⋅ on the sigma-finite measure space (Rd×Rd,μ) with dμ=∣x−y∣−d−spdx dy. If [f]s,p+[g]s,p=+∞ the claim is trivial; otherwise Minkowski's integral inequality [F4] applied with Y={1,2} carrying counting measure and F((x,y),1)=Δf(x,y), F((x,y),2)=Δg(x,y) gives [f+g]s,p≤[f]s,p+[g]s,p.

1.4F1F2F3algebragiven

Zero seminorm forces almost-everywhere constancy (iii). Assume [g]s,p=0, so by [F1] the nonnegative integrand u(x,y):=∣g(x)−g(y)∣p∣x−y∣−d−sp has integral 0; by [F3] u=0 almost everywhere for the completed product measure, and since ∣x−y∣−d−sp>0 off the diagonal, ∣g(x)−g(y)∣=0 for almost every pair (x,y) in the product measure. Applying the Fubini clause of [F2] to the indicator of E:={(x,y):g(x)≠g(y)}, whose product integral is 0, gives a Lebesgue-null set M such that Ex is null for every x∉M. Fix x0∉M with g(x0) finite, possible because g∈Lp is finite almost everywhere; then g(y)=g(x0) for almost every y.

2.1F6F7step 1.2step 1.3step 1.4algebragiven∎

Conclusion (iii) and the norm. By step 1.4 there is c∈K with g=c almost everywhere. If c≠0, then ∫Rd∣g∣p=∣c∣pλd(Rd), and λd(Rd)=+∞ because λd(Rd)≥λd([0,R]d)=Rd for every R>0 by [F5] and monotonicity of a measure; this contradicts g∈Lp. Hence c=0, and [g]s,p=0 forces g=0 almost everywhere. Consequently ∥g∥Ws,p=∥g∥Lp+[g]s,p vanishes only on the zero class, is homogeneous by step 1.2 and the homogeneity of the Lp norm [F6, F7], and satisfies the triangle inequality by step 1.3, the triangle inequality of the Lp norm [F6, F7], and addition of inequalities; Ws,p(Rd) is a vector space because sums and scalar multiples of classes with finite Lp norm and finite seminorm again have Lp norm and seminorm finite by steps 1.2 and 1.3. For the analogue over a finite-measure set Ω the integrand of a constant is identically zero, so the seminorm alone vanishes on constants and only the sum norm is definite; adding the Lp term removes that ambiguity, as claimed.

Source notes

Schikorra, printed p. 96, records the seminorm properties and the vanishing of [f]Ws,p on constants; Gagliardo, printed pp. 286-289, takes the norm on equivalence classes of boundary functions, which is the content of clause (i); Hunter, printed p. 73, describes the trace range as a Besov space carrying the Lp term, the reason the sum norm is used. The proof of clause (iii) above uses only the vanishing criterion for nonnegative integrals and Fubini.

Depends on

Used by

Cited to discharge well-definedness by The Gagliardo--Slobodeckij space on Euclidean space.

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