-
Notifications
You must be signed in to change notification settings - Fork 0
/
Conditional_Expectation_Banach.thy
1048 lines (916 loc) · 78.8 KB
/
Conditional_Expectation_Banach.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
(* Author: Ata Keskin, TU München
*)
theory Conditional_Expectation_Banach
imports "HOL-Probability.Conditional_Expectation" "HOL-Probability.Independent_Family" Bochner_Integration_Supplement
begin
section \<open>Conditional Expectation in Banach Spaces\<close>
text \<open>While constructing the conditional expectation operator, we have come up with the following approach, which is based on the construction in \cite{Hytoenen_2016}.
Both our approach, and the one in \cite{Hytoenen_2016} are based on showing that the conditional expectation is a contraction on some dense subspace of the space of functions \<open>L\<^sup>1(E)\<close>.
In our approach, we start by constructing the conditional expectation explicitly for simple functions.
Then we show that the conditional expectation is a contraction on simple functions, i.e. \<open>\<parallel>E(s|F)(x)\<parallel> \<le> E(\<parallel>s(x)\<parallel>|F)\<close> for \<open>\<mu>\<close>-almost all \<open>x \<in> \<Omega>\<close> with \<open>s : \<Omega> \<rightarrow> E\<close> simple and integrable.
Using this, we can show that the conditional expectation of a convergent sequence of simple functions is again convergent.
Finally, we show that this limit exhibits the properties of a conditional expectation.
This approach has the benefit of being straightforward and easy to implement, since we could make use of the existing formalization for real-valued functions.
To use the construction in \cite{Hytoenen_2016} we need more tools from functional analysis, which Isabelle/HOL currently does not have.\<close>
text \<open>Before we can talk about 'the' conditional expectation, we must define what it means for a function to have a conditional expectation.\<close>
definition has_cond_exp :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{real_normed_vector, second_countable_topology}) \<Rightarrow> bool" where
"has_cond_exp M F f g = ((\<forall>A \<in> sets F. (\<integral> x \<in> A. f x \<partial>M) = (\<integral> x \<in> A. g x \<partial>M))
\<and> integrable M f
\<and> integrable M g
\<and> g \<in> borel_measurable F)"
text \<open>This predicate precisely characterizes what it means for a function \<^term>\<open>f\<close> to have a conditional expectation \<^term>\<open>g\<close>,
with respect to the measure \<^term>\<open>M\<close> and the sub-\<open>\<sigma>\<close>-algebra \<^term>\<open>F\<close>.\<close>
lemma has_cond_expI':
assumes "\<And>A. A \<in> sets F \<Longrightarrow> (\<integral> x \<in> A. f x \<partial>M) = (\<integral> x \<in> A. g x \<partial>M)"
"integrable M f"
"integrable M g"
"g \<in> borel_measurable F"
shows "has_cond_exp M F f g"
using assms unfolding has_cond_exp_def by simp
lemma has_cond_expD:
assumes "has_cond_exp M F f g"
shows "\<And>A. A \<in> sets F \<Longrightarrow> (\<integral> x \<in> A. f x \<partial>M) = (\<integral> x \<in> A. g x \<partial>M)"
"integrable M f"
"integrable M g"
"g \<in> borel_measurable F"
using assms unfolding has_cond_exp_def by simp+
text \<open>Now we can use Hilbert’s \<open>\<some>\<close>-operator to define the conditional expectation, if it exists.\<close>
definition cond_exp :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{banach, second_countable_topology})" where
"cond_exp M F f = (if \<exists>g. has_cond_exp M F f g then (SOME g. has_cond_exp M F f g) else (\<lambda>_. 0))"
lemma borel_measurable_cond_exp[measurable]: "cond_exp M F f \<in> borel_measurable F"
by (metis cond_exp_def someI has_cond_exp_def borel_measurable_const)
lemma integrable_cond_exp[intro]: "integrable M (cond_exp M F f)"
by (metis cond_exp_def has_cond_expD(3) integrable_zero someI)
lemma set_integrable_cond_exp[intro]:
assumes "A \<in> sets M"
shows "set_integrable M A (cond_exp M F f)" using integrable_mult_indicator[OF assms integrable_cond_exp, of F f] by (auto simp add: set_integrable_def intro!: integrable_mult_indicator[OF assms integrable_cond_exp])
lemma has_cond_exp_self:
assumes "integrable M f"
shows "has_cond_exp M (vimage_algebra (space M) f borel) f f"
using assms by (auto intro!: has_cond_expI' measurable_vimage_algebra1)
lemma has_cond_exp_sets_cong:
assumes "sets F = sets G"
shows "has_cond_exp M F = has_cond_exp M G"
using assms unfolding has_cond_exp_def by force
lemma cond_exp_sets_cong:
assumes "sets F = sets G"
shows "AE x in M. cond_exp M F f x = cond_exp M G f x"
by (intro AE_I2, simp add: cond_exp_def has_cond_exp_sets_cong[OF assms, of M])
context sigma_finite_subalgebra
begin
lemma borel_measurable_cond_exp'[measurable]: "cond_exp M F f \<in> borel_measurable M"
by (metis cond_exp_def someI has_cond_exp_def borel_measurable_const subalg measurable_from_subalg)
lemma cond_exp_null:
assumes "\<nexists>g. has_cond_exp M F f g"
shows "cond_exp M F f = (\<lambda>_. 0)"
unfolding cond_exp_def using assms by argo
text \<open>We state the tower property of the conditional expectation in terms of the predicate \<^term>\<open>has_cond_exp\<close>.\<close>
lemma has_cond_exp_nested_subalg:
fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, banach}"
assumes "subalgebra G F" "has_cond_exp M F f h" "has_cond_exp M G f h'"
shows "has_cond_exp M F h' h"
by (intro has_cond_expI') (metis assms has_cond_expD in_mono subalgebra_def)+
text \<open>The following lemma shows that the conditional expectation is unique as an element of L1, given that it exists.\<close>
lemma has_cond_exp_charact:
fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, banach}"
assumes "has_cond_exp M F f g"
shows "has_cond_exp M F f (cond_exp M F f)"
"AE x in M. cond_exp M F f x = g x"
proof -
show cond_exp: "has_cond_exp M F f (cond_exp M F f)" using assms someI cond_exp_def by metis
let ?MF = "restr_to_subalg M F"
interpret sigma_finite_measure ?MF by (rule sigma_fin_subalg)
{
fix A assume "A \<in> sets ?MF"
then have [measurable]: "A \<in> sets F" using sets_restr_to_subalg[OF subalg] by simp
have "(\<integral>x \<in> A. g x \<partial>?MF) = (\<integral>x \<in> A. g x \<partial>M)" using assms subalg by (auto simp add: integral_subalgebra2 set_lebesgue_integral_def dest!: has_cond_expD)
also have "... = (\<integral>x \<in> A. cond_exp M F f x \<partial>M)" using assms cond_exp by (simp add: has_cond_exp_def)
also have "... = (\<integral>x \<in> A. cond_exp M F f x \<partial>?MF)" using subalg by (auto simp add: integral_subalgebra2 set_lebesgue_integral_def)
finally have "(\<integral>x \<in> A. g x \<partial>?MF) = (\<integral>x \<in> A. cond_exp M F f x \<partial>?MF)" by simp
}
hence "AE x in ?MF. cond_exp M F f x = g x" using cond_exp assms subalg by (intro density_unique_banach, auto dest: has_cond_expD intro!: integrable_in_subalg)
then show "AE x in M. cond_exp M F f x = g x" using AE_restr_to_subalg[OF subalg] by simp
qed
corollary cond_exp_charact:
fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, banach}"
assumes "\<And>A. A \<in> sets F \<Longrightarrow> (\<integral> x \<in> A. f x \<partial>M) = (\<integral> x \<in> A. g x \<partial>M)"
"integrable M f"
"integrable M g"
"g \<in> borel_measurable F"
shows "AE x in M. cond_exp M F f x = g x"
by (intro has_cond_exp_charact has_cond_expI' assms) auto
text \<open>Identity on F-measurable functions:\<close>
text \<open>If an integrable function \<^term>\<open>f\<close> is already \<^term>\<open>F\<close>-measurable, then \<^term>\<open>cond_exp M F f = f\<close> \<open>\<mu>\<close>-a.e.
This is a corollary of the lemma on the characterization of \<^term>\<open>cond_exp\<close>.\<close>
corollary cond_exp_F_meas[intro, simp]:
fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, banach}"
assumes "integrable M f"
"f \<in> borel_measurable F"
shows "AE x in M. cond_exp M F f x = f x"
by (rule cond_exp_charact, auto intro: assms)
text \<open>Congruence\<close>
lemma has_cond_exp_cong:
assumes "integrable M f" "\<And>x. x \<in> space M \<Longrightarrow> f x = g x" "has_cond_exp M F g h"
shows "has_cond_exp M F f h"
proof (intro has_cond_expI'[OF _ assms(1)])
fix A assume asm: "A \<in> sets F"
hence "set_lebesgue_integral M A f = set_lebesgue_integral M A g" by (intro set_lebesgue_integral_cong) (meson assms(2) subalg in_mono subalgebra_def sets.sets_into_space subalgebra_def subsetD)+
thus "set_lebesgue_integral M A f = set_lebesgue_integral M A h" using asm assms(3) by (simp add: has_cond_exp_def)
qed (auto simp add: has_cond_expD[OF assms(3)])
lemma cond_exp_cong:
fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology,banach}"
assumes "integrable M f" "integrable M g" "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"
shows "AE x in M. cond_exp M F f x = cond_exp M F g x"
proof (cases "\<exists>h. has_cond_exp M F f h")
case True
then obtain h where h: "has_cond_exp M F f h" "has_cond_exp M F g h" using has_cond_exp_cong assms by metis
show ?thesis using h[THEN has_cond_exp_charact(2)] by fastforce
next
case False
moreover have "\<nexists>h. has_cond_exp M F g h" using False has_cond_exp_cong assms by auto
ultimately show ?thesis unfolding cond_exp_def by auto
qed
lemma has_cond_exp_cong_AE:
assumes "integrable M f" "AE x in M. f x = g x" "has_cond_exp M F g h"
shows "has_cond_exp M F f h"
using assms(1,2) subalg subalgebra_def subset_iff
by (intro has_cond_expI', subst set_lebesgue_integral_cong_AE[OF _ assms(1)[THEN borel_measurable_integrable] borel_measurable_integrable(1)[OF has_cond_expD(2)[OF assms(3)]]])
(fast intro: has_cond_expD[OF assms(3)] integrable_cong_AE_imp[OF _ _ AE_symmetric])+
lemma has_cond_exp_cong_AE':
assumes "h \<in> borel_measurable F" "AE x in M. h x = h' x" "has_cond_exp M F f h'"
shows "has_cond_exp M F f h"
using assms(1, 2) subalg subalgebra_def subset_iff
using AE_restr_to_subalg2[OF subalg assms(2)] measurable_from_subalg
by (intro has_cond_expI' , subst set_lebesgue_integral_cong_AE[OF _ measurable_from_subalg(1,1)[OF subalg], OF _ assms(1) has_cond_expD(4)[OF assms(3)]])
(fast intro: has_cond_expD[OF assms(3)] integrable_cong_AE_imp[OF _ _ AE_symmetric])+
lemma cond_exp_cong_AE:
fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology,banach}"
assumes "integrable M f" "integrable M g" "AE x in M. f x = g x"
shows "AE x in M. cond_exp M F f x = cond_exp M F g x"
proof (cases "\<exists>h. has_cond_exp M F f h")
case True
then obtain h where h: "has_cond_exp M F f h" "has_cond_exp M F g h" using has_cond_exp_cong_AE assms by (metis (mono_tags, lifting) eventually_mono)
show ?thesis using h[THEN has_cond_exp_charact(2)] by fastforce
next
case False
moreover have "\<nexists>h. has_cond_exp M F g h" using False has_cond_exp_cong_AE assms by auto
ultimately show ?thesis unfolding cond_exp_def by auto
qed
text \<open>The conditional expectation operator on the reals, \<^term>\<open>real_cond_exp\<close>, satisfies the conditions of the conditional expectation as we have defined it.\<close>
lemma has_cond_exp_real:
fixes f :: "'a \<Rightarrow> real"
assumes "integrable M f"
shows "has_cond_exp M F f (real_cond_exp M F f)"
by (intro has_cond_expI', auto intro!: real_cond_exp_intA assms)
lemma cond_exp_real[intro]:
fixes f :: "'a \<Rightarrow> real"
assumes "integrable M f"
shows "AE x in M. cond_exp M F f x = real_cond_exp M F f x"
using has_cond_exp_charact has_cond_exp_real assms by blast
lemma cond_exp_cmult:
fixes f :: "'a \<Rightarrow> real"
assumes "integrable M f"
shows "AE x in M. cond_exp M F (\<lambda>x. c * f x) x = c * cond_exp M F f x"
using real_cond_exp_cmult[OF assms(1), of c] assms(1)[THEN cond_exp_real] assms(1)[THEN integrable_mult_right, THEN cond_exp_real, of c] by fastforce
subsection \<open>Existence\<close>
text \<open>Showing the existence is a bit involved. Specifically, what we aim to show is that \<^term>\<open>has_cond_exp M F f (cond_exp M F f)\<close> holds for any Bochner-integrable \<^term>\<open>f\<close>.
We will employ the standard machinery of measure theory. First, we will prove existence for indicator functions.
Then we will extend our proof by linearity to simple functions.
Finally we use a limiting argument to show that the conditional expectation exists for all Bochner-integrable functions.\<close>
text \<open>Indicator functions\<close>
lemma has_cond_exp_indicator:
assumes "A \<in> sets M" "emeasure M A < \<infinity>"
shows "has_cond_exp M F (\<lambda>x. indicat_real A x *\<^sub>R y) (\<lambda>x. real_cond_exp M F (indicator A) x *\<^sub>R y)"
proof (intro has_cond_expI', goal_cases)
case (1 B)
have "\<integral>x\<in>B. (indicat_real A x *\<^sub>R y) \<partial>M = (\<integral>x\<in>B. indicat_real A x \<partial>M) *\<^sub>R y" using assms by (intro set_integral_scaleR_left, meson 1 in_mono subalg subalgebra_def, blast)
also have "... = (\<integral>x\<in>B. real_cond_exp M F (indicator A) x \<partial>M) *\<^sub>R y" using 1 assms by (subst real_cond_exp_intA, auto)
also have "... = \<integral>x\<in>B. (real_cond_exp M F (indicator A) x *\<^sub>R y) \<partial>M" using assms by (intro set_integral_scaleR_left[symmetric], meson 1 in_mono subalg subalgebra_def, blast)
finally show ?case .
next
case 2
show ?case using integrable_scaleR_left integrable_real_indicator assms by blast
next
case 3
show ?case using assms by (intro integrable_scaleR_left, intro real_cond_exp_int, blast+)
next
case 4
show ?case by (intro borel_measurable_scaleR, intro Conditional_Expectation.borel_measurable_cond_exp, simp)
qed
lemma cond_exp_indicator[intro]:
fixes y :: "'b::{second_countable_topology,banach}"
assumes [measurable]: "A \<in> sets M" "emeasure M A < \<infinity>"
shows "AE x in M. cond_exp M F (\<lambda>x. indicat_real A x *\<^sub>R y) x = cond_exp M F (indicator A) x *\<^sub>R y"
proof -
have "AE x in M. cond_exp M F (\<lambda>x. indicat_real A x *\<^sub>R y) x = real_cond_exp M F (indicator A) x *\<^sub>R y" using has_cond_exp_indicator[OF assms] has_cond_exp_charact by blast
thus ?thesis using cond_exp_real[OF integrable_real_indicator, OF assms] by fastforce
qed
text \<open>Addition\<close>
lemma has_cond_exp_add:
fixes f g :: "'a \<Rightarrow> 'b::{second_countable_topology,banach}"
assumes "has_cond_exp M F f f'" "has_cond_exp M F g g'"
shows "has_cond_exp M F (\<lambda>x. f x + g x) (\<lambda>x. f' x + g' x)"
proof (intro has_cond_expI', goal_cases)
case (1 A)
have "\<integral>x\<in>A. (f x + g x)\<partial>M = (\<integral>x\<in>A. f x \<partial>M) + (\<integral>x\<in>A. g x \<partial>M)" using assms[THEN has_cond_expD(2)] subalg 1 by (intro set_integral_add(2), auto simp add: subalgebra_def set_integrable_def intro: integrable_mult_indicator)
also have "... = (\<integral>x\<in>A. f' x \<partial>M) + (\<integral>x\<in>A. g' x \<partial>M)" using assms[THEN has_cond_expD(1)[OF _ 1]] by argo
also have "... = \<integral>x\<in>A. (f' x + g' x)\<partial>M" using assms[THEN has_cond_expD(3)] subalg 1 by (intro set_integral_add(2)[symmetric], auto simp add: subalgebra_def set_integrable_def intro: integrable_mult_indicator)
finally show ?case .
next
case 2
show ?case by (metis Bochner_Integration.integrable_add assms has_cond_expD(2))
next
case 3
show ?case by (metis Bochner_Integration.integrable_add assms has_cond_expD(3))
next
case 4
show ?case using assms borel_measurable_add has_cond_expD(4) by blast
qed
lemma has_cond_exp_scaleR_right:
fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology,banach}"
assumes "has_cond_exp M F f f'"
shows "has_cond_exp M F (\<lambda>x. c *\<^sub>R f x) (\<lambda>x. c *\<^sub>R f' x)"
using has_cond_expD[OF assms] by (intro has_cond_expI', auto)
lemma cond_exp_scaleR_right:
fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology,banach}"
assumes "integrable M f"
shows "AE x in M. cond_exp M F (\<lambda>x. c *\<^sub>R f x) x = c *\<^sub>R cond_exp M F f x"
proof (cases "\<exists>f'. has_cond_exp M F f f'")
case True
then show ?thesis using assms has_cond_exp_charact has_cond_exp_scaleR_right by metis
next
case False
show ?thesis
proof (cases "c = 0")
case True
then show ?thesis by simp
next
case c_nonzero: False
have "\<nexists>f'. has_cond_exp M F (\<lambda>x. c *\<^sub>R f x) f'"
proof (standard, goal_cases)
case 1
then obtain f' where f': "has_cond_exp M F (\<lambda>x. c *\<^sub>R f x) f'" by blast
have "has_cond_exp M F f (\<lambda>x. inverse c *\<^sub>R f' x)" using has_cond_expD[OF f'] divideR_right[OF c_nonzero] assms by (intro has_cond_expI', auto)
then show ?case using False by blast
qed
then show ?thesis using cond_exp_null[OF False] cond_exp_null by force
qed
qed
lemma cond_exp_uminus:
fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology,banach}"
assumes "integrable M f"
shows "AE x in M. cond_exp M F (\<lambda>x. - f x) x = - cond_exp M F f x"
using cond_exp_scaleR_right[OF assms, of "-1"] by force
text \<open>Together with the induction scheme \<open>integrable_simple_function_induct\<close>, we can show that the conditional expectation of an integrable simple function exists.\<close>
corollary has_cond_exp_simple:
fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology,banach}"
assumes "simple_function M f" "emeasure M {y \<in> space M. f y \<noteq> 0} \<noteq> \<infinity>"
shows "has_cond_exp M F f (cond_exp M F f)"
using assms
proof (induction rule: integrable_simple_function_induct)
case (cong f g)
then show ?case using has_cond_exp_cong by (metis (no_types, opaque_lifting) Bochner_Integration.integrable_cong has_cond_expD(2) has_cond_exp_charact(1))
next
case (indicator A y)
then show ?case using has_cond_exp_charact[OF has_cond_exp_indicator] by fast
next
case (add u v)
then show ?case using has_cond_exp_add has_cond_exp_charact(1) by blast
qed
text \<open>Now comes the most difficult part. Given a convergent sequence of integrable simple functions \<^term>\<open>\<lambda>n. s n\<close>,
we must show that the sequence \<^term>\<open>\<lambda>n. cond_exp M F (s n)\<close> is also convergent. Furthermore, we must show that this limit satisfies the properties of a conditional expectation.
Unfortunately, we will only be able to show that this sequence convergences in the L1-norm.
Luckily, this is enough to show that the operator \<^term>\<open>cond_exp M F\<close> preserves limits as a function from L1 to L1.\<close>
text \<open>In anticipation of this result, we show that the conditional expectation operator is a contraction for simple functions.
We first reformulate the lemma \<open>real_cond_exp_abs\<close>, which shows the statement for real-valued functions, using our definitions.
Then we show the statement for simple functions via induction.\<close>
lemma cond_exp_contraction_real:
fixes f :: "'a \<Rightarrow> real"
assumes integrable[measurable]: "integrable M f"
shows "AE x in M. norm (cond_exp M F f x) \<le> cond_exp M F (\<lambda>x. norm (f x)) x"
proof-
have int: "integrable M (\<lambda>x. norm (f x))" using assms by blast
have *: "AE x in M. 0 \<le> cond_exp M F (\<lambda>x. norm (f x)) x" using cond_exp_real[THEN AE_symmetric, OF integrable_norm[OF integrable]] real_cond_exp_ge_c[OF integrable_norm[OF integrable], of 0] norm_ge_zero by fastforce
have **: "A \<in> sets F \<Longrightarrow> \<integral>x\<in>A. \<bar>f x\<bar> \<partial>M = \<integral>x\<in>A. real_cond_exp M F (\<lambda>x. norm (f x)) x \<partial>M" for A unfolding real_norm_def using assms integrable_abs real_cond_exp_intA by blast
have norm_int: "A \<in> sets F \<Longrightarrow> (\<integral>x\<in>A. \<bar>f x\<bar> \<partial>M) = (\<integral>\<^sup>+x\<in>A. \<bar>f x\<bar> \<partial>M)" for A using assms by (intro nn_set_integral_eq_set_integral[symmetric], blast, fastforce) (meson subalg subalgebra_def subsetD)
have "AE x in M. real_cond_exp M F (\<lambda>x. norm (f x)) x \<ge> 0" using int real_cond_exp_ge_c by force
hence cond_exp_norm_int: "A \<in> sets F \<Longrightarrow> (\<integral>x\<in>A. real_cond_exp M F (\<lambda>x. norm (f x)) x \<partial>M) = (\<integral>\<^sup>+x\<in>A. real_cond_exp M F (\<lambda>x. norm (f x)) x \<partial>M)" for A using assms by (intro nn_set_integral_eq_set_integral[symmetric], blast, fastforce) (meson subalg subalgebra_def subsetD)
have "A \<in> sets F \<Longrightarrow> \<integral>\<^sup>+x\<in>A. \<bar>f x\<bar>\<partial>M = \<integral>\<^sup>+x\<in>A. real_cond_exp M F (\<lambda>x. norm (f x)) x \<partial>M" for A using ** norm_int cond_exp_norm_int by (auto simp add: nn_integral_set_ennreal)
moreover have "(\<lambda>x. ennreal \<bar>f x\<bar>) \<in> borel_measurable M" by measurable
moreover have "(\<lambda>x. ennreal (real_cond_exp M F (\<lambda>x. norm (f x)) x)) \<in> borel_measurable F" by measurable
ultimately have "AE x in M. nn_cond_exp M F (\<lambda>x. ennreal \<bar>f x\<bar>) x = real_cond_exp M F (\<lambda>x. norm (f x)) x" by (intro nn_cond_exp_charact[THEN AE_symmetric], auto)
hence "AE x in M. nn_cond_exp M F (\<lambda>x. ennreal \<bar>f x\<bar>) x \<le> cond_exp M F (\<lambda>x. norm (f x)) x" using cond_exp_real[OF int] by force
moreover have "AE x in M. \<bar>real_cond_exp M F f x\<bar> = norm (cond_exp M F f x)" unfolding real_norm_def using cond_exp_real[OF assms] * by force
ultimately have "AE x in M. ennreal (norm (cond_exp M F f x)) \<le> cond_exp M F (\<lambda>x. norm (f x)) x" using real_cond_exp_abs[OF assms[THEN borel_measurable_integrable]] by fastforce
hence "AE x in M. enn2real (ennreal (norm (cond_exp M F f x))) \<le> enn2real (cond_exp M F (\<lambda>x. norm (f x)) x)" using ennreal_le_iff2 by force
thus ?thesis using * by fastforce
qed
lemma cond_exp_contraction_simple:
fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, banach}"
assumes "simple_function M f" "emeasure M {y \<in> space M. f y \<noteq> 0} \<noteq> \<infinity>"
shows "AE x in M. norm (cond_exp M F f x) \<le> cond_exp M F (\<lambda>x. norm (f x)) x"
using assms
proof (induction rule: integrable_simple_function_induct)
case (cong f g)
hence ae: "AE x in M. f x = g x" by blast
hence "AE x in M. cond_exp M F f x = cond_exp M F g x" using cong has_cond_exp_simple by (subst cond_exp_cong_AE) (auto intro!: has_cond_expD(2))
hence "AE x in M. norm (cond_exp M F f x) = norm (cond_exp M F g x)" by force
moreover have "AE x in M. cond_exp M F (\<lambda>x. norm (f x)) x = cond_exp M F (\<lambda>x. norm (g x)) x" using ae cong has_cond_exp_simple by (subst cond_exp_cong_AE) (auto dest: has_cond_expD)
ultimately show ?case using cong(6) by fastforce
next
case (indicator A y)
hence "AE x in M. cond_exp M F (\<lambda>a. indicator A a *\<^sub>R y) x = cond_exp M F (indicator A) x *\<^sub>R y" by blast
hence *: "AE x in M. norm (cond_exp M F (\<lambda>a. indicat_real A a *\<^sub>R y) x) \<le> norm y * cond_exp M F (\<lambda>x. norm (indicat_real A x)) x" using cond_exp_contraction_real[OF integrable_real_indicator, OF indicator] by fastforce
have "AE x in M. norm y * cond_exp M F (\<lambda>x. norm (indicat_real A x)) x = norm y * real_cond_exp M F (\<lambda>x. norm (indicat_real A x)) x" using cond_exp_real[OF integrable_real_indicator, OF indicator] by fastforce
moreover have "AE x in M. cond_exp M F (\<lambda>x. norm y * norm (indicat_real A x)) x = real_cond_exp M F (\<lambda>x. norm y * norm (indicat_real A x)) x" using indicator by (intro cond_exp_real, auto)
ultimately have "AE x in M. norm y * cond_exp M F (\<lambda>x. norm (indicat_real A x)) x = cond_exp M F (\<lambda>x. norm y * norm (indicat_real A x)) x" using real_cond_exp_cmult[of "\<lambda>x. norm (indicat_real A x)" "norm y"] indicator by fastforce
moreover have "(\<lambda>x. norm y * norm (indicat_real A x)) = (\<lambda>x. norm (indicat_real A x *\<^sub>R y))" by force
ultimately show ?case using * by force
next
case (add u v)
have "AE x in M. norm (cond_exp M F (\<lambda>a. u a + v a) x) = norm (cond_exp M F u x + cond_exp M F v x)" using has_cond_exp_charact(2)[OF has_cond_exp_add, OF has_cond_exp_simple(1,1), OF add(1,2,3,4)] by fastforce
moreover have "AE x in M. norm (cond_exp M F u x + cond_exp M F v x) \<le> norm (cond_exp M F u x) + norm (cond_exp M F v x)" using norm_triangle_ineq by blast
moreover have "AE x in M. norm (cond_exp M F u x) + norm (cond_exp M F v x) \<le> cond_exp M F (\<lambda>x. norm (u x)) x + cond_exp M F (\<lambda>x. norm (v x)) x" using add(6,7) by fastforce
moreover have "AE x in M. cond_exp M F (\<lambda>x. norm (u x)) x + cond_exp M F (\<lambda>x. norm (v x)) x = cond_exp M F (\<lambda>x. norm (u x) + norm (v x)) x" using integrable_simple_function[OF add(1,2)] integrable_simple_function[OF add(3,4)] by (intro has_cond_exp_charact(2)[OF has_cond_exp_add[OF has_cond_exp_charact(1,1)], THEN AE_symmetric], auto intro: has_cond_exp_real)
moreover have "AE x in M. cond_exp M F (\<lambda>x. norm (u x) + norm (v x)) x = cond_exp M F (\<lambda>x. norm (u x + v x)) x" using add(5) integrable_simple_function[OF add(1,2)] integrable_simple_function[OF add(3,4)] by (intro cond_exp_cong, auto)
ultimately show ?case by force
qed
lemma has_cond_exp_simple_lim:
fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, banach}"
assumes integrable[measurable]: "integrable M f"
and "\<And>i. simple_function M (s i)"
and "\<And>i. emeasure M {y \<in> space M. s i y \<noteq> 0} \<noteq> \<infinity>"
and "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. s i x) \<longlonglongrightarrow> f x"
and "\<And>x i. x \<in> space M \<Longrightarrow> norm (s i x) \<le> 2 * norm (f x)"
obtains r
where "strict_mono r" "has_cond_exp M F f (\<lambda>x. lim (\<lambda>i. cond_exp M F (s (r i)) x))"
"AE x in M. convergent (\<lambda>i. cond_exp M F (s (r i)) x)"
proof -
have [measurable]: "(s i) \<in> borel_measurable M" for i using assms(2) by (simp add: borel_measurable_simple_function)
have integrable_s: "integrable M (\<lambda>x. s i x)" for i using assms integrable_simple_function by blast
have integrable_4f: "integrable M (\<lambda>x. 4 * norm (f x))" using assms(1) by simp
have integrable_2f: "integrable M (\<lambda>x. 2 * norm (f x))" using assms(1) by simp
have integrable_2_cond_exp_norm_f: "integrable M (\<lambda>x. 2 * cond_exp M F (\<lambda>x. norm (f x)) x)" by fast
have "emeasure M {y \<in> space M. s i y - s j y \<noteq> 0} \<le> emeasure M {y \<in> space M. s i y \<noteq> 0} + emeasure M {y \<in> space M. s j y \<noteq> 0}" for i j using simple_functionD(2)[OF assms(2)] by (intro order_trans[OF emeasure_mono emeasure_subadditive], auto)
hence fin_sup: "emeasure M {y \<in> space M. s i y - s j y \<noteq> 0} \<noteq> \<infinity>" for i j using assms(3) by (metis (mono_tags) ennreal_add_eq_top linorder_not_less top.not_eq_extremum infinity_ennreal_def)
have "emeasure M {y \<in> space M. norm (s i y - s j y) \<noteq> 0} \<le> emeasure M {y \<in> space M. s i y \<noteq> 0} + emeasure M {y \<in> space M. s j y \<noteq> 0}" for i j using simple_functionD(2)[OF assms(2)] by (intro order_trans[OF emeasure_mono emeasure_subadditive], auto)
hence fin_sup_norm: "emeasure M {y \<in> space M. norm (s i y - s j y) \<noteq> 0} \<noteq> \<infinity>" for i j using assms(3) by (metis (mono_tags) ennreal_add_eq_top linorder_not_less top.not_eq_extremum infinity_ennreal_def)
have Cauchy: "Cauchy (\<lambda>n. s n x)" if "x \<in> space M" for x using assms(4) LIMSEQ_imp_Cauchy that by blast
hence bounded_range_s: "bounded (range (\<lambda>n. s n x))" if "x \<in> space M" for x using that cauchy_imp_bounded by fast
text \<open>Since the sequence \<^term>\<open>(\<lambda>n. s n x)\<close> is Cauchy for almost all \<^term>\<open>x\<close>, we know that the diameter tends to zero almost everywhere.\<close>
text \<open>Dominated convergence tells us that the integral of the diameter also converges to zero.\<close>
have "AE x in M. (\<lambda>n. diameter {s i x | i. n \<le> i}) \<longlonglongrightarrow> 0" using Cauchy cauchy_iff_diameter_tends_to_zero_and_bounded by fast
moreover have "(\<lambda>x. diameter {s i x |i. n \<le> i}) \<in> borel_measurable M" for n using bounded_range_s borel_measurable_diameter by measurable
moreover have "AE x in M. norm (diameter {s i x |i. n \<le> i}) \<le> 4 * norm (f x)" for n
proof -
{
fix x assume x: "x \<in> space M"
have "diameter {s i x |i. n \<le> i} \<le> 2 * norm (f x) + 2 * norm (f x)" by (intro diameter_le, blast, subst dist_norm[symmetric], intro dist_triangle3[THEN order_trans, of 0], intro add_mono) (auto intro: assms(5)[OF x])
hence "norm (diameter {s i x |i. n \<le> i}) \<le> 4 * norm (f x)" using diameter_ge_0[OF bounded_subset[OF bounded_range_s], OF x, of "{s i x |i. n \<le> i}"] by force
}
thus ?thesis by fast
qed
ultimately have diameter_tendsto_zero: "(\<lambda>n. LINT x|M. diameter {s i x | i. n \<le> i}) \<longlonglongrightarrow> 0" by (intro integral_dominated_convergence[OF borel_measurable_const[of 0] _ integrable_4f, simplified]) (fast+)
have diameter_integrable: "integrable M (\<lambda>x. diameter {s i x | i. n \<le> i})" for n using assms(1,5)
by (intro integrable_bound_diameter[OF bounded_range_s integrable_2f], auto)
have dist_integrable: "integrable M (\<lambda>x. dist (s i x) (s j x))" for i j using assms(5) dist_triangle3[of "s i _" _ 0, THEN order_trans, OF add_mono, of _ "2 * norm (f _)"]
by (intro Bochner_Integration.integrable_bound[OF integrable_4f]) fastforce+
text \<open>Since \<^term>\<open>cond_exp M F\<close> is a contraction for simple functions, the following sequence of integral values is also Cauchy.\<close>
text \<open>This follows, since the distance between the terms of this sequence are always less than or equal to the diameter, which itself converges to zero.\<close>
text \<open>Hence, we obtain a subsequence which is Cauchy almost everywhere.\<close>
have "\<exists>N. \<forall>i\<ge>N. \<forall>j\<ge>N. LINT x|M. norm (cond_exp M F (s i) x - cond_exp M F (s j) x) < e" if e_pos: "e > 0" for e
proof -
obtain N where *: "LINT x|M. diameter {s i x | i. n \<le> i} < e" if "n \<ge> N" for n using that order_tendsto_iff[THEN iffD1, OF diameter_tendsto_zero, unfolded eventually_sequentially] e_pos by presburger
{
fix i j x assume asm: "i \<ge> N" "j \<ge> N" "x \<in> space M"
have "case_prod dist ` ({s i x |i. N \<le> i} \<times> {s i x |i. N \<le> i}) = case_prod (\<lambda>i j. dist (s i x) (s j x)) ` ({N..} \<times> {N..})" by fast
hence "diameter {s i x | i. N \<le> i} = (SUP (i, j) \<in> {N..} \<times> {N..}. dist (s i x) (s j x))" unfolding diameter_def by auto
moreover have "(SUP (i, j) \<in> {N..} \<times> {N..}. dist (s i x) (s j x)) \<ge> dist (s i x) (s j x)" using asm bounded_imp_bdd_above[OF bounded_imp_dist_bounded, OF bounded_range_s] by (intro cSup_upper, auto)
ultimately have "diameter {s i x | i. N \<le> i} \<ge> dist (s i x) (s j x)" by presburger
}
hence "LINT x|M. dist (s i x) (s j x) < e" if "i \<ge> N" "j \<ge> N" for i j using that * by (intro integral_mono[OF dist_integrable diameter_integrable, THEN order.strict_trans1], blast+)
moreover have "LINT x|M. norm (cond_exp M F (s i) x - cond_exp M F (s j) x) \<le> LINT x|M. dist (s i x) (s j x)" for i j
proof -
have "LINT x|M. norm (cond_exp M F (s i) x - cond_exp M F (s j) x) = LINT x|M. norm (cond_exp M F (s i) x + - 1 *\<^sub>R cond_exp M F (s j) x)" unfolding dist_norm by simp
also have "... = LINT x|M. norm (cond_exp M F (\<lambda>x. s i x - s j x) x)" using has_cond_exp_charact(2)[OF has_cond_exp_add[OF _ has_cond_exp_scaleR_right, OF has_cond_exp_charact(1,1), OF has_cond_exp_simple(1,1)[OF assms(2,3)]], THEN AE_symmetric, of i "-1" j] by (intro integral_cong_AE) force+
also have "... \<le> LINT x|M. cond_exp M F (\<lambda>x. norm (s i x - s j x)) x" using cond_exp_contraction_simple[OF _ fin_sup, of i j] integrable_cond_exp assms(2) by (intro integral_mono_AE, fast+)
also have "... = LINT x|M. norm (s i x - s j x)" unfolding set_integral_space(1)[OF integrable_cond_exp, symmetric] set_integral_space[OF dist_integrable[unfolded dist_norm], symmetric] by (intro has_cond_expD(1)[OF has_cond_exp_simple[OF _ fin_sup_norm], symmetric]) (metis assms(2) simple_function_compose1 simple_function_diff, metis sets.top subalg subalgebra_def)
finally show ?thesis unfolding dist_norm .
qed
ultimately show ?thesis using order.strict_trans1 by meson
qed
then obtain r where strict_mono_r: "strict_mono r" and AE_Cauchy: "AE x in M. Cauchy (\<lambda>i. cond_exp M F (s (r i)) x)"
by (rule cauchy_L1_AE_cauchy_subseq[OF integrable_cond_exp], auto)
hence ae_lim_cond_exp: "AE x in M. (\<lambda>n. cond_exp M F (s (r n)) x) \<longlonglongrightarrow> lim (\<lambda>n. cond_exp M F (s (r n)) x)" using Cauchy_convergent_iff convergent_LIMSEQ_iff by fastforce
text \<open>Now that we have a candidate for the conditional expectation, we must show that it actually has the required properties.\<close>
text \<open>Dominated convergence shows that this limit is indeed integrable.\<close>
text \<open>Here, we again use the fact that conditional expectation is a contraction on simple functions.\<close>
have cond_exp_bounded: "AE x in M. norm (cond_exp M F (s (r n)) x) \<le> cond_exp M F (\<lambda>x. 2 * norm (f x)) x" for n
proof -
have "AE x in M. norm (cond_exp M F (s (r n)) x) \<le> cond_exp M F (\<lambda>x. norm (s (r n) x)) x" by (rule cond_exp_contraction_simple[OF assms(2,3)])
moreover have "AE x in M. real_cond_exp M F (\<lambda>x. norm (s (r n) x)) x \<le> real_cond_exp M F (\<lambda>x. 2 * norm (f x)) x" using integrable_s integrable_2f assms(5) by (intro real_cond_exp_mono, auto)
ultimately show ?thesis using cond_exp_real[OF integrable_norm, OF integrable_s, of "r n"] cond_exp_real[OF integrable_2f] by force
qed
have lim_integrable: "integrable M (\<lambda>x. lim (\<lambda>i. cond_exp M F (s (r i)) x))" by (intro integrable_dominated_convergence[OF _ borel_measurable_cond_exp' integrable_cond_exp ae_lim_cond_exp cond_exp_bounded], simp)
text \<open>Moreover, we can use the DCT twice to show that the conditional expectation property holds, i.e. the value of the integral of the candidate, agrees with \<^term>\<open>f\<close> on sets \<^term>\<open>A \<in> F\<close>.\<close>
{
fix A assume A_in_sets_F: "A \<in> sets F"
have "AE x in M. norm (indicator A x *\<^sub>R cond_exp M F (s (r n)) x) \<le> cond_exp M F (\<lambda>x. 2 * norm (f x)) x" for n
proof -
have "AE x in M. norm (indicator A x *\<^sub>R cond_exp M F (s (r n)) x) \<le> norm (cond_exp M F (s (r n)) x)" unfolding indicator_def by simp
thus ?thesis using cond_exp_bounded[of n] by force
qed
hence lim_cond_exp_int: "(\<lambda>n. LINT x:A|M. cond_exp M F (s (r n)) x) \<longlonglongrightarrow> LINT x:A|M. lim (\<lambda>n. cond_exp M F (s (r n)) x)"
using ae_lim_cond_exp measurable_from_subalg[OF subalg borel_measurable_indicator, OF A_in_sets_F] cond_exp_bounded
unfolding set_lebesgue_integral_def
by (intro integral_dominated_convergence[OF borel_measurable_scaleR borel_measurable_scaleR integrable_cond_exp]) (fastforce simp add: tendsto_scaleR)+
have "AE x in M. norm (indicator A x *\<^sub>R s (r n) x) \<le> 2 * norm (f x)" for n
proof -
have "AE x in M. norm (indicator A x *\<^sub>R s (r n) x) \<le> norm (s (r n) x)" unfolding indicator_def by simp
thus ?thesis using assms(5)[of _ "r n"] by fastforce
qed
hence lim_s_int: "(\<lambda>n. LINT x:A|M. s (r n) x) \<longlonglongrightarrow> LINT x:A|M. f x"
using measurable_from_subalg[OF subalg borel_measurable_indicator, OF A_in_sets_F] LIMSEQ_subseq_LIMSEQ[OF assms(4) strict_mono_r] assms(5)
unfolding set_lebesgue_integral_def comp_def
by (intro integral_dominated_convergence[OF borel_measurable_scaleR borel_measurable_scaleR integrable_2f]) (fastforce simp add: tendsto_scaleR)+
have "LINT x:A|M. lim (\<lambda>n. cond_exp M F (s (r n)) x) = lim (\<lambda>n. LINT x:A|M. cond_exp M F (s (r n)) x)" using limI[OF lim_cond_exp_int] by argo
also have "... = lim (\<lambda>n. LINT x:A|M. s (r n) x)" using has_cond_expD(1)[OF has_cond_exp_simple[OF assms(2,3)] A_in_sets_F, symmetric] by presburger
also have "... = LINT x:A|M. f x" using limI[OF lim_s_int] by argo
finally have "LINT x:A|M. lim (\<lambda>n. cond_exp M F (s (r n)) x) = LINT x:A|M. f x" .
}
text \<open>Putting it all together, we have the statement we are looking for.\<close>
hence "has_cond_exp M F f (\<lambda>x. lim (\<lambda>i. cond_exp M F (s (r i)) x))" using assms(1) lim_integrable by (intro has_cond_expI', auto)
thus thesis using AE_Cauchy Cauchy_convergent strict_mono_r by (auto intro!: that)
qed
text \<open>Now, we can show that the conditional expectation is well-defined for all integrable functions.\<close>
corollary has_cond_expI:
fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology,banach}"
assumes "integrable M f"
shows "has_cond_exp M F f (cond_exp M F f)"
proof -
obtain s where s_is: "\<And>i. simple_function M (s i)" "\<And>i. emeasure M {y \<in> space M. s i y \<noteq> 0} \<noteq> \<infinity>" "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. s i x) \<longlonglongrightarrow> f x" "\<And>x i. x \<in> space M \<Longrightarrow> norm (s i x) \<le> 2 * norm (f x)" using integrable_implies_simple_function_sequence[OF assms] by blast
show ?thesis using has_cond_exp_simple_lim[OF assms s_is] has_cond_exp_charact(1) by metis
qed
subsection \<open>Properties\<close>
text \<open>The defining property of the conditional expectation now always holds, given that the function \<^term>\<open>f\<close> is integrable.\<close>
lemma cond_exp_set_integral:
fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology,banach}"
assumes "integrable M f" "A \<in> sets F"
shows "(\<integral> x \<in> A. f x \<partial>M) = (\<integral> x \<in> A. cond_exp M F f x \<partial>M)"
using has_cond_expD(1)[OF has_cond_expI, OF assms] by argo
(* Tower Property *)
text \<open>The following property of the conditional expectation is called the "Tower Property".\<close>
lemma cond_exp_nested_subalg:
fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology,banach}"
assumes "integrable M f" "subalgebra M G" "subalgebra G F"
shows "AE \<xi> in M. cond_exp M F f \<xi> = cond_exp M F (cond_exp M G f) \<xi>"
using has_cond_expI assms sigma_finite_subalgebra_def by (auto intro!: has_cond_exp_nested_subalg[THEN has_cond_exp_charact(2), THEN AE_symmetric] sigma_finite_subalgebra.has_cond_expI[OF sigma_finite_subalgebra.intro[OF assms(2)]] nested_subalg_is_sigma_finite)
(* Linearity *)
text \<open>The conditional expectation is linear.\<close>
lemma cond_exp_add:
fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology,banach}"
assumes "integrable M f" "integrable M g"
shows "AE x in M. cond_exp M F (\<lambda>x. f x + g x) x = cond_exp M F f x + cond_exp M F g x"
using has_cond_exp_add[OF has_cond_expI(1,1), OF assms, THEN has_cond_exp_charact(2)] .
lemma cond_exp_diff:
fixes f :: "'a \<Rightarrow> 'b :: {second_countable_topology, banach}"
assumes "integrable M f" "integrable M g"
shows "AE x in M. cond_exp M F (\<lambda>x. f x - g x) x = cond_exp M F f x - cond_exp M F g x"
using has_cond_exp_add[OF _ has_cond_exp_scaleR_right, OF has_cond_expI(1,1), OF assms, THEN has_cond_exp_charact(2), of "-1"] by simp
lemma cond_exp_diff':
fixes f :: "'a \<Rightarrow> 'b :: {second_countable_topology, banach}"
assumes "integrable M f" "integrable M g"
shows "AE x in M. cond_exp M F (f - g) x = cond_exp M F f x - cond_exp M F g x"
unfolding fun_diff_def using assms by (rule cond_exp_diff)
lemma cond_exp_scaleR_left:
fixes f :: "'a \<Rightarrow> real"
assumes "integrable M f"
shows "AE x in M. cond_exp M F (\<lambda>x. f x *\<^sub>R c) x = cond_exp M F f x *\<^sub>R c"
using cond_exp_set_integral[OF assms] subalg assms unfolding subalgebra_def
by (intro cond_exp_charact,
subst set_integral_scaleR_left, blast, intro assms,
subst set_integral_scaleR_left, blast, intro integrable_cond_exp)
auto
text \<open>The conditional expectation operator is a contraction, i.e. a bounded linear operator with operator norm less than or equal to 1.\<close>
text \<open>To show this we first obtain a subsequence \<^term>\<open>\<lambda>x. (\<lambda>i. s (r i) x)\<close>, such that \<^term>\<open>(\<lambda>i. cond_exp M F (s (r i)) x)\<close> converges to \<^term>\<open>cond_exp M F f x\<close> a.e.
Afterwards, we obtain a sub-subsequence \<^term>\<open>\<lambda>x. (\<lambda>i. s (r (r' i)) x)\<close>, such that \<^term>\<open>(\<lambda>i. cond_exp M F (\<lambda>x. norm (s (r i))) x)\<close> converges to \<^term>\<open>cond_exp M F (\<lambda>x. norm (f x)) x\<close> a.e.
Finally, we show that the inequality holds by showing that the terms of the subsequences obey the inequality and the fact that a subsequence of a convergent sequence converges to the same limit.\<close>
lemma cond_exp_contraction:
fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, banach}"
assumes "integrable M f"
shows "AE x in M. norm (cond_exp M F f x) \<le> cond_exp M F (\<lambda>x. norm (f x)) x"
proof -
obtain s where s: "\<And>i. simple_function M (s i)" "\<And>i. emeasure M {y \<in> space M. s i y \<noteq> 0} \<noteq> \<infinity>" "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. s i x) \<longlonglongrightarrow> f x" "\<And>i x. x \<in> space M \<Longrightarrow> norm (s i x) \<le> 2 * norm (f x)"
by (blast intro: integrable_implies_simple_function_sequence[OF assms])
obtain r where r: "strict_mono r" and "has_cond_exp M F f (\<lambda>x. lim (\<lambda>i. cond_exp M F (s (r i)) x))" "AE x in M. (\<lambda>i. cond_exp M F (s (r i)) x) \<longlonglongrightarrow> lim (\<lambda>i. cond_exp M F (s (r i)) x)"
using has_cond_exp_simple_lim[OF assms s] unfolding convergent_LIMSEQ_iff by blast
hence r_tendsto: "AE x in M. (\<lambda>i. cond_exp M F (s (r i)) x) \<longlonglongrightarrow> cond_exp M F f x" using has_cond_exp_charact(2) by force
have norm_s_r: "\<And>i. simple_function M (\<lambda>x. norm (s (r i) x))" "\<And>i. emeasure M {y \<in> space M. norm (s (r i) y) \<noteq> 0} \<noteq> \<infinity>" "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. norm (s (r i) x)) \<longlonglongrightarrow> norm (f x)" "\<And>i x. x \<in> space M \<Longrightarrow> norm (norm (s (r i) x)) \<le> 2 * norm (norm (f x))"
using s by (auto intro: LIMSEQ_subseq_LIMSEQ[OF tendsto_norm r, unfolded comp_def] simple_function_compose1)
obtain r' where r': "strict_mono r'" and "has_cond_exp M F (\<lambda>x. norm (f x)) (\<lambda>x. lim (\<lambda>i. cond_exp M F (\<lambda>x. norm (s (r (r' i)) x)) x))" "AE x in M. (\<lambda>i. cond_exp M F (\<lambda>x. norm (s (r (r' i)) x)) x) \<longlonglongrightarrow> lim (\<lambda>i. cond_exp M F (\<lambda>x. norm (s (r (r' i)) x)) x)" using has_cond_exp_simple_lim[OF integrable_norm norm_s_r, OF assms] unfolding convergent_LIMSEQ_iff by blast
hence r'_tendsto: "AE x in M. (\<lambda>i. cond_exp M F (\<lambda>x. norm (s (r (r' i)) x)) x) \<longlonglongrightarrow> cond_exp M F (\<lambda>x. norm (f x)) x" using has_cond_exp_charact(2) by force
have "AE x in M. \<forall>i. norm (cond_exp M F (s (r (r' i))) x) \<le> cond_exp M F (\<lambda>x. norm (s (r (r' i)) x)) x" using s by (auto intro: cond_exp_contraction_simple simp add: AE_all_countable)
moreover have "AE x in M. (\<lambda>i. norm (cond_exp M F (s (r (r' i))) x)) \<longlonglongrightarrow> norm (cond_exp M F f x)" using r_tendsto LIMSEQ_subseq_LIMSEQ[OF tendsto_norm r', unfolded comp_def] by fast
ultimately show ?thesis using LIMSEQ_le r'_tendsto by fast
qed
text \<open>The following lemmas are called "pulling out whats known". We first show the statement for real-valued functions using the lemma \<open>real_cond_exp_intg\<close>, which is already present.
We then show it for arbitrary \<^term>\<open>g\<close> using the lecture notes of Gordan Zitkovic for the course "Theory of Probability I" \cite{Zitkovic_2015}.\<close>
lemma cond_exp_measurable_mult:
fixes f g :: "'a \<Rightarrow> real"
assumes [measurable]: "integrable M (\<lambda>x. f x * g x)" "integrable M g" "f \<in> borel_measurable F"
shows "integrable M (\<lambda>x. f x * cond_exp M F g x)"
"AE x in M. cond_exp M F (\<lambda>x. f x * g x) x = f x * cond_exp M F g x"
proof-
show integrable: "integrable M (\<lambda>x. f x * cond_exp M F g x)" using cond_exp_real[OF assms(2)] by (intro integrable_cong_AE_imp[OF real_cond_exp_intg(1), OF assms(1,3) assms(2)[THEN borel_measurable_integrable]] measurable_from_subalg[OF subalg]) auto
interpret sigma_finite_measure "restr_to_subalg M F" by (rule sigma_fin_subalg)
{
fix A assume asm: "A \<in> sets F"
hence asm': "A \<in> sets M" using subalg by (fastforce simp add: subalgebra_def)
have "set_lebesgue_integral M A (cond_exp M F (\<lambda>x. f x * g x)) = set_lebesgue_integral M A (\<lambda>x. f x * g x)" by (simp add: cond_exp_set_integral[OF assms(1) asm])
also have "... = set_lebesgue_integral M A (\<lambda>x. f x * real_cond_exp M F g x)" using borel_measurable_times[OF borel_measurable_indicator[OF asm] assms(3)] borel_measurable_integrable[OF assms(2)] integrable_mult_indicator[OF asm' assms(1)] by (fastforce simp add: set_lebesgue_integral_def mult.assoc[symmetric] intro: real_cond_exp_intg(2)[symmetric])
also have "... = set_lebesgue_integral M A (\<lambda>x. f x * cond_exp M F g x)" using cond_exp_real[OF assms(2)] asm' borel_measurable_cond_exp' borel_measurable_cond_exp2 measurable_from_subalg[OF subalg assms(3)] by (auto simp add: set_lebesgue_integral_def intro: integral_cong_AE)
finally have "set_lebesgue_integral M A (cond_exp M F (\<lambda>x. f x * g x)) = \<integral>x\<in>A. (f x * cond_exp M F g x)\<partial>M" .
}
hence "AE x in restr_to_subalg M F. cond_exp M F (\<lambda>x. f x * g x) x = f x * cond_exp M F g x" by (intro density_unique_banach integrable_cond_exp integrable integrable_in_subalg subalg, measurable, simp add: set_lebesgue_integral_def integral_subalgebra2[OF subalg] sets_restr_to_subalg[OF subalg])
thus "AE x in M. cond_exp M F (\<lambda>x. f x * g x) x = f x * cond_exp M F g x" by (rule AE_restr_to_subalg[OF subalg])
qed
lemma cond_exp_measurable_scaleR:
fixes f :: "'a \<Rightarrow> real" and g :: "'a \<Rightarrow> 'b :: {second_countable_topology, banach}"
assumes [measurable]: "integrable M (\<lambda>x. f x *\<^sub>R g x)" "integrable M g" "f \<in> borel_measurable F"
shows "integrable M (\<lambda>x. f x *\<^sub>R cond_exp M F g x)"
"AE x in M. cond_exp M F (\<lambda>x. f x *\<^sub>R g x) x = f x *\<^sub>R cond_exp M F g x"
proof -
let ?F = "restr_to_subalg M F"
have subalg': "subalgebra M (restr_to_subalg M F)" by (metis sets_eq_imp_space_eq sets_restr_to_subalg subalg subalgebra_def)
{
fix z assume asm[measurable]: "integrable M (\<lambda>x. z x *\<^sub>R g x)" "z \<in> borel_measurable ?F"
hence asm'[measurable]: "z \<in> borel_measurable F" using measurable_in_subalg' subalg by blast
have "integrable M (\<lambda>x. z x *\<^sub>R cond_exp M F g x)" "LINT x|M. z x *\<^sub>R g x = LINT x|M. z x *\<^sub>R cond_exp M F g x"
proof -
obtain s where s_is: "\<And>i. simple_function ?F (s i)" "\<And>x. x \<in> space ?F \<Longrightarrow> (\<lambda>i. s i x) \<longlonglongrightarrow> z x" "\<And>i x. x \<in> space ?F \<Longrightarrow> norm (s i x) \<le> 2 * norm (z x)" using borel_measurable_implies_sequence_metric[OF asm(2), of 0] by force
text \<open>We need to apply the dominated convergence theorem twice, therefore we need to show the following prerequisites.\<close>
have s_scaleR_g_tendsto: "AE x in M. (\<lambda>i. s i x *\<^sub>R g x) \<longlonglongrightarrow> z x *\<^sub>R g x" using s_is(2) by (simp add: space_restr_to_subalg tendsto_scaleR)
have s_scaleR_cond_exp_g_tendsto: "AE x in ?F. (\<lambda>i. s i x *\<^sub>R cond_exp M F g x) \<longlonglongrightarrow> z x *\<^sub>R cond_exp M F g x" using s_is(2) by (simp add: tendsto_scaleR)
have s_scaleR_g_meas: "(\<lambda>x. s i x *\<^sub>R g x) \<in> borel_measurable M" for i using s_is(1)[THEN borel_measurable_simple_function, THEN subalg'[THEN measurable_from_subalg]] by simp
have s_scaleR_cond_exp_g_meas: "(\<lambda>x. s i x *\<^sub>R cond_exp M F g x) \<in> borel_measurable ?F" for i using s_is(1)[THEN borel_measurable_simple_function] measurable_in_subalg[OF subalg borel_measurable_cond_exp] by (fastforce intro: borel_measurable_scaleR)
have s_scaleR_g_AE_bdd: "AE x in M. norm (s i x *\<^sub>R g x) \<le> 2 * norm (z x *\<^sub>R g x)" for i using s_is(3) by (fastforce simp add: space_restr_to_subalg mult.assoc[symmetric] mult_right_mono)
{
fix i
have asm: "integrable M (\<lambda>x. norm (z x) * norm (g x))" using asm(1)[THEN integrable_norm] by simp
have "AE x in ?F. norm (s i x *\<^sub>R cond_exp M F g x) \<le> 2 * norm (z x) * norm (cond_exp M F g x)" using s_is(3) by (fastforce simp add: mult_mono)
moreover have "AE x in ?F. norm (z x) * cond_exp M F (\<lambda>x. norm (g x)) x = cond_exp M F (\<lambda>x. norm (z x) * norm (g x)) x" by (rule cond_exp_measurable_mult(2)[THEN AE_symmetric, OF asm integrable_norm, OF assms(2), THEN AE_restr_to_subalg2[OF subalg]], auto)
ultimately have "AE x in ?F. norm (s i x *\<^sub>R cond_exp M F g x) \<le> 2 * cond_exp M F (\<lambda>x. norm (z x *\<^sub>R g x)) x" using cond_exp_contraction[OF assms(2), THEN AE_restr_to_subalg2[OF subalg]] order_trans[OF _ mult_mono] by fastforce
}
note s_scaleR_cond_exp_g_AE_bdd = this
text \<open>In the following section we need to pay attention to which measures we are using for integration. The rhs is F-measurable while the lhs is only M-measurable.\<close>
{
fix i
have s_meas_M[measurable]: "s i \<in> borel_measurable M" by (meson borel_measurable_simple_function measurable_from_subalg s_is(1) subalg')
have s_meas_F[measurable]: "s i \<in> borel_measurable F" by (meson borel_measurable_simple_function measurable_in_subalg' s_is(1) subalg)
have s_scaleR_eq: "s i x *\<^sub>R h x = (\<Sum>y\<in>s i ` space M. (indicator (s i -` {y} \<inter> space M) x *\<^sub>R y) *\<^sub>R h x)" if "x \<in> space M" for x and h :: "'a \<Rightarrow> 'b" using simple_function_indicator_representation[OF s_is(1), of x i] that unfolding space_restr_to_subalg scaleR_left.sum[of _ _ "h x", symmetric] by presburger
have "LINT x|M. s i x *\<^sub>R g x = LINT x|M. (\<Sum>y\<in>s i ` space M. indicator (s i -` {y} \<inter> space M) x *\<^sub>R y *\<^sub>R g x)" using s_scaleR_eq by (intro Bochner_Integration.integral_cong) auto
also have "... = (\<Sum>y\<in>s i ` space M. LINT x|M. indicator (s i -` {y} \<inter> space M) x *\<^sub>R y *\<^sub>R g x)" by (intro Bochner_Integration.integral_sum integrable_mult_indicator[OF _ integrable_scaleR_right] assms(2)) simp
also have "... = (\<Sum>y\<in>s i ` space M. y *\<^sub>R set_lebesgue_integral M (s i -` {y} \<inter> space M) g)" by (simp only: set_lebesgue_integral_def[symmetric]) simp
also have "... = (\<Sum>y\<in>s i ` space M. y *\<^sub>R set_lebesgue_integral M (s i -` {y} \<inter> space M) (cond_exp M F g))" using assms(2) subalg borel_measurable_vimage[OF s_meas_F] by (subst cond_exp_set_integral, auto simp add: subalgebra_def)
also have "... = (\<Sum>y\<in>s i ` space M. LINT x|M. indicator (s i -` {y} \<inter> space M) x *\<^sub>R y *\<^sub>R cond_exp M F g x)" by (simp only: set_lebesgue_integral_def[symmetric]) simp
also have "... = LINT x|M. (\<Sum>y\<in>s i ` space M. indicator (s i -` {y} \<inter> space M) x *\<^sub>R y *\<^sub>R cond_exp M F g x)" by (intro Bochner_Integration.integral_sum[symmetric] integrable_mult_indicator[OF _ integrable_scaleR_right]) auto
also have "... = LINT x|M. s i x *\<^sub>R cond_exp M F g x" using s_scaleR_eq by (intro Bochner_Integration.integral_cong) auto
finally have "LINT x|M. s i x *\<^sub>R g x = LINT x|?F. s i x *\<^sub>R cond_exp M F g x" by (simp add: integral_subalgebra2[OF subalg])
}
note integral_s_eq = this
text \<open>Now we just plug in the results we obtained into DCT, and use the fact that limits are unique.\<close>
show "integrable M (\<lambda>x. z x *\<^sub>R cond_exp M F g x)" using s_scaleR_cond_exp_g_meas asm(2) borel_measurable_cond_exp' by (intro integrable_from_subalg[OF subalg] integrable_cond_exp integrable_dominated_convergence[OF _ _ _ s_scaleR_cond_exp_g_tendsto s_scaleR_cond_exp_g_AE_bdd]) (auto intro: measurable_from_subalg[OF subalg] integrable_in_subalg measurable_in_subalg subalg)
have "(\<lambda>i. LINT x|M. s i x *\<^sub>R g x) \<longlonglongrightarrow> LINT x|M. z x *\<^sub>R g x" using s_scaleR_g_meas asm(1)[THEN integrable_norm] asm' borel_measurable_cond_exp' by (intro integral_dominated_convergence[OF _ _ _ s_scaleR_g_tendsto s_scaleR_g_AE_bdd]) (auto intro: measurable_from_subalg[OF subalg])
moreover have "(\<lambda>i. LINT x|?F. s i x *\<^sub>R cond_exp M F g x) \<longlonglongrightarrow> LINT x|?F. z x *\<^sub>R cond_exp M F g x" using s_scaleR_cond_exp_g_meas asm(2) borel_measurable_cond_exp' by (intro integral_dominated_convergence[OF _ _ _ s_scaleR_cond_exp_g_tendsto s_scaleR_cond_exp_g_AE_bdd]) (auto intro: measurable_from_subalg[OF subalg] integrable_in_subalg measurable_in_subalg subalg)
ultimately show "LINT x|M. z x *\<^sub>R g x = LINT x|M. z x *\<^sub>R cond_exp M F g x" using integral_s_eq using subalg by (simp add: LIMSEQ_unique integral_subalgebra2)
qed
}
note * = this
text \<open>The main statement now follows with \<^term>\<open>z = (\<lambda>x. indicator A x * f x)\<close>.\<close>
show "integrable M (\<lambda>x. f x *\<^sub>R cond_exp M F g x)" using * assms measurable_in_subalg[OF subalg] by blast
{
fix A assume asm: "A \<in> F"
hence "integrable M (\<lambda>x. indicat_real A x *\<^sub>R f x *\<^sub>R g x)" using subalg by (fastforce simp add: subalgebra_def intro!: integrable_mult_indicator assms(1))
hence "set_lebesgue_integral M A (\<lambda>x. f x *\<^sub>R g x) = set_lebesgue_integral M A (\<lambda>x. f x *\<^sub>R cond_exp M F g x)" unfolding set_lebesgue_integral_def using asm by (auto intro!: * measurable_in_subalg[OF subalg])
}
thus "AE x in M. cond_exp M F (\<lambda>x. f x *\<^sub>R g x) x = f x *\<^sub>R cond_exp M F g x" using borel_measurable_cond_exp by (intro cond_exp_charact, auto intro!: * assms measurable_in_subalg[OF subalg])
qed
lemma cond_exp_sum [intro, simp]:
fixes f :: "'t \<Rightarrow> 'a \<Rightarrow> 'b :: {second_countable_topology,banach}"
assumes [measurable]: "\<And>i. integrable M (f i)"
shows "AE x in M. cond_exp M F (\<lambda>x. \<Sum>i\<in>I. f i x) x = (\<Sum>i\<in>I. cond_exp M F (f i) x)"
proof (rule has_cond_exp_charact, intro has_cond_expI')
fix A assume [measurable]: "A \<in> sets F"
then have A_meas [measurable]: "A \<in> sets M" by (meson subsetD subalg subalgebra_def)
have "(\<integral>x\<in>A. (\<Sum>i\<in>I. f i x)\<partial>M) = (\<integral>x. (\<Sum>i\<in>I. indicator A x *\<^sub>R f i x)\<partial>M)" unfolding set_lebesgue_integral_def by (simp add: scaleR_sum_right)
also have "... = (\<Sum>i\<in>I. (\<integral>x. indicator A x *\<^sub>R f i x \<partial>M))" using assms by (auto intro!: Bochner_Integration.integral_sum integrable_mult_indicator)
also have "... = (\<Sum>i\<in>I. (\<integral>x. indicator A x *\<^sub>R cond_exp M F (f i) x \<partial>M))" using cond_exp_set_integral[OF assms] by (simp add: set_lebesgue_integral_def)
also have "... = (\<integral>x. (\<Sum>i\<in>I. indicator A x *\<^sub>R cond_exp M F (f i) x)\<partial>M)" using assms by (auto intro!: Bochner_Integration.integral_sum[symmetric] integrable_mult_indicator)
also have "... = (\<integral>x\<in>A. (\<Sum>i\<in>I. cond_exp M F (f i) x)\<partial>M)" unfolding set_lebesgue_integral_def by (simp add: scaleR_sum_right)
finally show "(\<integral>x\<in>A. (\<Sum>i\<in>I. f i x)\<partial>M) = (\<integral>x\<in>A. (\<Sum>i\<in>I. cond_exp M F (f i) x)\<partial>M)" by auto
qed (auto simp add: assms integrable_cond_exp)
subsection \<open>Linearly Ordered Banach Spaces\<close>
text \<open>In this subsection we show monotonicity results concerning the conditional expectation operator.\<close>
lemma cond_exp_gr_c:
fixes f :: "'a \<Rightarrow> 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
assumes "integrable M f" "AE x in M. f x > c"
shows "AE x in M. cond_exp M F f x > c"
proof -
define X where "X = {x \<in> space M. cond_exp M F f x \<le> c}"
have [measurable]: "X \<in> sets F" unfolding X_def by measurable (metis sets.top subalg subalgebra_def)
hence X_in_M: "X \<in> sets M" using sets_restr_to_subalg subalg subalgebra_def by blast
have "emeasure M X = 0"
proof (rule ccontr)
assume "emeasure M X \<noteq> 0"
have "emeasure (restr_to_subalg M F) X = emeasure M X" by (simp add: emeasure_restr_to_subalg subalg)
hence "emeasure (restr_to_subalg M F) X > 0" using \<open>\<not>(emeasure M X) = 0\<close> gr_zeroI by auto
then obtain A where A: "A \<in> sets (restr_to_subalg M F)" "A \<subseteq> X" "emeasure (restr_to_subalg M F) A > 0" "emeasure (restr_to_subalg M F) A < \<infinity>"
using sigma_fin_subalg by (metis emeasure_notin_sets ennreal_0 infinity_ennreal_def le_less_linear neq_top_trans not_gr_zero order_refl sigma_finite_measure.approx_PInf_emeasure_with_finite)
hence [simp]: "A \<in> sets F" using subalg sets_restr_to_subalg by blast
hence A_in_sets_M[simp]: "A \<in> sets M" using sets_restr_to_subalg subalg subalgebra_def by blast
have [simp]: "set_integrable M A (\<lambda>x. c)" using A subalg by (auto simp add: set_integrable_def emeasure_restr_to_subalg)
have [simp]: "set_integrable M A f" unfolding set_integrable_def by (rule integrable_mult_indicator, auto simp add: assms(1))
have "AE x in M. indicator A x *\<^sub>R c = indicator A x *\<^sub>R f x"
proof (rule integral_eq_mono_AE_eq_AE)
have "(\<integral>x\<in>A. c \<partial>M) \<le> (\<integral>x\<in>A. f x \<partial>M)" using assms(2) by (intro set_integral_mono_AE_banach) auto
moreover
{
have "(\<integral>x\<in>A. f x \<partial>M) = (\<integral>x\<in>A. cond_exp M F f x \<partial>M)" by (rule cond_exp_set_integral, auto simp add: assms)
also have "... \<le> (\<integral>x\<in>A. c \<partial>M)" using A by (auto intro!: set_integral_mono_banach simp add: X_def)
finally have "(\<integral>x\<in>A. f x \<partial>M) \<le> (\<integral>x\<in>A. c \<partial>M)" by simp
}
ultimately show "LINT x|M. indicator A x *\<^sub>R c = LINT x|M. indicator A x *\<^sub>R f x" unfolding set_lebesgue_integral_def by simp
show "AE x in M. indicator A x *\<^sub>R c \<le> indicator A x *\<^sub>R f x" using assms by (auto simp add: X_def indicator_def)
qed (auto simp add: set_integrable_def[symmetric])
hence "AE x\<in>A in M. c = f x" by auto
hence "AE x\<in>A in M. False" using assms(2) by auto
hence "A \<in> null_sets M" using AE_iff_null_sets A_in_sets_M by metis
thus False using A(3) by (simp add: emeasure_restr_to_subalg null_setsD1 subalg)
qed
thus ?thesis using AE_iff_null_sets[OF X_in_M] unfolding X_def by auto
qed
corollary cond_exp_less_c:
fixes f :: "'a \<Rightarrow> 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
assumes "integrable M f" "AE x in M. f x < c"
shows "AE x in M. cond_exp M F f x < c"
proof -
have "AE x in M. cond_exp M F f x = - cond_exp M F (\<lambda>x. - f x) x" using cond_exp_uminus[OF assms(1)] by auto
moreover have "AE x in M. cond_exp M F (\<lambda>x. - f x) x > - c" using assms by (intro cond_exp_gr_c) auto
ultimately show ?thesis by (force simp add: minus_less_iff)
qed
lemma cond_exp_mono_strict:
fixes f :: "'a \<Rightarrow> 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
assumes "integrable M f" "integrable M g" "AE x in M. f x < g x"
shows "AE x in M. cond_exp M F f x < cond_exp M F g x"
using cond_exp_less_c[OF Bochner_Integration.integrable_diff, OF assms(1,2), of 0]
cond_exp_diff[OF assms(1,2)] assms(3) by auto
lemma cond_exp_ge_c:
fixes f :: "'a \<Rightarrow> 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
assumes [measurable]: "integrable M f"
and "AE x in M. f x \<ge> c"
shows "AE x in M. cond_exp M F f x \<ge> c"
proof -
let ?F = "restr_to_subalg M F"
interpret sigma_finite_measure "restr_to_subalg M F" using sigma_fin_subalg by auto
{
fix A assume asm: "A \<in> sets ?F" "0 < measure ?F A"
have [simp]: "sets ?F = sets F" "measure ?F A = measure M A" using asm by (auto simp add: measure_def sets_restr_to_subalg[OF subalg] emeasure_restr_to_subalg[OF subalg])
have M_A: "emeasure M A < \<infinity>" using measure_zero_top asm by (force simp add: top.not_eq_extremum)
hence F_A: "emeasure ?F A < \<infinity>" using asm(1) emeasure_restr_to_subalg subalg by fastforce
have "set_lebesgue_integral M A (\<lambda>_. c) \<le> set_lebesgue_integral M A f" using assms asm M_A subalg by (intro set_integral_mono_AE_banach, auto simp add: set_integrable_def integrable_mult_indicator subalgebra_def sets_restr_to_subalg)
also have "... = set_lebesgue_integral M A (cond_exp M F f)" using cond_exp_set_integral[OF assms(1)] asm by auto
also have "... = set_lebesgue_integral ?F A (cond_exp M F f)" unfolding set_lebesgue_integral_def using asm borel_measurable_cond_exp by (intro integral_subalgebra2[OF subalg, symmetric], simp)
finally have "(1 / measure ?F A) *\<^sub>R set_lebesgue_integral ?F A (cond_exp M F f) \<in> {c..}" using asm subalg M_A by (auto simp add: set_integral_const subalgebra_def intro!: pos_divideR_le_eq[THEN iffD1])
}
thus ?thesis using AE_restr_to_subalg[OF subalg] averaging_theorem[OF integrable_in_subalg closed_atLeast, OF subalg borel_measurable_cond_exp integrable_cond_exp] by auto
qed
corollary cond_exp_le_c:
fixes f :: "'a \<Rightarrow> 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
assumes "integrable M f"
and "AE x in M. f x \<le> c"
shows "AE x in M. cond_exp M F f x \<le> c"
proof -
have "AE x in M. cond_exp M F f x = - cond_exp M F (\<lambda>x. - f x) x" using cond_exp_uminus[OF assms(1)] by force
moreover have "AE x in M. cond_exp M F (\<lambda>x. - f x) x \<ge> - c" using assms by (intro cond_exp_ge_c) auto
ultimately show ?thesis by (force simp add: minus_le_iff)
qed
corollary cond_exp_mono:
fixes f :: "'a \<Rightarrow> 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
assumes "integrable M f" "integrable M g" "AE x in M. f x \<le> g x"
shows "AE x in M. cond_exp M F f x \<le> cond_exp M F g x"
using cond_exp_le_c[OF Bochner_Integration.integrable_diff, OF assms(1,2), of 0]
cond_exp_diff[OF assms(1,2)] assms(3) by auto
corollary cond_exp_min:
fixes f :: "'a \<Rightarrow> 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
assumes "integrable M f" "integrable M g"
shows "AE \<xi> in M. cond_exp M F (\<lambda>x. min (f x) (g x)) \<xi> \<le> min (cond_exp M F f \<xi>) (cond_exp M F g \<xi>)"
proof -
have "AE \<xi> in M. cond_exp M F (\<lambda>x. min (f x) (g x)) \<xi> \<le> cond_exp M F f \<xi>" by (intro cond_exp_mono integrable_min assms, simp)
moreover have "AE \<xi> in M. cond_exp M F (\<lambda>x. min (f x) (g x)) \<xi> \<le> cond_exp M F g \<xi>" by (intro cond_exp_mono integrable_min assms, simp)
ultimately show "AE \<xi> in M. cond_exp M F (\<lambda>x. min (f x) (g x)) \<xi> \<le> min (cond_exp M F f \<xi>) (cond_exp M F g \<xi>)" by fastforce
qed
corollary cond_exp_max:
fixes f :: "'a \<Rightarrow> 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
assumes "integrable M f" "integrable M g"
shows "AE \<xi> in M. cond_exp M F (\<lambda>x. max (f x) (g x)) \<xi> \<ge> max (cond_exp M F f \<xi>) (cond_exp M F g \<xi>)"
proof -
have "AE \<xi> in M. cond_exp M F (\<lambda>x. max (f x) (g x)) \<xi> \<ge> cond_exp M F f \<xi>" by (intro cond_exp_mono integrable_max assms, simp)
moreover have "AE \<xi> in M. cond_exp M F (\<lambda>x. max (f x) (g x)) \<xi> \<ge> cond_exp M F g \<xi>" by (intro cond_exp_mono integrable_max assms, simp)
ultimately show "AE \<xi> in M. cond_exp M F (\<lambda>x. max (f x) (g x)) \<xi> \<ge> max (cond_exp M F f \<xi>) (cond_exp M F g \<xi>)" by fastforce
qed
corollary cond_exp_inf:
fixes f :: "'a \<Rightarrow> 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector, lattice}"
assumes "integrable M f" "integrable M g"
shows "AE \<xi> in M. cond_exp M F (\<lambda>x. inf (f x) (g x)) \<xi> \<le> inf (cond_exp M F f \<xi>) (cond_exp M F g \<xi>)"
unfolding inf_min using assms by (rule cond_exp_min)
corollary cond_exp_sup:
fixes f :: "'a \<Rightarrow> 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector, lattice}"
assumes "integrable M f" "integrable M g"
shows "AE \<xi> in M. cond_exp M F (\<lambda>x. sup (f x) (g x)) \<xi> \<ge> sup (cond_exp M F f \<xi>) (cond_exp M F g \<xi>)"
unfolding sup_max using assms by (rule cond_exp_max)
end
subsection \<open>Probability Spaces\<close>
lemma (in prob_space) sigma_finite_subalgebra_restr_to_subalg:
assumes "subalgebra M F"
shows "sigma_finite_subalgebra M F"
proof (intro sigma_finite_subalgebra.intro)
interpret F: prob_space "restr_to_subalg M F" using assms prob_space_restr_to_subalg prob_space_axioms by blast
show "sigma_finite_measure (restr_to_subalg M F)" by (rule F.sigma_finite_measure_axioms)
qed (rule assms)
lemma (in prob_space) cond_exp_trivial:
fixes f :: "'a \<Rightarrow> 'b :: {second_countable_topology, banach}"
assumes "integrable M f"
shows "AE x in M. cond_exp M (sigma (space M) {}) f x = expectation f"
proof -
interpret sigma_finite_subalgebra M "sigma (space M) {}" by (auto intro: sigma_finite_subalgebra_restr_to_subalg simp add: subalgebra_def sigma_sets_empty_eq)
show ?thesis using assms by (intro cond_exp_charact) (auto simp add: sigma_sets_empty_eq set_lebesgue_integral_def prob_space cong: Bochner_Integration.integral_cong)
qed
text \<open>The following lemma shows that independent \<open>\<sigma>\<close>-algebras don't matter for the conditional expectation. The proof is adapted from \cite{Zitkovic_2015}.\<close>
lemma (in prob_space) cond_exp_indep_subalgebra:
fixes f :: "'a \<Rightarrow> 'b :: {second_countable_topology, banach, real_normed_field}"
assumes subalgebra: "subalgebra M F" "subalgebra M G"
and independent: "indep_set G (sigma (space M) (F \<union> vimage_algebra (space M) f borel))"
assumes [measurable]: "integrable M f"
shows "AE x in M. cond_exp M (sigma (space M) (F \<union> G)) f x = cond_exp M F f x"
proof -
interpret Un_sigma: sigma_finite_subalgebra M "sigma (space M) (F \<union> G)" using assms(1,2) by (auto intro!: sigma_finite_subalgebra_restr_to_subalg sets.sigma_sets_subset simp add: subalgebra_def space_measure_of_conv sets_measure_of_conv)
interpret sigma_finite_subalgebra M F using assms by (auto intro: sigma_finite_subalgebra_restr_to_subalg)
{
fix A
assume asm: "A \<in> sigma (space M) {a \<inter> b | a b. a \<in> F \<and> b \<in> G}"
have in_events: "sigma_sets (space M) {a \<inter> b |a b. a \<in> sets F \<and> b \<in> sets G} \<subseteq> events" using subalgebra by (intro sets.sigma_sets_subset, auto simp add: subalgebra_def)
have "Int_stable {a \<inter> b | a b. a \<in> F \<and> b \<in> G}"
proof -
{
fix af bf ag bg
assume F: "af \<in> F" "bf \<in> F" and G: "ag \<in> G" "bg \<in> G"
have "af \<inter> bf \<in> F" by (intro sets.Int F)
moreover have "ag \<inter> bg \<in> G" by (intro sets.Int G)
ultimately have "\<exists>a b. af \<inter> ag \<inter> (bf \<inter> bg) = a \<inter> b \<and> a \<in> sets F \<and> b \<in> sets G" by (metis inf_assoc inf_left_commute)
}
thus ?thesis by (force intro!: Int_stableI)
qed
moreover have "{a \<inter> b | a b. a \<in> F \<and> b \<in> G} \<subseteq> Pow (space M)" using subalgebra by (force simp add: subalgebra_def dest: sets.sets_into_space)
moreover have "A \<in> sigma_sets (space M) {a \<inter> b | a b. a \<in> F \<and> b \<in> G}" using calculation asm by force
ultimately have "set_lebesgue_integral M A f = set_lebesgue_integral M A (cond_exp M F f)"
proof (induction rule: sigma_sets_induct_disjoint)
case (basic A)
then obtain a b where A: "A = a \<inter> b" "a \<in> F" "b \<in> G" by blast
hence events[measurable]: "a \<in> events" "b \<in> events" using subalgebra by (auto simp add: subalgebra_def)
have [simp]: "sigma_sets (space M) {indicator b -` A \<inter> space M |A. A \<in> borel} \<subseteq> G"
using borel_measurable_indicator[OF A(3), THEN measurable_sets] sets.top subalgebra
by (intro sets.sigma_sets_subset') (fastforce simp add: subalgebra_def)+
have Un_in_sigma: "F \<union> vimage_algebra (space M) f borel \<subseteq> sigma (space M) (F \<union> vimage_algebra (space M) f borel)" by (metis equalityE le_supI sets.space_closed sigma_le_sets space_vimage_algebra subalg subalgebra_def)
have [intro]: "indep_var borel (indicator b) borel (\<lambda>\<omega>. indicator a \<omega> *\<^sub>R f \<omega>)"
proof -
have [simp]: "sigma_sets (space M) {(\<lambda>\<omega>. indicator a \<omega> *\<^sub>R f \<omega>) -` A \<inter> space M |A. A \<in> borel} \<subseteq> sigma (space M) (F \<union> vimage_algebra (space M) f borel)"
proof -
have *: "(\<lambda>\<omega>. indicator a \<omega> *\<^sub>R f \<omega>) \<in> borel_measurable (sigma (space M) (F \<union> vimage_algebra (space M) f borel))"
using borel_measurable_indicator[OF A(2), THEN measurable_sets, OF borel_open] subalgebra
by (intro borel_measurable_scaleR borel_measurableI Un_in_sigma[THEN subsetD])
(auto simp add: space_measure_of_conv subalgebra_def sets_vimage_algebra2)
thus ?thesis using measurable_sets[OF *] by (intro sets.sigma_sets_subset', auto simp add: space_measure_of_conv)
qed
have "indep_set (sigma_sets (space M) {indicator b -` A \<inter> space M |A. A \<in> borel}) (sigma_sets (space M) {(\<lambda>\<omega>. indicator a \<omega> *\<^sub>R f \<omega>) -` A \<inter> space M |A. A \<in> borel})"
using independent unfolding indep_set_def by (rule indep_sets_mono_sets, auto split: bool.split)
thus ?thesis by (subst indep_var_eq, auto intro!: borel_measurable_scaleR)
qed
have [intro]: "indep_var borel (indicator b) borel (\<lambda>\<omega>. indicat_real a \<omega> *\<^sub>R cond_exp M F f \<omega>)"
proof -
have [simp]:"sigma_sets (space M) {(\<lambda>\<omega>. indicator a \<omega> *\<^sub>R cond_exp M F f \<omega>) -` A \<inter> space M |A. A \<in> borel} \<subseteq> sigma (space M) (F \<union> vimage_algebra (space M) f borel)"
proof -
have *: "(\<lambda>\<omega>. indicator a \<omega> *\<^sub>R cond_exp M F f \<omega>) \<in> borel_measurable (sigma (space M) (F \<union> vimage_algebra (space M) f borel))"
using borel_measurable_indicator[OF A(2), THEN measurable_sets, OF borel_open] subalgebra
borel_measurable_cond_exp[THEN measurable_sets, OF borel_open, of _ M F f]
by (intro borel_measurable_scaleR borel_measurableI Un_in_sigma[THEN subsetD])
(auto simp add: space_measure_of_conv subalgebra_def)
thus ?thesis using measurable_sets[OF *] by (intro sets.sigma_sets_subset', auto simp add: space_measure_of_conv)
qed
have "indep_set (sigma_sets (space M) {indicator b -` A \<inter> space M |A. A \<in> borel}) (sigma_sets (space M) {(\<lambda>\<omega>. indicator a \<omega> *\<^sub>R cond_exp M F f \<omega>) -` A \<inter> space M |A. A \<in> borel})"
using independent unfolding indep_set_def by (rule indep_sets_mono_sets, auto split: bool.split)
thus ?thesis by (subst indep_var_eq, auto intro!: borel_measurable_scaleR)
qed
have "set_lebesgue_integral M A f = (LINT x|M. indicator b x * (indicator a x *\<^sub>R f x))"
unfolding set_lebesgue_integral_def A indicator_inter_arith
by (intro Bochner_Integration.integral_cong, auto simp add: scaleR_scaleR[symmetric] indicator_times_eq_if(1))
also have "... = (LINT x|M. indicator b x) * (LINT x|M. indicator a x *\<^sub>R f x)"
by (intro indep_var_lebesgue_integral
Bochner_Integration.integrable_bound[OF integrable_const[of "1 :: 'b"] borel_measurable_indicator]
integrable_mult_indicator[OF _ assms(4)], blast) (auto simp add: indicator_def)
also have "... = (LINT x|M. indicator b x) * (LINT x|M. indicator a x *\<^sub>R cond_exp M F f x)"
using cond_exp_set_integral[OF assms(4) A(2)] unfolding set_lebesgue_integral_def by argo
also have "... = (LINT x|M. indicator b x * (indicator a x *\<^sub>R cond_exp M F f x))"
by (intro indep_var_lebesgue_integral[symmetric]
Bochner_Integration.integrable_bound[OF integrable_const[of "1 :: 'b"] borel_measurable_indicator]
integrable_mult_indicator[OF _ integrable_cond_exp], blast) (auto simp add: indicator_def)
also have "... = set_lebesgue_integral M A (cond_exp M F f)"
unfolding set_lebesgue_integral_def A indicator_inter_arith
by (intro Bochner_Integration.integral_cong, auto simp add: scaleR_scaleR[symmetric] indicator_times_eq_if(1))
finally show ?case .
next
case empty
then show ?case unfolding set_lebesgue_integral_def by simp
next
case (compl A)
have A_in_space: "A \<subseteq> space M" using compl using in_events sets.sets_into_space by blast
have "set_lebesgue_integral M (space M - A) f = set_lebesgue_integral M (space M - A \<union> A) f - set_lebesgue_integral M A f"
using compl(1) in_events
by (subst set_integral_Un[of "space M - A" A], blast)
(simp | intro integrable_mult_indicator[folded set_integrable_def, OF _ assms(4)], fast)+
also have "... = set_lebesgue_integral M (space M - A \<union> A) (cond_exp M F f) - set_lebesgue_integral M A (cond_exp M F f)"
using cond_exp_set_integral[OF assms(4) sets.top] compl subalgebra by (simp add: subalgebra_def Un_absorb2[OF A_in_space])
also have "... = set_lebesgue_integral M (space M - A) (cond_exp M F f)"
using compl(1) in_events
by (subst set_integral_Un[of "space M - A" A], blast)
(simp | intro integrable_mult_indicator[folded set_integrable_def, OF _ integrable_cond_exp], fast)+
finally show ?case .
next
case (union A)
have "set_lebesgue_integral M (\<Union> (range A)) f = (\<Sum>i. set_lebesgue_integral M (A i) f)"
using union in_events
by (intro lebesgue_integral_countable_add) (auto simp add: disjoint_family_onD intro!: integrable_mult_indicator[folded set_integrable_def, OF _ assms(4)])
also have "... = (\<Sum>i. set_lebesgue_integral M (A i) (cond_exp M F f))" using union by presburger
also have "... = set_lebesgue_integral M (\<Union> (range A)) (cond_exp M F f)"
using union in_events
by (intro lebesgue_integral_countable_add[symmetric]) (auto simp add: disjoint_family_onD intro!: integrable_mult_indicator[folded set_integrable_def, OF _ integrable_cond_exp])
finally show ?case .
qed
}
moreover have "sigma (space M) {a \<inter> b | a b. a \<in> F \<and> b \<in> G} = sigma (space M) (F \<union> G)"
proof -
have "sigma_sets (space M) {a \<inter> b |a b. a \<in> sets F \<and> b \<in> sets G} = sigma_sets (space M) (sets F \<union> sets G)"
proof -
{
fix a b assume asm: "a \<in> F" "b \<in> G"
hence "a \<inter> b \<in> sigma_sets (space M) (F \<union> G)" using subalgebra unfolding Int_range_binary by (intro sigma_sets_Inter[OF _ binary_in_sigma_sets]) (force simp add: subalgebra_def dest: sets.sets_into_space)+
}
moreover
{
fix a
assume "a \<in> sets F"
hence "a \<in> sigma_sets (space M) {a \<inter> b |a b. a \<in> sets F \<and> b \<in> sets G}"