Chapter Conservative

import Mathlib


/-!
# Chapter "Wave-function parametrization of a probability measure", §8 —
# Conservative transformations

This file formalizes the self-contained finite-dimensional core of the book's
section *"8. Conservative transformations"* (`book.tex` line ~1917), of the
main-conclusion chapter *"Wave-function parametrization of a probability
measure"*.

The book states that a conservative (canonical) transformation preserving the
measure is realized by a **unitary time-evolution** `U(t) = e^{iHt}` for a
self-adjoint Hamiltonian `H`, and remarks that *"any unitary automorphism can be
defined as a time-evolution, for some Hamiltonian and time"* and that a
conservative transformation *preserves the measure* (total probability).

We model this over a finite index set `n` and complex matrices. For a Hermitian
matrix `H : Matrix n n ℂ` we define the time-evolution
`timeEvo H t = exp((t : ℂ) • (I • H))` (the book's `e^{iHt}`) and prove:

* `timeEvo_zero` — `U(0) = 1`;
* `timeEvo_add` — the one-parameter group law `U(s) · U(t) = U(s + t)`;
* `timeEvo_unitary` / `timeEvo_unitary'` — `U(t)` is unitary (`U(t)ᴴ U(t) = 1`
  and `U(t) U(t)ᴴ = 1`);
* `timeEvo_mem_unitaryGroup` — hence `U(t) ∈ unitaryGroup n ℂ`;
* `timeEvo_inv` — the inverse of the time-evolution is the time-reversed
  evolution, `U(t)⁻¹ = U(-t)`;
* `timeEvo_conj_trace` — the conservative property: conjugating a density
  operator `ρ` by `U(t)` preserves its trace, `tr(U(t) ρ U(t)ᴴ) = tr ρ`
  (so total probability `tr ρ = 1` is preserved).

Everything is `sorry`-free and `axiom`-free (only `propext`, `Classical.choice`,
`Quot.sound`).
-/

open scoped Matrix

namespace BookProof.ChapterConservative

variable {n : Type*} [Fintype n] [DecidableEq n]

/-- The book's unitary time-evolution `U(t) = e^{iHt}` generated by the
self-adjoint Hamiltonian `H`. -/
noncomputable def timeEvo (H : Matrix n n ℂ) (t : ℝ) : Matrix n n ℂ :=
  NormedSpace.exp ((t : ℂ) • (Complex.I • H))

















end BookProof.ChapterConservative