`BookProof.Howland.howland_lintegral_normSq` (hU : IsPropagator U) (σ : ℝ) (ψ : ℝ → H) : ∫⁻ t, ENNReal.ofReal (‖howland U σ ψ t‖ ^ 2) = ∫⁻ t, ENNReal.ofReal (‖ψ t‖ ^ 2)

Initializing...

`BookProof.Howland.howland_lintegral_normSq` (hU : IsPropagator U) (σ : ℝ) (ψ : ℝ → H) : ∫⁻ t, ENNReal.ofReal (‖howland U σ ψ t‖ ^ 2) = ∫⁻ t, ENNReal.ofReal (‖ψ t‖ ^ 2) · Prove2Me