LemmaStatement: AI-adaptedProof: 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.

Cofactor, surface-Jacobian, and normal perturbation bounds

Statement

Let $A = D Φ$ and $A_{h} = D Φ_{h}$ be orientation-preserving cell-map derivatives with $\det A, \det A_{h} \geq j_{*} > 0$ , $∥ A ∥_{o p}, ∥ A_{h} ∥_{o p} \leq M$ , and $∥ A - A_{h} ∥_{o p} \leq e_{1}$ . For every unit reference-facet normal $\hat{n}$ , define the surface Jacobians $J_{Γ} (A) = ∥ cof (A) \hat{n} ∥$ , $J_{Γ} (A_{h}) = ∥ cof (A_{h}) \hat{n} ∥$ , and mapped unit normals $n_{Γ} (A) = cof (A) \hat{n} / J_{Γ} (A)$ and $n_{Γ} (A_{h}) = cof (A_{h}) \hat{n} / J_{Γ} (A_{h})$ . Then $∥ cof (A) - cof (A_{h}) ∥_{o p} + ∣ J_{Γ} (A) - J_{Γ} (A_{h}) ∣ + ∣ n_{Γ} (A) - n_{Γ} (A_{h}) ∣ \leq C (d, M, j_{*}) e_{1} .$ For any regular reference-facet parametrization $\hat{f}$ , the chart Gram-metric factor of Admissible isoparametric curved cells is $\sqrt{\det (D {\hat{f}}^{T} A^{T} A D \hat{f})} = J_{Γ} (A) \sqrt{\det (D {\hat{f}}^{T} D \hat{f})}$ , pointwise with $A = D Φ (\hat{f})$ . Thus $J_{Γ} (A)$ is the surface-area factor relative to reference-facet area; it equals the chart factor when the reference chart has unit area factor. The same relation holds for $A_{h}$ .

Facts & Assumptions

Given: Orientation-preserving invertible matrices $A, A_{h} \in R^{d \times d}$ with determinant lower bound $j_{*}$ , operator norm upper bound $M$ , derivative gap $e_{1}$ , and a unit reference normal $\hat{n}$ .

[F1]

Admissible isoparametric curved cells: for a reference facet chart $\hat{f}$ , the physical surface factor is the square root of the Gram determinant of $D (Φ \circ \hat{f})$ .

[F2]

Curved-domain geometry approximation errors: $e_{1} = ∥ D Φ - D Φ_{h} ∥_{L^{\infty}; o p}$ .

Proof

1.1F1F2givenalgebra

Each entry of $cof (A)$ is a signed $(d - 1)$ -minor, hence a polynomial of degree $d - 1$ in the entries of $A$ . On the bounded matrix ball $∥ A ∥_{o p}, ∥ A_{h} ∥_{o p} \leq M$ , its derivative is bounded by a constant depending only on $d, M$ . The mean-value inequality therefore gives $∥ cof (A) - cof (A_{h}) ∥_{o p} \leq C (d, M) ∥ A - A_{h} ∥_{o p} = C (d, M) e_{1}$ .

1.2F1givenalgebra

Let $T$ have orthonormal columns spanning the reference facet tangent space, so $Q = [T, \hat{n}]$ is orthogonal. The squared Gram-metric surface factor is $\det (T^{T} A^{T} A T)$ . The identity $cof (A)^{T} cof (A) = cof (A^{T} A)$ and orthogonal covariance of cofactors show ${\hat{n}}^{T} cof (A^{T} A) \hat{n}$ is the bottom-right cofactor of $Q^{T} A^{T} A Q$ , which is exactly $\det (T^{T} A^{T} A T)$ . Therefore $∥ cof (A) \hat{n} ∥^{2} = \det (T^{T} A^{T} A T)$ . For a regular chart write $D \hat{f} = T R$ , where $R$ is an invertible $(d - 1) \times (d - 1)$ matrix. Then $\det (D {\hat{f}}^{T} A^{T} A D \hat{f}) = \det (R)^{2} \det (T^{T} A^{T} A T)$ and $\det (D {\hat{f}}^{T} D \hat{f}) = \det (R)^{2}$ . Taking positive square roots gives the stated chart-factor relation, also for $A_{h}$ .

2.1F1givenstep 1.1algebra

If $σ_{1} (A) \geq \dots \geq σ_{d} (A) > 0$ are the singular values, the smallest singular value of $cof (A)$ is $\prod_{i = 2}^{d} σ_{i} (A) = \det (A) / σ_{1} (A) \geq j_{*} / M$ . Thus $J_{Γ} (A) \geq j_{*} / M$ , and the same bound holds for $A_{h}$ . The reverse triangle inequality and step 1.1 give $∣ J_{Γ} (A) - J_{Γ} (A_{h}) ∣ \leq C (d, M) e_{1}$ .

3.1step 1.1step 2.1algebra∎

Put $a = cof (A) \hat{n}$ and $b = cof (A_{h}) \hat{n}$ . For nonzero vectors, $∣ a / ∣ a ∣ - b / ∣ b ∣ ∣ \leq 2 ∣ a - b ∣ / \min (∣ a ∣, ∣ b ∣)$ . The lower bounds from step 2.1 and the cofactor gap from step 1.1 therefore imply $∣ n_{Γ} (A) - n_{Γ} (A_{h}) ∣ \leq C (d, M, j_{*}) e_{1}$ . Combining the three estimates proves the result.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

3 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 2023, Part III, Chapter 8 (standard reference, not scraped)
Gerald Dziuk and Charles M. Elliott, Finite element methods for surface PDEs, Acta Numerica 22 (2013) (standard reference, not scraped)