Prove2Me

`BookProof.ChapterEulerGenericDensity.outer_eulerVec` (θ : ℝ) (l w : Fin d → ℝ) : Matrix.vecMulVec (eulerVec θ l w) (eulerVec θ l w) = (Real.cos θ ^ 2) • Matrix.vecMulVec l l + (Re

Proved
BookProof.ChapterEulerGenericDensity.outer_eulerVec

by leonardopedro · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterEulerGenericDensity.

BookProof.ChapterEulerGenericDensity.outer_eulerVec (θ : ℝ) (l w : Fin d → ℝ) : Matrix.vecMulVec (eulerVec θ l w) (eulerVec θ l w) = (Real.cos θ ^ 2) • Matrix.vecMulVec l l + (Real.sin θ ^ 2) • Matrix.vecMulVec w w + (Real.cos θ * Real.sin θ) • (Matrix.vecMulVec l w + Matrix.vecMulVec w l)

Formalization note: Lean 4 identifier BookProof.ChapterEulerGenericDensity.outer_eulerVec.

Preamble
-- Generated from ChapterEulerGenericDensity.lean — theorem BookProof.ChapterEulerGenericDensity.outer_eulerVec
import Mathlib
import Definitions.Def_ChapterEulerGenericDensity
open BookProof.ChapterEulerGenericDensity


open scoped Matrix
open Matrix


variable {d : ℕ}
Formal statement
theorem BookProof.ChapterEulerGenericDensity.outer_eulerVec (θ : ℝ) (l w : Fin d → ℝ) :
    Matrix.vecMulVec (eulerVec θ l w) (eulerVec θ l w)
      = (Real.cos θ ^ 2) • Matrix.vecMulVec l l
        + (Real.sin θ ^ 2) • Matrix.vecMulVec w w
        + (Real.cos θ * Real.sin θ) •
            (Matrix.vecMulVec l w + Matrix.vecMulVec w l) := by sorry

View graph