# Theory Classifying_Markov_Chain_States

```section ‹Classifying Markov Chain States›

theory Classifying_Markov_Chain_States
imports
"HOL-Computational_Algebra.Group_Closure"
Discrete_Time_Markov_Chain
begin

lemma eventually_mult_Gcd:
fixes S :: "nat set"
assumes S: "⋀s t. s ∈ S ⟹ t ∈ S ⟹ s + t ∈ S"
assumes s: "s ∈ S" "s > 0"
shows "eventually (λm. m * Gcd S ∈ S) sequentially"
proof -
define T where "T = insert 0 (int ` S)"
with s S have "int s ∈ T" "0 ∈ T" and T: "r ∈ T ⟹ t ∈ T ⟹ r + t ∈ T" for r t
have "Gcd T ∈ group_closure T"
by (rule Gcd_in_group_closure)
also have "group_closure T = {s - t | s t. s ∈ T ∧ t ∈ T}"
proof (auto intro: group_closure.base group_closure.diff)
fix x assume "x ∈ group_closure T"
then show "∃s t. x = s - t ∧ s ∈ T ∧ t ∈ T"
proof induction
case (base x) with ‹0 ∈ T› show ?case
apply (rule_tac x=x in exI)
apply (rule_tac x=0 in exI)
apply auto
done
next
case (diff x y)
then obtain a b c d where
"a ∈ T" "b ∈ T" "x = a - b"
"c ∈ T" "d ∈ T" "y = c - d"
by auto
then show ?case
apply (rule_tac x="a + d" in exI)
apply (rule_tac x="b + c" in exI)
apply (auto intro: T)
done
qed
qed
finally obtain s' t' :: int
where "s' ∈ T" "t' ∈ T" "Gcd T = s' - t'"
by blast
moreover define s and t where "s = nat s'" and "t = nat t'"
moreover have "int (Gcd S) = - int t ⟷ S ⊆ {0} ∧ t = 0"
by auto (metis Gcd_dvd_nat dvd_0_right dvd_antisym nat_int nat_zminus_int)
ultimately have
st: "s = 0 ∨ s ∈ S" "t = 0 ∨ t ∈ S" and Gcd_S: "Gcd S = s - t"
using T_def by safe simp_all
with s
have "t < s"
by (rule_tac ccontr) auto

{ fix s n have "0 < n ⟹ s ∈ S ⟹ n * s ∈ S"
proof (induct n)
case (Suc n) then show ?case
by (cases n) (auto intro: S)
qed simp }
note cmult_S = this

show ?thesis
unfolding eventually_sequentially
proof cases
assume "s = 0 ∨ t = 0"
with st Gcd_S s have *: "Gcd S ∈ S"
by (auto simp: int_eq_iff)
then show "∃N. ∀n≥N. n * Gcd S ∈ S" by (auto intro!: exI[of _ 1] cmult_S)
next
assume "¬ (s = 0 ∨ t = 0)"
with st have "s ∈ S" "t ∈ S" "t ≠ 0" by auto
then have "Gcd S dvd t" by auto
then obtain a where a: "t = Gcd S * a" ..
with ‹t ≠ 0› have "0 < a" by auto

show "∃N. ∀n≥N. n * Gcd S ∈ S"
proof (safe intro!: exI[of _ "a * a"])
fix n
define m where "m = (n - a * a) div a"
define r where "r = (n - a * a) mod a"
with ‹0 < a› have "r < a" by simp
moreover define am where "am = a + m"
ultimately have "r < am" by simp
assume "a * a ≤ n" then have n: "n = a * a + (m * a + r)"
unfolding m_def r_def by simp
have "n * Gcd S = am * t + r * Gcd S"
unfolding n a by (simp add: field_simps am_def)
also have "… = r * s + (am - r) * t"
unfolding ‹Gcd S = s - t›
using ‹t < s› ‹r < am› by (simp add: field_simps diff_mult_distrib2)
also have "… ∈ S"
using ‹s ∈ S› ‹t ∈ S› ‹r < am›
by (cases "r = 0") (auto intro!: cmult_S S)
finally show "n * Gcd S ∈ S" .
qed
qed
qed

context MC_syntax
begin

subsection ‹Expected number of visits›

definition "G s t = (∫⇧+ω. scount (HLD {t}) (s ## ω) ∂T s)"

lemma G_eq: "G s t = (∫⇧+ω. emeasure (count_space UNIV) {i. (s ## ω) !! i = t} ∂T s)"
by (simp add: G_def scount_eq_emeasure HLD_iff)

definition "p s t n = 𝒫(ω in T s. (s ## ω) !! n = t)"

definition "gf_G s t z = (∑n. p s t n *⇩R z ^ n)"

definition "convergence_G s t z ⟷ summable (λn. p s t n * norm z ^ n)"

lemma p_nonneg[simp]: "0 ≤ p x y n"

lemma p_le_1: "p x y n ≤ 1"

lemma p_x_x_0[simp]: "p x x 0 = 1"
by (simp add: p_def T.prob_space del: space_T)

lemma p_0: "p x y 0 = (if x = y then 1 else 0)"
by (simp add: p_def T.prob_space del: space_T)

lemma p_in_reachable: assumes "(x, y) ∉ (SIGMA x:UNIV. K x)⇧*" shows "p x y n = 0"
unfolding p_def
proof (rule T.prob_eq_0_AE)
from AE_T_reachable show "AE ω in T x. (x ## ω) !! n ≠ y"
proof eventually_elim
fix ω assume "alw (HLD ((SIGMA ω:UNIV. K ω)⇧* `` {x})) ω"
then have "alw (HLD (- {y})) ω"
using assms by (auto intro: alw_mono simp: HLD_iff)
then show "(x ## ω) !! n ≠ y"
using assms by (cases n) (auto simp: alw_HLD_iff_streams streams_iff_snth)
qed
qed

lemma p_Suc: "ennreal (p x y (Suc n)) = (∫⇧+ w. p w y n ∂K x)"
unfolding p_def T.emeasure_eq_measure[symmetric] by (subst emeasure_Collect_T) simp_all

lemma p_Suc':
"p x y (Suc n) = (∫x'. p x' y n ∂K x)"
using p_Suc[of x y n]
by (subst (asm) nn_integral_eq_integral)
(auto simp: p_le_1 intro!: measure_pmf.integrable_const_bound[where B=1])

lemma p_add: "p x y (n + m) = (∫⇧+ w. p x w n * p w y m ∂count_space UNIV)"
proof (induction n arbitrary: x)
case 0
have [simp]: "⋀w. (if x = w then 1 else 0) * p w y m = ennreal (p x y m) * indicator {x} w"
by auto
show ?case
by (simp add: p_0 one_ennreal_def[symmetric] max_def)
next
case (Suc n)
define X where "X = (SIGMA x:UNIV. K x)⇧* `` K x"
then have X: "countable X"
by (blast intro: countable_Image countable_reachable countable_set_pmf)

then interpret X: sigma_finite_measure "count_space X"
by (rule sigma_finite_measure_count_space_countable)
interpret XK: pair_sigma_finite "K x" "count_space X"
by unfold_locales

