LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck pass

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.

Support, integrability, and divergence identity for the Bogovskii kernel

Statement

Assume Countable Choice. Let $U, ω$ and $B_{U}$ be as in The Bogovskii integral on a star-shaped set. For $f \in C_{c}^{\infty} (U)$ , write $G (x, y) = (x - y) \int_{0}^{1} ω (y + (x - y) / t) t^{- d - 1} d t$ . Then $B_{U} f (x) = \int_{U} G (x, y) f (y) d y$ defines an $L^{2}$ field supported in a compact subset of $U$ . Writing $K (x, y) = ∣ G (x, y) ∣$ and $(K_{U} g) (x) : = \int_{U} K (x, y) g (y) d y$ , the majorant $K_{U} ∣ f ∣$ is also in $L^{2} (U)$ , and $K_{U}$ has a finite $L^{2}$ bound. Moreover, $div B_{U} f = f - ω \int_{U} f$ in distributions on $R^{d}$ . In particular, mean-zero input has divergence $f$ .

Facts & Assumptions

Given: Countable Choice; bounded open $U$ star-shaped with respect to the support ball of $ω \in C_{c}^{\infty}$ , $\int ω = 1$ , and $f \in C_{c}^{\infty} (U)$ .

[A1]

Countable Choice is required by the affine Lebesgue change-of-variables supplier [F2]. (The Axiom of Countable Choice ( ${A C}_{ω}$ ))

[F1]

The Bogovskii vector kernel is $G (x, y) = (x - y) \int_{0}^{1} ω (y + (x - y) / t) t^{- d - 1} d t$ . (The Bogovskii integral on a star-shaped set)

[F2]

Translation preserves Lebesgue measurability and measure, and the linear map $z \mapsto t z$ scales measure by $t^{d}$ for $t > 0$ . Composing this dilation with translation by $(1 - t) y$ gives $x = y + t (z - y)$ and $d x = t^{d} d z$ . The integral substitution follows first for indicator functions, then for nonnegative simple functions and their increasing limits, and for integrable signed functions by positive and negative parts. (Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation, 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)

[F3]

Tonelli and Fubini allow the nonnegative/absolutely integrable changes of order in the kernel and test-function calculations. (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product, Fubini's theorem for L^1 functions on a sigma-finite product)

[F4]

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

[F5]

A continuous image of a compact set is compact. (A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism)

[F6]

Distributional divergence is defined by $⟨ div u, η ⟩ = - \int u \cdot \nabla η$ . (Distributional derivative)

[F7]

Closed bounded subsets of Euclidean space are compact. (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line)

Proof

1.1F1givenF5F7

If the integrand in [F1] is nonzero, $z = y + (x - y) / t \in supp ω$ , so $x = (1 - t) y + t z$ . Star-shapedness puts every such $x$ in $U$ . The sets $supp f$ , $supp ω$ and $[0, 1]$ are closed and bounded, so their product is closed and bounded in Euclidean space and compact by [F7]. Its image under the continuous map $(y, z, t) \mapsto (1 - t) y + t z$ is compact by [F5]. Star-shapedness puts the image inside $U$ .

1.2F1givenalgebra

Assign $G (x, x) = 0$ on the null diagonal. If the kernel integrand is nonzero and $r = ∣ x - y ∣ > 0$ , then $r / t = ∣ z - y ∣ \leq R : = diam (U)$ . Thus $t \geq r / R$ and $∣ G (x, y) ∣ \leq r ∥ ω ∥_{\infty} \int_{r / R}^{1} t^{- d - 1} d t \leq C r^{1 - d}$ . For any fixed $x$ , decompose $0 < ∣ x - y ∣ \leq R$ into annuli $2^{- n - 1} R < ∣ x - y ∣ \leq 2^{- n} R$ ; on the $n$ th annulus, $r^{1 - d} \leq (2^{- n - 1} R)^{1 - d}$ and its measure is at most $(2^{1 - n} R)^{d}$ . The annular integral is therefore at most $C R 2^{- n}$ , whose sum is finite. The same estimate with $x, y$ interchanged proves both $\sup_{x} \int_{U} ∣ G (x, y) ∣ d y < \infty$ and $\sup_{y} \int_{U} ∣ G (x, y) ∣ d x < \infty$ .

2.1F1F3F4step 1.1step 1.2

For the nonnegative kernel $K = ∣ G ∣$ , Cauchy–Schwarz gives $∣ \int K (x, y) f (y) d y ∣^{2} \leq (\int K (x, y) d y) (\int K (x, y) ∣ f (y) ∣^{2} d y)$ . Integrating in $x$ and using the two finite bounds in step 1.2 gives $∥ K_{U} ∣ f ∣ ∥_{2}^{2} \leq M_{x} M_{y} ∥ f ∥_{2}^{2}$ , where $M_{x} = \sup_{x} \int_{U} K (x, y) d y$ and $M_{y} = \sup_{y} \int_{U} K (x, y) d x$ . The vector field is componentwise dominated by this majorant, so it is in $L^{2}$ and has the support in step 1.1.

2.2A1F1F2F3step 1.2

Let $η \in C_{c}^{\infty} (R^{d})$ . Using [F2], Fubini (justified by step 1.2, the compact support of $f$ , and boundedness of $\nabla η$ ), and $x = y + t (z - y)$ gives $\int_{R^{d}} G (x, y) \cdot \nabla η (x) d x = \int ω (z) (z - y) \cdot \int_{0}^{1} \nabla η (y + t (z - y)) d t d z = \int ω (z) (η (z) - η (y)) d z .$ The last equality is the one-variable fundamental theorem along the segment.

3.1givenF6step 2.2∎

By the definition of distributional divergence, step 2.2 says ${div}_{x} G (\cdot, y) = δ_{y} - ω$ ; integrating against $f (y)$ yields $div B_{U} f = f - ω \int_{U} f$ . If $\int f = 0$ , the second term vanishes.

Depends on

Used by

Cited to discharge well-definedness by The Bogovskii integral on a star-shaped set.

Dependency tree · two levels

108 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)