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

Mixed Galerkin error bound retaining beta_h

Statement

Assume Countable Choice. Let V,Q be real Hilbert spaces and let F∈V′, G∈Q′ be bounded data. Suppose bounded bilinear forms a,b and (u,p)∈V×Q satisfy a(u,v)+b(v,p)=F(v),b(u,q)=G(q) for all v∈V,q∈Q. Let Vh⊂V, Qh⊂Q be finite-dimensional conforming subspaces, with Vh≠{0}, Qh≠{0}, and discrete inf-sup constant βh:=inf⁡qh≠0sup⁡vh≠0b(vh,qh)/(∥vh∥V∥qh∥Q)>0. Assume the discrete kernel coercivity a(vh,vh)≥α∗∥vh∥V2 for every vh∈Zh:={wh:b(wh,qh)=0 for all qh∈Qh}, where α∗>0. Put Ma=∥a∥, Mb=∥b∥. The Galerkin system with the same F,G has a unique solution (uh,ph). For any wh∈Vh, rh∈Qh, define δu=∥u−wh∥V, δp=∥p−rh∥Q, Rh=βh−1Mbδu, and Uh=δu+α∗−1{Ma(δu+Rh)+Mbδp}+Rh, Ph=δp+βh−1{Ma(Uh+δu)+Mbδp}. Then ∥u−uh∥V≤Uh and ∥p−ph∥Q≤Ph. In particular the pressure bound retains βh−1 explicitly; taking infima over wh,rh gives the corresponding best-approximation bound.

Facts & Assumptions

Given: A continuous solution, nonzero conforming finite-dimensional subspaces Vh,Qh, positive discrete inf-sup βh, boundedness constants Ma,Mb, and coercivity on Zh with constant α∗. The discrete equations use the same F,G.

[A1]

Countable Choice is used through the Babuška–Brezzi/Lax–Milgram solvability theorem for the discrete pair. (The Axiom of Countable Choice (ACω))

[F1]

On any real Hilbert pair, coercivity on the constraint kernel and a positive inf-sup constant give unique mixed solvability. (Babuska-Brezzi solvability by kernel coercivity and inf-sup)

[F2]

The discrete inf-sup bound gives a right inverse of the discrete constraint operator with norm at most βh−1. (Hilbert inf-sup gives a bounded constraint right inverse)

Proof

1.1A1F1given

Apply [F1] to Vh,Qh with the assumed Zh-coercivity and discrete inf-sup constant βh. Since the restricted forms are bounded, the Galerkin system with the same F,G has a unique solution (uh,ph).

2.1A1givenstep 1.1

Fix wh,rh and set θu=wh−uh, θp=rh−ph, ηu=u−wh, ηp=p−rh. Subtracting the discrete equations from the continuous equations gives a(θu,vh)+b(vh,θp)=−a(ηu,vh)−b(vh,ηp) and b(θu,qh)=−b(ηu,qh).

3.1A1F2step 2.1

The second identity implies ∥Bhθu∥Q≤Mbδu. By [F2] choose ru∈Vh with Bhru=Bhθu and ∥ru∥V≤Rh. Then zh=θu−ru∈Zh.

4.1givenstep 2.1step 3.1

Test the first identity of step 2.1 with zh. Since b(zh,θp)=0, a(zh,zh)=−a(ηu,zh)−b(zh,ηp)−a(ru,zh). Discrete-kernel coercivity and boundedness imply, when zh≠0, ∥zh∥≤α∗−1{Ma(δu+Rh)+Mbδp}; if zh=0 this bound is immediate. Therefore ∥u−uh∥≤∥ηu∥+∥zh∥+∥ru∥≤Uh.

5.1A1F2algebrastep 2.1step 4.1∎

Since θu+ηu=u−uh, the first identity of step 2.1 gives b(vh,θp)=−a(u−uh,vh)−b(vh,ηp). Therefore ∣b(vh,θp)∣≤[MaUh+Mbδp]∥vh∥ by step 4.1. Taking the supremum and applying the discrete inf-sup yields ∥θp∥≤βh−1(MaUh+Mbδp)≤βh−1{Ma(Uh+δu)+Mbδp}. Hence ∥p−ph∥≤δp+∥θp∥≤Ph.

Depends on

Used by

Dependency tree · two levels

11 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