Theory Markov_Models_Auxiliary
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