The one-parameter unitary group exp(−itH) of a Hermitian matrix

Category: 1-Mathlib (CSD-free; the matrix exponential of a skew-Hermitian generator).

For a Hermitian matrix H and a real time t, the generator −(it) H is skew-Hermitian, so its matrix exponential is unitary. This file packages exp(−itH) as an element of Matrix.unitaryGroup, proves that the family is a one-parameter group, and differentiates it: U t has derivative U t * (−iH) at every t, the C¹ datum finite-dimensional Stone theorems consume. The derivative is taken under the C*-algebra L2Operator norm scope, where the completeness instance that hasDerivAt_exp_smul_const needs synthesises without a diamond.

Main declarations

• Matrix.schrodingerGen H t = (−t i) • H and schrodingerGen_star (skew-Hermitian for Hermitian H); schrodingerGen_exp_mem_unitaryGroup — its exponential is unitary.
• Matrix.schrodingerUnitary hH t : unitaryGroup (Fin N) ℂ — the bundled exp(−itH).
• expNegITH_unitary_group — U (s + t) = U s * U t and U 0 = 1 in the unitary group.
• schrodingerUnitary_hasDerivAt — HasDerivAt (U ·) (U t * (−i • H)) t, with the helpers schrodingerGen_neg_i_smul_skew and schrodingerGen_eq_real_smul.

Provenance

Moved verbatim on 2026-09-16 from CsdLean4/LF4/ProjectedDynamics.lean (the generator, the unitary and the group law, 2026-06) and CsdLean4/LF4/ManyToOneSchrodingerDerived.lean (the derivative, 2026-07-19), where they back the projected Schrödinger flow of that programme; CSD.LF4 re-exports the names. The move makes the Category-1 manifold modules that use exp(−itH) (the Schrödinger flow on ℂℙⁿ) Category 1 by closure.

References

• specs/future-work.md (the completed-work ledger).

def Matrix.schrodingerGen {N : ℕ} (H : Matrix (Fin N) (Fin N) ℂ) (t : ℝ) : Matrix (Fin N) (Fin N) ℂ

The candidate Schrödinger generator matrix -(i t) H for a time t and a matrix H. When H is Hermitian and t real this is skew-Hermitian, so its matrix exponential is unitary.

Equations

• H.schrodingerGen t = (-↑t * Complex.I) • H

theorem Matrix.schrodingerGen_star {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (t : ℝ) : (H.schrodingerGen t).conjTranspose = -H.schrodingerGen t

For Hermitian H, the generator -(i t) H is skew-Hermitian: (schrodingerGen H t)ᴴ = - schrodingerGen H t.

theorem Matrix.schrodingerGen_exp_mem_unitaryGroup {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (t : ℝ) : NormedSpace.exp (H.schrodingerGen t) ∈ unitaryGroup (Fin N) ℂ

exp(-itH) is unitary. For Hermitian H and real t, the matrix exponential exp(schrodingerGen H t) = exp(-i t H) lies in unitaryGroup (Fin N) ℂ: the generator is skew-Hermitian, so (exp A)ᴴ = exp (Aᴴ) = exp (-A) and exp A * exp (-A) = exp 0 = 1.

noncomputable def Matrix.schrodingerUnitary {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (t : ℝ) : ↥(unitaryGroup (Fin N) ℂ)

The unitary exp(-i t H) ∈ unitaryGroup as a bundled group element.

Equations

• Matrix.schrodingerUnitary hH t = ⟨NormedSpace.exp (H.schrodingerGen t), ⋯⟩

theorem Matrix.expNegITH_unitary_group {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) : (∀ (s t : ℝ), schrodingerUnitary hH (s + t) = schrodingerUnitary hH s * schrodingerUnitary hH t) ∧ schrodingerUnitary hH 0 = 1

The exp(-itH) family is a one-parameter unitary group. For Hermitian H, the family U t = exp(-i t H) satisfies U (s + t) = U s * U t and U 0 = 1 as genuine unitary-group identities (not merely up to phase).

theorem Matrix.schrodingerGen_neg_i_smul_skew {N : ℕ} (H : Matrix (Fin N) (Fin N) ℂ) (hH : H.IsHermitian) : star (-Complex.I • H) = -(-Complex.I • H)

The skew-Hermitian Schrödinger generator A = -i H for Hermitian H: star (-i H) = -(-i H).

theorem Matrix.schrodingerGen_eq_real_smul {N : ℕ} (H : Matrix (Fin N) (Fin N) ℂ) (τ : ℝ) : H.schrodingerGen τ = τ • -Complex.I • H

schrodingerGen H τ = τ • (-i H) as a real scalar action (tower ℝ → ℂ → Matrix). Rewrites the time-τ generator into the t • A form hasDerivAt_exp_smul_const expects.

theorem Matrix.schrodingerUnitary_hasDerivAt {N : ℕ} (H : Matrix (Fin N) (Fin N) ℂ) (hH : H.IsHermitian) (t : ℝ) : HasDerivAt (fun (τ : ℝ) => ↑(schrodingerUnitary hH τ)) (↑(schrodingerUnitary hH t) * -Complex.I • H) t

The C¹ datum. The family U t = exp(-itH) has derivative U t * (-iH) at every t, for every Hermitian H — the hypothesis finite-dimensional Stone theorems consume.