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.

The diffusion Schur complement is positive and minimizes energy

Statement

Let $B = (\begin{array}{cc} K & C \\ C^{*} & D \end{array})$ be a self-adjoint positive-definite operator on a finite-dimensional real inner-product direct sum $I \oplus Λ$ . Then $K$ is positive definite, $S : = D - C^{*} K^{- 1} C$ is positive definite on $Λ$ , and for every $z \in Λ$ ,

$⟨ S z, z ⟩ = \min_{x \in I} ⟨ B (x, z), (x, z) ⟩ .$

In particular, the local Schur operators $S_{i}$ in Finite-dimensional backward-Euler diffusion transmission model are positive definite.

Facts & Assumptions

Given: The block matrix $B$ is self-adjoint positive definite on $I \oplus Λ$ , as are the local backward-Euler blocks $B_{i}$ in Finite-dimensional backward-Euler diffusion transmission model.

[F1]

Finite-dimensional backward-Euler diffusion transmission model: each $B_{i} = Δ t^{- 1} M_{i} + A_{i}$ is self-adjoint positive definite and its interface Schur complement is $S_{i} = B_{i, Γ Γ} - B_{i, Γ 0} B_{i, 00}^{- 1} B_{i, 0 Γ}$ .

Proof

1.1givenF1algebra

For $x \neq 0$ , $⟨ K x, x ⟩ = ⟨ B (x, 0), (x, 0) ⟩ > 0$ . Thus $K$ has zero kernel and is invertible because it is an endomorphism of a finite-dimensional space.

2.1step 1.1algebra

For fixed $z$ , put $x_{*} = - K^{- 1} C z$ . Expanding the quadratic form and completing the square gives $⟨ B (x, z), (x, z) ⟩ = ⟨ K (x - x_{*}), x - x_{*} ⟩ + ⟨ (D - C^{*} K^{- 1} C) z, z ⟩$ . The first term is nonnegative and vanishes exactly at $x = x_{*}$ , proving the minimum formula.

3.1F1step 2.1givenalgebra∎

If $z \neq 0$ , then $(x_{*}, z) \neq 0$ , so positive definiteness of $B$ gives $⟨ S z, z ⟩ = ⟨ B (x_{*}, z), (x_{*}, z) ⟩ > 0$ . Hence $S$ is positive definite; applying this to each $B_{i}$ in [F1] proves the final claim.

Depends on

Finite-dimensional backward-Euler diffusion transmission model

Used by

Dependency tree · one level

1 result within one dependency step 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

Emil Engström and Eskil Hansen, Time-dependent Steklov–Poincaré operators and space-time Robin–Robin decomposition for the heat equation (2022) (standard reference, not scraped)
Martina Maria Joosten, Aspects of interface modelling in fluid-structure interaction problems, PhD thesis, Swansea University (2011) (standard reference, not scraped)