`BookProof.ChapterEnergyBoundedEvolution.energyLimited_evol` {Emax : ℝ} (t : ℝ) (h : EnergyLimited E μ Emax f) : EnergyLimited E μ Emax (evol E t f)
ProvedBookProof.ChapterEnergyBoundedEvolution.energyLimited_evoltheoremstimepiece
Prove the following Lean 4 theorem from ChapterEnergyBoundedEvolution.
BookProof.ChapterEnergyBoundedEvolution.energyLimited_evol {Emax : ℝ} (t : ℝ) (h : EnergyLimited E μ Emax f) : EnergyLimited E μ Emax (evol E t f)
Formalization note: Lean 4 identifier BookProof.ChapterEnergyBoundedEvolution.energyLimited_evol.
Preamble
-- Generated from ChapterEnergyBoundedEvolution.lean — theorem BookProof.ChapterEnergyBoundedEvolution.energyLimited_evol
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.energyLimited_evol {Emax : ℝ} (t : ℝ) (h : EnergyLimited E μ Emax f) :
EnergyLimited E μ Emax (evol E t f) := by sorry