`BookProof.ProbabilityClockStochastic.rotMat_mulVec_clockPsi` (t a : ℝ) : (rotMat a).mulVec (clockPsi t) = clockPsi (t + a)

Proved

BookProof.ProbabilityClockStochastic.rotMat_mulVec_clockPsi

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterProbabilityClockStochastic.

BookProof.ProbabilityClockStochastic.rotMat_mulVec_clockPsi (t a : ℝ) : (rotMat a).mulVec (clockPsi t) = clockPsi (t + a)

Formalization note: Lean 4 identifier BookProof.ProbabilityClockStochastic.rotMat_mulVec_clockPsi.

Preamble

-- Generated from ChapterProbabilityClockStochastic.lean — theorem BookProof.ProbabilityClockStochastic.rotMat_mulVec_clockPsi
import Mathlib
import Definitions.Def_ChapterProbabilityClockStochastic
import Definitions.Def_ChapterEulerDensityMatrix
import Definitions.Def_ChapterFullQuadraticEsa
open BookProof.ChapterEulerDensityMatrix
open BookProof.FullQuadratic
open BookProof.ProbabilityClockStochastic



open Matrix
open scoped Norms.Operator

Formal statement

theorem BookProof.ProbabilityClockStochastic.rotMat_mulVec_clockPsi (t a : ℝ) :
    (rotMat a).mulVec (clockPsi t) = clockPsi (t + a) := by sorry

View graph