LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedprecheck 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 interval stability of the phase-field L2 projector

Statement

Let $Ω = (0, L)$ and let $V_{h}$ be the conforming interval space in No-flux finite-volume and conforming realizations for phase fields, with center spacing $h$ . Let $I_{h} v$ interpolate the absolutely-continuous representative of $v \in H^{1} (0, L)$ at the centers and extend it constantly to the two boundary half-cells. Let $P_{h}$ be the exact $L^{2}$ -orthogonal projection onto $V_{h}$ . There is a constant $C$ independent of $h$ such that $∥ I_{h} v ∥_{H^{1}} \leq C ∥ v ∥_{H^{1}}, ∥ v - I_{h} v ∥_{L^{2}} \leq C h ∥ v^{'} ∥_{L^{2}}, ∥ P_{h} v ∥_{H^{1}} \leq C ∥ v ∥_{H^{1}} .$ In addition, $∥ P_{h} v - v ∥_{L^{2}} \leq C h ∥ v^{'} ∥_{L^{2}}$ for every $v \in H^{1} (0, L)$ , $P_{h} v \to v$ in $H^{1} (0, L)$ for every $v \in H^{1} (0, L)$ , and $P_{h} g \to g$ in $L^{2} (0, L)$ for every $g \in L^{2} (0, L)$ as $h \to 0$ .

Facts & Assumptions

Given: A bounded interval, a uniform center mesh, and the definitions of $V_{h}$ , $I_{h}$ , and $P_{h}$ in the statement.

[F1]

No-flux finite-volume and conforming realizations for phase fields: $V_{h}$ consists of continuous functions affine between centers and constant on the boundary half-cells, so its $L^{2}$ inner product is positive definite and $P_{h}$ is the orthogonal projection.

[F2]

