Theory Markov_Models.Markov_Models_Auxiliary

(* Author: Johannes Hölzl <hoelzl@in.tum.de> *)

section ‹Auxiliary Theory›

text ‹Parts of it should be moved to the Isabelle repository›

theory Markov_Models_Auxiliary
imports
  "HOL-Probability.Probability"
  "HOL-Library.Rewrite"
  "HOL-Library.Linear_Temporal_Logic_on_Streams"
  Coinductive.Coinductive_Stream
  Coinductive.Coinductive_Nat
begin

lemma lfp_upperbound: "(⋀y. x ≤ f y) ⟹ x ≤ lfp f"
  unfolding lfp_def by (intro Inf_greatest) (auto intro: order_trans)

(* ?? *)
lemma lfp_arg: "(λt. lfp (F t)) = lfp (λx t. F t (x t))"
  apply (auto simp: lfp_def le_fun_def fun_eq_iff intro!: Inf_eqI Inf_greatest)
  subgoal for x y
    by (rule INF_lower2[of "top(x := y)"]) auto
  done

lemma lfp_pair: "lfp (λf (a, b). F (λa b. f (a, b)) a b) (a, b) = lfp F a b"
  unfolding lfp_def
  by (auto intro!: INF_eq simp: le_fun_def)
     (auto intro!: exI[of _ "λ(a, b). x a b" for x])

lemma all_Suc_split: "(∀i. P i) ⟷ (P 0 ∧ (∀i. P (Suc i)))"
  using nat_induct by auto

definition "with P f d = (if ∃x. P x then f (SOME x. P x) else d)"

lemma withI[case_names default exists]:
  "((⋀x. ¬ P x) ⟹ Q d) ⟹ (⋀x. P x ⟹ Q (f x)) ⟹ Q (with P f d)"
  unfolding with_def by (auto intro: someI2)

context order
begin

definition
  "maximal f S = {x∈S. ∀y∈S. f y ≤ f x}"

lemma maximalI: "x ∈ S ⟹ (⋀y. y ∈ S ⟹ f y ≤ f x) ⟹ x ∈ maximal f S"
  by (simp add: maximal_def)

lemma maximalI_trans: "x ∈ maximal f S ⟹ f x ≤ f y ⟹ y ∈ S ⟹ y ∈ maximal f S"
  unfolding maximal_def by (blast intro: antisym order_trans)

lemma maximalD1: "x ∈ maximal f S ⟹ x ∈ S"
  by (simp add: maximal_def)

lemma maximalD2: "x ∈ maximal f S ⟹ y ∈ S ⟹ f y ≤ f x"
  by (simp add: maximal_def)

lemma maximal_inject: "x ∈ maximal f S ⟹ y ∈ maximal f S ⟹ f x = f y"
  by (rule order.antisym) (simp_all add: maximal_def)

lemma maximal_empty[simp]: "maximal f {} = {}"
  by (simp add: maximal_def)

lemma maximal_singleton[simp]: "maximal f {x} = {x}"
  by (auto simp add: maximal_def)

lemma maximal_in_S: "maximal f S ⊆ S"
  by (auto simp: maximal_def)

end

context linorder
begin

lemma maximal_ne:
  assumes "finite S" "S ≠ {}"
  shows "maximal f S ≠ {}"
  using assms
proof (induct rule: finite_ne_induct)
  case (insert s S)
  show ?case
  proof cases
    assume "∀x∈S. f x ≤ f s"
    with insert have "s ∈ maximal f (insert s S)"
      by (auto intro!: maximalI)
    then show ?thesis
      by auto
  next
    assume "¬ (∀x∈S. f x ≤ f s)"
    then have "maximal f (insert s S) = maximal f S"
      by (auto simp: maximal_def)
    with insert show ?thesis
      by auto
  qed
qed simp

end

