`BookProof.ChapterMarkovEntropy.entropy_applyMarkov_ge` (M : Fin n → Fin n → ℝ) (hM : IsDoublyStochastic M) (p : Fin n → ℝ) (hp : ∀ i, 0 ≤ p i) : entropy p ≤ entropy (applyMarkov M

Proved

BookProof.ChapterMarkovEntropy.entropy_applyMarkov_ge

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterMarkovEntropy.

BookProof.ChapterMarkovEntropy.entropy_applyMarkov_ge (M : Fin n → Fin n → ℝ) (hM : IsDoublyStochastic M) (p : Fin n → ℝ) (hp : ∀ i, 0 ≤ p i) : entropy p ≤ entropy (applyMarkov M p)

Formalization note: Lean 4 identifier BookProof.ChapterMarkovEntropy.entropy_applyMarkov_ge.

Preamble

-- Generated from ChapterMarkovEntropy.lean — theorem BookProof.ChapterMarkovEntropy.entropy_applyMarkov_ge
import Mathlib
import Definitions.Def_ChapterMarkovEntropy
import Definitions.Def_ChapterIrreversible
open BookProof.ChapterIrreversible
open BookProof.ChapterMarkovEntropy


open scoped BigOperators
open Finset


variable {n : ℕ}

Formal statement

theorem BookProof.ChapterMarkovEntropy.entropy_applyMarkov_ge (M : Fin n → Fin n → ℝ) (hM : IsDoublyStochastic M)
    (p : Fin n → ℝ) (hp : ∀ i, 0 ≤ p i) :
    entropy p ≤ entropy (applyMarkov M p) := by sorry

View graph