From 53dc49a1e977cf99dbf9c18c7116f9bfc50532c3 Mon Sep 17 00:00:00 2001 From: Alejandro Aguirre Date: Thu, 1 May 2025 17:31:29 +0200 Subject: [PATCH 01/14] Started implementation of Giry monad --- giry.v | 953 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 953 insertions(+) create mode 100644 giry.v diff --git a/giry.v b/giry.v new file mode 100644 index 0000000000..567625e497 --- /dev/null +++ b/giry.v @@ -0,0 +1,953 @@ +From mathcomp Require Import all_ssreflect all_algebra boolp classical_sets functions. +From mathcomp Require Import reals topology separation_axioms ereal sequences measure measurable_realfun lebesgue_measure lebesgue_integral. +(* +From clutch.prob.monad Require Export prelude. +From clutch.prelude Require Import classical. +Import Coq.Relations.Relation_Definitions. +From Coq Require Import Classes.Morphisms Reals. + *) +From HB Require Import structures. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Import Order.TTheory GRing.Theory Num.Def Num.Theory. + +Section giryM_def. +Local Open Scope classical_set_scope. +Context d (T : measurableType d) (R : realType). + + + +Definition giryM : Type := @subprobability d T R. + +Let mzero_setT : (@mzero d T R setT <= 1)%E. +Proof. by rewrite /mzero/=. Qed. + +HB.instance Definition _ := gen_eqMixin giryM. +HB.instance Definition _ := gen_choiceMixin giryM. +HB.instance Definition _ := Measure_isSubProbability.Build _ _ _ (@mzero d T R) mzero_setT. +HB.instance Definition _ := isPointed.Build giryM mzero. + +Definition gEval (S : set T) (mu : giryM) := mu S. +Definition gEvalPreImg (S : set T) := preimage_set_system setT (gEval S) measurable. + +Definition giry_measurable := <>. + +(* Axiom giry_measurable : set (set giryM). *) +Let giry_measurable0 : giry_measurable set0. +Proof. exact: sigma_algebra0. Qed. + +Let giry_measurableC (S : set giryM) : + giry_measurable S -> giry_measurable (~` S). +Proof. exact: sigma_algebraC. Qed. + +Let giry_measurableU (A : (set giryM)^nat) : + (forall i, giry_measurable (A i)) -> giry_measurable (\bigcup_i A i). +Proof. exact: sigma_algebra_bigcup. Qed. + +Definition giry_display : measure_display. +Proof. by constructor. Qed. + +HB.instance Definition _ := + @isMeasurable.Build giry_display giryM giry_measurable + giry_measurable0 giry_measurableC giry_measurableU. + +End giryM_def. + + +Definition measure_eq {d : measure_display} {T : measurableType d} {R : realType} : giryM T R -> giryM T R -> Prop := + fun μ1 μ2 => forall (S : set T), measurable S -> μ1 S = μ2 S. +Notation "x ≡μ y" := (measure_eq x y) (at level 70). +Global Hint Extern 0 (_ ≡μ _) => reflexivity : core. +Global Hint Extern 0 (_ ≡μ _) => symmetry; assumption : core. + +Section giry_eval. + +Local Open Scope ereal_scope. +Local Open Scope classical_set_scope. +Context d (T : measurableType d) (R : realType). + +(* TODO: Make hint *) +Lemma gEval_meas_fun (S : set T) (HmS : d.-measurable S) : measurable_fun [set: giryM T R] (gEval S). +Proof. + apply: (@measurability giry_display _ (@giryM _ T R) _ setT (@gEval _ _ R S)). + rewrite smallest_id; first reflexivity. + exact: sigma_algebra_measurable. + rewrite /giry_display.-measurable /= /giry_measurable /=. + apply: subset_trans; last exact: sub_gen_smallest. + apply: subset_trans; [ | apply bigcup_sup; exact HmS]. + exact: subset_refl. +Qed. + +End giry_eval. + + +Section giry_integral. +Local Open Scope classical_set_scope. +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType). + +Definition gInt (f : T -> \bar R) (mu : giryM T R) := \int[mu]_x f x. + +Import HBNNSimple. + +Lemma gInt_meas_fun (f : T -> \bar R) : + (measurable_fun setT f) -> + (forall x, 0 <= f x) -> + measurable_fun setT (gInt f). +Proof. + (* + The idea is to reconstruct f from simple functions, then use + measurability of gEval. See "Codensity and the Giry monad", Avery + *) + move => Hmf Hge0. + pose g := nnsfun_approx measurableT Hmf. + pose gE := (fun n => EFin \o g n). + have HgEmeas n : measurable_fun [set: T] (gE n). + rewrite /gE /=. + exact/ measurable_EFinP. + have HgEge0 n x : [set: T] x -> 0 <= (gE n) x + by rewrite /gE /= // lee_fin. + have HgEmono x : [set: T] x -> {homo gE^~ x : n m / (Order.le n m) >-> n <= m}. + move => Hx n m Hnm. + apply/ lefP. + exact/ nd_nnsfun_approx. + + (* By MCT, limit of the integrals of g_n is the integral of the limit of g_n *) + have Hcvg := (cvg_monotone_convergence _ HgEmeas HgEge0 HgEmono). + + pose gEInt := fun n => fun μ => \int[μ]_x (gE n) x. + have HgEIntmeas n : measurable_fun [set: giryM T R] (gEInt n). + rewrite /gEInt /gE /=. + eapply eq_measurable_fun. + move => μ Hμ. + rewrite integralT_nnsfun sintegralE //. + apply emeasurable_fsum => // r. + have Hrmeas : d.-measurable (g n @^-1` [set r]) by []. + apply (measurable_funeM (r%:E)). + have : measurable_fun [set: giryM T R] (fun x : giryM T R => x (g n @^-1` [set r])); auto. + exact : eq_measurable_fun (gEval_meas_fun Hrmeas). + (* The μ ↦ int[mu] lim g_n is measurable if every μ ↦ int[mu] g_n is measurable *) + apply (emeasurable_fun_cvg _ (fun (μ : giryM T R) => \int[μ]_x f x) HgEIntmeas). + move => μ Hμ. + rewrite /gEInt /=. + rewrite (eq_integral (fun x : T => limn (gE^~ x))); first exact: (Hcvg μ measurableT). + move => x Hx. + apply: esym. + apply/ cvg_lim => //. + apply/ cvg_nnsfun_approx => //. + Qed. + +End giry_integral. + +(* TODO: Everything below needs to be cleaned up *) + +Section giry_cod_meas. +Local Open Scope classical_set_scope. + + (* TODO: Either move this lemma to a more accessible location, or integrate within + the proof below *) +Let measurability_aux d d' (aT : measurableType d) (rT : measurableType d') + (f : aT -> rT) (G : set (set rT)) : + @measurable _ rT = <> -> ( forall (S : set rT), G S -> @measurable _ aT (f @^-1` S)) -> + measurable_fun setT f. +Proof. + move => HG HS. + apply/ (measurability (G := G)) => //. + apply image_subP => ??. + rewrite setTI. + exact: HS. +Qed. + +(* Adapted from mathlib induction_on_inter *) +(* TODO: Clean up proof, move lemma, change premises to use setX_closed like notations *) +Lemma dynkin_induction d {T : measurableType d} (G : set (set T)) (P : (set T) -> Prop) : + @measurable _ T = <> -> + setI_closed G -> + (P setT) -> + (forall S, G S -> P S) -> + (forall S, measurable S -> P S -> P (setC S)) -> + (forall F : sequences.sequence (set T), + (forall n, measurable (F n)) -> + trivIset setT F -> + (forall n, P (F n)) -> P (\bigcup_k F k)) -> + (forall S, <> S -> P S). +Proof. + move => HG HIclosed HsetT Hgen HsetC Hbigcup S HGS. + have HmS : measurable S; [ rewrite HG // |]. + have Haux : <> `<=` [set S : (set T) | measurable S /\ P S]; + last by apply Haux. + apply lambda_system_subset; first by []. + apply (dynkin_lambda_system ([set S0 | measurable S0 /\ P S0])). + split; first by []. + move=> ?[??]. + split; first exact: measurableC. + exact: HsetC. + move=> ?? Hm. + split. + apply bigcup_measurable; auto. + move=> k Hk. + apply Hm => //. + apply Hbigcup => //. + apply Hm. + apply Hm. + move=> ??. + split; last by apply Hgen. + rewrite HG //. + apply sub_gen_smallest; auto. + by []. +Qed. + +Let eq_measurable {d} {T : measurableType d} [X Y : set T] : + d.-measurable X -> Y = X -> d.-measurable Y. +Proof. by move=>?->. Qed. + +Lemma giryM_cod_meas_fun {d1 : measure_display} {d2 : measure_display} + {T1 : measurableType d1} {T2 : measurableType d2} {R : realType} + (f : T1 -> giryM T2 R) : + (forall (S : set T2) (HmS : measurable S), measurable_fun setT (fun t => f t S)) -> + measurable_fun setT f. +Proof. + move => HS. + eapply measurability_aux. + { + rewrite /giry_display.-measurable /= /giry_measurable. + auto. + } + move => S [U HU1 HU2]. + specialize (HS U HU1). + rewrite /gEvalPreImg /preimage_class in HU2. + destruct HU2 as [B HB <-]. + specialize (HS measurableT B HB). + rewrite setTI. + rewrite -comp_preimage. + apply (eq_measurable HS). + rewrite setTI /gEval /= //. +Qed. + +End giry_cod_meas. + +Section giry_map. +Local Open Scope classical_set_scope. +Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). + +Variables (f : T1 -> T2) (Hmf : measurable_fun setT f) (μ1 : giryM T1 R). + +Definition gMap_ev := pushforward μ1 Hmf. + +Let gMap0 : gMap_ev set0 = 0%E. +Proof. + rewrite /gMap_ev measure0 //. +Qed. + +Let gMap_ge0 A : (0 <= gMap_ev A)%E. +Proof. + rewrite /gMap_ev measure_ge0 //. +Qed. + +Let gMap_semi_sigma_additive : semi_sigma_additive (gMap_ev). +Proof. + rewrite /gMap_ev. + apply measure_semi_sigma_additive. +Qed. + +Let gMap_setT : (gMap_ev setT <= 1)%E. +Proof. + rewrite /gMap_ev /pushforward /=. + apply sprobability_setT. +Qed. + + +HB.instance Definition _ := isMeasure.Build d2 T2 R gMap_ev gMap0 gMap_ge0 gMap_semi_sigma_additive. +HB.instance Definition _ := Measure_isSubProbability.Build _ _ _ gMap_ev gMap_setT. + +Definition gMap : giryM T2 R := gMap_ev. + +End giry_map. + +Section giry_map_meas. + + +Local Open Scope classical_set_scope. +Local Open Scope ereal_scope. +Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). + +Lemma gMap_to_int (f : T1 -> T2) (Hmf : measurable_fun setT f) (μ1 : giryM T1 R) + (S : set T2) (HmS : measurable S): + (gMap Hmf μ1 S = \int[μ1]_x (numfun.indic S (f x))%:E)%E. +Proof. + rewrite /gMap /gMap_ev. + rewrite -{1}(setIT S). + rewrite -(integral_indic (pushforward μ1 Hmf)); auto. + rewrite ge0_integral_pushforward; auto. + apply EFin_measurable_fun. + apply measurable_indic; auto. + intros y. + rewrite /numfun.indic. + case: (y \in S); auto. +Qed. + +Lemma gMap_meas_fun (f : T1 -> T2) (Hmf : measurable_fun setT f): + measurable_fun setT (gMap Hmf (R:= R)). +Proof. + rewrite /gMap. + apply (@giryM_cod_meas_fun _ _ (giryM T1 R)); simpl. + intros S HmS. + rewrite /gMap_ev /pushforward /=. + apply gEval_meas_fun. + rewrite -(setTI (f @^-1` S)). + apply Hmf; auto. +Qed. + + +Lemma gMapInt (f : T1 -> T2) (Hmf : measurable_fun setT f) (μ : giryM T1 R) + (h : T2 -> \bar R) (Hmh : measurable_fun setT h) (Hpos : forall x, 0 <= h x): + gInt h (gMap Hmf μ) = gInt (h \o f) μ. +Proof. + rewrite /gInt. + have Haux : (forall S, d2.-measurable S -> S `<=` [set : T2] -> gMap Hmf μ S = pushforward μ Hmf S); auto. + erewrite (eq_measure_integral _ Haux). + rewrite ge0_integral_pushforward; auto. + by []. +Qed. + + +End giry_map_meas. + +Section giry_ret. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType). + + +Definition gRet (x:T) : giryM T R := (dirac^~ R x)%R. + +Lemma gRet_meas_fun : measurable_fun setT gRet. +Proof. + rewrite /gRet /dirac. + apply giryM_cod_meas_fun; simpl. + intros S HmS. + rewrite /dirac. + apply EFin_measurable_fun. + apply measurable_indic; auto. +Qed. + + +Lemma gRetInt (x : T) (h : T -> \bar R) (H : measurable_fun setT h): + gInt h (gRet x) = h x. +Proof. + rewrite /gInt. + have Haux : (forall S, d.-measurable S -> S `<=` [set : T] -> gRet x S = dirac x S); auto. + erewrite (eq_measure_integral _ Haux). + rewrite integral_dirac; auto. + rewrite diracT mul1e //. +Qed. + +Lemma gRetInt_rw (x : T) (h : T -> \bar R) (H : measurable_fun setT h): + \int[gRet x]_x h x = h x. +Proof. + apply gRetInt; auto. +Qed. + + +End giry_ret. + + +Section giry_join. +Local Open Scope classical_set_scope. +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType). +Variable (M : giryM (giryM T R) R). + +Definition gJoin_ev (S : set T) := gInt (gEval S) M. + +Let gJoin0 : gJoin_ev set0 = 0%E. +Proof. + rewrite /gJoin_ev /gEval. + apply integral0_eq. + auto. +Qed. + +Let gJoin_ge0 A : (0 <= gJoin_ev A)%E. +Proof. + rewrite /gJoin_ev. + apply integral_ge0. + auto. +Qed. + +(* TODO: Cleaner proof? *) +Let gJoin_semi_sigma_additive : semi_sigma_additive (gJoin_ev). +Proof. + rewrite /gJoin_ev /gInt. + rewrite /gEval /=. + intros F HF HFTriv HcupF. + have Hμ : (forall (μ : giryM T R), semi_sigma_additive μ). + { + intros; auto. + apply measure_semi_sigma_additive. + } + eapply cvg_trans. + { + erewrite eq_cvg; last first. + intros ?. + rewrite -ge0_integral_sum; auto. + by reflexivity. + intros. + apply gEval_meas_fun; auto. + auto. + } + eapply cvg_trans. + { + apply cvg_monotone_convergence; auto. + { + intros n. + apply emeasurable_fun_sum. + intros. + apply gEval_meas_fun; auto. + } + { + intros n ? ?. + rewrite sume_ge0; auto. + } + intros ? ?. + intros ? ? ?. + rewrite ereal_nondecreasing_series //. + } + simpl. + have -> :(\int[M]_x x (\bigcup_n F n) = \int[M]_x \big[+%R/0%R]_(0 <= k -> R} ) (Hmh : measurable_fun setT h) : + sintegral (gJoin M) h = \int[M]_μ sintegral μ h. +Proof. + etransitivity; last first. + { + eapply eq_integral. + intros μ Hμ. + rewrite sintegralE. + by reflexivity. + } + simpl. + rewrite ge0_integral_fsum; auto; last first. + { + intros ???. + apply nnsfun_mulemu_ge0. + } + { + intros ?. + apply measurable_funeM. + apply gEval_meas_fun; auto. + } + rewrite sintegralE /=. + have Heq: forall x, (x%:E * gJoin_ev M (h @^-1` [set x]))%E = (\int[M]_μ (x%:E * μ (h @^-1` [set x])))%E. + { + intro x. + rewrite integralZl; auto. + eapply le_integrable; last first. + apply (finite_measure_integrable_cst _ 1). + intros μ ?. + simpl. + rewrite Num.Theory.normr1. + rewrite gee0_abs. + eapply Order.le_trans; [ | apply (@sprobability_setT _ _ _ μ)]. + apply le_measure; auto. + rewrite in_setE //. + rewrite in_setE //. + apply subsetT. + rewrite measure_ge0 //. + apply gEval_meas_fun; auto. + auto. + } + apply: fsbigop.eq_fsbigr => //. +Qed. + +(* TODO: Messy proof, cleanup *) + +Lemma gJoinInt (M : giryM (giryM T R) R) + (h : T -> \bar R) (Hmh : measurable_fun setT h) (Hpos : forall x, 0 <= h x): + gInt h (gJoin M) = gInt (fun (μ : giryM T R) => \int[μ]_x h x) M. +Proof. + have HTmeas : d.-measurable [set: T]; auto. + have Hhge0' : (forall t, [set: T] t -> 0 <= h t); auto. + pose proof (approximation HTmeas Hmh Hhge0') as [g [Hgmono Hgconv]]. + + set gE := (fun n => EFin \o (g n)). + have HgEmeas : (forall n : nat, measurable_fun [set: T] (gE n)). + { + intro. + rewrite /gE /=. + apply EFin_measurable_fun; auto. + } + have HgEge0: (forall (n : nat) (x : T), [set: T] x -> 0 <= gE n x). + { + intros. + rewrite /gE /= //. + apply g. + } + have HgEmono : (forall x: T, [set: T] x -> {homo gE^~ x : n m / (Order.le n m) >-> n <= m}). + { + intros x Hx n m Hnm. + apply lee_tofin. + pose (lefP _ _ (Hgmono n m Hnm)); auto. + } + + (* By MCT, limit of the integrals of g_n is the integral of the limit of g_n *) + have Hcvg := (monotone_convergence _ _ HgEmeas HgEge0 HgEmono). + rewrite /gInt. + (* TODO: Fix failing inference? *) + + have Hgconv' : forall x : T, + [set: T] x -> + h x = (lim (fmap (EFin \o (fun x0 : nat => g x0 x)) (@nbhs nat _ eventually))). + { + intros x Hx. + specialize (Hgconv x Hx). + pose (Hgconv2 := cvgP _ Hgconv). + rewrite (cvg_unique _ Hgconv Hgconv2); auto. + } + + have Hcvg' : + forall t : measure T _, + d.-measurable [set: T] -> + \int[t]_x h x = + lim (fmap (fun n : nat => \int[t]_x gE n x) (@nbhs nat _ eventually)). + { + intros ??. + rewrite -Hcvg. auto. + apply eq_integral => x Hx. + rewrite Hgconv'; auto. + apply set_mem => //. + by []. + } + rewrite Hcvg'; auto. + rewrite (@congr_lim _ _ (fun n : nat => \int[M]_μ \int[μ]_x gE n x)); last first. + { + apply functional_extensionality_dep. + intros n. + rewrite integralT_nnsfun. + rewrite gJoinSInt. + apply eq_integral. + intros ??. + rewrite integralT_nnsfun //. + auto. + } + erewrite (@eq_integral _ _ _ M _ _ (fun μ => \int[μ]_x h x)); last first. + { + intros ??. rewrite Hcvg' //. + } + rewrite monotone_convergence; auto. + { + intros n. + eapply (gInt_meas_fun (HgEmeas n)); auto. + intros. + apply HgEge0; auto. + apply set_mem. + apply in_setT. + } + { + intros. + apply integral_ge0; auto. + } + { + intros ?????. + apply ge0_le_integral; auto. + intros ??; auto. + apply HgEmono; auto. + } +Qed. + +End giry_join_meas_fun. + +Section giry_bind. +Local Open Scope classical_set_scope. +Context d1 d2 + (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). + +Definition gBind (f : T1 -> giryM T2 R) (H : measurable_fun setT f) : giryM T1 R -> giryM T2 R := + (gJoin (R := R)) \o (gMap H (R := R)). + + +Lemma gBind_meas_fun (f : T1 -> giryM T2 R) (H : measurable_fun setT f) : measurable_fun setT (gBind H). +Proof. + eapply (@measurable_comp _ _ _ _ _ _ setT). + { by eapply @measurableT. } + { by apply subsetT. } + { by apply gJoin_meas_fun. } + { by apply gMap_meas_fun. } +Qed. + + +End giry_bind. + + +Section giry_bind_meas_fun. +Local Open Scope classical_set_scope. +Local Open Scope ereal_scope. +Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2). +Context (R : realType). + + +Lemma gBindInt_meas_fun (μ : giryM T1 R) (f : T1 -> giryM T2 R) (H : measurable_fun setT f) + (h : T2 -> \bar R) (mh : measurable_fun setT h) (Hhge0 : forall x, 0 <= h x) : + measurable_fun setT (fun x => gInt h (f x)). +Proof. + eapply (@measurable_comp _ _ _ _ _ _ setT _ _ f). + { by eapply @measurableT. } + { by apply subsetT. } + { by apply gInt_meas_fun. } + { by apply H. } +Qed. + +Lemma gBindInt : + forall (μ : giryM T1 R) (f : T1 -> giryM T2 R) (H : measurable_fun setT f) (h : T2 -> \bar R) (mh : measurable_fun setT h) (Hhge0 : forall x, 0 <= h x), + gInt h (gBind H μ) = gInt (fun x => gInt h (f x)) μ. +Proof. + intros ??????. + rewrite /gBind /=. + rewrite gJoinInt; auto. + rewrite gMapInt; auto. + apply gInt_meas_fun; auto. + intros. + apply integral_ge0; auto. +Qed. + +Lemma gBindInt_rw (μ : giryM T1 R) (f : T1 -> giryM T2 R) (H : measurable_fun setT f) (h : T2 -> \bar R) (mh : measurable_fun setT h) (Hhge0 : forall x, 0 <= h x) : + \int[gBind H μ]_y h y = \int[μ]_x \int[f x]_y h y. +Proof. + apply gBindInt; auto. +Qed. + +End giry_bind_meas_fun. + +Section giry_monad. +Local Open Scope classical_set_scope. +Local Open Scope ereal_scope. +Context d1 d2 d3 (T1 : measurableType d1) (T2 : measurableType d2) (T3 : measurableType d3). +Context (R : realType). + +Lemma gJoin_assoc : forall (x : giryM (giryM (giryM T1 R) R) R), + ((@gJoin _ _ R) \o (gMap (@gJoin_meas_fun _ _ R))) x ≡μ ((@gJoin _ _ R) \o (@gJoin _ _ R)) x. +Proof. + intros μ S HmS. + rewrite /= /gJoin_ev. + rewrite gMapInt //. + rewrite gJoinInt //. + all: apply gEval_meas_fun; auto. +Qed. + + +Lemma gJoin_id1 : forall (x : giryM T1 R), + ((@gJoin _ _ R) \o (gMap (@gRet_meas_fun _ _ R))) x ≡μ ((@gJoin _ _ R) \o (@gRet _ _ R)) x. +Proof. + intros μ S HmS. + rewrite /= /gJoin_ev; simpl. + rewrite gMapInt; auto; [|apply gEval_meas_fun; auto]. + rewrite gRetInt; auto; [|apply gEval_meas_fun; auto]. + rewrite /gInt /gEval /gRet /= /dirac. + rewrite integral_indic; auto. + rewrite setIT //. +Qed. + +Lemma gJoin_id2 : forall (x : giryM (giryM T1 R) R) (f : T1 -> T2) (H : measurable_fun setT f), + ((@gJoin _ _ R) \o gMap (gMap_meas_fun H)) x ≡μ (gMap H \o (@gJoin _ _ R)) x. +Proof. + intros μ f Hmf S HmS. + rewrite /= /gJoin_ev; simpl. + rewrite gMapInt; auto. + apply gEval_meas_fun; auto. +Qed. + + +End giry_monad. + +Section giry_zero_def. +Local Open Scope classical_set_scope. +Context d1 (T1 : measurableType d1) (R : realType). +Definition gZero := mzero : giryM T1 R. +Lemma gZero_eval : forall S (H: d1.-measurable S), gZero S = (0% E). +Proof. + intros ??. + rewrite /gZero/mzero //. +Qed. +End giry_zero_def. + + +Section giry_zero. +Local Open Scope classical_set_scope. + +Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2). +Context (R : realType). + +Lemma gZero_map : forall (f : T1 -> T2) (H : measurable_fun setT f), + gMap H (@gZero d1 T1 R) ≡μ (@gZero d2 T2 R). +Proof. + intros f H S HmS. + rewrite /=/gMap_ev /mzero //. +Qed. + +End giry_zero. + + + +Section giry_prod. +Local Open Scope classical_set_scope. +Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2). +Context (R : realType). +Variable (μ12 : giryM T1 R * giryM T2 R). + +(* https://en.wikipedia.org/wiki/Giry_monad#Product_distributions *) +Definition gProd_ev (S : set (T1 * T2)) := product_measure1 μ12.1 μ12.2 S. + + +Let gProd0 : gProd_ev set0 = 0%E. +Proof. + rewrite /gProd_ev. + auto. +Qed. + +Let gProd_ge0 A : (0 <= gProd_ev A)%E. +Proof. + rewrite /gProd_ev. + auto. +Qed. + +Let gProd_semi_sigma_additive : semi_sigma_additive (gProd_ev). +Proof. + rewrite /gProd_ev /=. + apply measure_semi_sigma_additive. +Qed. + +Let gProd_setT : (gProd_ev setT <= 1)%E. +Proof. + rewrite /gProd_ev. + rewrite -setXTT. + rewrite product_measure1E; auto. + eapply (@Order.le_trans _ _ (1*1)%E); [ | rewrite mul1e; auto]. + apply (@lee_pmul _ (μ12.1 setT) 1 (μ12.2 setT) 1); auto. + apply (@sprobability_setT d1 T1 _ μ12.1). + apply (@sprobability_setT d2 T2 _ μ12.2). + apply Order.isDuallyPOrder.le_refl. +Qed. + + +HB.instance Definition _ := isMeasure.Build _ _ R gProd_ev gProd0 gProd_ge0 gProd_semi_sigma_additive. +HB.instance Definition _ := Measure_isSubProbability.Build _ _ _ gProd_ev gProd_setT. +Definition gProd : giryM (T1*T2)%type R := gProd_ev. + +(* gBind' (fun v1 => gBind' (gRet \o (pair v1)) (snd μ)) (fst μ). *) + + +End giry_prod. + + +Section giry_prod_meas_fun. +Local Open Scope classical_set_scope. +Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2). +Context (R : realType). + +(* Is this already a mathcomp lemma? *) +Lemma measurable_setI {d : measure_display} {T: measurableType d} +(A B : set T) (HA : d.-measurable A) (HB : d.-measurable B) : + d.-measurable (A `&` B). +Proof. + rewrite -(setCK (A `&` B)). + rewrite setCI. + apply measurableC. + rewrite -bigcup2E. + apply bigcup_measurable. + intros i ?. + simpl. + case (i == 0). apply measurableC; auto. + case (i == 1). apply measurableC; auto. + apply measurable0. +Qed. + + +(* TODO: Clean up, maybe move elsewhere *) +Lemma subprobability_prod_setC + (P : giryM T1 R * giryM T2 R) (A : set (prod T1 T2)) : + measurable A -> + (product_measure1 P.1 P.2) (~` A) = + ((product_measure1 P.1 P.2) [set: T1 * T2] - (product_measure1 P.1 P.2) A)%E. +Proof. +move=> mA. +rewrite -(setvU A) measureU ?addeK ?setICl//. +- simpl. + rewrite ge0_fin_numE //. + apply (@Order.POrderTheory.le_lt_trans _ _ (((product_measure1 P.1 P.2) setT))). + rewrite le_measure; auto. + apply mem_set; auto. + apply mem_set; auto. + apply subsetT. + apply (@Order.POrderTheory.le_lt_trans _ _ 1%E); auto. + rewrite -(mul1e 1). + rewrite -setXTT product_measure1E; auto. + apply (@lee_pmul _ (P.1 setT)); auto. + apply sprobability_setT. + apply sprobability_setT. + apply (ltry (GRing.one R)). +- exact: measurableC. +Qed. + +(* + See "A synthetic approach to Markov kernels, conditional + independence and theorems on sufficient statistics", Fritz + + TODO: Clean up proof + *) +Lemma gProd_meas_fun : measurable_fun setT (@gProd d1 d2 T1 T2 R). +Proof. + simpl. + apply (@giryM_cod_meas_fun _ _ _ _ R (@gProd _ _ _ _ R)). + + rewrite measurable_prod_measurableType; simpl. + rewrite /gProd_ev. + apply dynkin_induction; simpl. + - rewrite measurable_prod_measurableType //. + - intros A B [A1 HA1 [A2 HA2 <-]] [B1 HB1 [B2 HB2 <-]]. + exists (A1 `&` B1); auto. + apply measurable_setI; auto. + exists (A2 `&` B2); auto. + apply measurable_setI; auto. + rewrite setXI //. + - eapply eq_measurable_fun; [intros ??; rewrite -setXTT product_measure1E // |]. + apply emeasurable_funM. + apply (@measurableT_comp _ _ _ _ _ _ (gEval _) _ fst). + apply gEval_meas_fun; auto. + apply (@measurable_fst _ _ (giryM T1 R) (giryM T2 R)). + + apply (@measurableT_comp _ _ _ _ _ _ (gEval _) _ snd). + apply gEval_meas_fun; auto. + apply (@measurable_snd _ _ (giryM T1 R) (giryM T2 R)). + - intros S [A HA [B HB <-]]. + eapply eq_measurable_fun; [intros ??; rewrite product_measure1E // |]. + apply emeasurable_funM. + apply (@measurableT_comp _ _ _ _ _ _ (gEval _) _ fst). + apply gEval_meas_fun; auto. + apply (@measurable_fst _ _ (giryM T1 R) (giryM T2 R)). + + apply (@measurableT_comp _ _ _ _ _ _ (gEval _) _ snd). + apply gEval_meas_fun; auto. + apply (@measurable_snd _ _ (giryM T1 R) (giryM T2 R)). + - intros S HmS HS. + eapply (eq_measurable_fun). + intros ??. simpl in x. rewrite (subprobability_prod_setC x). + rewrite -setXTT product_measure1E; first by reflexivity. + by []. + by []. + by []. + apply emeasurable_funB; auto; simpl. + apply emeasurable_funM. + apply (@measurableT_comp _ _ _ _ _ _ (gEval _) _ fst). + apply gEval_meas_fun; auto. + apply (@measurable_fst _ _ (giryM T1 R) (giryM T2 R)). + + apply (@measurableT_comp _ _ _ _ _ _ (gEval _) _ snd). + apply gEval_meas_fun; auto. + apply (@measurable_snd _ _ (giryM T1 R) (giryM T2 R)). + + - intros F HmF HF Hn. + eapply eq_measurable_fun. + intros ??. + rewrite measure_semi_bigcup //. + apply bigcup_measurable; auto. + simpl. + apply ge0_emeasurable_sum; auto. +Qed. + +End giry_prod_meas_fun. + + +Section giry_prod_int. +Local Open Scope classical_set_scope. +Local Open Scope ereal_scope. +Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2). +Context (R : realType). + +Lemma gProdInt1 (μ1 : giryM T1 R) (μ2 : giryM T2 R) + (h : (T1 * T2)%type -> \bar R) (Hmh : measurable_fun setT h) (Hpos : forall x, 0 <= h x): + gInt h (gProd (μ1, μ2)) = gInt (fun x => gInt (fun y => h (x, y)) μ2 ) μ1. +Proof. + rewrite /gInt/=/gProd_ev/=. + rewrite fubini_tonelli1; auto. +Qed. + +Lemma gProdInt2 (μ1 : giryM T1 R) (μ2 : giryM T2 R) + (h : (T1 * T2)%type -> \bar R) (Hmh : measurable_fun setT h) (Hpos : forall x, 0 <= h x): + gInt h (gProd (μ1, μ2)) = gInt (fun y => gInt (fun x => h (x, y)) μ1 ) μ2. +Proof. + rewrite /gInt/=/gProd_ev/=. + rewrite fubini_tonelli2; auto. +Qed. + +End giry_prod_int. + From 2f8b32d35896dc3e5326283f63dfa48428563780 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 3 May 2025 14:59:34 +0900 Subject: [PATCH 02/14] use existing facilities - Measure.on for gMap_ev - Measure.on for gProd_ev - \x notation for product_measure1 - measurable_fun_dirac --- giry.v | 78 ++++++++++++++-------------------------------------------- 1 file changed, 19 insertions(+), 59 deletions(-) diff --git a/giry.v b/giry.v index 567625e497..e6673c7e37 100644 --- a/giry.v +++ b/giry.v @@ -13,20 +13,25 @@ Unset Strict Implicit. Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Def Num.Theory. -Section giryM_def. -Local Open Scope classical_set_scope. +(* TODO: small PR to measure.v? *) +Section mzero_subprobability. Context d (T : measurableType d) (R : realType). +Let mzero_setT : (@mzero d T R setT <= 1)%E. +Proof. by rewrite /mzero/=. Qed. +HB.instance Definition _ := + Measure_isSubProbability.Build _ _ _ (@mzero d T R) mzero_setT. +End mzero_subprobability. -Definition giryM : Type := @subprobability d T R. +Section giryM_def. +Local Open Scope classical_set_scope. +Context d (T : measurableType d) (R : realType). -Let mzero_setT : (@mzero d T R setT <= 1)%E. -Proof. by rewrite /mzero/=. Qed. +Definition giryM : Type := @subprobability d T R. HB.instance Definition _ := gen_eqMixin giryM. HB.instance Definition _ := gen_choiceMixin giryM. -HB.instance Definition _ := Measure_isSubProbability.Build _ _ _ (@mzero d T R) mzero_setT. HB.instance Definition _ := isPointed.Build giryM mzero. Definition gEval (S : set T) (mu : giryM) := mu S. @@ -236,21 +241,7 @@ Variables (f : T1 -> T2) (Hmf : measurable_fun setT f) (μ1 : giryM T1 R). Definition gMap_ev := pushforward μ1 Hmf. -Let gMap0 : gMap_ev set0 = 0%E. -Proof. - rewrite /gMap_ev measure0 //. -Qed. - -Let gMap_ge0 A : (0 <= gMap_ev A)%E. -Proof. - rewrite /gMap_ev measure_ge0 //. -Qed. - -Let gMap_semi_sigma_additive : semi_sigma_additive (gMap_ev). -Proof. - rewrite /gMap_ev. - apply measure_semi_sigma_additive. -Qed. +HB.instance Definition _ := Measure.on gMap_ev. Let gMap_setT : (gMap_ev setT <= 1)%E. Proof. @@ -259,7 +250,6 @@ Proof. Qed. -HB.instance Definition _ := isMeasure.Build d2 T2 R gMap_ev gMap0 gMap_ge0 gMap_semi_sigma_additive. HB.instance Definition _ := Measure_isSubProbability.Build _ _ _ gMap_ev gMap_setT. Definition gMap : giryM T2 R := gMap_ev. @@ -329,10 +319,7 @@ Lemma gRet_meas_fun : measurable_fun setT gRet. Proof. rewrite /gRet /dirac. apply giryM_cod_meas_fun; simpl. - intros S HmS. - rewrite /dirac. - apply EFin_measurable_fun. - apply measurable_indic; auto. +exact: measurable_fun_dirac. Qed. @@ -765,41 +752,16 @@ Context (R : realType). Variable (μ12 : giryM T1 R * giryM T2 R). (* https://en.wikipedia.org/wiki/Giry_monad#Product_distributions *) -Definition gProd_ev (S : set (T1 * T2)) := product_measure1 μ12.1 μ12.2 S. +Definition gProd_ev := (μ12.1 \x μ12.2)%E. - -Let gProd0 : gProd_ev set0 = 0%E. -Proof. - rewrite /gProd_ev. - auto. -Qed. - -Let gProd_ge0 A : (0 <= gProd_ev A)%E. -Proof. - rewrite /gProd_ev. - auto. -Qed. - -Let gProd_semi_sigma_additive : semi_sigma_additive (gProd_ev). -Proof. - rewrite /gProd_ev /=. - apply measure_semi_sigma_additive. -Qed. +HB.instance Definition _ := Measure.on gProd_ev. Let gProd_setT : (gProd_ev setT <= 1)%E. Proof. - rewrite /gProd_ev. - rewrite -setXTT. - rewrite product_measure1E; auto. - eapply (@Order.le_trans _ _ (1*1)%E); [ | rewrite mul1e; auto]. - apply (@lee_pmul _ (μ12.1 setT) 1 (μ12.2 setT) 1); auto. - apply (@sprobability_setT d1 T1 _ μ12.1). - apply (@sprobability_setT d2 T2 _ μ12.2). - apply Order.isDuallyPOrder.le_refl. +rewrite -setXTT [leLHS]product_measure1E// -[1%E]mule1. +by rewrite lee_pmul// sprobability_setT. Qed. - -HB.instance Definition _ := isMeasure.Build _ _ R gProd_ev gProd0 gProd_ge0 gProd_semi_sigma_additive. HB.instance Definition _ := Measure_isSubProbability.Build _ _ _ gProd_ev gProd_setT. Definition gProd : giryM (T1*T2)%type R := gProd_ev. @@ -836,14 +798,13 @@ Qed. Lemma subprobability_prod_setC (P : giryM T1 R * giryM T2 R) (A : set (prod T1 T2)) : measurable A -> - (product_measure1 P.1 P.2) (~` A) = - ((product_measure1 P.1 P.2) [set: T1 * T2] - (product_measure1 P.1 P.2) A)%E. + ((P.1 \x P.2) (~` A) = (P.1 \x P.2) [set: T1 * T2] - (P.1 \x P.2) A)%E. Proof. move=> mA. rewrite -(setvU A) measureU ?addeK ?setICl//. - simpl. rewrite ge0_fin_numE //. - apply (@Order.POrderTheory.le_lt_trans _ _ (((product_measure1 P.1 P.2) setT))). + apply (@Order.POrderTheory.le_lt_trans _ _ ((P.1 \x P.2)%E setT)). rewrite le_measure; auto. apply mem_set; auto. apply mem_set; auto. @@ -950,4 +911,3 @@ Proof. Qed. End giry_prod_int. - From c3cd60e6272e849faba38b96cc14ac5788a831c8 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 3 May 2025 15:26:31 +0900 Subject: [PATCH 03/14] measurable_setI was measurableI --- giry.v | 60 ++++++++++++---------------------------------------------- 1 file changed, 12 insertions(+), 48 deletions(-) diff --git a/giry.v b/giry.v index e6673c7e37..563a5d050b 100644 --- a/giry.v +++ b/giry.v @@ -776,24 +776,6 @@ Local Open Scope classical_set_scope. Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2). Context (R : realType). -(* Is this already a mathcomp lemma? *) -Lemma measurable_setI {d : measure_display} {T: measurableType d} -(A B : set T) (HA : d.-measurable A) (HB : d.-measurable B) : - d.-measurable (A `&` B). -Proof. - rewrite -(setCK (A `&` B)). - rewrite setCI. - apply measurableC. - rewrite -bigcup2E. - apply bigcup_measurable. - intros i ?. - simpl. - case (i == 0). apply measurableC; auto. - case (i == 1). apply measurableC; auto. - apply measurable0. -Qed. - - (* TODO: Clean up, maybe move elsewhere *) Lemma subprobability_prod_setC (P : giryM T1 R * giryM T2 R) (A : set (prod T1 T2)) : @@ -835,30 +817,18 @@ Proof. apply dynkin_induction; simpl. - rewrite measurable_prod_measurableType //. - intros A B [A1 HA1 [A2 HA2 <-]] [B1 HB1 [B2 HB2 <-]]. - exists (A1 `&` B1); auto. - apply measurable_setI; auto. - exists (A2 `&` B2); auto. - apply measurable_setI; auto. - rewrite setXI //. + exists (A1 `&` B1); first exact: measurableI. + exists (A2 `&` B2); first exact: measurableI. + by rewrite setXI. - eapply eq_measurable_fun; [intros ??; rewrite -setXTT product_measure1E // |]. - apply emeasurable_funM. - apply (@measurableT_comp _ _ _ _ _ _ (gEval _) _ fst). - apply gEval_meas_fun; auto. - apply (@measurable_fst _ _ (giryM T1 R) (giryM T2 R)). - - apply (@measurableT_comp _ _ _ _ _ _ (gEval _) _ snd). - apply gEval_meas_fun; auto. - apply (@measurable_snd _ _ (giryM T1 R) (giryM T2 R)). + apply: emeasurable_funM; + apply: (@measurableT_comp _ _ _ _ _ _ (gEval _)) => //; + exact: gEval_meas_fun. - intros S [A HA [B HB <-]]. eapply eq_measurable_fun; [intros ??; rewrite product_measure1E // |]. - apply emeasurable_funM. - apply (@measurableT_comp _ _ _ _ _ _ (gEval _) _ fst). - apply gEval_meas_fun; auto. - apply (@measurable_fst _ _ (giryM T1 R) (giryM T2 R)). - - apply (@measurableT_comp _ _ _ _ _ _ (gEval _) _ snd). - apply gEval_meas_fun; auto. - apply (@measurable_snd _ _ (giryM T1 R) (giryM T2 R)). + apply: emeasurable_funM; + apply: (@measurableT_comp _ _ _ _ _ _ (gEval _)) => //; + exact: gEval_meas_fun. - intros S HmS HS. eapply (eq_measurable_fun). intros ??. simpl in x. rewrite (subprobability_prod_setC x). @@ -867,15 +837,9 @@ Proof. by []. by []. apply emeasurable_funB; auto; simpl. - apply emeasurable_funM. - apply (@measurableT_comp _ _ _ _ _ _ (gEval _) _ fst). - apply gEval_meas_fun; auto. - apply (@measurable_fst _ _ (giryM T1 R) (giryM T2 R)). - - apply (@measurableT_comp _ _ _ _ _ _ (gEval _) _ snd). - apply gEval_meas_fun; auto. - apply (@measurable_snd _ _ (giryM T1 R) (giryM T2 R)). - + apply: emeasurable_funM; + apply: (@measurableT_comp _ _ _ _ _ _ (gEval _)) => //; + exact: gEval_meas_fun. - intros F HmF HF Hn. eapply eq_measurable_fun. intros ??. From 35b8b0b633a78bf2e9eb0b8d39c4b0e3c96263d3 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 3 May 2025 17:05:54 +0900 Subject: [PATCH 04/14] more idiomatic use of library - import numfun for the \1_ notation - redundant hypo in gJoinSInt - use fin_num_measure - use nnsfun_approx in gJoinInt --- giry.v | 201 ++++++++++++++------------------------------------------- 1 file changed, 50 insertions(+), 151 deletions(-) diff --git a/giry.v b/giry.v index 563a5d050b..67af53dd1d 100644 --- a/giry.v +++ b/giry.v @@ -1,5 +1,5 @@ From mathcomp Require Import all_ssreflect all_algebra boolp classical_sets functions. -From mathcomp Require Import reals topology separation_axioms ereal sequences measure measurable_realfun lebesgue_measure lebesgue_integral. +From mathcomp Require Import reals topology separation_axioms ereal sequences numfun measure measurable_realfun lebesgue_measure lebesgue_integral. (* From clutch.prob.monad Require Export prelude. From clutch.prelude Require Import classical. @@ -11,6 +11,7 @@ From HB Require Import structures. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. + Import Order.TTheory GRing.Theory Num.Def Num.Theory. (* TODO: small PR to measure.v? *) @@ -265,17 +266,12 @@ Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). Lemma gMap_to_int (f : T1 -> T2) (Hmf : measurable_fun setT f) (μ1 : giryM T1 R) (S : set T2) (HmS : measurable S): - (gMap Hmf μ1 S = \int[μ1]_x (numfun.indic S (f x))%:E)%E. + (gMap Hmf μ1 S = \int[μ1]_x (\1_S (f x))%:E)%E. Proof. - rewrite /gMap /gMap_ev. - rewrite -{1}(setIT S). - rewrite -(integral_indic (pushforward μ1 Hmf)); auto. - rewrite ge0_integral_pushforward; auto. - apply EFin_measurable_fun. - apply measurable_indic; auto. - intros y. - rewrite /numfun.indic. - case: (y \in S); auto. +rewrite -[in LHS](setIT S) -[LHS]integral_indic//. +rewrite ge0_integral_pushforward//. + exact/measurable_EFinP/measurable_indic. +by move=> y _; rewrite lee_fin. Qed. Lemma gMap_meas_fun (f : T1 -> T2) (Hmf : measurable_fun setT f): @@ -295,11 +291,7 @@ Lemma gMapInt (f : T1 -> T2) (Hmf : measurable_fun setT f) (μ : giryM T1 R) (h : T2 -> \bar R) (Hmh : measurable_fun setT h) (Hpos : forall x, 0 <= h x): gInt h (gMap Hmf μ) = gInt (h \o f) μ. Proof. - rewrite /gInt. - have Haux : (forall S, d2.-measurable S -> S `<=` [set : T2] -> gMap Hmf μ S = pushforward μ Hmf S); auto. - erewrite (eq_measure_integral _ Haux). - rewrite ge0_integral_pushforward; auto. - by []. +exact: ge0_integral_pushforward. Qed. @@ -371,11 +363,6 @@ Proof. rewrite /gJoin_ev /gInt. rewrite /gEval /=. intros F HF HFTriv HcupF. - have Hμ : (forall (μ : giryM T R), semi_sigma_additive μ). - { - intros; auto. - apply measure_semi_sigma_additive. - } eapply cvg_trans. { erewrite eq_cvg; last first. @@ -409,11 +396,8 @@ Proof. apply eq_integral. intros μ Hμ'. simpl. - rewrite /semi_sigma_additive in Hμ. - specialize (Hμ μ F HF HFTriv HcupF). - symmetry. - apply cvg_lim; auto. - apply eventually_filter. + apply/esym/cvg_lim => //. + exact: measure_sigma_additive. Qed. (* TODO: Cleaner proof? *) @@ -473,7 +457,7 @@ Qed. Import HBNNSimple. (* TODO: Messy proof, cleanup *) -Lemma gJoinSInt (M : giryM (giryM T R) R) (h : {nnsfun T >-> R} ) (Hmh : measurable_fun setT h) : +Lemma gJoinSInt (M : giryM (giryM T R) R) (h : {nnsfun T >-> R}) : sintegral (gJoin M) h = \int[M]_μ sintegral μ h. Proof. etransitivity; last first. @@ -495,121 +479,48 @@ Proof. apply gEval_meas_fun; auto. } rewrite sintegralE /=. - have Heq: forall x, (x%:E * gJoin_ev M (h @^-1` [set x]))%E = (\int[M]_μ (x%:E * μ (h @^-1` [set x])))%E. - { - intro x. - rewrite integralZl; auto. - eapply le_integrable; last first. - apply (finite_measure_integrable_cst _ 1). - intros μ ?. - simpl. - rewrite Num.Theory.normr1. - rewrite gee0_abs. - eapply Order.le_trans; [ | apply (@sprobability_setT _ _ _ μ)]. - apply le_measure; auto. - rewrite in_setE //. - rewrite in_setE //. - apply subsetT. - rewrite measure_ge0 //. - apply gEval_meas_fun; auto. - auto. - } + have Heq x : (x%:E * gJoin_ev M (h @^-1` [set x]) = \int[M]_μ (x%:E * μ (h @^-1` [set x])))%E. + rewrite integralZl//. + have := finite_measure_integrable_cst M 1. + apply: le_integrable => //; first exact: gEval_meas_fun. + move=> mu _ /=. + rewrite normr1 gee0_abs// (le_trans _ (@sprobability_setT _ _ _ mu))//. + by rewrite le_measure// ?inE. apply: fsbigop.eq_fsbigr => //. Qed. (* TODO: Messy proof, cleanup *) Lemma gJoinInt (M : giryM (giryM T R) R) - (h : T -> \bar R) (Hmh : measurable_fun setT h) (Hpos : forall x, 0 <= h x): - gInt h (gJoin M) = gInt (fun (μ : giryM T R) => \int[μ]_x h x) M. -Proof. - have HTmeas : d.-measurable [set: T]; auto. - have Hhge0' : (forall t, [set: T] t -> 0 <= h t); auto. - pose proof (approximation HTmeas Hmh Hhge0') as [g [Hgmono Hgconv]]. - - set gE := (fun n => EFin \o (g n)). - have HgEmeas : (forall n : nat, measurable_fun [set: T] (gE n)). - { - intro. - rewrite /gE /=. - apply EFin_measurable_fun; auto. - } - have HgEge0: (forall (n : nat) (x : T), [set: T] x -> 0 <= gE n x). - { - intros. - rewrite /gE /= //. - apply g. - } - have HgEmono : (forall x: T, [set: T] x -> {homo gE^~ x : n m / (Order.le n m) >-> n <= m}). - { - intros x Hx n m Hnm. - apply lee_tofin. - pose (lefP _ _ (Hgmono n m Hnm)); auto. - } - - (* By MCT, limit of the integrals of g_n is the integral of the limit of g_n *) - have Hcvg := (monotone_convergence _ _ HgEmeas HgEge0 HgEmono). - rewrite /gInt. - (* TODO: Fix failing inference? *) - - have Hgconv' : forall x : T, - [set: T] x -> - h x = (lim (fmap (EFin \o (fun x0 : nat => g x0 x)) (@nbhs nat _ eventually))). - { - intros x Hx. - specialize (Hgconv x Hx). - pose (Hgconv2 := cvgP _ Hgconv). - rewrite (cvg_unique _ Hgconv Hgconv2); auto. - } - - have Hcvg' : - forall t : measure T _, - d.-measurable [set: T] -> - \int[t]_x h x = - lim (fmap (fun n : nat => \int[t]_x gE n x) (@nbhs nat _ eventually)). - { - intros ??. - rewrite -Hcvg. auto. - apply eq_integral => x Hx. - rewrite Hgconv'; auto. - apply set_mem => //. - by []. - } - rewrite Hcvg'; auto. - rewrite (@congr_lim _ _ (fun n : nat => \int[M]_μ \int[μ]_x gE n x)); last first. - { - apply functional_extensionality_dep. - intros n. - rewrite integralT_nnsfun. - rewrite gJoinSInt. - apply eq_integral. - intros ??. - rewrite integralT_nnsfun //. - auto. - } - erewrite (@eq_integral _ _ _ M _ _ (fun μ => \int[μ]_x h x)); last first. - { - intros ??. rewrite Hcvg' //. - } - rewrite monotone_convergence; auto. - { - intros n. - eapply (gInt_meas_fun (HgEmeas n)); auto. - intros. - apply HgEge0; auto. - apply set_mem. - apply in_setT. - } - { - intros. - apply integral_ge0; auto. - } - { - intros ?????. - apply ge0_le_integral; auto. - intros ??; auto. - apply HgEmono; auto. - } + (h : T -> \bar R) (mh : measurable_fun setT h) (h_ge0 : forall x, 0 <= h x) : + gInt h (gJoin M) = gInt (fun μ : giryM T R => \int[μ]_x h x) M. +Proof. +pose g := nnsfun_approx measurableT mh. +pose gE := fun n => EFin \o (g n). +have mgE n : measurable_fun setT (gE n) by exact/measurable_EFinP. +have gE_ge0 n x : 0 <= gE n x by rewrite lee_fin. +have nd_gE x : {homo gE ^~ x : n m / (n <= m)%O >-> n <= m}. + by move=> *; exact/lefP/nd_nnsfun_approx. +(* By MCT, limit of the integrals of g_n is the integral of the limit of g_n *) +rewrite /gInt. +transitivity (limn (fun n => \int[gJoin M]_x gE n x)). + rewrite -monotone_convergence//. + apply: eq_integral => t _. + by apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. +transitivity (limn (fun n => \int[M]_μ \int[μ]_x gE n x)). + apply: congr_lim; apply/funext => n. + rewrite integralT_nnsfun. + rewrite gJoinSInt. + apply: eq_integral => x _. + by rewrite integralT_nnsfun. +rewrite -monotone_convergence//; last 3 first. + by move=> n; exact: gInt_meas_fun. + by move=> n x _; exact: integral_ge0. + by move=> x _ m n mn; apply: ge0_le_integral => // t _; exact: nd_gE. +apply: eq_integral => mu _. +rewrite -monotone_convergence//. +apply: eq_integral => t _. +by apply/cvg_lim => //; exact: cvg_nnsfun_approx. Qed. End giry_join_meas_fun. @@ -783,21 +694,9 @@ Lemma subprobability_prod_setC ((P.1 \x P.2) (~` A) = (P.1 \x P.2) [set: T1 * T2] - (P.1 \x P.2) A)%E. Proof. move=> mA. -rewrite -(setvU A) measureU ?addeK ?setICl//. -- simpl. - rewrite ge0_fin_numE //. - apply (@Order.POrderTheory.le_lt_trans _ _ ((P.1 \x P.2)%E setT)). - rewrite le_measure; auto. - apply mem_set; auto. - apply mem_set; auto. - apply subsetT. - apply (@Order.POrderTheory.le_lt_trans _ _ 1%E); auto. - rewrite -(mul1e 1). - rewrite -setXTT product_measure1E; auto. - apply (@lee_pmul _ (P.1 setT)); auto. - apply sprobability_setT. - apply sprobability_setT. - apply (ltry (GRing.one R)). +rewrite -(setvU A) measureU//= ?addeK ?setICl//. +- rewrite -/(gProd_ev _). + exact: fin_num_measure. - exact: measurableC. Qed. From 4f8c40e310822e434decb14c9d0a70aacc8a4212 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 3 May 2025 19:18:50 +0900 Subject: [PATCH 05/14] minor cleaning in proofs marked as TODOs --- giry.v | 160 +++++++++++++++++++-------------------------------------- 1 file changed, 54 insertions(+), 106 deletions(-) diff --git a/giry.v b/giry.v index 67af53dd1d..d3074f557a 100644 --- a/giry.v +++ b/giry.v @@ -1,5 +1,7 @@ -From mathcomp Require Import all_ssreflect all_algebra boolp classical_sets functions. -From mathcomp Require Import reals topology separation_axioms ereal sequences numfun measure measurable_realfun lebesgue_measure lebesgue_integral. +From mathcomp Require Import all_ssreflect all_algebra boolp classical_sets. +From mathcomp Require Import fsbigop functions reals topology separation_axioms. +From mathcomp Require Import ereal sequences numfun measure measurable_realfun. +From mathcomp Require Import lebesgue_measure lebesgue_integral. (* From clutch.prob.monad Require Export prelude. From clutch.prelude Require Import classical. @@ -339,104 +341,65 @@ Section giry_join. Local Open Scope classical_set_scope. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType). -Variable (M : giryM (giryM T R) R). +Variable M : giryM (giryM T R) R. Definition gJoin_ev (S : set T) := gInt (gEval S) M. -Let gJoin0 : gJoin_ev set0 = 0%E. -Proof. - rewrite /gJoin_ev /gEval. - apply integral0_eq. - auto. -Qed. +Let gJoin0 : gJoin_ev set0 = 0. +Proof. by rewrite /gJoin_ev /gEval /gInt integral0_eq. Qed. -Let gJoin_ge0 A : (0 <= gJoin_ev A)%E. -Proof. - rewrite /gJoin_ev. - apply integral_ge0. - auto. -Qed. +Let gJoin_ge0 A : 0 <= gJoin_ev A. +Proof. by rewrite /gJoin_ev integral_ge0. Qed. (* TODO: Cleaner proof? *) Let gJoin_semi_sigma_additive : semi_sigma_additive (gJoin_ev). Proof. - rewrite /gJoin_ev /gInt. - rewrite /gEval /=. - intros F HF HFTriv HcupF. - eapply cvg_trans. - { - erewrite eq_cvg; last first. - intros ?. - rewrite -ge0_integral_sum; auto. - by reflexivity. - intros. - apply gEval_meas_fun; auto. - auto. - } - eapply cvg_trans. - { - apply cvg_monotone_convergence; auto. - { - intros n. - apply emeasurable_fun_sum. - intros. - apply gEval_meas_fun; auto. - } - { - intros n ? ?. - rewrite sume_ge0; auto. - } - intros ? ?. - intros ? ? ?. - rewrite ereal_nondecreasing_series //. - } - simpl. - have -> :(\int[M]_x x (\bigcup_n F n) = \int[M]_x \big[+%R/0%R]_(0 <= k F mF tF _. +rewrite /gJoin_ev /gInt /gEval /=. +rewrite [X in _ --> X](_ : _ = \int[M]_x \sum_(0 <= k mu _. apply/esym/cvg_lim => //. exact: measure_sigma_additive. +rewrite [X in X @ _](_ : _ = + (fun n => \int[M]_x \sum_(0 <= i < n) x (F i))); last first. + apply/funext => n. + rewrite -ge0_integral_sum// => m. + exact: gEval_meas_fun. +apply: cvg_monotone_convergence => //. +- move=> n; apply: emeasurable_sum => m. + exact: gEval_meas_fun. +- by move=> n x _; rewrite sume_ge0. +- by move=> x _ m n mn; exact: ereal_nondecreasing_series. Qed. +HB.instance Definition _ := isMeasure.Build d _ R gJoin_ev + gJoin0 gJoin_ge0 gJoin_semi_sigma_additive. + (* TODO: Cleaner proof? *) -Let gJoin_setT : (gJoin_ev setT <= 1)%E. +Let gJoin_setT : gJoin_ev setT <= 1. Proof. - rewrite /gJoin_ev. - apply (@Order.le_trans _ _ (1%:E * (M setT))); last first. - { - rewrite mul1e. - apply sprobability_setT. - } - eapply Order.le_trans; last first. - { - apply (@integral_le_bound _ _ R M _ (gEval setT) 1); auto. - apply gEval_meas_fun; auto. - apply (aeW M). - intros ??. - rewrite gee0_abs; auto. - rewrite /gEval. - apply (@sprobability_setT d T R x). - } - apply ge0_le_integral; auto. - apply gEval_meas_fun; auto. - intros; apply abse_ge0. - apply (@measurableT_comp _ _ _ _ _ _ abse). - apply abse_measurable. - apply gEval_meas_fun; auto. - intros ??. - rewrite gee0_abs; auto. +rewrite /gJoin_ev. +rewrite (@le_trans _ _ (\int[M]_x `|gEval setT x|))//; last first. + rewrite (@le_trans _ _ (1%E * M setT))//; last first. + by rewrite mul1e sprobability_setT. + rewrite integral_le_bound//. + exact: gEval_meas_fun. + apply/aeW => x _. + by rewrite gee0_abs// sprobability_setT. +rewrite ge0_le_integral//=. +- exact: gEval_meas_fun. +- by move=> x _; rewrite abse_ge0. +- by apply: measurableT_comp => //; exact: gEval_meas_fun. +- by move=> x _; rewrite gee0_abs. Qed. -HB.instance Definition _ := isMeasure.Build d _ R gJoin_ev gJoin0 gJoin_ge0 gJoin_semi_sigma_additive. -HB.instance Definition _ := Measure_isSubProbability.Build _ _ _ gJoin_ev gJoin_setT. +HB.instance Definition _ := + Measure_isSubProbability.Build _ _ _ gJoin_ev gJoin_setT. Definition gJoin : giryM T R := gJoin_ev. End giry_join. - Section giry_join_meas_fun. Local Open Scope classical_set_scope. Local Open Scope ereal_scope. @@ -460,33 +423,18 @@ Import HBNNSimple. Lemma gJoinSInt (M : giryM (giryM T R) R) (h : {nnsfun T >-> R}) : sintegral (gJoin M) h = \int[M]_μ sintegral μ h. Proof. - etransitivity; last first. - { - eapply eq_integral. - intros μ Hμ. - rewrite sintegralE. - by reflexivity. - } - simpl. - rewrite ge0_integral_fsum; auto; last first. - { - intros ???. - apply nnsfun_mulemu_ge0. - } - { - intros ?. - apply measurable_funeM. - apply gEval_meas_fun; auto. - } - rewrite sintegralE /=. - have Heq x : (x%:E * gJoin_ev M (h @^-1` [set x]) = \int[M]_μ (x%:E * μ (h @^-1` [set x])))%E. - rewrite integralZl//. - have := finite_measure_integrable_cst M 1. - apply: le_integrable => //; first exact: gEval_meas_fun. - move=> mu _ /=. - rewrite normr1 gee0_abs// (le_trans _ (@sprobability_setT _ _ _ mu))//. - by rewrite le_measure// ?inE. - apply: fsbigop.eq_fsbigr => //. +under eq_integral do rewrite sintegralE. +rewrite ge0_integral_fsum//; last 2 first. + by move=> r; apply: measurable_funeM; exact: gEval_meas_fun. + by move=> n x _; exact: nnsfun_mulemu_ge0. +rewrite sintegralE /=. +apply: fsbigop.eq_fsbigr => // r rh. +rewrite integralZl//. +have := finite_measure_integrable_cst M 1. +apply: le_integrable => //; first exact: gEval_meas_fun. +move=> mu _ /=. +rewrite normr1 gee0_abs// (le_trans _ (@sprobability_setT _ _ _ mu))//. +by rewrite le_measure// ?inE. Qed. (* TODO: Messy proof, cleanup *) From 8f5ae95366c3efcea8d61605c6ed2b09f76932f7 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 9 Jul 2025 16:50:52 +0900 Subject: [PATCH 06/14] just rebase and lint --- giry.v | 598 ++++++++++++++++++++++++++------------------------------- 1 file changed, 268 insertions(+), 330 deletions(-) diff --git a/giry.v b/giry.v index d3074f557a..f461beb2a3 100644 --- a/giry.v +++ b/giry.v @@ -25,6 +25,7 @@ Proof. by rewrite /mzero/=. Qed. HB.instance Definition _ := Measure_isSubProbability.Build _ _ _ (@mzero d T R) mzero_setT. + End mzero_subprobability. Section giryM_def. @@ -38,11 +39,12 @@ HB.instance Definition _ := gen_choiceMixin giryM. HB.instance Definition _ := isPointed.Build giryM mzero. Definition gEval (S : set T) (mu : giryM) := mu S. -Definition gEvalPreImg (S : set T) := preimage_set_system setT (gEval S) measurable. -Definition giry_measurable := <>. +Definition gEvalPreImg (S : set T) := + preimage_set_system setT (gEval S) measurable. + +Definition giry_measurable := <>. -(* Axiom giry_measurable : set (set giryM). *) Let giry_measurable0 : giry_measurable set0. Proof. exact: sigma_algebra0. Qed. @@ -63,10 +65,11 @@ HB.instance Definition _ := End giryM_def. - -Definition measure_eq {d : measure_display} {T : measurableType d} {R : realType} : giryM T R -> giryM T R -> Prop := - fun μ1 μ2 => forall (S : set T), measurable S -> μ1 S = μ2 S. +Definition measure_eq {d} {T : measurableType d} {R : realType} : + giryM T R -> giryM T R -> Prop := + fun μ1 μ2 => forall S : set T, measurable S -> μ1 S = μ2 S. Notation "x ≡μ y" := (measure_eq x y) (at level 70). + Global Hint Extern 0 (_ ≡μ _) => reflexivity : core. Global Hint Extern 0 (_ ≡μ _) => symmetry; assumption : core. @@ -77,20 +80,20 @@ Local Open Scope classical_set_scope. Context d (T : measurableType d) (R : realType). (* TODO: Make hint *) -Lemma gEval_meas_fun (S : set T) (HmS : d.-measurable S) : measurable_fun [set: giryM T R] (gEval S). +Lemma gEval_meas_fun (S : set T) : d.-measurable S -> + measurable_fun [set: giryM T R] (gEval S). Proof. - apply: (@measurability giry_display _ (@giryM _ T R) _ setT (@gEval _ _ R S)). - rewrite smallest_id; first reflexivity. - exact: sigma_algebra_measurable. - rewrite /giry_display.-measurable /= /giry_measurable /=. - apply: subset_trans; last exact: sub_gen_smallest. - apply: subset_trans; [ | apply bigcup_sup; exact HmS]. - exact: subset_refl. +move=> mS. +apply: (@measurability giry_display _ (@giryM _ T R) _ setT (@gEval _ _ R S) + (@measurable _ (\bar R))). + rewrite smallest_id//. + exact: sigma_algebra_measurable. +apply: subset_trans; last exact: sub_gen_smallest. +exact: (bigcup_sup mS). Qed. End giry_eval. - Section giry_integral. Local Open Scope classical_set_scope. Local Open Scope ereal_scope. @@ -101,51 +104,42 @@ Definition gInt (f : T -> \bar R) (mu : giryM T R) := \int[mu]_x f x. Import HBNNSimple. Lemma gInt_meas_fun (f : T -> \bar R) : - (measurable_fun setT f) -> - (forall x, 0 <= f x) -> - measurable_fun setT (gInt f). + measurable_fun [set: T] f -> (forall x, 0 <= f x) -> + measurable_fun [set: giryM T R] (gInt f). Proof. - (* - The idea is to reconstruct f from simple functions, then use - measurability of gEval. See "Codensity and the Giry monad", Avery - *) - move => Hmf Hge0. - pose g := nnsfun_approx measurableT Hmf. - pose gE := (fun n => EFin \o g n). - have HgEmeas n : measurable_fun [set: T] (gE n). - rewrite /gE /=. - exact/ measurable_EFinP. - have HgEge0 n x : [set: T] x -> 0 <= (gE n) x - by rewrite /gE /= // lee_fin. - have HgEmono x : [set: T] x -> {homo gE^~ x : n m / (Order.le n m) >-> n <= m}. - move => Hx n m Hnm. - apply/ lefP. - exact/ nd_nnsfun_approx. - - (* By MCT, limit of the integrals of g_n is the integral of the limit of g_n *) - have Hcvg := (cvg_monotone_convergence _ HgEmeas HgEge0 HgEmono). - - pose gEInt := fun n => fun μ => \int[μ]_x (gE n) x. - have HgEIntmeas n : measurable_fun [set: giryM T R] (gEInt n). - rewrite /gEInt /gE /=. - eapply eq_measurable_fun. - move => μ Hμ. - rewrite integralT_nnsfun sintegralE //. - apply emeasurable_fsum => // r. - have Hrmeas : d.-measurable (g n @^-1` [set r]) by []. - apply (measurable_funeM (r%:E)). - have : measurable_fun [set: giryM T R] (fun x : giryM T R => x (g n @^-1` [set r])); auto. - exact : eq_measurable_fun (gEval_meas_fun Hrmeas). - (* The μ ↦ int[mu] lim g_n is measurable if every μ ↦ int[mu] g_n is measurable *) - apply (emeasurable_fun_cvg _ (fun (μ : giryM T R) => \int[μ]_x f x) HgEIntmeas). - move => μ Hμ. - rewrite /gEInt /=. - rewrite (eq_integral (fun x : T => limn (gE^~ x))); first exact: (Hcvg μ measurableT). - move => x Hx. - apply: esym. - apply/ cvg_lim => //. - apply/ cvg_nnsfun_approx => //. - Qed. +(* + The idea is to reconstruct f from simple functions, then use + measurability of gEval. See "Codensity and the Giry monad", Avery + *) +move=> mf h0. +pose g := nnsfun_approx measurableT mf. +pose gE := fun n => EFin \o g n. +have mgE n : measurable_fun [set: T] (gE n) by exact/measurable_EFinP. +have gE0 n x : [set: T] x -> 0 <= (gE n) x by rewrite /gE /= // lee_fin. +have HgEmono x : [set: T] x -> {homo gE ^~ x : n m / (n <= m)%O >-> n <= m}. + by move=> _ n m nm; exact/lefP/nd_nnsfun_approx. +(* By MCT, limit of the integrals of g_n is the integral of the limit of g_n *) +have Hcvg := cvg_monotone_convergence _ mgE gE0 HgEmono. +pose gEInt := fun n μ => \int[μ]_x (gE n) x. +have mgEInt n : measurable_fun [set: giryM T R] (gEInt n). + rewrite /gEInt /gE /=. + apply (eq_measurable_fun (fun μ : giryM T R => + \sum_(x \in range (g n)) (x%:E * μ (g n @^-1` [set x])))). + by move=> μ Hμ; rewrite integralT_nnsfun sintegralE. + apply: emeasurable_fsum => // r. + have mg : d.-measurable (g n @^-1` [set r]) by []. + apply (measurable_funeM r%:E). + have : measurable_fun [set: giryM T R] (fun x : giryM T R => x (g n @^-1` [set r])); auto. + exact : eq_measurable_fun (gEval_meas_fun mg). +(* The μ ↦ int[mu] lim g_n is measurable if every μ ↦ int[mu] g_n is measurable *) +apply: (emeasurable_fun_cvg _ (fun μ : giryM T R => \int[μ]_x f x) mgEInt). +move=> μ Hμ. +rewrite /gEInt /=. +rewrite (eq_integral (fun x : T => limn (gE^~ x))). + exact: (Hcvg μ measurableT). +move=> x _; apply/esym/cvg_lim => //. +exact/cvg_nnsfun_approx. +Qed. End giry_integral. @@ -158,101 +152,101 @@ Local Open Scope classical_set_scope. the proof below *) Let measurability_aux d d' (aT : measurableType d) (rT : measurableType d') (f : aT -> rT) (G : set (set rT)) : - @measurable _ rT = <> -> ( forall (S : set rT), G S -> @measurable _ aT (f @^-1` S)) -> - measurable_fun setT f. + @measurable _ rT = <> -> + (forall (S : set rT), G S -> @measurable _ aT (f @^-1` S)) -> + measurable_fun [set: aT] f. Proof. - move => HG HS. - apply/ (measurability (G := G)) => //. - apply image_subP => ??. - rewrite setTI. - exact: HS. +move=> HG HS. +apply/(measurability G) => //. +apply/image_subP => A GA. +rewrite setTI. +exact: HS. Qed. (* Adapted from mathlib induction_on_inter *) (* TODO: Clean up proof, move lemma, change premises to use setX_closed like notations *) -Lemma dynkin_induction d {T : measurableType d} (G : set (set T)) (P : (set T) -> Prop) : +Lemma dynkin_induction d {T : measurableType d} (G : set (set T)) (P : set_system T) : @measurable _ T = <> -> setI_closed G -> - (P setT) -> - (forall S, G S -> P S) -> - (forall S, measurable S -> P S -> P (setC S)) -> - (forall F : sequences.sequence (set T), - (forall n, measurable (F n)) -> - trivIset setT F -> - (forall n, P (F n)) -> P (\bigcup_k F k)) -> + P [set: T] -> + G `<=` P -> + (forall S, measurable S -> P S -> P (~` S)) -> + (forall F : (set T)^nat, + (forall n, measurable (F n)) -> + trivIset setT F -> + (forall n, P (F n)) -> P (\bigcup_k F k)) -> (forall S, <> S -> P S). Proof. - move => HG HIclosed HsetT Hgen HsetC Hbigcup S HGS. - have HmS : measurable S; [ rewrite HG // |]. - have Haux : <> `<=` [set S : (set T) | measurable S /\ P S]; - last by apply Haux. - apply lambda_system_subset; first by []. - apply (dynkin_lambda_system ([set S0 | measurable S0 /\ P S0])). +move=> HG GI HsetT Hgen HsetC Hbigcup S HGS. +have mS : measurable S by rewrite HG. +suff Haux : <> `<=` [set S : set T | measurable S /\ P S]. + by apply Haux. +apply lambda_system_subset; first by []. +- apply (dynkin_lambda_system ([set S0 | measurable S0 /\ P S0])). split; first by []. - move=> ?[??]. + move=> A [mA PA]. split; first exact: measurableC. exact: HsetC. - move=> ?? Hm. - split. + move=> F tF Hm. + split. apply bigcup_measurable; auto. move=> k Hk. - apply Hm => //. - apply Hbigcup => //. - apply Hm. - apply Hm. - move=> ??. - split; last by apply Hgen. - rewrite HG //. - apply sub_gen_smallest; auto. - by []. + by apply Hm. + apply: Hbigcup => //. + by apply Hm. + by apply Hm. +- move=> A GA; split; last exact: Hgen. + rewrite HG //. + exact: sub_gen_smallest. +- by []. Qed. -Let eq_measurable {d} {T : measurableType d} [X Y : set T] : - d.-measurable X -> Y = X -> d.-measurable Y. -Proof. by move=>?->. Qed. - -Lemma giryM_cod_meas_fun {d1 : measure_display} {d2 : measure_display} - {T1 : measurableType d1} {T2 : measurableType d2} {R : realType} - (f : T1 -> giryM T2 R) : - (forall (S : set T2) (HmS : measurable S), measurable_fun setT (fun t => f t S)) -> - measurable_fun setT f. +Lemma giryM_cod_meas_fun {d1} {d2} {T1 : measurableType d1} + {T2 : measurableType d2} {R : realType} (f : T1 -> giryM T2 R) : + (forall (S : set T2), measurable S -> measurable_fun setT (f ^~ S)) -> + measurable_fun [set: T1] f. Proof. - move => HS. - eapply measurability_aux. - { - rewrite /giry_display.-measurable /= /giry_measurable. - auto. - } - move => S [U HU1 HU2]. - specialize (HS U HU1). - rewrite /gEvalPreImg /preimage_class in HU2. - destruct HU2 as [B HB <-]. - specialize (HS measurableT B HB). - rewrite setTI. - rewrite -comp_preimage. - apply (eq_measurable HS). - rewrite setTI /gEval /= //. +move=> HS. +pose G : set_system (giryM T2 R) := \bigcup_(S in d2.-measurable) gEvalPreImg S. +apply: (measurability_aux (G := G)) => // S [U mU [M mB] <-]. +rewrite -comp_preimage. +exact: HS. Qed. End giry_cod_meas. Section giry_map. Local Open Scope classical_set_scope. -Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). +Local Open Scope ereal_scope. +Context {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} {R : realType}. + +Variables (f : T1 -> T2) (Hmf : measurable_fun [set: T1] f) (μ1 : giryM T1 R). + +Definition gMap_ev := pushforward μ1 f. + +Let gMap_ev0 : gMap_ev set0 = 0. +Proof. exact: measure0. Qed. -Variables (f : T1 -> T2) (Hmf : measurable_fun setT f) (μ1 : giryM T1 R). +Let gMap_ev_ge0 A : 0 <= gMap_ev A. +Proof. exact: measure_ge0. Qed. -Definition gMap_ev := pushforward μ1 Hmf. +Let gMap_ev_sigma_additive : semi_sigma_additive gMap_ev. +Proof. exact: measure_semi_sigma_additive. Qed. +HB.instance Definition _ := isMeasure.Build _ _ _ gMap_ev + gMap_ev0 gMap_ev_ge0 gMap_ev_sigma_additive. + +(* used to work before the change of definition of pushforward HB.instance Definition _ := Measure.on gMap_ev. +the change of definition was maybe not a good idea... +https://github.com/math-comp/analysis/pull/1661 +*) -Let gMap_setT : (gMap_ev setT <= 1)%E. +Let gMap_setT : gMap_ev setT <= 1. Proof. - rewrite /gMap_ev /pushforward /=. - apply sprobability_setT. +by rewrite /gMap_ev /pushforward /= sprobability_setT. Qed. - HB.instance Definition _ := Measure_isSubProbability.Build _ _ _ gMap_ev gMap_setT. Definition gMap : giryM T2 R := gMap_ev. @@ -260,83 +254,72 @@ Definition gMap : giryM T2 R := gMap_ev. End giry_map. Section giry_map_meas. - - Local Open Scope classical_set_scope. Local Open Scope ereal_scope. Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). -Lemma gMap_to_int (f : T1 -> T2) (Hmf : measurable_fun setT f) (μ1 : giryM T1 R) - (S : set T2) (HmS : measurable S): - (gMap Hmf μ1 S = \int[μ1]_x (\1_S (f x))%:E)%E. +Lemma gMap_to_int (f : T1 -> T2) (mf : measurable_fun [set: T1] f) + (μ1 : giryM T1 R) (S : set T2) : measurable S -> + gMap mf μ1 S = \int[μ1]_x (\1_S (f x))%:E. Proof. +move=> mS. rewrite -[in LHS](setIT S) -[LHS]integral_indic//. rewrite ge0_integral_pushforward//. exact/measurable_EFinP/measurable_indic. by move=> y _; rewrite lee_fin. Qed. -Lemma gMap_meas_fun (f : T1 -> T2) (Hmf : measurable_fun setT f): - measurable_fun setT (gMap Hmf (R:= R)). +Lemma gMap_meas_fun (f : T1 -> T2) (mf : measurable_fun [set: T1] f): + measurable_fun [set: giryM T1 R] (gMap mf (R:= R)). Proof. - rewrite /gMap. - apply (@giryM_cod_meas_fun _ _ (giryM T1 R)); simpl. - intros S HmS. - rewrite /gMap_ev /pushforward /=. - apply gEval_meas_fun. - rewrite -(setTI (f @^-1` S)). - apply Hmf; auto. +rewrite /gMap. +apply: (@giryM_cod_meas_fun _ _ (giryM T1 R)) => S mS. +rewrite /gMap_ev /pushforward /=. +apply: gEval_meas_fun. +rewrite -(setTI (f @^-1` S)). +exact: mf. Qed. - -Lemma gMapInt (f : T1 -> T2) (Hmf : measurable_fun setT f) (μ : giryM T1 R) - (h : T2 -> \bar R) (Hmh : measurable_fun setT h) (Hpos : forall x, 0 <= h x): - gInt h (gMap Hmf μ) = gInt (h \o f) μ. +Lemma gMapInt (f : T1 -> T2) (mf : measurable_fun [set: T1] f) (μ : giryM T1 R) + (h : T2 -> \bar R) : + measurable_fun [set: T2] h -> (forall x, 0 <= h x) -> + gInt h (gMap mf μ) = gInt (h \o f) μ. Proof. -exact: ge0_integral_pushforward. +by move=> mh h0; exact: ge0_integral_pushforward. Qed. - End giry_map_meas. Section giry_ret. - Local Open Scope classical_set_scope. Local Open Scope ring_scope. Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType). - +Context {d} {T : measurableType d} {R : realType}. -Definition gRet (x:T) : giryM T R := (dirac^~ R x)%R. +Definition gRet (x : T) : giryM T R := dirac^~ R x. -Lemma gRet_meas_fun : measurable_fun setT gRet. +Lemma gRet_meas_fun : measurable_fun [set: T] gRet. Proof. - rewrite /gRet /dirac. - apply giryM_cod_meas_fun; simpl. +apply: giryM_cod_meas_fun. exact: measurable_fun_dirac. Qed. - -Lemma gRetInt (x : T) (h : T -> \bar R) (H : measurable_fun setT h): - gInt h (gRet x) = h x. -Proof. - rewrite /gInt. - have Haux : (forall S, d.-measurable S -> S `<=` [set : T] -> gRet x S = dirac x S); auto. - erewrite (eq_measure_integral _ Haux). - rewrite integral_dirac; auto. - rewrite diracT mul1e //. -Qed. - -Lemma gRetInt_rw (x : T) (h : T -> \bar R) (H : measurable_fun setT h): - \int[gRet x]_x h x = h x. +Lemma gRetInt (x : T) (h : T -> \bar R) : measurable_fun [set: T] h -> + gInt h (gRet x) = h x. Proof. - apply gRetInt; auto. +move=> mh. +rewrite /gInt. +have : forall S, d.-measurable S -> S `<=` [set : T] -> gRet x S = dirac x S by []. +move/eq_measure_integral => ->//. +by rewrite integral_dirac// diracT mul1e. Qed. +Lemma gRetInt_rw (x : T) (h : T -> \bar R) : + measurable_fun [set: T] h -> \int[gRet x]_x h x = h x. +Proof. exact: gRetInt. Qed. End giry_ret. - Section giry_join. Local Open Scope classical_set_scope. Local Open Scope ereal_scope. @@ -401,20 +384,15 @@ Definition gJoin : giryM T R := gJoin_ev. End giry_join. Section giry_join_meas_fun. - Local Open Scope classical_set_scope. - Local Open Scope ereal_scope. - Context d (T : measurableType d) (R : realType). - +Local Open Scope classical_set_scope. +Local Open Scope ereal_scope. +Context {d} {T : measurableType d} {R : realType}. -Lemma gJoin_meas_fun : measurable_fun setT (@gJoin d T R). +Lemma gJoin_meas_fun : measurable_fun [set: giryM (giryM T R) R] (@gJoin d T R). Proof. - apply (@giryM_cod_meas_fun _ _ (giryM (giryM T _)_)); simpl. - rewrite /gJoin_ev. - intros S HmS. - eapply (@gInt_meas_fun _ _ _ (gEval S)). - Unshelve. - apply gEval_meas_fun; auto. - auto. +apply: (@giryM_cod_meas_fun _ _ (giryM (giryM T _)_)) => S mS. +apply: (@gInt_meas_fun _ _ _ (gEval S)) => //=. +exact: gEval_meas_fun. Qed. Import HBNNSimple. @@ -439,10 +417,11 @@ Qed. (* TODO: Messy proof, cleanup *) -Lemma gJoinInt (M : giryM (giryM T R) R) - (h : T -> \bar R) (mh : measurable_fun setT h) (h_ge0 : forall x, 0 <= h x) : +Lemma gJoinInt (M : giryM (giryM T R) R) (h : T -> \bar R) : + measurable_fun [set: T] h -> (forall x, 0 <= h x) -> gInt h (gJoin M) = gInt (fun μ : giryM T R => \int[μ]_x h x) M. Proof. +move=> mh h0. pose g := nnsfun_approx measurableT mh. pose gE := fun n => EFin \o (g n). have mgE n : measurable_fun setT (gE n) by exact/measurable_EFinP. @@ -475,117 +454,103 @@ End giry_join_meas_fun. Section giry_bind. Local Open Scope classical_set_scope. -Context d1 d2 - (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). - -Definition gBind (f : T1 -> giryM T2 R) (H : measurable_fun setT f) : giryM T1 R -> giryM T2 R := - (gJoin (R := R)) \o (gMap H (R := R)). +Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). +Definition gBind (f : T1 -> giryM T2 R) (mf : measurable_fun [set: T1] f) + : giryM T1 R -> giryM T2 R := + (gJoin (R := R)) \o (gMap mf (R := R)). -Lemma gBind_meas_fun (f : T1 -> giryM T2 R) (H : measurable_fun setT f) : measurable_fun setT (gBind H). +Lemma gBind_meas_fun (f : T1 -> giryM T2 R) (mf : measurable_fun [set: T1] f) : + measurable_fun [set: giryM T1 R] (gBind mf). Proof. - eapply (@measurable_comp _ _ _ _ _ _ setT). - { by eapply @measurableT. } - { by apply subsetT. } - { by apply gJoin_meas_fun. } - { by apply gMap_meas_fun. } +apply: (@measurable_comp _ _ _ _ _ _ setT) => //. + exact: gJoin_meas_fun. +exact: gMap_meas_fun. Qed. - End giry_bind. - Section giry_bind_meas_fun. Local Open Scope classical_set_scope. Local Open Scope ereal_scope. Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2). Context (R : realType). - -Lemma gBindInt_meas_fun (μ : giryM T1 R) (f : T1 -> giryM T2 R) (H : measurable_fun setT f) - (h : T2 -> \bar R) (mh : measurable_fun setT h) (Hhge0 : forall x, 0 <= h x) : - measurable_fun setT (fun x => gInt h (f x)). +Lemma gBindInt_meas_fun (μ : giryM T1 R) (f : T1 -> giryM T2 R) + (h : T2 -> \bar R) : measurable_fun [set: T1] f -> + measurable_fun [set: T2] h -> (forall x, 0 <= h x) -> + measurable_fun setT (fun x => gInt h (f x)). Proof. - eapply (@measurable_comp _ _ _ _ _ _ setT _ _ f). - { by eapply @measurableT. } - { by apply subsetT. } - { by apply gInt_meas_fun. } - { by apply H. } +move=> mf mh h0. +apply: (@measurable_comp _ _ _ _ _ _ setT _ _ f) => //. +exact: gInt_meas_fun. Qed. -Lemma gBindInt : - forall (μ : giryM T1 R) (f : T1 -> giryM T2 R) (H : measurable_fun setT f) (h : T2 -> \bar R) (mh : measurable_fun setT h) (Hhge0 : forall x, 0 <= h x), - gInt h (gBind H μ) = gInt (fun x => gInt h (f x)) μ. +Lemma gBindInt (μ : giryM T1 R) (f : T1 -> giryM T2 R) + (mf : measurable_fun [set: T1] f) (h : T2 -> \bar R) : + measurable_fun [set: T2] h -> (forall x, 0 <= h x) -> + gInt h (gBind mf μ) = gInt (fun x => gInt h (f x)) μ. Proof. - intros ??????. - rewrite /gBind /=. - rewrite gJoinInt; auto. - rewrite gMapInt; auto. - apply gInt_meas_fun; auto. - intros. - apply integral_ge0; auto. +move=> mh h0; rewrite /gBind /= gJoinInt// gMapInt//. + exact: gInt_meas_fun. +by move=> x; exact: integral_ge0. Qed. -Lemma gBindInt_rw (μ : giryM T1 R) (f : T1 -> giryM T2 R) (H : measurable_fun setT f) (h : T2 -> \bar R) (mh : measurable_fun setT h) (Hhge0 : forall x, 0 <= h x) : - \int[gBind H μ]_y h y = \int[μ]_x \int[f x]_y h y. -Proof. - apply gBindInt; auto. -Qed. +Lemma gBindInt_rw (μ : giryM T1 R) (f : T1 -> giryM T2 R) + (mf : measurable_fun [set: T1] f) (h : T2 -> \bar R) : + measurable_fun [set: T2] h -> (forall x, 0 <= h x) -> + \int[gBind mf μ]_y h y = \int[μ]_x \int[f x]_y h y. +Proof. exact: gBindInt. Qed. End giry_bind_meas_fun. Section giry_monad. Local Open Scope classical_set_scope. Local Open Scope ereal_scope. -Context d1 d2 d3 (T1 : measurableType d1) (T2 : measurableType d2) (T3 : measurableType d3). -Context (R : realType). +Context d1 d2 d3 (T1 : measurableType d1) (T2 : measurableType d2) + (T3 : measurableType d3) (R : realType). -Lemma gJoin_assoc : forall (x : giryM (giryM (giryM T1 R) R) R), - ((@gJoin _ _ R) \o (gMap (@gJoin_meas_fun _ _ R))) x ≡μ ((@gJoin _ _ R) \o (@gJoin _ _ R)) x. +Lemma gJoin_assoc (x : giryM (giryM (giryM T1 R) R) R) : + ((@gJoin _ _ R) \o (gMap (@gJoin_meas_fun _ _ R))) x ≡μ ((@gJoin _ _ R) \o (@gJoin _ _ R)) x. Proof. - intros μ S HmS. - rewrite /= /gJoin_ev. - rewrite gMapInt //. - rewrite gJoinInt //. - all: apply gEval_meas_fun; auto. +move=> S mS. +rewrite /= /gJoin_ev gMapInt//; last exact: gEval_meas_fun. +by rewrite gJoinInt//; exact: gEval_meas_fun. Qed. - -Lemma gJoin_id1 : forall (x : giryM T1 R), - ((@gJoin _ _ R) \o (gMap (@gRet_meas_fun _ _ R))) x ≡μ ((@gJoin _ _ R) \o (@gRet _ _ R)) x. +Lemma gJoin_id1 (x : giryM T1 R) : + ((@gJoin _ _ R) \o (gMap (@gRet_meas_fun _ _ R))) x + ≡μ ((@gJoin _ _ R) \o (@gRet _ _ R)) x. Proof. - intros μ S HmS. - rewrite /= /gJoin_ev; simpl. - rewrite gMapInt; auto; [|apply gEval_meas_fun; auto]. - rewrite gRetInt; auto; [|apply gEval_meas_fun; auto]. - rewrite /gInt /gEval /gRet /= /dirac. - rewrite integral_indic; auto. - rewrite setIT //. +move=> S mS. +rewrite /= /gJoin_ev. +rewrite gMapInt//; last exact: gEval_meas_fun. +rewrite gRetInt//; last exact: gEval_meas_fun. +by rewrite /gInt /gEval /gRet /= /dirac integral_indic// setIT. Qed. -Lemma gJoin_id2 : forall (x : giryM (giryM T1 R) R) (f : T1 -> T2) (H : measurable_fun setT f), - ((@gJoin _ _ R) \o gMap (gMap_meas_fun H)) x ≡μ (gMap H \o (@gJoin _ _ R)) x. +Lemma gJoin_id2 (x : giryM (giryM T1 R) R) (f : T1 -> T2) + (mf : measurable_fun [set: T1] f) : + ((@gJoin _ _ R) \o gMap (gMap_meas_fun mf)) x ≡μ (gMap mf \o (@gJoin _ _ R)) x. Proof. - intros μ f Hmf S HmS. - rewrite /= /gJoin_ev; simpl. - rewrite gMapInt; auto. - apply gEval_meas_fun; auto. +move=> X mS. +rewrite /= /gJoin_ev gMapInt//. +exact: gEval_meas_fun. Qed. - End giry_monad. Section giry_zero_def. Local Open Scope classical_set_scope. -Context d1 (T1 : measurableType d1) (R : realType). +Local Open Scope ereal_scope. +Context {d1} {T1 : measurableType d1} {R : realType}. + Definition gZero := mzero : giryM T1 R. -Lemma gZero_eval : forall S (H: d1.-measurable S), gZero S = (0% E). -Proof. - intros ??. - rewrite /gZero/mzero //. -Qed. -End giry_zero_def. +Lemma gZero_eval S : (*d1.-measurable S ->*) gZero S = 0. +Proof. by []. Qed. + +End giry_zero_def. Section giry_zero. Local Open Scope classical_set_scope. @@ -593,132 +558,105 @@ Local Open Scope classical_set_scope. Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2). Context (R : realType). -Lemma gZero_map : forall (f : T1 -> T2) (H : measurable_fun setT f), - gMap H (@gZero d1 T1 R) ≡μ (@gZero d2 T2 R). -Proof. - intros f H S HmS. - rewrite /=/gMap_ev /mzero //. -Qed. +Lemma gZero_map (f : T1 -> T2) (mf : measurable_fun [set: T1] f) : + gMap mf (@gZero d1 T1 R) ≡μ @gZero d2 T2 R. +Proof. by []. Qed. End giry_zero. - - Section giry_prod. Local Open Scope classical_set_scope. -Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2). -Context (R : realType). -Variable (μ12 : giryM T1 R * giryM T2 R). +Local Open Scope ereal_scope. +Context {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} {R : realType}. +Variable μ12 : giryM T1 R * giryM T2 R. (* https://en.wikipedia.org/wiki/Giry_monad#Product_distributions *) -Definition gProd_ev := (μ12.1 \x μ12.2)%E. +Definition gProd_ev := μ12.1 \x μ12.2. HB.instance Definition _ := Measure.on gProd_ev. -Let gProd_setT : (gProd_ev setT <= 1)%E. +Let gProd_setT : gProd_ev setT <= 1. Proof. -rewrite -setXTT [leLHS]product_measure1E// -[1%E]mule1. +rewrite -setXTT [leLHS]product_measure1E// -[leRHS]mule1. by rewrite lee_pmul// sprobability_setT. Qed. -HB.instance Definition _ := Measure_isSubProbability.Build _ _ _ gProd_ev gProd_setT. -Definition gProd : giryM (T1*T2)%type R := gProd_ev. +HB.instance Definition _ := + Measure_isSubProbability.Build _ _ _ gProd_ev gProd_setT. -(* gBind' (fun v1 => gBind' (gRet \o (pair v1)) (snd μ)) (fst μ). *) +Definition gProd : giryM (T1 * T2)%type R := gProd_ev. +(* gBind' (fun v1 => gBind' (gRet \o (pair v1)) (snd μ)) (fst μ). *) End giry_prod. - Section giry_prod_meas_fun. Local Open Scope classical_set_scope. Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2). Context (R : realType). (* TODO: Clean up, maybe move elsewhere *) -Lemma subprobability_prod_setC - (P : giryM T1 R * giryM T2 R) (A : set (prod T1 T2)) : +Lemma subprobability_prod_setC (P : giryM T1 R * giryM T2 R) (A : set (T1 * T2)) : measurable A -> ((P.1 \x P.2) (~` A) = (P.1 \x P.2) [set: T1 * T2] - (P.1 \x P.2) A)%E. Proof. -move=> mA. -rewrite -(setvU A) measureU//= ?addeK ?setICl//. +move=> mA; rewrite -(setvU A) measureU//= ?addeK ?setICl//. - rewrite -/(gProd_ev _). exact: fin_num_measure. - exact: measurableC. Qed. -(* - See "A synthetic approach to Markov kernels, conditional - independence and theorems on sufficient statistics", Fritz - - TODO: Clean up proof - *) -Lemma gProd_meas_fun : measurable_fun setT (@gProd d1 d2 T1 T2 R). +(* See Tobias Fritz, + A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics, + https://arxiv.org/abs/1908.07021 *) +Lemma gProd_meas_fun : measurable_fun [set: giryM T1 R * giryM T2 R] gProd. Proof. - simpl. - apply (@giryM_cod_meas_fun _ _ _ _ R (@gProd _ _ _ _ R)). - - rewrite measurable_prod_measurableType; simpl. - rewrite /gProd_ev. - apply dynkin_induction; simpl. - - rewrite measurable_prod_measurableType //. - - intros A B [A1 HA1 [A2 HA2 <-]] [B1 HB1 [B2 HB2 <-]]. - exists (A1 `&` B1); first exact: measurableI. - exists (A2 `&` B2); first exact: measurableI. - by rewrite setXI. - - eapply eq_measurable_fun; [intros ??; rewrite -setXTT product_measure1E // |]. - apply: emeasurable_funM; - apply: (@measurableT_comp _ _ _ _ _ _ (gEval _)) => //; +apply: (@giryM_cod_meas_fun _ _ _ _ R (@gProd _ _ _ _ R)) => /=. +rewrite measurable_prod_measurableType. +rewrite /gProd_ev. +apply: dynkin_induction => /=. +- by rewrite measurable_prod_measurableType. +- move=> _ _ [A1 mA1 [A2 mA2 <-]] [B1 mB1 [B2 mB2 <-]]. + exists (A1 `&` B1); first exact: measurableI. + exists (A2 `&` B2); first exact: measurableI. + by rewrite setXI. +- apply: (eq_measurable_fun (fun x : giryM T1 R * giryM T2 R => x.1 [set: T1] * x.2 [set: T2])%E). + by move=> x _; rewrite -setXTT product_measure1E. + by apply: emeasurable_funM => /=; + apply: (@measurableT_comp _ _ _ _ _ _ (gEval _)) => //; exact: gEval_meas_fun. +- move=> _ [A mA [B mB <-]]. +- apply: (eq_measurable_fun (fun x : giryM T1 R * giryM T2 R => x.1 A * x.2 B)%E). + by move=> x _; rewrite product_measure1E. + by apply: emeasurable_funM; + apply: (@measurableT_comp _ _ _ _ _ _ (gEval _)) => //; exact: gEval_meas_fun. +- move=> S mS HS. + apply: (eq_measurable_fun (fun x : giryM T1 R * giryM T2 R => + x.1 [set: T1] * x.2 [set: T2] - (x.1 \x x.2) S)%E). + by move=> /= x _; rewrite subprobability_prod_setC// -setXTT product_measure1E. + apply emeasurable_funB => //=. + by apply: emeasurable_funM => //=; apply: (@measurableT_comp _ _ _ _ _ _ (gEval _)) => //; exact: gEval_meas_fun. - - intros S [A HA [B HB <-]]. - eapply eq_measurable_fun; [intros ??; rewrite product_measure1E // |]. - apply: emeasurable_funM; - apply: (@measurableT_comp _ _ _ _ _ _ (gEval _)) => //; - exact: gEval_meas_fun. - - intros S HmS HS. - eapply (eq_measurable_fun). - intros ??. simpl in x. rewrite (subprobability_prod_setC x). - rewrite -setXTT product_measure1E; first by reflexivity. - by []. - by []. - by []. - apply emeasurable_funB; auto; simpl. - apply: emeasurable_funM; - apply: (@measurableT_comp _ _ _ _ _ _ (gEval _)) => //; - exact: gEval_meas_fun. - - intros F HmF HF Hn. - eapply eq_measurable_fun. - intros ??. - rewrite measure_semi_bigcup //. - apply bigcup_measurable; auto. - simpl. - apply ge0_emeasurable_sum; auto. +- move=> F mF tF Fn. + apply: (eq_measurable_fun (fun x : giryM T1 R * giryM T2 R => \sum_(0 <= k x _; rewrite measure_semi_bigcup//; exact: bigcup_measurable. + exact: ge0_emeasurable_sum. Qed. End giry_prod_meas_fun. - Section giry_prod_int. Local Open Scope classical_set_scope. Local Open Scope ereal_scope. -Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2). -Context (R : realType). +Context {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} {R : realType}. -Lemma gProdInt1 (μ1 : giryM T1 R) (μ2 : giryM T2 R) - (h : (T1 * T2)%type -> \bar R) (Hmh : measurable_fun setT h) (Hpos : forall x, 0 <= h x): +Lemma gProdInt1 (μ1 : giryM T1 R) (μ2 : giryM T2 R) (h : T1 * T2 -> \bar R) : + measurable_fun [set: T1 * T2] h -> (forall x, 0 <= h x) -> gInt h (gProd (μ1, μ2)) = gInt (fun x => gInt (fun y => h (x, y)) μ2 ) μ1. -Proof. - rewrite /gInt/=/gProd_ev/=. - rewrite fubini_tonelli1; auto. -Qed. +Proof. by move=> mh h0; rewrite /gInt/= /gProd_ev/= fubini_tonelli1. Qed. -Lemma gProdInt2 (μ1 : giryM T1 R) (μ2 : giryM T2 R) - (h : (T1 * T2)%type -> \bar R) (Hmh : measurable_fun setT h) (Hpos : forall x, 0 <= h x): +Lemma gProdInt2 (μ1 : giryM T1 R) (μ2 : giryM T2 R) (h : T1 * T2 -> \bar R) : + measurable_fun [set: T1 * T2] h -> (forall x, 0 <= h x) -> gInt h (gProd (μ1, μ2)) = gInt (fun y => gInt (fun x => h (x, y)) μ1 ) μ2. -Proof. - rewrite /gInt/=/gProd_ev/=. - rewrite fubini_tonelli2; auto. -Qed. +Proof. by move=> mh h0; rewrite /gInt/=/gProd_ev/= fubini_tonelli2. Qed. End giry_prod_int. From 77c3d46c7cd957468fe30711b3675b9f4cc7c1f7 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 12 Jul 2025 17:44:01 +0900 Subject: [PATCH 07/14] naming convention --- giry.v | 662 ------------------------------------------------ theories/giry.v | 581 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 581 insertions(+), 662 deletions(-) delete mode 100644 giry.v create mode 100644 theories/giry.v diff --git a/giry.v b/giry.v deleted file mode 100644 index f461beb2a3..0000000000 --- a/giry.v +++ /dev/null @@ -1,662 +0,0 @@ -From mathcomp Require Import all_ssreflect all_algebra boolp classical_sets. -From mathcomp Require Import fsbigop functions reals topology separation_axioms. -From mathcomp Require Import ereal sequences numfun measure measurable_realfun. -From mathcomp Require Import lebesgue_measure lebesgue_integral. -(* -From clutch.prob.monad Require Export prelude. -From clutch.prelude Require Import classical. -Import Coq.Relations.Relation_Definitions. -From Coq Require Import Classes.Morphisms Reals. - *) -From HB Require Import structures. - -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. - -Import Order.TTheory GRing.Theory Num.Def Num.Theory. - -(* TODO: small PR to measure.v? *) -Section mzero_subprobability. -Context d (T : measurableType d) (R : realType). - -Let mzero_setT : (@mzero d T R setT <= 1)%E. -Proof. by rewrite /mzero/=. Qed. - -HB.instance Definition _ := - Measure_isSubProbability.Build _ _ _ (@mzero d T R) mzero_setT. - -End mzero_subprobability. - -Section giryM_def. -Local Open Scope classical_set_scope. -Context d (T : measurableType d) (R : realType). - -Definition giryM : Type := @subprobability d T R. - -HB.instance Definition _ := gen_eqMixin giryM. -HB.instance Definition _ := gen_choiceMixin giryM. -HB.instance Definition _ := isPointed.Build giryM mzero. - -Definition gEval (S : set T) (mu : giryM) := mu S. - -Definition gEvalPreImg (S : set T) := - preimage_set_system setT (gEval S) measurable. - -Definition giry_measurable := <>. - -Let giry_measurable0 : giry_measurable set0. -Proof. exact: sigma_algebra0. Qed. - -Let giry_measurableC (S : set giryM) : - giry_measurable S -> giry_measurable (~` S). -Proof. exact: sigma_algebraC. Qed. - -Let giry_measurableU (A : (set giryM)^nat) : - (forall i, giry_measurable (A i)) -> giry_measurable (\bigcup_i A i). -Proof. exact: sigma_algebra_bigcup. Qed. - -Definition giry_display : measure_display. -Proof. by constructor. Qed. - -HB.instance Definition _ := - @isMeasurable.Build giry_display giryM giry_measurable - giry_measurable0 giry_measurableC giry_measurableU. - -End giryM_def. - -Definition measure_eq {d} {T : measurableType d} {R : realType} : - giryM T R -> giryM T R -> Prop := - fun μ1 μ2 => forall S : set T, measurable S -> μ1 S = μ2 S. -Notation "x ≡μ y" := (measure_eq x y) (at level 70). - -Global Hint Extern 0 (_ ≡μ _) => reflexivity : core. -Global Hint Extern 0 (_ ≡μ _) => symmetry; assumption : core. - -Section giry_eval. - -Local Open Scope ereal_scope. -Local Open Scope classical_set_scope. -Context d (T : measurableType d) (R : realType). - -(* TODO: Make hint *) -Lemma gEval_meas_fun (S : set T) : d.-measurable S -> - measurable_fun [set: giryM T R] (gEval S). -Proof. -move=> mS. -apply: (@measurability giry_display _ (@giryM _ T R) _ setT (@gEval _ _ R S) - (@measurable _ (\bar R))). - rewrite smallest_id//. - exact: sigma_algebra_measurable. -apply: subset_trans; last exact: sub_gen_smallest. -exact: (bigcup_sup mS). -Qed. - -End giry_eval. - -Section giry_integral. -Local Open Scope classical_set_scope. -Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType). - -Definition gInt (f : T -> \bar R) (mu : giryM T R) := \int[mu]_x f x. - -Import HBNNSimple. - -Lemma gInt_meas_fun (f : T -> \bar R) : - measurable_fun [set: T] f -> (forall x, 0 <= f x) -> - measurable_fun [set: giryM T R] (gInt f). -Proof. -(* - The idea is to reconstruct f from simple functions, then use - measurability of gEval. See "Codensity and the Giry monad", Avery - *) -move=> mf h0. -pose g := nnsfun_approx measurableT mf. -pose gE := fun n => EFin \o g n. -have mgE n : measurable_fun [set: T] (gE n) by exact/measurable_EFinP. -have gE0 n x : [set: T] x -> 0 <= (gE n) x by rewrite /gE /= // lee_fin. -have HgEmono x : [set: T] x -> {homo gE ^~ x : n m / (n <= m)%O >-> n <= m}. - by move=> _ n m nm; exact/lefP/nd_nnsfun_approx. -(* By MCT, limit of the integrals of g_n is the integral of the limit of g_n *) -have Hcvg := cvg_monotone_convergence _ mgE gE0 HgEmono. -pose gEInt := fun n μ => \int[μ]_x (gE n) x. -have mgEInt n : measurable_fun [set: giryM T R] (gEInt n). - rewrite /gEInt /gE /=. - apply (eq_measurable_fun (fun μ : giryM T R => - \sum_(x \in range (g n)) (x%:E * μ (g n @^-1` [set x])))). - by move=> μ Hμ; rewrite integralT_nnsfun sintegralE. - apply: emeasurable_fsum => // r. - have mg : d.-measurable (g n @^-1` [set r]) by []. - apply (measurable_funeM r%:E). - have : measurable_fun [set: giryM T R] (fun x : giryM T R => x (g n @^-1` [set r])); auto. - exact : eq_measurable_fun (gEval_meas_fun mg). -(* The μ ↦ int[mu] lim g_n is measurable if every μ ↦ int[mu] g_n is measurable *) -apply: (emeasurable_fun_cvg _ (fun μ : giryM T R => \int[μ]_x f x) mgEInt). -move=> μ Hμ. -rewrite /gEInt /=. -rewrite (eq_integral (fun x : T => limn (gE^~ x))). - exact: (Hcvg μ measurableT). -move=> x _; apply/esym/cvg_lim => //. -exact/cvg_nnsfun_approx. -Qed. - -End giry_integral. - -(* TODO: Everything below needs to be cleaned up *) - -Section giry_cod_meas. -Local Open Scope classical_set_scope. - - (* TODO: Either move this lemma to a more accessible location, or integrate within - the proof below *) -Let measurability_aux d d' (aT : measurableType d) (rT : measurableType d') - (f : aT -> rT) (G : set (set rT)) : - @measurable _ rT = <> -> - (forall (S : set rT), G S -> @measurable _ aT (f @^-1` S)) -> - measurable_fun [set: aT] f. -Proof. -move=> HG HS. -apply/(measurability G) => //. -apply/image_subP => A GA. -rewrite setTI. -exact: HS. -Qed. - -(* Adapted from mathlib induction_on_inter *) -(* TODO: Clean up proof, move lemma, change premises to use setX_closed like notations *) -Lemma dynkin_induction d {T : measurableType d} (G : set (set T)) (P : set_system T) : - @measurable _ T = <> -> - setI_closed G -> - P [set: T] -> - G `<=` P -> - (forall S, measurable S -> P S -> P (~` S)) -> - (forall F : (set T)^nat, - (forall n, measurable (F n)) -> - trivIset setT F -> - (forall n, P (F n)) -> P (\bigcup_k F k)) -> - (forall S, <> S -> P S). -Proof. -move=> HG GI HsetT Hgen HsetC Hbigcup S HGS. -have mS : measurable S by rewrite HG. -suff Haux : <> `<=` [set S : set T | measurable S /\ P S]. - by apply Haux. -apply lambda_system_subset; first by []. -- apply (dynkin_lambda_system ([set S0 | measurable S0 /\ P S0])). - split; first by []. - move=> A [mA PA]. - split; first exact: measurableC. - exact: HsetC. - move=> F tF Hm. - split. - apply bigcup_measurable; auto. - move=> k Hk. - by apply Hm. - apply: Hbigcup => //. - by apply Hm. - by apply Hm. -- move=> A GA; split; last exact: Hgen. - rewrite HG //. - exact: sub_gen_smallest. -- by []. -Qed. - -Lemma giryM_cod_meas_fun {d1} {d2} {T1 : measurableType d1} - {T2 : measurableType d2} {R : realType} (f : T1 -> giryM T2 R) : - (forall (S : set T2), measurable S -> measurable_fun setT (f ^~ S)) -> - measurable_fun [set: T1] f. -Proof. -move=> HS. -pose G : set_system (giryM T2 R) := \bigcup_(S in d2.-measurable) gEvalPreImg S. -apply: (measurability_aux (G := G)) => // S [U mU [M mB] <-]. -rewrite -comp_preimage. -exact: HS. -Qed. - -End giry_cod_meas. - -Section giry_map. -Local Open Scope classical_set_scope. -Local Open Scope ereal_scope. -Context {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} {R : realType}. - -Variables (f : T1 -> T2) (Hmf : measurable_fun [set: T1] f) (μ1 : giryM T1 R). - -Definition gMap_ev := pushforward μ1 f. - -Let gMap_ev0 : gMap_ev set0 = 0. -Proof. exact: measure0. Qed. - -Let gMap_ev_ge0 A : 0 <= gMap_ev A. -Proof. exact: measure_ge0. Qed. - -Let gMap_ev_sigma_additive : semi_sigma_additive gMap_ev. -Proof. exact: measure_semi_sigma_additive. Qed. - -HB.instance Definition _ := isMeasure.Build _ _ _ gMap_ev - gMap_ev0 gMap_ev_ge0 gMap_ev_sigma_additive. - -(* used to work before the change of definition of pushforward -HB.instance Definition _ := Measure.on gMap_ev. -the change of definition was maybe not a good idea... -https://github.com/math-comp/analysis/pull/1661 -*) - -Let gMap_setT : gMap_ev setT <= 1. -Proof. -by rewrite /gMap_ev /pushforward /= sprobability_setT. -Qed. - -HB.instance Definition _ := Measure_isSubProbability.Build _ _ _ gMap_ev gMap_setT. - -Definition gMap : giryM T2 R := gMap_ev. - -End giry_map. - -Section giry_map_meas. -Local Open Scope classical_set_scope. -Local Open Scope ereal_scope. -Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). - -Lemma gMap_to_int (f : T1 -> T2) (mf : measurable_fun [set: T1] f) - (μ1 : giryM T1 R) (S : set T2) : measurable S -> - gMap mf μ1 S = \int[μ1]_x (\1_S (f x))%:E. -Proof. -move=> mS. -rewrite -[in LHS](setIT S) -[LHS]integral_indic//. -rewrite ge0_integral_pushforward//. - exact/measurable_EFinP/measurable_indic. -by move=> y _; rewrite lee_fin. -Qed. - -Lemma gMap_meas_fun (f : T1 -> T2) (mf : measurable_fun [set: T1] f): - measurable_fun [set: giryM T1 R] (gMap mf (R:= R)). -Proof. -rewrite /gMap. -apply: (@giryM_cod_meas_fun _ _ (giryM T1 R)) => S mS. -rewrite /gMap_ev /pushforward /=. -apply: gEval_meas_fun. -rewrite -(setTI (f @^-1` S)). -exact: mf. -Qed. - -Lemma gMapInt (f : T1 -> T2) (mf : measurable_fun [set: T1] f) (μ : giryM T1 R) - (h : T2 -> \bar R) : - measurable_fun [set: T2] h -> (forall x, 0 <= h x) -> - gInt h (gMap mf μ) = gInt (h \o f) μ. -Proof. -by move=> mh h0; exact: ge0_integral_pushforward. -Qed. - -End giry_map_meas. - -Section giry_ret. -Local Open Scope classical_set_scope. -Local Open Scope ring_scope. -Local Open Scope ereal_scope. -Context {d} {T : measurableType d} {R : realType}. - -Definition gRet (x : T) : giryM T R := dirac^~ R x. - -Lemma gRet_meas_fun : measurable_fun [set: T] gRet. -Proof. -apply: giryM_cod_meas_fun. -exact: measurable_fun_dirac. -Qed. - -Lemma gRetInt (x : T) (h : T -> \bar R) : measurable_fun [set: T] h -> - gInt h (gRet x) = h x. -Proof. -move=> mh. -rewrite /gInt. -have : forall S, d.-measurable S -> S `<=` [set : T] -> gRet x S = dirac x S by []. -move/eq_measure_integral => ->//. -by rewrite integral_dirac// diracT mul1e. -Qed. - -Lemma gRetInt_rw (x : T) (h : T -> \bar R) : - measurable_fun [set: T] h -> \int[gRet x]_x h x = h x. -Proof. exact: gRetInt. Qed. - -End giry_ret. - -Section giry_join. -Local Open Scope classical_set_scope. -Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType). -Variable M : giryM (giryM T R) R. - -Definition gJoin_ev (S : set T) := gInt (gEval S) M. - -Let gJoin0 : gJoin_ev set0 = 0. -Proof. by rewrite /gJoin_ev /gEval /gInt integral0_eq. Qed. - -Let gJoin_ge0 A : 0 <= gJoin_ev A. -Proof. by rewrite /gJoin_ev integral_ge0. Qed. - -(* TODO: Cleaner proof? *) -Let gJoin_semi_sigma_additive : semi_sigma_additive (gJoin_ev). -Proof. -move=> F mF tF _. -rewrite /gJoin_ev /gInt /gEval /=. -rewrite [X in _ --> X](_ : _ = \int[M]_x \sum_(0 <= k mu _. - apply/esym/cvg_lim => //. - exact: measure_sigma_additive. -rewrite [X in X @ _](_ : _ = - (fun n => \int[M]_x \sum_(0 <= i < n) x (F i))); last first. - apply/funext => n. - rewrite -ge0_integral_sum// => m. - exact: gEval_meas_fun. -apply: cvg_monotone_convergence => //. -- move=> n; apply: emeasurable_sum => m. - exact: gEval_meas_fun. -- by move=> n x _; rewrite sume_ge0. -- by move=> x _ m n mn; exact: ereal_nondecreasing_series. -Qed. - -HB.instance Definition _ := isMeasure.Build d _ R gJoin_ev - gJoin0 gJoin_ge0 gJoin_semi_sigma_additive. - -(* TODO: Cleaner proof? *) -Let gJoin_setT : gJoin_ev setT <= 1. -Proof. -rewrite /gJoin_ev. -rewrite (@le_trans _ _ (\int[M]_x `|gEval setT x|))//; last first. - rewrite (@le_trans _ _ (1%E * M setT))//; last first. - by rewrite mul1e sprobability_setT. - rewrite integral_le_bound//. - exact: gEval_meas_fun. - apply/aeW => x _. - by rewrite gee0_abs// sprobability_setT. -rewrite ge0_le_integral//=. -- exact: gEval_meas_fun. -- by move=> x _; rewrite abse_ge0. -- by apply: measurableT_comp => //; exact: gEval_meas_fun. -- by move=> x _; rewrite gee0_abs. -Qed. - -HB.instance Definition _ := - Measure_isSubProbability.Build _ _ _ gJoin_ev gJoin_setT. - -Definition gJoin : giryM T R := gJoin_ev. - -End giry_join. - -Section giry_join_meas_fun. -Local Open Scope classical_set_scope. -Local Open Scope ereal_scope. -Context {d} {T : measurableType d} {R : realType}. - -Lemma gJoin_meas_fun : measurable_fun [set: giryM (giryM T R) R] (@gJoin d T R). -Proof. -apply: (@giryM_cod_meas_fun _ _ (giryM (giryM T _)_)) => S mS. -apply: (@gInt_meas_fun _ _ _ (gEval S)) => //=. -exact: gEval_meas_fun. -Qed. - -Import HBNNSimple. - -(* TODO: Messy proof, cleanup *) -Lemma gJoinSInt (M : giryM (giryM T R) R) (h : {nnsfun T >-> R}) : - sintegral (gJoin M) h = \int[M]_μ sintegral μ h. -Proof. -under eq_integral do rewrite sintegralE. -rewrite ge0_integral_fsum//; last 2 first. - by move=> r; apply: measurable_funeM; exact: gEval_meas_fun. - by move=> n x _; exact: nnsfun_mulemu_ge0. -rewrite sintegralE /=. -apply: fsbigop.eq_fsbigr => // r rh. -rewrite integralZl//. -have := finite_measure_integrable_cst M 1. -apply: le_integrable => //; first exact: gEval_meas_fun. -move=> mu _ /=. -rewrite normr1 gee0_abs// (le_trans _ (@sprobability_setT _ _ _ mu))//. -by rewrite le_measure// ?inE. -Qed. - -(* TODO: Messy proof, cleanup *) - -Lemma gJoinInt (M : giryM (giryM T R) R) (h : T -> \bar R) : - measurable_fun [set: T] h -> (forall x, 0 <= h x) -> - gInt h (gJoin M) = gInt (fun μ : giryM T R => \int[μ]_x h x) M. -Proof. -move=> mh h0. -pose g := nnsfun_approx measurableT mh. -pose gE := fun n => EFin \o (g n). -have mgE n : measurable_fun setT (gE n) by exact/measurable_EFinP. -have gE_ge0 n x : 0 <= gE n x by rewrite lee_fin. -have nd_gE x : {homo gE ^~ x : n m / (n <= m)%O >-> n <= m}. - by move=> *; exact/lefP/nd_nnsfun_approx. -(* By MCT, limit of the integrals of g_n is the integral of the limit of g_n *) -rewrite /gInt. -transitivity (limn (fun n => \int[gJoin M]_x gE n x)). - rewrite -monotone_convergence//. - apply: eq_integral => t _. - by apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. -transitivity (limn (fun n => \int[M]_μ \int[μ]_x gE n x)). - apply: congr_lim; apply/funext => n. - rewrite integralT_nnsfun. - rewrite gJoinSInt. - apply: eq_integral => x _. - by rewrite integralT_nnsfun. -rewrite -monotone_convergence//; last 3 first. - by move=> n; exact: gInt_meas_fun. - by move=> n x _; exact: integral_ge0. - by move=> x _ m n mn; apply: ge0_le_integral => // t _; exact: nd_gE. -apply: eq_integral => mu _. -rewrite -monotone_convergence//. -apply: eq_integral => t _. -by apply/cvg_lim => //; exact: cvg_nnsfun_approx. -Qed. - -End giry_join_meas_fun. - -Section giry_bind. -Local Open Scope classical_set_scope. -Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). - -Definition gBind (f : T1 -> giryM T2 R) (mf : measurable_fun [set: T1] f) - : giryM T1 R -> giryM T2 R := - (gJoin (R := R)) \o (gMap mf (R := R)). - -Lemma gBind_meas_fun (f : T1 -> giryM T2 R) (mf : measurable_fun [set: T1] f) : - measurable_fun [set: giryM T1 R] (gBind mf). -Proof. -apply: (@measurable_comp _ _ _ _ _ _ setT) => //. - exact: gJoin_meas_fun. -exact: gMap_meas_fun. -Qed. - -End giry_bind. - -Section giry_bind_meas_fun. -Local Open Scope classical_set_scope. -Local Open Scope ereal_scope. -Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2). -Context (R : realType). - -Lemma gBindInt_meas_fun (μ : giryM T1 R) (f : T1 -> giryM T2 R) - (h : T2 -> \bar R) : measurable_fun [set: T1] f -> - measurable_fun [set: T2] h -> (forall x, 0 <= h x) -> - measurable_fun setT (fun x => gInt h (f x)). -Proof. -move=> mf mh h0. -apply: (@measurable_comp _ _ _ _ _ _ setT _ _ f) => //. -exact: gInt_meas_fun. -Qed. - -Lemma gBindInt (μ : giryM T1 R) (f : T1 -> giryM T2 R) - (mf : measurable_fun [set: T1] f) (h : T2 -> \bar R) : - measurable_fun [set: T2] h -> (forall x, 0 <= h x) -> - gInt h (gBind mf μ) = gInt (fun x => gInt h (f x)) μ. -Proof. -move=> mh h0; rewrite /gBind /= gJoinInt// gMapInt//. - exact: gInt_meas_fun. -by move=> x; exact: integral_ge0. -Qed. - -Lemma gBindInt_rw (μ : giryM T1 R) (f : T1 -> giryM T2 R) - (mf : measurable_fun [set: T1] f) (h : T2 -> \bar R) : - measurable_fun [set: T2] h -> (forall x, 0 <= h x) -> - \int[gBind mf μ]_y h y = \int[μ]_x \int[f x]_y h y. -Proof. exact: gBindInt. Qed. - -End giry_bind_meas_fun. - -Section giry_monad. -Local Open Scope classical_set_scope. -Local Open Scope ereal_scope. -Context d1 d2 d3 (T1 : measurableType d1) (T2 : measurableType d2) - (T3 : measurableType d3) (R : realType). - -Lemma gJoin_assoc (x : giryM (giryM (giryM T1 R) R) R) : - ((@gJoin _ _ R) \o (gMap (@gJoin_meas_fun _ _ R))) x ≡μ ((@gJoin _ _ R) \o (@gJoin _ _ R)) x. -Proof. -move=> S mS. -rewrite /= /gJoin_ev gMapInt//; last exact: gEval_meas_fun. -by rewrite gJoinInt//; exact: gEval_meas_fun. -Qed. - -Lemma gJoin_id1 (x : giryM T1 R) : - ((@gJoin _ _ R) \o (gMap (@gRet_meas_fun _ _ R))) x - ≡μ ((@gJoin _ _ R) \o (@gRet _ _ R)) x. -Proof. -move=> S mS. -rewrite /= /gJoin_ev. -rewrite gMapInt//; last exact: gEval_meas_fun. -rewrite gRetInt//; last exact: gEval_meas_fun. -by rewrite /gInt /gEval /gRet /= /dirac integral_indic// setIT. -Qed. - -Lemma gJoin_id2 (x : giryM (giryM T1 R) R) (f : T1 -> T2) - (mf : measurable_fun [set: T1] f) : - ((@gJoin _ _ R) \o gMap (gMap_meas_fun mf)) x ≡μ (gMap mf \o (@gJoin _ _ R)) x. -Proof. -move=> X mS. -rewrite /= /gJoin_ev gMapInt//. -exact: gEval_meas_fun. -Qed. - -End giry_monad. - -Section giry_zero_def. -Local Open Scope classical_set_scope. -Local Open Scope ereal_scope. -Context {d1} {T1 : measurableType d1} {R : realType}. - -Definition gZero := mzero : giryM T1 R. - -Lemma gZero_eval S : (*d1.-measurable S ->*) gZero S = 0. -Proof. by []. Qed. - -End giry_zero_def. - -Section giry_zero. -Local Open Scope classical_set_scope. - -Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2). -Context (R : realType). - -Lemma gZero_map (f : T1 -> T2) (mf : measurable_fun [set: T1] f) : - gMap mf (@gZero d1 T1 R) ≡μ @gZero d2 T2 R. -Proof. by []. Qed. - -End giry_zero. - -Section giry_prod. -Local Open Scope classical_set_scope. -Local Open Scope ereal_scope. -Context {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} {R : realType}. -Variable μ12 : giryM T1 R * giryM T2 R. - -(* https://en.wikipedia.org/wiki/Giry_monad#Product_distributions *) -Definition gProd_ev := μ12.1 \x μ12.2. - -HB.instance Definition _ := Measure.on gProd_ev. - -Let gProd_setT : gProd_ev setT <= 1. -Proof. -rewrite -setXTT [leLHS]product_measure1E// -[leRHS]mule1. -by rewrite lee_pmul// sprobability_setT. -Qed. - -HB.instance Definition _ := - Measure_isSubProbability.Build _ _ _ gProd_ev gProd_setT. - -Definition gProd : giryM (T1 * T2)%type R := gProd_ev. - -(* gBind' (fun v1 => gBind' (gRet \o (pair v1)) (snd μ)) (fst μ). *) - -End giry_prod. - -Section giry_prod_meas_fun. -Local Open Scope classical_set_scope. -Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2). -Context (R : realType). - -(* TODO: Clean up, maybe move elsewhere *) -Lemma subprobability_prod_setC (P : giryM T1 R * giryM T2 R) (A : set (T1 * T2)) : - measurable A -> - ((P.1 \x P.2) (~` A) = (P.1 \x P.2) [set: T1 * T2] - (P.1 \x P.2) A)%E. -Proof. -move=> mA; rewrite -(setvU A) measureU//= ?addeK ?setICl//. -- rewrite -/(gProd_ev _). - exact: fin_num_measure. -- exact: measurableC. -Qed. - -(* See Tobias Fritz, - A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics, - https://arxiv.org/abs/1908.07021 *) -Lemma gProd_meas_fun : measurable_fun [set: giryM T1 R * giryM T2 R] gProd. -Proof. -apply: (@giryM_cod_meas_fun _ _ _ _ R (@gProd _ _ _ _ R)) => /=. -rewrite measurable_prod_measurableType. -rewrite /gProd_ev. -apply: dynkin_induction => /=. -- by rewrite measurable_prod_measurableType. -- move=> _ _ [A1 mA1 [A2 mA2 <-]] [B1 mB1 [B2 mB2 <-]]. - exists (A1 `&` B1); first exact: measurableI. - exists (A2 `&` B2); first exact: measurableI. - by rewrite setXI. -- apply: (eq_measurable_fun (fun x : giryM T1 R * giryM T2 R => x.1 [set: T1] * x.2 [set: T2])%E). - by move=> x _; rewrite -setXTT product_measure1E. - by apply: emeasurable_funM => /=; - apply: (@measurableT_comp _ _ _ _ _ _ (gEval _)) => //; exact: gEval_meas_fun. -- move=> _ [A mA [B mB <-]]. -- apply: (eq_measurable_fun (fun x : giryM T1 R * giryM T2 R => x.1 A * x.2 B)%E). - by move=> x _; rewrite product_measure1E. - by apply: emeasurable_funM; - apply: (@measurableT_comp _ _ _ _ _ _ (gEval _)) => //; exact: gEval_meas_fun. -- move=> S mS HS. - apply: (eq_measurable_fun (fun x : giryM T1 R * giryM T2 R => - x.1 [set: T1] * x.2 [set: T2] - (x.1 \x x.2) S)%E). - by move=> /= x _; rewrite subprobability_prod_setC// -setXTT product_measure1E. - apply emeasurable_funB => //=. - by apply: emeasurable_funM => //=; apply: (@measurableT_comp _ _ _ _ _ _ (gEval _)) => //; - exact: gEval_meas_fun. -- move=> F mF tF Fn. - apply: (eq_measurable_fun (fun x : giryM T1 R * giryM T2 R => \sum_(0 <= k x _; rewrite measure_semi_bigcup//; exact: bigcup_measurable. - exact: ge0_emeasurable_sum. -Qed. - -End giry_prod_meas_fun. - -Section giry_prod_int. -Local Open Scope classical_set_scope. -Local Open Scope ereal_scope. -Context {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} {R : realType}. - -Lemma gProdInt1 (μ1 : giryM T1 R) (μ2 : giryM T2 R) (h : T1 * T2 -> \bar R) : - measurable_fun [set: T1 * T2] h -> (forall x, 0 <= h x) -> - gInt h (gProd (μ1, μ2)) = gInt (fun x => gInt (fun y => h (x, y)) μ2 ) μ1. -Proof. by move=> mh h0; rewrite /gInt/= /gProd_ev/= fubini_tonelli1. Qed. - -Lemma gProdInt2 (μ1 : giryM T1 R) (μ2 : giryM T2 R) (h : T1 * T2 -> \bar R) : - measurable_fun [set: T1 * T2] h -> (forall x, 0 <= h x) -> - gInt h (gProd (μ1, μ2)) = gInt (fun y => gInt (fun x => h (x, y)) μ1 ) μ2. -Proof. by move=> mh h0; rewrite /gInt/=/gProd_ev/= fubini_tonelli2. Qed. - -End giry_prod_int. diff --git a/theories/giry.v b/theories/giry.v new file mode 100644 index 0000000000..6a4a63a4a3 --- /dev/null +++ b/theories/giry.v @@ -0,0 +1,581 @@ +From HB Require Import structures. +From mathcomp Require Import all_ssreflect all_algebra boolp classical_sets. +From mathcomp Require Import fsbigop functions reals topology separation_axioms. +From mathcomp Require Import ereal sequences numfun measure measurable_realfun. +From mathcomp Require Import lebesgue_measure lebesgue_integral. + +(**md**************************************************************************) +(* # The Giry monad *) +(* *) +(* giry T R == the type of subprobability measures over T *) +(* giry_ev P A == the evaluation map `giryM T R -> [0, 1]` *) +(* giry_int mu f := \int[mu]_x f x *) +(* giry_ret x == the unit of the Giry monad, i.e., \d_x *) +(* @giry_join _ T R == the multiplication of the Giry monad *) +(* type : giry (giry T R) R -> giry T R *) +(* giry_map mf == the map of type giry T1 R -> giry T2 R *) +(* where mf is a proof that f : T1 -> T2 is measurable *) +(* giry_bind mu mf == the bind with mu : giry T1 R and f : T1 -> giry T2 R *) +(* giry_prod == product of type *) +(* giry T1 R * giry T2 R -> giry (T1 * T2) R *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Import Order.TTheory GRing.Theory Num.Def Num.Theory. + +(* TODO: PR to measure.v? *) +Section mzero_subprobability. +Context d (T : measurableType d) (R : realType). + +Let mzero_setT : (@mzero d T R setT <= 1)%E. +Proof. by rewrite /mzero/=. Qed. + +HB.instance Definition _ := + Measure_isSubProbability.Build _ _ _ (@mzero d T R) mzero_setT. + +End mzero_subprobability. + +Section giry_def. +Local Open Scope classical_set_scope. +Context d (T : measurableType d) (R : realType). + +Definition giry : Type := @subprobability d T R. + +HB.instance Definition _ := gen_eqMixin giry. +HB.instance Definition _ := gen_choiceMixin giry. +HB.instance Definition _ := isPointed.Build giry mzero. + +Definition giry_ev (mu : giry) (A : set T) := mu A. + +Definition preimg_giry_ev (A : set T) : set_system giry := + preimage_set_system [set: giry] (giry_ev ^~ A) measurable. + +Definition giry_measurable := <>. + +Let giry_measurable0 : giry_measurable set0. +Proof. exact: sigma_algebra0. Qed. + +Let giry_measurableC (U : set giry) : + giry_measurable U -> giry_measurable (~` U). +Proof. exact: sigma_algebraC. Qed. + +Let giry_measurableU (F : (set giry)^nat) : + (forall i, giry_measurable (F i)) -> giry_measurable (\bigcup_i F i). +Proof. exact: sigma_algebra_bigcup. Qed. + +Definition giry_display : measure_display. +Proof. by constructor. Qed. + +HB.instance Definition _ := + @isMeasurable.Build giry_display giry giry_measurable + giry_measurable0 giry_measurableC giry_measurableU. + +(* TODO: Make hint? *) +Lemma measurable_giry_ev (A : set T) : measurable A -> + measurable_fun [set: giry] (giry_ev ^~ A). +Proof. +move=> mS. +apply: (@measurability giry_display _ giry _ setT (giry_ev ^~ A) measurable). + by rewrite smallest_id//; exact: sigma_algebra_measurable. +apply: subset_trans; last exact: sub_gen_smallest. +exact: (bigcup_sup mS). +Qed. + +End giry_def. +Arguments giry_ev {d T R} mu A. + +Definition measure_eq {d} {T : measurableType d} {R : realType} : + giry T R -> giry T R -> Prop := + fun μ1 μ2 => forall S : set T, measurable S -> μ1 S = μ2 S. +Notation "x ≡μ y" := (measure_eq x y) (at level 70). + +Global Hint Extern 0 (_ ≡μ _) => reflexivity : core. + +Section giry_integral. +Local Open Scope classical_set_scope. +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType). + +Definition giry_int (mu : giry T R) (f : T -> \bar R) := \int[mu]_x f x. + +Import HBNNSimple. + +Lemma measurable_giry_int (f : T -> \bar R) : + measurable_fun [set: T] f -> (forall x, 0 <= f x) -> + measurable_fun [set: giry T R] (giry_int ^~ f). +Proof. +(* + The idea is to reconstruct f from simple functions, then use measurability of giry_ev. + Tom Avery. Codensity and the Giry monad. https://arxiv.org/pdf/1410.4432. + *) +move=> mf h0. +pose g := nnsfun_approx measurableT mf. +pose gE := fun n => EFin \o g n. +have mgE n : measurable_fun [set: T] (gE n) by exact/measurable_EFinP. +have gE0 n x : [set: T] x -> 0 <= (gE n) x by rewrite /gE /= // lee_fin. +have HgEmono x : [set: T] x -> {homo gE ^~ x : n m / (n <= m)%O >-> n <= m}. + by move=> _ n m nm; exact/lefP/nd_nnsfun_approx. +(* By MCT, limit of the integrals of g_n is the integral of the limit of g_n *) +have Hcvg := cvg_monotone_convergence _ mgE gE0 HgEmono. +pose gEInt := fun n μ => \int[μ]_x (gE n) x. +have mgEInt n : measurable_fun [set: giry T R] (gEInt n). + rewrite /gEInt /gE /=. + apply (eq_measurable_fun (fun μ : giry T R => + \sum_(x \in range (g n)) x%:E * μ (g n @^-1` [set x]))). + by move=> μ Hμ; rewrite integralT_nnsfun sintegralE. + apply: emeasurable_fsum => // r. + apply: measurable_funeM. + exact: measurable_giry_ev. +(* The μ ↦ int[mu] lim g_n is measurable if every μ ↦ int[mu] g_n is measurable *) +apply: (emeasurable_fun_cvg _ (fun μ : giry T R => \int[μ]_x f x) mgEInt). +move=> μ Hμ. +rewrite /gEInt /=. +rewrite (eq_integral (fun x : T => limn (gE ^~ x))). + exact: (Hcvg μ measurableT). +move=> x _; apply/esym/cvg_lim => //. +exact/cvg_nnsfun_approx. +Qed. + +End giry_integral. +Arguments giry_int {d T R} mu f. + +Local Open Scope classical_set_scope. +(* Adapted from mathlib induction_on_inter *) +(* TODO: change premises to use setX_closed like notations *) +Lemma dynkin_induction d {T : measurableType d} (G : set (set T)) + (P : set_system T) : + @measurable _ T = <> -> + setI_closed G -> + P [set: T] -> + G `<=` P -> + (forall S, measurable S -> P S -> P (~` S)) -> + (forall F : (set T)^nat, + (forall n, measurable (F n)) -> + trivIset setT F -> + (forall n, P (F n)) -> P (\bigcup_k F k)) -> + (forall S, <> S -> P S). +Proof. +move=> GE GI PsetT GP PsetC Pbigcup A sGA. +suff: <> `<=` [set A | measurable A /\ P A] by move=> /(_ _ sGA)[]. +apply: lambda_system_subset; [by []| | |by []]. +- apply/dynkin_lambda_system; split => //. + + by move=> B [mB PB]; split; [exact: measurableC|exact: PsetC]. + + move=> F tF Hm; split. + by apply: bigcup_measurable => k _; apply Hm. + by apply: Pbigcup => //; apply Hm. +- move=> B GB; split; last exact: GP. + by rewrite GE; exact: sub_gen_smallest. +Qed. +Local Close Scope classical_set_scope. + +Section measurable_giry_codensity. +Local Open Scope classical_set_scope. + +(* TODO: move this lemma to a more accessible location? *) +Let measurability_image_sub d d' (aT : measurableType d) (rT : measurableType d') + (f : aT -> rT) (G : set (set rT)) : + @measurable _ rT = <> -> + (forall B, G B -> measurable (f @^-1` B)) -> + measurable_fun [set: aT] f. +Proof. +move=> GE Gf; apply/(measurability G) => //. +by apply/image_subP => A /Gf; rewrite setTI. +Qed. + +Lemma measurable_giry_codensity {d1} {d2} {T1 : measurableType d1} + {T2 : measurableType d2} {R : realType} (f : T1 -> giry T2 R) : + (forall B, measurable B -> measurable_fun [set: T1] (f ^~ B)) -> + measurable_fun [set: T1] f. +Proof. +move=> mf. +pose G : set_system (giry T2 R) := \bigcup_(B in measurable) preimg_giry_ev B. +apply: (measurability_image_sub (G := G)) => // _ [B mB [Y mY] <-]. +exact: mf. +Qed. + +End measurable_giry_codensity. + +Section giry_map. +Local Open Scope classical_set_scope. +Local Open Scope ereal_scope. +Context {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} {R : realType}. + +Variables (f : T1 -> T2) (mf : measurable_fun [set: T1] f) (mu1 : giry T1 R). + +Let map := pushforward mu1 f. + +Let map0 : map set0 = 0. Proof. exact: measure0. Qed. + +Let map_ge0 A : 0 <= map A. Proof. exact: measure_ge0. Qed. + +Let map_sigma_additive : semi_sigma_additive map. +Proof. exact: measure_semi_sigma_additive. Qed. + +HB.instance Definition _ := isMeasure.Build _ _ _ map + map0 map_ge0 map_sigma_additive. + +(* used to work before the change of definition of pushforward +HB.instance Definition _ := Measure.on gMap_ev. +the change of definition was maybe not a good idea... +https://github.com/math-comp/analysis/pull/1661 +*) + +Let map_setT : map [set: T2] <= 1. +Proof. by rewrite /map /pushforward /= sprobability_setT. Qed. + +HB.instance Definition _ := Measure_isSubProbability.Build _ _ _ map map_setT. + +Definition giry_map : giry T2 R := map. + +End giry_map. + +Section giry_map_meas. +Local Open Scope classical_set_scope. +Local Open Scope ereal_scope. +Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). +Implicit Type f : T1 -> T2. + +Lemma giry_int_map f (mf : measurable_fun [set: T1] f) + (mu : giry T1 R) (h : T2 -> \bar R) : + measurable_fun [set: T2] h -> (forall x, 0 <= h x) -> + giry_int (giry_map mf mu) h = giry_int mu (h \o f). +Proof. by move=> mh h0; exact: ge0_integral_pushforward. Qed. + +Lemma giry_mapE f (mf : measurable_fun [set: T1] f) + (mu1 : giry T1 R) (B : set T2) : measurable B -> + giry_map mf mu1 B = \int[mu1]_x (\d_(f x))%R B. +Proof. +move=> mA. +rewrite -[in LHS](setIT B) -[LHS]integral_indic// [LHS]giry_int_map//. + exact/measurable_EFinP/measurable_indic. +by move=> ?; rewrite lee_fin. +Qed. + +Lemma measurable_giry_map f (mf : measurable_fun [set: T1] f) : + measurable_fun [set: giry T1 R] (giry_map mf). +Proof. +rewrite /giry_map. +apply: (@measurable_giry_codensity _ _ (giry T1 R)) => B mB. +apply: measurable_giry_ev. +by rewrite -(setTI (f @^-1` B)); exact: mf. +Qed. + +End giry_map_meas. + +Section giry_ret. +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. +Local Open Scope ereal_scope. +Context {d} {T : measurableType d} {R : realType}. + +Definition giry_ret (x : T) : giry T R := \d_x. + +Lemma measurable_giry_ret : measurable_fun [set: T] giry_ret. +Proof. by apply: measurable_giry_codensity; exact: measurable_fun_dirac. Qed. + +Lemma giry_int_ret (x : T) (f : T -> \bar R) : measurable_fun [set: T] f -> + giry_int (giry_ret x) f = f x. +Proof. +by move=> mf; rewrite /giry_int /giry_ret integral_dirac// diracT mul1e. +Qed. + +End giry_ret. + +Section giry_join. +Local Open Scope classical_set_scope. +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType). +Variable M : giry (giry T R) R. + +Let join A := giry_int M (giry_ev ^~ A). + +Let join0 : join set0 = 0. +Proof. by rewrite /join /giry_ev /giry_int/= integral0_eq. Qed. + +Let join_ge0 A : 0 <= join A. Proof. by rewrite /join integral_ge0. Qed. + +Let join_semi_sigma_additive : semi_sigma_additive join. +Proof. +move=> F mF tF _; rewrite [X in _ --> X](_ : _ = + giry_int M (fun x => \sum_(0 <= k mu _. + by apply/esym/cvg_lim => //; exact: measure_sigma_additive. +rewrite [X in X @ _](_ : _ = + (fun n => giry_int M (fun mu => \sum_(0 <= i < n) mu (F i)))); last first. + apply/funext => n; rewrite -ge0_integral_sum//. + by move=> ?; exact: measurable_giry_ev. +apply: cvg_monotone_convergence => //. +- by move=> n; apply: emeasurable_sum => m; exact: measurable_giry_ev. +- by move=> n x _; rewrite sume_ge0. +- by move=> x _ m n mn; exact: ereal_nondecreasing_series. +Qed. + +HB.instance Definition _ := isMeasure.Build d _ R join + join0 join_ge0 join_semi_sigma_additive. + +Let join_setT : join [set: T] <= 1. +Proof. +rewrite (@le_trans _ _ (\int[M]_x `|giry_ev x [set: T]|))//; last first. + rewrite (le_trans _ (@sprobability_setT _ _ _ M))//. + rewrite -[leRHS]mul1e integral_le_bound//. + exact: measurable_giry_ev. + by apply/aeW => x _; rewrite gee0_abs// sprobability_setT. +rewrite ge0_le_integral//=. +- exact: measurable_giry_ev. +- by move=> x _; rewrite abse_ge0. +- by apply: measurableT_comp => //; exact: measurable_giry_ev. +- by move=> x _; rewrite gee0_abs. +Qed. + +HB.instance Definition _ := Measure_isSubProbability.Build _ _ _ join join_setT. + +Definition giry_join : giry T R := join. + +End giry_join. +Arguments giry_join {d T R}. + +Section measurable_giry_join. +Local Open Scope classical_set_scope. +Local Open Scope ereal_scope. +Context {d} {T : measurableType d} {R : realType}. + +Lemma measurable_giry_join : measurable_fun [set: giry (giry T R) R] giry_join. +Proof. +apply: measurable_giry_codensity => B mB/=. +by apply: measurable_giry_int => //; exact: measurable_giry_ev. +Qed. + +Import HBNNSimple. + +Lemma sintegral_giry_join (M : giry (giry T R) R) (h : {nnsfun T >-> R}) : + sintegral (giry_join M) h = \int[M]_mu sintegral mu h. +Proof. +under eq_integral do rewrite sintegralE. +rewrite ge0_integral_fsum//; last 2 first. + by move=> r; apply: measurable_funeM; exact: measurable_giry_ev. + by move=> n x _; exact: nnsfun_mulemu_ge0. +rewrite sintegralE /=. +apply: fsbigop.eq_fsbigr => // r rh. +rewrite integralZl//. +have := finite_measure_integrable_cst M 1. +apply: le_integrable => //; first exact: measurable_giry_ev. +move=> mu _ /=. +rewrite normr1 (le_trans _ (@sprobability_setT _ _ _ mu))// gee0_abs//. +by rewrite le_measure// ?inE. +Qed. + +Lemma giry_int_join (M : giry (giry T R) R) (h : T -> \bar R) : + measurable_fun [set: T] h -> (forall x, 0 <= h x) -> + giry_int (giry_join M) h = giry_int M (giry_int ^~ h). +Proof. +move=> mh h0. +pose g := nnsfun_approx measurableT mh. +pose gE := fun n => EFin \o g n. +have mgE n : measurable_fun [set: T] (gE n) by exact/measurable_EFinP. +have gE_ge0 n x : 0 <= gE n x by rewrite lee_fin. +have nd_gE x : {homo gE ^~ x : n m / (n <= m)%O >-> n <= m}. + by move=> *; exact/lefP/nd_nnsfun_approx. +rewrite /giry_int. +transitivity (limn (fun n => \int[giry_join M]_x gE n x)). + rewrite -monotone_convergence//; apply: eq_integral => t _. + by apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. +transitivity (limn (fun n => \int[M]_mu \int[mu]_x gE n x)). + apply: congr_lim; apply/funext => n. + rewrite integralT_nnsfun sintegral_giry_join; apply: eq_integral => x _. + by rewrite integralT_nnsfun. +rewrite -monotone_convergence//; last 3 first. + by move=> n; exact: measurable_giry_int. + by move=> n x _; exact: integral_ge0. + by move=> x _ m n mn; apply: ge0_le_integral => // t _; exact: nd_gE. +apply: eq_integral => mu _. +rewrite -monotone_convergence//. +apply: eq_integral => t _. +by apply/cvg_lim => //; exact: cvg_nnsfun_approx. +Qed. + +End measurable_giry_join. + +Reserved Notation "m >>= f" (at level 49). + +Section giry_bind. +Local Open Scope classical_set_scope. +Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). +Implicit Types (mu : giry T1 R) (f : T1 -> giry T2 R). + +Definition giry_bind mu f (mf : measurable_fun [set: T1] f) : giry T2 R := + (giry_join \o giry_map mf) mu. + +Local Notation "m >>= mf" := (giry_bind m mf). + +Lemma measurable_giry_bind f (mf : measurable_fun [set: T1] f) : + measurable_fun [set: giry T1 R] (fun mu => mu >>= mf). +Proof. +apply: (@measurableT_comp _ _ _ _ _ _ _ _ (giry_map mf)) => //=. + exact: measurable_giry_join. +exact: measurable_giry_map. +Qed. + +Lemma giry_int_bind mu f (mf : measurable_fun [set: T1] f) (h : T2 -> \bar R) : + measurable_fun [set: T2] h -> (forall x, 0 <= h x)%E -> + giry_int (mu >>= mf) h = giry_int mu (fun x => giry_int (f x) h). +Proof. +move=> mh h0; rewrite /giry_bind /= giry_int_join// giry_int_map//. + exact: measurable_giry_int. +by move=> ?; exact: integral_ge0. +Qed. + +End giry_bind. + +Section giry_monad. +Local Open Scope classical_set_scope. +Local Open Scope ereal_scope. +Context d1 d2 d3 (T1 : measurableType d1) (T2 : measurableType d2) + (T3 : measurableType d3) (R : realType). + +Lemma giry_joinA (x : giry (giry (giry T1 R) R) R) : + (giry_join \o giry_map measurable_giry_join) x ≡μ + (giry_join \o giry_join) x. +Proof. +move=> A mA/=. +rewrite giry_int_map//; last exact: measurable_giry_ev. +by rewrite giry_int_join//; exact: measurable_giry_ev. +Qed. + +Lemma giry_join_id1 (x : giry T1 R) : + (giry_join \o giry_map measurable_giry_ret) x ≡μ + (giry_join \o giry_ret) x. +Proof. +move=> A mA/=. +rewrite giry_int_map//; last exact: measurable_giry_ev. +rewrite giry_int_ret//; last exact: measurable_giry_ev. +by rewrite /giry_int /giry_ev /giry_ret/= /dirac integral_indic// setIT. +Qed. + +Lemma giry_join_id2 (x : giry (giry T1 R) R) (f : T1 -> T2) + (mf : measurable_fun [set: T1] f) : + (giry_join \o giry_map (measurable_giry_map mf)) x ≡μ + (giry_map mf \o giry_join) x. +Proof. +by move=> X mS /=; rewrite giry_int_map//; exact: measurable_giry_ev. +Qed. + +End giry_monad. + +Section giry_map_zero. +Local Open Scope classical_set_scope. +Context {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} + {R : realType}. + +Lemma giry_map_zero (f : T1 -> T2) (mf : measurable_fun [set: T1] f) : + giry_map mf (@mzero d1 T1 R) ≡μ @mzero d2 T2 R. +Proof. by []. Qed. + +End giry_map_zero. + +Section giry_prod. +Local Open Scope classical_set_scope. +Local Open Scope ereal_scope. +Context {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} {R : realType}. +Variable μ12 : giry T1 R * giry T2 R. + +(* https://en.wikipedia.org/wiki/Giry_monad#Product_distributions *) +Let prod := μ12.1 \x μ12.2. + +HB.instance Definition _ := Measure.on prod. + +Let prod_setT : prod setT <= 1. +Proof. +rewrite -setXTT [leLHS]product_measure1E// -[leRHS]mule1. +by rewrite lee_pmul// sprobability_setT. +Qed. + +HB.instance Definition _ := + Measure_isSubProbability.Build _ _ _ prod prod_setT. + +Definition giry_prod : giry (T1 * T2)%type R := prod. + +(* gBind' (fun v1 => gBind' (gRet \o (pair v1)) (snd μ)) (fst μ). *) + +End giry_prod. + +Section measurable_giry_prod. +Local Open Scope classical_set_scope. +Local Open Scope ereal_scope. +Context {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} + {R : realType}. + +(* TODO: Clean up, maybe move elsewhere *) +Lemma subprobability_prod_setC (P : giry T1 R * giry T2 R) (A : set (T1 * T2)) : + measurable A -> + (P.1 \x P.2) (~` A) = (P.1 \x P.2) [set: T1 * T2] - (P.1 \x P.2) A. +Proof. +move=> mA; rewrite -(setvU A) measureU//= ?addeK ?setICl//. +- by rewrite (_ : (_ \x _)%E = giry_prod P)// fin_num_measure. +- exact: measurableC. +Qed. + +(* See: Tobias Fritz. A synthetic approach to Markov kernels, conditional + independence and theorems on sufficient statistics. + https://arxiv.org/abs/1908.07021 *) +Lemma measurable_giry_prod : + measurable_fun [set: giry T1 R * giry T2 R] giry_prod. +Proof. +apply: measurable_giry_codensity => /=. +rewrite measurable_prod_measurableType. +apply: dynkin_induction => /=. +- by rewrite measurable_prod_measurableType. +- move=> _ _ [A1 mA1 [A2 mA2 <-]] [B1 mB1 [B2 mB2 <-]]. + exists (A1 `&` B1); first exact: measurableI. + exists (A2 `&` B2); first exact: measurableI. + by rewrite setXI. +- apply: (eq_measurable_fun (fun x : giry T1 R * giry T2 R => + x.1 [set: T1] * x.2 [set: T2])). + by move=> x _; rewrite -setXTT product_measure1E. + by apply: emeasurable_funM => /=; + apply: (@measurableT_comp _ _ _ _ _ _ (giry_ev ^~ _)) => //; + exact: measurable_giry_ev. +- move=> _ [A mA [B mB <-]]. + apply: (eq_measurable_fun (fun x : giry T1 R * giry T2 R => x.1 A * x.2 B)). + by move=> x _; rewrite product_measure1E. + by apply: emeasurable_funM; + apply: (@measurableT_comp _ _ _ _ _ _ (giry_ev ^~ _)) => //; + exact: measurable_giry_ev. +- move=> S mS HS. + apply: (eq_measurable_fun (fun x : giry T1 R * giry T2 R => + x.1 [set: T1] * x.2 [set: T2] - (x.1 \x x.2) S)). + move=> /= x _; rewrite subprobability_prod_setC//. + by rewrite -setXTT product_measure1E. + apply emeasurable_funB => //=. + by apply: emeasurable_funM => //=; + apply: (@measurableT_comp _ _ _ _ _ _ (giry_ev ^~ _)) => //; + exact: measurable_giry_ev. +- move=> F mF tF Fn. + apply: (eq_measurable_fun (fun x : giry T1 R * giry T2 R => + \sum_(0 <= k x _; rewrite measure_semi_bigcup//; exact: bigcup_measurable. + exact: ge0_emeasurable_sum. +Qed. + +End measurable_giry_prod. + +Section giry_prod_int. +Local Open Scope classical_set_scope. +Local Open Scope ereal_scope. +Context {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} + {R : realType}. +Variables (μ1 : giry T1 R) (μ2 : giry T2 R) (h : T1 * T2 -> \bar R). +Hypotheses (mh : measurable_fun [set: T1 * T2] h) (h0 : forall x, 0 <= h x). + +Lemma giry_int_prod1 : giry_int (giry_prod (μ1, μ2)) h = + giry_int μ1 (fun x => giry_int μ2 (fun y => h (x, y))). +Proof. exact: fubini_tonelli1. Qed. + +Lemma giry_int_prod2 : giry_int (giry_prod (μ1, μ2)) h = + giry_int μ2 (fun y => giry_int μ1 (fun x => h (x, y))). +Proof. exact: fubini_tonelli2. Qed. + +End giry_prod_int. From f8052cea916a9483bf9c515234ff44c0cd45cb5d Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 12 Jul 2025 17:48:02 +0900 Subject: [PATCH 08/14] add to makefiles --- _CoqProject | 1 + theories/Make | 1 + theories/giry.v | 2 +- 3 files changed, 3 insertions(+), 1 deletion(-) diff --git a/_CoqProject b/_CoqProject index 4a35dbab15..28c8729463 100644 --- a/_CoqProject +++ b/_CoqProject @@ -128,6 +128,7 @@ theories/charge.v theories/kernel.v theories/pi_irrational.v theories/gauss_integral.v +theories/giry.v theories/all_analysis.v diff --git a/theories/Make b/theories/Make index 98c1b98895..853aae6993 100644 --- a/theories/Make +++ b/theories/Make @@ -96,4 +96,5 @@ kernel.v pi_irrational.v gauss_integral.v all_analysis.v +giry.v showcase/summability.v diff --git a/theories/giry.v b/theories/giry.v index 6a4a63a4a3..b6601ca0f6 100644 --- a/theories/giry.v +++ b/theories/giry.v @@ -361,7 +361,7 @@ rewrite ge0_integral_fsum//; last 2 first. rewrite sintegralE /=. apply: fsbigop.eq_fsbigr => // r rh. rewrite integralZl//. -have := finite_measure_integrable_cst M 1. +have := finite_measure_integrable_cst M 1 measurableT. apply: le_integrable => //; first exact: measurable_giry_ev. move=> mu _ /=. rewrite normr1 (le_trans _ (@sprobability_setT _ _ _ mu))// gee0_abs//. From 58f6efa54916217b94fa63d65815dc677a3b027b Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 23 Nov 2025 00:13:58 +0900 Subject: [PATCH 09/14] changelog, doc until measurable_giry_int --- CHANGELOG_UNRELEASED.md | 11 +++++++++++ _CoqProject | 2 +- theories/Make | 2 +- theories/{ => lebesgue_integral_theory}/giry.v | 0 theories/measure_theory/probability_measure.v | 11 +++++++++++ 5 files changed, 24 insertions(+), 2 deletions(-) rename theories/{ => lebesgue_integral_theory}/giry.v (100%) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 9ea5c99a8a..46a19d4a6b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -13,6 +13,17 @@ - in `normed_module.v`: + lemma `limit_point_infinite_setP` +- new file `lebesgue_integral_theory/giry.v` + + definition `measure_eq` + + definition `giry` + + definition `giry_ev` + + definition `giry_measurable` + + definition `preimg_giry_ev` + + definition `giry_display` + + lemma `measurable_giry_ev` + + definition `giry_int` + + lemma `measurable_giry_int` + ### Changed ### Renamed diff --git a/_CoqProject b/_CoqProject index 28c8729463..ccb3905b52 100644 --- a/_CoqProject +++ b/_CoqProject @@ -119,6 +119,7 @@ theories/lebesgue_integral_theory/lebesgue_Rintegral.v theories/lebesgue_integral_theory/lebesgue_integral_fubini.v theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v theories/lebesgue_integral_theory/lebesgue_integral.v +theories/lebesgue_integral_theory/giry.v theories/ftc.v theories/hoelder.v @@ -128,7 +129,6 @@ theories/charge.v theories/kernel.v theories/pi_irrational.v theories/gauss_integral.v -theories/giry.v theories/all_analysis.v diff --git a/theories/Make b/theories/Make index 853aae6993..d67f6b5447 100644 --- a/theories/Make +++ b/theories/Make @@ -86,6 +86,7 @@ lebesgue_integral_theory/lebesgue_Rintegral.v lebesgue_integral_theory/lebesgue_integral_fubini.v lebesgue_integral_theory/lebesgue_integral_differentiation.v lebesgue_integral_theory/lebesgue_integral.v +lebesgue_integral_theory/giry.v ftc.v hoelder.v @@ -96,5 +97,4 @@ kernel.v pi_irrational.v gauss_integral.v all_analysis.v -giry.v showcase/summability.v diff --git a/theories/giry.v b/theories/lebesgue_integral_theory/giry.v similarity index 100% rename from theories/giry.v rename to theories/lebesgue_integral_theory/giry.v diff --git a/theories/measure_theory/probability_measure.v b/theories/measure_theory/probability_measure.v index 59be2b94a7..adcdb9f54d 100644 --- a/theories/measure_theory/probability_measure.v +++ b/theories/measure_theory/probability_measure.v @@ -73,6 +73,17 @@ HB.instance Definition _ := @isSubProbability.Build _ _ _ P sprobability_setT. HB.end. +Section mzero_subprobability. +Context d (T : measurableType d) (R : realType). + +Let mzero_setT : (@mzero d T R setT <= 1)%E. +Proof. by rewrite /mzero/=. Qed. + +HB.instance Definition _ := + Measure_isSubProbability.Build _ _ _ (@mzero d T R) mzero_setT. + +End mzero_subprobability. + HB.mixin Record isProbability d (T : measurableType d) (R : realType) (P : set T -> \bar R) := { probability_setT : P setT = 1%E }. From af7caebb565683c000853204734755c29532f92a Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 23 Nov 2025 21:47:28 +0900 Subject: [PATCH 10/14] doc until giry_join --- CHANGELOG_UNRELEASED.md | 10 ++ theories/lebesgue_integral_theory/giry.v | 203 ++++++++++------------- 2 files changed, 101 insertions(+), 112 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 46a19d4a6b..1cd64393a1 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -15,6 +15,7 @@ - new file `lebesgue_integral_theory/giry.v` + definition `measure_eq` + + lemma `dynkin_induction` + definition `giry` + definition `giry_ev` + definition `giry_measurable` @@ -23,6 +24,15 @@ + lemma `measurable_giry_ev` + definition `giry_int` + lemma `measurable_giry_int` + + lemma `measurable_giry_codensity` + + definition `giry_map` + + lemma `measurable_giry_map` + + lemma `giry_int_map` + + lemma `giry_map_dirac` + + definition `giry_ret` + + lemma `measurable_giry_ret` + + lemma `giry_int_ret` + + definition `giry_join` ### Changed diff --git a/theories/lebesgue_integral_theory/giry.v b/theories/lebesgue_integral_theory/giry.v index b6601ca0f6..e6817ca16a 100644 --- a/theories/lebesgue_integral_theory/giry.v +++ b/theories/lebesgue_integral_theory/giry.v @@ -7,17 +7,25 @@ From mathcomp Require Import lebesgue_measure lebesgue_integral. (**md**************************************************************************) (* # The Giry monad *) (* *) +(* ``` *) +(* m1 ≡μ m2 == m1 S = m2 S for any measurable set S *) (* giry T R == the type of subprobability measures over T *) (* giry_ev P A == the evaluation map `giryM T R -> [0, 1]` *) +(* preimg_giry_ev A == preimage of the sigma-algebra of extended real numbers *) +(* via the function giry_ev ^~ A *) +(* giry_measurable == the sigma-algebra generated by the countable unions of *) +(* preimg_giry_ev *) +(* giry_display == display of giry_measurable *) (* giry_int mu f := \int[mu]_x f x *) +(* giry_map mf == the map of type giry T1 R -> giry T2 R *) +(* where mf is a proof that f : T1 -> T2 is measurable *) (* giry_ret x == the unit of the Giry monad, i.e., \d_x *) (* @giry_join _ T R == the multiplication of the Giry monad *) (* type : giry (giry T R) R -> giry T R *) -(* giry_map mf == the map of type giry T1 R -> giry T2 R *) -(* where mf is a proof that f : T1 -> T2 is measurable *) (* giry_bind mu mf == the bind with mu : giry T1 R and f : T1 -> giry T2 R *) (* giry_prod == product of type *) (* giry T1 R * giry T2 R -> giry (T1 * T2) R *) +(* ``` *) (* *) (******************************************************************************) @@ -27,17 +35,41 @@ Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Def Num.Theory. -(* TODO: PR to measure.v? *) -Section mzero_subprobability. -Context d (T : measurableType d) (R : realType). - -Let mzero_setT : (@mzero d T R setT <= 1)%E. -Proof. by rewrite /mzero/=. Qed. +Definition measure_eq {d} {T : measurableType d} {R : realType} : + measure T R -> measure T R -> Prop := + fun m1 m2 => forall S : set T, measurable S -> m1 S = m2 S. +Notation "x ≡μ y" := (measure_eq x y) (at level 70). -HB.instance Definition _ := - Measure_isSubProbability.Build _ _ _ (@mzero d T R) mzero_setT. +Global Hint Extern 0 (_ ≡μ _) => reflexivity : core. -End mzero_subprobability. +Local Open Scope classical_set_scope. +(* Adapted from mathlib induction_on_inter *) +(* TODO: change premises to use setX_closed like notations *) +Lemma dynkin_induction d {T : measurableType d} (G : set (set T)) + (P : set_system T) : + @measurable _ T = <> -> + setI_closed G -> + P [set: T] -> + G `<=` P -> + (forall S, measurable S -> P S -> P (~` S)) -> + (forall F : (set T)^nat, + (forall n, measurable (F n)) -> + trivIset setT F -> + (forall n, P (F n)) -> P (\bigcup_k F k)) -> + (forall S, <> S -> P S). +Proof. +move=> GE GI PsetT GP PsetC Pbigcup A sGA. +suff: <> `<=` [set A | measurable A /\ P A] by move=> /(_ _ sGA)[]. +apply: lambda_system_subset; [by []| | |by []]. +- apply/dynkin_lambda_system; split => //. + + by move=> B [mB PB]; split; [exact: measurableC|exact: PsetC]. + + move=> F tF Hm; split. + by apply: bigcup_measurable => k _; apply Hm. + by apply: Pbigcup => //; apply Hm. +- move=> B GB; split; last exact: GP. + by rewrite GE; exact: sub_gen_smallest. +Qed. +Local Close Scope classical_set_scope. Section giry_def. Local Open Scope classical_set_scope. @@ -74,7 +106,6 @@ HB.instance Definition _ := @isMeasurable.Build giry_display giry giry_measurable giry_measurable0 giry_measurableC giry_measurableU. -(* TODO: Make hint? *) Lemma measurable_giry_ev (A : set T) : measurable A -> measurable_fun [set: giry] (giry_ev ^~ A). Proof. @@ -88,13 +119,6 @@ Qed. End giry_def. Arguments giry_ev {d T R} mu A. -Definition measure_eq {d} {T : measurableType d} {R : realType} : - giry T R -> giry T R -> Prop := - fun μ1 μ2 => forall S : set T, measurable S -> μ1 S = μ2 S. -Notation "x ≡μ y" := (measure_eq x y) (at level 70). - -Global Hint Extern 0 (_ ≡μ _) => reflexivity : core. - Section giry_integral. Local Open Scope classical_set_scope. Local Open Scope ereal_scope. @@ -104,97 +128,50 @@ Definition giry_int (mu : giry T R) (f : T -> \bar R) := \int[mu]_x f x. Import HBNNSimple. +(**md The idea is to reconstruct f from simple functions, then use measurability + of giry_ev. Reference: Tom Avery. Codensity and the Giry monad. + https://arxiv.org/pdf/1410.4432. + *) Lemma measurable_giry_int (f : T -> \bar R) : measurable_fun [set: T] f -> (forall x, 0 <= f x) -> measurable_fun [set: giry T R] (giry_int ^~ f). Proof. -(* - The idea is to reconstruct f from simple functions, then use measurability of giry_ev. - Tom Avery. Codensity and the Giry monad. https://arxiv.org/pdf/1410.4432. - *) move=> mf h0. pose g := nnsfun_approx measurableT mf. -pose gE := fun n => EFin \o g n. -have mgE n : measurable_fun [set: T] (gE n) by exact/measurable_EFinP. -have gE0 n x : [set: T] x -> 0 <= (gE n) x by rewrite /gE /= // lee_fin. -have HgEmono x : [set: T] x -> {homo gE ^~ x : n m / (n <= m)%O >-> n <= m}. - by move=> _ n m nm; exact/lefP/nd_nnsfun_approx. -(* By MCT, limit of the integrals of g_n is the integral of the limit of g_n *) -have Hcvg := cvg_monotone_convergence _ mgE gE0 HgEmono. -pose gEInt := fun n μ => \int[μ]_x (gE n) x. -have mgEInt n : measurable_fun [set: giry T R] (gEInt n). - rewrite /gEInt /gE /=. - apply (eq_measurable_fun (fun μ : giry T R => - \sum_(x \in range (g n)) x%:E * μ (g n @^-1` [set x]))). - by move=> μ Hμ; rewrite integralT_nnsfun sintegralE. - apply: emeasurable_fsum => // r. - apply: measurable_funeM. - exact: measurable_giry_ev. -(* The μ ↦ int[mu] lim g_n is measurable if every μ ↦ int[mu] g_n is measurable *) -apply: (emeasurable_fun_cvg _ (fun μ : giry T R => \int[μ]_x f x) mgEInt). -move=> μ Hμ. -rewrite /gEInt /=. -rewrite (eq_integral (fun x : T => limn (gE ^~ x))). - exact: (Hcvg μ measurableT). -move=> x _; apply/esym/cvg_lim => //. -exact/cvg_nnsfun_approx. +pose Eg := fun n => EFin \o g n. +pose intEg := fun n mu => giry_int mu (Eg n). +have mintgE n : measurable_fun [set: giry T R] (intEg n). + rewrite /intEg /giry_int/=. + under eq_fun do rewrite integralT_nnsfun sintegralE. + apply: emeasurable_fsum => //= r. + by apply: measurable_funeM => //=; exact: measurable_giry_ev. +apply: (emeasurable_fun_cvg _ (giry_int ^~ f) mintgE) => mu _. +rewrite (_ : giry_int mu f = \int[mu]_x limn (Eg ^~ x)). + apply: cvg_monotone_convergence => //. + - by move=> n; exact/measurable_EFinP. + - by move=> n x _; rewrite lee_fin. + - by move=> t _ n m nm; apply/lefP/nd_nnsfun_approx. +apply: eq_integral => t _. +by apply/esym/cvg_lim => //; exact/cvg_nnsfun_approx. Qed. End giry_integral. Arguments giry_int {d T R} mu f. -Local Open Scope classical_set_scope. -(* Adapted from mathlib induction_on_inter *) -(* TODO: change premises to use setX_closed like notations *) -Lemma dynkin_induction d {T : measurableType d} (G : set (set T)) - (P : set_system T) : - @measurable _ T = <> -> - setI_closed G -> - P [set: T] -> - G `<=` P -> - (forall S, measurable S -> P S -> P (~` S)) -> - (forall F : (set T)^nat, - (forall n, measurable (F n)) -> - trivIset setT F -> - (forall n, P (F n)) -> P (\bigcup_k F k)) -> - (forall S, <> S -> P S). -Proof. -move=> GE GI PsetT GP PsetC Pbigcup A sGA. -suff: <> `<=` [set A | measurable A /\ P A] by move=> /(_ _ sGA)[]. -apply: lambda_system_subset; [by []| | |by []]. -- apply/dynkin_lambda_system; split => //. - + by move=> B [mB PB]; split; [exact: measurableC|exact: PsetC]. - + move=> F tF Hm; split. - by apply: bigcup_measurable => k _; apply Hm. - by apply: Pbigcup => //; apply Hm. -- move=> B GB; split; last exact: GP. - by rewrite GE; exact: sub_gen_smallest. -Qed. -Local Close Scope classical_set_scope. - Section measurable_giry_codensity. Local Open Scope classical_set_scope. +Context d1 {T1 : measurableType d1}. -(* TODO: move this lemma to a more accessible location? *) -Let measurability_image_sub d d' (aT : measurableType d) (rT : measurableType d') - (f : aT -> rT) (G : set (set rT)) : - @measurable _ rT = <> -> - (forall B, G B -> measurable (f @^-1` B)) -> - measurable_fun [set: aT] f. +Lemma measurable_giry_codensity d2 {T2 : measurableType d2} {R : realType} + (D : set T1) (f : T1 -> giry T2 R) : + measurable D -> + (forall B, measurable B -> measurable_fun D (f ^~ B)) -> + measurable_fun D f. Proof. -move=> GE Gf; apply/(measurability G) => //. -by apply/image_subP => A /Gf; rewrite setTI. -Qed. - -Lemma measurable_giry_codensity {d1} {d2} {T1 : measurableType d1} - {T2 : measurableType d2} {R : realType} (f : T1 -> giry T2 R) : - (forall B, measurable B -> measurable_fun [set: T1] (f ^~ B)) -> - measurable_fun [set: T1] f. -Proof. -move=> mf. +move=> mD mf. pose G : set_system (giry T2 R) := \bigcup_(B in measurable) preimg_giry_ev B. -apply: (measurability_image_sub (G := G)) => // _ [B mB [Y mY] <-]. -exact: mf. +apply: (measurability G) => //= _ [_ [C mC [Z mZ] <-] <-]. +by rewrite setTI; exact: mf. Qed. End measurable_giry_codensity. @@ -202,8 +179,8 @@ End measurable_giry_codensity. Section giry_map. Local Open Scope classical_set_scope. Local Open Scope ereal_scope. -Context {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} {R : realType}. - +Context {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} + {R : realType}. Variables (f : T1 -> T2) (mf : measurable_fun [set: T1] f) (mu1 : giry T1 R). Let map := pushforward mu1 f. @@ -233,19 +210,28 @@ Definition giry_map : giry T2 R := map. End giry_map. -Section giry_map_meas. +Section giry_map_lemmas. Local Open Scope classical_set_scope. Local Open Scope ereal_scope. Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). Implicit Type f : T1 -> T2. +Lemma measurable_giry_map f (mf : measurable_fun [set: T1] f) : + measurable_fun [set: giry T1 R] (giry_map mf). +Proof. +rewrite /giry_map. +apply: measurable_giry_codensity => // B mB. +apply: measurable_giry_ev. +by rewrite -(setTI (f @^-1` B)); exact: mf. +Qed. + Lemma giry_int_map f (mf : measurable_fun [set: T1] f) (mu : giry T1 R) (h : T2 -> \bar R) : measurable_fun [set: T2] h -> (forall x, 0 <= h x) -> giry_int (giry_map mf mu) h = giry_int mu (h \o f). Proof. by move=> mh h0; exact: ge0_integral_pushforward. Qed. -Lemma giry_mapE f (mf : measurable_fun [set: T1] f) +Lemma giry_map_dirac f (mf : measurable_fun [set: T1] f) (mu1 : giry T1 R) (B : set T2) : measurable B -> giry_map mf mu1 B = \int[mu1]_x (\d_(f x))%R B. Proof. @@ -255,16 +241,7 @@ rewrite -[in LHS](setIT B) -[LHS]integral_indic// [LHS]giry_int_map//. by move=> ?; rewrite lee_fin. Qed. -Lemma measurable_giry_map f (mf : measurable_fun [set: T1] f) : - measurable_fun [set: giry T1 R] (giry_map mf). -Proof. -rewrite /giry_map. -apply: (@measurable_giry_codensity _ _ (giry T1 R)) => B mB. -apply: measurable_giry_ev. -by rewrite -(setTI (f @^-1` B)); exact: mf. -Qed. - -End giry_map_meas. +End giry_map_lemmas. Section giry_ret. Local Open Scope classical_set_scope. @@ -275,7 +252,9 @@ Context {d} {T : measurableType d} {R : realType}. Definition giry_ret (x : T) : giry T R := \d_x. Lemma measurable_giry_ret : measurable_fun [set: T] giry_ret. -Proof. by apply: measurable_giry_codensity; exact: measurable_fun_dirac. Qed. +Proof. +by apply: measurable_giry_codensity => //; exact: measurable_fun_dirac. +Qed. Lemma giry_int_ret (x : T) (f : T -> \bar R) : measurable_fun [set: T] f -> giry_int (giry_ret x) f = f x. @@ -288,7 +267,7 @@ End giry_ret. Section giry_join. Local Open Scope classical_set_scope. Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType). +Context {d} {T : measurableType d} {R : realType}. Variable M : giry (giry T R) R. Let join A := giry_int M (giry_ev ^~ A). @@ -345,7 +324,7 @@ Context {d} {T : measurableType d} {R : realType}. Lemma measurable_giry_join : measurable_fun [set: giry (giry T R) R] giry_join. Proof. -apply: measurable_giry_codensity => B mB/=. +apply: measurable_giry_codensity => //= B mB. by apply: measurable_giry_int => //; exact: measurable_giry_ev. Qed. @@ -524,7 +503,7 @@ Qed. Lemma measurable_giry_prod : measurable_fun [set: giry T1 R * giry T2 R] giry_prod. Proof. -apply: measurable_giry_codensity => /=. +apply: measurable_giry_codensity => //=. rewrite measurable_prod_measurableType. apply: dynkin_induction => /=. - by rewrite measurable_prod_measurableType. From 76e16d39643800b46458fce92a1f5de902adde7c Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 24 Nov 2025 10:57:41 +0900 Subject: [PATCH 11/14] mv lemmas --- CHANGELOG_UNRELEASED.md | 24 ++-- theories/lebesgue_integral_theory/giry.v | 135 +++--------------- .../lebesgue_integral_fubini.v | 56 +++++++- .../measure_theory/measurable_structure.v | 27 +++- 4 files changed, 113 insertions(+), 129 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 1cd64393a1..ff3539f636 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -13,9 +13,15 @@ - in `normed_module.v`: + lemma `limit_point_infinite_setP` +- in `measurable_structure.v`: + + lemma `dynkin_induction`` + +- in `lebesgue_integral_fubini.v`: + + definition `product_subprobability` + + lemma `product_subprobability__setC` + - new file `lebesgue_integral_theory/giry.v` + definition `measure_eq` - + lemma `dynkin_induction` + definition `giry` + definition `giry_ev` + definition `giry_measurable` @@ -23,16 +29,18 @@ + definition `giry_display` + lemma `measurable_giry_ev` + definition `giry_int` - + lemma `measurable_giry_int` - + lemma `measurable_giry_codensity` + + lemmas `measurable_giry_int`, `measurable_giry_codensity` + definition `giry_map` - + lemma `measurable_giry_map` - + lemma `giry_int_map` - + lemma `giry_map_dirac` + + lemmas `measurable_giry_map`, `giry_int_map`, `giry_map_dirac` + definition `giry_ret` - + lemma `measurable_giry_ret` - + lemma `giry_int_ret` + + lemmas `measurable_giry_ret`, `giry_int_ret` + definition `giry_join` + + lemmas `measurable_giry_join`, `sintegral_giry_join`, `giry_int_join` + + definition `giry_bind` + + lemmas `measurable_giry_bind`, `giry_int_bind` + + lemmas `giry_joinA`, `giry_join_id1`, `giry_join_id2`, `giry_map_zero` + + definition `giry_prod` + + lemmas `measurable_giry_prod`, `giry_int_prod1`, `giry_int_prod2` ### Changed diff --git a/theories/lebesgue_integral_theory/giry.v b/theories/lebesgue_integral_theory/giry.v index e6817ca16a..c14c18f30e 100644 --- a/theories/lebesgue_integral_theory/giry.v +++ b/theories/lebesgue_integral_theory/giry.v @@ -29,6 +29,8 @@ From mathcomp Require Import lebesgue_measure lebesgue_integral. (* *) (******************************************************************************) +Reserved Notation "m >>= f" (at level 49). + Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -43,36 +45,9 @@ Notation "x ≡μ y" := (measure_eq x y) (at level 70). Global Hint Extern 0 (_ ≡μ _) => reflexivity : core. Local Open Scope classical_set_scope. -(* Adapted from mathlib induction_on_inter *) -(* TODO: change premises to use setX_closed like notations *) -Lemma dynkin_induction d {T : measurableType d} (G : set (set T)) - (P : set_system T) : - @measurable _ T = <> -> - setI_closed G -> - P [set: T] -> - G `<=` P -> - (forall S, measurable S -> P S -> P (~` S)) -> - (forall F : (set T)^nat, - (forall n, measurable (F n)) -> - trivIset setT F -> - (forall n, P (F n)) -> P (\bigcup_k F k)) -> - (forall S, <> S -> P S). -Proof. -move=> GE GI PsetT GP PsetC Pbigcup A sGA. -suff: <> `<=` [set A | measurable A /\ P A] by move=> /(_ _ sGA)[]. -apply: lambda_system_subset; [by []| | |by []]. -- apply/dynkin_lambda_system; split => //. - + by move=> B [mB PB]; split; [exact: measurableC|exact: PsetC]. - + move=> F tF Hm; split. - by apply: bigcup_measurable => k _; apply Hm. - by apply: Pbigcup => //; apply Hm. -- move=> B GB; split; last exact: GP. - by rewrite GE; exact: sub_gen_smallest. -Qed. -Local Close Scope classical_set_scope. +Local Open Scope ereal_scope. Section giry_def. -Local Open Scope classical_set_scope. Context d (T : measurableType d) (R : realType). Definition giry : Type := @subprobability d T R. @@ -120,8 +95,6 @@ End giry_def. Arguments giry_ev {d T R} mu A. Section giry_integral. -Local Open Scope classical_set_scope. -Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType). Definition giry_int (mu : giry T R) (f : T -> \bar R) := \int[mu]_x f x. @@ -159,7 +132,6 @@ End giry_integral. Arguments giry_int {d T R} mu f. Section measurable_giry_codensity. -Local Open Scope classical_set_scope. Context d1 {T1 : measurableType d1}. Lemma measurable_giry_codensity d2 {T2 : measurableType d2} {R : realType} @@ -177,8 +149,6 @@ Qed. End measurable_giry_codensity. Section giry_map. -Local Open Scope classical_set_scope. -Local Open Scope ereal_scope. Context {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} {R : realType}. Variables (f : T1 -> T2) (mf : measurable_fun [set: T1] f) (mu1 : giry T1 R). @@ -211,13 +181,11 @@ Definition giry_map : giry T2 R := map. End giry_map. Section giry_map_lemmas. -Local Open Scope classical_set_scope. -Local Open Scope ereal_scope. Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). -Implicit Type f : T1 -> T2. +Variable f : T1 -> T2. +Hypothesis mf : measurable_fun [set: T1] f. -Lemma measurable_giry_map f (mf : measurable_fun [set: T1] f) : - measurable_fun [set: giry T1 R] (giry_map mf). +Lemma measurable_giry_map : measurable_fun [set: giry T1 R] (giry_map mf). Proof. rewrite /giry_map. apply: measurable_giry_codensity => // B mB. @@ -225,17 +193,15 @@ apply: measurable_giry_ev. by rewrite -(setTI (f @^-1` B)); exact: mf. Qed. -Lemma giry_int_map f (mf : measurable_fun [set: T1] f) - (mu : giry T1 R) (h : T2 -> \bar R) : +Lemma giry_int_map (mu : giry T1 R) (h : T2 -> \bar R) : measurable_fun [set: T2] h -> (forall x, 0 <= h x) -> giry_int (giry_map mf mu) h = giry_int mu (h \o f). Proof. by move=> mh h0; exact: ge0_integral_pushforward. Qed. -Lemma giry_map_dirac f (mf : measurable_fun [set: T1] f) - (mu1 : giry T1 R) (B : set T2) : measurable B -> +Lemma giry_map_dirac (mu1 : giry T1 R) (B : set T2) : measurable B -> giry_map mf mu1 B = \int[mu1]_x (\d_(f x))%R B. Proof. -move=> mA. +move=> mB. rewrite -[in LHS](setIT B) -[LHS]integral_indic// [LHS]giry_int_map//. exact/measurable_EFinP/measurable_indic. by move=> ?; rewrite lee_fin. @@ -244,12 +210,9 @@ Qed. End giry_map_lemmas. Section giry_ret. -Local Open Scope classical_set_scope. -Local Open Scope ring_scope. -Local Open Scope ereal_scope. Context {d} {T : measurableType d} {R : realType}. -Definition giry_ret (x : T) : giry T R := \d_x. +Definition giry_ret (x : T) : giry T R := (\d_x)%R. Lemma measurable_giry_ret : measurable_fun [set: T] giry_ret. Proof. @@ -265,8 +228,6 @@ Qed. End giry_ret. Section giry_join. -Local Open Scope classical_set_scope. -Local Open Scope ereal_scope. Context {d} {T : measurableType d} {R : realType}. Variable M : giry (giry T R) R. @@ -318,8 +279,6 @@ End giry_join. Arguments giry_join {d T R}. Section measurable_giry_join. -Local Open Scope classical_set_scope. -Local Open Scope ereal_scope. Context {d} {T : measurableType d} {R : realType}. Lemma measurable_giry_join : measurable_fun [set: giry (giry T R) R] giry_join. @@ -337,8 +296,7 @@ under eq_integral do rewrite sintegralE. rewrite ge0_integral_fsum//; last 2 first. by move=> r; apply: measurable_funeM; exact: measurable_giry_ev. by move=> n x _; exact: nnsfun_mulemu_ge0. -rewrite sintegralE /=. -apply: fsbigop.eq_fsbigr => // r rh. +rewrite sintegralE /=; apply: eq_fsbigr => // r rh. rewrite integralZl//. have := finite_measure_integrable_cst M 1 measurableT. apply: le_integrable => //; first exact: measurable_giry_ev. @@ -366,7 +324,7 @@ transitivity (limn (fun n => \int[M]_mu \int[mu]_x gE n x)). apply: congr_lim; apply/funext => n. rewrite integralT_nnsfun sintegral_giry_join; apply: eq_integral => x _. by rewrite integralT_nnsfun. -rewrite -monotone_convergence//; last 3 first. +rewrite -[LHS]monotone_convergence//; last 3 first. by move=> n; exact: measurable_giry_int. by move=> n x _; exact: integral_ge0. by move=> x _ m n mn; apply: ge0_le_integral => // t _; exact: nd_gE. @@ -378,10 +336,7 @@ Qed. End measurable_giry_join. -Reserved Notation "m >>= f" (at level 49). - Section giry_bind. -Local Open Scope classical_set_scope. Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). Implicit Types (mu : giry T1 R) (f : T1 -> giry T2 R). @@ -410,8 +365,6 @@ Qed. End giry_bind. Section giry_monad. -Local Open Scope classical_set_scope. -Local Open Scope ereal_scope. Context d1 d2 d3 (T1 : measurableType d1) (T2 : measurableType d2) (T3 : measurableType d3) (R : realType). @@ -444,59 +397,15 @@ Qed. End giry_monad. -Section giry_map_zero. -Local Open Scope classical_set_scope. -Context {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} - {R : realType}. - -Lemma giry_map_zero (f : T1 -> T2) (mf : measurable_fun [set: T1] f) : - giry_map mf (@mzero d1 T1 R) ≡μ @mzero d2 T2 R. -Proof. by []. Qed. - -End giry_map_zero. - -Section giry_prod. -Local Open Scope classical_set_scope. -Local Open Scope ereal_scope. -Context {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} {R : realType}. -Variable μ12 : giry T1 R * giry T2 R. - (* https://en.wikipedia.org/wiki/Giry_monad#Product_distributions *) -Let prod := μ12.1 \x μ12.2. - -HB.instance Definition _ := Measure.on prod. - -Let prod_setT : prod setT <= 1. -Proof. -rewrite -setXTT [leLHS]product_measure1E// -[leRHS]mule1. -by rewrite lee_pmul// sprobability_setT. -Qed. - -HB.instance Definition _ := - Measure_isSubProbability.Build _ _ _ prod prod_setT. - -Definition giry_prod : giry (T1 * T2)%type R := prod. - -(* gBind' (fun v1 => gBind' (gRet \o (pair v1)) (snd μ)) (fst μ). *) - -End giry_prod. +Definition giry_prod {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} + {R : realType} (m : giry T1 R * giry T2 R) : giry (T1 * T2)%type R := + @product_subprobability _ _ T1 T2 R m. Section measurable_giry_prod. -Local Open Scope classical_set_scope. -Local Open Scope ereal_scope. Context {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} {R : realType}. -(* TODO: Clean up, maybe move elsewhere *) -Lemma subprobability_prod_setC (P : giry T1 R * giry T2 R) (A : set (T1 * T2)) : - measurable A -> - (P.1 \x P.2) (~` A) = (P.1 \x P.2) [set: T1 * T2] - (P.1 \x P.2) A. -Proof. -move=> mA; rewrite -(setvU A) measureU//= ?addeK ?setICl//. -- by rewrite (_ : (_ \x _)%E = giry_prod P)// fin_num_measure. -- exact: measurableC. -Qed. - (* See: Tobias Fritz. A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics. https://arxiv.org/abs/1908.07021 *) @@ -526,7 +435,7 @@ apply: dynkin_induction => /=. - move=> S mS HS. apply: (eq_measurable_fun (fun x : giry T1 R * giry T2 R => x.1 [set: T1] * x.2 [set: T2] - (x.1 \x x.2) S)). - move=> /= x _; rewrite subprobability_prod_setC//. + move=> /= x _; rewrite product_subprobability_setC//. by rewrite -setXTT product_measure1E. apply emeasurable_funB => //=. by apply: emeasurable_funM => //=; @@ -542,19 +451,17 @@ Qed. End measurable_giry_prod. Section giry_prod_int. -Local Open Scope classical_set_scope. -Local Open Scope ereal_scope. Context {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} {R : realType}. -Variables (μ1 : giry T1 R) (μ2 : giry T2 R) (h : T1 * T2 -> \bar R). +Variables (m1 : giry T1 R) (m2 : giry T2 R) (h : T1 * T2 -> \bar R). Hypotheses (mh : measurable_fun [set: T1 * T2] h) (h0 : forall x, 0 <= h x). -Lemma giry_int_prod1 : giry_int (giry_prod (μ1, μ2)) h = - giry_int μ1 (fun x => giry_int μ2 (fun y => h (x, y))). +Lemma giry_int_prod1 : giry_int (giry_prod (m1, m2)) h = + giry_int m1 (fun x => giry_int m2 (fun y => h (x, y))). Proof. exact: fubini_tonelli1. Qed. -Lemma giry_int_prod2 : giry_int (giry_prod (μ1, μ2)) h = - giry_int μ2 (fun y => giry_int μ1 (fun x => h (x, y))). +Lemma giry_int_prod2 : giry_int (giry_prod (m1, m2)) h = + giry_int m2 (fun y => giry_int m1 (fun x => h (x, y))). Proof. exact: fubini_tonelli2. Qed. End giry_prod_int. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v index 381aa72af2..ee5bc4e044 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v @@ -25,12 +25,14 @@ From mathcomp Require Import lebesgue_integral_nonneg lebesgue_integrable. (* *) (* Detailed contents: *) (* ``` *) -(* m1 \x m2 == product measure over T1 * T2, m1 is a measure *) -(* over T1, and m2 is a sigma finite measure over *) -(* T2 *) -(* m1 \x^ m2 == product measure over T1 * T2, m2 is a measure *) -(* over T1, and m1 is a sigma finite measure over *) -(* T2 *) +(* m1 \x m2 == product measure over T1 * T2, m1 is a measure *) +(* over T1, and m2 is a sigma finite measure over *) +(* T2 *) +(* product_subprobability P == P.1 \x P.2 where P is a pair of subprobability *) +(* measures *) +(* m1 \x^ m2 == product measure over T1 * T2, m2 is a measure *) +(* over T1, and m1 is a sigma finite measure over *) +(* T2 *) (* ``` *) (* *) (******************************************************************************) @@ -316,6 +318,48 @@ Qed. End product_measure1E. +Section product_subprobability. +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. +Local Open Scope ereal_scope. +Context {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} + {R : realType}. +Variable m12 : subprobability T1 R * subprobability T2 R. + +Let prod := m12.1 \x m12.2. + +HB.instance Definition _ := Measure.on prod. + +Let prod_setT : prod setT <= 1. +Proof. +rewrite -setXTT [leLHS]product_measure1E// -[leRHS]mule1. +by rewrite lee_pmul// sprobability_setT. +Qed. + +HB.instance Definition _ := + Measure_isSubProbability.Build _ _ _ prod prod_setT. + +Definition product_subprobability : subprobability (T1 * T2)%type R := prod. + +End product_subprobability. + +Section product_subprobability_setC. +Local Open Scope classical_set_scope. +Local Open Scope ereal_scope. +Context {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} + {R : realType}. + +Lemma product_subprobability_setC (P : subprobability T1 R * subprobability T2 R) + (A : set (T1 * T2)) : measurable A -> + (P.1 \x P.2) (~` A) = (P.1 \x P.2) [set: T1 * T2] - (P.1 \x P.2) A. +Proof. +move=> mA. +rewrite -(setvU A) measureU//=; [|exact: measurableC|exact: setICl]. +by rewrite addeK// (_ : (_ \x _)%E = product_subprobability P)// fin_num_measure. +Qed. + +End product_subprobability_setC. + Section product_measure_unique. Local Open Scope ereal_scope. Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). diff --git a/theories/measure_theory/measurable_structure.v b/theories/measure_theory/measurable_structure.v index 72a63b8d61..b52ae7d358 100644 --- a/theories/measure_theory/measurable_structure.v +++ b/theories/measure_theory/measurable_structure.v @@ -1163,6 +1163,32 @@ Proof. by move=> PF; apply: bigcap_measurable => //; exists 1. Qed. End sigmaring_lemmas. +(* Adapted from mathlib induction_on_inter *) +Lemma dynkin_induction d {T : measurableType d} (G : set (set T)) + (P : set_system T) : + @measurable _ T = <> -> + setI_closed G -> + P [set: T] -> + G `<=` P -> + (forall S, measurable S -> P S -> P (~` S)) -> + (forall F : (set T)^nat, + (forall n, measurable (F n)) -> + trivIset [set: nat] F -> + (forall n, P (F n)) -> P (\bigcup_k F k)) -> + (forall S, <> S -> P S). +Proof. +move=> GE GI PsetT GP PsetC Pbigcup A sGA. +suff: <> `<=` [set A | measurable A /\ P A] by move=> /(_ _ sGA)[]. +apply: lambda_system_subset; [by []| | |by []]. +- apply/dynkin_lambda_system; split => //. + + by move=> B [mB PB]; split; [exact: measurableC|exact: PsetC]. + + move=> F tF Hm; split. + by apply: bigcup_measurable => k _; apply Hm. + by apply: Pbigcup => //; apply Hm. +- move=> B GB; split; last exact: GP. + by rewrite GE; exact: sub_gen_smallest. +Qed. + Lemma countable_measurable d (T : sigmaRingType d) (A : set T) : (forall t : T, measurable [set t]) -> countable A -> measurable A. Proof. @@ -1173,7 +1199,6 @@ rewrite [X in _ X](_ : _ = \bigcup_(x in f @` A) [set 'pinv_(cst r) A f x]). by rewrite eqEsubset; split=> [_ [_ [s As <-]] <-|_ [_ [s As <-]] ->]; exists (f s). Qed. - Section sigma_ring_lambda_system. Context d (T : sigmaRingType d). From 7702034e092cb245c2eb7c5aabd6629477a846b3 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 24 Nov 2025 23:25:12 +0900 Subject: [PATCH 12/14] fix --- CHANGELOG_UNRELEASED.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index ff3539f636..92cf507ae2 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -18,7 +18,7 @@ - in `lebesgue_integral_fubini.v`: + definition `product_subprobability` - + lemma `product_subprobability__setC` + + lemma `product_subprobability_setC` - new file `lebesgue_integral_theory/giry.v` + definition `measure_eq` From 877115be6937cc22e671f9c61674fc3aa7d70b15 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 24 Nov 2025 23:25:42 +0900 Subject: [PATCH 13/14] fix --- theories/lebesgue_integral_theory/lebesgue_integral_fubini.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v index ee5bc4e044..e4548acab0 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v @@ -29,7 +29,7 @@ From mathcomp Require Import lebesgue_integral_nonneg lebesgue_integrable. (* over T1, and m2 is a sigma finite measure over *) (* T2 *) (* product_subprobability P == P.1 \x P.2 where P is a pair of subprobability *) -(* measures *) +(* measures *) (* m1 \x^ m2 == product measure over T1 * T2, m2 is a measure *) (* over T1, and m1 is a sigma finite measure over *) (* T2 *) From 53310e1f6448cd35f74a8917b7d91097d535b662 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 24 Nov 2025 23:26:40 +0900 Subject: [PATCH 14/14] fix --- theories/lebesgue_integral_theory/giry.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/lebesgue_integral_theory/giry.v b/theories/lebesgue_integral_theory/giry.v index c14c18f30e..ead9220485 100644 --- a/theories/lebesgue_integral_theory/giry.v +++ b/theories/lebesgue_integral_theory/giry.v @@ -17,7 +17,7 @@ From mathcomp Require Import lebesgue_measure lebesgue_integral. (* preimg_giry_ev *) (* giry_display == display of giry_measurable *) (* giry_int mu f := \int[mu]_x f x *) -(* giry_map mf == the map of type giry T1 R -> giry T2 R *) +(* giry_map mf == the map of type giry T1 R -> giry T2 R *) (* where mf is a proof that f : T1 -> T2 is measurable *) (* giry_ret x == the unit of the Giry monad, i.e., \d_x *) (* @giry_join _ T R == the multiplication of the Giry monad *)