TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)

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.

Uniform RT0/P0 divergence lift and inf-sup bound

Statement

Assume Countable Choice, a bounded connected Lipschitz polyhedral $D$ in dimension two or three, and a shape-regular conforming mesh. Let $C_{I}$ be the mesh-independent constant in the RT0 interpolation estimate and let $L$ be a coordinate-slab width for $D$ . If $B_{D}$ is the actual right inverse of Divergence right inverse on bounded connected Lipschitz domains, define $S_{h} q_{h} : = I_{h} B_{D} q_{h}, C_{R} : = C_{I} C_{d i v} (L + diam D) .$ Then $S_{h} : Q_{h} \to V_{h}$ is a linear right inverse of divergence and $∥ S_{h} q_{h} ∥_{L^{2} (D)} \leq C_{R} ∥ q_{h} ∥_{L^{2} (D)}$ . Consequently $∥ S_{h} q_{h} ∥_{H (div)} \leq \sqrt{1 + C_{R}^{2}} ∥ q_{h} ∥_{2}$ . When $Q_{h} \neq {0}$ , the RT0/P0 inf-sup constant satisfies $β_{h} \geq (1 + C_{R}^{2})^{- 1 / 2}$ uniformly in mesh size.

Facts & Assumptions

Given: Countable Choice, $D$ , a shape-regular mesh, and $q_{h} \in Q_{h}$ .

[A1]

Countable Choice is inherited through the continuous divergence-lift and interpolation suppliers. (The Axiom of Countable Choice ( ${A C}_{ω}$ ))

[F1]

$B_{D} q_{h} \in H_{0}^{1} (D; R^{d})$ , $div B_{D} q_{h} = q_{h}$ , and $∥ \nabla B_{D} q_{h} ∥_{2} \leq C_{d i v} ∥ q_{h} ∥_{2}$ . (Divergence right inverse on bounded connected Lipschitz domains)

[F2]

$I_{h}$ maps H1 fields to RT0, commutes with divergence cell averages, is zero-normal on H1_0 inputs, and obeys $∥ I_{h} w ∥_{2} \leq C_{I} (∥ w ∥_{2} + h ∥ \nabla w ∥_{2})$ . (Boundedness and divergence commutation of RT0 interpolation)

[F3]

$∥ B_{D} q_{h} ∥_{2} \leq L ∥ \nabla B_{D} q_{h} ∥_{2}$ for the chosen slab width. (A bounded-domain Poincare inequality for H1-zero fields)

Proof

1.1A1F1F2construct

Since $q_{h}$ is cellwise constant, its cell average is itself. By [F1] and the commuting identity [F2], $div S_{h} q_{h} = P_{0} (div B_{D} q_{h}) = q_{h}$ . The input $B_{D} q_{h}$ is in H1_0, so [F2] gives $S_{h} q_{h} \in V_{h}$ . Linearity follows from the linear divergence lift and interpolation.

2.1F1F2F3step 1.1algebra

The stability estimate [F2] and [F1], [F3] imply $∥ S_{h} q_{h} ∥_{2} \leq C_{I} C_{d i v} (L + h) ∥ q_{h} ∥_{2} \leq C_{R} ∥ q_{h} ∥_{2},$ because $h \leq diam D$ . The right-inverse identity from step 1.1 then yields $∥ S_{h} q_{h} ∥_{H (div)}^{2} = ∥ S_{h} q_{h} ∥_{2}^{2} + ∥ q_{h} ∥_{2}^{2} \leq (1 + C_{R}^{2}) ∥ q_{h} ∥_{2}^{2}$ .

3.1F2step 1.1step 2.1algebra∎

For nonzero $q_{h} \in Q_{h}$ , take $v_{h} = - S_{h} q_{h}$ . Then $b (v_{h}, q_{h}) = ∥ q_{h} ∥_{2}^{2}$ and $∥ v_{h} ∥_{H (div)} \leq \sqrt{1 + C_{R}^{2}} ∥ q_{h} ∥_{2}$ by step 2.1. This admissible test gives the lower bound on the supremum for each $q_{h}$ ; taking the infimum over nonzero $q_{h}$ proves the stated $β_{h}$ bound. The constants depend on $D$ , its chosen continuous lift, and the shape bound, but not on $h$ .

Depends on

Used by

Dependency tree · two levels

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