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 be real Hilbert spaces and let , be bounded data. Suppose bounded bilinear forms and satisfy for all . Let , be finite-dimensional conforming subspaces, with , , and discrete inf-sup constant . Assume the discrete kernel coercivity for every , where . Put , . The Galerkin system with the same has a unique solution . For any , , define , , , and Then and . In particular the pressure bound retains explicitly; taking infima over gives the corresponding best-approximation bound.
Facts & Assumptions
Given: A continuous solution, nonzero conforming finite-dimensional subspaces , positive discrete inf-sup , boundedness constants , and coercivity on with constant . The discrete equations use the same .
Countable Choice is used through the Babuška–Brezzi/Lax–Milgram solvability theorem for the discrete pair. (The Axiom of Countable Choice ())
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)
The discrete inf-sup bound gives a right inverse of the discrete constraint operator with norm at most . (Hilbert inf-sup gives a bounded constraint right inverse)
Proof
Apply [F1] to with the assumed -coercivity and discrete inf-sup constant . Since the restricted forms are bounded, the Galerkin system with the same has a unique solution .
Fix and set , , , . Subtracting the discrete equations from the continuous equations gives and .
The second identity implies . By [F2] choose with and . Then .
Test the first identity of step 2.1 with . Since , . Discrete-kernel coercivity and boundedness imply, when , ; if this bound is immediate. Therefore .
Since , the first identity of step 2.1 gives . Therefore by step 4.1. Taking the supremum and applying the discrete inf-sup yields . Hence .
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
- Jean-Luc Guermond, MATH 661 Fall 2025, Chapters 49–54 (complete course notes) (standard reference, not scraped)
- Daniele Boffi, Franco Brezzi, Michel Fortin, Mixed Finite Element Methods and Applications (complete textbook) (standard reference, not scraped)