`BookProof.ChapterEnergyBoundedEvolution.phase_split` {A B C z : ℂ} (h : A * B = C) : C * z - A * z = A * (B * z - z)
ProvedBookProof.ChapterEnergyBoundedEvolution.phase_splittheoremstimepiece
Prove the following Lean 4 theorem from ChapterEnergyBoundedEvolution.
BookProof.ChapterEnergyBoundedEvolution.phase_split {A B C z : ℂ} (h : A * B = C) : C * z - A * z = A * (B * z - z)
Formalization note: Lean 4 identifier BookProof.ChapterEnergyBoundedEvolution.phase_split.
Preamble
-- Generated from ChapterEnergyBoundedEvolution.lean — theorem BookProof.ChapterEnergyBoundedEvolution.phase_split
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.phase_split {A B C z : ℂ} (h : A * B = C) : C * z - A * z = A * (B * z - z) := by sorry