# Theory Distribution_Functions

theory Distribution_Functions
imports Probability_Measure
```(*  Title:    HOL/Probability/Distribution_Functions.thy
Authors:  Jeremy Avigad (CMU) and Luke Serafin (CMU)
*)

section ‹Distribution Functions›

text ‹
Shows that the cumulative distribution function (cdf) of a distribution (a measure on the reals) is
nondecreasing and right continuous, which tends to 0 and 1 in either direction.

Conversely, every such function is the cdf of a unique distribution. This direction defines the
measure in the obvious way on half-open intervals, and then applies the Caratheodory extension
theorem.
›

(* TODO: the locales "finite_borel_measure" and "real_distribution" are defined here, but maybe they
should be somewhere else. *)

theory Distribution_Functions
imports Probability_Measure
begin

lemma UN_Ioc_eq_UNIV: "(⋃n. { -real n <.. real n}) = UNIV"
by auto
(metis le_less_trans minus_minus neg_less_iff_less not_le real_arch_simple
of_nat_0_le_iff reals_Archimedean2)

subsection ‹Properties of cdf's›

definition
cdf :: "real measure ⇒ real ⇒ real"
where
"cdf M ≡ λx. measure M {..x}"

lemma cdf_def2: "cdf M x = measure M {..x}"
by (simp add: cdf_def)

locale finite_borel_measure = finite_measure M for M :: "real measure" +
assumes M_is_borel: "sets M = sets borel"
begin

lemma sets_M[intro]: "a ∈ sets borel ⟹ a ∈ sets M"
using M_is_borel by auto

lemma cdf_diff_eq:
assumes "x < y"
shows "cdf M y - cdf M x = measure M {x<..y}"
proof -
from assms have *: "{..x} ∪ {x<..y} = {..y}" by auto
have "measure M {..y} = measure M {..x} + measure M {x<..y}"
by (subst finite_measure_Union [symmetric], auto simp add: *)
thus ?thesis
unfolding cdf_def by auto
qed

lemma cdf_nondecreasing: "x ≤ y ⟹ cdf M x ≤ cdf M y"
unfolding cdf_def by (auto intro!: finite_measure_mono)

lemma borel_UNIV: "space M = UNIV"
by (metis in_mono sets.sets_into_space space_in_borel top_le M_is_borel)

lemma cdf_nonneg: "cdf M x ≥ 0"
unfolding cdf_def by (rule measure_nonneg)

lemma cdf_bounded: "cdf M x ≤ measure M (space M)"
unfolding cdf_def by (intro bounded_measure)

lemma cdf_lim_infty:
"((λi. cdf M (real i)) ⇢ measure M (space M))"
proof -
have "(λi. cdf M (real i)) ⇢ measure M (⋃ i::nat. {..real i})"
unfolding cdf_def by (rule finite_Lim_measure_incseq) (auto simp: incseq_def)
also have "(⋃ i::nat. {..real i}) = space M"
by (auto simp: borel_UNIV intro: real_arch_simple)
finally show ?thesis .
qed

lemma cdf_lim_at_top: "(cdf M ⤏ measure M (space M)) at_top"
by (rule tendsto_at_topI_sequentially_real)
(simp_all add: mono_def cdf_nondecreasing cdf_lim_infty)

lemma cdf_lim_neg_infty: "((λi. cdf M (- real i)) ⇢ 0)"
proof -
have "(λi. cdf M (- real i)) ⇢ measure M (⋂ i::nat. {.. - real i })"
unfolding cdf_def by (rule finite_Lim_measure_decseq) (auto simp: decseq_def)
also have "(⋂ i::nat. {..- real i}) = {}"
by auto (metis leD le_minus_iff reals_Archimedean2)
finally show ?thesis
by simp
qed

lemma cdf_lim_at_bot: "(cdf M ⤏ 0) at_bot"
proof -
have *: "((λx :: real. - cdf M (- x)) ⤏ 0) at_top"
by (intro tendsto_at_topI_sequentially_real monoI)
(auto simp: cdf_nondecreasing cdf_lim_neg_infty tendsto_minus_cancel_left[symmetric])
from filterlim_compose [OF *, OF filterlim_uminus_at_top_at_bot]
show ?thesis
unfolding tendsto_minus_cancel_left[symmetric] by simp
qed

lemma cdf_is_right_cont: "continuous (at_right a) (cdf M)"
unfolding continuous_within
proof (rule tendsto_at_right_sequentially[where b="a + 1"])
fix f :: "nat ⇒ real" and x assume f: "decseq f" "f ⇢ a"
then have "(λn. cdf M (f n)) ⇢ measure M (⋂i. {.. f i})"
using ‹decseq f› unfolding cdf_def
by (intro finite_Lim_measure_decseq) (auto simp: decseq_def)
also have "(⋂i. {.. f i}) = {.. a}"
using decseq_ge[OF f] by (auto intro: order_trans LIMSEQ_le_const[OF f(2)])
finally show "(λn. cdf M (f n)) ⇢ cdf M a"
by (simp add: cdf_def)
qed simp

lemma cdf_at_left: "(cdf M ⤏ measure M {..<a}) (at_left a)"
proof (rule tendsto_at_left_sequentially[of "a - 1"])
fix f :: "nat ⇒ real" and x assume f: "incseq f" "f ⇢ a" "⋀x. f x < a" "⋀x. a - 1 < f x"
then have "(λn. cdf M (f n)) ⇢ measure M (⋃i. {.. f i})"
using ‹incseq f› unfolding cdf_def
by (intro finite_Lim_measure_incseq) (auto simp: incseq_def)
also have "(⋃i. {.. f i}) = {..<a}"
by (auto dest!: order_tendstoD(1)[OF f(2)] eventually_happens'[OF sequentially_bot]
intro: less_imp_le le_less_trans f(3))
finally show "(λn. cdf M (f n)) ⇢ measure M {..<a}"
by (simp add: cdf_def)
qed auto

lemma isCont_cdf: "isCont (cdf M) x ⟷ measure M {x} = 0"
proof -
have "isCont (cdf M) x ⟷ cdf M x = measure M {..<x}"
by (auto simp: continuous_at_split cdf_is_right_cont continuous_within[where s="{..< _}"]
cdf_at_left tendsto_unique[OF _ cdf_at_left])
also have "cdf M x = measure M {..<x} ⟷ measure M {x} = 0"
unfolding cdf_def ivl_disj_un(2)[symmetric]
by (subst finite_measure_Union) auto
finally show ?thesis .
qed

lemma countable_atoms: "countable {x. measure M {x} > 0}"
using countable_support unfolding zero_less_measure_iff .

end

locale real_distribution = prob_space M for M :: "real measure" +
assumes events_eq_borel [simp, measurable_cong]: "sets M = sets borel"
begin

lemma finite_borel_measure_M: "finite_borel_measure M"
by standard auto

sublocale finite_borel_measure M
by (rule finite_borel_measure_M)

lemma space_eq_univ [simp]: "space M = UNIV"
using events_eq_borel[THEN sets_eq_imp_space_eq] by simp

lemma cdf_bounded_prob: "⋀x. cdf M x ≤ 1"
by (subst prob_space [symmetric], rule cdf_bounded)

lemma cdf_lim_infty_prob: "(λi. cdf M (real i)) ⇢ 1"
by (subst prob_space [symmetric], rule cdf_lim_infty)

lemma cdf_lim_at_top_prob: "(cdf M ⤏ 1) at_top"
by (subst prob_space [symmetric], rule cdf_lim_at_top)

lemma measurable_finite_borel [simp]:
"f ∈ borel_measurable borel ⟹ f ∈ borel_measurable M"
by (rule borel_measurable_subalgebra[where N=borel]) auto

end

lemma (in prob_space) real_distribution_distr [intro, simp]:
"random_variable borel X ⟹ real_distribution (distr M borel X)"
unfolding real_distribution_def real_distribution_axioms_def by (auto intro!: prob_space_distr)

subsection ‹Uniqueness›

lemma (in finite_borel_measure) emeasure_Ioc:
assumes "a ≤ b" shows "emeasure M {a <.. b} = cdf M b - cdf M a"
proof -
have "{a <.. b} = {..b} - {..a}"
by auto
moreover have "{..x} ∈ sets M" for x
using atMost_borel[of x] M_is_borel by auto
moreover note ‹a ≤ b›
ultimately show ?thesis
by (simp add: emeasure_eq_measure finite_measure_Diff cdf_def)
qed

lemma cdf_unique':
fixes M1 M2
assumes "finite_borel_measure M1" and "finite_borel_measure M2"
assumes "cdf M1 = cdf M2"
shows "M1 = M2"
proof (rule measure_eqI_generator_eq[where Ω=UNIV])
fix X assume "X ∈ range (λ(a, b). {a<..b::real})"
then obtain a b where Xeq: "X = {a<..b}" by auto
then show "emeasure M1 X = emeasure M2 X"
by (cases "a ≤ b")
(simp_all add: assms(1,2)[THEN finite_borel_measure.emeasure_Ioc] assms(3))
next
show "(⋃i. {- real (i::nat)<..real i}) = UNIV"
by (rule UN_Ioc_eq_UNIV)
qed (auto simp: finite_borel_measure.emeasure_Ioc[OF assms(1)]
assms(1,2)[THEN finite_borel_measure.M_is_borel] borel_sigma_sets_Ioc
Int_stable_def)

lemma cdf_unique:
"real_distribution M1 ⟹ real_distribution M2 ⟹ cdf M1 = cdf M2 ⟹ M1 = M2"
using cdf_unique'[of M1 M2] by (simp add: real_distribution.finite_borel_measure_M)

lemma
fixes F :: "real ⇒ real"
assumes nondecF : "⋀ x y. x ≤ y ⟹ F x ≤ F y"
and right_cont_F : "⋀a. continuous (at_right a) F"
and lim_F_at_bot : "(F ⤏ 0) at_bot"
and lim_F_at_top : "(F ⤏ m) at_top"
and m: "0 ≤ m"
shows interval_measure_UNIV: "emeasure (interval_measure F) UNIV = m"
and finite_borel_measure_interval_measure: "finite_borel_measure (interval_measure F)"
proof -
let ?F = "interval_measure F"
{ have "ennreal (m - 0) = (SUP i::nat. ennreal (F (real i) - F (- real i)))"
by (intro LIMSEQ_unique[OF _ LIMSEQ_SUP] tendsto_ennrealI tendsto_intros
lim_F_at_bot[THEN filterlim_compose] lim_F_at_top[THEN filterlim_compose]
lim_F_at_bot[THEN filterlim_compose] filterlim_real_sequentially
filterlim_uminus_at_top[THEN iffD1])
(auto simp: incseq_def nondecF intro!: diff_mono)
also have "… = (SUP i::nat. emeasure ?F {- real i<..real i})"
by (subst emeasure_interval_measure_Ioc) (simp_all add: nondecF right_cont_F)
also have "… = emeasure ?F (⋃i::nat. {- real i<..real i})"
by (rule SUP_emeasure_incseq) (auto simp: incseq_def)
also have "(⋃i. {- real (i::nat)<..real i}) = space ?F"
by (simp add: UN_Ioc_eq_UNIV)
finally have "emeasure ?F (space ?F) = m"
by simp }
note * = this
then show "emeasure (interval_measure F) UNIV = m"
by simp

interpret finite_measure ?F
proof
show "emeasure ?F (space ?F) ≠ ∞"
using * by simp
qed
show "finite_borel_measure (interval_measure F)"
proof qed simp_all
qed

lemma real_distribution_interval_measure:
fixes F :: "real ⇒ real"
assumes nondecF : "⋀ x y. x ≤ y ⟹ F x ≤ F y" and
right_cont_F : "⋀a. continuous (at_right a) F" and
lim_F_at_bot : "(F ⤏ 0) at_bot" and
lim_F_at_top : "(F ⤏ 1) at_top"
shows "real_distribution (interval_measure F)"
proof -
let ?F = "interval_measure F"
interpret prob_space ?F
proof qed (use interval_measure_UNIV[OF assms] in simp)
show ?thesis
proof qed simp_all
qed

lemma
fixes F :: "real ⇒ real"
assumes nondecF : "⋀ x y. x ≤ y ⟹ F x ≤ F y" and
right_cont_F : "⋀a. continuous (at_right a) F" and
lim_F_at_bot : "(F ⤏ 0) at_bot"
shows emeasure_interval_measure_Iic: "emeasure (interval_measure F) {.. x} = F x"
and measure_interval_measure_Iic: "measure (interval_measure F) {.. x} = F x"
unfolding cdf_def
proof -
have F_nonneg[simp]: "0 ≤ F y" for y
using lim_F_at_bot by (rule tendsto_upperbound) (auto simp: eventually_at_bot_linorder nondecF intro!: exI[of _ y])

have "emeasure (interval_measure F) (⋃i::nat. {-real i <.. x}) = F x - ennreal 0"
proof (intro LIMSEQ_unique[OF Lim_emeasure_incseq])
have "(λi. F x - F (- real i)) ⇢ F x - 0"
by (intro tendsto_intros lim_F_at_bot[THEN filterlim_compose] filterlim_real_sequentially
filterlim_uminus_at_top[THEN iffD1])
from tendsto_ennrealI[OF this]
show "(λi. emeasure (interval_measure F) {- real i<..x}) ⇢ F x - ennreal 0"
apply (rule filterlim_cong[THEN iffD1, rotated 3])
apply simp
apply simp
apply (rule eventually_sequentiallyI[where c="nat (ceiling (- x))"])
apply (simp add: emeasure_interval_measure_Ioc right_cont_F nondecF)
done
qed (auto simp: incseq_def)
also have "(⋃i::nat. {-real i <.. x}) = {..x}"
by auto (metis minus_minus neg_less_iff_less reals_Archimedean2)
finally show "emeasure (interval_measure F) {..x} = F x"
by simp
then show "measure (interval_measure F) {..x} = F x"
by (simp add: measure_def)
qed

lemma cdf_interval_measure:
"(⋀ x y. x ≤ y ⟹ F x ≤ F y) ⟹ (⋀a. continuous (at_right a) F) ⟹ (F ⤏ 0) at_bot ⟹ cdf (interval_measure F) = F"
by (simp add: cdf_def fun_eq_iff measure_interval_measure_Iic)

end
```