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

Proved

BookProof.ChapterE4.density_recursion

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterE4.

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

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

Preamble

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


open scoped BigOperators

Formal statement

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

View graph