Theory Lemmas_Coproduct_Measure
section ‹ Preliminaries ›
theory Lemmas_Coproduct_Measure
imports "HOL-Probability.Probability"
"Standard_Borel_Spaces.Abstract_Metrizable_Topology"
begin
lemma metrizable_space_metric_space:
assumes d:"Metric_space UNIV d" "Metric_space.mtopology UNIV d = euclidean"
shows "class.metric_space d (⨅e∈{0<..}. principal {(x,y). d x y < e}) open"
proof -
interpret Metric_space UNIV d by fact
show ?thesis
proof
show "open U ⟷ (∀x∈U. ∀⇩F (x', y) in ⨅e∈{0<..}. principal {(F, y). d F y < e}. x' = x ⟶ y ∈ U)" for U
proof(subst eventually_INF_base)
show "a ∈ {0<..} ⟹ b ∈ {0<..} ⟹ ∃x∈{0<..}. principal {(F, y). d F y < x} ≤ principal {(F, y). d F y < a} ⊓ principal {(F, y). d F y < b}" for a b
by(auto intro!: bexI[where x="min a b"])
next
show "open U ⟷ (∀x∈U. ∃b∈{0<..}. ∀⇩F (x', y) in principal {(F, y). d F y < b}. x' = x ⟶ y ∈ U)"
by(fastforce simp: openin_mtopology[simplified d(2),simplified] eventually_principal)
qed simp
qed(auto simp: triangle')
qed
corollary metrizable_space_metric_space_ex:
assumes "metrizable_space (euclidean :: 'a :: topological_space topology)"
shows "∃(d :: 'a ⇒ 'a ⇒ real) F. class.metric_space d F open"
proof -
from assms obtain d :: "'a ⇒ 'a ⇒ real" where "Metric_space UNIV d" "Metric_space.mtopology UNIV d = euclidean"
by (metis Metric_space.topspace_mtopology metrizable_space_def topspace_euclidean)
from metrizable_space_metric_space[OF this] show ?thesis
by blast
qed
lemma completely_metrizable_space_metric_space:
assumes "Metric_space (UNIV :: 'a ::topological_space set) d" "Metric_space.mtopology UNIV d = euclidean" "Metric_space.mcomplete UNIV d"
shows "class.complete_space d (⨅e∈{0<..}. principal {(x,y). d x y < e}) open"
proof -
interpret Metric_space UNIV d by fact
interpret m:metric_space d "⨅e∈{0<..}. principal {(x,y). d x y < e}" "open"
by(auto intro!: metrizable_space_metric_space assms)
have [simp]:"topological_space.convergent (open :: 'a set ⇒ bool) = convergent"
proof
fix x :: "nat ⇒ 'a"
have *:"class.topological_space (open :: 'a set ⇒ bool)"
by standard auto
show "topological_space.convergent open x = convergent x"
by(simp add: topological_space.convergent_def[OF *] topological_space.nhds_def[OF *] convergent_def nhds_def)
qed
show ?thesis
apply unfold_locales
using assms(3) by(auto simp: mcomplete_def assms(2) MCauchy_def m.Cauchy_def convergent_def)
qed
lemma completely_metrizable_space_metric_space_ex:
assumes "completely_metrizable_space (euclidean :: 'a :: topological_space topology)"
shows "∃(d :: 'a ⇒ 'a ⇒ real) F. class.complete_space d F open"
proof -
from assms obtain d :: "'a ⇒ 'a ⇒ real" where "Metric_space UNIV d" "Metric_space.mtopology UNIV d = euclidean" "Metric_space.mcomplete UNIV d"
by (metis Metric_space.topspace_mtopology completely_metrizable_space_def topspace_euclidean)
from completely_metrizable_space_metric_space[OF this] show ?thesis
by blast
qed
subsection ‹ Polishness of Extended Reals and Non-Negative Extended Reals›
text ‹ We instantiate @{class polish_space} for @{typ ereal} and @{typ ennreal} with
\emph{non-canonical} metrics in order to change the order of @{term infsum}
using the lemma \isa{infsum{\isacharunderscore}Sigma}.›
instantiation ereal :: metric_space
begin
definition dist_ereal :: "ereal ⇒ ereal ⇒ real"
where "dist_ereal ≡ SOME d. Metric_space UNIV d ∧
Metric_space.mtopology UNIV d = euclidean ∧
Metric_space.mcomplete UNIV d"
definition uniformity_ereal :: "(ereal × ereal) filter"
where "uniformity_ereal ≡ ⨅e∈{0<..}. principal {(x,y). dist x y < e}"
instance
proof -
let ?open = "open :: ereal set ⇒ bool"
interpret c:complete_space dist uniformity ?open
proof -
have "∃d. Metric_space (UNIV :: ereal set) d ∧
Metric_space.mtopology UNIV d = euclidean ∧
Metric_space.mcomplete UNIV d"
by (metis Polish_space_ereal Metric_space.topspace_mtopology Polish_space_def completely_metrizable_space_def topspace_euclidean)
hence "Metric_space (UNIV :: ereal set) dist ∧
Metric_space.mtopology (UNIV :: ereal set) dist = euclidean ∧
Metric_space.mcomplete (UNIV :: ereal set) dist"
unfolding dist_ereal_def by(rule someI_ex)
with completely_metrizable_space_metric_space show "class.complete_space dist uniformity ?open"
by(fastforce simp: uniformity_ereal_def)
qed
have [simp]:"topological_space.convergent ?open = convergent"
proof
fix x :: "nat ⇒ ereal"
have *:"class.topological_space ?open"
by standard auto
show "topological_space.convergent open x = convergent x"
by(simp add: topological_space.convergent_def topological_space.nhds_def * convergent_def nhds_def)
qed
show "OFCLASS(ereal, metric_space_class)"
by standard (use uniformity_ereal_def c.open_uniformity c.dist_triangle2 c.Cauchy_convergent in auto)
qed
end
instantiation ereal :: polish_space
begin
instance
proof
let ?open = "open :: ereal set ⇒ bool"
interpret c:complete_space dist uniformity ?open
proof -
have "∃d. Metric_space (UNIV :: ereal set) d ∧
Metric_space.mtopology UNIV d = euclidean ∧
Metric_space.mcomplete UNIV d"
by (metis Polish_space_ereal Metric_space.topspace_mtopology Polish_space_def completely_metrizable_space_def topspace_euclidean)
hence "Metric_space (UNIV :: ereal set) dist ∧
Metric_space.mtopology (UNIV :: ereal set) dist = euclidean ∧
Metric_space.mcomplete (UNIV :: ereal set) dist"
unfolding dist_ereal_def by(rule someI_ex)
with completely_metrizable_space_metric_space show "class.complete_space dist uniformity ?open"
by(fastforce simp: uniformity_ereal_def)
qed
have [simp]:"topological_space.convergent ?open = convergent"
proof
fix x :: "nat ⇒ ereal"
have *:"class.topological_space ?open"
by standard auto
show "topological_space.convergent open x = convergent x"
by(simp add: topological_space.convergent_def topological_space.nhds_def * convergent_def nhds_def)
qed
have [simp]:"uniform_space.Cauchy (uniformity :: (ereal × ereal) filter) = Cauchy"
by(auto simp add: metric_space.Cauchy_def[OF metric_space_axioms] Cauchy_def)
fix x :: "nat ⇒ ereal"
show "Cauchy x ⟹ convergent x"
using c.Cauchy_convergent by(auto simp: Cauchy_def)
qed
end
instantiation ennreal :: metric_space
begin
definition dist_ennreal :: "ennreal ⇒ ennreal ⇒ real"
where "dist_ennreal ≡ SOME d. Metric_space UNIV d ∧
Metric_space.mtopology UNIV d = euclidean ∧
Metric_space.mcomplete UNIV d"
definition uniformity_ennreal :: "(ennreal × ennreal) filter"
where "uniformity_ennreal ≡ ⨅e∈{0<..}. principal {(x,y). dist x y < e}"
instance
proof -
let ?open = "open :: ennreal set ⇒ bool"
interpret c:complete_space dist uniformity ?open
proof -
have "∃d. Metric_space (UNIV :: ennreal set) d ∧
Metric_space.mtopology UNIV d = euclidean ∧
Metric_space.mcomplete UNIV d"
by (metis Polish_space_ennreal Metric_space.topspace_mtopology Polish_space_def completely_metrizable_space_def topspace_euclidean)
hence "Metric_space (UNIV :: ennreal set) dist ∧
Metric_space.mtopology (UNIV :: ennreal set) dist = euclidean ∧
Metric_space.mcomplete (UNIV :: ennreal set) dist"
unfolding dist_ennreal_def by(rule someI_ex)
with completely_metrizable_space_metric_space show "class.complete_space dist uniformity ?open"
by(fastforce simp: uniformity_ennreal_def)
qed
have [simp]:"topological_space.convergent ?open = convergent"
proof
fix x :: "nat ⇒ ennreal"
have *:"class.topological_space ?open"
by standard auto
show "topological_space.convergent open x = convergent x"
by(simp add: topological_space.convergent_def[OF *] topological_space.nhds_def[OF *] convergent_def nhds_def)
qed
show "OFCLASS(ennreal, metric_space_class)"
by standard (use uniformity_ennreal_def c.open_uniformity c.dist_triangle2 c.Cauchy_convergent in auto)
qed
end
instantiation ennreal :: polish_space
begin
instance
proof
let ?open = "open :: ennreal set ⇒ bool"
interpret c:complete_space dist uniformity ?open
proof -
have "∃d. Metric_space (UNIV :: ennreal set) d ∧
Metric_space.mtopology UNIV d = euclidean ∧
Metric_space.mcomplete UNIV d"
by (metis Polish_space_ennreal Metric_space.topspace_mtopology Polish_space_def completely_metrizable_space_def topspace_euclidean)
hence "Metric_space (UNIV :: ennreal set) dist ∧
Metric_space.mtopology (UNIV :: ennreal set) dist = euclidean ∧
Metric_space.mcomplete (UNIV :: ennreal set) dist"
unfolding dist_ennreal_def by(rule someI_ex)
with completely_metrizable_space_metric_space show "class.complete_space dist uniformity ?open"
by(fastforce simp: uniformity_ennreal_def)
qed
have [simp]:"topological_space.convergent ?open = convergent"
proof
fix x :: "nat ⇒ ennreal"
have *:"class.topological_space ?open"
by standard auto
show "topological_space.convergent open x = convergent x"
by(simp add: topological_space.convergent_def topological_space.nhds_def * convergent_def nhds_def)
qed
have [simp]:"uniform_space.Cauchy (uniformity :: (ennreal × ennreal) filter) = Cauchy"
by(auto simp add: metric_space.Cauchy_def[OF metric_space_axioms] Cauchy_def)
fix x :: "nat ⇒ ennreal"
show "Cauchy x ⟹ convergent x"
using c.Cauchy_convergent by(auto simp: Cauchy_def)
qed
end
subsection ‹ Lemmas for Infinite Sum ›
lemma uniformly_continuous_add_ennreal: "isUCont (λ(x::ennreal, y). x + y)"
proof(safe intro!: compact_uniformly_continuous)
have "compact (UNIV × UNIV :: (ennreal × ennreal) set)"
by(intro compact_Times compact_UNIV)
thus "compact (UNIV :: (ennreal × ennreal) set)"
by simp
qed(auto intro!: continuous_on_add_ennreal continuous_on_fst continuous_on_snd simp: split_beta')
lemma infsum_eq_suminf:
assumes "f summable_on UNIV"
shows "(∑⇩∞ n∈UNIV. f n) = suminf f"
using has_sum_imp_sums[OF has_sum_infsum[OF assms]]
by (simp add: sums_iff)
lemma infsum_Sigma_ennreal:
fixes f :: "_ ⇒ ennreal"
shows "infsum f (Sigma A B) = infsum (λx. infsum (λy. f (x, y)) (B x)) A"
by(auto intro!: uniformly_continuous_add_ennreal infsum_Sigma nonneg_summable_on_complete)
lemma infsum_swap_ennreal:
fixes f :: "_ ⇒ _ ⇒ ennreal"
shows "infsum (λx. infsum (λy. f x y) B) A = infsum (λy. infsum (λx. f x y) A) B"
by(auto intro!: infsum_swap uniformly_continuous_add_ennreal nonneg_summable_on_complete)
lemma has_sum_cmult_right_ennreal:
fixes f :: "_ ⇒ ennreal"
assumes "c < ⊤" "(f has_sum a) A"
shows "((λx. c * f x) has_sum c * a) A"
using ennreal_tendsto_cmult[OF assms(1)] assms(2)
by (force simp add: has_sum_def sum_distrib_left)
lemma infsum_cmult_right_ennreal:
fixes f :: "_ ⇒ ennreal"
assumes "c < ⊤"
shows "(∑⇩∞x∈A. c * f x) = c * infsum f A"
by (simp add: assms has_sum_cmult_right_ennreal infsumI nonneg_summable_on_complete)
lemma ennreal_sum_SUP_eq:
fixes f :: "nat ⇒ _ ⇒ ennreal"
assumes "finite A" "⋀x. x ∈ A ⟹ incseq (λj. f j x)"
shows "(∑i∈A. ⨆n. f n i) = (⨆n. ∑i∈A. f n i)"
using assms
proof induction
case empty
then show ?case
by simp
next
case ih:(insert x F)
show ?case (is "?lhs = ?rhs")
proof -
have "?lhs = (⨆n. f n x) + (⨆n. sum (f n) F)"
using ih by simp
also have "... = (⨆n. f n x + sum (f n) F)"
using ih by(auto intro!: incseq_sumI2 ennreal_SUP_add[symmetric])
also have "... = ?rhs"
using ih by simp
finally show ?thesis .
qed
qed
lemma ennreal_infsum_Sup_eq:
fixes f :: "nat ⇒ _ ⇒ ennreal"
assumes "⋀x. x ∈ A ⟹ incseq (λj. f j x)"
shows "(∑⇩∞x∈A. (SUP j. f j x)) = (SUP j. (∑⇩∞x∈A. f j x))" (is "?lhs = ?rhs")
proof -
have "?lhs = (⨆ (sum (λx. ⨆j. f j x) ` {F. finite F ∧ F ⊆ A}))"
by(auto intro!: nonneg_infsum_complete simp: SUP_upper2 assms)
also have "... = (⨆A∈{F. finite F ∧ F ⊆ A}. ⨆j. sum (f j) A)"
using assms by(auto intro!: SUP_cong ennreal_sum_SUP_eq)
also have "... = (⨆j. ⨆A∈{F. finite F ∧ F ⊆ A}. sum (f j) A)"
using SUP_commute by fast
also have "... = ?rhs"
by(subst nonneg_infsum_complete) (use assms in auto)
finally show ?thesis .
qed
lemma bounded_infsum_summable:
assumes "⋀x. x ∈ A ⟹ f x ≥ 0" "(∑⇩∞x∈A. ennreal (f x)) < top"
shows "f summable_on A"
proof(rule nonneg_bdd_above_summable_on)
from assms(2) obtain K where K:"(∑⇩∞x∈A. ennreal (f x)) ≤ ennreal K" "K ≥ 0"
using less_top_ennreal by force
show "bdd_above (sum f ` {F. F ⊆ A ∧ finite F})"
proof(safe intro!: bdd_aboveI[where M=K])
fix A'
assume A':"A' ⊆ A" "finite A'"
have "(∑⇩∞x∈A. ennreal (f x)) = (⨆ (sum (λx. ennreal (f x)) ` {F. finite F ∧ F ⊆ A}))"
by (simp add: nonneg_infsum_complete)
also have "... = (⨆ ((λF. ennreal (sum f F)) ` {F. finite F ∧ F ⊆ A}))"
by(auto intro!: SUP_cong sum_ennreal assms)
finally have "(⨆ ((λF. ennreal (sum f F)) ` {F. finite F ∧ F ⊆ A})) ≤ ennreal K"
using K by order
hence "ennreal (sum f A') ≤ ennreal K"
by (simp add: A' SUP_le_iff)
thus "sum f A' ≤ K"
by (simp add: K(2))
qed
qed fact
lemma infsum_less_top_dest:
fixes f :: "_ ⇒ _::{ordered_comm_monoid_add, topological_comm_monoid_add, t2_space, complete_linorder, linorder_topology}"
assumes "(∑⇩∞x∈A. f x) < top" "⋀x. x ∈ A ⟹ f x ≥ 0" "x ∈ A"
shows "f x < top"
proof(rule ccontr)
assume f:"¬ f x < top"
have "(∑⇩∞x∈A. f x) = (∑⇩∞y∈A - {x} ∪ {x}. f y)"
by(rule arg_cong[where f="infsum _"]) (use assms in auto)
also have "... = (∑⇩∞y∈A- {x}. f y) + (∑⇩∞y∈{x}. f y)"
using assms(2) by(intro infsum_Un_disjoint) (auto intro!: nonneg_summable_on_complete)
also have "... = (∑⇩∞y∈A- {x}. f y) + top"
using f top.not_eq_extremum by fastforce
also have "... = top"
by(auto intro!: add_top infsum_nonneg assms)
finally show False
using assms(1) by simp
qed
lemma infsum_ennreal_eq:
assumes "f summable_on A" "⋀x. x ∈ A ⟹ f x ≥ 0"
shows "(∑⇩∞x∈A. ennreal (f x)) = ennreal (∑⇩∞x∈A. f x)"
proof -
have "(∑⇩∞x∈A. ennreal (f x)) = (⨆ (sum (λx. ennreal (f x)) ` {F. finite F ∧ F ⊆ A}))"
by (simp add: nonneg_infsum_complete)
also have "... = (⨆ ((λF. ennreal (sum f F)) ` {F. finite F ∧ F ⊆ A}))"
by(auto intro!: SUP_cong sum_ennreal assms)
also have "... = ennreal (∑⇩∞x∈A. f x)"
using infsum_nonneg_is_SUPREMUM_ennreal[OF assms] by simp
finally show ?thesis .
qed
lemma abs_summable_on_integrable_iff:
fixes f :: "_ ⇒ _ :: {banach, second_countable_topology}"
shows "Infinite_Sum.abs_summable_on f A ⟷ integrable (count_space A) f"
by (simp add: abs_summable_equivalent abs_summable_on_def)
lemma infsum_eq_integral:
fixes f :: "_ ⇒ _ :: {banach, second_countable_topology}"
assumes "Infinite_Sum.abs_summable_on f A"
shows "infsum f A = integral⇧L (count_space A) f"
using assms infsetsum_infsum[of f A,symmetric]
by(auto simp: abs_summable_on_integrable_iff abs_summable_on_def infsetsum_def)
end