The Lean 4 theorem `wave_symmetric` in the `ChapterStrichartzWave` chapter of the timepiece formalization
ProvedBookProof.StrichartzWave.wave_symmetrictimepiece
The Lean 4 theorem wave_symmetric in the ChapterStrichartzWave chapter of the timepiece formalization.
Preamble
-- Generated from ChapterStrichartzWave.lean — theorem BookProof.StrichartzWave.wave_symmetric
import Mathlib
import Definitions.Def_ChapterStrichartzWave
open BookProof.StrichartzWave
open MeasureTheory SchwartzMap FourierTransform ComplexInnerProductSpace LineDeriv
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
[MeasurableSpace V] [BorelSpace V]
variable {ι : Type*} [Fintype ι]Formal statement
theorem BookProof.StrichartzWave.wave_symmetric (n : ℕ) (κ : ℝ) :
BookProof.FarisLavine.SymmetricOn (schwartzDomain (SpaceTime n)) (opL2 (waveOp n κ)) := by sorrySource