TheoremStatement: 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.

Bounded commuting projection onto the zero-normal RT0 space

Statement

Assume Countable Choice and a shape-regular mesh. Let $P_{0}$ be the cellwise $L^{2}$ -orthogonal projection onto piecewise constants, let $S_{h} : Q_{h} \to V_{h}$ be the stable right inverse above, and put $Z_{h} = {z_{h} \in V_{h} : div z_{h} = 0}$ . There is a linear projection $Π_{h} : H_{0} (div; D) \to V_{h}$ such that $div Π_{h} v = P_{0} div v, ∥ Π_{h} v ∥_{H (div)} \leq C ∥ v ∥_{H (div)},$ where $C$ depends on the domain and mesh shape bound, not mesh size. The construction uses the finite-dimensional $L^{2}$ -orthogonal projection onto $Z_{h}$ and never applies facet moments to rough H(div)-only fields.

Facts & Assumptions

Given: Countable Choice, a shape-regular mesh, and $v \in H_{0} (div; D)$ .

[A1]

Countable Choice is inherited through the H(div) and real $L^{2}$ interfaces; the finite-dimensional projection is constructed below. (The Axiom of Countable Choice ( ${A C}_{ω}$ ))

[F1]

$div v$ has zero mean, so $q_{h} : = P_{0} div v$ belongs to $Q_{h}$ ; $P_{0}$ is an $L^{2}$ contraction and preserves the integral. (Zero mean of the divergence under zero normal trace, Cell averaging is the $L^{2}$ projection onto P0)

[F2]

The right inverse obeys $div S_{h} q_{h} = q_{h}$ , $∥ S_{h} q_{h} ∥_{2} \leq C_{R} ∥ q_{h} ∥_{2}$ , and $∥ S_{h} q_{h} ∥_{H (div)} \leq C_{S} ∥ q_{h} ∥_{2}$ , where $C_{S} = \sqrt{1 + C_{R}^{2}}$ . (Uniform RT0/P0 divergence lift and inf-sup bound)

[F3]

$Z_{h}$ is finite-dimensional, since the mesh is finite and each local RT0 space has dimension $d + 1$ . Real $L^{2}$ has the integral inner product used below. ( $L^{2}$ with the integral pairing is a Hilbert space)

[F4]

The divergencefree members of $V_{h}$ are exactly the discrete kernel $Z_{h}$ . (The RT0/P0 discrete kernel is exactly divergence-free)

Proof

1.1A1F3constructalgebra

If $Z_{h} = {0}$ , set $P_{Z_{h}} = 0$ . Otherwise take a basis $z_{1}, \dots, z_{m}$ of $Z_{h}$ and its Gram matrix $G_{i j} = (z_{j}, z_{i})_{L^{2}}$ . For nonzero $c \in R^{m}$ , $c^{T} G c = ∥ \sum_{j} c_{j} z_{j} ∥_{2}^{2} > 0$ , so $G$ is invertible. For any $r \in L^{2} (D; R^{d})$ , solve $G c = ((r, z_{i})_{L^{2}})_{i = 1}^{m}$ and set $P_{Z_{h}} r = \sum_{j} c_{j} z_{j}$ . This is linear, and $(r - P_{Z_{h}} r, z_{i})_{L^{2}} = 0$ for every basis vector. Thus $r - P_{Z_{h}} r$ is orthogonal to $Z_{h}$ , $P_{Z_{h}} z = z$ for $z \in Z_{h}$ , and $∥ r ∥_{2}^{2} = ∥ P_{Z_{h}} r ∥_{2}^{2} + ∥ r - P_{Z_{h}} r ∥_{2}^{2}$ gives $∥ P_{Z_{h}} r ∥_{2} \leq ∥ r ∥_{2}$ . These conclusions hold also for $Z_{h} = {0}$ .

2.1A1F1F2F4step 1.1constructalgebra

Define $q_{h} = P_{0} div v$ , $r = v - S_{h} q_{h}$ , and let $P_{Z_{h}}$ be the orthogonal projection constructed in step 1.1. Set $Π_{h} v : = S_{h} q_{h} + P_{Z_{h}} r .$ Both terms are in $V_{h}$ , and the second lies in $Z_{h}$ . Thus [F2] and [F4] give $div Π_{h} v = q_{h} = P_{0} div v$ . The cell-average map, $S_{h}$ , and the orthogonal projection are linear, so $Π_{h}$ is linear.

3.1F2F4step 1.1step 2.1algebra

If $v_{h} \in V_{h}$ , then $div v_{h}$ is cellwise constant, so $P_{0} div v_{h} = div v_{h}$ . Consequently $v_{h} - S_{h} (div v_{h}) \in V_{h}$ has zero divergence and lies in $Z_{h}$ by [F4]. Its orthogonal projection is itself; substituting in the formula of step 2.1 gives $Π_{h} v_{h} = v_{h}$ . Hence $Π_{h}$ is a projection.

4.1F1F2step 1.1step 2.1algebra∎

Let $C_{S} = \sqrt{1 + C_{R}^{2}}$ . Since $∥ q_{h} ∥_{2} \leq ∥ div v ∥_{2}$ , [F2] gives $∥ S_{h} q_{h} ∥_{2} \leq C_{R} ∥ q_{h} ∥_{2}$ , hence $∥ r ∥_{2} \leq ∥ v ∥_{2} + C_{R} ∥ q_{h} ∥_{2}$ . Also $∥ P_{Z_{h}} r ∥_{2} \leq ∥ r ∥_{2}$ and its divergence is zero. Therefore [F2] gives $∥ Π_{h} v ∥_{H (div)} \leq C_{S} ∥ q_{h} ∥_{2} + ∥ r ∥_{2} \leq C_{S} ∥ q_{h} ∥_{2} + ∥ v ∥_{2} + C_{R} ∥ q_{h} ∥_{2} \leq (1 + C_{S} + C_{R}) ∥ v ∥_{H (div)} .$ This bound is uniform in mesh size. The formula uses only the $L^{2}$ divergence, the discrete right inverse, and a finite-dimensional $L^{2}$ projection, so no facet trace of $v$ is used.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

35 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 16: Local interpolation in H(div) and H(curl) (I) (standard reference, not scraped)
Daniele Boffi, Franco Brezzi and Michel Fortin, Mixed Finite Element Methods and Applications (standard reference, not scraped)