author | haftmann |
Wed, 07 Apr 2021 12:28:19 +0000 | |
changeset 73536 | 5131c388a9b0 |
parent 73253 | f6bb31879698 |
child 75455 | 91c16c5ad3e9 |
permissions | -rw-r--r-- |
73253
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1 |
(* |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
2 |
File: Product_PMF.thy |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
3 |
Authors: Manuel Eberl, Max W. Haslbeck |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
4 |
*) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
5 |
section \<open>Indexed products of PMFs\<close> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
6 |
theory Product_PMF |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
7 |
imports Probability_Mass_Function Independent_Family |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
8 |
begin |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
9 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
10 |
subsection \<open>Preliminaries\<close> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
11 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
12 |
lemma pmf_expectation_eq_infsetsum: "measure_pmf.expectation p f = infsetsum (\<lambda>x. pmf p x * f x) UNIV" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
13 |
unfolding infsetsum_def measure_pmf_eq_density by (subst integral_density) simp_all |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
14 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
15 |
lemma measure_pmf_prob_product: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
16 |
assumes "countable A" "countable B" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
17 |
shows "measure_pmf.prob (pair_pmf M N) (A \<times> B) = measure_pmf.prob M A * measure_pmf.prob N B" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
18 |
proof - |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
19 |
have "measure_pmf.prob (pair_pmf M N) (A \<times> B) = (\<Sum>\<^sub>a(a, b)\<in>A \<times> B. pmf M a * pmf N b)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
20 |
by (auto intro!: infsetsum_cong simp add: measure_pmf_conv_infsetsum pmf_pair) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
21 |
also have "\<dots> = measure_pmf.prob M A * measure_pmf.prob N B" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
22 |
using assms by (subst infsetsum_product) (auto simp add: measure_pmf_conv_infsetsum) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
23 |
finally show ?thesis |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
24 |
by simp |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
25 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
26 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
27 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
28 |
subsection \<open>Definition\<close> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
29 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
30 |
text \<open> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
31 |
In analogy to @{const PiM}, we define an indexed product of PMFs. In the literature, this |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
32 |
is typically called taking a vector of independent random variables. Note that the components |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
33 |
do not have to be identically distributed. |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
34 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
35 |
The operation takes an explicit index set \<^term>\<open>A :: 'a set\<close> and a function \<^term>\<open>f :: 'a \<Rightarrow> 'b pmf\<close> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
36 |
that maps each element from \<^term>\<open>A\<close> to a PMF and defines the product measure |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
37 |
$\bigotimes_{i\in A} f(i)$ , which is represented as a \<^typ>\<open>('a \<Rightarrow> 'b) pmf\<close>. |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
38 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
39 |
Note that unlike @{const PiM}, this only works for \<^emph>\<open>finite\<close> index sets. It could |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
40 |
be extended to countable sets and beyond, but the construction becomes somewhat more involved. |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
41 |
\<close> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
42 |
definition Pi_pmf :: "'a set \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b pmf) \<Rightarrow> ('a \<Rightarrow> 'b) pmf" where |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
43 |
"Pi_pmf A dflt p = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
44 |
embed_pmf (\<lambda>f. if (\<forall>x. x \<notin> A \<longrightarrow> f x = dflt) then \<Prod>x\<in>A. pmf (p x) (f x) else 0)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
45 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
46 |
text \<open> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
47 |
A technical subtlety that needs to be addressed is this: Intuitively, the functions in the |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
48 |
support of a product distribution have domain \<open>A\<close>. However, since HOL is a total logic, these |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
49 |
functions must still return \<^emph>\<open>some\<close> value for inputs outside \<open>A\<close>. The product measure |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
50 |
@{const PiM} simply lets these functions return @{const undefined} in these cases. We chose a |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
51 |
different solution here, which is to supply a default value \<^term>\<open>dflt :: 'b\<close> that is returned |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
52 |
in these cases. |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
53 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
54 |
As one possible application, one could model the result of \<open>n\<close> different independent coin |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
55 |
tosses as @{term "Pi_pmf {0..<n} False (\<lambda>_. bernoulli_pmf (1 / 2))"}. This returns a function |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
56 |
of type \<^typ>\<open>nat \<Rightarrow> bool\<close> that maps every natural number below \<open>n\<close> to the result of the |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
57 |
corresponding coin toss, and every other natural number to \<^term>\<open>False\<close>. |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
58 |
\<close> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
59 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
60 |
lemma pmf_Pi: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
61 |
assumes A: "finite A" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
62 |
shows "pmf (Pi_pmf A dflt p) f = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
63 |
(if (\<forall>x. x \<notin> A \<longrightarrow> f x = dflt) then \<Prod>x\<in>A. pmf (p x) (f x) else 0)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
64 |
unfolding Pi_pmf_def |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
65 |
proof (rule pmf_embed_pmf, goal_cases) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
66 |
case 2 |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
67 |
define S where "S = {f. \<forall>x. x \<notin> A \<longrightarrow> f x = dflt}" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
68 |
define B where "B = (\<lambda>x. set_pmf (p x))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
69 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
70 |
have neutral_left: "(\<Prod>xa\<in>A. pmf (p xa) (f xa)) = 0" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
71 |
if "f \<in> PiE A B - (\<lambda>f. restrict f A) ` S" for f |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
72 |
proof - |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
73 |
have "restrict (\<lambda>x. if x \<in> A then f x else dflt) A \<in> (\<lambda>f. restrict f A) ` S" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
74 |
by (intro imageI) (auto simp: S_def) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
75 |
also have "restrict (\<lambda>x. if x \<in> A then f x else dflt) A = f" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
76 |
using that by (auto simp: PiE_def Pi_def extensional_def fun_eq_iff) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
77 |
finally show ?thesis using that by blast |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
78 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
79 |
have neutral_right: "(\<Prod>xa\<in>A. pmf (p xa) (f xa)) = 0" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
80 |
if "f \<in> (\<lambda>f. restrict f A) ` S - PiE A B" for f |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
81 |
proof - |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
82 |
from that obtain f' where f': "f = restrict f' A" "f' \<in> S" by auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
83 |
moreover from this and that have "restrict f' A \<notin> PiE A B" by simp |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
84 |
then obtain x where "x \<in> A" "pmf (p x) (f' x) = 0" by (auto simp: B_def set_pmf_eq) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
85 |
with f' and A show ?thesis by auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
86 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
87 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
88 |
have "(\<lambda>f. \<Prod>x\<in>A. pmf (p x) (f x)) abs_summable_on PiE A B" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
89 |
by (intro abs_summable_on_prod_PiE A) (auto simp: B_def) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
90 |
also have "?this \<longleftrightarrow> (\<lambda>f. \<Prod>x\<in>A. pmf (p x) (f x)) abs_summable_on (\<lambda>f. restrict f A) ` S" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
91 |
by (intro abs_summable_on_cong_neutral neutral_left neutral_right) auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
92 |
also have "\<dots> \<longleftrightarrow> (\<lambda>f. \<Prod>x\<in>A. pmf (p x) (restrict f A x)) abs_summable_on S" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
93 |
by (rule abs_summable_on_reindex_iff [symmetric]) (force simp: inj_on_def fun_eq_iff S_def) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
94 |
also have "\<dots> \<longleftrightarrow> (\<lambda>f. if \<forall>x. x \<notin> A \<longrightarrow> f x = dflt then \<Prod>x\<in>A. pmf (p x) (f x) else 0) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
95 |
abs_summable_on UNIV" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
96 |
by (intro abs_summable_on_cong_neutral) (auto simp: S_def) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
97 |
finally have summable: \<dots> . |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
98 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
99 |
have "1 = (\<Prod>x\<in>A. 1::real)" by simp |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
100 |
also have "(\<Prod>x\<in>A. 1) = (\<Prod>x\<in>A. \<Sum>\<^sub>ay\<in>B x. pmf (p x) y)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
101 |
unfolding B_def by (subst infsetsum_pmf_eq_1) auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
102 |
also have "(\<Prod>x\<in>A. \<Sum>\<^sub>ay\<in>B x. pmf (p x) y) = (\<Sum>\<^sub>af\<in>Pi\<^sub>E A B. \<Prod>x\<in>A. pmf (p x) (f x))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
103 |
by (intro infsetsum_prod_PiE [symmetric] A) (auto simp: B_def) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
104 |
also have "\<dots> = (\<Sum>\<^sub>af\<in>(\<lambda>f. restrict f A) ` S. \<Prod>x\<in>A. pmf (p x) (f x))" using A |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
105 |
by (intro infsetsum_cong_neutral neutral_left neutral_right refl) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
106 |
also have "\<dots> = (\<Sum>\<^sub>af\<in>S. \<Prod>x\<in>A. pmf (p x) (restrict f A x))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
107 |
by (rule infsetsum_reindex) (force simp: inj_on_def fun_eq_iff S_def) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
108 |
also have "\<dots> = (\<Sum>\<^sub>af\<in>S. \<Prod>x\<in>A. pmf (p x) (f x))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
109 |
by (intro infsetsum_cong) (auto simp: S_def) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
110 |
also have "\<dots> = (\<Sum>\<^sub>af. if \<forall>x. x \<notin> A \<longrightarrow> f x = dflt then \<Prod>x\<in>A. pmf (p x) (f x) else 0)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
111 |
by (intro infsetsum_cong_neutral) (auto simp: S_def) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
112 |
also have "ennreal \<dots> = (\<integral>\<^sup>+f. ennreal (if \<forall>x. x \<notin> A \<longrightarrow> f x = dflt |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
113 |
then \<Prod>x\<in>A. pmf (p x) (f x) else 0) \<partial>count_space UNIV)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
114 |
by (intro nn_integral_conv_infsetsum [symmetric] summable) (auto simp: prod_nonneg) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
115 |
finally show ?case by simp |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
116 |
qed (auto simp: prod_nonneg) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
117 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
118 |
lemma Pi_pmf_cong: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
119 |
assumes "A = A'" "dflt = dflt'" "\<And>x. x \<in> A \<Longrightarrow> f x = f' x" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
120 |
shows "Pi_pmf A dflt f = Pi_pmf A' dflt' f'" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
121 |
proof - |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
122 |
have "(\<lambda>fa. if \<forall>x. x \<notin> A \<longrightarrow> fa x = dflt then \<Prod>x\<in>A. pmf (f x) (fa x) else 0) = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
123 |
(\<lambda>f. if \<forall>x. x \<notin> A' \<longrightarrow> f x = dflt' then \<Prod>x\<in>A'. pmf (f' x) (f x) else 0)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
124 |
using assms by (intro ext) (auto intro!: prod.cong) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
125 |
thus ?thesis |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
126 |
by (simp only: Pi_pmf_def) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
127 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
128 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
129 |
lemma pmf_Pi': |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
130 |
assumes "finite A" "\<And>x. x \<notin> A \<Longrightarrow> f x = dflt" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
131 |
shows "pmf (Pi_pmf A dflt p) f = (\<Prod>x\<in>A. pmf (p x) (f x))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
132 |
using assms by (subst pmf_Pi) auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
133 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
134 |
lemma pmf_Pi_outside: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
135 |
assumes "finite A" "\<exists>x. x \<notin> A \<and> f x \<noteq> dflt" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
136 |
shows "pmf (Pi_pmf A dflt p) f = 0" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
137 |
using assms by (subst pmf_Pi) auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
138 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
139 |
lemma pmf_Pi_empty [simp]: "Pi_pmf {} dflt p = return_pmf (\<lambda>_. dflt)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
140 |
by (intro pmf_eqI, subst pmf_Pi) (auto simp: indicator_def) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
141 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
142 |
lemma set_Pi_pmf_subset: "finite A \<Longrightarrow> set_pmf (Pi_pmf A dflt p) \<subseteq> {f. \<forall>x. x \<notin> A \<longrightarrow> f x = dflt}" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
143 |
by (auto simp: set_pmf_eq pmf_Pi) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
144 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
145 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
146 |
subsection \<open>Dependent product sets with a default\<close> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
147 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
148 |
text \<open> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
149 |
The following describes a dependent product of sets where the functions are required to return |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
150 |
the default value \<^term>\<open>dflt\<close> outside their domain, in analogy to @{const PiE}, which uses |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
151 |
@{const undefined}. |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
152 |
\<close> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
153 |
definition PiE_dflt |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
154 |
where "PiE_dflt A dflt B = {f. \<forall>x. (x \<in> A \<longrightarrow> f x \<in> B x) \<and> (x \<notin> A \<longrightarrow> f x = dflt)}" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
155 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
156 |
lemma restrict_PiE_dflt: "(\<lambda>h. restrict h A) ` PiE_dflt A dflt B = PiE A B" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
157 |
proof (intro equalityI subsetI) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
158 |
fix h assume "h \<in> (\<lambda>h. restrict h A) ` PiE_dflt A dflt B" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
159 |
thus "h \<in> PiE A B" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
160 |
by (auto simp: PiE_dflt_def) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
161 |
next |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
162 |
fix h assume h: "h \<in> PiE A B" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
163 |
hence "restrict (\<lambda>x. if x \<in> A then h x else dflt) A \<in> (\<lambda>h. restrict h A) ` PiE_dflt A dflt B" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
164 |
by (intro imageI) (auto simp: PiE_def extensional_def PiE_dflt_def) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
165 |
also have "restrict (\<lambda>x. if x \<in> A then h x else dflt) A = h" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
166 |
using h by (auto simp: fun_eq_iff) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
167 |
finally show "h \<in> (\<lambda>h. restrict h A) ` PiE_dflt A dflt B" . |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
168 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
169 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
170 |
lemma dflt_image_PiE: "(\<lambda>h x. if x \<in> A then h x else dflt) ` PiE A B = PiE_dflt A dflt B" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
171 |
(is "?f ` ?X = ?Y") |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
172 |
proof (intro equalityI subsetI) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
173 |
fix h assume "h \<in> ?f ` ?X" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
174 |
thus "h \<in> ?Y" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
175 |
by (auto simp: PiE_dflt_def PiE_def) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
176 |
next |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
177 |
fix h assume h: "h \<in> ?Y" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
178 |
hence "?f (restrict h A) \<in> ?f ` ?X" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
179 |
by (intro imageI) (auto simp: PiE_def extensional_def PiE_dflt_def) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
180 |
also have "?f (restrict h A) = h" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
181 |
using h by (auto simp: fun_eq_iff PiE_dflt_def) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
182 |
finally show "h \<in> ?f ` ?X" . |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
183 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
184 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
185 |
lemma finite_PiE_dflt [intro]: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
186 |
assumes "finite A" "\<And>x. x \<in> A \<Longrightarrow> finite (B x)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
187 |
shows "finite (PiE_dflt A d B)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
188 |
proof - |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
189 |
have "PiE_dflt A d B = (\<lambda>f x. if x \<in> A then f x else d) ` PiE A B" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
190 |
by (rule dflt_image_PiE [symmetric]) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
191 |
also have "finite \<dots>" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
192 |
by (intro finite_imageI finite_PiE assms) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
193 |
finally show ?thesis . |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
194 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
195 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
196 |
lemma card_PiE_dflt: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
197 |
assumes "finite A" "\<And>x. x \<in> A \<Longrightarrow> finite (B x)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
198 |
shows "card (PiE_dflt A d B) = (\<Prod>x\<in>A. card (B x))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
199 |
proof - |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
200 |
from assms have "(\<Prod>x\<in>A. card (B x)) = card (PiE A B)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
201 |
by (intro card_PiE [symmetric]) auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
202 |
also have "PiE A B = (\<lambda>f. restrict f A) ` PiE_dflt A d B" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
203 |
by (rule restrict_PiE_dflt [symmetric]) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
204 |
also have "card \<dots> = card (PiE_dflt A d B)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
205 |
by (intro card_image) (force simp: inj_on_def restrict_def fun_eq_iff PiE_dflt_def) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
206 |
finally show ?thesis .. |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
207 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
208 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
209 |
lemma PiE_dflt_empty_iff [simp]: "PiE_dflt A dflt B = {} \<longleftrightarrow> (\<exists>x\<in>A. B x = {})" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
210 |
by (simp add: dflt_image_PiE [symmetric] PiE_eq_empty_iff) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
211 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
212 |
lemma set_Pi_pmf_subset': |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
213 |
assumes "finite A" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
214 |
shows "set_pmf (Pi_pmf A dflt p) \<subseteq> PiE_dflt A dflt (set_pmf \<circ> p)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
215 |
using assms by (auto simp: set_pmf_eq pmf_Pi PiE_dflt_def) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
216 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
217 |
lemma set_Pi_pmf: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
218 |
assumes "finite A" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
219 |
shows "set_pmf (Pi_pmf A dflt p) = PiE_dflt A dflt (set_pmf \<circ> p)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
220 |
proof (rule equalityI) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
221 |
show "PiE_dflt A dflt (set_pmf \<circ> p) \<subseteq> set_pmf (Pi_pmf A dflt p)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
222 |
proof safe |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
223 |
fix f assume f: "f \<in> PiE_dflt A dflt (set_pmf \<circ> p)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
224 |
hence "pmf (Pi_pmf A dflt p) f = (\<Prod>x\<in>A. pmf (p x) (f x))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
225 |
using assms by (auto simp: pmf_Pi PiE_dflt_def) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
226 |
also have "\<dots> > 0" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
227 |
using f by (intro prod_pos) (auto simp: PiE_dflt_def set_pmf_eq) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
228 |
finally show "f \<in> set_pmf (Pi_pmf A dflt p)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
229 |
by (auto simp: set_pmf_eq) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
230 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
231 |
qed (use set_Pi_pmf_subset'[OF assms, of dflt p] in auto) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
232 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
233 |
text \<open> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
234 |
The probability of an independent combination of events is precisely the product |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
235 |
of the probabilities of each individual event. |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
236 |
\<close> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
237 |
lemma measure_Pi_pmf_PiE_dflt: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
238 |
assumes [simp]: "finite A" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
239 |
shows "measure_pmf.prob (Pi_pmf A dflt p) (PiE_dflt A dflt B) = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
240 |
(\<Prod>x\<in>A. measure_pmf.prob (p x) (B x))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
241 |
proof - |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
242 |
define B' where "B' = (\<lambda>x. B x \<inter> set_pmf (p x))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
243 |
have "measure_pmf.prob (Pi_pmf A dflt p) (PiE_dflt A dflt B) = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
244 |
(\<Sum>\<^sub>ah\<in>PiE_dflt A dflt B. pmf (Pi_pmf A dflt p) h)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
245 |
by (rule measure_pmf_conv_infsetsum) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
246 |
also have "\<dots> = (\<Sum>\<^sub>ah\<in>PiE_dflt A dflt B. \<Prod>x\<in>A. pmf (p x) (h x))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
247 |
by (intro infsetsum_cong, subst pmf_Pi') (auto simp: PiE_dflt_def) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
248 |
also have "\<dots> = (\<Sum>\<^sub>ah\<in>(\<lambda>h. restrict h A) ` PiE_dflt A dflt B. \<Prod>x\<in>A. pmf (p x) (h x))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
249 |
by (subst infsetsum_reindex) (force simp: inj_on_def PiE_dflt_def fun_eq_iff)+ |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
250 |
also have "(\<lambda>h. restrict h A) ` PiE_dflt A dflt B = PiE A B" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
251 |
by (rule restrict_PiE_dflt) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
252 |
also have "(\<Sum>\<^sub>ah\<in>PiE A B. \<Prod>x\<in>A. pmf (p x) (h x)) = (\<Sum>\<^sub>ah\<in>PiE A B'. \<Prod>x\<in>A. pmf (p x) (h x))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
253 |
by (intro infsetsum_cong_neutral) (auto simp: B'_def set_pmf_eq) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
254 |
also have "(\<Sum>\<^sub>ah\<in>PiE A B'. \<Prod>x\<in>A. pmf (p x) (h x)) = (\<Prod>x\<in>A. infsetsum (pmf (p x)) (B' x))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
255 |
by (intro infsetsum_prod_PiE) (auto simp: B'_def) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
256 |
also have "\<dots> = (\<Prod>x\<in>A. infsetsum (pmf (p x)) (B x))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
257 |
by (intro prod.cong infsetsum_cong_neutral) (auto simp: B'_def set_pmf_eq) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
258 |
also have "\<dots> = (\<Prod>x\<in>A. measure_pmf.prob (p x) (B x))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
259 |
by (subst measure_pmf_conv_infsetsum) (rule refl) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
260 |
finally show ?thesis . |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
261 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
262 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
263 |
lemma measure_Pi_pmf_Pi: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
264 |
fixes t::nat |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
265 |
assumes [simp]: "finite A" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
266 |
shows "measure_pmf.prob (Pi_pmf A dflt p) (Pi A B) = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
267 |
(\<Prod>x\<in>A. measure_pmf.prob (p x) (B x))" (is "?lhs = ?rhs") |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
268 |
proof - |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
269 |
have "?lhs = measure_pmf.prob (Pi_pmf A dflt p) (PiE_dflt A dflt B)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
270 |
by (intro measure_prob_cong_0) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
271 |
(auto simp: PiE_dflt_def PiE_def intro!: pmf_Pi_outside)+ |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
272 |
also have "\<dots> = ?rhs" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
273 |
using assms by (simp add: measure_Pi_pmf_PiE_dflt) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
274 |
finally show ?thesis |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
275 |
by simp |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
276 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
277 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
278 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
279 |
subsection \<open>Common PMF operations on products\<close> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
280 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
281 |
text \<open> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
282 |
@{const Pi_pmf} distributes over the `bind' operation in the Giry monad: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
283 |
\<close> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
284 |
lemma Pi_pmf_bind: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
285 |
assumes "finite A" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
286 |
shows "Pi_pmf A d (\<lambda>x. bind_pmf (p x) (q x)) = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
287 |
do {f \<leftarrow> Pi_pmf A d' p; Pi_pmf A d (\<lambda>x. q x (f x))}" (is "?lhs = ?rhs") |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
288 |
proof (rule pmf_eqI, goal_cases) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
289 |
case (1 f) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
290 |
show ?case |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
291 |
proof (cases "\<exists>x\<in>-A. f x \<noteq> d") |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
292 |
case False |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
293 |
define B where "B = (\<lambda>x. set_pmf (p x))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
294 |
have [simp]: "countable (B x)" for x by (auto simp: B_def) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
295 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
296 |
{ |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
297 |
fix x :: 'a |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
298 |
have "(\<lambda>a. pmf (p x) a * 1) abs_summable_on B x" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
299 |
by (simp add: pmf_abs_summable) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
300 |
moreover have "norm (pmf (p x) a * 1) \<ge> norm (pmf (p x) a * pmf (q x a) (f x))" for a |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
301 |
unfolding norm_mult by (intro mult_left_mono) (auto simp: pmf_le_1) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
302 |
ultimately have "(\<lambda>a. pmf (p x) a * pmf (q x a) (f x)) abs_summable_on B x" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
303 |
by (rule abs_summable_on_comparison_test) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
304 |
} note summable = this |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
305 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
306 |
have "pmf ?rhs f = (\<Sum>\<^sub>ag. pmf (Pi_pmf A d' p) g * (\<Prod>x\<in>A. pmf (q x (g x)) (f x)))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
307 |
by (subst pmf_bind, subst pmf_Pi') |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
308 |
(insert assms False, simp_all add: pmf_expectation_eq_infsetsum) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
309 |
also have "\<dots> = (\<Sum>\<^sub>ag\<in>PiE_dflt A d' B. |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
310 |
pmf (Pi_pmf A d' p) g * (\<Prod>x\<in>A. pmf (q x (g x)) (f x)))" unfolding B_def |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
311 |
using assms by (intro infsetsum_cong_neutral) (auto simp: pmf_Pi PiE_dflt_def set_pmf_eq) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
312 |
also have "\<dots> = (\<Sum>\<^sub>ag\<in>PiE_dflt A d' B. |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
313 |
(\<Prod>x\<in>A. pmf (p x) (g x) * pmf (q x (g x)) (f x)))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
314 |
using assms by (intro infsetsum_cong) (auto simp: pmf_Pi PiE_dflt_def prod.distrib) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
315 |
also have "\<dots> = (\<Sum>\<^sub>ag\<in>(\<lambda>g. restrict g A) ` PiE_dflt A d' B. |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
316 |
(\<Prod>x\<in>A. pmf (p x) (g x) * pmf (q x (g x)) (f x)))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
317 |
by (subst infsetsum_reindex) (force simp: PiE_dflt_def inj_on_def fun_eq_iff)+ |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
318 |
also have "(\<lambda>g. restrict g A) ` PiE_dflt A d' B = PiE A B" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
319 |
by (rule restrict_PiE_dflt) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
320 |
also have "(\<Sum>\<^sub>ag\<in>\<dots>. (\<Prod>x\<in>A. pmf (p x) (g x) * pmf (q x (g x)) (f x))) = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
321 |
(\<Prod>x\<in>A. \<Sum>\<^sub>aa\<in>B x. pmf (p x) a * pmf (q x a) (f x))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
322 |
using assms summable by (subst infsetsum_prod_PiE) simp_all |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
323 |
also have "\<dots> = (\<Prod>x\<in>A. \<Sum>\<^sub>aa. pmf (p x) a * pmf (q x a) (f x))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
324 |
by (intro prod.cong infsetsum_cong_neutral) (auto simp: B_def set_pmf_eq) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
325 |
also have "\<dots> = pmf ?lhs f" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
326 |
using False assms by (subst pmf_Pi') (simp_all add: pmf_bind pmf_expectation_eq_infsetsum) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
327 |
finally show ?thesis .. |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
328 |
next |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
329 |
case True |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
330 |
have "pmf ?rhs f = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
331 |
measure_pmf.expectation (Pi_pmf A d' p) (\<lambda>x. pmf (Pi_pmf A d (\<lambda>xa. q xa (x xa))) f)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
332 |
using assms by (simp add: pmf_bind) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
333 |
also have "\<dots> = measure_pmf.expectation (Pi_pmf A d' p) (\<lambda>x. 0)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
334 |
using assms True by (intro Bochner_Integration.integral_cong pmf_Pi_outside) auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
335 |
also have "\<dots> = pmf ?lhs f" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
336 |
using assms True by (subst pmf_Pi_outside) auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
337 |
finally show ?thesis .. |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
338 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
339 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
340 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
341 |
lemma Pi_pmf_return_pmf [simp]: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
342 |
assumes "finite A" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
343 |
shows "Pi_pmf A dflt (\<lambda>x. return_pmf (f x)) = return_pmf (\<lambda>x. if x \<in> A then f x else dflt)" |
73536 | 344 |
using assms by (intro pmf_eqI) (auto simp: pmf_Pi simp: indicator_def split: if_splits) |
73253
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
345 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
346 |
text \<open> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
347 |
Analogously any componentwise mapping can be pulled outside the product: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
348 |
\<close> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
349 |
lemma Pi_pmf_map: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
350 |
assumes [simp]: "finite A" and "f dflt = dflt'" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
351 |
shows "Pi_pmf A dflt' (\<lambda>x. map_pmf f (g x)) = map_pmf (\<lambda>h. f \<circ> h) (Pi_pmf A dflt g)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
352 |
proof - |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
353 |
have "Pi_pmf A dflt' (\<lambda>x. map_pmf f (g x)) = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
354 |
Pi_pmf A dflt' (\<lambda>x. g x \<bind> (\<lambda>x. return_pmf (f x)))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
355 |
using assms by (simp add: map_pmf_def Pi_pmf_bind) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
356 |
also have "\<dots> = Pi_pmf A dflt g \<bind> (\<lambda>h. return_pmf (\<lambda>x. if x \<in> A then f (h x) else dflt'))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
357 |
by (subst Pi_pmf_bind[where d' = dflt]) (auto simp: ) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
358 |
also have "\<dots> = map_pmf (\<lambda>h. f \<circ> h) (Pi_pmf A dflt g)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
359 |
unfolding map_pmf_def using set_Pi_pmf_subset'[of A dflt g] |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
360 |
by (intro bind_pmf_cong refl arg_cong[of _ _ return_pmf]) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
361 |
(auto dest: simp: fun_eq_iff PiE_dflt_def assms(2)) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
362 |
finally show ?thesis . |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
363 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
364 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
365 |
text \<open> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
366 |
We can exchange the default value in a product of PMFs like this: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
367 |
\<close> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
368 |
lemma Pi_pmf_default_swap: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
369 |
assumes "finite A" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
370 |
shows "map_pmf (\<lambda>f x. if x \<in> A then f x else dflt') (Pi_pmf A dflt p) = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
371 |
Pi_pmf A dflt' p" (is "?lhs = ?rhs") |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
372 |
proof (rule pmf_eqI, goal_cases) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
373 |
case (1 f) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
374 |
let ?B = "(\<lambda>f x. if x \<in> A then f x else dflt') -` {f} \<inter> PiE_dflt A dflt (\<lambda>_. UNIV)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
375 |
show ?case |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
376 |
proof (cases "\<exists>x\<in>-A. f x \<noteq> dflt'") |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
377 |
case False |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
378 |
let ?f' = "\<lambda>x. if x \<in> A then f x else dflt" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
379 |
from False have "pmf ?lhs f = measure_pmf.prob (Pi_pmf A dflt p) ?B" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
380 |
using assms unfolding pmf_map |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
381 |
by (intro measure_prob_cong_0) (auto simp: PiE_dflt_def pmf_Pi_outside) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
382 |
also from False have "?B = {?f'}" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
383 |
by (auto simp: fun_eq_iff PiE_dflt_def) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
384 |
also have "measure_pmf.prob (Pi_pmf A dflt p) {?f'} = pmf (Pi_pmf A dflt p) ?f'" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
385 |
by (simp add: measure_pmf_single) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
386 |
also have "\<dots> = pmf ?rhs f" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
387 |
using False assms by (subst (1 2) pmf_Pi) auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
388 |
finally show ?thesis . |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
389 |
next |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
390 |
case True |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
391 |
have "pmf ?lhs f = measure_pmf.prob (Pi_pmf A dflt p) ?B" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
392 |
using assms unfolding pmf_map |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
393 |
by (intro measure_prob_cong_0) (auto simp: PiE_dflt_def pmf_Pi_outside) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
394 |
also from True have "?B = {}" by auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
395 |
also have "measure_pmf.prob (Pi_pmf A dflt p) \<dots> = 0" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
396 |
by simp |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
397 |
also have "0 = pmf ?rhs f" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
398 |
using True assms by (intro pmf_Pi_outside [symmetric]) auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
399 |
finally show ?thesis . |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
400 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
401 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
402 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
403 |
text \<open> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
404 |
The following rule allows reindexing the product: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
405 |
\<close> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
406 |
lemma Pi_pmf_bij_betw: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
407 |
assumes "finite A" "bij_betw h A B" "\<And>x. x \<notin> A \<Longrightarrow> h x \<notin> B" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
408 |
shows "Pi_pmf A dflt (\<lambda>_. f) = map_pmf (\<lambda>g. g \<circ> h) (Pi_pmf B dflt (\<lambda>_. f))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
409 |
(is "?lhs = ?rhs") |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
410 |
proof - |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
411 |
have B: "finite B" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
412 |
using assms bij_betw_finite by auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
413 |
have "pmf ?lhs g = pmf ?rhs g" for g |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
414 |
proof (cases "\<forall>a. a \<notin> A \<longrightarrow> g a = dflt") |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
415 |
case True |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
416 |
define h' where "h' = the_inv_into A h" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
417 |
have h': "h' (h x) = x" if "x \<in> A" for x |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
418 |
unfolding h'_def using that assms by (auto simp add: bij_betw_def the_inv_into_f_f) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
419 |
have h: "h (h' x) = x" if "x \<in> B" for x |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
420 |
unfolding h'_def using that assms f_the_inv_into_f_bij_betw by fastforce |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
421 |
have "pmf ?rhs g = measure_pmf.prob (Pi_pmf B dflt (\<lambda>_. f)) ((\<lambda>g. g \<circ> h) -` {g})" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
422 |
unfolding pmf_map by simp |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
423 |
also have "\<dots> = measure_pmf.prob (Pi_pmf B dflt (\<lambda>_. f)) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
424 |
(((\<lambda>g. g \<circ> h) -` {g}) \<inter> PiE_dflt B dflt (\<lambda>_. UNIV))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
425 |
using B by (intro measure_prob_cong_0) (auto simp: PiE_dflt_def pmf_Pi_outside) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
426 |
also have "\<dots> = pmf (Pi_pmf B dflt (\<lambda>_. f)) (\<lambda>x. if x \<in> B then g (h' x) else dflt)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
427 |
proof - |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
428 |
have "(if h x \<in> B then g (h' (h x)) else dflt) = g x" for x |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
429 |
using h' assms True by (cases "x \<in> A") (auto simp add: bij_betwE) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
430 |
then have "(\<lambda>g. g \<circ> h) -` {g} \<inter> PiE_dflt B dflt (\<lambda>_. UNIV) = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
431 |
{(\<lambda>x. if x \<in> B then g (h' x) else dflt)}" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
432 |
using assms h' h True unfolding PiE_dflt_def by auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
433 |
then show ?thesis |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
434 |
by (simp add: measure_pmf_single) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
435 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
436 |
also have "\<dots> = pmf (Pi_pmf A dflt (\<lambda>_. f)) g" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
437 |
using B assms True h'_def |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
438 |
by (auto simp add: pmf_Pi intro!: prod.reindex_bij_betw bij_betw_the_inv_into) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
439 |
finally show ?thesis |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
440 |
by simp |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
441 |
next |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
442 |
case False |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
443 |
have "pmf ?rhs g = infsetsum (pmf (Pi_pmf B dflt (\<lambda>_. f))) ((\<lambda>g. g \<circ> h) -` {g})" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
444 |
using assms by (auto simp add: measure_pmf_conv_infsetsum pmf_map) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
445 |
also have "\<dots> = infsetsum (\<lambda>_. 0) ((\<lambda>g x. g (h x)) -` {g})" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
446 |
using B False assms by (intro infsetsum_cong pmf_Pi_outside) fastforce+ |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
447 |
also have "\<dots> = 0" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
448 |
by simp |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
449 |
finally show ?thesis |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
450 |
using assms False by (auto simp add: pmf_Pi pmf_map) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
451 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
452 |
then show ?thesis |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
453 |
by (rule pmf_eqI) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
454 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
455 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
456 |
text \<open> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
457 |
A product of uniform random choices is again a uniform distribution. |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
458 |
\<close> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
459 |
lemma Pi_pmf_of_set: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
460 |
assumes "finite A" "\<And>x. x \<in> A \<Longrightarrow> finite (B x)" "\<And>x. x \<in> A \<Longrightarrow> B x \<noteq> {}" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
461 |
shows "Pi_pmf A d (\<lambda>x. pmf_of_set (B x)) = pmf_of_set (PiE_dflt A d B)" (is "?lhs = ?rhs") |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
462 |
proof (rule pmf_eqI, goal_cases) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
463 |
case (1 f) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
464 |
show ?case |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
465 |
proof (cases "\<exists>x. x \<notin> A \<and> f x \<noteq> d") |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
466 |
case True |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
467 |
hence "pmf ?lhs f = 0" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
468 |
using assms by (intro pmf_Pi_outside) (auto simp: PiE_dflt_def) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
469 |
also from True have "f \<notin> PiE_dflt A d B" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
470 |
by (auto simp: PiE_dflt_def) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
471 |
hence "0 = pmf ?rhs f" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
472 |
using assms by (subst pmf_of_set) auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
473 |
finally show ?thesis . |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
474 |
next |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
475 |
case False |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
476 |
hence "pmf ?lhs f = (\<Prod>x\<in>A. pmf (pmf_of_set (B x)) (f x))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
477 |
using assms by (subst pmf_Pi') auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
478 |
also have "\<dots> = (\<Prod>x\<in>A. indicator (B x) (f x) / real (card (B x)))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
479 |
by (intro prod.cong refl, subst pmf_of_set) (use assms False in auto) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
480 |
also have "\<dots> = (\<Prod>x\<in>A. indicator (B x) (f x)) / real (\<Prod>x\<in>A. card (B x))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
481 |
by (subst prod_dividef) simp_all |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
482 |
also have "(\<Prod>x\<in>A. indicator (B x) (f x) :: real) = indicator (PiE_dflt A d B) f" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
483 |
using assms False by (auto simp: indicator_def PiE_dflt_def) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
484 |
also have "(\<Prod>x\<in>A. card (B x)) = card (PiE_dflt A d B)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
485 |
using assms by (intro card_PiE_dflt [symmetric]) auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
486 |
also have "indicator (PiE_dflt A d B) f / \<dots> = pmf ?rhs f" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
487 |
using assms by (intro pmf_of_set [symmetric]) auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
488 |
finally show ?thesis . |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
489 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
490 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
491 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
492 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
493 |
subsection \<open>Merging and splitting PMF products\<close> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
494 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
495 |
text \<open> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
496 |
The following lemma shows that we can add a single PMF to a product: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
497 |
\<close> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
498 |
lemma Pi_pmf_insert: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
499 |
assumes "finite A" "x \<notin> A" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
500 |
shows "Pi_pmf (insert x A) dflt p = map_pmf (\<lambda>(y,f). f(x:=y)) (pair_pmf (p x) (Pi_pmf A dflt p))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
501 |
proof (intro pmf_eqI) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
502 |
fix f |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
503 |
let ?M = "pair_pmf (p x) (Pi_pmf A dflt p)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
504 |
have "pmf (map_pmf (\<lambda>(y, f). f(x := y)) ?M) f = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
505 |
measure_pmf.prob ?M ((\<lambda>(y, f). f(x := y)) -` {f})" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
506 |
by (subst pmf_map) auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
507 |
also have "((\<lambda>(y, f). f(x := y)) -` {f}) = (\<Union>y'. {(f x, f(x := y'))})" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
508 |
by (auto simp: fun_upd_def fun_eq_iff) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
509 |
also have "measure_pmf.prob ?M \<dots> = measure_pmf.prob ?M {(f x, f(x := dflt))}" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
510 |
using assms by (intro measure_prob_cong_0) (auto simp: pmf_pair pmf_Pi split: if_splits) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
511 |
also have "\<dots> = pmf (p x) (f x) * pmf (Pi_pmf A dflt p) (f(x := dflt))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
512 |
by (simp add: measure_pmf_single pmf_pair pmf_Pi) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
513 |
also have "\<dots> = pmf (Pi_pmf (insert x A) dflt p) f" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
514 |
proof (cases "\<forall>y. y \<notin> insert x A \<longrightarrow> f y = dflt") |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
515 |
case True |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
516 |
with assms have "pmf (p x) (f x) * pmf (Pi_pmf A dflt p) (f(x := dflt)) = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
517 |
pmf (p x) (f x) * (\<Prod>xa\<in>A. pmf (p xa) ((f(x := dflt)) xa))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
518 |
by (subst pmf_Pi') auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
519 |
also have "(\<Prod>xa\<in>A. pmf (p xa) ((f(x := dflt)) xa)) = (\<Prod>xa\<in>A. pmf (p xa) (f xa))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
520 |
using assms by (intro prod.cong) auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
521 |
also have "pmf (p x) (f x) * \<dots> = pmf (Pi_pmf (insert x A) dflt p) f" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
522 |
using assms True by (subst pmf_Pi') auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
523 |
finally show ?thesis . |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
524 |
qed (insert assms, auto simp: pmf_Pi) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
525 |
finally show "\<dots> = pmf (map_pmf (\<lambda>(y, f). f(x := y)) ?M) f" .. |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
526 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
527 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
528 |
lemma Pi_pmf_insert': |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
529 |
assumes "finite A" "x \<notin> A" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
530 |
shows "Pi_pmf (insert x A) dflt p = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
531 |
do {y \<leftarrow> p x; f \<leftarrow> Pi_pmf A dflt p; return_pmf (f(x := y))}" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
532 |
using assms |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
533 |
by (subst Pi_pmf_insert) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
534 |
(auto simp add: map_pmf_def pair_pmf_def case_prod_beta' bind_return_pmf bind_assoc_pmf) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
535 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
536 |
lemma Pi_pmf_singleton: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
537 |
"Pi_pmf {x} dflt p = map_pmf (\<lambda>a b. if b = x then a else dflt) (p x)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
538 |
proof - |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
539 |
have "Pi_pmf {x} dflt p = map_pmf (fun_upd (\<lambda>_. dflt) x) (p x)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
540 |
by (subst Pi_pmf_insert) (simp_all add: pair_return_pmf2 pmf.map_comp o_def) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
541 |
also have "fun_upd (\<lambda>_. dflt) x = (\<lambda>z y. if y = x then z else dflt)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
542 |
by (simp add: fun_upd_def fun_eq_iff) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
543 |
finally show ?thesis . |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
544 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
545 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
546 |
text \<open> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
547 |
Projecting a product of PMFs onto a component yields the expected result: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
548 |
\<close> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
549 |
lemma Pi_pmf_component: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
550 |
assumes "finite A" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
551 |
shows "map_pmf (\<lambda>f. f x) (Pi_pmf A dflt p) = (if x \<in> A then p x else return_pmf dflt)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
552 |
proof (cases "x \<in> A") |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
553 |
case True |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
554 |
define A' where "A' = A - {x}" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
555 |
from assms and True have A': "A = insert x A'" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
556 |
by (auto simp: A'_def) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
557 |
from assms have "map_pmf (\<lambda>f. f x) (Pi_pmf A dflt p) = p x" unfolding A' |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
558 |
by (subst Pi_pmf_insert) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
559 |
(auto simp: A'_def pmf.map_comp o_def case_prod_unfold map_fst_pair_pmf) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
560 |
with True show ?thesis by simp |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
561 |
next |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
562 |
case False |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
563 |
have "map_pmf (\<lambda>f. f x) (Pi_pmf A dflt p) = map_pmf (\<lambda>_. dflt) (Pi_pmf A dflt p)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
564 |
using assms False set_Pi_pmf_subset[of A dflt p] |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
565 |
by (intro pmf.map_cong refl) (auto simp: set_pmf_eq pmf_Pi_outside) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
566 |
with False show ?thesis by simp |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
567 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
568 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
569 |
text \<open> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
570 |
We can take merge two PMF products on disjoint sets like this: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
571 |
\<close> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
572 |
lemma Pi_pmf_union: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
573 |
assumes "finite A" "finite B" "A \<inter> B = {}" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
574 |
shows "Pi_pmf (A \<union> B) dflt p = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
575 |
map_pmf (\<lambda>(f,g) x. if x \<in> A then f x else g x) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
576 |
(pair_pmf (Pi_pmf A dflt p) (Pi_pmf B dflt p))" (is "_ = map_pmf (?h A) (?q A)") |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
577 |
using assms(1,3) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
578 |
proof (induction rule: finite_induct) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
579 |
case (insert x A) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
580 |
have "map_pmf (?h (insert x A)) (?q (insert x A)) = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
581 |
do {v \<leftarrow> p x; (f, g) \<leftarrow> pair_pmf (Pi_pmf A dflt p) (Pi_pmf B dflt p); |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
582 |
return_pmf (\<lambda>y. if y \<in> insert x A then (f(x := v)) y else g y)}" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
583 |
by (subst Pi_pmf_insert) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
584 |
(insert insert.hyps insert.prems, |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
585 |
simp_all add: pair_pmf_def map_bind_pmf bind_map_pmf bind_assoc_pmf bind_return_pmf) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
586 |
also have "\<dots> = do {v \<leftarrow> p x; (f, g) \<leftarrow> ?q A; return_pmf ((?h A (f,g))(x := v))}" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
587 |
by (intro bind_pmf_cong refl) (auto simp: fun_eq_iff) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
588 |
also have "\<dots> = do {v \<leftarrow> p x; f \<leftarrow> map_pmf (?h A) (?q A); return_pmf (f(x := v))}" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
589 |
by (simp add: bind_map_pmf map_bind_pmf case_prod_unfold cong: if_cong) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
590 |
also have "\<dots> = do {v \<leftarrow> p x; f \<leftarrow> Pi_pmf (A \<union> B) dflt p; return_pmf (f(x := v))}" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
591 |
using insert.hyps and insert.prems by (intro bind_pmf_cong insert.IH [symmetric] refl) auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
592 |
also have "\<dots> = Pi_pmf (insert x (A \<union> B)) dflt p" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
593 |
by (subst Pi_pmf_insert) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
594 |
(insert assms insert.hyps insert.prems, auto simp: pair_pmf_def map_bind_pmf) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
595 |
also have "insert x (A \<union> B) = insert x A \<union> B" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
596 |
by simp |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
597 |
finally show ?case .. |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
598 |
qed (simp_all add: case_prod_unfold map_snd_pair_pmf) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
599 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
600 |
text \<open> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
601 |
We can also project a product to a subset of the indices by mapping all the other |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
602 |
indices to the default value: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
603 |
\<close> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
604 |
lemma Pi_pmf_subset: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
605 |
assumes "finite A" "A' \<subseteq> A" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
606 |
shows "Pi_pmf A' dflt p = map_pmf (\<lambda>f x. if x \<in> A' then f x else dflt) (Pi_pmf A dflt p)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
607 |
proof - |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
608 |
let ?P = "pair_pmf (Pi_pmf A' dflt p) (Pi_pmf (A - A') dflt p)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
609 |
from assms have [simp]: "finite A'" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
610 |
by (blast dest: finite_subset) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
611 |
from assms have "A = A' \<union> (A - A')" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
612 |
by blast |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
613 |
also have "Pi_pmf \<dots> dflt p = map_pmf (\<lambda>(f,g) x. if x \<in> A' then f x else g x) ?P" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
614 |
using assms by (intro Pi_pmf_union) auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
615 |
also have "map_pmf (\<lambda>f x. if x \<in> A' then f x else dflt) \<dots> = map_pmf fst ?P" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
616 |
unfolding map_pmf_comp o_def case_prod_unfold |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
617 |
using set_Pi_pmf_subset[of A' dflt p] by (intro map_pmf_cong refl) (auto simp: fun_eq_iff) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
618 |
also have "\<dots> = Pi_pmf A' dflt p" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
619 |
by (simp add: map_fst_pair_pmf) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
620 |
finally show ?thesis .. |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
621 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
622 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
623 |
lemma Pi_pmf_subset': |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
624 |
fixes f :: "'a \<Rightarrow> 'b pmf" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
625 |
assumes "finite A" "B \<subseteq> A" "\<And>x. x \<in> A - B \<Longrightarrow> f x = return_pmf dflt" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
626 |
shows "Pi_pmf A dflt f = Pi_pmf B dflt f" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
627 |
proof - |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
628 |
have "Pi_pmf (B \<union> (A - B)) dflt f = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
629 |
map_pmf (\<lambda>(f, g) x. if x \<in> B then f x else g x) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
630 |
(pair_pmf (Pi_pmf B dflt f) (Pi_pmf (A - B) dflt f))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
631 |
using assms by (intro Pi_pmf_union) (auto dest: finite_subset) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
632 |
also have "Pi_pmf (A - B) dflt f = Pi_pmf (A - B) dflt (\<lambda>_. return_pmf dflt)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
633 |
using assms by (intro Pi_pmf_cong) auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
634 |
also have "\<dots> = return_pmf (\<lambda>_. dflt)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
635 |
using assms by simp |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
636 |
also have "map_pmf (\<lambda>(f, g) x. if x \<in> B then f x else g x) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
637 |
(pair_pmf (Pi_pmf B dflt f) (return_pmf (\<lambda>_. dflt))) = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
638 |
map_pmf (\<lambda>f x. if x \<in> B then f x else dflt) (Pi_pmf B dflt f)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
639 |
by (simp add: map_pmf_def pair_pmf_def bind_assoc_pmf bind_return_pmf bind_return_pmf') |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
640 |
also have "\<dots> = Pi_pmf B dflt f" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
641 |
using assms by (intro Pi_pmf_default_swap) (auto dest: finite_subset) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
642 |
also have "B \<union> (A - B) = A" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
643 |
using assms by auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
644 |
finally show ?thesis . |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
645 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
646 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
647 |
lemma Pi_pmf_if_set: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
648 |
assumes "finite A" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
649 |
shows "Pi_pmf A dflt (\<lambda>x. if b x then f x else return_pmf dflt) = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
650 |
Pi_pmf {x\<in>A. b x} dflt f" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
651 |
proof - |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
652 |
have "Pi_pmf A dflt (\<lambda>x. if b x then f x else return_pmf dflt) = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
653 |
Pi_pmf {x\<in>A. b x} dflt (\<lambda>x. if b x then f x else return_pmf dflt)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
654 |
using assms by (intro Pi_pmf_subset') auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
655 |
also have "\<dots> = Pi_pmf {x\<in>A. b x} dflt f" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
656 |
by (intro Pi_pmf_cong) auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
657 |
finally show ?thesis . |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
658 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
659 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
660 |
lemma Pi_pmf_if_set': |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
661 |
assumes "finite A" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
662 |
shows "Pi_pmf A dflt (\<lambda>x. if b x then return_pmf dflt else f x) = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
663 |
Pi_pmf {x\<in>A. \<not>b x} dflt f" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
664 |
proof - |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
665 |
have "Pi_pmf A dflt (\<lambda>x. if b x then return_pmf dflt else f x) = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
666 |
Pi_pmf {x\<in>A. \<not>b x} dflt (\<lambda>x. if b x then return_pmf dflt else f x)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
667 |
using assms by (intro Pi_pmf_subset') auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
668 |
also have "\<dots> = Pi_pmf {x\<in>A. \<not>b x} dflt f" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
669 |
by (intro Pi_pmf_cong) auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
670 |
finally show ?thesis . |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
671 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
672 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
673 |
text \<open> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
674 |
Lastly, we can delete a single component from a product: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
675 |
\<close> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
676 |
lemma Pi_pmf_remove: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
677 |
assumes "finite A" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
678 |
shows "Pi_pmf (A - {x}) dflt p = map_pmf (\<lambda>f. f(x := dflt)) (Pi_pmf A dflt p)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
679 |
proof - |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
680 |
have "Pi_pmf (A - {x}) dflt p = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
681 |
map_pmf (\<lambda>f xa. if xa \<in> A - {x} then f xa else dflt) (Pi_pmf A dflt p)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
682 |
using assms by (intro Pi_pmf_subset) auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
683 |
also have "\<dots> = map_pmf (\<lambda>f. f(x := dflt)) (Pi_pmf A dflt p)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
684 |
using set_Pi_pmf_subset[of A dflt p] assms |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
685 |
by (intro map_pmf_cong refl) (auto simp: fun_eq_iff) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
686 |
finally show ?thesis . |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
687 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
688 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
689 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
690 |
subsection \<open>Additional properties\<close> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
691 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
692 |
lemma nn_integral_prod_Pi_pmf: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
693 |
assumes "finite A" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
694 |
shows "nn_integral (Pi_pmf A dflt p) (\<lambda>y. \<Prod>x\<in>A. f x (y x)) = (\<Prod>x\<in>A. nn_integral (p x) (f x))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
695 |
using assms |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
696 |
proof (induction rule: finite_induct) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
697 |
case (insert x A) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
698 |
have "nn_integral (Pi_pmf (insert x A) dflt p) (\<lambda>y. \<Prod>z\<in>insert x A. f z (y z)) = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
699 |
(\<integral>\<^sup>+a. \<integral>\<^sup>+b. f x a * (\<Prod>z\<in>A. f z (if z = x then a else b z)) \<partial>Pi_pmf A dflt p \<partial>p x)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
700 |
using insert by (auto simp: Pi_pmf_insert case_prod_unfold nn_integral_pair_pmf' cong: if_cong) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
701 |
also have "(\<lambda>a b. \<Prod>z\<in>A. f z (if z = x then a else b z)) = (\<lambda>a b. \<Prod>z\<in>A. f z (b z))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
702 |
by (intro ext prod.cong) (use insert.hyps in auto) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
703 |
also have "(\<integral>\<^sup>+a. \<integral>\<^sup>+b. f x a * (\<Prod>z\<in>A. f z (b z)) \<partial>Pi_pmf A dflt p \<partial>p x) = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
704 |
(\<integral>\<^sup>+y. f x y \<partial>(p x)) * (\<integral>\<^sup>+y. (\<Prod>z\<in>A. f z (y z)) \<partial>(Pi_pmf A dflt p))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
705 |
by (simp add: nn_integral_multc nn_integral_cmult) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
706 |
also have "(\<integral>\<^sup>+y. (\<Prod>z\<in>A. f z (y z)) \<partial>(Pi_pmf A dflt p)) = (\<Prod>x\<in>A. nn_integral (p x) (f x))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
707 |
by (rule insert.IH) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
708 |
also have "(\<integral>\<^sup>+y. f x y \<partial>(p x)) * \<dots> = (\<Prod>x\<in>insert x A. nn_integral (p x) (f x))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
709 |
using insert.hyps by simp |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
710 |
finally show ?case . |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
711 |
qed auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
712 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
713 |
lemma integrable_prod_Pi_pmf: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
714 |
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {real_normed_field, second_countable_topology, banach}" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
715 |
assumes "finite A" and "\<And>x. x \<in> A \<Longrightarrow> integrable (measure_pmf (p x)) (f x)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
716 |
shows "integrable (measure_pmf (Pi_pmf A dflt p)) (\<lambda>h. \<Prod>x\<in>A. f x (h x))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
717 |
proof (intro integrableI_bounded) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
718 |
have "(\<integral>\<^sup>+ x. ennreal (norm (\<Prod>xa\<in>A. f xa (x xa))) \<partial>measure_pmf (Pi_pmf A dflt p)) = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
719 |
(\<integral>\<^sup>+ x. (\<Prod>y\<in>A. ennreal (norm (f y (x y)))) \<partial>measure_pmf (Pi_pmf A dflt p))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
720 |
by (simp flip: prod_norm prod_ennreal) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
721 |
also have "\<dots> = (\<Prod>x\<in>A. \<integral>\<^sup>+ a. ennreal (norm (f x a)) \<partial>measure_pmf (p x))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
722 |
by (intro nn_integral_prod_Pi_pmf) fact |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
723 |
also have "(\<integral>\<^sup>+a. ennreal (norm (f i a)) \<partial>measure_pmf (p i)) \<noteq> top" if i: "i \<in> A" for i |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
724 |
using assms(2)[OF i] by (simp add: integrable_iff_bounded) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
725 |
hence "(\<Prod>x\<in>A. \<integral>\<^sup>+ a. ennreal (norm (f x a)) \<partial>measure_pmf (p x)) \<noteq> top" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
726 |
by (subst ennreal_prod_eq_top) auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
727 |
finally show "(\<integral>\<^sup>+ x. ennreal (norm (\<Prod>xa\<in>A. f xa (x xa))) \<partial>measure_pmf (Pi_pmf A dflt p)) < \<infinity>" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
728 |
by (simp add: top.not_eq_extremum) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
729 |
qed auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
730 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
731 |
lemma expectation_prod_Pi_pmf: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
732 |
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> real" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
733 |
assumes "finite A" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
734 |
assumes "\<And>x. x \<in> A \<Longrightarrow> integrable (measure_pmf (p x)) (f x)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
735 |
assumes "\<And>x y. x \<in> A \<Longrightarrow> y \<in> set_pmf (p x) \<Longrightarrow> f x y \<ge> 0" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
736 |
shows "measure_pmf.expectation (Pi_pmf A dflt p) (\<lambda>y. \<Prod>x\<in>A. f x (y x)) = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
737 |
(\<Prod>x\<in>A. measure_pmf.expectation (p x) (\<lambda>v. f x v))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
738 |
proof - |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
739 |
have nonneg: "measure_pmf.expectation (p x) (f x) \<ge> 0" if "x \<in> A" for x |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
740 |
using that by (intro Bochner_Integration.integral_nonneg_AE AE_pmfI assms) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
741 |
have nonneg': "0 \<le> measure_pmf.expectation (Pi_pmf A dflt p) (\<lambda>y. \<Prod>x\<in>A. f x (y x))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
742 |
by (intro Bochner_Integration.integral_nonneg_AE AE_pmfI assms prod_nonneg) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
743 |
(use assms in \<open>auto simp: set_Pi_pmf PiE_dflt_def\<close>) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
744 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
745 |
have "ennreal (measure_pmf.expectation (Pi_pmf A dflt p) (\<lambda>y. \<Prod>x\<in>A. f x (y x))) = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
746 |
nn_integral (Pi_pmf A dflt p) (\<lambda>y. ennreal (\<Prod>x\<in>A. f x (y x)))" using assms |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
747 |
by (intro nn_integral_eq_integral [symmetric] assms integrable_prod_Pi_pmf) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
748 |
(auto simp: AE_measure_pmf_iff set_Pi_pmf PiE_dflt_def prod_nonneg) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
749 |
also have "\<dots> = nn_integral (Pi_pmf A dflt p) (\<lambda>y. (\<Prod>x\<in>A. ennreal (f x (y x))))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
750 |
by (intro nn_integral_cong_AE AE_pmfI prod_ennreal [symmetric]) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
751 |
(use assms(1) in \<open>auto simp: set_Pi_pmf PiE_dflt_def intro!: assms(3)\<close>) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
752 |
also have "\<dots> = (\<Prod>x\<in>A. \<integral>\<^sup>+ a. ennreal (f x a) \<partial>measure_pmf (p x))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
753 |
by (rule nn_integral_prod_Pi_pmf) fact+ |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
754 |
also have "\<dots> = (\<Prod>x\<in>A. ennreal (measure_pmf.expectation (p x) (f x)))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
755 |
by (intro prod.cong nn_integral_eq_integral assms AE_pmfI) auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
756 |
also have "\<dots> = ennreal (\<Prod>x\<in>A. measure_pmf.expectation (p x) (f x))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
757 |
by (intro prod_ennreal nonneg) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
758 |
finally show ?thesis |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
759 |
using nonneg nonneg' by (subst (asm) ennreal_inj) (auto intro!: prod_nonneg) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
760 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
761 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
762 |
lemma indep_vars_Pi_pmf: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
763 |
assumes fin: "finite I" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
764 |
shows "prob_space.indep_vars (measure_pmf (Pi_pmf I dflt p)) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
765 |
(\<lambda>_. count_space UNIV) (\<lambda>x f. f x) I" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
766 |
proof (cases "I = {}") |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
767 |
case True |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
768 |
show ?thesis |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
769 |
by (subst prob_space.indep_vars_def [OF measure_pmf.prob_space_axioms], |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
770 |
subst prob_space.indep_sets_def [OF measure_pmf.prob_space_axioms]) (simp_all add: True) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
771 |
next |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
772 |
case [simp]: False |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
773 |
show ?thesis |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
774 |
proof (subst prob_space.indep_vars_iff_distr_eq_PiM') |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
775 |
show "distr (measure_pmf (Pi_pmf I dflt p)) (Pi\<^sub>M I (\<lambda>i. count_space UNIV)) (\<lambda>x. restrict x I) = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
776 |
Pi\<^sub>M I (\<lambda>i. distr (measure_pmf (Pi_pmf I dflt p)) (count_space UNIV) (\<lambda>f. f i))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
777 |
proof (rule product_sigma_finite.PiM_eqI, goal_cases) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
778 |
case 1 |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
779 |
interpret product_prob_space "\<lambda>i. distr (measure_pmf (Pi_pmf I dflt p)) (count_space UNIV) (\<lambda>f. f i)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
780 |
by (intro product_prob_spaceI prob_space.prob_space_distr measure_pmf.prob_space_axioms) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
781 |
simp_all |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
782 |
show ?case by unfold_locales |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
783 |
next |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
784 |
case 3 |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
785 |
have "sets (Pi\<^sub>M I (\<lambda>i. distr (measure_pmf (Pi_pmf I dflt p)) (count_space UNIV) (\<lambda>f. f i))) = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
786 |
sets (Pi\<^sub>M I (\<lambda>_. count_space UNIV))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
787 |
by (intro sets_PiM_cong) simp_all |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
788 |
thus ?case by simp |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
789 |
next |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
790 |
case (4 A) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
791 |
have "Pi\<^sub>E I A \<in> sets (Pi\<^sub>M I (\<lambda>i. count_space UNIV))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
792 |
using 4 by (intro sets_PiM_I_finite fin) auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
793 |
hence "emeasure (distr (measure_pmf (Pi_pmf I dflt p)) (Pi\<^sub>M I (\<lambda>i. count_space UNIV)) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
794 |
(\<lambda>x. restrict x I)) (Pi\<^sub>E I A) = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
795 |
emeasure (measure_pmf (Pi_pmf I dflt p)) ((\<lambda>x. restrict x I) -` Pi\<^sub>E I A)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
796 |
using 4 by (subst emeasure_distr) (auto simp: space_PiM) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
797 |
also have "\<dots> = emeasure (measure_pmf (Pi_pmf I dflt p)) (PiE_dflt I dflt A)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
798 |
by (intro emeasure_eq_AE AE_pmfI) (auto simp: PiE_dflt_def set_Pi_pmf fin) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
799 |
also have "\<dots> = (\<Prod>i\<in>I. emeasure (measure_pmf (p i)) (A i))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
800 |
by (simp add: measure_pmf.emeasure_eq_measure measure_Pi_pmf_PiE_dflt fin prod_ennreal) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
801 |
also have "\<dots> = (\<Prod>i\<in>I. emeasure (measure_pmf (map_pmf (\<lambda>f. f i) (Pi_pmf I dflt p))) (A i))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
802 |
by (intro prod.cong refl, subst Pi_pmf_component) (auto simp: fin) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
803 |
finally show ?case |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
804 |
by (simp add: map_pmf_rep_eq) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
805 |
qed fact+ |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
806 |
qed (simp_all add: measure_pmf.prob_space_axioms) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
807 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
808 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
809 |
lemma |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
810 |
fixes h :: "'a :: comm_monoid_add \<Rightarrow> 'b::{banach, second_countable_topology}" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
811 |
assumes fin: "finite I" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
812 |
assumes integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (measure_pmf (D i)) h" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
813 |
shows integrable_sum_Pi_pmf: "integrable (Pi_pmf I dflt D) (\<lambda>g. \<Sum>i\<in>I. h (g i))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
814 |
and expectation_sum_Pi_pmf: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
815 |
"measure_pmf.expectation (Pi_pmf I dflt D) (\<lambda>g. \<Sum>i\<in>I. h (g i)) = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
816 |
(\<Sum>i\<in>I. measure_pmf.expectation (D i) h)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
817 |
proof - |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
818 |
have integrable': "integrable (Pi_pmf I dflt D) (\<lambda>g. h (g i))" if i: "i \<in> I" for i |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
819 |
proof - |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
820 |
have "integrable (D i) h" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
821 |
using i by (rule assms) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
822 |
also have "D i = map_pmf (\<lambda>g. g i) (Pi_pmf I dflt D)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
823 |
by (subst Pi_pmf_component) (use fin i in auto) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
824 |
finally show "integrable (measure_pmf (Pi_pmf I dflt D)) (\<lambda>x. h (x i))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
825 |
by simp |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
826 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
827 |
thus "integrable (Pi_pmf I dflt D) (\<lambda>g. \<Sum>i\<in>I. h (g i))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
828 |
by (intro Bochner_Integration.integrable_sum) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
829 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
830 |
have "measure_pmf.expectation (Pi_pmf I dflt D) (\<lambda>x. \<Sum>i\<in>I. h (x i)) = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
831 |
(\<Sum>i\<in>I. measure_pmf.expectation (map_pmf (\<lambda>x. x i) (Pi_pmf I dflt D)) h)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
832 |
using integrable' by (subst Bochner_Integration.integral_sum) auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
833 |
also have "\<dots> = (\<Sum>i\<in>I. measure_pmf.expectation (D i) h)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
834 |
by (intro sum.cong refl, subst Pi_pmf_component) (use fin in auto) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
835 |
finally show "measure_pmf.expectation (Pi_pmf I dflt D) (\<lambda>g. \<Sum>i\<in>I. h (g i)) = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
836 |
(\<Sum>i\<in>I. measure_pmf.expectation (D i) h)" . |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
837 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
838 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
839 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
840 |
subsection \<open>Applications\<close> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
841 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
842 |
text \<open> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
843 |
Choosing a subset of a set uniformly at random is equivalent to tossing a fair coin |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
844 |
independently for each element and collecting all the elements that came up heads. |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
845 |
\<close> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
846 |
lemma pmf_of_set_Pow_conv_bernoulli: |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
847 |
assumes "finite (A :: 'a set)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
848 |
shows "map_pmf (\<lambda>b. {x\<in>A. b x}) (Pi_pmf A P (\<lambda>_. bernoulli_pmf (1/2))) = pmf_of_set (Pow A)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
849 |
proof - |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
850 |
have "Pi_pmf A P (\<lambda>_. bernoulli_pmf (1/2)) = pmf_of_set (PiE_dflt A P (\<lambda>x. UNIV))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
851 |
using assms by (simp add: bernoulli_pmf_half_conv_pmf_of_set Pi_pmf_of_set) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
852 |
also have "map_pmf (\<lambda>b. {x\<in>A. b x}) \<dots> = pmf_of_set (Pow A)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
853 |
proof - |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
854 |
have "bij_betw (\<lambda>b. {x \<in> A. b x}) (PiE_dflt A P (\<lambda>_. UNIV)) (Pow A)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
855 |
by (rule bij_betwI[of _ _ _ "\<lambda>B b. if b \<in> A then b \<in> B else P"]) (auto simp add: PiE_dflt_def) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
856 |
then show ?thesis |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
857 |
using assms by (intro map_pmf_of_set_bij_betw) auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
858 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
859 |
finally show ?thesis |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
860 |
by simp |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
861 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
862 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
863 |
text \<open> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
864 |
A binomial distribution can be seen as the number of successes in \<open>n\<close> independent coin tosses. |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
865 |
\<close> |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
866 |
lemma binomial_pmf_altdef': |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
867 |
fixes A :: "'a set" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
868 |
assumes "finite A" and "card A = n" and p: "p \<in> {0..1}" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
869 |
shows "binomial_pmf n p = |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
870 |
map_pmf (\<lambda>f. card {x\<in>A. f x}) (Pi_pmf A dflt (\<lambda>_. bernoulli_pmf p))" (is "?lhs = ?rhs") |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
871 |
proof - |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
872 |
from assms have "?lhs = binomial_pmf (card A) p" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
873 |
by simp |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
874 |
also have "\<dots> = ?rhs" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
875 |
using assms(1) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
876 |
proof (induction rule: finite_induct) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
877 |
case empty |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
878 |
with p show ?case by (simp add: binomial_pmf_0) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
879 |
next |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
880 |
case (insert x A) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
881 |
from insert.hyps have "card (insert x A) = Suc (card A)" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
882 |
by simp |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
883 |
also have "binomial_pmf \<dots> p = do { |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
884 |
b \<leftarrow> bernoulli_pmf p; |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
885 |
f \<leftarrow> Pi_pmf A dflt (\<lambda>_. bernoulli_pmf p); |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
886 |
return_pmf ((if b then 1 else 0) + card {y \<in> A. f y}) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
887 |
}" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
888 |
using p by (simp add: binomial_pmf_Suc insert.IH bind_map_pmf) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
889 |
also have "\<dots> = do { |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
890 |
b \<leftarrow> bernoulli_pmf p; |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
891 |
f \<leftarrow> Pi_pmf A dflt (\<lambda>_. bernoulli_pmf p); |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
892 |
return_pmf (card {y \<in> insert x A. (f(x := b)) y}) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
893 |
}" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
894 |
proof (intro bind_pmf_cong refl, goal_cases) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
895 |
case (1 b f) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
896 |
have "(if b then 1 else 0) + card {y\<in>A. f y} = card ((if b then {x} else {}) \<union> {y\<in>A. f y})" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
897 |
using insert.hyps by auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
898 |
also have "(if b then {x} else {}) \<union> {y\<in>A. f y} = {y\<in>insert x A. (f(x := b)) y}" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
899 |
using insert.hyps by auto |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
900 |
finally show ?case by simp |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
901 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
902 |
also have "\<dots> = map_pmf (\<lambda>f. card {y\<in>insert x A. f y}) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
903 |
(Pi_pmf (insert x A) dflt (\<lambda>_. bernoulli_pmf p))" |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
904 |
using insert.hyps by (subst Pi_pmf_insert) (simp_all add: pair_pmf_def map_bind_pmf) |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
905 |
finally show ?case . |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
906 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
907 |
finally show ?thesis . |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
908 |
qed |
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
909 |
|
f6bb31879698
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
910 |
end |