Skip to content

Commit af7caeb

Browse files
affeldt-aistaffeldt-aist
committed
doc until giry_join
1 parent 58f6efa commit af7caeb

2 files changed

Lines changed: 101 additions & 112 deletions

File tree

‎CHANGELOG_UNRELEASED.md‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@
1515

1616
- new file `lebesgue_integral_theory/giry.v`
1717
+ definition `measure_eq`
18+
+ lemma `dynkin_induction`
1819
+ definition `giry`
1920
+ definition `giry_ev`
2021
+ definition `giry_measurable`
@@ -23,6 +24,15 @@
2324
+ lemma `measurable_giry_ev`
2425
+ definition `giry_int`
2526
+ lemma `measurable_giry_int`
27+
+ lemma `measurable_giry_codensity`
28+
+ definition `giry_map`
29+
+ lemma `measurable_giry_map`
30+
+ lemma `giry_int_map`
31+
+ lemma `giry_map_dirac`
32+
+ definition `giry_ret`
33+
+ lemma `measurable_giry_ret`
34+
+ lemma `giry_int_ret`
35+
+ definition `giry_join`
2636

2737
### Changed
2838

‎theories/lebesgue_integral_theory/giry.v‎

Lines changed: 91 additions & 112 deletions
Original file line numberDiff line numberDiff line change
@@ -7,17 +7,25 @@ From mathcomp Require Import lebesgue_measure lebesgue_integral.
77
(**md**************************************************************************)
88
(* # The Giry monad *)
99
(* *)
10+
(* ``` *)
11+
(* m1 ≡μ m2 == m1 S = m2 S for any measurable set S *)
1012
(* giry T R == the type of subprobability measures over T *)
1113
(* giry_ev P A == the evaluation map `giryM T R -> [0, 1]` *)
14+
(* preimg_giry_ev A == preimage of the sigma-algebra of extended real numbers *)
15+
(* via the function giry_ev ^~ A *)
16+
(* giry_measurable == the sigma-algebra generated by the countable unions of *)
17+
(* preimg_giry_ev *)
18+
(* giry_display == display of giry_measurable *)
1219
(* giry_int mu f := \int[mu]_x f x *)
20+
(* giry_map mf == the map of type giry T1 R -> giry T2 R *)
21+
(* where mf is a proof that f : T1 -> T2 is measurable *)
1322
(* giry_ret x == the unit of the Giry monad, i.e., \d_x *)
1423
(* @giry_join _ T R == the multiplication of the Giry monad *)
1524
(* type : giry (giry T R) R -> giry T R *)
16-
(* giry_map mf == the map of type giry T1 R -> giry T2 R *)
17-
(* where mf is a proof that f : T1 -> T2 is measurable *)
1825
(* giry_bind mu mf == the bind with mu : giry T1 R and f : T1 -> giry T2 R *)
1926
(* giry_prod == product of type *)
2027
(* giry T1 R * giry T2 R -> giry (T1 * T2) R *)
28+
(* ``` *)
2129
(* *)
2230
(******************************************************************************)
2331

@@ -27,17 +35,41 @@ Unset Printing Implicit Defensive.
2735

2836
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
2937

30-
(* TODO: PR to measure.v? *)
31-
Section mzero_subprobability.
32-
Context d (T : measurableType d) (R : realType).
33-
34-
Let mzero_setT : (@mzero d T R setT <= 1)%E.
35-
Proof. by rewrite /mzero/=. Qed.
38+
Definition measure_eq {d} {T : measurableType d} {R : realType} :
39+
measure T R -> measure T R -> Prop :=
40+
fun m1 m2 => forall S : set T, measurable S -> m1 S = m2 S.
41+
Notation "x ≡μ y" := (measure_eq x y) (at level 70).
3642

37-
HB.instance Definition _ :=
38-
Measure_isSubProbability.Build _ _ _ (@mzero d T R) mzero_setT.
43+
Global Hint Extern 0 (_ ≡μ _) => reflexivity : core.
3944

40-
End mzero_subprobability.
45+
Local Open Scope classical_set_scope.
46+
(* Adapted from mathlib induction_on_inter *)
47+
(* TODO: change premises to use setX_closed like notations *)
48+
Lemma dynkin_induction d {T : measurableType d} (G : set (set T))
49+
(P : set_system T) :
50+
@measurable _ T = <<s G >> ->
51+
setI_closed G ->
52+
P [set: T] ->
53+
G `<=` P ->
54+
(forall S, measurable S -> P S -> P (~` S)) ->
55+
(forall F : (set T)^nat,
56+
(forall n, measurable (F n)) ->
57+
trivIset setT F ->
58+
(forall n, P (F n)) -> P (\bigcup_k F k)) ->
59+
(forall S, <<s G >> S -> P S).
60+
Proof.
61+
move=> GE GI PsetT GP PsetC Pbigcup A sGA.
62+
suff: <<s G >> `<=` [set A | measurable A /\ P A] by move=> /(_ _ sGA)[].
63+
apply: lambda_system_subset; [by []| | |by []].
64+
- apply/dynkin_lambda_system; split => //.
65+
+ by move=> B [mB PB]; split; [exact: measurableC|exact: PsetC].
66+
+ move=> F tF Hm; split.
67+
by apply: bigcup_measurable => k _; apply Hm.
68+
by apply: Pbigcup => //; apply Hm.
69+
- move=> B GB; split; last exact: GP.
70+
by rewrite GE; exact: sub_gen_smallest.
71+
Qed.
72+
Local Close Scope classical_set_scope.
4173

4274
Section giry_def.
4375
Local Open Scope classical_set_scope.
@@ -74,7 +106,6 @@ HB.instance Definition _ :=
74106
@isMeasurable.Build giry_display giry giry_measurable
75107
giry_measurable0 giry_measurableC giry_measurableU.
76108

77-
(* TODO: Make hint? *)
78109
Lemma measurable_giry_ev (A : set T) : measurable A ->
79110
measurable_fun [set: giry] (giry_ev ^~ A).
80111
Proof.
@@ -88,13 +119,6 @@ Qed.
88119
End giry_def.
89120
Arguments giry_ev {d T R} mu A.
90121

91-
Definition measure_eq {d} {T : measurableType d} {R : realType} :
92-
giry T R -> giry T R -> Prop :=
93-
fun μ1 μ2 => forall S : set T, measurable S -> μ1 S = μ2 S.
94-
Notation "x ≡μ y" := (measure_eq x y) (at level 70).
95-
96-
Global Hint Extern 0 (_ ≡μ _) => reflexivity : core.
97-
98122
Section giry_integral.
99123
Local Open Scope classical_set_scope.
100124
Local Open Scope ereal_scope.
@@ -104,106 +128,59 @@ Definition giry_int (mu : giry T R) (f : T -> \bar R) := \int[mu]_x f x.
104128

105129
Import HBNNSimple.
106130

131+
(**md The idea is to reconstruct f from simple functions, then use measurability
132+
of giry_ev. Reference: Tom Avery. Codensity and the Giry monad.
133+
https://arxiv.org/pdf/1410.4432.
134+
*)
107135
Lemma measurable_giry_int (f : T -> \bar R) :
108136
measurable_fun [set: T] f -> (forall x, 0 <= f x) ->
109137
measurable_fun [set: giry T R] (giry_int ^~ f).
110138
Proof.
111-
(*
112-
The idea is to reconstruct f from simple functions, then use measurability of giry_ev.
113-
Tom Avery. Codensity and the Giry monad. https://arxiv.org/pdf/1410.4432.
114-
*)
115139
move=> mf h0.
116140
pose g := nnsfun_approx measurableT mf.
117-
pose gE := fun n => EFin \o g n.
118-
have mgE n : measurable_fun [set: T] (gE n) by exact/measurable_EFinP.
119-
have gE0 n x : [set: T] x -> 0 <= (gE n) x by rewrite /gE /= // lee_fin.
120-
have HgEmono x : [set: T] x -> {homo gE ^~ x : n m / (n <= m)%O >-> n <= m}.
121-
by move=> _ n m nm; exact/lefP/nd_nnsfun_approx.
122-
(* By MCT, limit of the integrals of g_n is the integral of the limit of g_n *)
123-
have Hcvg := cvg_monotone_convergence _ mgE gE0 HgEmono.
124-
pose gEInt := fun n μ => \int[μ]_x (gE n) x.
125-
have mgEInt n : measurable_fun [set: giry T R] (gEInt n).
126-
rewrite /gEInt /gE /=.
127-
apply (eq_measurable_fun (fun μ : giry T R =>
128-
\sum_(x \in range (g n)) x%:E * μ (g n @^-1` [set x]))).
129-
by move=> μ Hμ; rewrite integralT_nnsfun sintegralE.
130-
apply: emeasurable_fsum => // r.
131-
apply: measurable_funeM.
132-
exact: measurable_giry_ev.
133-
(* The μ ↦ int[mu] lim g_n is measurable if every μ ↦ int[mu] g_n is measurable *)
134-
apply: (emeasurable_fun_cvg _ (fun μ : giry T R => \int[μ]_x f x) mgEInt).
135-
move=> μ Hμ.
136-
rewrite /gEInt /=.
137-
rewrite (eq_integral (fun x : T => limn (gE ^~ x))).
138-
exact: (Hcvg μ measurableT).
139-
move=> x _; apply/esym/cvg_lim => //.
140-
exact/cvg_nnsfun_approx.
141+
pose Eg := fun n => EFin \o g n.
142+
pose intEg := fun n mu => giry_int mu (Eg n).
143+
have mintgE n : measurable_fun [set: giry T R] (intEg n).
144+
rewrite /intEg /giry_int/=.
145+
under eq_fun do rewrite integralT_nnsfun sintegralE.
146+
apply: emeasurable_fsum => //= r.
147+
by apply: measurable_funeM => //=; exact: measurable_giry_ev.
148+
apply: (emeasurable_fun_cvg _ (giry_int ^~ f) mintgE) => mu _.
149+
rewrite (_ : giry_int mu f = \int[mu]_x limn (Eg ^~ x)).
150+
apply: cvg_monotone_convergence => //.
151+
- by move=> n; exact/measurable_EFinP.
152+
- by move=> n x _; rewrite lee_fin.
153+
- by move=> t _ n m nm; apply/lefP/nd_nnsfun_approx.
154+
apply: eq_integral => t _.
155+
by apply/esym/cvg_lim => //; exact/cvg_nnsfun_approx.
141156
Qed.
142157

