rebase

Author: affeldt-aist

theories/kernel.v

@@ -765,8 +765,6 @@ HB.instance Definition _ (P : probability Y R):=
 
 End knormalize.
 
-<<<<<<< HEAD
-(* TODO: useful? *)
 Lemma measurable_fun_mnormalize d d' (X : measurableType d)
     (Y : measurableType d') (R : realType) (k : R.-ker X ~> Y) :
   measurable_fun [set: X] (fun x =>
@@ -797,8 +795,6 @@ apply: measurable_fun_if => //.
   + by apply: measurableT_comp => //; exact/measurable_funS/measurable_kernel.
 Qed.
 
-=======
->>>>>>> ea7f1064 (rm duplicate, more uniform naming)
 Section kcomp_def.
 Context d1 d2 d3 (X : measurableType d1) (Y : measurableType d2)
   (Z : measurableType d3) (R : realType).

theories/lang_syntax.v

@@ -168,10 +168,10 @@ rewrite /ubeta_nat_pdf /=; apply: measurable_fun_if => //=; last first.
   by rewrite setTI; apply: measurable_funTS; exact: measurable_fun_expn_onem.
 apply: measurable_and => /=.
   apply: (measurable_fun_bool true).
-  rewrite [X in measurable X](_ : _ = `[0, +oo[%classic)//.
+  rewrite setTI [X in measurable X](_ : _ = `[0, +oo[%classic)//.
   by rewrite set_interval.set_itv_c_infty.
 apply: (measurable_fun_bool true).
-by rewrite [X in measurable X](_ : _ = `]-oo, 1]%classic)//.
+by rewrite setTI [X in measurable X](_ : _ = `]-oo, 1]%classic)//.
 Qed.
 
 Local Notation mu := lebesgue_measure.

theories/lebesgue_measure.v

@@ -1728,7 +1728,7 @@ Lemma measurable_fun_pow D f n : measurable_fun D f ->
   measurable_fun D (fun x => f x ^+ n).
 Proof.
 move=> mf.
-apply: (@measurable_comp _ _ _ _ _ _ setT (fun x : R => x ^+ n) _ f) => //.
+exact: (@measurable_comp _ _ _ _ _ _ setT (fun x : R => x ^+ n) _ f).
 Qed.
 
 Lemma measurable_fun_ltr D f g : measurable_fun D f -> measurable_fun D g ->
@@ -1747,20 +1747,6 @@ under eq_fun do rewrite -subr_ge0.
 by rewrite preimage_true -preimage_itv_c_infty; exact: measurable_funB.
 Qed.
 
-Lemma measurable_fun_ler D f g : measurable_fun D f -> measurable_fun D g ->
-  measurable_fun D (fun x => f x <= g x).
-Proof.
-move=> mf mg mD Y mY; have [| | |] := set_bool Y => /eqP ->.
-- under eq_fun do rewrite -subr_ge0.
-  rewrite preimage_true -preimage_itv_c_infty.
-  by apply: (measurable_funB mg mf) => //; exact: measurable_itv.
-- under eq_fun do rewrite leNgt -subr_gt0.
-  rewrite preimage_false set_predC setCK -preimage_itv_o_infty.
-  by apply: (measurable_funB mf mg) => //; exact: measurable_itv.
-- by rewrite preimage_set0 setI0.
-- by rewrite preimage_setT setIT.
-Qed.
-
 (* setT should be D? (derived from measurable_and) *)
 Lemma measurable_fun_eqr D f g : measurable_fun D f -> measurable_fun D g ->
   measurable_fun D (fun x => f x == g x).
@@ -1876,7 +1862,7 @@ have [Y0|Y0] := boolP (0%E \in Y).
     rewrite [X in _ -> X](_ : _ = Y (\d_r U)) //.
     rewrite diracE.
     move/mem_set.
-    case (_ \in _) => //= _.
+    case: (_ \in _) => //= _.
     by rewrite inE in Y1.
   + rewrite [X in measurable X](_ : _ = set0).
       exact: measurable0.
@@ -1922,13 +1908,6 @@ under eq_fun do rewrite -mulr_natr.
 by do 2 apply: measurable_funM => //.
 Qed.
 
-Lemma measurable_fun_pow {R : realType} D (f : R -> R) n : measurable_fun D f ->
-  measurable_fun D (fun x => f x ^+ n).
-Proof.
-move=> mf.
-exact: (@measurable_comp _ _ _ _ _ _ setT (fun x : R => x ^+ n) _ f).
-Qed.
-
 Lemma measurable_powR (R : realType) p :
   measurable_fun [set: R] (@powR R ^~ p).
 Proof.

theories/measure.v

@@ -1615,6 +1615,21 @@ rewrite [X in measurable X](_ : _ = D `&` f @^-1` [set true] `&`
 by apply: measurableI; [exact: mf|exact: mg].
 Qed.
 
+Lemma measurable_or D (f : T1 -> bool) (g : T1 -> bool) :
+  measurable_fun D f -> measurable_fun D g ->
+  measurable_fun D (fun x => f x || g x).
+Proof.
+move=> mf mg mD; apply: (measurable_fun_bool true) => //.
+rewrite [X in measurable X](_ : _ = D `&` f @^-1` [set true] `|`
+                                    (D `&` g @^-1` [set true])); last first.
+  apply/seteqP; split=> [x [Dx/= /orP[]->]|x [|]/=].
+  by left.
+  by right.
+  by move=> [Dx ->]; split.
+  by move=> [Dx ->]; split => //; apply/orP; right.
+by apply: measurableU; [exact: mf|exact: mg].
+Qed.
+
 End measurable_fun_measurableType.
 #[global] Hint Extern 0 (measurable_fun _ (fun=> _)) =>
   solve [apply: measurable_cst] : core.

theories/prob_lang.v

@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
-From mathcomp Require Import rat.
+From mathcomp Require Import rat archimedean.
 From mathcomp Require Import mathcomp_extra boolp classical_sets.
 From mathcomp Require Import functions cardinality fsbigop.
 Require Import reals ereal signed topology normedtype sequences esum measure.
@@ -921,14 +921,14 @@ pose floor_f := widen_ord (leq_addl n `|floor `|f t| |.+1)
                           (Ordinal (ltnSn `|floor `|f t| |)).
 rewrite big_mkord (bigD1 floor_f)//= ifT; last first.
   rewrite lee_fin lte_fin; apply/andP; split.
-    by rewrite natr_absz (@ger0_norm _ (floor `|f t|)) ?floor_ge0 ?floor_le.
-  rewrite -addn1 natrD natr_absz.
-  by rewrite (@ger0_norm _ (floor `|f t|)) ?floor_ge0 ?lt_succ_floor.
+   by rewrite natr_absz (@ger0_norm _ (floor `|f t|)) ?floor_ge0// ?ge_floor.
+  rewrite -natr1 natr_absz.
+  by rewrite (@ger0_norm _ (floor `|f t|)) ?floor_ge0// intrD1 lt_succ_floor.
 rewrite big1 ?adde0//= => j jk.
 rewrite ifF// lte_fin lee_fin.
 move: jk; rewrite neq_ltn/= => /orP[|] jr.
 - suff : (j.+1%:R <= `|f t|)%R by rewrite leNgt => /negbTE ->; rewrite andbF.
-  rewrite (_ : j.+1%:R = j.+1%:~R)// floor_ge_int.
+  rewrite (_ : j.+1%:R = j.+1%:~R)// floor_ge_int//.
   move: jr; rewrite -lez_nat => /le_trans; apply.
   by rewrite -[leRHS](@ger0_norm _ (floor `|f t|)) ?floor_ge0.
 - suff : (`|f t| < j%:R)%R by rewrite ltNge => /negbTE ->.
@@ -1823,7 +1823,7 @@ Hypotheses (mf : measurable_fun setT f) (mg : measurable_fun setT g).
 Lemma measurable_fun_flift_neq : measurable_fun setT flift_neq.
 Proof.
 apply: (measurable_fun_bool true).
-rewrite /flift_neq /= (_ : _ @^-1` _ = ([set x | f x] `&` [set x | ~~ g x]) `|`
+rewrite setTI /flift_neq /= (_ : _ @^-1` _ = ([set x | f x] `&` [set x | ~~ g x]) `|`
                                        ([set x | ~~ f x] `&` [set x | g x])).
   apply: measurableU; apply: measurableI.
   - by rewrite -[X in measurable X]setTI; exact: mf.
@@ -2074,7 +2074,7 @@ Lemma sample_and_branchE t U : sample_and_branch t U =
   (2 / 7)%:E * \d_(3 : R) U + (5 / 7)%:E * \d_(10 : R) U.
 Proof.
 rewrite /sample_and_branch letin_sample_bernoulli/=; last lra.
-by rewrite !iteE !retE onem27.
+by rewrite !iteE/= onem27.
 Qed.
 
 End sample_and_branch.