`BookProof.ProbabilityClockStochastic.IsColumnStochastic.mulVec_isProbabilityVector` {M : Matrix (Fin 2) (Fin 2) ℝ} (hM : IsColumnStochastic M) {v : Fin 2 → ℝ} (hv : IsProbabilityV

Proved

BookProof.ProbabilityClockStochastic.IsColumnStochastic.mulVec_isProbabilityVector

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterProbabilityClockStochastic.

BookProof.ProbabilityClockStochastic.IsColumnStochastic.mulVec_isProbabilityVector {M : Matrix (Fin 2) (Fin 2) ℝ} (hM : IsColumnStochastic M) {v : Fin 2 → ℝ} (hv : IsProbabilityVector v) : IsProbabilityVector (M.mulVec v)

Formalization note: Lean 4 identifier BookProof.ProbabilityClockStochastic.IsColumnStochastic.mulVec_isProbabilityVector.

Preamble

-- Generated from ChapterProbabilityClockStochastic.lean — theorem BookProof.ProbabilityClockStochastic.IsColumnStochastic.mulVec_isProbabilityVector
import Mathlib
import Definitions.Def_ChapterProbabilityClockStochastic
open BookProof.ProbabilityClockStochastic



open Matrix
open scoped Norms.Operator

Formal statement

theorem BookProof.ProbabilityClockStochastic.IsColumnStochastic.mulVec_isProbabilityVector
    {M : Matrix (Fin 2) (Fin 2) ℝ} (hM : IsColumnStochastic M)
    {v : Fin 2 → ℝ} (hv : IsProbabilityVector v) :
    IsProbabilityVector (M.mulVec v) := by sorry

View graph