`BookProof.ChapterSpectralEnergyBound.norm_evolve` (f : n → ℝ) (t : ℝ) (v : EuclideanSpace ℂ n) : ‖evolve f t v‖ = ‖v‖
ProvedBookProof.ChapterSpectralEnergyBound.norm_evolvetheoremstimepiece
Prove the following Lean 4 theorem from ChapterSpectralEnergyBound.
BookProof.ChapterSpectralEnergyBound.norm_evolve (f : n → ℝ) (t : ℝ) (v : EuclideanSpace ℂ n) : ‖evolve f t v‖ = ‖v‖
Formalization note: Lean 4 identifier BookProof.ChapterSpectralEnergyBound.norm_evolve.
Preamble
-- Generated from ChapterSpectralEnergyBound.lean — theorem BookProof.ChapterSpectralEnergyBound.norm_evolve
import Mathlib
import Definitions.Def_ChapterSpectralEnergyBound
import Definitions.Def_ChapterBornMeasure
open BookProof.ChapterBornMeasure
open BookProof.ChapterSpectralEnergyBound
variable {n : Type*} [Fintype n]Formal statement
theorem BookProof.ChapterSpectralEnergyBound.norm_evolve (f : n → ℝ) (t : ℝ) (v : EuclideanSpace ℂ n) :
‖evolve f t v‖ = ‖v‖ := by sorry