LemmaStatement: AI-adaptedProof: 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.

The RT0/P0 discrete kernel is exactly divergence-free

Statement

Assume Countable Choice and the mesh conventions of Affine simplicial meshes and RT/BDM spaces. With $V_{h} = {RT}_{0} (T_{h}) \cap H_{0} (div; D)$ , $Q_{h} = P_{0} (T_{h}) \cap L_{0}^{2} (D)$ and $b (v_{h}, q_{h}) = - \int_{D} q_{h} div v_{h}$ , the discrete kernel $Z_{h} : = {v_{h} \in V_{h} : b (v_{h}, q_{h}) = 0 for every q_{h} \in Q_{h}}$ is exactly ${v_{h} \in V_{h} : div v_{h} = 0}$ .

Facts & Assumptions

Given: A conforming mesh, the spaces $V_{h}, Q_{h}$ , and $v_{h} \in V_{h}$ .

[A1]

Countable Choice is inherited from the zero-normal trace and Sobolev interfaces. (The Axiom of Countable Choice ( ${A C}_{ω}$ ))

[F1]

The divergence of an H(div) field with zero normal trace has zero integral. (Zero mean of the divergence under zero normal trace)

[F2]

By definition, $V_{h}$ consists of global H(div) fields whose cell restrictions are RT0; their cellwise divergence is constant, and membership in $V_{h}$ includes zero normal trace. (Affine simplicial meshes and RT/BDM spaces, Zero-normal-trace H(div) space)

Proof

1.1A1givenF1F2

By [F2], $div v_{h}$ is cellwise constant; by [F1], its global mean is zero. Thus $div v_{h} \in Q_{h}$ .

2.1givenstep 1.1algebracases∎

If $v_{h} \in Z_{h}$ , test its defining orthogonality with the admissible choice $q_{h} = div v_{h}$ from step 1.1. Then $0 = b (v_{h}, q_{h}) = - ∥ div v_{h} ∥_{L^{2} (D)}^{2}$ , so its divergence vanishes in $L^{2}$ . Conversely, if $div v_{h} = 0$ , the defining integral $b (v_{h}, q_{h})$ is zero for every $q_{h} \in Q_{h}$ . This proves the equality, including the case $Q_{h} = {0}$ .

Depends on

Used by

Dependency tree · two levels

16 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

Jean-Luc Guermond, MATH 661 Fall 2025, Part III Chapter 14: H(div) finite elements (standard reference, not scraped)
Daniele Boffi, Franco Brezzi and Michel Fortin, Mixed Finite Element Methods and Applications (standard reference, not scraped)