inductive PDEClassification.PDEType : Type

Hadamard's classification of second-order linear PDEs into elliptic, hyperbolic, and parabolic types, determined by the signature of the leading symbol matrix.

• elliptic : PDEType
• hyperbolic : PDEType
• parabolic : PDEType

@[implicit_reducible]

instance PDEClassification.instDecidableEqPDEType : DecidableEq PDEType

def PDEClassification.instReprPDEType.repr : PDEType → ℕ → Std.Format

@[implicit_reducible]

instance PDEClassification.instReprPDEType : Repr PDEType

def PDEClassification.IsElliptic {N : Type u_1} [Fintype N] [DecidableEq N] {A : Matrix N N ℝ} (hA : A.IsHermitian) : Prop

$A$ is elliptic iff all eigenvalues of $A$ are strictly positive, or all are strictly negative — i.e. the leading-symbol matrix is definite.

def PDEClassification.IsHyperbolic {N : Type u_1} [Fintype N] [DecidableEq N] {A : Matrix N N ℝ} (hA : A.IsHermitian) : Prop

$A$ is hyperbolic iff all eigenvalues are nonzero and there exists an index $j$ such that every other eigenvalue has sign opposite to that of $\lambda_j$ (signature $(1, n-1)$ or $(n-1, 1)$).

def PDEClassification.IsParabolic {N : Type u_1} [Fintype N] [DecidableEq N] {A : Matrix N N ℝ} (hA : A.IsHermitian) : Prop

$A$ is parabolic iff there is exactly one zero eigenvalue (at some index $j$) and all other eigenvalues are nonzero and share a common sign (their pairwise products are positive).

theorem PDEClassification.spectral_diagonalization {N : Type u_1} [Fintype N] [DecidableEq N] {A : Matrix N N ℝ} (hA : A.IsHermitian) : (↑hA.eigenvectorUnitary).transpose * A * ↑hA.eigenvectorUnitary = Matrix.diagonal hA.eigenvalues

Spectral theorem (real-symmetric form): for a real Hermitian matrix $A$ with the orthogonal matrix $U$ of eigenvectors, $U^{T} A U = \operatorname{diag}(\lambda_i)$.

theorem PDEClassification.eigenvectorUnitary_det_ne_zero {N : Type u_1} [Fintype N] [DecidableEq N] {A : Matrix N N ℝ} (hA : A.IsHermitian) : (↑hA.eigenvectorUnitary).det ≠ 0

The matrix of eigenvectors produced by the spectral theorem is invertible (nonzero determinant), as it is orthogonal.

theorem PDEClassification.ne_zero_lt_or_gt {x : ℝ} (hx : x ≠ 0) : x < 0 ∨ 0 < x

Sign trichotomy for nonzero reals: $x \neq 0$ implies $x < 0$ or $0 < x$.

theorem PDEClassification.classification_normal_form {N : Type u_1} [Fintype N] [DecidableEq N] [Nonempty N] {A : Matrix N N ℝ} (hA : A.IsHermitian) : ∃ (M : Matrix N N ℝ), M.det ≠ 0 ∧ M.transpose * A * M = Matrix.diagonal fun (i : N) => if 0 < hA.eigenvalues i then 1 else if hA.eigenvalues i < 0 then -1 else 0

Normal form for a real Hermitian matrix: there is an invertible $M$ with $M^T A M$ a diagonal matrix whose entries are $+1$, $-1$, or $0$ according to the sign of the corresponding eigenvalue. This is the matrix-level statement behind Hadamard's classification of second-order PDEs.

theorem PDEClassification.sign_diagonal_eq_one {N : Type u_1} [Fintype N] [DecidableEq N] {A : Matrix N N ℝ} (hA : A.IsHermitian) (hpos : ∀ (i : N), 0 < hA.eigenvalues i) : (Matrix.diagonal fun (i : N) => if 0 < hA.eigenvalues i then 1 else if hA.eigenvalues i < 0 then -1 else 0) = 1

Helper: when all eigenvalues are positive, the sign-diagonal $\operatorname{diag}(\pm 1, 0)$ collapses to the identity matrix.

theorem PDEClassification.sign_diagonal_eq_neg_one {N : Type u_1} [Fintype N] [DecidableEq N] {A : Matrix N N ℝ} (hA : A.IsHermitian) (hneg : ∀ (i : N), hA.eigenvalues i < 0) : (Matrix.diagonal fun (i : N) => if 0 < hA.eigenvalues i then 1 else if hA.eigenvalues i < 0 then -1 else 0) = -1

Helper: when all eigenvalues are negative, the sign-diagonal collapses to $-I$.

theorem PDEClassification.sign_of_ne_zero {N : Type u_1} [Fintype N] [DecidableEq N] {A : Matrix N N ℝ} (hA : A.IsHermitian) {i : N} (hi : hA.eigenvalues i ≠ 0) : (if 0 < hA.eigenvalues i then 1 else if hA.eigenvalues i < 0 then -1 else 0) = 1 ∨ (if 0 < hA.eigenvalues i then 1 else if hA.eigenvalues i < 0 then -1 else 0) = -1

Helper: at a nonzero eigenvalue, the sign expression evaluates to either $+1$ or $-1$.

theorem PDEClassification.classification_theorem_3_1 {N : Type u_1} [Fintype N] [DecidableEq N] [Nonempty N] {A : Matrix N N ℝ} (hA : A.IsHermitian) : ∃ (M : Matrix N N ℝ), M.det ≠ 0 ∧ (M.transpose * A * M = Matrix.diagonal fun (i : N) => if 0 < hA.eigenvalues i then 1 else if hA.eigenvalues i < 0 then -1 else 0) ∧ (IsElliptic hA → M.transpose * A * M = 1 ∨ M.transpose * A * M = -1) ∧ (IsHyperbolic hA → ∃ (σ : N → ℝ), (∀ (i : N), σ i = 1 ∨ σ i = -1) ∧ (∃ (j : N), ∀ (i : N), i ≠ j → σ i * σ j < 0) ∧ M.transpose * A * M = Matrix.diagonal σ) ∧ (IsParabolic hA → ∃ (j₀ : N) (σ : N → ℝ), σ j₀ = 0 ∧ (∀ (i : N), i ≠ j₀ → σ i = 1 ∨ σ i = -1) ∧ (∀ (i₁ i₂ : N), i₁ ≠ j₀ → i₂ ≠ j₀ → σ i₁ = σ i₂) ∧ M.transpose * A * M = Matrix.diagonal σ)

Hadamard's classification of second-order PDEs (Theorem 3.1, matrix form): for any real Hermitian leading-symbol matrix $A$, there exists an invertible change of variables $M$ bringing $A$ into a diagonal sign normal form, and additionally

• in the elliptic case, $M^T A M = \pm I$,
• in the hyperbolic case, $M^T A M$ is a $\pm 1$-diagonal whose entries split in sign with exactly one differing sign,
• in the parabolic case, $M^T A M$ is a diagonal with exactly one $0$ entry and the remaining entries all $+1$ or all $-1$.