122structure DiscreteEvolution (N : ℕ) where 123 hamiltonian : Fin N → Fin N → ℝ 124 symmetric : ∀ i j, hamiltonian i j = hamiltonian j i 125 126/-- Apply one step of discrete evolution to deviations (linearized). -/ 127def DiscreteEvolution.step (ev : DiscreteEvolution N) (ψ : DeviationHilbert N) : 128 DeviationHilbert N :=
proof body
Definition body.
129 fun i => ψ i - Complex.I * (Finset.univ.sum fun j => (ev.hamiltonian i j : ℂ) * ψ j) 130 131/-- The diagonal Hamiltonian: H_ii = 1 (from J''(1) = 1 calibration). -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.