`BookProof.ChapterE4.diag_collapse` (θ : ℕ → ℝ) (s d i : ℕ) : (wave θ s (d + 1) i) ^ 2 = Real.cos (θ s) ^ 2 * (basisVec s i) ^ 2 + Real.sin (θ s) ^ 2 * (wave θ (s + 1) d i) ^ 2

Proved

BookProof.ChapterE4.diag_collapse

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterE4.

BookProof.ChapterE4.diag_collapse (θ : ℕ → ℝ) (s d i : ℕ) : (wave θ s (d + 1) i) ^ 2 = Real.cos (θ s) ^ 2 * (basisVec s i) ^ 2 + Real.sin (θ s) ^ 2 * (wave θ (s + 1) d i) ^ 2

Formalization note: Lean 4 identifier BookProof.ChapterE4.diag_collapse.

Preamble

-- Generated from ChapterE4.lean — theorem BookProof.ChapterE4.diag_collapse
import Mathlib
import Definitions.Def_ChapterE4
open BookProof.ChapterE4


open scoped BigOperators

Formal statement

theorem BookProof.ChapterE4.diag_collapse (θ : ℕ → ℝ) (s d i : ℕ) :
    (wave θ s (d + 1) i) ^ 2
      = Real.cos (θ s) ^ 2 * (basisVec s i) ^ 2
        + Real.sin (θ s) ^ 2 * (wave θ (s + 1) d i) ^ 2 := by sorry

View graph