`BookProof.ChapterSinusoidalPosition.peInner_symm` (w : Fin n → ℝ) (p q : ℝ) : peInner w p q = peInner w q p
ProvedBookProof.ChapterSinusoidalPosition.peInner_symmtheoremstimepiece
Prove the following Lean 4 theorem from ChapterSinusoidalPosition.
BookProof.ChapterSinusoidalPosition.peInner_symm (w : Fin n → ℝ) (p q : ℝ) : peInner w p q = peInner w q p
Formalization note: Lean 4 identifier BookProof.ChapterSinusoidalPosition.peInner_symm.
Preamble
-- Generated from ChapterSinusoidalPosition.lean — theorem BookProof.ChapterSinusoidalPosition.peInner_symm
import Definitions.Def_ChapterSoftmaxSharpness
import Definitions.Def_ChapterSoftmaxOrder
import Mathlib
import Definitions.Def_ChapterSinusoidalPosition
open BookProof.ChapterSinusoidalPosition
open scoped BigOperators
noncomputable section
open BookProof.ChapterSoftmaxSharpness BookProof.ChapterSoftmaxOrder
variable {n : ℕ}Formal statement
theorem BookProof.ChapterSinusoidalPosition.peInner_symm (w : Fin n → ℝ) (p q : ℝ) : peInner w p q = peInner w q p := by sorry