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
    by (auto simp del: of_nat_add simp add: of_nat_add [symmetric])
  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. nN. 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. nN. 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"
  by (simp add: p_def)

lemma p_le_1: "p x y n  1"
  by (simp add: p_def)

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)"
    by (simp add: p_Suc Suc)
  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)"
    by (simp add: nn_integral_multc[symmetric] ennreal_mult)
  finally show ?case
    by (simp add: ennreal_mult p_Suc)
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))"
    by (subst p_add)
       (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. nN. norm (p x y n * norm z ^ n)  norm z ^ n"
    by (simp add: norm_power)
qed (simp add: z summable_geometric)

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"
  by (simp add: u_def f_def)

lemma f_Suc_eq: "f x x (Suc n) = 0"
  by (simp add: f_def)

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"
  by (simp_all add: u_def)

lemma shows f_nonneg: "0  f x y n" and f_le_1: "f x y n  1"
  by (simp_all add: f_def)

lemma U_nonneg[simp]: "0  U x y"
  by (simp add: U_def)

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"
  by (simp add: F_def)

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"
    by (simp add: gf_F_eq_F F_def)
  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) = (in. 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"])
  qed (simp add: HLD_iff)
  then have "p x y (Suc n) = (in. 𝒫(ω 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 " = (in. 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"
      by (simp add: p_def u_def)
  qed
  finally show ?thesis .
qed

lemma p_eq_sum_p_f: "p x y n = (in. 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. in. 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. in. (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])
       (simp_all add: power_add[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"
    by (simp add: gf_F_def gf_G_def)
  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 = (in. (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 " = (in. (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) = (in. (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. in. (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")
    apply (auto simp add: field_simps)
    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)
    apply (simp add: field_simps)
    done
  then show ?thesis
    by (simp add: gf_U_def[abs_def] U_def)
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
    by (simp add: gf_F_def[abs_def] F_def)
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"
    by (simp add: H'_def)
  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 ω}"
      by (simp add: H'_def)
    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"
      by (simp add: T.emeasure_eq_measure) }
  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"
    by (simp add: H'_eq)
  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)"
    by (simp add: p_Suc')
  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"
      by (simp add: AE_measure_pmf_iff less_le)
    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))"
        by (simp add: ac_simps ennreal_mult'[symmetric])
    qed auto
    also have "  (i. ennreal (p x x (i + (n + m))))"
      by (simp add: ac_simps)
    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 = "
      by (simp add: top_unique) }
  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)"
      by (subst Bochner_Integration.integral_add)
         (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)"
      by (simp add: measure_pmf.emeasure_eq_measure Compl_eq_Diff_UNIV)
    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"
      by (simp add: measure_pmf.emeasure_eq_measure pmf.rep_eq)
    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"
      by (simp add: set_pmf_iff)
    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"
      by (simp add: recurrent_iffI_communicating)
    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. yC. 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 "yC. alw (ev (HLD {y})) ω"
      by (rule pigeonhole_stream) fact
  qed
  then have "1 = 𝒫(ω in T x. yC. alw (ev (HLD {y})) ω)"
    by (subst (asm) T.prob_Collect_eq_1[symmetric]) (auto simp: finite C)
  also have " = measure (T x) (yC. {ωspace (T x). alw (ev (HLD {y})) ω})"
    by (intro arg_cong2[where f=measure]) auto
  also have "  (yC. H x y)"
    unfolding H_def using finite C by (rule T.finite_measure_subadditive_finite) auto
  also have " = (yC. U x y * H y y)"
    by (auto intro!: sum.cong H_eq)
  finally have "yC. 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"
    by (simp add: communicating_def)
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  (xC. 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"
  unfolding U'_def by (simp add: nn_integral_add)

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"
  by (simp add: nn_integral_add T.emeasure_space_1 U'_def del: space_T)

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))"
        using z by (auto simp add: ac_simps power_add intro!: mult_left_mono)
    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)
      apply (simp add: sum_nonneg)
      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
      by (auto simp add: mult_le_0_iff)
  qed
  with recurrent x show ?thesis
    by (simp add: pos_recurrent_def nn_integral_add)
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]
  by (auto simp add: communicating_def)

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)"
  by (simp add: stat_def