Skip to content

Commit 9f6a234

Browse files
affeldt-aistaffeldt-aist
committed
giry monad is symmetric monoidal (done)
1 parent bcecc98 commit 9f6a234

1 file changed

Lines changed: 262 additions & 8 deletions

File tree

  • theories/lebesgue_integral_theory

‎theories/lebesgue_integral_theory/giry.v‎

Lines changed: 262 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,205 @@ Global Hint Extern 0 (_ ≡μ _) => reflexivity : core.
5050
Local Open Scope classical_set_scope.
5151
Local Open Scope ereal_scope.
5252

53+
(* from a PR in progress *)
54+
Definition preimage_display {T T'} : (T -> T') -> measure_display.
55+
Proof. exact. Qed.
56+
57+
Definition g_sigma_algebra_preimageType d' (T : pointedType)
58+
(T' : measurableType d') (f : T -> T') : Type := T.
59+
60+
Definition g_sigma_algebra_preimage d' (T : pointedType)
61+
(T' : measurableType d') (f : T -> T') :=
62+
preimage_set_system setT f (@measurable _ T').
63+
64+
Section preimage_generated_sigma_algebra.
65+
Context {d'} (T : pointedType) (T' : measurableType d').
66+
Variable f : T -> T'.
67+
68+
Let preimage_set0 : g_sigma_algebra_preimage f set0.
69+
Proof.
70+
rewrite /g_sigma_algebra_preimage /preimage_set_system/=.
71+
by exists set0 => //; rewrite preimage_set0 setI0.
72+
Qed.
73+
74+
Let preimage_setC A :
75+
g_sigma_algebra_preimage f A -> g_sigma_algebra_preimage f (~` A).
76+
Proof.
77+
rewrite /g_sigma_algebra_preimage /preimage_set_system/= => -[B mB] <-{A}.
78+
by exists (~` B); [exact: measurableC|rewrite !setTI preimage_setC].
79+
Qed.
80+
81+
Let preimage_bigcup (F : (set T)^nat) :
82+
(forall i, g_sigma_algebra_preimage f (F i)) ->
83+
g_sigma_algebra_preimage f (\bigcup_i (F i)).
84+
Proof.
85+
move=> mF; rewrite /g_sigma_algebra_preimage /preimage_set_system/=.
86+
pose g := fun i => sval (cid2 (mF i)).
87+
pose mg := fun i => svalP (cid2 (mF i)).
88+
exists (\bigcup_i g i).
89+
by apply: bigcup_measurable => k; case: (mg k).
90+
rewrite setTI /g preimage_bigcup; apply: eq_bigcupr => k _.
91+
by case: (mg k) => _; rewrite setTI.
92+
Qed.
93+
94+
HB.instance Definition _ := Pointed.on (g_sigma_algebra_preimageType f).
95+
96+
HB.instance Definition _ := @isMeasurable.Build (preimage_display f)
97+
(g_sigma_algebra_preimageType f) (g_sigma_algebra_preimage f)
98+
preimage_set0 preimage_setC preimage_bigcup.
99+
100+
End preimage_generated_sigma_algebra.
101+
(*/ from a PR in progress *)
102+
103+
Notation "f .-preimage" := (preimage_display f) : measure_display_scope.
104+
Notation "f .-preimage.-measurable" :=
105+
(measurable : set (set (g_sigma_algebra_preimageType f))) : classical_set_scope.
106+
107+
Section rect_cross.
108+
Context {T1 T2 : Type}.
109+
Implicit Types (X : set_system T1) (Y : set_system T2).
110+
111+
Definition rect X Y := [set U `*` V | U in X & V in Y].
112+
113+
Definition cross X Y :=
114+
preimage_set_system setT fst X `|` preimage_set_system setT snd Y.
115+
116+
End rect_cross.
117+
118+
Reserved Notation "A `x` B" (at level 46, left associativity).
119+
Notation "A `x` B" := (cross A B) : classical_set_scope.
120+
121+
Lemma yoneda {T} (A B : set_system T) :
122+
sigma_algebra setT A ->
123+
sigma_algebra setT B ->
124+
(forall Z, sigma_algebra setT Z -> A `<=` Z <-> B `<=` Z)
125+
<->
126+
A = B.
127+
Proof.
128+
move=> sA sB.
129+
split=> [AB|AB]; last by rewrite AB.
130+
by apply/seteqP; split; exact/AB.
131+
Qed.
132+
133+
Lemma preimage_set_system_mon {T1 T2} (A B : set_system T2) (f : T1 -> T2) :
134+
A `<=` B ->
135+
preimage_set_system [set: _] f A `<=` preimage_set_system [set: _] f B.
136+
Proof. by move=> AB _ [C ? <-]; exists C => //; exact: AB. Qed.
137+
138+
Section rect_cross_prop.
139+
Context {T1 T2 T3 : pointedType}.
140+
141+
Definition RR {T : pointedType} (Z : set_system T) : set_system T := <<s Z>>.
142+
143+
Lemma thm4 {T : pointedType} (X Y : set_system T) : sigma_algebra setT Y ->
144+
RR X `<=` Y <-> X `<=` Y.
145+
Proof.
146+
move=> sY.
147+
split=> [RXY|].
148+
clear sY.
149+
apply: subset_trans RXY.
150+
exact: sub_gen_smallest.
151+
exact: smallest_sub.
152+
Qed.
153+
154+
Lemma lem6' (Y : set_system T2) :
155+
preimage_set_system setT (@snd T1 T2) (RR Y) =
156+
RR (preimage_set_system setT snd Y).
157+
Proof.
158+
apply/seteqP; split; last first.
159+
apply/(thm4 _ _).2.
160+
set RY := @g_sigma_algebraType _ Y.
161+
exact: (sigma_algebra_measurable (g_sigma_algebra_preimageType (@snd T1 RY))).
162+
apply: preimage_set_system_mon.
163+
exact: sub_sigma_algebra.
164+
move=> _ [Z RYZ <-].
165+
rewrite /preimage_set_system.
166+
red.
167+
move=> /= G [sigG HG].
168+
pose i := @image_set_system _ T2 setT (@snd _ _) G.
169+
(* TODO: use image_set_system *)
170+
apply: (RYZ i).
171+
split.
172+
by apply: sigma_algebra_image.
173+
move=> A YA.
174+
apply: HG => //.
175+
by exists A.
176+
Qed.
177+
178+
Lemma lem6 (X : set_system T1) (Y : set_system T2) :
179+
RR (X `x` RR Y) = RR (X `x` Y).
180+
Proof.
181+
apply/yoneda; [exact: smallest_sigma_algebra..|].
182+
move => /= Z mZ.
183+
rewrite thm4//=.
184+
rewrite {1}/cross/=.
185+
rewrite subUset.
186+
rewrite lem6'//.
187+
rewrite thm4//=.
188+
rewrite -subUset.
189+
by rewrite -thm4//=.
190+
Qed.
191+
192+
Lemma lem9 (X : set_system T1) (Y : set_system T2) :
193+
X setT ->
194+
Y setT ->
195+
(* sigma_algebra setT X ->
196+
sigma_algebra setT Y ->*)
197+
RR (rect X Y) = RR (X `x` Y).
198+
Proof.
199+
move=> sX sY; apply/seteqP; split; last first.
200+
apply: sub_sigma_algebra2.
201+
move=> A [|].
202+
rewrite /preimage_set_system/= => -[A1 XA1 <-{A}].
203+
rewrite -setXT setTI.
204+
rewrite /rect/=.
205+
exists A1 =>//.
206+
by exists setT => //.
207+
rewrite /preimage_set_system/= => -[A1 XA1 <-{A}].
208+
rewrite -setTX setTI.
209+
rewrite /rect/=.
210+
exists setT => //.
211+
by exists A1.
212+
(* apply: sub_sigma_algebra2. (* TODO: rename that thing!! *) *)
213+
rewrite thm4//; last first.
214+
exact: smallest_sigma_algebra.
215+
move=> _ [A1 X1] [A2 X2] <-.
216+
rewrite /setX.
217+
rewrite (_ : [set z | A1 z.1 /\ A2 z.2] = fst @^-1` A1 `&` snd @^-1` A2)//.
218+
apply: (@measurableI _ (@g_sigma_algebraType _ (X `x` Y))).
219+
- apply: sub_sigma_algebra.
220+
left.
221+
exists A1 => //.
222+
by rewrite setTI.
223+
- apply: sub_sigma_algebra.
224+
right.
225+
exists A2 => //.
226+
by rewrite setTI.
227+
Qed.
228+
229+
End rect_cross_prop.
230+
231+
Section rect_cross_prop2.
232+
Context {T1 T2 T3 : pointedType}.
233+
234+
Lemma lem17 (X : set_system T1) (Y : set_system T2) (Z : set_system T3) :
235+
X setT ->
236+
Y setT ->
237+
Z setT ->
238+
RR (X `x` RR (Y `x` Z)) = RR (rect X (rect Y Z)).
239+
Proof.
240+
move=> mX mY mZ.
241+
rewrite -(lem9 mY mZ).
242+
rewrite lem6.
243+
rewrite -(lem9 mX)//.
244+
red.
245+
exists setT => //.
246+
exists setT => //.
247+
by rewrite setXTT.
248+
Qed.
249+
250+
End rect_cross_prop2.
251+
53252
(* TODO: move *)
54253
Definition fun_pair {X T1 T2} (f : X -> T1) (g : X -> T2)
55254
(x : X) := (f x, g x).
@@ -673,17 +872,72 @@ Lemma giry_monoidal_assoc (xyz : (giry X R * giry Y R) * giry Y' R) :
673872
Proof.
674873
move: xyz => [[x y] z].
675874
move=> U mU.
676-
apply: product_measure_unique => // U1 U2 mU1 mU2.
677-
rewrite /giry_prod /prodA.
678-
transitivity ((x \x (y \x z)) ((U1 `*` U2))); last first.
679-
by rewrite (@product_measure1E _ _ _ _ _ x (product_subprobability (y, z)))//.
875+
red in mU.
876+
simpl in mU.
877+
rewrite /g_sigma_preimageU in mU.
878+
have mU' : RR (@measurable _ X `x` RR (@measurable _ Y `x` @measurable _ Y')) U.
879+
rewrite /RR.
880+
rewrite /cross/=.
881+
done.
882+
rewrite lem17 in mU'; [|exact: measurableT..].
883+
red in mU'.
884+
apply: (measure_unique (rect d1.-measurable (rect d2.-measurable d2'.-measurable)) (fun=> setT)) => //.
885+
rewrite -/(RR (rect _ (rect _ _))).
886+
by rewrite -lem17//.
887+
move=> /= P Q [P1 mP1 [P2 [P3 mP3 [P4 mP4]]]] HP2 Hp.
888+
move=> [Q1 mQ1 [Q2 [Q3 mQ3] [Q4 mQ4]]] HQ2 HQ.
889+
red.
890+
simpl.
891+
rewrite -HQ -Hp.
892+
rewrite -setXI.
893+
exists (P1 `&` Q1).
894+
exact: measurableI.
895+
exists (P2 `&` Q2).
896+
red.
897+
simpl.
898+
rewrite -HQ2 -HP2.
899+
rewrite -setXI.
900+
exists (P3 `&` Q3).
901+
exact: measurableI.
902+
exists (P4 `&` Q4).
903+
exact: measurableI.
904+
done.
905+
done.
906+
move=> _.
680907
rewrite /=.
681-
apply/esym.
682-
apply: (@product_measure_unique _ _ _ _ _ x (product_subprobability (y, z))) => //=; last first.
683-
exact: measurableX.
684-
move=> A B mA mB.
908+
exists setT => //.
909+
exists setT => //.
910+
exists setT => //.
911+
exists setT => //.
912+
by rewrite setXTT.
913+
by rewrite setXTT.
914+
apply: bigcupT => //.
915+
by exists O.
916+
move=> A /=.
917+
case => Q mQ [E].
918+
case => E1 mE1 [E2 mE2] <- <-.
685919
rewrite /pushforward.
920+
rewrite (_ : _ @^-1` _ = ((Q `*` E1) `*` E2)); last first.
921+
by apply/seteqP; split => -[[]]/= *; tauto.
922+
rewrite !product_measure1E//=.
923+
rewrite (@product_measure1E _ _ _ _ _ x (product_subprobability (y, z)))//=.
924+
rewrite !product_measure1E//=.
925+
by rewrite muleA.
926+
exact: measurableX.
927+
exact: measurableX.
928+
by rewrite ltey_eq fin_num_measure.
929+
Qed.
930+
931+
Definition giry_copy (x : X) : giry _ R := giry_ret (x, x).
686932

933+
Definition giry_discard (x : X) : giry _ R := giry_ret tt.
934+
935+
936+
Lemma test (P1 P2 : probability unit R) : P1 ≡μ P2.
937+
Proof.
938+
move=> A mA.
939+
apply: (measure_unique).
687940
Abort.
941+
(* Kleisli category is symmetric monoidal *)
688942

689943
End proj_giry_prod.

0 commit comments

Comments
 (0)