One-dimensional $W^{1, p}$ functions have unique absolutely continuous representatives: each $H^{1} (0, L)$ class has a unique absolutely-continuous representative on $[0, L]$ with $v (x) - v (y) = \int_{y}^{x} v^{'} (s) d s$ .

[F3]

Assume Countable Choice. For every $g \in L^{2} (0, L)$ and $δ > 0$ there is $q \in C_{c}^{\infty} (0, L)$ with $∥ g - q ∥_{2} < δ$ (Smooth compactly supported functions of an open set are dense in $L^{2}$ ).

[F4]

Every compactly supported smooth function on $(0, L)$ lies in $H^{1} (0, L)$ because its classical derivatives are weak derivatives (Classical derivatives agree with weak derivatives).

[A1]

Assume the Axiom of Choice through [F2] when selecting the canonical representative at the finitely many interpolation nodes; it supplies the Countable Choice hypothesis in [F3].

Proof

1.1A1F1F2givenalgebra

On every segment between adjacent centers, $I_{h} v$ has slope $h^{- 1} \int_{x_{i}}^{x_{i + 1}} v^{'} (s) d s$ , so Cauchy–Schwarz bounds its squared derivative integral by $\int_{x_{i}}^{x_{i + 1}} ∣ v^{'} ∣^{2}$ . It is constant on the boundary half-cells. Summing proves $∥ (I_{h} v)^{'} ∥_{2} \leq ∥ v^{'} ∥_{2}$ . The fundamental-theorem identity in [F2] gives $∣ v (x) - I_{h} v (x) ∣ \leq 2 \sqrt{h} ∥ v^{'} ∥_{L^{2} (K)}$ on each center interval $K$ and the same bound on each boundary half-cell. Squaring and summing proves $∥ v - I_{h} v ∥_{2} \leq C h ∥ v^{'} ∥_{2}$ ; then $∥ I_{h} v ∥_{2} \leq ∥ v ∥_{2} + C h ∥ v^{'} ∥_{2}$ .

1.2F1algebra

For an affine function $w_{h}$ on an interval $J$ of length $h$ with endpoint values $a, b$ , direct integration gives $∥ w_{h}^{'} ∥_{L^{2} (J)}^{2} = (b - a)^{2} / h$ and $∥ w_{h} ∥_{L^{2} (J)}^{2} = h (a^{2} + a b + b^{2}) / 3 \geq h (a^{2} + b^{2}) / 6$ . Hence $∥ w_{h}^{'} ∥_{L^{2} (J)} \leq \sqrt{12} h^{- 1} ∥ w_{h} ∥_{L^{2} (J)}$ . Summing this inequality over the affine segments proves the inverse estimate $∥ w_{h}^{'} ∥_{2} \leq \sqrt{12} h^{- 1} ∥ w_{h} ∥_{2}$ on $V_{h}$ ; the constant boundary segments add no derivative.

2.1F1step 1.1step 1.2algebra

Since $P_{h} I_{h} v = I_{h} v$ and $P_{h}$ is an $L^{2}$ contraction, $∥ P_{h} v - I_{h} v ∥_{2} = ∥ P_{h} (v - I_{h} v) ∥_{2} \leq C h ∥ v^{'} ∥_{2}$ by step 1.1. The triangle inequality with step 1.1 gives $∥ P_{h} v - v ∥_{2} \leq C h ∥ v^{'} ∥_{2}$ . Apply step 1.2 to $P_{h} v - I_{h} v \in V_{h}$ , and then step 1.1, to obtain $∥ (P_{h} v)^{'} ∥_{2} \leq ∥ (I_{h} v)^{'} ∥_{2} + C h^{- 1} ∥ P_{h} v - I_{h} v ∥_{2} \leq C ∥ v^{'} ∥_{2}$ . The $L^{2}$ contraction gives the full $H^{1}$ stability.

3.1step 2.1givenalgebra

If $v \in C^{2} ([0, L])$ , linear interpolation on each interior segment has $H^{1}$ error tending to zero, while on a boundary half-cell the derivative error is bounded by $\sqrt{h} ∥ v^{'} ∥_{\infty}$ . Thus $∥ I_{h} v - v ∥_{H^{1}} \to 0$ . Step 2.1 applied to $v - I_{h} v$ gives $∥ P_{h} v - I_{h} v ∥_{H^{1}} \leq C ∥ v - I_{h} v ∥_{H^{1}} \to 0$ , so $P_{h} v \to v$ in $H^{1}$ .

4.1A1F2F3step 2.1step 3.1givenalgebra

For arbitrary $v \in H^{1} (0, L)$ , let $v^{'}$ be its $L^{2}$ weak derivative and use [F3] to choose $q_{j} \in C_{c}^{\infty} (0, L)$ with $q_{j} \to v^{'}$ in $L^{2}$ . Define $v_{j} (x) = v (0) + \int_{0}^{x} q_{j} (s) d s$ using the representative in [F2]. Then $v_{j} \in C^{\infty} ([0, L])$ and $∥ v_{j}^{'} - v^{'} ∥_{2} = ∥ q_{j} - v^{'} ∥_{2} \to 0$ , while Cauchy--Schwarz gives $∥ v_{j} - v ∥_{2} \leq L ∥ q_{j} - v^{'} ∥_{2}$ . Hence $v_{j} \to v$ in $H^{1}$ . Uniform stability from step 2.1 and smooth convergence from step 3.1 yield $∥ P_{h} v - v ∥_{H^{1}} \leq C ∥ v - v_{j} ∥_{H^{1}} + ∥ P_{h} v_{j} - v_{j} ∥_{H^{1}} + ∥ v_{j} - v ∥_{H^{1}};$ first let $h \to 0$ with $j$ fixed and then let $j \to \infty$ . Thus $P_{h} v \to v$ in $H^{1}$ for every $v \in H^{1} (0, L)$ .

5.1A1F1F3F4step 2.1givenalgebra∎

For $g \in L^{2} (0, L)$ and $δ > 0$ , [F3] gives $q \in C_{c}^{\infty} (0, L) \subset H^{1} (0, L)$ with $∥ g - q ∥_{2} < δ$ . The orthogonal projector is an $L^{2}$ contraction by [F1], and step 2.1 gives $P_{h} q \to q$ in $L^{2}$ . Therefore $∥ P_{h} g - g ∥_{2} \leq 2 ∥ g - q ∥_{2} + ∥ P_{h} q - q ∥_{2},$ so ${lim sup}_{h \to 0} ∥ P_{h} g - g ∥_{2} \leq 2 δ$ . Letting $δ ↓ 0$ proves strong $L^{2}$ convergence for every $g \in L^{2} (0, L)$ .

Depends on

Used by

One-dimensional mesh and time convergence of convex-splitting phase flows Theorem

Dependency tree · two levels

55 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

Christian Clason, Introduction to Finite Element Methods, complete lecture notes, arXiv:1709.08618v2 (standard reference, not scraped)
R. Eymard, T. Gallouët, and R. Herbin, Finite Volume Methods, Handbook of Numerical Analysis, Vol. VII, 2000; complete updated author text (standard reference, not scraped)