`BookProof.ChapterEulerNState.sum_cos_tail` (θ : ℕ → ℝ) (m : ℕ) : ∑ k ∈ Finset.range m, tailProd θ k * Real.cos (θ k) ^ 2 = 1 - tailProd θ m

Proved

BookProof.ChapterEulerNState.sum_cos_tail

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterEulerNState.

BookProof.ChapterEulerNState.sum_cos_tail (θ : ℕ → ℝ) (m : ℕ) : ∑ k ∈ Finset.range m, tailProd θ k * Real.cos (θ k) ^ 2 = 1 - tailProd θ m

Formalization note: Lean 4 identifier BookProof.ChapterEulerNState.sum_cos_tail.

Preamble

-- Generated from ChapterEulerNState.lean — theorem BookProof.ChapterEulerNState.sum_cos_tail
import Mathlib
import Definitions.Def_ChapterEulerNState
open BookProof.ChapterEulerNState


open scoped BigOperators

Formal statement

theorem BookProof.ChapterEulerNState.sum_cos_tail (θ : ℕ → ℝ) (m : ℕ) :
    ∑ k ∈ Finset.range m, tailProd θ k * Real.cos (θ k) ^ 2
      = 1 - tailProd θ m := by sorry

View graph