Chapter EnergyBoundedEvolution

import Definitions.Def_ChapterEnergyBandDecomposition
import Mathlib


/-!
# An energy bound on the initial condition forbids a divergent time-derivative

Source: `book.tex`, chapter *"Resolution of the singularity of the ODE x'=x² when the
initial x has uncertainties"*, §*Resolution of the singularity using the uncertainties in x*:

> "A singularity at finite-time in the time-evolution of an initial value problem defined by
> an ordinary differential equation implies that the derivative in time of the corresponding
> wave-function diverges. […] Since the derivative in time corresponds to the Hamiltonian
> (whose spectral measure is conserved by the time-evolution) then if the initial condition
> only involves eigenfunctions corresponding to a spectrum up to some maximum absolute value,
> there is no way in which the time-evolution will produce a divergent derivative in time of
> the wave-function."

This file proves that statement.  As in `BookProof.ChapterEnergyBandDecomposition`, the
Hamiltonian is realized as the multiplication operator by a real *energy* function `E` on
`L²(X, μ)`, so that its unitary group is multiplication by `exp(−i t E(x))` (`evol`).  A state
*obeys the energy bound* `Emax` when it vanishes outside the spectral window `|E| ≤ Emax`
(`EnergyLimited`) — the book's "initial condition only involves eigenfunctions corresponding
to a spectrum up to some maximum absolute value".

## Deliverables

* `norm_evol_apply`, `eLpNorm_evol` — the evolution is pointwise and `L²`-isometric, so the
  state stays normalized at all times;
* `energyLimited_evol` — the energy window is conserved by the evolution (the book's
  "spectral measure is conserved by the time-evolution");
* **`eLpNorm_evol_sub_evol_le`** — the trajectory is **Lipschitz in time** with constant
  `Emax ‖ψ‖`: `‖U(t)ψ − U(s)ψ‖₂ ≤ |t − s| · Emax · ‖ψ‖₂`;
* **`eLpNorm_difference_quotient_le`** — equivalently every difference quotient of the
  trajectory is bounded by `Emax ‖ψ‖`, uniformly in the time step: **the derivative in time
  cannot diverge**, which is exactly the chapter's claim;
* `eLpNorm_evol_sub_self_le` — the special case `s = 0`.

No claim is made that the trajectory is differentiable: the point of the chapter is exactly
that *every* difference quotient stays bounded by `Emax ‖ψ‖`, so no divergence of the time
derivative can occur, whatever the initial state inside the energy window.

Everything is `sorry`-free and uses only the standard axioms.
-/

namespace BookProof.ChapterEnergyBoundedEvolution

open MeasureTheory Complex
open scoped ENNReal
open BookProof.EnergyBandDecomposition

variable {X : Type*} [MeasurableSpace X] {μ : Measure X} {E : X → ℝ} {f : X → ℂ}

/-- The time evolution generated by the energy function `E`: multiplication by
`exp(−i t E(x))`. -/
noncomputable def evol (E : X → ℝ) (t : ℝ) (f : X → ℂ) (x : X) : ℂ :=
  Complex.exp (-(Complex.I * (t * E x))) * f x

/-- A state **obeys the energy bound `Emax`** when it vanishes (almost everywhere) outside the
spectral window `|E| ≤ Emax`. -/
def EnergyLimited (E : X → ℝ) (μ : Measure X) (Emax : ℝ) (f : X → ℂ) : Prop :=
  ∀ᵐ x ∂μ, f x ≠ 0 → |E x| ≤ Emax



















end BookProof.ChapterEnergyBoundedEvolution