Chapter SpectralEnergyBound

import Mathlib


/-!
# Energy-bounded initial conditions: no finite-time blow-up

This closes goal **A.4** of the book's *Proof Plans* appendix
(`Book/ProofPlans.lean`): *an initial wave-function supported on the part of the
spectrum below `Emax` has a bounded time-derivative, hence cannot blow up in
finite time*.

We work in the spectral representation, where the Hamiltonian is the diagonal
(multiplication) operator `H = diagOp f` with real eigenvalues `f i` — by the
spectral theorem (`BookProof.ChapterDensitySpectral`) every Hermitian matrix is
unitarily equivalent to such an operator, and a unitary change of basis preserves
all the norms below.  The Schrödinger evolution is then the explicit phase flow
`evolve f t v i = e^{-i t f i} · v i`.

Formalized here:

* `norm_diagOp_le` — the **spectral bound**: if every eigenvalue on the support of
  `ψ` satisfies `|f i| ≤ Emax`, then `‖H ψ‖ ≤ Emax ‖ψ‖`;
* `norm_evolve` — the evolution is **unitary**: `‖ψ(t)‖ = ‖ψ(0)‖`;
* `evolve_support` — the evolution preserves the spectral subspace;
* `hasDerivAt_evolve` — the Schrödinger equation `ψ'(t) = -i H ψ(t)`;
* `norm_deriv_evolve_le` — the **energy bound**: `‖ψ'(t)‖ ≤ Emax ‖ψ(0)‖` for all
  `t`, uniformly in time;
* `evolve_lipschitz` — hence `‖ψ(t) − ψ(s)‖ ≤ Emax ‖ψ(0)‖ · |t − s|`: the solution
  is globally Lipschitz, so there is **no finite-time singularity**.

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

namespace BookProof.ChapterSpectralEnergyBound

variable {n : Type*} [Fintype n]

/-- The Hamiltonian in its spectral representation: multiplication by the real
eigenvalue function `f`. -/
def diagOp (f : n → ℝ) (v : EuclideanSpace ℂ n) : EuclideanSpace ℂ n :=
  WithLp.toLp 2 (fun i => (f i : ℂ) * v i)



/-- The Schrödinger flow generated by `diagOp f`: `ψ(t) i = e^{-i t f i} ψ(0) i`. -/
noncomputable def evolve (f : n → ℝ) (t : ℝ) (v : EuclideanSpace ℂ n) :
    EuclideanSpace ℂ n :=
  WithLp.toLp 2 (fun i => Complex.exp (-Complex.I * (t : ℂ) * (f i : ℂ)) * v i)



















end BookProof.ChapterSpectralEnergyBound