have "ennreal (p x y (Suc n + m)) = (∫⇧+t. (∫⇧+w. p t w n * p w y m ∂count_space UNIV) ∂K x)"
also have "… = (∫⇧+t. (∫⇧+w. ennreal (p t w n * p w y m) * indicator X w ∂count_space UNIV) ∂K x)"
by (auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff AE_count_space Image_iff p_in_reachable X_def             split: split_indicator)
also have "… = (∫⇧+t. (∫⇧+w. p t w n * p w y m ∂count_space X) ∂K x)"
by (subst nn_integral_restrict_space[symmetric]) (simp_all add: restrict_count_space)
also have "… = (∫⇧+w. (∫⇧+t. p t w n * p w y m ∂K x) ∂count_space X)"
apply (rule XK.Fubini'[symmetric])
unfolding measurable_split_conv
apply (rule measurable_compose_countable'[OF _ measurable_snd X])
apply (rule measurable_compose[OF measurable_fst])
apply simp
done
also have "… = (∫⇧+w. (∫⇧+t. ennreal (p t w n * p w y m) * indicator X w ∂K x) ∂count_space UNIV)"
by (simp add: nn_integral_restrict_space[symmetric] restrict_count_space nn_integral_multc)
also have "… = (∫⇧+w. (∫⇧+t. ennreal (p t w n * p w y m) ∂K x) ∂count_space UNIV)"
by (auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff AE_count_space Image_iff p_in_reachable X_def             split: split_indicator)
also have "… = (∫⇧+w. (∫⇧+t. p t w n ∂K x) * p w y m ∂count_space UNIV)"
finally show ?case
qed

lemma prob_reachable_le:
assumes [simp]: "m ≤ n"
shows "p x y m * p y w (n - m) ≤ p x w n"
proof -
have "p x y m * p y w (n - m) = (∫⇧+y'. ennreal (p x y m * p y w (n - m)) * indicator {y} y' ∂count_space UNIV)"
by simp
also have "… ≤ p x w (m + (n - m))"
(auto intro!: nn_integral_mono split: split_indicator simp del: nn_integral_indicator_singleton)
finally show ?thesis
by simp
qed

lemma G_eq_suminf: "G x y = (∑i. ennreal (p x y i))"
proof -
have *: "⋀i ω. indicator {ω ∈ space S. (x ## ω) !! i = y} ω = indicator {i. (x ## ω) !! i = y} i"
by (auto simp: space_stream_space split: split_indicator)

have "G x y = (∫⇧+ ω. (∑i. indicator {ω∈space (T x). (x ## ω) !! i = y} ω) ∂T x)"
unfolding G_eq by (simp add: nn_integral_count_space_nat[symmetric] *)
also have "… = (∑i. ennreal (p x y i))"
by (simp add: T.emeasure_eq_measure[symmetric] p_def nn_integral_suminf)
finally show ?thesis .
qed

lemma G_eq_real_suminf:
"convergence_G x y (1::real) ⟹ G x y = ennreal (∑i. p x y i)"
unfolding G_eq_suminf
by (intro suminf_ennreal ennreal_suminf_neq_top p_nonneg)
(auto simp: convergence_G_def p_def)

lemma convergence_norm_G:
"convergence_G x y z ⟹ summable (λn. p x y n * norm z ^ n)"
unfolding convergence_G_def .

lemma convergence_G:
"convergence_G x y (z::'a::{banach, real_normed_div_algebra}) ⟹ summable (λn. p x y n *⇩R z ^ n)"
unfolding convergence_G_def
by (rule summable_norm_cancel) (simp add: abs_mult norm_power)

lemma convergence_G_less_1:
fixes z :: "_ :: {banach, real_normed_field}"
assumes z: "norm z < 1" shows "convergence_G x y z"
unfolding convergence_G_def
proof (rule summable_comparison_test)
have "⋀n. p x y n * norm (z ^ n) ≤ 1 * norm (z ^ n)"
by (intro mult_right_mono p_le_1) simp_all
then show "∃N. ∀n≥N. norm (p x y n * norm z ^ n) ≤ norm z ^ n"

lemma lim_gf_G: "((λz. ennreal (gf_G x y z)) ⤏ G x y) (at_left (1::real))"
unfolding gf_G_def G_eq_suminf real_scaleR_def
by (intro power_series_tendsto_at_left p_nonneg p_le_1 summable_power_series)

subsection ‹Reachability probability›

definition "u x y n = 𝒫(ω in T x. ev_at (HLD {y}) n ω)"

definition "U s t = 𝒫(ω in T s. ev (HLD {t}) ω)"

definition "gf_U x y z = (∑n. u x y n *⇩R z ^ Suc n)"

definition "f x y n = 𝒫(ω in T x. ev_at (HLD {y}) n (x ## ω))"

definition "F s t = 𝒫(ω in T s. ev (HLD {t}) (s ## ω))"

definition "gf_F x y z = (∑n. f x y n * z ^ n)"

lemma f_Suc: "x ≠ y ⟹ f x y (Suc n) = u x y n"

lemma f_Suc_eq: "f x x (Suc n) = 0"

lemma f_0: "f x y 0 = (if x = y then 1 else 0)"
using T.prob_space by (simp add: f_def)

lemma shows u_nonneg: "0 ≤ u x y n" and u_le_1: "u x y n ≤ 1"

lemma shows f_nonneg: "0 ≤ f x y n" and f_le_1: "f x y n ≤ 1"

lemma U_nonneg[simp]: "0 ≤ U x y"

lemma U_le_1: "U s t ≤ 1"
by (auto simp add: U_def intro!: antisym)

lemma U_cases: "U s s = 1 ∨ U s s < 1"
by (auto simp add: U_def intro!: antisym)

lemma u_sums_U: "u x y sums U x y"
unfolding u_def[abs_def] U_def ev_iff_ev_at by (intro T.prob_sums) (auto intro: ev_at_unique)

lemma gf_U_eq_U: "gf_U x y 1 = U x y"
using u_sums_U[THEN sums_unique] by (simp add: gf_U_def U_def)

lemma f_sums_F: "f x y sums F x y"
unfolding f_def[abs_def] F_def ev_iff_ev_at
by (intro T.prob_sums) (auto intro: ev_at_unique)

lemma F_nonneg[simp]: "0 ≤ F x y"
by (auto simp: F_def)

lemma F_le_1: "F x y ≤ 1"

lemma gf_F_eq_F: "gf_F x y 1 = F x y"
using f_sums_F[THEN sums_unique] by (simp add: gf_F_def F_def)

lemma gf_F_le_1:
fixes z :: real
assumes z: "0 ≤ z" "z ≤ 1"
shows "gf_F x y z ≤ 1"
proof -
have "gf_F x y z ≤ gf_F x y 1"
using z unfolding gf_F_def
by (intro suminf_le[OF _ summable_comparison_test[OF _ sums_summable[OF f_sums_F[of x y]]]] mult_left_mono allI f_nonneg)
(simp_all add: power_le_one f_nonneg mult_right_le_one_le f_le_1 sums_summable[OF f_sums_F[of x y]])
also have "… ≤ 1"
finally show ?thesis .
qed

lemma u_le_p: "u x y n ≤ p x y (Suc n)"
unfolding u_def p_def by (auto intro!: T.finite_measure_mono dest: ev_at_HLD_imp_snth)

lemma f_le_p: "f x y n ≤ p x y n"
unfolding f_def p_def by (auto intro!: T.finite_measure_mono dest: ev_at_HLD_imp_snth)

lemma convergence_norm_U:
fixes z :: "_ :: real_normed_div_algebra"
assumes z: "convergence_G x y z"
shows "summable (λn. u x y n * norm z ^ Suc n)"
using summable_ignore_initial_segment[OF convergence_norm_G[OF z], of 1]
by (rule summable_comparison_test[rotated])
(auto simp add: u_nonneg abs_mult intro!: exI[of _ 0] mult_right_mono u_le_p)

lemma convergence_norm_F:
fixes z :: "_ :: real_normed_div_algebra"
assumes z: "convergence_G x y z"
shows "summable (λn. f x y n * norm z ^ n)"
using convergence_norm_G[OF z]
by (rule summable_comparison_test[rotated])
(auto simp add: f_nonneg abs_mult intro!: exI[of _ 0] mult_right_mono f_le_p)

lemma gf_G_nonneg:
fixes z :: real
shows "0 ≤ z ⟹ z < 1 ⟹ 0 ≤ gf_G x y z"
unfolding gf_G_def
by (intro suminf_nonneg convergence_G convergence_G_less_1) simp_all

lemma gf_F_nonneg:
fixes z :: real
shows "0 ≤ z ⟹ z < 1 ⟹ 0 ≤ gf_F x y z"
unfolding gf_F_def
using convergence_norm_F[OF convergence_G_less_1, of z x y]
by (intro suminf_nonneg) (simp_all add: f_nonneg)

lemma convergence_U:
fixes z :: "_ :: banach"
shows "convergence_G x y z ⟹ summable (λn. u x y n * z ^ Suc n)"
by (rule summable_norm_cancel)
(auto simp add: abs_mult u_nonneg power_abs dest!: convergence_norm_U)

lemma p_eq_sum_p_u: "p x y (Suc n) = (∑i≤n. p y y (n - i) * u x y i)"
proof -
have "⋀ω. ω !! n = y ⟹ (∃i. i ≤ n ∧ ev_at (HLD {y}) i ω)"
proof (induction n)
case (Suc n)
then obtain i where "i ≤ n" "ev_at (HLD {y}) i (stl ω)"
by auto
then show ?case
by (auto intro!: exI[of _ "if HLD {y} ω then 0 else Suc i"])
then have "p x y (Suc n) = (∑i≤n. 𝒫(ω in T x. ev_at (HLD {y}) i ω ∧ ω !! n = y))"
unfolding p_def by (intro T.prob_sum) (auto intro: ev_at_unique)
also have "… = (∑i≤n. p y y (n - i) * u x y i)"
proof (intro sum.cong refl)
fix i assume i: "i ∈ {.. n}"
then have "⋀ω. (Suc i ≤ n ⟶ ω !! (n - Suc i) = y) ⟷ ((y ## ω) !! (n - i) = y)"
by (auto simp: Stream_snth diff_Suc split: nat.split)
from i have "i ≤ n" by auto
then have "𝒫(ω in T x. ev_at (HLD {y}) i ω ∧ ω !! n = y) =
(∫ω'. 𝒫(ω in T y. (y ## ω) !! (n - i) = y) *
indicator {ω'∈space (T x). ev_at (HLD {y}) i ω' } ω' ∂T x)"
by (subst prob_T_split[where n="Suc i"])
(auto simp: ev_at_shift ev_at_HLD_single_imp_snth shift_snth diff_Suc
split: split_indicator nat.split intro!: Bochner_Integration.integral_cong arg_cong2[where f=measure]
simp del: stake.simps integral_mult_right_zero)
then show "𝒫(ω in T x. ev_at (HLD {y}) i ω ∧ ω !! n = y) = p y y (n - i) * u x y i"
qed
finally show ?thesis .
qed

lemma p_eq_sum_p_f: "p x y n = (∑i≤n. p y y (n - i) * f x y i)"
by (cases n)
(simp_all del: sum.atMost_Suc
add: f_0 p_0 p_eq_sum_p_u atMost_Suc_eq_insert_0 zero_notin_Suc_image sum.reindex
f_Suc f_Suc_eq)

lemma gf_G_eq_gf_F:
assumes z: "norm z < 1"
shows "gf_G x y z = gf_F x y z * gf_G y y z"
proof -
have "gf_G x y z = (∑n. ∑i≤n. p y y (n - i) * f x y i * z^n)"
by (simp add: gf_G_def p_eq_sum_p_f[of x y] sum_distrib_right)
also have "… = (∑n. ∑i≤n. (f x y i * z^i) * (p y y (n - i) * z^(n - i)))"
by (intro arg_cong[where f=suminf] sum.cong ext atLeast0AtMost[symmetric])
also have "… = (∑n. f x y n * z^n) * (∑n. p y y n * z^n)"
using convergence_norm_F[OF convergence_G_less_1[OF z]] convergence_norm_G[OF convergence_G_less_1[OF z]]
by (intro Cauchy_product[symmetric]) (auto simp: f_nonneg abs_mult power_abs)
also have "… = gf_F x y z * gf_G y y z"
finally show ?thesis .
qed

lemma gf_G_eq_gf_U:
fixes z :: "'z :: {banach, real_normed_field}"
assumes z: "convergence_G x x z"
shows "gf_G x x z = 1 / (1 - gf_U x x z)" "gf_U x x z ≠ 1"
proof -
{ fix n
have "p x x (Suc n) *⇩R z^Suc n = (∑i≤n. (p x x (n - i) * u x x i) *⇩R z^Suc n)"
unfolding scaleR_sum_left[symmetric] by (simp add: p_eq_sum_p_u)
also have "… = (∑i≤n. (u x x i *⇩R z^Suc i) * (p x x (n - i) *⇩R z^(n - i)))"
by (intro sum.cong refl) (simp add: field_simps power_diff cong: disj_cong)
finally have "p x x (Suc n) *⇩R z^(Suc n) = (∑i≤n. (u x x i *⇩R z^Suc i) * (p x x (n - i) *⇩R z^(n - i)))"
unfolding atLeast0AtMost . }
note gfs_Suc_eq = this

have "gf_G x x z = 1 + (∑n. p x x (Suc n) *⇩R z^(Suc n))"
unfolding gf_G_def
by (subst suminf_split_initial_segment[OF convergence_G[OF z], of 1]) simp
also have "… = 1 + (∑n. ∑i≤n. (u x x i *⇩R z^Suc i) * (p x x (n - i) *⇩R z^(n - i)))"
unfolding gfs_Suc_eq ..
also have "… = 1 + gf_U x x z * gf_G x x z"
unfolding gf_U_def gf_G_def
by (subst Cauchy_product)
(auto simp: u_nonneg norm_power simp del: power_Suc
intro!: z convergence_norm_G convergence_norm_U)
finally show "gf_G x x z = 1 / (1 - gf_U x x z)" "gf_U x x z ≠ 1"
apply -
apply (cases "gf_U x x z = 1")
done
qed

lemma gf_U: "(gf_U x y ⤏ U x y) (at_left 1)"
proof -
have "((λz. ennreal (∑n. u x y n * z ^ n)) ⤏ (∑n. ennreal (u x y n))) (at_left 1)"
using u_le_1 u_nonneg by (intro power_series_tendsto_at_left summable_power_series)
also have "(∑n. ennreal (u x y n)) = ennreal (suminf (u x y))"
by (intro u_nonneg suminf_ennreal ennreal_suminf_neq_top sums_summable[OF u_sums_U])
also have "suminf (u x y) = U x y"
using u_sums_U by (rule sums_unique[symmetric])
finally have "((λz. ∑n. u x y n * z ^ n) ⤏ U x y) (at_left 1)"
by (rule tendsto_ennrealD)
(auto simp: u_nonneg u_le_1 intro!: suminf_nonneg summable_power_series eventually_at_left_1)
then have "((λz. z * (∑n. u x y n * z ^ n)) ⤏ 1 * U x y) (at_left 1)"
by (intro tendsto_intros) simp
then have "((λz. ∑n. u x y n * z ^ Suc n) ⤏ 1 * U x y) (at_left 1)"
apply (rule filterlim_cong[OF refl refl, THEN iffD1, rotated])
apply (rule eventually_at_left_1)
apply (subst suminf_mult[symmetric])
apply (auto intro!: summable_power_series u_le_1 u_nonneg)
done
then show ?thesis
qed

lemma gf_U_le_1: assumes z: "0 < z" "z < 1" shows "gf_U x y z ≤ (1::real)"
proof -
note u = u_sums_U[of x y, THEN sums_summable]
have "gf_U x y z ≤ gf_U x y 1"
using z
unfolding gf_U_def real_scaleR_def
by (intro suminf_le allI mult_mono power_mono summable_comparison_test_ev[OF _ u] always_eventually)
(auto simp: u_nonneg intro!: mult_left_le mult_le_one power_le_one)
also have "… ≤ 1"
unfolding gf_U_eq_U by (rule U_le_1)
finally show ?thesis .
qed

lemma gf_F: "(gf_F x y ⤏ F x y) (at_left 1)"
proof -
have "((λz. ennreal (∑n. f x y n * z ^ n)) ⤏ (∑n. ennreal (f x y n))) (at_left 1)"
using f_le_1 f_nonneg by (intro power_series_tendsto_at_left summable_power_series)
also have "(∑n. ennreal (f x y n)) = ennreal (suminf (f x y))"
by (intro f_nonneg suminf_ennreal ennreal_suminf_neq_top sums_summable[OF f_sums_F])
also have "suminf (f x y) = F x y"
using f_sums_F by (rule sums_unique[symmetric])
finally have "((λz. ∑n. f x y n * z ^ n) ⤏ F x y) (at_left 1)"
by (rule tendsto_ennrealD)
(auto simp: f_nonneg f_le_1 intro!: suminf_nonneg summable_power_series eventually_at_left_1)
then show ?thesis
qed

lemma U_bounded: "0 ≤ U x y" "U x y ≤ 1"
unfolding U_def by simp_all

subsection ‹Recurrent states›

definition recurrent :: "'s ⇒ bool" where
"recurrent s ⟷ (AE ω in T s. ev (HLD {s}) ω)"

lemma recurrent_iff_U_eq_1: "recurrent s ⟷ U s s = 1"
unfolding recurrent_def U_def by (subst T.prob_Collect_eq_1) simp_all

definition "H s t = 𝒫(ω in T s. alw (ev (HLD {t})) ω)"

lemma H_eq:
"recurrent s ⟷ H s s = 1"
"¬ recurrent s ⟷ H s s = 0"
"H s t = U s t * H t t"
proof -
define H' where "H' t n = {ω∈space S. enat n ≤ scount (HLD {t::'s}) ω}" for t n
have [measurable]: "⋀y n. H' y n ∈ sets S"
let ?H' = "λs t n. measure (T s) (H' t n)"
{ fix x y :: 's and ω
have "Suc 0 ≤ scount (HLD {y}) ω ⟷ ev (HLD {y}) ω"
using scount_eq_0_iff[of "HLD {y}" ω]
by (cases "scount (HLD {y}) ω" rule: enat_coexhaust)
(auto simp: not_ev_iff[symmetric] eSuc_enat[symmetric] enat_0 HLD_iff[abs_def]) }
then have H'_1: "⋀x y. ?H' x y 1 = U x y"
unfolding H'_def U_def by simp

{ fix n and x y :: 's
let ?U = "(not (HLD {y}) suntil (HLD {y} aand nxt (λω. enat n ≤ scount (HLD {y}) ω)))"
{ fix ω
have "enat (Suc n) ≤ scount (HLD {y}) ω ⟷ ?U ω"
proof
assume "enat (Suc n) ≤ scount (HLD {y}) ω"
with scount_eq_0_iff[of "HLD {y}" ω] have "ev (HLD {y}) ω" "enat (Suc n) ≤ scount (HLD {y}) ω"
by (auto simp add: not_ev_iff[symmetric] eSuc_enat[symmetric])
then show "?U ω"
by (induction rule: ev_induct_strong)
(auto simp: scount_simps eSuc_enat[symmetric] intro: suntil.intros)
next
assume "?U ω" then show "enat (Suc n) ≤ scount (HLD {y}) ω"
by induction (auto simp: scount_simps  eSuc_enat[symmetric])
qed }
then have "emeasure (T x) (H' y (Suc n)) = emeasure (T x) {ω∈space (T x). ?U ω}"
also have "… = U x y * ?H' y y n"
by (subst emeasure_suntil_HLD) (simp_all add: T.emeasure_eq_measure U_def H'_def ennreal_mult)
finally have "?H' x y (Suc n) = U x y * ?H' y y n"
note H'_Suc = this

{ fix m and x :: 's
have "?H' x x (Suc m) = U x x^Suc m"
using H'_1 H'_Suc by (induct m) auto }
note H'_eq = this

{ fix x y
have "?H' x y ⇢ measure (T x) (⋂i. H' y i)"
proof (rule T.finite_Lim_measure_decseq)
show "range (H' y) ⊆ T.events x"
by auto
next
show "decseq (H' y)"
by (rule antimonoI) (simp add: subset_eq H'_def order_subst2)
qed
also have "(⋂i. H' y i) = {ω∈space (T x). alw (ev (HLD {y})) ω}"
by (auto simp: H'_def scount_infinite_iff[symmetric]) (metis Suc_ile_eq enat.exhaust neq_iff)
finally have "?H' x y ⇢ H x y"
unfolding H_def . }
note H'_lim = this

from H'_lim[of s s, THEN LIMSEQ_Suc]
have "(λn. U s s ^ Suc n) ⇢ H s s"
then have lim_H: "(λn. U s s ^ n) ⇢ H s s"
by (rule LIMSEQ_imp_Suc)

have "U s s < 1 ⟹ (λn. U s s ^ n) ⇢ 0"
by (rule LIMSEQ_realpow_zero) (simp_all add: U_def)
with lim_H have "U s s < 1 ⟹ H s s = 0"
by (blast intro: LIMSEQ_unique)
moreover have "U s s = 1 ⟹ (λn. U s s ^ n) ⇢ 1"
by simp
with lim_H have "U s s = 1 ⟹ H s s = 1"
by (blast intro: LIMSEQ_unique)
moreover note recurrent_iff_U_eq_1 U_cases
ultimately show "recurrent s ⟷ H s s = 1" "¬ recurrent s ⟷ H s s = 0"
by (metis one_neq_zero)+

from H'_lim[of s t, THEN LIMSEQ_Suc] H'_Suc[of s]
have "(λn. U s t * ?H' t t n) ⇢ H s t"
by simp
moreover have "(λn. U s t * ?H' t t n) ⇢ U s t * H t t"
by (intro tendsto_intros H'_lim)
ultimately show "H s t = U s t * H t t"
by (blast intro: LIMSEQ_unique)
qed

lemma recurrent_iff_G_infinite: "recurrent x ⟷ G x x = ∞"
proof -
have "((λz. ennreal (gf_G x x z)) ⤏ G x x) (at_left 1)"
by (rule lim_gf_G)
then have G: "((λz. ennreal (1 / (1 - gf_U x x z))) ⤏ G x x) (at_left (1::real))"
apply (rule filterlim_cong[OF refl refl, THEN iffD1, rotated])
apply (rule eventually_at_left_1)
apply (subst gf_G_eq_gf_U)
apply (rule convergence_G_less_1)
apply simp
apply simp
done

{ fix z :: real assume z: "0 < z" "z < 1"
have 1: "summable (u x x)"
using u_sums_U by (rule sums_summable)
have "gf_U x x z ≠ 1"
using gf_G_eq_gf_U[OF convergence_G_less_1[of z]] z by simp
moreover
have "gf_U x x z ≤ U x x"
unfolding gf_U_def gf_U_eq_U[symmetric]
using z
by (intro suminf_le)
(auto simp add: 1 convergence_U convergence_G_less_1 u_nonneg simp del: power_Suc
intro!: mult_right_le_one_le power_le_one)
ultimately have "gf_U x x z < 1"
using U_bounded[of x x] by simp }
note strict = this

{ assume "U x x = 1"
moreover have "((λxa. 1 - gf_U x x xa :: real) ⤏ 1 - U x x) (at_left 1)"
by (intro tendsto_intros gf_U)
moreover have "eventually (λz. gf_U x x z < 1) (at_left (1::real))"
by (auto intro!: eventually_at_left_1 strict simp: ‹U x x = 1› gf_U_eq_U)
ultimately have "((λz. ennreal (1 / (1 - gf_U x x z))) ⤏ top) (at_left 1)"
unfolding ennreal_tendsto_top_eq_at_top
by (intro LIM_at_top_divide[where a=1] tendsto_const zero_less_one)
(auto simp: field_simps)
with G have "G x x = top"
by (rule tendsto_unique[rotated]) simp }
moreover
{ assume "U x x < 1"
then have "((λxa. ennreal (1 / (1 - gf_U x x xa))) ⤏ 1 / (1 - U x x)) (at_left 1)"
by (intro tendsto_intros gf_U tendsto_ennrealI) simp
from tendsto_unique[OF _ G this] have "G x x ≠ ∞"
by simp }
ultimately show ?thesis
using U_cases recurrent_iff_U_eq_1 by auto
qed

definition communicating :: "('s × 's) set" where
"communicating = acc ∩ acc¯"

definition essential_class :: "'s set ⇒ bool" where
"essential_class C ⟷ C ∈ UNIV // communicating ∧ acc `` C ⊆ C"

lemma accI_U:
assumes "0 < U x y" shows "(x, y) ∈ acc"
proof (rule ccontr)
assume *: "(x, y) ∉ acc"

{ fix ω assume "ev (HLD {y}) ω" "alw (HLD (acc `` {x})) ω" from this * have False
by induction (auto simp: HLD_iff) }
with AE_T_reachable[of x] have "U x y = 0"
unfolding U_def by (intro T.prob_eq_0_AE) auto
with ‹0 < U x y› show False by auto
qed

lemma accD_pos:
assumes "(x, y) ∈ acc"
shows "∃n. 0 < p x y n"
using assms proof induction
case base with T.prob_space[of x] show ?case
by (auto intro!: exI[of _ 0])
next
have [simp]: "⋀x y. (if x = y then 1 else 0::real) = indicator {y} x"
by simp
case (step w y)
then obtain n where "0 < p x w n" and "0 < pmf (K w) y"
by (auto simp: set_pmf_iff less_le)
then have "0 < p x w n * pmf (K w) y"
by (intro mult_pos_pos)
also have "… ≤ p x w n * p w y (Suc 0)"
by (simp add: p_Suc' p_0 pmf.rep_eq)
also have "… ≤ p x y (Suc n)"
using prob_reachable_le[of n "Suc n" x w y] by simp
finally show ?case ..
qed

lemma accI_pos: "0 < p x y n ⟹ (x, y) ∈ acc"
proof (induct n arbitrary: x)
case (Suc n)
then have less: "0 < (∫x'. p x' y n ∂K x)"
have "∃x'∈K x. 0 < p x' y n"
proof (rule ccontr)
assume "¬ ?thesis"
then have "AE x' in K x. p x' y n = 0"
then have "(∫x'. p x' y n ∂K x) = (∫x'. 0 ∂K x)"
by (intro integral_cong_AE) simp_all
with less show False by simp
qed
with Suc show ?case
by (auto intro: converse_rtrancl_into_rtrancl)
qed (simp add: p_0 split: if_split_asm)

lemma recurrent_iffI_communicating:
assumes "(x, y) ∈ communicating"
shows "recurrent x ⟷ recurrent y"
proof -
from assms obtain n m where "0 < p x y n" "0 < p y x m"
by (force simp: communicating_def dest: accD_pos)
moreover
{ fix x y n m assume "0 < p x y n" "0 < p y x m" "G y y = ∞"
then have "∞ = ennreal (p x y n * p y x m) * G y y"
by (auto intro: mult_pos_pos simp: ennreal_mult_top)
also have "ennreal (p x y n * p y x m) * G y y = (∑i. ennreal (p x y n * p y x m) * p y y i)"
unfolding G_eq_suminf by (rule ennreal_suminf_cmult[symmetric])
also have "… ≤ (∑i. ennreal (p x x (n + i + m)))"
proof (intro suminf_le allI)
fix i
have "(p x y n * p y y ((n + i) - n)) * p y x ((n + i + m) - (n + i)) ≤ p x y (n + i) * p y x ((n + i + m) - (n + i))"
by (intro mult_right_mono prob_reachable_le) simp_all
also have "… ≤ p x x (n + i + m)"
by (intro prob_reachable_le) simp_all
finally show "ennreal (p x y n * p y x m) * p y y i ≤ ennreal (p x x (n + i + m))"
qed auto
also have "… ≤ (∑i. ennreal (p x x (i + (n + m))))"
also have "… ≤ (∑i. ennreal (p x x i))"
by (subst suminf_offset[of "λi. ennreal (p x x i)" "n + m"]) auto
also have "… ≤ G x x"
unfolding G_eq_suminf by (auto intro!: suminf_le_pos)
finally have "G x x = ∞"
ultimately show ?thesis
using recurrent_iff_G_infinite by blast
qed

lemma recurrent_acc:
assumes "recurrent x" "(x, y) ∈ acc"
shows "U y x = 1" "H y x = 1" "recurrent y" "(x, y) ∈ communicating"
proof -
{ fix w y assume step: "(x, w) ∈ acc" "y ∈ K w" "U w x = 1" "H w x = 1" "recurrent w" "x ≠ y"
have "measure (K w) UNIV = U w x"
using step measure_pmf.prob_space[of "K w"] by simp
also have "… = (∫v. indicator {x} v + U v x * indicator (- {x}) v ∂K w)"
unfolding U_def
by (subst prob_T)
(auto intro!: Bochner_Integration.integral_cong arg_cong2[where f=measure] AE_I2
simp: ev_Stream T.prob_eq_1 split: split_indicator)
also have "… = measure (K w) {x} + (∫v. U v x * indicator (- {x}) v ∂K w)"
(auto intro!: measure_pmf.integrable_const_bound[where B=1]
simp: abs_mult mult_le_one U_bounded(2) measure_pmf.emeasure_eq_measure)
finally have "measure (K w) UNIV - measure (K w) {x} = (∫v. U v x * indicator (- {x}) v ∂K w)"
by simp
also have "measure (K w) UNIV - measure (K w) {x} = measure (K w) (UNIV - {x})"
by (subst measure_pmf.finite_measure_Diff) auto
finally have "0 = (∫v. indicator (- {x}) v ∂K w) - (∫v. U v x * indicator (- {x}) v ∂K w)"
also have "… = (∫v. (1 - U v x) * indicator (- {x}) v ∂K w)"
by (subst Bochner_Integration.integral_diff[symmetric])
(auto intro!: measure_pmf.integrable_const_bound[where B=1] Bochner_Integration.integral_cong
simp: abs_mult mult_le_one U_bounded(2) split: split_indicator)
also have "… ≥ (∫v. (1 - U y x) * indicator {y} v ∂K w)" (is "_ ≥ ?rhs")
using ‹recurrent x›
by (intro integral_mono measure_pmf.integrable_const_bound[where B=1])
(auto simp: abs_mult mult_le_one U_bounded(2) recurrent_iff_U_eq_1 field_simps
split: split_indicator)
also (xtrans) have "?rhs = (1 - U y x) * pmf (K w) y"
finally have "(1 - U y x) * pmf (K w) y = 0"
by (auto intro!: antisym simp: U_bounded(2) mult_le_0_iff)
with ‹y ∈ K w› have "U y x = 1"
then have "U y x = 1" "H y x = 1"
using H_eq(3)[of y x] H_eq(1)[of x] by (simp_all add: ‹recurrent x›)
then have "(y, x) ∈ acc"
by (intro accI_U) auto
with step have "(x, y) ∈ communicating"
by (auto simp add: communicating_def intro: rtrancl_trans)
with ‹recurrent x› have "recurrent y"
note this ‹U y x = 1› ‹H y x = 1› ‹(x, y) ∈ communicating› }
note enabled = this

from ‹(x, y) ∈ acc›
show "U y x = 1" "H y x = 1" "recurrent y" "(x, y) ∈ communicating"
proof induction
case base then show "U x x = 1" "H x x = 1" "recurrent x" "(x, x) ∈ communicating"
using ‹recurrent x› H_eq(1)[of x] by (auto simp: recurrent_iff_U_eq_1 communicating_def)
next
case (step w y)
with enabled[of w y] ‹recurrent x› H_eq(1)[of x]
have "U y x = 1 ∧ H y x = 1 ∧ recurrent y ∧ (x, y) ∈ communicating"
by (cases "x = y") (auto simp: recurrent_iff_U_eq_1 communicating_def)
then show "U y x = 1" "H y x = 1" "recurrent y" "(x, y) ∈ communicating"
by auto
qed
qed

lemma equiv_communicating: "equiv UNIV communicating"
by (auto simp: equiv_def sym_def communicating_def refl_on_def trans_def)

lemma recurrent_class:
assumes "recurrent x"
shows "acc `` {x} = communicating `` {x}"
using recurrent_acc(4)[OF ‹recurrent x›] by (auto simp: communicating_def)

lemma irreduccible_recurrent_class:
assumes "recurrent x" shows "acc `` {x} ∈ UNIV // communicating"
unfolding recurrent_class[OF ‹recurrent x›] by (rule quotientI) simp

lemma essential_classI:
assumes C: "C ∈ UNIV // communicating"
assumes eq: "⋀x y. x ∈ C ⟹ (x, y) ∈ acc ⟹ y ∈ C"
shows "essential_class C"
by (auto simp: essential_class_def intro: C) (metis eq)

lemma essential_recurrent_class:
assumes "recurrent x" shows "essential_class (communicating `` {x})"
unfolding recurrent_class[OF ‹recurrent x›, symmetric]
apply (rule essential_classI)
apply (rule irreduccible_recurrent_class[OF assms])
apply (auto simp: communicating_def)
done

lemma essential_classD2:
"essential_class C ⟹ x ∈ C ⟹ (x, y) ∈ acc ⟹ y ∈ C"
unfolding essential_class_def by auto

lemma essential_classD3:
"essential_class C ⟹ x ∈ C ⟹ y ∈ C ⟹ (x, y) ∈ communicating"
unfolding essential_class_def
by (auto elim!: quotientE simp: communicating_def)

lemma AE_acc:
shows "AE ω in T x. ∀m. (x, (x ## ω) !! m) ∈ acc"
using AE_T_reachable
by eventually_elim (auto simp: alw_HLD_iff_streams streams_iff_snth Stream_snth split: nat.splits)

lemma finite_essential_class_imp_recurrent:
assumes C: "essential_class C" "finite C" and x: "x ∈ C"
shows "recurrent x"
proof -
have "AE ω in T x. ∃y∈C. alw (ev (HLD {y})) ω"
using AE_T_reachable
proof eventually_elim
fix ω assume "alw (HLD (acc `` {x})) ω"
then have "alw (HLD C) ω"
by (rule alw_mono) (auto simp: HLD_iff intro: assms essential_classD2)
then show "∃y∈C. alw (ev (HLD {y})) ω"
by (rule pigeonhole_stream) fact
qed
then have "1 = 𝒫(ω in T x. ∃y∈C. alw (ev (HLD {y})) ω)"
by (subst (asm) T.prob_Collect_eq_1[symmetric]) (auto simp: ‹finite C›)
also have "… = measure (T x) (⋃y∈C. {ω∈space (T x). alw (ev (HLD {y})) ω})"
by (intro arg_cong2[where f=measure]) auto
also have "… ≤ (∑y∈C. H x y)"
unfolding H_def using ‹finite C› by (rule T.finite_measure_subadditive_finite) auto
also have "… = (∑y∈C. U x y * H y y)"
by (auto intro!: sum.cong H_eq)
finally have "∃y∈C. recurrent y"
by (rule_tac ccontr) (simp add: H_eq(2))
then obtain y where "y ∈ C" "recurrent y" ..
from essential_classD3[OF C(1) x this(1)] recurrent_acc(3)[OF this(2)]
show "recurrent x"
qed

lemma irreducibleD:
"C ∈ UNIV // communicating ⟹ a ∈ C ⟹ b ∈ C ⟹ (a, b) ∈ communicating"
by (auto elim!: quotientE simp: communicating_def)

lemma irreducibleD2:
"C ∈ UNIV // communicating ⟹ a ∈ C ⟹ (a, b) ∈ communicating ⟹ b ∈ C"
by (auto elim!: quotientE simp: communicating_def)

lemma essential_class_iff_recurrent:
"finite C ⟹ C ∈ UNIV // communicating ⟹ essential_class C ⟷ (∀x∈C. recurrent x)"
by (metis finite_essential_class_imp_recurrent irreducibleD2 recurrent_acc(4) essential_classI)

definition "U' x y = (∫⇧+ω. eSuc (sfirst (HLD {y}) ω) ∂T x)"

lemma U'_neq_zero[simp]: "U' x y ≠ 0"

definition "gf_U' x y z = (∑n. u x y n * Suc n * z ^ n)"

definition "pos_recurrent x ⟷ recurrent x ∧ U' x x ≠ ∞"

lemma summable_gf_U':
assumes z: "norm z < 1"
shows "summable (λn. u x y n * Suc n * z ^ n)"
proof -
have "summable (λn. n * ¦z¦ ^ n)"
proof (rule root_test_convergence)
have "(λn. root n n * ¦z¦) ⇢ 1 * ¦z¦"
by (intro tendsto_intros LIMSEQ_root)
then show "(λn. root n (norm (n * ¦z¦ ^ n))) ⇢ ¦z¦"
by (rule filterlim_cong[THEN iffD1, rotated 3])
(auto intro!: exI[of _ 1]
simp add: abs_mult u_nonneg real_root_mult power_abs eventually_sequentially real_root_power)
qed (insert z, simp add: abs_less_iff)
note summable_mult[OF this, of "1 / ¦z¦"]
from summable_ignore_initial_segment[OF this, of 1]
show "summable (λn. u x y n * Suc n * z ^ n)"
apply (rule summable_comparison_test[rotated])
using z
apply (auto intro!: exI[of _ 1]
simp: abs_mult u_nonneg power_abs Suc_le_eq gr0_conv_Suc field_simps le_divide_eq u_le_1
simp del: of_nat_Suc)
done
qed

lemma gf_U'_nonneg[simp]: "0 < z ⟹ z < 1 ⟹ 0 ≤ gf_U' x y z"
unfolding gf_U'_def
by (intro suminf_nonneg summable_gf_U') (auto simp: u_nonneg)

lemma DERIV_gf_U:
fixes z :: real assumes z: "0 < z" "z < 1"
shows "DERIV (gf_U x y) z :> gf_U' x y z"
unfolding gf_U_def[abs_def]  gf_U'_def real_scaleR_def u_def[symmetric]
using z by (intro DERIV_power_series'[where R=1] summable_gf_U') auto

lemma sfirst_finiteI_recurrent:
"recurrent x ⟹ (x, y) ∈ acc ⟹ AE ω in T x. sfirst (HLD {y}) ω < ∞"
using recurrent_acc(1)[of y x] recurrent_acc[of x y]
T.AE_prob_1[of x "{ω∈space (T x). ev (HLD {y}) ω}"]
unfolding sfirst_finite U_def by (simp add: space_stream_space communicating_def)

lemma U'_eq_suminf:
assumes x: "recurrent x" "(x, y) ∈ acc"
shows "U' x y = (∑i. ennreal (u x y i * Suc i))"
proof -
have "(∫⇧+ω. eSuc (sfirst (HLD {y}) ω) ∂T x) =
(∫⇧+ω. (∑i. ennreal (Suc i) * indicator {ω∈space (T y). ev_at (HLD {y}) i ω} ω) ∂T x)"
using sfirst_finiteI_recurrent[OF x]
proof (intro nn_integral_cong_AE, eventually_elim)
fix ω assume "sfirst (HLD {y}) ω < ∞"
then obtain n :: nat where [simp]: "sfirst (HLD {y}) ω = n"
by auto
show "eSuc (sfirst (HLD {y}) ω) = (∑i. ennreal (Suc i) * indicator {ω∈space (T y). ev_at (HLD {y}) i ω} ω)"
by (subst suminf_cmult_indicator[where i=n])
(auto simp: disjoint_family_on_def ev_at_unique space_stream_space
sfirst_eq_enat_iff[symmetric] ennreal_of_nat_eq_real_of_nat
split: split_indicator)
qed
also have "… = (∑i. ennreal (Suc i) * emeasure (T x) {ω∈space (T x). ev_at (HLD {y}) i ω})"
by (subst nn_integral_suminf)
(auto intro!: arg_cong[where f=suminf] nn_integral_cmult_indicator simp: fun_eq_iff)
finally show ?thesis
by (simp add: U'_def u_def T.emeasure_eq_measure mult_ac ennreal_mult)
qed

lemma gf_U'_tendsto_U':
assumes x: "recurrent x" "(x, y) ∈ acc"
shows "((λz. ennreal (gf_U' x y z)) ⤏ U' x y) (at_left 1)"
unfolding U'_eq_suminf[OF x] gf_U'_def
by (auto intro!: power_series_tendsto_at_left summable_gf_U' mult_nonneg_nonneg u_nonneg simp del: of_nat_Suc)

lemma one_le_integral_t:
assumes x: "recurrent x" shows "1 ≤ U' x x"

lemma gf_U'_pos:
fixes z :: real
assumes z: "0 < z" "z < 1" and "U x y ≠ 0"
shows "0 < gf_U' x y z"
unfolding gf_U'_def
proof (subst suminf_pos_iff)
show "summable (λn. u x y n * real (Suc n) * z ^ n)"
using z by (intro summable_gf_U') simp
show pos: "⋀n. 0 ≤ u x y n * real (Suc n) * z ^ n"
using u_nonneg z by auto
show "∃n. 0 < u x y n * real (Suc n) * z ^ n"
proof (rule ccontr)
assume "¬ (∃n. 0 < u x y n * real (Suc n) * z ^ n)"
with pos have "∀n. u x y n * real (Suc n) * z ^ n = 0"
by (intro antisym allI) (simp_all add: not_less)
with z have "u x y = (λn. 0)"
by (intro ext) simp
with u_sums_U[of x y, THEN sums_unique] ‹U x y ≠ 0› show False
by simp
qed
qed

lemma inverse_gf_U'_tendsto:
assumes "recurrent y"
shows "((λx. - 1 / - gf_U' y y x) ⤏ enn2real (1 / U' y y)) (at_left (1::real))"
proof cases
assume inf: "U' y y = ∞"
with gf_U'_tendsto_U'[of y y] ‹recurrent y›
have "LIM z (at_left 1). gf_U' y y z :> at_top"
by (auto simp: ennreal_tendsto_top_eq_at_top U'_def)
then have "LIM z (at_left 1). gf_U' y y z :> at_infinity"
by (rule filterlim_mono) (auto simp: at_top_le_at_infinity)
with inf show ?thesis
by (auto intro!: tendsto_divide_0)
next
assume fin: "U' y y ≠ ∞"
then obtain r where r: "U' y y = ennreal r" and [simp]: "0 ≤ r"
by (cases "U' y y") (auto simp: U'_def)
then have eq: "enn2real (1 / U' y y) = - 1 / - r" and "1 ≤ r"
using one_le_integral_t[OF ‹recurrent y›]
by (auto simp add: ennreal_1[symmetric] divide_ennreal simp del: ennreal_1)
have "((λz. ennreal (gf_U' y y z)) ⤏ ennreal r) (at_left 1)"
using gf_U'_tendsto_U'[OF ‹recurrent y›, of y] r by simp
then have gf_U': "(gf_U' y y ⤏ r) (at_left (1::real))"
by (rule tendsto_ennrealD)
(insert summable_gf_U', auto intro!: eventually_at_left_1 suminf_nonneg simp: gf_U'_def u_nonneg)
show ?thesis
using ‹1 ≤ r› unfolding eq by (intro tendsto_intros gf_U') simp
qed

lemma gf_G_pos:
fixes z :: real
assumes z: "0 < z" "z < 1" and *: "(x, y) ∈ acc"
shows "0 < gf_G x y z"
unfolding gf_G_def
proof (subst suminf_pos_iff)
show "summable (λn. p x y n *⇩R z ^ n)"
using z by (intro convergence_G convergence_G_less_1) simp
show pos: "⋀n. 0 ≤ p x y n *⇩R z ^ n"
using z by (auto intro!: mult_nonneg_nonneg p_nonneg)
show "∃n. 0 < p x y n *⇩R z ^ n"
proof (rule ccontr)
assume "¬ (∃n. 0 < p x y n *⇩R z ^ n)"
with pos have "∀n. p x y n * z ^ n = 0"
by (intro antisym allI) (simp_all add: not_less)
with z have "⋀n. p x y n = 0"
by simp
with *[THEN accD_pos] show False
by simp
qed
qed

lemma pos_recurrentI_communicating:
assumes y: "pos_recurrent y" and x: "(y, x) ∈ communicating"
shows "pos_recurrent x"
proof -
from y x have recurrent: "recurrent y" "recurrent x" and fin: "U' y y ≠ ∞"
by (auto simp: pos_recurrent_def recurrent_iffI_communicating nn_integral_add)
have pos: "0 < enn2real (1 / U' y y)"
using one_le_integral_t[OF ‹recurrent y›] fin
by (auto simp: U'_def enn2real_positive_iff less_top[symmetric] ennreal_zero_less_divide ennreal_divide_eq_top_iff)

from fin obtain r where r: "U' y y = ennreal r" and [simp]: "0 ≤ r"
by (cases "U' y y") (auto simp: U'_def)

from x obtain n m where "0 < p x y n" "0 < p y x m"
by (auto dest!: accD_pos simp: communicating_def)

let ?L = "at_left (1::real)"
have le: "eventually (λz. p x y n * p y x m * z^(n + m) ≤ (1 - gf_U y y z) / (1 - gf_U x x z)) ?L"
proof (rule eventually_at_left_1)
fix z :: real assume z: "0 < z" "z < 1"
then have conv: "⋀x. convergence_G x x z"
by (intro convergence_G_less_1) simp
have sums: "(λi. (p x y n * p y x m * z^(n + m)) * (p y y i * z^i)) sums ((p x y n * p y x m * z^(n + m)) * gf_G y y z)"
unfolding gf_G_def
by (intro sums_mult summable_sums) (auto intro!: conv convergence_G[where 'a=real, simplified])
have "(∑i. (p x y n * p y x m * z^(n + m)) * (p y y i * z^i)) ≤ (∑i. p x x (i + (n + m)) * z^(i + (n + m)))"
proof (intro allI suminf_le sums_summable[OF sums] summable_ignore_initial_segment convergence_G[where 'a=real, simplified] convergence_G_less_1)
show "norm z < 1" using z by simp
fix i
have "(p x y n * p y y ((n + i) - n)) * p y x ((n + i + m) - (n + i)) ≤ p x y (n + i) * p y x ((n + i + m) - (n + i))"
by (intro mult_right_mono prob_reachable_le) simp_all
also have "… ≤ p x x (n + i + m)"
by (intro prob_reachable_le) simp_all
finally show "p x y n * p y x m * z ^ (n + m) * (p y y i * z ^ i) ≤ p x x (i + (n + m)) * z ^ (i + (n + m))"
qed
also have "… ≤ gf_G x x z"
unfolding gf_G_def
using z
apply (subst (2) suminf_split_initial_segment[where k="n + m"])
apply (intro convergence_G conv)
done
finally have "(p x y n * p y x m * z^(n + m)) * gf_G y y z ≤ gf_G x x z"
using sums_unique[OF sums] by simp
then have "(p x y n * p y x m * z^(n + m)) ≤ gf_G x x z / gf_G y y z"
using z gf_G_pos[of z y y] by (simp add: field_simps)
also have "… = (1 - gf_U y y z) / (1 - gf_U x x z)"
unfolding gf_G_eq_gf_U[OF conv] using gf_G_eq_gf_U(2)[OF conv] by (simp add: field_simps )
finally show "p x y n * p y x m * z^(n + m) ≤ (1 - gf_U y y z) / (1 - gf_U x x z)" .
qed

have "U' x x ≠ ∞"
proof
assume "U' x x = ∞"
have "((λz. (1 - gf_U y y z) / (1 - gf_U x x z)) ⤏ 0) ?L"
proof (rule lhopital_left)
show "((λz. 1 - gf_U y y z) ⤏ 0) ?L"
using gf_U[of y] recurrent_iff_U_eq_1[of y] ‹recurrent y› by (auto intro!: tendsto_eq_intros)
show "((λz. 1 - gf_U x x z) ⤏ 0) ?L"
using gf_U[of x] recurrent_iff_U_eq_1[of x] ‹recurrent x› by (auto intro!: tendsto_eq_intros)
show "eventually (λz. 1 - gf_U x x z ≠ 0) ?L"
by (auto intro!: eventually_at_left_1 simp: gf_G_eq_gf_U(2) convergence_G_less_1)
show "eventually (λz. - gf_U' x x z ≠ 0) ?L"
using gf_U'_pos[of _ x x] recurrent_iff_U_eq_1[of x] ‹recurrent x›
by (auto intro!: eventually_at_left_1) (metis less_le)
show "eventually (λz. DERIV (λxa. 1 - gf_U x x xa) z :> - gf_U' x x z) ?L"
by (auto intro!: eventually_at_left_1 derivative_eq_intros DERIV_gf_U)
show "eventually (λz. DERIV (λxa. 1 - gf_U y y xa) z :> - gf_U' y y z) ?L"
by (auto intro!: eventually_at_left_1 derivative_eq_intros DERIV_gf_U)

have "(gf_U' y y ⤏ U' y y) ?L"
using ‹recurrent y› by (rule gf_U'_tendsto_U') simp
then have *: "(gf_U' y y ⤏ r) ?L"
by (auto simp add: r eventually_at_left_1 dest!: tendsto_ennrealD)
moreover
have "(gf_U' x x ⤏ U' x x) ?L"
using ‹recurrent x› by (rule gf_U'_tendsto_U') simp
then have "LIM z ?L. - gf_U' x x z :> at_bot"
by (simp add: ennreal_tendsto_top_eq_at_top ‹U' x x = ∞› filterlim_uminus_at_top
del: ennreal_of_enat_eSuc)
then have "LIM z ?L. - gf_U' x x z :> at_infinity"
by (rule filterlim_mono) (auto simp: at_bot_le_at_infinity)
ultimately show "((λz. - gf_U' y y z / - gf_U' x x z) ⤏ 0) ?L"
by (intro tendsto_divide_0[where c="- r"] tendsto_intros)
qed
moreover
have "((λz. p x y n * p y x m * z^(n + m)) ⤏ p x y n * p y x m) ?L"
by (auto intro!: tendsto_eq_intros)
ultimately have "p x y n * p y x m ≤ 0"
using le by (rule tendsto_le[OF trivial_limit_at_left_real])
with ‹0 < p x y n› ‹0 < p y x m› show False
qed
with ‹recurrent x› show ?thesis
qed

lemma pos_recurrent_iffI_communicating:
"(y, x) ∈ communicating ⟹ pos_recurrent y ⟷ pos_recurrent x"
using pos_recurrentI_communicating[of x y] pos_recurrentI_communicating[of y x]

lemma U_le_F: "U x y ≤ F x y"
by (auto simp: U_def F_def intro!: T.finite_measure_mono)

lemma not_empty_irreducible: "C ∈ UNIV // communicating ⟹ C ≠ {}"
by (auto simp: quotient_def Image_def communicating_def)

subsection ‹Stationary distribution›

definition stat :: "'s set ⇒ 's measure" where
"stat C = point_measure UNIV (λx. indicator C x / U' x x)"

lemma sets_stat[simp]: "sets (stat C) = sets (count_space UNIV)"