`BookProof.Howland.howland_lintegral_normSq` (hU : IsPropagator U) (σ : ℝ) (ψ : ℝ → H) : ∫⁻ t, ENNReal.ofReal (‖howland U σ ψ t‖ ^ 2) = ∫⁻ t, ENNReal.ofReal (‖ψ t‖ ^ 2)
ProvedBookProof.Howland.howland_lintegral_normSqtheoremstimepiece
Prove the following Lean 4 theorem from ChapterHowlandAutonomization.
BookProof.Howland.howland_lintegral_normSq (hU : IsPropagator U) (σ : ℝ) (ψ : ℝ → H) : ∫⁻ t, ENNReal.ofReal (‖howland U σ ψ t‖ ^ 2) = ∫⁻ t, ENNReal.ofReal (‖ψ t‖ ^ 2)
Formalization note: Lean 4 identifier BookProof.Howland.howland_lintegral_normSq.
Preamble
-- Generated from ChapterHowlandAutonomization.lean — theorem BookProof.Howland.howland_lintegral_normSq
import Mathlib
import Definitions.Def_ChapterHowlandAutonomization
open BookProof.Howland
open MeasureTheory
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
variable {H : Type*} [NormedAddCommGroup H]
variable {U : ℝ → ℝ → H → H}Formal statement
theorem BookProof.Howland.howland_lintegral_normSq (hU : IsPropagator U) (σ : ℝ) (ψ : ℝ → H) :
∫⁻ t, ENNReal.ofReal (‖howland U σ ψ t‖ ^ 2)
= ∫⁻ t, ENNReal.ofReal (‖ψ t‖ ^ 2) := by sorry