TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck 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.

Discrete TPFA Rellich compactness and physical weak gradients

Statement

Assume the Axiom of Choice. Let TPFA-admissible meshes also form a regular simplicial companion family, with homogeneous Dirichlet data and fixed $0 < λ_{*} \leq λ_{K} \leq λ^{*}$ . If cell vectors $v_{h}$ satisfy $\sup_{h} ∥ v_{h} ∥_{E_{h}} < \infty$ , there are a subsequence and $v \in H_{0}^{1} (Ω)$ such that $Π_{h} v_{h} \to v$ strongly in $L^{2} (Ω)$ , and the gradients of the conforming companions converge weakly to $\nabla v$ in $L^{2}$ .

There is also an explicit physical weak-gradient reconstruction. Let $P_{K, F}$ be the pyramid with vertex $x_{K}$ and base $\overline{F}$ , ignoring its measure-zero boundary. For $F = K ∣ L$ put $D_{F} = P_{K, F} \cup P_{L, F}$ , fix the normal $n = n_{K, F}$ , and define $G_{h} v = d \frac{v_{L} - v_{K}}{d_{F}} n on D_{F} .$ On a boundary pyramid put $G_{h} v = - d v_{K} n_{K, F} / d_{K, F}$ . These regions partition $Ω$ up to null sets. Along the same subsequence $G_{h} v_{h} ⇀ \nabla v$ in $L^{2} (Ω; R^{d})$ , and $∥ G_{h} v_{h} ∥_{2}^{2} = d (\sum_{F = K ∣ L} \frac{∣ F ∣}{d_{F}} ∣ v_{L} - v_{K} ∣^{2} + \sum_{F \in F_{b d y}} \frac{∣ F ∣}{d_{K, F}} ∣ v_{K} ∣^{2}) \leq \frac{d}{λ_{*}} ∥ v_{h} ∥_{E_{h}}^{2} .$ The dimension factor $d$ is essential. This physical gradient differs from the face-copy bookkeeping gradient in the TPFA Definition; no identification of that separate copy space with $Ω$ is asserted.

Facts & Assumptions

Given: AC, the stated refining meshes, positive coefficient bounds, and energy-bounded zero-boundary cell states.

[F1]

Orthogonal TPFA diffusion with harmonic face transmissibility gives $d_{F} = d_{K, F} + d_{L, F}$ and $λ_{*} \leq λ_{F}^{h a r m} \leq λ^{*}$ , so its energy is uniformly equivalent to the unweighted face energy.

[F2]

Finite-volume companions, mean tests and weak-gradient closure bounds companions in $W_{0}^{1, 2}$ and their $L^{2}$ distance from cell states by $C h D_{h, 2}$ . The subcritical W0 one p embedding into L2 gives compactness of $H_{0}^{1} \to L^{2}$ ; reflexive weak subsequences are supplied by Reflexivity of Lp for one less p less infinity and Reflexivity is equivalent to weak subsequential compactness of bounded sequences. The gradient-closed-range argument is also proved in Weak compactness of bounded space-time Sobolev gradients.

[F3]

Finite-volume families with a regular simplicial companion gives convex cells, fans, a uniformly bounded face count and $diam K \leq h$ .

[F4]

Under the assumed AC, The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter supplies the ultrafilter lemma, AC implies DC implies countable choice supplies DC and Countable Choice, and Hahn-Banach dominated extension theorem for real vector spaces supplies HB. Thus the choice hypotheses of both weak-subsequence suppliers in [F2] are discharged.

Proof

1.1F1givenconstructalgebra

Assign the interior face value $v_{F} = (d_{L, F} v_{K} + d_{K, F} v_{L}) / d_{F}$ and the boundary face value zero. Then $v_{F} - v_{K} = d_{K, F} (v_{L} - v_{K}) / d_{F}$ and $v_{F} - v_{L} = - d_{L, F} (v_{L} - v_{K}) / d_{F}$ . Summing both incident terms gives $D_{h, 2} (v)^{2} = \sum_{F = K ∣ L} ∣ F ∣ ∣ v_{L} - v_{K} ∣^{2} / d_{F} + \sum_{F \in F_{b d y}} ∣ F ∣ ∣ v_{K} ∣^{2} / d_{K, F}$ . Thus [F1] bounds $D_{h, 2}$ by $λ_{*}^{- 1 / 2} ∥ v ∥_{E_{h}}$ .

2.1F2F4step 1.1given

By [F2], the companions are bounded in $H_{0}^{1}$ and have a subsequence converging strongly in $L^{2}$ . Apply the space-time gradient-compactness lemma in [F2] to these companions as constant-in-time functions on $(0, 1)$ , with $p = 2$ and $H = L^{2} (Ω)$ . It identifies the strong limit as some $v \in H_{0}^{1}$ and gives weak convergence of the companion gradients to $\nabla v$ ; testing against functions constant in time gives the spatial weak convergence. Their $L^{2}$ distance from $Π_{h} v_{h}$ tends to zero by $h \to 0$ and step 1.1. This proves the claimed strong state convergence and companion-gradient assertion.

2.2F1F3step 1.1algebra

Convexity and the cell point in the interior make each cell the union of its face pyramids with disjoint interiors. Orthogonality makes their volumes $∣ P_{K, F} ∣ = ∣ F ∣ d_{K, F} / d$ , so $∣ D_{F} ∣ = ∣ F ∣ d_{F} / d$ . Multiplying each squared reconstruction value by its physical region volume gives exactly the displayed norm identity, and [F1] proves its bound.

3.1F1F3step 1.1step 2.2algebra

Let $ϕ$ be any smooth vector field on a neighborhood of $\overline{Ω}$ , and write $ϕ_{F}$ for its face mean. The face-oriented finite sum $\sum_{F = K ∣ L} ∣ F ∣ (v_{L} - v_{K}) n_{K, F} \cdot ϕ_{F} - \sum_{F \in F_{b d y}} ∣ F ∣ v_{K} n_{K, F} \cdot ϕ_{F}$ is exactly $- \int_{Ω} Π_{h} v div ϕ$ , by the divergence formula in each cell and face cancellation. Replacing each $ϕ_{F}$ by the mean of $ϕ$ over the corresponding diamond or boundary pyramid changes this sum by at most $C h ∥ \nabla ϕ ∥_{\infty} \sum_{F} ∣ F ∣ ∣ Δ_{F} v ∣$ . Cauchy–Schwarz bounds that last face sum by $D_{h, 2} (v) (\sum_{F} ∣ F ∣ d_{F})^{1 / 2}$ , taking boundary $d_{F} = d_{K, F}$ . The second factor equals $(d ∣ Ω ∣)^{1 / 2}$ . By step 2.2 the modified sum is $\int G_{h} v \cdot ϕ$ . Hence the weak-gradient defect tends to zero.

4.1F2F4step 2.1step 2.2step 3.1∎

The norm bound in step 2.2 and [F2, F4], applied successively to the $d$ scalar $L^{2}$ coordinates, supply a weakly convergent subsequence of physical gradients. Steps 2.1 and 3.1 identify its distributional limit as $\nabla v$ . Smooth compactly supported tests determine the $L^{2}$ field uniquely, so every weak subsequence on the extracted state subsequence has that limit, giving the asserted weak convergence.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

66 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

Jérôme Droniou, Finite volume schemes for diffusion equations: introduction to and review of modern methods, 2014 (standard reference, not scraped)