143158
End giry_integral.
144159
Arguments giry_int {d T R} mu f.
145160

146-
Local Open Scope classical_set_scope.
147-
(* Adapted from mathlib induction_on_inter *)
148-
(* TODO: change premises to use setX_closed like notations *)
149-
Lemma dynkin_induction d {T : measurableType d} (G : set (set T))
150-
(P : set_system T) :
151-
@measurable _ T = <<s G >> ->
152-
setI_closed G ->
153-
P [set: T] ->
154-
G `<=` P ->
155-
(forall S, measurable S -> P S -> P (~` S)) ->
156-
(forall F : (set T)^nat,
157-
(forall n, measurable (F n)) ->
158-
trivIset setT F ->
159-
(forall n, P (F n)) -> P (\bigcup_k F k)) ->
160-
(forall S, <<s G >> S -> P S).
161-
Proof.
162-
move=> GE GI PsetT GP PsetC Pbigcup A sGA.
163-
suff: <<s G >> `<=` [set A | measurable A /\ P A] by move=> /(_ _ sGA)[].
164-
apply: lambda_system_subset; [by []| | |by []].
165-
- apply/dynkin_lambda_system; split => //.
166-
+ by move=> B [mB PB]; split; [exact: measurableC|exact: PsetC].
167-
+ move=> F tF Hm; split.
168-
by apply: bigcup_measurable => k _; apply Hm.
169-
by apply: Pbigcup => //; apply Hm.
170-
- move=> B GB; split; last exact: GP.
171-
by rewrite GE; exact: sub_gen_smallest.
172-
Qed.
173-
Local Close Scope classical_set_scope.
174-
175161
Section measurable_giry_codensity.
176162
Local Open Scope classical_set_scope.
163+
Context d1 {T1 : measurableType d1}.
177164

178-
(* TODO: move this lemma to a more accessible location? *)
179-
Let measurability_image_sub d d' (aT : measurableType d) (rT : measurableType d')
180-
(f : aT -> rT) (G : set (set rT)) :
181-
@measurable _ rT = <<s G >> ->
182-
(forall B, G B -> measurable (f @^-1` B)) ->
183-
measurable_fun [set: aT] f.
165+
Lemma measurable_giry_codensity d2 {T2 : measurableType d2} {R : realType}
166+
(D : set T1) (f : T1 -> giry T2 R) :
167+
measurable D ->
168+
(forall B, measurable B -> measurable_fun D (f ^~ B)) ->
169+
measurable_fun D f.
184170
Proof.
185-
move=> GE Gf; apply/(measurability G) => //.
186-
by apply/image_subP => A /Gf; rewrite setTI.
187-
Qed.
188-
189-
Lemma measurable_giry_codensity {d1} {d2} {T1 : measurableType d1}
190-
{T2 : measurableType d2} {R : realType} (f : T1 -> giry T2 R) :
191-
(forall B, measurable B -> measurable_fun [set: T1] (f ^~ B)) ->
192-
measurable_fun [set: T1] f.
193-
Proof.
194-
move=> mf.
171+
move=> mD mf.
195172
pose G : set_system (giry T2 R) := \bigcup_(B in measurable) preimg_giry_ev B.
196-
apply: (measurability_image_sub (G := G)) => // _ [B mB [Y mY] <-].
197-
exact: mf.
173+
apply: (measurability G) => //= _ [_ [C mC [Z mZ] <-] <-].
174+
by rewrite setTI; exact: mf.
198175
Qed.
199176

