`BookProof.ChapterSinusoidalPosition.abs_peInner_le` (w : Fin n → ℝ) (p q : ℝ) : |peInner w p q| ≤ (n : ℝ)
ProvedBookProof.ChapterSinusoidalPosition.abs_peInner_letheoremstimepiece
Prove the following Lean 4 theorem from ChapterSinusoidalPosition.
BookProof.ChapterSinusoidalPosition.abs_peInner_le (w : Fin n → ℝ) (p q : ℝ) : |peInner w p q| ≤ (n : ℝ)
Formalization note: Lean 4 identifier BookProof.ChapterSinusoidalPosition.abs_peInner_le.
Preamble
-- Generated from ChapterSinusoidalPosition.lean — theorem BookProof.ChapterSinusoidalPosition.abs_peInner_le
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.abs_peInner_le (w : Fin n → ℝ) (p q : ℝ) : |peInner w p q| ≤ (n : ℝ) := by sorry