forked from Quickblink/verML
-
Notifications
You must be signed in to change notification settings - Fork 2
/
NewTry.thy
2581 lines (2225 loc) · 117 KB
/
NewTry.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
\<^marker>\<open>creator Maximilian P. L. Haslbeck\<close>
theory NewTry
imports LearningTheory
begin
paragraph \<open>Summary\<close>
text \<open>Work in Progress!
This theory attempts to prove Theorem 6.11. from @{cite UnderstandingML}.\<close>
subsection \<open>Stuff about Pi_pmf\<close>
lemma set_pmf_Pi_pmf: "\<And>S i. finite A \<Longrightarrow> S \<in> set_pmf (Pi_pmf A dflt D) \<Longrightarrow> i \<in> A \<Longrightarrow> S i \<in> set_pmf (D i)"
apply(subst set_pmf_iff)
apply(subst (asm) set_pmf_iff)
apply(subst (asm) pmf_Pi) apply simp apply auto
using prod_zero by metis
lemma set_pmf_Samples: "\<And>S i. S \<in> set_pmf (Samples m D) \<Longrightarrow> i < m \<Longrightarrow> S i \<in> set_pmf D"
unfolding Samples_def using set_pmf_Pi_pmf[OF finite_atLeastLessThan] by force
definition Samples1 :: "nat \<Rightarrow> (real) pmf \<Rightarrow> ((nat \<Rightarrow> real)) pmf" where
"Samples1 n D = Pi_pmf {0..<n} (1::real) (\<lambda>_. D)"
lemma Samples1_set_pmf : "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> y \<in> set_pmf (Samples1 m (pmf_of_set S))
\<Longrightarrow> (\<forall>i< m. y i \<in> S)"
unfolding Samples1_def apply(intro allI impI) subgoal for i
apply(drule set_pmf_Pi_pmf[OF finite_atLeastLessThan, where D="\<lambda>_. pmf_of_set S", where i=i])
by auto
done
lemma set_pmf_Pi_pmf2: "finite S \<Longrightarrow> set_pmf (Pi_pmf S dflt D) \<subseteq> {f. \<forall>s\<in>S. f s \<in> set_pmf (D s)}"
using set_pmf_Pi_pmf by fast
lemma expectation_pair_pmf:
"measure_pmf.expectation (pair_pmf p q) f
= measure_pmf.expectation p (\<lambda>x. measure_pmf.expectation q (\<lambda>y. f (x, y)))"
using nn_integral_pair_pmf'
sorry
lemma
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> real"
shows expectation_Pi_pmf_prod:
"finite A \<Longrightarrow> measure_pmf.expectation (Pi_pmf A dflt p) (\<lambda>y. prod (\<lambda>x. f x (y x)) A) =
(prod (\<lambda>x. measure_pmf.expectation (p x) (\<lambda>v. f x v)) A)"
proof (induct rule: finite_induct)
case empty
then show ?case by auto
next
case (insert a A)
have p: "\<And>x y. (\<Prod>xa\<in>A. f xa (if xa = a then x else y xa)) = (\<Prod>xa\<in>A. f xa (y xa))"
apply(rule prod.cong) apply simp using insert by auto
have "measure_pmf.expectation (Pi_pmf (insert a A) dflt p) (\<lambda>y. \<Prod>x\<in>insert a A. f x (y x))
= measure_pmf.expectation (p a) (\<lambda>x. f a x * measure_pmf.expectation (Pi_pmf A dflt p) (\<lambda>y. \<Prod>xa\<in>A. f xa (y xa)))"
apply(subst Pi_pmf_insert) apply fact apply fact
apply simp thm integral_mult_left_zero integral_map_pmf
unfolding expectation_pair_pmf
apply(subst prod.insert) apply fact apply fact
apply simp unfolding p by simp
also have "\<dots> = (\<Prod>x\<in>insert a A. measure_pmf.expectation (p x) (f x))"
apply(subst insert(3))
apply(subst prod.insert) apply fact apply fact by simp
finally show ?case .
qed
(*
lemma expectation_Pi_pmf_sum:
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> real"
assumes [simp]: "finite A"
shows "measure_pmf.expectation (Pi_pmf A dflt p) (\<lambda>y. \<Sum>x\<in>A. (f x) (y x)) =
(\<Sum>x\<in>A. measure_pmf.expectation (p x) (f x))"
using assms
proof (induct rule: finite_induct)
case empty
then show ?case by auto
next
case (insert a A)
have p: "\<And>x y. (\<Sum>xa\<in>A. f xa (if xa = a then x else y xa)) = (\<Sum>xa\<in>A. f xa (y xa))"
apply(rule sum.cong) apply simp using insert by auto
have "measure_pmf.expectation (Pi_pmf (insert a A) dflt p) (\<lambda>y. \<Sum>x\<in>insert a A. f x (y x))
= measure_pmf.expectation (p a) (\<lambda>x. f a x + measure_pmf.expectation (Pi_pmf A dflt p) (\<lambda>y. \<Sum>xa\<in>A. f xa (y xa)))"
apply(subst Pi_pmf_insert) apply fact apply fact
apply(subst integral_map_pmf)
apply(subst Bochner_Integration.integral_add)
subgoal sorry
subgoal sorry
apply simp
unfolding expectation_pair_pmf
apply(subst sum.insert) apply fact apply fact
apply simp
apply(subst Bochner_Integration.integral_add)
subgoal sorry
subgoal sorry
apply(subst Bochner_Integration.integral_add)
subgoal sorry
subgoal sorry
unfolding p by simp
also have "\<dots> = (\<Sum>x\<in>insert a A. measure_pmf.expectation (p x) (f x))"
apply(subst insert(3))
apply(subst sum.insert) apply fact apply fact
apply(subst Bochner_Integration.integral_add)
subgoal sorry
subgoal sorry
by simp
finally show ?case .
qed
*)
lemma Pi_pmf_map2:
assumes [simp]: "finite A" and "\<And>x. x\<notin>A \<Longrightarrow> f x dflt = dflt'"
shows "Pi_pmf A dflt' (\<lambda>x. map_pmf (f x) (g x)) = map_pmf (\<lambda>h. (\<lambda>x. (f x) (h x))) (Pi_pmf A dflt g)"
(is "?lhs = ?rhs")
proof (rule pmf_eqI)
fix h
show "pmf ?lhs h = pmf ?rhs h"
proof (cases "\<forall>x. x \<notin> A \<longrightarrow> h x = dflt'")
case True
hence "pmf ?lhs h = (\<Prod>x\<in>A. measure_pmf.prob (g x) (f x -` {h x}))"
by (subst pmf_Pi) (auto simp: pmf_map)
also have "\<dots> = measure_pmf.prob (Pi_pmf A dflt g) (PiE_dflt A dflt (\<lambda>x. f x -` {h x}))"
by (rule measure_Pi_pmf_PiE_dflt [symmetric]) auto
also have "PiE_dflt A dflt (\<lambda>x. f x -` {h x}) = ((\<lambda>g x. f x (g x)) -` {h}) \<inter> PiE_dflt A dflt (\<lambda>_. UNIV)"
using True by (fastforce simp: assms(2) [symmetric] fun_eq_iff PiE_dflt_def o_def)
also have "measure_pmf.prob (Pi_pmf A dflt g) \<dots> =
measure_pmf.prob (Pi_pmf A dflt g) ((\<lambda>g x. f x (g x)) -` {h})"
by (intro pmf_prob_cong) (auto simp: PiE_dflt_def pmf_Pi_outside)
also have "\<dots> = pmf ?rhs h" by (simp add: pmf_map)
finally show ?thesis .
next
case False
have "pmf ?rhs h = infsetsum (pmf (Pi_pmf A dflt g)) ((\<lambda>g x. f x (g x)) -` {h})"
by (simp add: pmf_map measure_pmf_conv_infsetsum)
also from False have "\<dots> = infsetsum (\<lambda>_. 0) ((\<lambda>g x. f x (g x)) -` {h})"
by (intro infsetsum_cong pmf_Pi_outside) (auto simp: fun_eq_iff o_def assms(2) [symmetric])
also have "\<dots> = 0" by simp
also from False have "\<dots> = pmf ?lhs h"
by (subst pmf_Pi_outside) auto
finally show ?thesis ..
qed
qed
definition "mapify f = (\<lambda>x. Some (f x))"
definition "allmaps C D = {m. dom m = C \<and> ran m \<subseteq> D}"
definition "restrictH H C D = {m\<in>(allmaps C D). \<exists>h\<in>H. m \<subseteq>\<^sub>m h}"
definition "shatters H C D \<longleftrightarrow> allmaps C D = restrictH H C D"
lemma "H\<noteq>{} \<Longrightarrow> card C \<ge> 1 \<Longrightarrow> card D \<ge> 2 \<Longrightarrow> card (restrictH H C D) \<ge> 4"
oops
lemma finitemaps: "finite C \<Longrightarrow> finite D \<Longrightarrow> finite (allmaps C D)"
by (simp add: allmaps_def finite_set_of_finite_maps)
lemma finiteres: "finite C \<Longrightarrow> finite D \<Longrightarrow> finite (restrictH H C D)"
by (simp add: finitemaps restrictH_def)
lemma auxtemp: "\<forall>h\<in>H. dom h = UNIV \<Longrightarrow> \<forall>h\<in>H. ran h \<subseteq> D \<Longrightarrow> restrictH H C D = (\<lambda>h. restrict_map h C) ` H"
proof safe
fix m
assume "m \<in> restrictH H C D"
then have s1: "dom m = C"
by (simp add: allmaps_def restrictH_def)
moreover obtain h where o1: "h\<in>H" "m \<subseteq>\<^sub>m h" using restrictH_def
proof -
assume a1: "\<And>h. \<lbrakk>h \<in> H; m \<subseteq>\<^sub>m h\<rbrakk> \<Longrightarrow> thesis"
have "m \<in> {f \<in> allmaps C D. \<exists>fa. fa \<in> H \<and> f \<subseteq>\<^sub>m fa}"
using \<open>m \<in> restrictH H C D\<close> restrictH_def by blast
then show ?thesis
using a1 by blast
qed
ultimately have "\<forall>x\<in>C. m x = h x"
by (simp add: map_le_def)
then have "\<forall>x. m x = (h |` C) x" using s1
by (metis domIff restrict_map_def)
then have "m = h |` C" by auto
then show "m\<in>(\<lambda>h. h |` C) ` H" using o1(1) by auto
next
fix h
assume a1: "h\<in>H" "\<forall>h\<in>H. ran h \<subseteq> D" "\<forall>h\<in>H. dom h = UNIV"
then have "ran (h |` C) \<subseteq> D"
by (meson ranI ran_restrictD subsetI subset_eq)
moreover have "dom (h |` C) = C" by (simp add: a1)
then show "h |` C \<in> restrictH H C D"
by (metis (mono_tags, lifting) a1(1) allmaps_def calculation map_le_def
mem_Collect_eq restrictH_def restrict_in)
qed
locale vcd =learning_basics where X=X and Y=Y and H=H
for X::"'a set" and Y::"'b set" and H :: "('a \<Rightarrow> 'b) set" +
assumes infx: "infinite X"
begin
abbreviation "H_map \<equiv> image mapify H"
definition "growth m = Max {k. \<exists>C\<subseteq>X. k = card (restrictH H_map C Y) \<and> card C = m}"
theorem growth_mono: "m \<le> m' \<Longrightarrow> growth m \<le> growth m'"
(* maybe one needs infinite X here *)
sorry
lemma "card X \<noteq> 0 \<Longrightarrow> growth m > 1"
proof -
assume "card X \<noteq> 0"
then have "X \<noteq> {}" by auto
then obtain x where "x\<in>X" by blast
show ?thesis
unfolding growth_def sorry
qed
term measure_pmf.expectation
lemma nn_integral_Markov_inequality_strict:
assumes u: "u \<in> borel_measurable M" and "A \<in> sets M"
shows "(emeasure M) ({x\<in>space M. 1 < c * u x} \<inter> A) \<le> c * (\<integral>\<^sup>+ x. u x * indicator A x \<partial>M)"
(is "(emeasure M) ?A \<le> _ * ?PI")
proof -
have "?A \<in> sets M"
using \<open>A \<in> sets M\<close> u by auto
hence "(emeasure M) ?A = (\<integral>\<^sup>+ x. indicator ?A x \<partial>M)"
using nn_integral_indicator by simp
also have "\<dots> \<le> (\<integral>\<^sup>+ x. c * (u x * indicator A x) \<partial>M)"
using u apply (auto intro!: nn_integral_mono_AE simp: indicator_def) by auto
also have "\<dots> = c * (\<integral>\<^sup>+ x. u x * indicator A x \<partial>M)"
using assms by (auto intro!: nn_integral_cmult)
finally show ?thesis .
qed
lemma integral_Markov_inequality_strict:
assumes [measurable]: "integrable M u" and "AE x in M. 0 \<le> u x" "0 < (c::real)"
shows "(emeasure M) {x\<in>space M. u x > c} \<le> (1/c) * (\<integral>x. u x \<partial>M)"
proof -
have "(\<integral>\<^sup>+ x. ennreal(u x) * indicator (space M) x \<partial>M) \<le> (\<integral>\<^sup>+ x. u x \<partial>M)"
by (rule nn_integral_mono_AE, auto simp add: \<open>c>0\<close> less_eq_real_def)
also have "... = (\<integral>x. u x \<partial>M)"
by (rule nn_integral_eq_integral, auto simp add: assms)
finally have *: "(\<integral>\<^sup>+ x. ennreal(u x) * indicator (space M) x \<partial>M) \<le> (\<integral>x. u x \<partial>M)"
by simp
have "{x \<in> space M. u x > c} = {x \<in> space M. ennreal(1/c) * u x > 1} \<inter> (space M)"
using \<open>c>0\<close> by (auto simp: ennreal_mult'[symmetric])
then have "emeasure M {x \<in> space M. u x > c} = emeasure M ({x \<in> space M. ennreal(1/c) * u x > 1} \<inter> (space M))"
by simp
also have "... \<le> ennreal(1/c) * (\<integral>\<^sup>+ x. ennreal(u x) * indicator (space M) x \<partial>M)"
by (rule nn_integral_Markov_inequality_strict) (auto simp add: assms)
also have "... \<le> ennreal(1/c) * (\<integral>x. u x \<partial>M)"
apply (rule mult_left_mono) using * \<open>c>0\<close> by auto
finally show ?thesis
using \<open>0<c\<close> by (simp add: ennreal_mult'[symmetric])
qed
lemma markov_inequality:
assumes
b: "integrable (measure_pmf D) f"
and pos: "AE x in measure_pmf D. 0 \<le> f x"
and apos: "a>0"
shows
"measure_pmf.prob D {x. f x > a} \<le> (measure_pmf.expectation D f / a)"
proof -
have "measure_pmf.expectation D f \<ge> 0"
apply(rule integral_nonneg_AE) apply(rule pos) done
then have a: "0 \<le> measure_pmf.expectation D f / a"
apply(rule divide_nonneg_pos) using apos .
have "ennreal (measure_pmf.prob D {x. f x > a})
= emeasure (measure_pmf D) {x. a < f x}"
unfolding measure_pmf.emeasure_eq_measure[symmetric] ..
also have "\<dots> = emeasure (measure_pmf D) {x\<in> space (measure_pmf D). a < f x}"
by simp
also have "\<dots> \<le> ennreal (1 / a * measure_pmf.expectation D f)"
apply(rule integral_Markov_inequality_strict)
apply(fact b) apply (fact pos) apply (fact apos) done
finally have"ennreal (measure_pmf.prob D {x. f x > a})
\<le> ennreal (1 / a * measure_pmf.expectation D f)" .
then show ?thesis apply simp
apply(subst (asm) ennreal_le_iff) apply (fact a) by simp
qed
thm integral_Markov_inequality[where c=a and u=f and M=D] measure_pmf.emeasure_eq_measure integral_real_bounded
thm ennreal_le_iff
thm integral_Markov_inequality
thm integral_Markov_inequality
thm nn_integral_Markov_inequality
lemma A :
fixes a b :: real
shows "a\<ge>1-b \<Longrightarrow> 1-a\<le>b" by auto
lemma "abs(PredErr D h - TrainErr S {0..<m} h) \<ge> 0"
by auto
lemma abs_bound_neg: "\<And>a b :: real. b\<ge>0 \<Longrightarrow> abs a \<le> b \<Longrightarrow> -b \<le> a" by auto
lemma abs_bound_pos: "\<And>a b :: real. b\<ge>0 \<Longrightarrow> abs a \<le> b \<Longrightarrow> a \<le> b" by auto
lemma assumes mgt0: "m>0"
shows TError_bounded: "abs(TrainErr S' {0..<m::nat} h - TrainErr S {0..<m::nat} h) \<le> 2"
proof -
have T: "\<And>S. abs(TrainErr S {0..<m} h) \<le> 1" using TrainErr_nn
apply(subst abs_of_nonneg) using mgt0 by (auto intro!: TrainErr_le1)
have "abs(TrainErr S' {0..<m::nat} h - TrainErr S {0..<m} h)
\<le> abs(TrainErr S' {0..<m::nat} h) + abs (TrainErr S {0..<m} h)"
by(rule abs_triangle_ineq4)
also have "\<dots> \<le> 2" apply(rule order.trans) apply(rule add_mono) apply(rule T)+ by simp
finally show ?thesis .
qed
lemma assumes mgt0: "m>0"
shows Error_bounded: "abs(PredErr D h - TrainErr S {0..<m::nat} h) \<le> 2"
proof -
have P: "abs(PredErr D h) \<le> 1" using PredErr_nn PredErr_le1
apply(subst abs_of_nonneg) by auto
have T: "abs(TrainErr S {0..<m} h) \<le> 1" using TrainErr_nn
apply(subst abs_of_nonneg) using mgt0 by (auto intro!: TrainErr_le1)
have "abs(PredErr D h - TrainErr S {0..<m} h)
\<le> abs(PredErr D h) + abs (TrainErr S {0..<m} h)"
by(rule abs_triangle_ineq4)
also have "\<dots> \<le> 2" using P T by simp
finally show ?thesis .
qed
thm Pi_pmf_component
definition TrainErr2 :: " ('d \<Rightarrow> ('e * 'f)) \<Rightarrow> 'd set \<Rightarrow> ('e \<Rightarrow> 'f) \<Rightarrow> real" where
"TrainErr2 S I h = sum (indicator {i. case (S i) of (x,y) \<Rightarrow> h x \<noteq> y}) I "
lemma PredErr_as_expectation:
"PredErr D h = measure_pmf.expectation (Samples m D) (\<lambda>S. TrainErr S {0..<m} h )"
unfolding PredErr_def unfolding TrainErr_def sorry
term measure
definition E :: "real pmf \<Rightarrow> real" where
"E M = (\<integral>x. x \<partial> measure_pmf M)"
term prob_space
(* abbreviation (in prob_space) "expectation \<equiv> integral\<^sup>L M"
abbreviation (in prob_space) "prob \<equiv> measure M" *)
lemma "E M = measure_pmf.expectation M id"
unfolding E_def
by (metis comp_id fun.map_ident)
lemma "E (map_pmf f M) = measure_pmf.expectation M f"
unfolding E_def
by simp
lemma expectation_mono:
fixes f::"'c \<Rightarrow> real"
shows
"integrable (measure_pmf M) f \<Longrightarrow>
integrable (measure_pmf M) u \<Longrightarrow> (\<And>x. x\<in>set_pmf M \<Longrightarrow> f x \<le> u x) \<Longrightarrow> measure_pmf.expectation M f \<le> measure_pmf.expectation M u"
apply(rule integral_mono_AE)
by (auto simp add: AE_measure_pmf_iff)
lemma expectation_const: "measure_pmf.expectation M (\<lambda>_. c::real) = c"
by simp
lemma E_cong:
fixes f::"'a \<Rightarrow> real"
shows "(\<forall>x\<in> set_pmf S. (f x) = (u x)) \<Longrightarrow> E (map_pmf f S) = E (map_pmf u S)"
unfolding E_def integral_map_pmf apply(rule integral_cong_AE)
apply(simp add: integrable_measure_pmf_finite)+
by (simp add: AE_measure_pmf_iff)
lemma expectation_cong: "(\<And>m. m\<in>set_pmf M \<Longrightarrow> f m = g m) \<Longrightarrow> measure_pmf.expectation M f = measure_pmf.expectation M g"
by (rule integral_cong_AE, simp_all add: AE_measure_pmf_iff)
lemma expectation_Sup_le:
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> real"
assumes Hnn: "H\<noteq>{}"
and 2: "\<And>x. x \<in> H \<Longrightarrow> integrable (measure_pmf D) (f x)"
and 3: "\<And>x. x \<in> H \<Longrightarrow> integrable (measure_pmf D) (\<lambda>S'. \<Squnion>h\<in>H. f h S')" (* could be deduced from 2 and a stronger 4 *)
and 4: "\<And>d. d \<in> set_pmf D \<Longrightarrow> bdd_above ((\<lambda>h. f h d) ` H)"
shows "(\<Squnion>h\<in>H. measure_pmf.expectation D (f h))
\<le> measure_pmf.expectation D (\<lambda>S'. \<Squnion>h\<in>H. f h S')"
proof -
show ?thesis apply(rule cSUP_least)
subgoal using Hnn by auto
proof -
fix x
assume "x\<in>H"
then show "measure_pmf.expectation D (f x) \<le> measure_pmf.expectation D (\<lambda>S'. \<Squnion>h\<in>H. f h S')"
apply(intro expectation_mono)
subgoal using 2 by simp
subgoal using 3 by simp
subgoal for d apply(rule cSUP_upper)
apply simp using 4 by simp
done
qed
qed
lemma nn_integral_Sup_le:
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> real"
shows "(\<Squnion>h\<in>H. nn_integral (measure_pmf D) (f h))
\<le> nn_integral (measure_pmf D) (\<lambda>S'. \<Squnion>h\<in>H. ennreal (f h S'))"
proof -
show ?thesis apply(rule SUP_least)
proof -
fix x
assume "x\<in>H"
then show "nn_integral D (f x) \<le> nn_integral D (\<lambda>S'. \<Squnion>h\<in>H. ennreal (f h S'))"
apply(intro nn_integral_mono_AE) apply(rule AE_pmfI)
subgoal for d
apply(rule SUP_upper)
by simp
done
qed
qed
thm pair_sigma_finite.integrable_fst
(* idea to compress integrability of two expectations into one:
pair_sigma_finite.integrable_fst *)
(* idea, there is the tactic apply(measurable),
what does it do? *)
thm pair_sigma_finite.Fubini_integrable
lemma "measure_pmf (pair_pmf M M2)
= pair_measure (measure_pmf M) (measure_pmf M2)"
unfolding pair_measure_def
unfolding pair_pmf_def
sorry
lemma (in product_sigma_finite) product_nn_integral_insert_rev:
assumes I[simp]: "finite I" "i \<notin> I"
and [measurable]: "f \<in> borel_measurable (Pi\<^sub>M (insert i I) M)"
shows "integral\<^sup>N (Pi\<^sub>M (insert i I) M) f = (\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f (x(i := y)) \<partial>(Pi\<^sub>M I M)) \<partial>(M i))"
apply (subst product_nn_integral_insert[OF assms])
apply (rule pair_sigma_finite.Fubini')
apply intro_locales []
apply (rule sigma_finite[OF I(1)])
apply measurable
done
lemma nn_integral_linear':
(* assumes "(\<lambda>p. f (snd p) (fst p)) \<in> borel_measurable (measure_pmf M2 \<Otimes>\<^sub>M measure_pmf M)" *)
shows
"nn_integral (measure_pmf M) (\<lambda>S. nn_integral (measure_pmf M2) (\<lambda>S'. (f S S')))
= nn_integral (measure_pmf M2) (\<lambda>S2. nn_integral (measure_pmf M) (\<lambda>S. (f S S2)))"
proof -
(* fubini *)
thm pair_sigma_finite.Fubini_integral
find_theorems name: Fubini
thm lborel_pair.Fubini lborel_pair.Fubini'
thm pair_sigma_finite.Fubini'
have *: "\<And>M M'. measure_pmf (pair_pmf M M') = pair_measure (measure_pmf M) (measure_pmf M')"
sorry
show ?thesis
apply(rule pair_sigma_finite.Fubini')
subgoal
by (simp add: measure_pmf.sigma_finite_measure_axioms pair_sigma_finite_def) (* apply intro_locales [] *)
subgoal
apply(rule borel_measurableI)
unfolding *[symmetric]
by simp
(*
apply(simp add: split_def) by fact (*
apply(measurable)
apply(subst pair_measure_countable) apply auto
unfolding borel_def unfolding measurable_def apply auto
sorry *) *)
done
qed
term prob_space
lemma expectation_linear':
fixes
f :: "_ \<Rightarrow> _ \<Rightarrow> real"
shows
"measure_pmf.expectation M (\<lambda>S. measure_pmf.expectation M2 (f S))
= measure_pmf.expectation M2 (\<lambda>S2. measure_pmf.expectation M (\<lambda>S. f S S2))"
proof -
have "integrable (measure_pmf M2 \<Otimes>\<^sub>M measure_pmf M) (\<lambda>(x, S). f S x)"
apply(rule pair_sigma_finite.Fubini_integrable)
subgoal
by (simp add: measure_pmf.sigma_finite_measure_axioms pair_sigma_finite_def)
subgoal sorry
subgoal apply(rule measure_pmf.integrable_const_bound)
sorry
sorry
thm pair_sigma_finite.Fubini_integral
term "integral\<^sup>L M"
show ?thesis apply(subst pair_sigma_finite.Fubini_integral)
subgoal
by (simp add: measure_pmf.sigma_finite_measure_axioms pair_sigma_finite_def)
subgoal by fact
subgoal apply simp done
done
qed
lemma expectation_linear:
"measure_pmf.expectation M (\<lambda>S. measure_pmf.expectation M2 (f S))
= measure_pmf.expectation M2 (\<lambda>S2. measure_pmf.expectation M (\<lambda>S. f S S2))"
sorry
section "help by auto3"
(* by auto3 aka Manuel Eberl: *)
lemma convex_on_exp:
fixes l :: real
assumes "l > 0"
shows "convex_on UNIV (\<lambda>x. exp(l*x))"
using assms
by (intro convex_on_realI[where f' = "\<lambda>x. l * exp (l * x)"]) (auto
intro!: derivative_eq_intros)
lemma mult_const_minus_self_real_le:
fixes x :: real
shows "x * (c - x) \<le> c\<^sup>2 / 4"
proof -
have "x * (c - x) = -(x - c / 2)\<^sup>2 + c\<^sup>2 / 4"
by (simp add: field_simps power2_eq_square)
also have "\<dots> \<le> 0 + c\<^sup>2 / 4"
by (intro add_mono) auto
finally show ?thesis by simp
qed
lemma outsourced:
fixes a b l :: real
assumes "l > 0" and ab: "a < 0" "b > 0"
defines "p \<equiv> -a / (b - a)"
defines "h \<equiv> l * (b - a)"
defines "L \<equiv> (\<lambda>h. -h * p + ln (1 + p * (exp h - 1)))"
shows "L h \<le> h\<^sup>2 / 8"
proof -
define L' where "L' = (\<lambda>h. -p + p * exp h / (1 + p * (exp h - 1)))"
define L'' where "L'' = (\<lambda>h. -(p ^ 2) * exp h * exp h / (1 + p * (exp
h - 1)) ^ 2 +
p * exp h / (1 + p * (exp h - 1)))"
define Ls where "Ls = (\<lambda>n. [L, L', L''] ! n)"
from ab have "p > 0"
by (auto simp: p_def field_simps)
from ab and \<open>l > 0\<close> have "h > 0"
by (auto simp: h_def)
have [simp]: "L 0 = 0" "L' 0 = 0"
by (auto simp: L_def L'_def)
have L': "(L has_real_derivative L' x) (at x)" if "x \<in> {0..h}" for x
proof -
have "1 + p * (exp x - 1) > 0"
using \<open>p > 0\<close> that by (intro add_pos_nonneg mult_nonneg_nonneg) auto
thus ?thesis
unfolding L_def L'_def by (auto intro!: derivative_eq_intros)
qed
have L'': "(L' has_real_derivative L'' x) (at x)" if "x \<in> {0..h}" for x
proof -
have *: "1 + p * (exp x - 1) > 0"
using \<open>p > 0\<close> that by (intro add_pos_nonneg mult_nonneg_nonneg) auto
show ?thesis
unfolding L'_def L''_def
by (insert *, (rule derivative_eq_intros refl | simp)+) (auto
simp: divide_simps; algebra)
qed
have diff: "\<forall>m t. m < 2 \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> (Ls m has_real_derivative Ls
(Suc m) t) (at t)"
using L' L'' by (auto simp: Ls_def nth_Cons split: nat.splits)
from Taylor[of 2 Ls L 0 h 0 h, OF _ _ diff]
obtain t where t: "t \<in> {0<..<h}" "L h = L'' t * h ^ 2 / 2"
using \<open>h > 0\<close> ab by (auto simp: Ls_def lessThan_nat_numeral)
define u where "u = p * exp t / (1 + p * (exp t - 1))"
have "L'' t = u * (1 - u)"
by (simp add: L''_def u_def divide_simps; algebra)
also have "\<dots> \<le> 1 / 4"
using mult_const_minus_self_real_le[of u 1] by simp
finally have "L'' t \<le> 1 / 4" .
note t(2)
also have "L'' t * h\<^sup>2 / 2 \<le> (1 / 4) * h\<^sup>2 / 2"
using \<open>L'' t \<le> 1 / 4\<close> by (intro mult_right_mono divide_right_mono) auto
finally show "L h \<le> h\<^sup>2 / 8" by simp
qed
lemma
assumes
range: "measure_pmf.prob D {x. a \<le> x \<and> x \<le> b} = 1"
shows setofDi: "set_pmf D \<subseteq> {a..b}"
proof -
have "measure_pmf.prob D (space (measure_pmf D) - {x. a \<le> x \<and> x \<le> b}) = 0"
using range by (subst measure_pmf.prob_compl) (auto)
also have "(space (measure_pmf D) - {x. a \<le> x \<and> x \<le> b}) = -{x. a \<le> x \<and> x \<le> b}"
by auto
finally have "set_pmf D \<inter> -{x. a \<le> x \<and> x \<le> b} = {}"
by (subst (asm) measure_pmf_zero_iff)
thus "set_pmf D \<subseteq> {a..b}"
by auto
qed
lemma hoeffdings_lemma:
fixes a b :: real
assumes range: "\<And>i. measure_pmf.prob D {x. a \<le> x \<and> x \<le> b} = 1"
and E0: "measure_pmf.expectation D id = 0" and lgt0: "l>0"
and aleb: "a\<le>b" and al0: "a<0"and bg0: "0<b" (* those do actually follow from E0 I think *)
shows "measure_pmf.expectation D (\<lambda>x. exp (l*x)) \<le> exp ( l^2 *(b-a)^2 / 8)"
proof -
let ?f = "(\<lambda>x. exp (l * x))"
from setofDi[OF range] have xbetweenab: "\<And>x. x\<in>set_pmf D \<Longrightarrow> x \<in> {x. a \<le> x \<and> x \<le> b}"
unfolding atLeastAtMost_def atLeast_def atMost_def by blast
from al0 bg0 have ab: "a<b" by auto
(* for integrable side conditions *)
thm measure_pmf.integrable_const_bound
thm integrable_measure_pmf_finite
then have anb: "a\<noteq>b" by auto
have F: "\<And>x :: real. (1 - (b - x) / (b - a)) = (x-a)/(b-a)"
proof -
fix x
have "1 = (b-a) / (b-a)" using anb by auto
have "(1 - (b - x) / (b - a)) = ((b-a) / (b-a) - (b - x) / (b - a))"
using anb by auto
also have "\<dots> = ( (b-a) - (b - x) ) / (b - a)" using anb by argo
also have "\<dots> = (x-a)/(b-a)" by auto
finally show "(1 - (b - x) / (b - a)) = (x-a)/(b-a)" .
qed
have cvon: "convex_on UNIV (\<lambda>x. exp(l*x))" using convex_on_exp assms(3) by auto
have *: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> ?f x \<le> (b - x) / (b - a) * exp (l * a) + (x-a)/(b-a) * exp (l * b)"
proof -
fix x :: real
let ?\<alpha> = "(b-x) / (b-a)"
have g: "1 - ?\<alpha> = (x-a) / (b-a)" using F .
assume "a \<le> x" "x \<le> b"
then have C: "0 \<le> ?\<alpha>" "?\<alpha> \<le> 1" using ab by auto
from convex_onD[OF cvon, of _ b a, simplified ] have A:
"\<And>t. 0 \<le> t \<Longrightarrow> t \<le> 1 \<Longrightarrow> exp (l * ((1 - t) * b + t * a)) \<le> (1 - t) * exp (l * b) + t * exp (l * a)" .
have B: "(1 - ?\<alpha>) * b + ?\<alpha> * a = x"
proof -
have "(1 - ?\<alpha>) * b + ?\<alpha> * a = ((x-a) / (b-a)) * b + ((b-x) / (b-a)) * a"
unfolding g ..
also have "\<dots> = (x*(b-a)) / (b-a)" by algebra
also have "\<dots> = x" using ab by simp
finally show ?thesis .
qed
from A[of ?\<alpha>, simplified B, OF C]
show "exp (l * x) \<le> (b - x) / (b - a) * exp (l * a) + (x-a)/(b-a) * exp (l * b)"
unfolding g by simp
qed
have i: "\<And>y Z. 0 \<le> Z \<Longrightarrow> a\<le>y \<Longrightarrow> y\<le>b \<Longrightarrow> a<b \<Longrightarrow> b>0 \<Longrightarrow> (b - y) * Z / (b - a) \<le> Z"
proof -
fix y Z :: real
assume A: "0 \<le> Z" "a\<le>y" "y\<le>b" "a<b" "b>0"
have "(b - y) * Z / (b - a) = ((b - y) / (b - a)) * Z" by auto
also have "\<dots> \<le> Z" apply(rule mult_left_le_one_le)
using A by auto
finally show "(b - y) * Z / (b - a) \<le> Z" .
qed
have ii: "\<And>y Z. 0 \<le> Z \<Longrightarrow> a\<le>y \<Longrightarrow> y\<le>b \<Longrightarrow> a<b \<Longrightarrow> b>0 \<Longrightarrow> (y - a) * Z / (b - a) \<le> Z"
proof -
fix y Z :: real
assume A: "0 \<le> Z" "a\<le>y" "y\<le>b" "a<b" "b>0"
have "(y - a) * Z / (b - a) = ((y - a) / (b - a)) * Z" by auto
also have "\<dots> \<le> Z" apply(rule mult_left_le_one_le)
using A by auto
finally show "(y - a) * Z / (b - a) \<le> Z" .
qed
have "measure_pmf.expectation D ?f \<le> measure_pmf.expectation D (\<lambda>x. (b - x) / (b - a) * exp (l * a) + (x-a)/(b-a) * exp (l * b))"
apply(rule expectation_mono)
subgoal
apply(rule measure_pmf.integrable_const_bound[where B="exp (l * b)"]) using lgt0
by (auto intro!: AE_pmfI dest: xbetweenab)
subgoal
apply(rule measure_pmf.integrable_const_bound[where B="exp (l * a) + exp (l * b)"])
using lgt0
apply (auto intro!: AE_pmfI dest!: xbetweenab)
apply(rule add_mono)
subgoal apply(rule i) using ab bg0 by auto
subgoal apply(rule ii) using ab bg0 by auto
done
apply(rule *)
using xbetweenab by auto
also
have "\<dots> = (b - measure_pmf.expectation D id) / (b - a) * exp (l * a) + (measure_pmf.expectation D id-a)/(b-a) * exp (l * b)"
(is "?L = ?R")
proof -
have "?L = measure_pmf.expectation D (\<lambda>x. (b + (x * -1)) / (b - a) * exp (l * a) + (x + (- a)) / (b - a) * exp (l * b))" by simp
also have "\<dots> = measure_pmf.expectation D (\<lambda>x. (b + x * -1) / (b - a) * exp (l * a)) + measure_pmf.expectation D (\<lambda>x. (x + - a) / (b - a) * exp (l * b))"
apply(rule Bochner_Integration.integral_add)
subgoal using bg0 ab
apply (auto intro!: measure_pmf.integrable_const_bound[where B="exp (l * a) "]
AE_pmfI dest!: xbetweenab) apply(rule i) by auto
subgoal using bg0 ab
apply (auto intro!: measure_pmf.integrable_const_bound[where B="exp (l * b) "]
AE_pmfI dest!: xbetweenab) apply(rule ii) by auto
done
also have "measure_pmf.expectation D (\<lambda>x. (b + x * -1) / (b - a) * exp (l * a)) = measure_pmf.expectation D (\<lambda>x. (b + x * -1) / (b - a)) * exp (l * a)"
by (rule integral_mult_left_zero)
also have "measure_pmf.expectation D (\<lambda>x. (b + x * -1) / (b - a)) = measure_pmf.expectation D (\<lambda>x. (b + x * -1) ) / (b - a) "
by(rule integral_divide_zero)
also have "measure_pmf.expectation D (\<lambda>x. (b + x * -1) ) = measure_pmf.expectation D (\<lambda>_. b) + measure_pmf.expectation D (\<lambda>x. x * -1 )"
apply(rule Bochner_Integration.integral_add)
subgoal by auto
subgoal
by(auto intro!: measure_pmf.integrable_const_bound[where B="max (abs a) (abs b)"]
AE_pmfI dest!: xbetweenab)
done
also have "measure_pmf.expectation D (\<lambda>_. b) = b"
using expectation_const by simp
also have "measure_pmf.expectation D (\<lambda>x. x * -1) = - measure_pmf.expectation D id"
apply(subst integral_mult_left_zero) unfolding id_def by simp
also have "measure_pmf.expectation D (\<lambda>x. (x + - a) / (b - a) * exp (l * b)) = measure_pmf.expectation D (\<lambda>x. (x + - a) / (b - a) ) * exp (l * b)"
by (rule integral_mult_left_zero)
also have "measure_pmf.expectation D (\<lambda>x. (x + - a) / (b - a) ) = measure_pmf.expectation D (\<lambda>x. (x + - a) ) / (b - a) "
by(rule integral_divide_zero)
also have "measure_pmf.expectation D (\<lambda>x. (x + - a) ) = measure_pmf.expectation D (\<lambda>x. x) + measure_pmf.expectation D (\<lambda>_. -a )"
apply(rule Bochner_Integration.integral_add)
subgoal
by(auto intro!: measure_pmf.integrable_const_bound[where B="max (abs a) (abs b)"]
AE_pmfI dest!: xbetweenab)
subgoal by auto
done
also have "measure_pmf.expectation D (\<lambda>_. -a) = -a"
using expectation_const by simp
also have "measure_pmf.expectation D (\<lambda>x. x ) = measure_pmf.expectation D id"
unfolding id_def by simp
finally
show "?L = ?R" by argo
qed
(*
thm integral_add integral_mult_left_zero integral_divide_zero expectation_const
thm integral_bij_count_space
thm integral_bounded_linear
apply(subst integral_bounded_linear[symmetric, where M=D and T="?f" and f=id])
by simp *)
also have "\<dots> = b / (b - a) * exp (l * a) - a/(b-a) * exp (l * b)"
by (simp add: E0)
finally have 1: "measure_pmf.expectation D ?f \<le> (b / (b - a)) * ?f a - (a/(b-a)) * ?f b" .
let ?h = "l*(b-a)"
let ?p = "-a / (b-a)"
let ?L = "\<lambda>h. -h * ?p + ln (1- ?p + ?p * exp h)"
have 2: "(b / (b - a)) * ?f a - (a/(b-a)) * ?f b = exp (?L ?h)"
proof -
have nn: "1 - ?p + ?p * exp ?h > 0"
proof -
have i: "?p \<ge> 0" using ab al0
by (smt divide_nonneg_pos)
have ii: "exp ?h > 1" apply(subst one_less_exp_iff) using assms(3) ab by auto
then have "(exp ?h -1) \<ge>0" by simp
have "(exp ?h -1) * ?p \<ge> 0" apply(intro mult_nonneg_nonneg) by fact+
moreover have "1 - ?p + ?p * exp ?h = 1 + (exp ?h -1) * ?p" by algebra
ultimately show ?thesis by argo
qed
have "exp (?L ?h) = exp (- ?h * ?p) * exp ( ln (1- ?p + ?p * exp ?h))"
using exp_add by fast
also have "exp ( ln (1- ?p + ?p * exp ?h)) = 1- ?p + ?p * exp ?h" using nn by simp
finally have "exp (?L ?h) = exp (- ?h * ?p) * (1- ?p + ?p * exp ?h)" .
also have "\<dots> = (exp (- ?h * ?p) - ?p * exp (- ?h * ?p)) + ?p * exp ?h * exp (- ?h * ?p)" by algebra
also have "(exp (- ?h * ?p) - ?p * exp (- ?h * ?p)) = (b / (b - a)) * ?f a"
proof -
have expand: "exp (l * a) = ((b-a) * exp (l * a)) / (b-a)" using ab by auto
have "(exp (- ?h * ?p) - ?p * exp (- ?h * ?p)) = exp (l * a) + a * exp (l * a) / (b - a)"
using ab by simp
also have "\<dots> = ((b-a) * exp (l * a) + a * exp (l * a)) / (b - a)"
apply(subst expand) by algebra
also have "((b-a) * exp (l * a) + a * exp (l * a)) = b * exp (l * a)" by algebra
finally show ?thesis by simp
qed
also have "?p * exp ?h * exp (- ?h * ?p) = - (a/(b-a)) * ?f b"
proof -
have collapse: "exp (l * (b - a)) * exp (l * a) = exp (l * (b-a) + l *a)" using mult_exp_exp by blast
have "?p * exp ?h * exp (- ?h * ?p) = - (a * (exp (l * (b - a)) * exp (l * a)) / (b - a))"
using ab by simp
also have "\<dots> = - (a * exp (l * b) / (b - a))"
apply(subst collapse) by argo
finally show ?thesis by simp
qed
finally
show ?thesis by simp
qed
have G: "1 + a / (b - a) - a * exp (l * (b - a)) / (b - a)
= 1 - a * (exp (l * (b - a)) - 1) / (b - a) "
using al0 bg0 apply (auto simp: algebra_simps)
unfolding add_divide_distrib[symmetric] by simp
have 3: "?L ?h \<le> ?h^2 / 8"
apply(rule order.trans[OF _ outsourced])
using al0 bg0 lgt0 apply auto unfolding G by simp
have 4: "?h^2 = l^2 *(b-a)^2" by algebra
note 1
also have "(b / (b - a)) * ?f a - (a/(b-a)) * ?f b = exp (?L ?h)" using 2 by simp
also have "\<dots> \<le> exp (?h^2 / 8)" using 3 ..
also have "\<dots> \<le> exp ( l^2 *(b-a)^2 / 8)" unfolding 4 ..
finally show ?thesis .
qed
lemma set_Pi_pmf': "finite A \<Longrightarrow> f \<in> set_pmf (Pi_pmf A dflt D) \<Longrightarrow> (\<forall>i\<in>A. f i \<in> set_pmf (D i))"
apply (auto simp: set_pmf_eq pmf_Pi)
by (meson prod_zero)
lemma hoeffding_ineq:
assumes
"\<And>i::nat. i < m \<Longrightarrow> measure_pmf.expectation (D i) id = \<mu> i"
and range: "\<And>i. i<m \<Longrightarrow> measure_pmf.prob (D i) {x. a \<le> x \<and> x \<le> b} = 1" and "(\<epsilon>::real)>0"
and PA: "\<And>i. i < m \<Longrightarrow> a - \<mu> i < 0" and PB: "\<And>i. i < m \<Longrightarrow> 0 < b - \<mu> i" and ab2: "a<b" and mgt0: "m>0"
shows "measure_pmf.prob (Pi_pmf {0..<m} dflt D) {\<sigma>. abs(sum (\<lambda>i. (\<sigma> i) - \<mu> i) {0..<m} / m) > \<epsilon> }
\<le> 2 * exp (- 2 * m * \<epsilon>^2 / (b-a)^2 )"
proof -
from setofDi[OF range] have xbetweenab: "\<And>x i. i<m \<Longrightarrow> x\<in>set_pmf (D i) \<Longrightarrow> x \<in> {x. a \<le> x \<and> x \<le> b}"
by fastforce
{
fix D :: "nat \<Rightarrow> real pmf" and a b :: "nat \<Rightarrow> real" and d :: real
assume ONE: "\<And>i. i<m \<Longrightarrow> measure_pmf.prob (D i) {x. a i \<le> x \<and> x \<le> b i} = 1"
assume TWO: "\<And>x. x<m \<Longrightarrow> measure_pmf.expectation (D x) (\<lambda>x. id (x / real m)) = 0"
assume defd: "\<And>i. i<m \<Longrightarrow> b i - a i = d"
assume dgt0: "d>0"
assume ab: "\<And>i. i<m \<Longrightarrow> a i \<le> b i"
assume ab2: "\<And>i. i<m \<Longrightarrow> a i < b i"
assume ai: "\<And>i. i<m \<Longrightarrow> a i < 0 "
assume bi: "\<And>i. i<m \<Longrightarrow> 0 < b i"
thm markov_inequality
{ fix M and \<epsilon>::real and l :: real
assume "integrable (measure_pmf M) (\<lambda>x. exp (l * x))"
assume "l>0"
then
have "measure_pmf.prob M {x. x > \<epsilon>} = measure_pmf.prob M {x. exp (l * x) > exp (l * \<epsilon>)}"
by simp
also have "\<dots> \<le> measure_pmf.expectation M (\<lambda>x. exp (l * x)) / exp (l * \<epsilon>)"
apply(rule markov_inequality)
subgoal by fact
subgoal by simp
subgoal by simp
done
finally have "measure_pmf.prob M {x. x > \<epsilon>} \<le> measure_pmf.expectation M (\<lambda>x. exp (l * x)) / exp (l * \<epsilon>)" .
} note first = this
{
fix p and Q and l :: real
have "measure_pmf.expectation (Pi_pmf {0..<m} dflt p) (\<lambda>y. exp (l * (\<Sum>x\<in> {0..<m}. (Q x) (y x) / m) ))
= measure_pmf.expectation (Pi_pmf {0..<m} dflt p) (\<lambda>y. ( \<Prod>x\<in> {0..<m}. exp (l * (Q x) (y x) / m)))"
by (auto simp: sum_distrib_left exp_sum)
also have "\<dots> = (\<Prod>x\<in> {0..<m}. measure_pmf.expectation (p x) (\<lambda>y. ( exp (l * (Q x) y / m))))"
by (auto intro: expectation_Pi_pmf_prod)
finally have "measure_pmf.expectation (Pi_pmf {0..<m} dflt p) (\<lambda>y. exp (l * (\<Sum>x = 0..<m. Q x (y x) / real m))) =
(\<Prod>x = 0..<m. measure_pmf.expectation (p x) (\<lambda>y. exp (l * Q x y / real m))) ".
} note second = this
note second' = second[of _ _ "(\<lambda>x y. y)"]
note second'_sym = second[of _ _ "(\<lambda>x y. -y)"]
{
fix x :: nat and l :: real
assume xm: "x<m"
assume lgt0: "l>0"
from mgt0 have p: "\<And>x y. (x / real m \<le> y / real m) \<longleftrightarrow> x \<le> y"
by (smt divide_strict_right_mono of_nat_0_less_iff)
have ahhhh: "\<And>a b. {y. a / real m \<ge> (y / real m) \<and> (y / real m) \<ge> b / real m} = {x. a \<ge> x \<and> x \<ge> b}"
unfolding p
by simp
have "measure_pmf.expectation (D x) (\<lambda>y. exp (l * (-y / real m)))
= measure_pmf.expectation (map_pmf (\<lambda>y. (-y / real m)) (D x) ) (\<lambda>y. exp (l * y))"
by simp
also have "\<dots> \<le> exp (l\<^sup>2 * (b x / real m - a x / real m)\<^sup>2 / 8)"
apply(rule order.trans)
apply(rule hoeffdings_lemma[where a="-b x/m" and b="-a x/m"])
subgoal apply(subst measure_map_pmf)
apply simp unfolding ahhhh apply(subst conj_commute)
using ONE[OF xm] .
subgoal unfolding integral_map_pmf using TWO[OF xm] by simp
subgoal using lgt0 .
subgoal using mgt0 ab[OF xm] divide_right_mono by force
subgoal using bi[OF xm] mgt0 by auto
subgoal apply(rule divide_pos_pos) using ai[OF xm] mgt0 by auto
apply simp
done
also have "\<dots> = exp (l\<^sup>2 * (b x - a x)\<^sup>2 / (8 * (real m)^2))" apply simp
unfolding power2_eq_square using ab mgt0 apply (auto simp: algebra_simps)
unfolding add_divide_distrib[symmetric] by simp
also have "\<dots> = exp (l\<^sup>2 * d\<^sup>2 / (8 * (real m)^2))"
using defd[OF xm] by simp
finally have "measure_pmf.expectation (D x) (\<lambda>y. exp (l * (-y / real m))) \<le> exp (l\<^sup>2 * d\<^sup>2 / (8 * (real m)\<^sup>2)) " .
} note third_sym = this
{
fix x :: nat and l :: real
assume xm: "x<m"
assume lgt0: "l>0"
from mgt0 have p: "\<And>x y. (x / real m \<le> y / real m) \<longleftrightarrow> x \<le> y"
by (smt divide_strict_right_mono of_nat_0_less_iff)
have ahhhh: "\<And>a b. {y. a / real m \<le> y / real m \<and> y / real m \<le> b / real m} = {x. a \<le> x \<and> x \<le> b}"
unfolding p
by simp
have "measure_pmf.expectation (D x) (\<lambda>y. exp (l * (y / real m)))
= measure_pmf.expectation (map_pmf (\<lambda>y. (y / real m)) (D x) ) (\<lambda>y. exp (l * y))"
by simp
also have "\<dots> \<le> exp (l\<^sup>2 * (b x / real m - a x / real m)\<^sup>2 / 8)"
apply(rule hoeffdings_lemma[where a="a x/m" and b="b x/m"])
subgoal apply(subst measure_map_pmf)
apply simp unfolding ahhhh
using ONE[OF xm] .
subgoal unfolding integral_map_pmf using TWO[OF xm] .
subgoal using lgt0 .
subgoal using mgt0 ab[OF xm] divide_right_mono by force
subgoal apply(rule divide_neg_pos) using ai[OF xm] mgt0 by simp_all
subgoal using bi[OF xm] mgt0 by auto
done
also have "\<dots> = exp (l\<^sup>2 * (b x - a x)\<^sup>2 / (8 * (real m)^2))" apply simp
unfolding power2_eq_square using ab mgt0 apply (auto simp: algebra_simps)
unfolding add_divide_distrib[symmetric] by simp
also have "\<dots> = exp (l\<^sup>2 * d\<^sup>2 / (8 * (real m)^2))"
using defd[OF xm] by simp
finally have "measure_pmf.expectation (D x) (\<lambda>y. exp (l * (y / real m))) \<le> exp (l\<^sup>2 * d\<^sup>2 / (8 * (real m)\<^sup>2)) " .
} note third = this
note first second
{
fix l::real
assume lgt0: "l>0"
have "(\<Prod>x = 0..<m. measure_pmf.expectation (D x) (\<lambda>y. exp (l * y / real m)))
= (\<Prod>x = 0..<m. measure_pmf.expectation (D x) (\<lambda>y. exp (l * (y / real m))))" by simp
also have "\<dots> \<le> (\<Prod>x = 0..<m. exp (l\<^sup>2 * d\<^sup>2 / (8 * (real m)\<^sup>2)))"
apply(rule prod_mono)
apply rule
subgoal for x apply(rule Bochner_Integration.integral_nonneg) by simp
subgoal apply(rule third) using lgt0 by simp_all
done
finally have "(\<Prod>x = 0..<m. measure_pmf.expectation (D x) (\<lambda>y. exp (l * y / real m)))
\<le> (\<Prod>x = 0..<m. exp (l\<^sup>2 * d\<^sup>2 / (8 * (real m)\<^sup>2))) " .
} note third' = this
{
fix l::real
assume lgt0: "l>0"