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

Pressure Schur equivalence from inf-sup, continuity, and stiffness scaling

Statement

Let V,Q be finite-dimensional real inner-product spaces with norms ∥⋅∥V,∥⋅∥Q. Let a(v,w)=vTAw be symmetric positive definite, and let b(v,q)=qTBv be a bilinear constraint form, represented by the matrices in Symmetric saddle-point system, Schur complement, and block preconditioners. Suppose that, for constants α,Λ,Cb,β>0, α∥v∥V2≤a(v,v)≤Λ∥v∥V2,∣b(v,q)∣≤Cb∥v∥V∥q∥Q,sup⁡v≠0∣b(v,q)∣∥v∥V≥β∥q∥Q. If MQ is the pressure mass matrix for ∥⋅∥Q, then the positive Schur matrix S=BA−1BT satisfies, for every q∈Q, β2ΛqTMQq≤qTSq≤Cb2αqTMQq. Thus pressure-mass Schur equivalence is conditional on the actual inf-sup, continuity, and velocity stiffness scalings shown here.

Facts & Assumptions

Given: Finite-dimensional real spaces V,Q, an SPD velocity matrix A, a constraint matrix B, a pressure mass matrix MQ, and the positive constants in the statement.

[F1]

The saddle matrix, its velocity and constraint blocks, and the pressure Schur matrix S=BA−1BT use the conventions of Symmetric saddle-point system, Schur complement, and block preconditioners.

[F2]

The positive-definite bilinear form a is an inner product with norm ∥v∥A=a(v,v) (Real and complex inner product spaces, with the inner product linear in the first argument).

Proof

1.1F1F2F3algebra

Fix q∈Q and put w=A−1BTq. By [F1] and symmetry of A, b(v,q)=qTBv=vTBTq=vTAw=a(v,w) for every v∈V. By [F3], ∣a(v,w)∣≤∥v∥A∥w∥A. If w≠0, equality is attained at v=w; if w=0, both sides are zero. Hence sup⁡v≠0∣b(v,q)∣a(v,v)=a(w,w)=qTBA−1BTq.

2.1givenstep 1.1algebra

The upper energy inequality in the statement implies a(v,v)≤Λ∥v∥V, so the supremum in step 1.1 is at least β∥q∥Q/Λ. The lower energy inequality implies a(v,v)≥α∥v∥V; continuity of b therefore makes that supremum at most Cb∥q∥Q/α. Squaring these inequalities and using step 1.1 proves both displayed Schur bounds.

3.1F1givenstep 2.1algebra∎

For nonzero q, the lower bound in step 2.1 is positive because β>0 and MQ is positive definite. Thus S is positive definite, and the two quadratic-form inequalities are the stated pressure-mass spectral equivalence.

Depends on

Used by

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