200177
End measurable_giry_codensity.
201178

202179
Section giry_map.
203180
Local Open Scope classical_set_scope.
204181
Local Open Scope ereal_scope.
205-
Context {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} {R : realType}.
206-
182+
Context {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2}
183+
{R : realType}.
207184
Variables (f : T1 -> T2) (mf : measurable_fun [set: T1] f) (mu1 : giry T1 R).
208185

209186
Let map := pushforward mu1 f.
@@ -233,19 +210,28 @@ Definition giry_map : giry T2 R := map.
233210

234211
End giry_map.
235212

236-
Section giry_map_meas.
213+
Section giry_map_lemmas.
237214
Local Open Scope classical_set_scope.
238215
Local Open Scope ereal_scope.
239216
Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType).
240217
Implicit Type f : T1 -> T2.
241218

219+
Lemma measurable_giry_map f (mf : measurable_fun [set: T1] f) :
220+
measurable_fun [set: giry T1 R] (giry_map mf).
221+
Proof.
222+
rewrite /giry_map.
223+
apply: measurable_giry_codensity => // B mB.
224+
apply: measurable_giry_ev.
225+
by rewrite -(setTI (f @^-1` B)); exact: mf.
226+
Qed.
227+
242228
Lemma giry_int_map f (mf : measurable_fun [set: T1] f)
243229
(mu : giry T1 R) (h : T2 -> \bar R) :
244230
measurable_fun [set: T2] h -> (forall x, 0 <= h x) ->
245231
giry_int (giry_map mf mu) h = giry_int mu (h \o f).
246232
Proof. by move=> mh h0; exact: ge0_integral_pushforward. Qed.
247233

248-
Lemma giry_mapE f (mf : measurable_fun [set: T1] f)
234+
Lemma giry_map_dirac f (mf : measurable_fun [set: T1] f)
249235
(mu1 : giry T1 R) (B : set T2) : measurable B ->
250236
giry_map mf mu1 B = \int[mu1]_x (\d_(f x))%R B.
251237
Proof.
@@ -255,16 +241,7 @@ rewrite -[in LHS](setIT B) -[LHS]integral_indic// [LHS]giry_int_map//.
255241
by move=> ?; rewrite lee_fin.
256242
Qed.
257243

258-
Lemma measurable_giry_map f (mf : measurable_fun [set: T1] f) :
259-
measurable_fun [set: giry T1 R] (giry_map mf).
260-
Proof.
261-
rewrite /giry_map.
262-
apply: (@measurable_giry_codensity _ _ (giry T1 R)) => B mB.
263-
apply: measurable_giry_ev.
264-
by rewrite -(setTI (f @^-1` B)); exact: mf.
265-
Qed.
266-
267-
End giry_map_meas.
244+
End giry_map_lemmas.
268245

