`BookProof.EnergyBandDecomposition.norm_evolution_sub_scalar_le` (hε : 0 < ε) (hx : x ∈ band E ε k) (t : ℝ) (z : ℂ) : ‖Complex.exp (-(Complex.I * (t * (E x : ℂ)))) * z

Initializing...

`BookProof.EnergyBandDecomposition.norm_evolution_sub_scalar_le` (hε : 0 < ε) (hx : x ∈ band E ε k) (t : ℝ) (z : ℂ) : ‖Complex.exp (-(Complex.I * (t * (E x : ℂ)))) * z - Complex.ex · Prove2Me