`BookProof.ChapterEnergyBoundedEvolution.norm_evol_apply` (t : ℝ) (f : X → ℂ) (x : X) : ‖evol E t f x‖ = ‖f x‖
ProvedBookProof.ChapterEnergyBoundedEvolution.norm_evol_applytheoremstimepiece
Prove the following Lean 4 theorem from ChapterEnergyBoundedEvolution.
BookProof.ChapterEnergyBoundedEvolution.norm_evol_apply (t : ℝ) (f : X → ℂ) (x : X) : ‖evol E t f x‖ = ‖f x‖
Formalization note: Lean 4 identifier BookProof.ChapterEnergyBoundedEvolution.norm_evol_apply.
Preamble
-- Generated from ChapterEnergyBoundedEvolution.lean — theorem BookProof.ChapterEnergyBoundedEvolution.norm_evol_apply
import Definitions.Def_ChapterEnergyBandDecomposition
import Mathlib
import Definitions.Def_ChapterEnergyBoundedEvolution
open BookProof.ChapterEnergyBoundedEvolution
open MeasureTheory Complex
open scoped ENNReal
open BookProof.EnergyBandDecomposition
variable {X : Type*} [MeasurableSpace X] {μ : Measure X} {E : X → ℝ} {f : X → ℂ}Formal statement
theorem BookProof.ChapterEnergyBoundedEvolution.norm_evol_apply (t : ℝ) (f : X → ℂ) (x : X) : ‖evol E t f x‖ = ‖f x‖ := by sorry