269246
Section giry_ret.
270247
Local Open Scope classical_set_scope.
@@ -275,7 +252,9 @@ Context {d} {T : measurableType d} {R : realType}.
275252
Definition giry_ret (x : T) : giry T R := \d_x.
276253

277254
Lemma measurable_giry_ret : measurable_fun [set: T] giry_ret.
278-
Proof. by apply: measurable_giry_codensity; exact: measurable_fun_dirac. Qed.
255+
Proof.
256+
by apply: measurable_giry_codensity => //; exact: measurable_fun_dirac.
257+
Qed.
279258

280259
Lemma giry_int_ret (x : T) (f : T -> \bar R) : measurable_fun [set: T] f ->
281260
giry_int (giry_ret x) f = f x.
@@ -288,7 +267,7 @@ End giry_ret.
288267
Section giry_join.
289268
Local Open Scope classical_set_scope.
290269
Local Open Scope ereal_scope.
291-
Context d (T : measurableType d) (R : realType).
270+
Context {d} {T : measurableType d} {R : realType}.
292271
Variable M : giry (giry T R) R.
293272

294273
Let join A := giry_int M (giry_ev ^~ A).
@@ -345,7 +324,7 @@ Context {d} {T : measurableType d} {R : realType}.
345324

346325
Lemma measurable_giry_join : measurable_fun [set: giry (giry T R) R] giry_join.
347326
Proof.
348-
apply: measurable_giry_codensity => B mB/=.
327+
apply: measurable_giry_codensity => //= B mB.
349328
by apply: measurable_giry_int => //; exact: measurable_giry_ev.
350329
Qed.
351330

@@ -524,7 +503,7 @@ Qed.
524503
Lemma measurable_giry_prod :
525504
measurable_fun [set: giry T1 R * giry T2 R] giry_prod.
526505
Proof.
527-
apply: measurable_giry_codensity => /=.
506+
apply: measurable_giry_codensity => //=.
528507
rewrite measurable_prod_measurableType.
529508
apply: dynkin_induction => /=.
530509
- by rewrite measurable_prod_measurableType.

0 commit comments

Comments
 (0)