`BookProof.Howland.howland_neg` (hU : IsPropagator U) (σ : ℝ) (ψ : ℝ → H) : howland U (-σ) (howland U σ ψ) = ψ
ProvedBookProof.Howland.howland_negtheoremstimepiece
Prove the following Lean 4 theorem from ChapterHowlandAutonomization.
BookProof.Howland.howland_neg (hU : IsPropagator U) (σ : ℝ) (ψ : ℝ → H) : howland U (-σ) (howland U σ ψ) = ψ
Formalization note: Lean 4 identifier BookProof.Howland.howland_neg.
Preamble
-- Generated from ChapterHowlandAutonomization.lean — theorem BookProof.Howland.howland_neg
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_neg (hU : IsPropagator U) (σ : ℝ) (ψ : ℝ → H) :
howland U (-σ) (howland U σ ψ) = ψ := by sorry