theorem lemma2_3 (P Q : RateMatrix) (lambdaP lambdaQ : ℕ → ℝ) (h : (∀ (i : ℕ), P.Q i (i + 1) = Q.Q i (i + 1) ∧ ∀ (i : ℕ), i ≠ 0 → P.Q i (i - 1) ≥ Q.Q i (i - 1)) ∧ InvariantDistribution P lambdaP ∧ InvariantDistribution Q lambdaQ) : MeanNumberInSystem P lambdaP ⋯ ≥ MeanNumberInSystem Q lambdaQ ⋯

theorem lemma2_3_help (P : RateMatrix) (lambdaP : ℕ → ℝ) (h : InvariantDistribution P lambdaP) (i : ℕ) : P.Q (i + 2) (i + 1) ≠ 0 → lambdaP (i + 2) = ((P.Q (i + 1) i + P.Q (i + 1) (i + 2)) * lambdaP (i + 1) - P.Q i (i + 1) * lambdaP i) / P.Q (i + 2) (i + 1)

theorem rewrite (a b c : ℝ) (hab : a = 0 ∨ b = c) : a * b = a * c

theorem Nat.eq_div_of_cast_eq_div (a b c : ℕ) (h : ↑a = ↑b / ↑c) : a = b / c

theorem lemma2_3_1 (P : RateMatrix) (lambdaP : ℕ → ℝ) : (InvariantDistribution P lambdaP ∧ ∀ (i : ℕ), i ≠ 0 → P.Q i (i - 1) ≠ 0) → (∀ (i : ℕ), P.Q i (i + 1) ≠ 0) → ∀ (n : ℕ), lambdaP n = (∏ i : Fin n, P.Q (↑i) (↑i + 1) / P.Q (↑i + 1) ↑i) * lambdaP 0

theorem lemma2_3_3a' (P : RateMatrix) (lambdaP : ℕ → ℝ) : InvariantDistribution P lambdaP → ∀ (k : ℕ), ((∀ (i : ℕ), i ≠ 0 ∧ i < k → P.Q i (i - 1) ≠ 0) ∧ ∀ i < k, P.Q i (i + 1) ≠ 0) → ∀ n < k, lambdaP n = (∏ i : Fin n, P.Q (↑i) (↑i + 1) / P.Q (↑i + 1) ↑i) * lambdaP 0

theorem lemma2_3_3a (P : RateMatrix) (lambdaP : ℕ → ℝ) (h : InvariantDistribution P lambdaP) (n : ℕ) : n ≠ 0 → ∀ k > n, (∀ (m : ℕ), n < m ∧ m < k → P.Q (m - 1) m ≠ 0 ∧ P.Q m (m - 1) ≠ 0) → P.Q n (n - 1) = 0 ∧ P.Q k (k - 1) = 0 → lambdaP (n - 1) = 0 → ∀ (m' : ℕ), n < m' ∧ m' < k → lambdaP m' = (∏ i : Fin (m' - n), P.Q (↑i + n) (↑i + n + 1) / P.Q (↑i + n + 1) (↑i + n)) * lambdaP n

theorem fin_add_eq_non_add (n : ℕ) (n_non_zero : n ≠ 0) : Fin (n - 1 + 1) = Fin n

theorem n_sub_one_add_one_eq_n (n : ℕ) (n_non_zero : n ≠ 0) : n - 1 + 1 = n

theorem helper_lema (i : ℕ) {n : ℕ} (h : i < n - 1) : i < n

theorem helper_lema' (i : ℕ) {n : ℕ} (h : i < n - 1) : i + 1 < n

theorem lemma2_3_3b (P : RateMatrix) (lambdaP : ℕ → ℝ) (h'' : InvariantDistribution P lambdaP) (n : ℕ) [NeZero n] (n_non_zero : n ≠ 0) (A : Fin n → ℕ) (Indices_props : (∀ (i : ℕ) (h : i < n - 1), A ⟨i, ⋯⟩ < A ⟨i + 1, ⋯⟩) ∧ ∀ (i : ℕ) (h : i < n), A ⟨i, h⟩ ≠ 0 → P.Q (A ⟨i, h⟩) (A ⟨i, h⟩ - 1) = 0) : (∀ (i : ℕ), P.Q i (i + 1) ≠ 0) → (∀ (m : ℕ), m ≠ 0 ∧ P.Q m (m - 1) = 0 → ∃ (i : Fin n), m = A i) → ∀ (i : Fin n), A i ≠ 0 → lambdaP (A i - 1) = 0

theorem monotonically_increasing_imp_smaller (n : ℕ) [NeZero n] (A : Fin n → ℕ) (Indices_props : ∀ (i : ℕ) (h : i < n - 1), A ⟨i, ⋯⟩ < A ⟨i + 1, ⋯⟩) (i j : Fin n) : i > j → A i > A j

theorem lemma2_3_3c (P : RateMatrix) (lambdaP : ℕ → ℝ) (h'' : InvariantDistribution P lambdaP) (n : ℕ) [NeZero n] (n_non_zero : n ≠ 0) (A : Fin n → ℕ) (Indices_props : (∀ (i : ℕ) (h : i < n - 1), A ⟨i, ⋯⟩ < A ⟨i + 1, ⋯⟩) ∧ ∀ (i : ℕ) (h : i < n), A ⟨i, h⟩ ≠ 0 → P.Q (A ⟨i, h⟩) (A ⟨i, h⟩ - 1) = 0) : (∀ (i : ℕ), P.Q i (i + 1) ≠ 0) → (∀ (m : ℕ), m ≠ 0 ∧ P.Q m (m - 1) = 0 → ∃ (i : Fin n), m = A i) → (∃ (i : Fin n), A i ≠ 0) → lambdaP 0 = 0

theorem lemma2_3_3d (P : RateMatrix) (lambdaP : ℕ → ℝ) (h'' : InvariantDistribution P lambdaP) (n : ℕ) [NeZero n] (n_non_zero : n ≠ 0) (A : Fin n → ℕ) (Indices_props : (∀ (i : ℕ) (h : i < n - 1), A ⟨i, ⋯⟩ < A ⟨i + 1, ⋯⟩) ∧ ∀ (i : ℕ) (h : i < n), A ⟨i, h⟩ ≠ 0 → P.Q (A ⟨i, h⟩) (A ⟨i, h⟩ - 1) = 0) : (∀ (i : ℕ), P.Q i (i + 1) ≠ 0) → (∀ (m : ℕ), m ≠ 0 ∧ P.Q m (m - 1) = 0 → ∃ (i : Fin n), m = A i) → ∀ (i : Fin n) (h : 1 ≤ ↑i), lambdaP (A (Fin.subNat 1 i.castSucc h)) = 0