lemma mono_les:
  fixes s S N and l1 l2 :: "'a ⇒ real" and K :: "'a ⇒ 'a pmf"
  defines "Δ x ≡ l2 x - l1 x"
  assumes s: "s ∈ S" and S: "(⋃s∈S. set_pmf (K s)) ⊆ S ∪ N"
  assumes int_l1[simp]: "⋀s. s ∈ S ⟹ integrable (K s) l1"
  assumes int_l2[simp]: "⋀s. s ∈ S ⟹ integrable (K s) l2"
  assumes to_N: "⋀s. s ∈ S ⟹ ∃t∈N. (s, t) ∈ (SIGMA s:UNIV. K s)⇧*"
  assumes l1: "⋀s. s ∈ S ⟹ (∫t. l1 t ∂K s) + c s ≤ l1 s"
  assumes l2: "⋀s. s ∈ S ⟹ l2 s ≤ (∫t. l2 t ∂K s) + c s"
  assumes eq: "⋀s. s ∈ N ⟹ l2 s ≤ l1 s"
  assumes finitary: "finite (Δ ` (S∪N))"
  shows "l2 s ≤ l1 s"
proof -
  define M where "M = {s∈S∪N. ∀t∈S∪N. Δ t ≤ Δ s}"

  have [simp]: "⋀s. s∈S ⟹ integrable (K s) Δ"
    by (simp add: Δ_def[abs_def])

  have M_unqiue: "⋀s t. s ∈ M ⟹ t ∈ M ⟹ Δ s = Δ t"
    by (auto intro!: antisym simp: M_def)
  have M1: "⋀s. s ∈ M ⟹ s ∈ S ∪ N"
    by (auto simp: M_def)
  have M2: "⋀s t. s ∈ M ⟹ t ∈ S ∪ N ⟹ Δ t ≤ Δ s"
    by (auto simp: M_def)
  have M3: "⋀s t. s ∈ M ⟹ t ∈ S ∪ N ⟹ t ∉ M ⟹ Δ t < Δ s"
    by (auto simp: M_def less_le)

  have N: "∀s∈N. Δ s ≤ 0"
    using eq by (simp add: Δ_def)

  { fix s assume s: "s ∈ M" "M ∩ N = {}"
    then have "s ∈ S - N"
      by (auto dest: M1)
    with to_N[of s] obtain t where "(s, t) ∈ (SIGMA s:UNIV. K s)⇧*" and "t ∈ N"
      by (auto simp: M_def)
    from this(1) ‹s ∈ M› have "Δ s ≤ 0"
    proof (induction rule: converse_rtrancl_induct)
      case (step s s')
      then have s: "s ∈ M" "s ∈ S" "s ∉ N" and s': "s' ∈ S ∪ N" "s' ∈ K s"
        using S ‹M ∩ N = {}› by (auto dest: M1)
      have "s' ∈ M"
      proof (rule ccontr)
        assume "s' ∉ M"
        with ‹s ∈ S› s' ‹s ∈ M›
        have "0 < pmf (K s) s'" "Δ s' < Δ s"
          by (auto intro: M2 M3 pmf_positive)

        have "Δ s ≤ ((∫t. l2 t ∂K s) + c s) - ((∫t. l1 t ∂K s) + c s)"
          unfolding Δ_def using ‹s ∈ S› ‹s ∉ N› by (intro diff_mono l1 l2) auto
        then have "Δ s ≤ (∫s'. Δ s' ∂K s)"
          using ‹s ∈ S› by (simp add: Δ_def)
        also have "… < (∫s'. Δ s ∂K s)"
          using ‹s' ∈ K s› ‹Δ s' < Δ s› ‹s∈S› S ‹s∈M›
          by (intro measure_pmf.integral_less_AE[where A="{s'}"])
             (auto simp: emeasure_measure_pmf_finite AE_measure_pmf_iff set_pmf_iff[symmetric]
                   intro!: M2)
        finally show False
          using measure_pmf.prob_space[of "K s"] by simp
      qed
      with step.IH ‹t∈N› N have "Δ s' ≤ 0" "s' ∈ M"
        by auto
      with ‹s∈S› show "Δ s ≤ 0"
        by (force simp: M_def)
    qed (insert N ‹t∈N›, auto) }

  show ?thesis
  proof cases
    assume "M ∩ N = {}"
    have "Max (Δ`(S∪N)) ∈ Δ`(S∪N)"
      using ‹s ∈ S› by (intro Max_in finitary) auto
    then obtain t where "t ∈ S ∪ N" "Δ t = Max (Δ`(S∪N))"
      unfolding image_iff by metis
    then have "t ∈ M"
      by (auto simp: M_def finitary intro!: Max_ge)
    have "Δ s ≤ Δ t"
      using ‹t∈M› ‹s∈S› by (auto dest: M2)
    also have "Δ t ≤ 0"
      using ‹t∈M› ‹M ∩ N = {}› by fact
    finally show ?thesis
      by (simp add: Δ_def)
  next
    assume "M ∩ N ≠ {}"
    then obtain t where "t ∈ M" "t ∈ N" by auto
    with N ‹s∈S› have "Δ s ≤ 0"
      by (intro order_trans[of "Δ s" "Δ t" 0]) (auto simp: M_def)
    then show ?thesis
      by (simp add: Δ_def)
  qed
qed

lemma unique_les:
  fixes s S N and l1 l2 :: "'a ⇒ real" and K :: "'a ⇒ 'a pmf"
  defines "Δ x ≡ l2 x - l1 x"
  assumes s: "s ∈ S" and S: "(⋃s∈S. set_pmf (K s)) ⊆ S ∪ N"
  assumes "⋀s. s ∈ S ⟹ integrable (K s) l1"
  assumes "⋀s. s ∈ S ⟹ integrable (K s) l2"
  assumes "⋀s. s ∈ S ⟹ ∃t∈N. (s, t) ∈ (SIGMA s:UNIV. K s)⇧*"
  assumes "⋀s. s ∈ S ⟹ l1 s = (∫t. l1 t ∂K s) + c s"
  assumes "⋀s. s ∈ S ⟹ l2 s = (∫t. l2 t ∂K s) + c s"
  assumes "⋀s. s ∈ N ⟹ l2 s = l1 s"
  assumes 1: "finite (Δ ` (S∪N))"
  shows "l2 s = l1 s"
proof -
  have "finite ((λx. l2 x - l1 x) ` (S∪N))"
    using 1 by (auto simp: Δ_def[abs_def])
  moreover then have "finite (uminus ` (λx. l2 x - l1 x) ` (S∪N))"
    by auto
  ultimately show ?thesis
    using assms
    by (intro antisym mono_les[of s S K N l2 l1 c] mono_les[of s S K N l1 l2 c])
       (auto simp: image_comp comp_def)
qed

lemma inf_continuous_suntil_disj[order_continuous_intros]:
  assumes Q: "inf_continuous Q"
  assumes disj: "⋀x ω. ¬ (P ω ∧ Q x ω)"
  shows "inf_continuous (λx. P suntil Q x)"
  unfolding inf_continuous_def
proof (safe intro!: ext)
  fix M ω i assume "(P suntil Q (⨅i. M i)) ω" "decseq M" then show "(P suntil Q (M i)) ω"
    unfolding inf_continuousD[OF Q ‹decseq M›] by induction (auto intro: suntil.intros)
next
  fix M ω assume *: "(⨅i. P suntil Q (M i)) ω" "decseq M"
  then have "(P suntil Q (M 0)) ω"
    by auto
  from this * show "(P suntil Q (⨅i. M i)) ω"
    unfolding inf_continuousD[OF Q ‹decseq M›]
  proof induction
    case (base ω) with disj[of ω "M _"] show ?case by (auto intro: suntil.intros elim: suntil.cases)
  next
    case (step ω) with disj[of ω "M _"] show ?case by (auto intro: suntil.intros elim: suntil.cases)
  qed
qed

lemma inf_continuous_nxt[order_continuous_intros]: "inf_continuous P ⟹ inf_continuous (λx. nxt (P x) ω)"
  by (auto simp: inf_continuous_def image_comp)

lemma sup_continuous_nxt[order_continuous_intros]: "sup_continuous P ⟹ sup_continuous (λx. nxt (P x) ω)"
  by (auto simp: sup_continuous_def image_comp)

lemma mcont_ennreal_of_enat: "mcont Sup (≤) Sup (≤) ennreal_of_enat"
  by (auto intro!: mcontI monotoneI contI ennreal_of_enat_Sup)

lemma mcont2mcont_ennreal_of_enat[cont_intro]:
  "mcont lub ord Sup (≤) f ⟹ mcont lub ord Sup (≤) (λx. ennreal_of_enat (f x))"
  by (auto intro: ccpo.mcont2mcont[OF complete_lattice_ccpo'] mcont_ennreal_of_enat)

declare stream.exhaust[cases type: stream]

lemma scount_eq_emeasure: "scount P ω = emeasure (count_space UNIV) {i. P (sdrop i ω)}"
proof cases
  assume "alw (ev P) ω"
  moreover then have "infinite {i. P (sdrop i ω)}"
    using infinite_iff_alw_ev[of P ω] by simp
  ultimately show ?thesis
    by (simp add: scount_infinite_iff[symmetric])
next
  assume "¬ alw (ev P) ω"
  moreover then have "finite {i. P (sdrop i ω)}"
    using infinite_iff_alw_ev[of P ω] by simp
  ultimately show ?thesis
    by (simp add: not_alw_iff not_ev_iff scount_eq_card)
qed

lemma measurable_scount[measurable]:
  assumes [measurable]: "Measurable.pred (stream_space M) P"
  shows "scount P ∈ measurable (stream_space M) (count_space UNIV)"
  unfolding scount_eq[abs_def] by measurable

lemma measurable_sfirst2:
  assumes [measurable]: "Measurable.pred (N ⨂⇩M stream_space M) (λ(x, ω). P x ω)"
  shows "(λ(x, ω). sfirst (P x) ω) ∈ measurable (N ⨂⇩M  stream_space M) (count_space UNIV)"
  apply (coinduction rule: measurable_enat_coinduct)
  apply simp
  apply (rule exI[of _ "λx. 0"])
  apply (rule exI[of _ "λ(x, ω). (x, stl ω)"])
  apply (rule exI[of _ "λ(x, ω). P x ω"])
  apply (subst sfirst.simps[abs_def])
  apply (simp add: fun_eq_iff)
  done

lemma measurable_sfirst2'[measurable (raw)]:
  assumes [measurable (raw)]: "f ∈ N →⇩M stream_space M" "Measurable.pred (N ⨂⇩M stream_space M) (λx. P (fst x) (snd x))"
  shows "(λx. sfirst (P x) (f x)) ∈ measurable N (count_space UNIV)"
  using measurable_sfirst2[measurable] by measurable

lemma measurable_sfirst[measurable]:
  assumes [measurable]: "Measurable.pred (stream_space M) P"
  shows "sfirst P ∈ measurable (stream_space M) (count_space UNIV)"
  by measurable

lemma measurable_epred[measurable]: "epred ∈ count_space UNIV →⇩M count_space UNIV"
  by (rule measurable_count_space)

lemma nn_integral_stretch:
  "f ∈ borel →⇩M borel ⟹ c ≠ 0 ⟹ (∫⇧+x. f (c * x) ∂lborel) = (1 / ¦c¦::real) * (∫⇧+x. f x ∂lborel)"
  using nn_integral_real_affine[of f c 0] by (simp add: mult.assoc[symmetric] ennreal_mult[symmetric])

lemma prod_sum_distrib:
  fixes f g :: "'a ⇒ 'b ⇒ 'c::comm_semiring_1"
  assumes "finite I" shows "(⋀i. i ∈ I ⟹ finite (J i)) ⟹ (∏i∈I. ∑j∈J i. f i j) = (∑m∈Pi⇩E I J. ∏i∈I. f i (m i))"
  using ‹finite I›
proof induction
  case (insert i I) then show ?case
    by (auto simp: PiE_insert_eq finite_PiE sum.reindex inj_combinator sum.swap[of _ "Pi⇩E I J"]
                   sum.cartesian_product' sum_distrib_left sum_distrib_right
             intro!: sum.cong prod.cong arg_cong[where f="(*) x" for x])
qed simp

lemma prod_add_distrib:
  fixes f g :: "'a ⇒ 'b::comm_semiring_1"
  assumes "finite I" shows "(∏i∈I. f i + g i) = (∑J∈Pow I. (∏i∈J. f i) * (∏i∈I - J. g i))"
proof -
  have "(∏i∈I. f i + g i) = (∏i∈I. ∑b∈{True, False}. if b then f i else g i)"
    by simp
  also have "… = (∑m∈I →⇩E {True, False}. ∏i∈I. if m i then f i else g i)"
    using ‹finite I› by (rule prod_sum_distrib) simp
  also have "… = (∑J∈Pow I. (∏i∈J. f i) * (∏i∈I - J. g i))"
    by (rule sum.reindex_bij_witness[where i="λJ. λi∈I. i∈J" and j="λm. {i∈I. m i}"])
       (auto simp: fun_eq_iff prod.If_cases ‹finite I› intro!: arg_cong2[where f="(*)"] prod.cong)
  finally show ?thesis .
qed

subclass (in linordered_nonzero_semiring) ordered_semiring_0
  proof qed

lemma (in linordered_nonzero_semiring) prod_nonneg: "(∀a∈A. 0 ≤ f a) ⟹ 0 ≤ prod f A"
  by (induct A rule: infinite_finite_induct) simp_all

lemma (in linordered_nonzero_semiring) prod_mono:
  "∀i∈A. 0 ≤ f i ∧ f i ≤ g i ⟹ prod f A ≤ prod g A"
  by (induct A rule: infinite_finite_induct) (auto intro!: prod_nonneg mult_mono)

lemma (in linordered_nonzero_semiring) prod_mono2:
  assumes "finite J" "I ⊆ J" "⋀i. i ∈ I ⟹ 0 ≤ g i ∧ g i ≤ f i" "(⋀i. i ∈ J - I ⟹ 1 ≤ f i)"
  shows "prod g I ≤ prod f J"
proof -
  have "prod g I = (∏i∈J. if i ∈ I then g i else 1)"
    using ‹finite J› ‹I ⊆ J› by (simp add: prod.If_cases Int_absorb1)
  also have "… ≤ prod f J"
    using assms by (intro prod_mono) auto
  finally show ?thesis .
qed

lemma (in linordered_nonzero_semiring) prod_mono3:
  assumes "finite J" "I ⊆ J" "⋀i. i ∈ J ⟹ 0 ≤ g i" "⋀i. i ∈ I ⟹ g i ≤ f i" "(⋀i. i ∈ J - I ⟹ g i ≤ 1)"
  shows "prod g J ≤ prod f I"
proof -
  have "prod g J ≤ (∏i∈J. if i ∈ I then f i else 1)"
    using assms by (intro prod_mono) auto
  also have "… = prod f I"
    using ‹finite J› ‹I ⊆ J› by (simp add: prod.If_cases Int_absorb1)
  finally show ?thesis .
qed

lemma (in linordered_nonzero_semiring) one_le_prod: "(⋀i. i ∈ I ⟹ 1 ≤ f i) ⟹ 1 ≤ prod f I"
proof (induction I rule: infinite_finite_induct)
  case (insert i I) then show ?case
    using mult_mono[of 1 "f i" 1 "prod f I"]
    by (auto intro: order_trans[OF zero_le_one])
qed auto

lemma sum_plus_one_le_prod_plus_one:
  fixes p :: "'a ⇒ 'b::linordered_nonzero_semiring"
  assumes "⋀i. i ∈ I ⟹ 0 ≤ p i"
  shows "(∑i∈I. p i) + 1 ≤ (∏i∈I. p i + 1)"
proof cases
  assume [simp]: "finite I"
  with assms have [simp]: "J ⊆ I ⟹ 0 ≤ prod p J" for J
    by (intro prod_nonneg) auto
  have "1 + (∑i∈I. p i) = (∑J∈insert {} ((λx. {x})`I). (∏i∈J. p i) * (∏i∈I - J. 1))"
    by (subst sum.insert) (auto simp: sum.reindex)
  also have "… ≤ (∑J∈Pow I. (∏i∈J. p i) * (∏i∈I - J. 1))"
    using assms by (intro sum_mono2) auto
  finally show ?thesis
    by (subst prod_add_distrib) (auto simp: add.commute)
qed simp

lemma summable_iff_convergent_prod:
  fixes p :: "nat ⇒ real" assumes p: "⋀i. 0 ≤ p i"
  shows "summable p ⟷ convergent (λn. ∏i<n. p i + 1)"
  unfolding summable_iff_convergent
proof
  assume "convergent (λn. ∏i<n. p i + 1)"
  then obtain x where x: "(λn. ∏i<n. p i + 1) ⇢ x"
    by (auto simp: convergent_def)
  then have "1 ≤ x"
    by (rule tendsto_lowerbound) (auto intro!: always_eventually one_le_prod p)

  have "convergent (λn. 1 + (∑i<n. p i))"
  proof (intro Bseq_mono_convergent BseqI allI)
    show "0 < x" using ‹1 ≤ x› by auto
  next
    fix n
    have "norm ((∑i<n. p i) + 1) ≤ (∏i<n. p i + 1)"
      using p by (simp add: sum_nonneg sum_plus_one_le_prod_plus_one p)
    also have "… ≤ x"
      using assms
      by (intro tendsto_lowerbound[OF x])
          (auto simp: eventually_sequentially intro!: exI[of _ n] prod_mono2)
    finally show "norm (1 + sum p {..<n}) ≤ x"
      by (simp add: add.commute)
  qed (insert p, auto intro!: sum_mono2)
  then show "convergent (λn. ∑i<n. p i)"
    unfolding convergent_add_const_iff .
next
  assume "convergent (λn. ∑i<n. p i)"
  then obtain x where x: "(λn. exp (∑i<n. p i)) ⇢ exp x"
    by (force simp: convergent_def intro!: tendsto_exp)
  show "convergent (λn. ∏i<n. p i + 1)"
  proof (intro Bseq_mono_convergent BseqI allI)
    show "0 < exp x" by simp
  next
    fix n
    have "norm (∏i<n. p i + 1) ≤ exp (∑i<n. p i)"
      using p exp_ge_add_one_self[of "p _"] by (auto simp add: prod_nonneg exp_sum add.commute intro!: prod_mono)
    also have "… ≤ exp x"
      using p
      by (intro tendsto_lowerbound[OF x]) (auto simp: eventually_sequentially intro!: sum_mono2 )
    finally show "norm (∏i<n. p i + 1) ≤ exp x" .
  qed (insert p, auto intro!: prod_mono2)
qed

primrec eexp :: "ereal ⇒ ennreal"
  where
    "eexp MInfty = 0"
  | "eexp (ereal r) = ennreal (exp r)"
  | "eexp PInfty = top"

lemma
  shows eexp_minus_infty[simp]: "eexp (-∞) = 0"
    and eexp_infty[simp]: "eexp ∞ = top"
  using eexp.simps by simp_all

lemma eexp_0[simp]: "eexp 0 = 1"
  by (simp add: zero_ereal_def)

lemma eexp_inj[simp]: "eexp x = eexp y ⟷ x = y"
  by (cases x; cases y; simp)

lemma eexp_mono[simp]: "eexp x ≤ eexp y ⟷ x ≤ y"
  by (cases x; cases y; simp add: top_unique)

lemma eexp_strict_mono[simp]: "eexp x < eexp y ⟷ x < y"
  by (simp add: less_le)

lemma exp_eq_0_iff[simp]: "eexp x = 0 ⟷ x = -∞"
  using eexp_inj[of x "-∞"] unfolding eexp_minus_infty .

lemma eexp_surj: "range eexp = UNIV"
proof -
  have part: "UNIV = {0} ∪ {0 <..< top} ∪ {top::ennreal}"
    by (auto simp: less_top)
  show ?thesis
    unfolding part
    by (force simp: image_iff less_top less_top_ennreal intro!: eexp.simps[symmetric] eexp.simps dest: exp_total)
qed

lemma continuous_on_eexp': "continuous_on UNIV eexp"
  by (rule continuous_onI_mono) (auto simp: eexp_surj)

lemma continuous_on_eexp[continuous_intros]: "continuous_on A f ⟹ continuous_on A (λx. eexp (f x))"
  by (rule continuous_on_compose2[OF continuous_on_eexp']) auto

lemma tendsto_eexp[tendsto_intros]: "(f ⤏ x) F ⟹ ((λx. eexp (f x)) ⤏ eexp x) F"
  by (rule continuous_on_tendsto_compose[OF continuous_on_eexp']) auto

lemma measurable_eexp[measurable]: "eexp ∈ borel →⇩M borel"
  using continuous_on_eexp' by (rule borel_measurable_continuous_onI)

lemma eexp_add: "¬ ((x = ∞ ∧ y = -∞) ∨ (x = -∞ ∧ y = ∞)) ⟹ eexp (x + y) = eexp x * eexp y"
  by (cases x; cases y; simp add: exp_add ennreal_mult ennreal_top_mult ennreal_mult_top)

lemma sum_Pinfty:
  fixes f :: "'a ⇒ ereal"
  shows "sum f I = ∞ ⟷ (finite I ∧ (∃i∈I. f i = ∞))"
  by (induction I rule: infinite_finite_induct) auto

lemma sum_Minfty:
  fixes f :: "'a ⇒ ereal"
  shows "sum f I = -∞ ⟷ (finite I ∧ ¬ (∃i∈I. f i = ∞) ∧ (∃i∈I. f i = -∞))"
  by (induction I rule: infinite_finite_induct)
     (auto simp: sum_Pinfty)

lemma eexp_sum: "¬ (∃i∈I. ∃j∈I. f i = -∞ ∧ f j = ∞) ⟹ eexp (∑i∈I. f i) = (∏i∈I. eexp (f i))"
proof (induction I rule: infinite_finite_induct)
  case (insert i I)
  have "eexp (sum f (insert i I)) = eexp (f i) * eexp (sum f I)"
    using insert.prems insert.hyps by (auto simp: sum_Pinfty sum_Minfty intro!: eexp_add)
  then show ?case
    using insert by auto
qed simp_all

lemma eexp_suminf:
  assumes wf_f: "¬ {-∞, ∞} ⊆ range f" and f: "summable f"
  shows "(λn. ∏i<n. eexp (f i)) ⇢ eexp (∑i. f i)"
proof -
  have "(λn. eexp (∑i<n. f i)) ⇢ eexp (∑i. f i)"
    by (intro tendsto_eexp summable_LIMSEQ f)
  also have "(λn. eexp (∑i<n. f i)) = (λn. ∏i<n. eexp (f i))"
    using wf_f by (auto simp: fun_eq_iff image_iff eq_commute intro!: eexp_sum)
  finally show ?thesis .
qed

lemma continuous_onI_antimono:
  fixes f :: "'a::linorder_topology ⇒ 'b::{dense_order,linorder_topology}"
  assumes "open (f`A)"
    and mono: "⋀x y. x ∈ A ⟹ y ∈ A ⟹ x ≤ y ⟹ f y ≤ f x"
  shows "continuous_on A f"
proof (rule continuous_on_generate_topology[OF open_generated_order], safe)
  have monoD: "⋀x y. x ∈ A ⟹ y ∈ A ⟹ f y < f x ⟹ x < y"
    by (auto simp: not_le[symmetric] mono)
  have "∃x. x ∈ A ∧ f x < b ∧ x < a" if a: "a ∈ A" and fa: "f a < b" for a b
  proof -
    obtain y where "f a < y" "{f a ..< y} ⊆ f`A"
      using open_right[OF ‹open (f`A)›, of "f a" b] a fa
      by auto
    obtain z where z: "f a < z" "z < min b y"
      using dense[of "f a" "min b y"] ‹f a < y› ‹f a < b› by auto
    then obtain c where "z = f c" "c ∈ A"
      using ‹{f a ..< y} ⊆ f`A›[THEN subsetD, of z] by (auto simp: less_imp_le)
    with a z show ?thesis
      by (auto intro!: exI[of _ c] simp: monoD)
  qed
  then show "∃C. open C ∧ C ∩ A = f -` {..<b} ∩ A" for b
    by (intro exI[of _ "(⋃x∈{x∈A. f x < b}. {x <..})"])
       (auto intro: le_less_trans[OF mono] less_imp_le)

  have "∃x. x ∈ A ∧ b < f x ∧ x > a" if a: "a ∈ A" and fa: "b < f a" for a b
  proof -
    note a fa
    moreover
    obtain y where "y < f a" "{y <.. f a} ⊆ f`A"
      using open_left[OF ‹open (f`A)›, of "f a" b]  a fa
      by auto
    then obtain z where z: "max b y < z" "z < f a"
      using dense[of "max b y" "f a"] ‹y < f a› ‹b < f a› by auto
    then obtain c where "z = f c" "c ∈ A"
      using ‹{y <.. f a} ⊆ f`A›[THEN subsetD, of z] by (auto simp: less_imp_le)
    with a z show ?thesis
      by (auto intro!: exI[of _ c] simp: monoD)
  qed
  then show "∃C. open C ∧ C ∩ A = f -` {b <..} ∩ A" for b
    by (intro exI[of _ "(⋃x∈{x∈A. b < f x}. {..< x})"])
       (auto intro: less_le_trans[OF _ mono] less_imp_le)
qed

lemma minus_add_eq_ereal: "¬ ((a = ∞ ∧ b = -∞) ∨ (a = -∞ ∧ b = ∞)) ⟹ - (a + b::ereal) = -a - b"
  by (cases a; cases b; simp)

lemma setsum_negf_ereal: "¬ {-∞, ∞} ⊆ f`I ⟹ (∑i∈I. - f i) = - (∑i∈I. f i::ereal)"
  by (induction I rule: infinite_finite_induct)
     (auto simp: minus_add_eq_ereal sum_Minfty sum_Pinfty,
      (subst minus_add_eq_ereal; auto simp: sum_Pinfty sum_Minfty image_iff minus_ereal_def)+)

lemma convergent_minus_iff_ereal: "convergent (λx. - f x::ereal) ⟷ convergent f"
  unfolding convergent_def  by (metis ereal_uminus_uminus ereal_Lim_uminus)

lemma summable_minus_ereal: "¬ {-∞, ∞} ⊆ range f ⟹ summable (λn. f n) ⟹ summable (λn. - f n::ereal)"
  unfolding summable_iff_convergent
  by (subst setsum_negf_ereal) (auto simp: convergent_minus_iff_ereal)

lemma (in product_prob_space) product_nn_integral_component:
  assumes "f ∈ borel_measurable (M i)""i ∈ I"
  shows "integral⇧N (Pi⇩M I M) (λx. f (x i)) = integral⇧N (M i) f"
proof -
  from assms show ?thesis
    apply (subst PiM_component[symmetric, OF ‹i ∈ I›])
    apply (subst nn_integral_distr[OF measurable_component_singleton])
    apply simp_all
    done
qed

lemma ennreal_inverse_le[simp]: "inverse x ≤ inverse y ⟷ y ≤ (x::ennreal)"
  by (cases "0 < x"; cases x; cases "0 < y"; cases y; auto simp: top_unique inverse_ennreal)

lemma inverse_inverse_ennreal[simp]: "inverse (inverse x::ennreal) = x"
  by (cases "0 < x"; cases x; auto simp: inverse_ennreal)

lemma range_inverse_ennreal: "range inverse = (UNIV::ennreal set)"
proof -
  have "∃x. y = inverse x" for y :: ennreal
    by (intro exI[of _ "inverse y"]) simp
  then show ?thesis
    unfolding surj_def by auto
qed

lemma continuous_on_inverse_ennreal': "continuous_on (UNIV :: ennreal set) inverse"
  by (rule continuous_onI_antimono) (auto simp: range_inverse_ennreal)

lemma sums_minus_ereal: "¬ {- ∞, ∞} ⊆ f ` UNIV ⟹ (λn. - f n::ereal) sums x ⟹ f sums - x"
  unfolding sums_def
  apply (subst ereal_Lim_uminus)
  apply (subst (asm) setsum_negf_ereal)
  apply auto
  done

lemma suminf_minus_ereal: "¬ {- ∞, ∞} ⊆ f ` UNIV ⟹ summable f ⟹ (∑n. - f n :: ereal) = - suminf f"
  apply (rule sums_unique[symmetric])
  apply (rule sums_minus_ereal)
  apply (auto simp: ereal_uminus_eq_reorder)
  done

end