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.
A scale integral estimate for mean-zero kernels
Statement
Assume Countable Choice. Let , , , and let with . For put . Then for every and every , with independent of and of .
Facts & Assumptions
Given: Countable Choice; , , ; a kernel with and support in a ball of radius ; the scaled kernels for ; a function ; and .
Assume Countable Choice. For complex and , the convolution exists absolutely a.e., defines a measurable class independent of representatives, and satisfies . (Complex translation, convolution, approximate identities, and mollification)
Holder's inequality: for conjugate exponents and measurable with , , . (Holder's inequality for integrals, including the endpoint cases)
Assume Countable Choice. For nonnegative measurable functions on a product of sigma-finite measure spaces the double integral equals the iterated integrals with measurable section integrals. (Tonelli and Fubini for the completed product, with only almost-everywhere section measurability, The Axiom of Countable Choice ())
The Euclidean seminorm is the extended double integral , and it is comparable to the sum of coordinate-direction integrals: , and also , with . (The Gagliardo--Slobodeckij space on Euclidean space, The coordinate-direction form of the Slobodeckij seminorm)
Proof
The difference form and the pointwise ball estimate. For one has by the change of variables , so for a.e. the convolution equals , the subtracted term vanishing; this is well defined for a.e. by [F1] and the a.e. finiteness of . Since and , the absolute value is at most , and Holder [F2] over that ball gives .
Integrating in and . Integrating the bound of step 1.1 over and using Tonelli [F3] to exchange the - and -integrals gives , where and . Multiplying by and integrating over , another application of Tonelli [F3] gives ; the inner integral vanishes for and is at most , so the left-hand side is at most , a bound independent of .
Identifying the weight and invoking the coordinate-direction form. The substitution together with translation invariance of Lebesgue measure and Tonelli [F3] gives , because at . By the comparability clause of [F4], (again ). Step 2.1 first gives the bound by the seminorm. Combining with both directions of [F4] gives both displayed inequalities, with the second constant independent of and of .
Source notes
Mironescu's estimates (11.32)-(11.37) (printed pp. 78-79) bound a mean-zero kernel of scale by on the ball and apply Holder over the ball; Kampanou's estimates leading to (3.6)-(3.7) (printed pp. 24-26) decompose the difference and apply Tonelli; Gagliardo's direct and inverse estimates (printed pp. 290-300) and Schikorra's Section V.2 (printed pp. 98-100) use scaled kernels with vanishing moments of exactly this form. The proof above keeps the -upper limit through both integrations and drops it only into a convergent tail integral, which is why the final constant does not depend on .
Depends on
- The coordinate-direction form of the Slobodeckij seminorm
- Complex translation, convolution, approximate identities, and mollification
- Holder's inequality for integrals, including the endpoint cases
- Tonelli and Fubini for the completed product, with only almost-everywhere section measurability
- The Gagliardo--Slobodeckij space on Euclidean space
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- Minkowski's integral inequality
Used by
Dependency tree · two levels
55 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
- Petru Mironescu, Fine properties of functions: an introduction (Internet Archive capture of the HAL deposit cel-00747696) (standard reference, not scraped)
- Maria Kampanou, Trace Theorems for Sobolev Spaces (master's thesis, National and Kapodistrian University of Athens, July 2018) (standard reference, not scraped)
- Emilio Gagliardo, Caratterizzazioni delle tracce sulla frontiera relative ad alcune classi di funzioni in $n$ variabili, Rend. Sem. Mat. Univ. Padova 27 (1957), 284-305 (standard reference, not scraped)
- Armin Schikorra, Partial Differential Equations (University of Pittsburgh, version 4 December 2019) (standard reference, not scraped)
- Petru Mironescu, Fine properties of functions: an introduction (author-hosted 89-page edition) (standard reference, not scraped)