Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

A direct Strang-type energy error estimate for SIPDG

Statement

Assume Countable Choice and the mesh, coefficient, penalty, and exact-solution hypotheses of Exact consistency of the symmetric interior-penalty DG form and SIPDG coercivity above the discrete inverse-trace threshold. Let uh∈Vhbr be the unique discrete solution, so ah(uh,vh)=ℓh(vh) for every vh∈Vhbr. Let Cflux be the constant in Discrete inverse-trace bound for SIPDG coefficient fluxes and put CB:=2+2γ−1/2. Then for every wh∈Vhbr, ∥u−uh∥DG≤(1+2CB1+Cflux)∥u−wh∥DG,∗. Consequently ∥u−uh∥DG≤(1+2CB1+Cflux)inf⁡wh∈Vhbr∥u−wh∥DG,∗. The augmented approximation term retains the face-flux trace needed to bound the SIP consistency terms; no approximation rate is asserted without a separate bound on that term.

Facts & Assumptions

Given: Countable Choice; the exact solution u and discrete solution uh satisfying the equations in the Statement; the coercivity threshold; and the mesh-dependent expressions ∥⋅∥DG and ∥⋅∥DG,∗.

[F1]

The form and energy expressions are defined on Dh, which contains the cellwise H2 exact solution and the broken polynomials. (Symmetric interior-penalty DG form and energy seminorm)

[F2]

For γ≥4Cflux, ah(vh,vh)≥12∥vh∥DG2 on Vhbr. (SIPDG coercivity above the discrete inverse-trace threshold)

[F3]

For the stated piecewise H2 exact solution, ah(u,vh)=ℓh(vh) for every vh∈Vhbr. (Exact consistency of the symmetric interior-penalty DG form)

[F4]

For every zh∈Vhbr, ∑FhF∥qF(zh)∥L2(F)2≤Cflux∑K∫K∇zhTAK∇zh. (Discrete inverse-trace bound for SIPDG coefficient fluxes)

[F5]

The form obeys ∣ah(v,w)∣≤CB∥v∥DG,∗∥w∥DG,∗ on Dh, and ∥⋅∥DG is a seminorm there. (Boundedness of the SIPDG form in the augmented norm)

[F6]

Countable Choice is used by the inverse-trace and physical-simplex Green suppliers [F3]–[F4]. (The Axiom of Countable Choice (ACω))

Proof

1.1F1F5given

The exact solution u is cellwise H2 and uh,wh are broken polynomials, so u−wh and uh−wh belong to Dh. The boundedness constant for their form pairing is CB=2+2γ−1/2 by [F5].

2.1F1F2F3F4F5F6step 1.1givenalgebra

Fix wh and set zh=uh−wh. If ∥zh∥DG=0, then ∥zh∥DG≤2CB1+Cflux∥u−wh∥DG,∗ is immediate. Otherwise, coercivity [F2], the discrete equation and exact consistency [F3] give 12∥zh∥DG2≤ah(zh,zh)=ah(u−wh,zh). By [F4] and ∑K∫K∇zhTAK∇zh≤∥zh∥DG2, ∥zh∥DG,∗≤1+Cflux∥zh∥DG. Apply [F5] and step 1.1 to obtain 12∥zh∥DG2≤CB1+Cflux∥u−wh∥DG,∗∥zh∥DG. Dividing by ∥zh∥DG>0 proves ∥zh∥DG≤2CB1+Cflux∥u−wh∥DG,∗.

3.1F5step 2.1algebra∎

Since ∥⋅∥DG is a seminorm on Dh by [F5], its triangle inequality and step 2.1 give ∥u−uh∥DG≤∥u−wh∥DG+∥wh−uh∥DG≤(1+2CB1+Cflux)∥u−wh∥DG,∗. This holds for every wh, so taking the infimum proves both assertions.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

20 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