`BookProof.ChapterE3.euler_density_diag_real` (l w : Fin n → ℝ) (θ : ℝ) (i : Fin n) (hli : l i = 1) (hwi : w i = 0) : Matrix.vecMulVec (fun j => Real.cos θ * l j + Real.sin θ * w j

Proved

BookProof.ChapterE3.euler_density_diag_real

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterE3.

BookProof.ChapterE3.euler_density_diag_real (l w : Fin n → ℝ) (θ : ℝ) (i : Fin n) (hli : l i = 1) (hwi : w i = 0) : Matrix.vecMulVec (fun j => Real.cos θ * l j + Real.sin θ * w j) (fun j => Real.cos θ * l j + Real.sin θ * w j) i i = Real.cos θ ^ 2

Formalization note: Lean 4 identifier BookProof.ChapterE3.euler_density_diag_real.

Preamble

-- Generated from ChapterE3.lean — theorem BookProof.ChapterE3.euler_density_diag_real
import Mathlib
import Definitions.Def_ChapterE3
open BookProof.ChapterE3


open scoped Matrix BigOperators


variable {n : ℕ}

Formal statement

theorem BookProof.ChapterE3.euler_density_diag_real (l w : Fin n → ℝ) (θ : ℝ) (i : Fin n)
    (hli : l i = 1) (hwi : w i = 0) :
    Matrix.vecMulVec (fun j => Real.cos θ * l j + Real.sin θ * w j)
        (fun j => Real.cos θ * l j + Real.sin θ * w j) i i
      = Real.cos θ ^ 2 := by sorry

View graph