Fixes 1948

CHANGELOG_UNRELEASED.md

@@ -76,6 +76,9 @@
 - in `ereal.v`:
   + lemma `ge0_addBefctE`
 
+- in `measure_extension.v`:
+  + definition `caratheodory_measure`
+
 ### Changed
 
 - moved from `measurable_structure.v` to `classical_sets.v`:

theories/homotopy_theory/continuous_path.v

@@ -113,13 +113,13 @@ Context (f : {path i from x to y}) (phi : {path j from zero to one in i}).
 *)
 Definition reparameterize := f \o phi.
 
-#[local] Lemma fphi_zero : reparameterize zero = x.
+Let fphi_zero : reparameterize zero = x.
 Proof. by rewrite /reparameterize /= ?path_zero. Qed.
 
-#[loca] Lemma fphi_one : reparameterize one = y.
+Let fphi_one : reparameterize one = y.
 Proof. by rewrite /reparameterize /= ?path_one. Qed.
 
-#[local] Lemma fphi_cts : continuous reparameterize.
+Let fphi_cts : continuous reparameterize.
 Proof. by move=> ?; apply: continuous_comp; exact: continuous_fun. Qed.
 
 HB.instance Definition _ := isContinuous.Build _ _ reparameterize fphi_cts.
@@ -156,19 +156,19 @@ Section chain_path.
 Context {T : topologicalType} {i j : bpTopologicalType} (x y z: T).
 Context (p : {path i from x to y}) (q : {path j from y to z}).
 
-#[local] Lemma chain_path_zero : chain_path p q zero = x.
+Let chain_path_zero : chain_path p q zero = x.
 Proof.
 rewrite /chain_path /= wedge_lift_funE ?path_one ?path_zero //.
 by case => //= [][] //=; rewrite ?path_one ?path_zero.
 Qed.
 
-#[local] Lemma chain_path_one : chain_path p q one = z.
+Let chain_path_one : chain_path p q one = z.
 Proof.
 rewrite /chain_path /= wedge_lift_funE ?path_zero ?path_one //.
 by case => //= [][] //=; rewrite ?path_one ?path_zero.
 Qed.
 
-#[local] Lemma chain_path_cts : continuous (chain_path p q).
+Let chain_path_cts : continuous (chain_path p q).
 Proof.
 apply: chain_path_cts_point; [exact: continuous_fun..|].
 by rewrite path_zero path_one.

theories/kernel.v

@@ -1537,17 +1537,17 @@ Context d0 d1 d2 (T0 : measurableType d0)
   (T1 : measurableType d1) (T2 : measurableType d2) {R : realType}
   (k1 : R.-ftker T0 ~> T1) (k2 : R.-ftker (T0 * T1) ~> T2).
 
-#[local] Lemma kproduct0 x : kproduct k1 k2 x set0 = 0.
+Let kproduct0 x : kproduct k1 k2 x set0 = 0.
 Proof.
 by apply: integral0_eq => y _; apply: integral0_eq => z _; rewrite indic0.
 Qed.
 
-#[local] Lemma kproduct_ge0 x A : 0 <= kproduct k1 k2 x A.
+Let kproduct_ge0 x A : 0 <= kproduct k1 k2 x A.
 Proof.
 by apply: integral_ge0 => y _; apply: integral_ge0 => z _; rewrite lee_fin.
 Qed.
 
-#[local] Lemma kproduct_additive x : semi_sigma_additive (kproduct k1 k2 x).
+Let kproduct_additive x : semi_sigma_additive (kproduct k1 k2 x).
 Proof. exact: semi_sigma_additive_kproduct. Qed.
 
 HB.instance Definition _ x := isMeasure.Build
@@ -1638,7 +1638,7 @@ Context d0 d1 d2 (T0 : measurableType d0)
 Local Definition kernel_snd : (T0 * T1)%type -> {measure set T2 -> \bar R} :=
   k \o snd.
 
-#[local] Lemma measurable_kernel_snd U : measurable U ->
+Let measurable_kernel_snd U : measurable U ->
   measurable_fun [set: _] (kernel_snd ^~ U).
 Proof.
 move=> mU; have /= mk1 := measurable_kernel k _ mU.
@@ -1652,7 +1652,7 @@ Qed.
 HB.instance Definition _ :=
   @isKernel.Build _ _ _ _ _ kernel_snd measurable_kernel_snd.
 
-#[local] Lemma measure_uub_kernel_snd : measure_fam_uub kernel_snd.
+Let measure_uub_kernel_snd : measure_fam_uub kernel_snd.
 Proof.
 exists 2%R => /= -[x y].
 rewrite /kernel_snd/= (@le_lt_trans _ _ 1%:E) ?lte1n//.
@@ -1662,7 +1662,7 @@ Qed.
 HB.instance Definition _ :=
   @Kernel_isFinite.Build _ _ _ _ _ kernel_snd measure_uub_kernel_snd.
 
-#[local] Lemma sprob_kernel_kernel_snd :
+Let sprob_kernel_kernel_snd :
   ereal_sup [set kernel_snd z [set: _] | z in [set: _]] <= 1.
 Proof.
 by apply: (sprob_kernelP kernel_snd).2 => -[x y]; exact: sprob_kernel_le1.
@@ -1671,7 +1671,7 @@ Qed.
 HB.instance Definition _ := isSubProbabilityKernel.Build _ _ _ _ _
   kernel_snd sprob_kernel_kernel_snd.
 
-#[local] Lemma intker_indic_snd (A : set T2) x y : measurable A ->
+Lemma intker_indic_snd (A : set T2) x y : measurable A ->
   intker_indic kernel_snd ([set: _] `*` A) (x, y) = k y A.
 Proof.
 move=> mA; rewrite intker_indicE//=; first exact: measurableX.
@@ -1698,13 +1698,13 @@ Context d0 d1 d2 (T0 : measurableType d0)
   (T1 : measurableType d1) (T2 : measurableType d2) {R : realType}
   (k1 : R.-spker T0 ~> T1) (k2 : R.-spker T1 ~> T2).
 
-#[local] Lemma kcomp_noparam0 x : kcomp_noparam k1 k2 x set0 = 0.
+Let kcomp_noparam0 x : kcomp_noparam k1 k2 x set0 = 0.
 Proof. by apply: integral0_eq => y _; rewrite measure0. Qed.
 
-#[local] Lemma kcomp_noparam_ge0 x A : 0 <= kcomp_noparam k1 k2 x A.
+Let kcomp_noparam_ge0 x A : 0 <= kcomp_noparam k1 k2 x A.
 Proof. by apply: integral_ge0 => y _; exact: measure_ge0. Qed.
 
-#[local] Lemma kcomp_noparam_additive x :
+Let kcomp_noparam_additive x :
   semi_sigma_additive (kcomp_noparam k1 k2 x).
 Proof.
 move=> F mF tF mUF.
@@ -1736,7 +1736,7 @@ HB.instance Definition _ x := isMeasure.Build d2 T2 R (kcomp_noparam k1 k2 x)
 Definition mkcomp_noparam :=
   (kcomp_noparam k1 k2 : T0 -> {measure set T2 -> \bar R}).
 
-#[local] Lemma measurable_kernel_mkcomp_noparam U :
+Let measurable_kernel_mkcomp_noparam U :
   measurable U -> measurable_fun [set: _] (mkcomp_noparam ^~ U).
 Proof.
 move=> mU.
@@ -1776,7 +1776,7 @@ apply: ge0_le_integral => //; first exact: measurable_kernel.
 by move=> y _; exact: sprob_kernel_le1.
 Qed.
 
-#[local] Lemma sprob_kernel_kcomp_noparam :
+Let sprob_kernel_kcomp_noparam :
   ereal_sup [set (kcomp_noparam k1 k2) x setT | x in [set: T0]] <= 1.
 Proof. by apply/sprob_kernelP => x; exact: sprob_mkcomp_noparam. Qed.
 

theories/measure_theory/measure_extension.v

@@ -30,17 +30,18 @@ From mathcomp Require Import measure_negligible.
 (* ```                                                                        *)
 (*                                                                            *)
 (* ```                                                                        *)
-(*      mu.-caratheodory == the set of Caratheodory measurable sets for the   *)
-(*                          outer measure mu, i.e., sets A such that          *)
-(*                          forall B, mu A = mu (A `&` B) + mu (A `&` ~` B)   *)
-(*  caratheodory_type mu := T, where mu : {outer_measure set T -> \bar R}     *)
-(*                          It is a canonical measurableType copy of T.       *)
-(*                          The restriction of the outer measure mu to the    *)
-(*                          sigma algebra of Caratheodory measurable sets is  *)
-(*                          a measure.                                        *)
-(*                          Remark: sets that are negligible for              *)
-(*                          this measure are Caratheodory measurable.         *)
-(* mu .-cara.-measurable == sigma-algebra of Caratheodory measurable sets     *)
+(*        mu.-caratheodory == the set of Caratheodory measurable sets for the *)
+(*                            outer measure mu, i.e., sets A such that        *)
+(*                            forall B, mu A = mu (A `&` B) + mu (A `&` ~` B) *)
+(*    caratheodory_type mu := T, where mu : {outer_measure set T -> \bar R}   *)
+(*                            It is a canonical measurableType copy of T.     *)
+(*                            The restriction of the outer measure mu to the  *)
+(*                            sigma algebra of Caratheodory measurable sets   *)
+(*                            is a measure.                                   *)
+(*                            Remark: sets that are negligible for            *)
+(*                            this measure are Caratheodory measurable.       *)
+(* caratheodory_measure mu == measure built out of mu, an outer measure       *)
+(*   mu .-cara.-measurable == sigma-algebra of Caratheodory measurable sets   *)
 (* ```                                                                        *)
 (*                                                                            *)
 (* From a premeasure to an outer measure (Measure Extension Theorem part 1):  *)
@@ -108,6 +109,9 @@ Notation "{ 'outer_measure' 'set' T '->' '\bar' R }" := (outer_measure R T)
   : ring_scope.
 
 #[global] Hint Extern 0 (_ set0 = 0%R) => solve [apply: outer_measure0] : core.
+#[global] Hint Extern 0
+  (is_true (0%R <= (_ : {outer_measure set _ -> \bar _}) _)%E) =>
+  solve [apply: outer_measure_ge0] : core.
 #[global] Hint Extern 0 (sigma_subadditive _) =>
   solve [apply: outer_measure_sigma_subadditive] : core.
 
@@ -414,28 +418,32 @@ HB.instance Definition _ := @isMeasurable.Build (caratheodory_display mu)
 
 End caratheodory_sigma_algebra.
 
+Definition caratheodory_measure {R : realType} (T : pointedType)
+    (mu : {outer_measure set T -> \bar R})
+  : set (caratheodory_type mu) -> \bar R := mu.
+Arguments caratheodory_measure {R T} mu.
+
 Section caratheodory_measure.
 Local Open Scope ereal_scope.
 Variables (R : realType) (T : pointedType).
 Variable mu : {outer_measure set T -> \bar R}.
-Let U := caratheodory_type mu.
 
-Lemma caratheodory_measure0 : mu (set0 : set U) = 0.
+Let caratheodory_measure0 : caratheodory_measure mu set0 = 0.
 Proof. exact: outer_measure0. Qed.
 
-Lemma caratheodory_measure_ge0 (A : set U) : 0 <= mu A.
+Let caratheodory_measure_ge0 A : 0 <= caratheodory_measure mu A.
 Proof. exact: outer_measure_ge0. Qed.
 
-Lemma caratheodory_measure_sigma_additive :
-  semi_sigma_additive (mu : set U -> _).
+Let caratheodory_measure_sigma_additive :
+  semi_sigma_additive (caratheodory_measure mu).
 Proof.
 move=> A mA tA mbigcupA; set B := \bigcup_k A k.
 suff : forall X, mu X = \sum_(k <oo) mu (X `&` A k) + mu (X `&` ~` B).
   move/(_ B); rewrite setICr outer_measure0 adde0.
   rewrite (_ : (fun n => _) = fun n => \sum_(k < n) mu (A k)).
     rewrite funeqE => n; rewrite big_mkord; apply: eq_bigr => i _; congr (mu _).
     by rewrite setIC; apply/setIidPl; exact: bigcup_sup.
-  move=> ->.
+  rewrite /caratheodory_measure => ->.
   have := fun n (_ : xpredT n) (_ : xpredT n) => outer_measure_ge0 mu (A n).
   move/(@is_cvg_nneseries _ _ _ 0) => /cvg_ex[l] hl.
   under [in X in _ --> X]eq_fun do rewrite -(big_mkord xpredT (mu \o A)).
@@ -448,12 +456,12 @@ by rewrite -le_caratheodory_measurable // => ?; rewrite -mB.
 Qed.
 
 HB.instance Definition _ := isMeasure.Build _ _ _
-  (mu : set (caratheodory_type mu) -> _)
+  (caratheodory_measure mu)
   caratheodory_measure0 caratheodory_measure_ge0
   caratheodory_measure_sigma_additive.
 
 Lemma measure_is_complete_caratheodory :
-  measure_is_complete (mu : set (caratheodory_type mu) -> _).
+  measure_is_complete (caratheodory_measure mu).
 Proof.
 move=> B [A [mA muA0 BA]]; apply: le_caratheodory_measurable => X.
 suff -> : mu (X `&` B) = 0.
@@ -509,7 +517,7 @@ Unshelve. all: by end_near. Qed.
 
 Lemma mu_ext0 : mu^* set0 = 0.
 Proof.
-apply/eqP; rewrite eq_le; apply/andP; split; last exact/mu_ext_ge0.
+apply/eqP; rewrite eq_le; apply/andP; split => //; last exact/mu_ext_ge0.
 rewrite /mu_ext; apply: ereal_inf_lbound; exists (fun=> set0); first by split.
 by apply: lim_near_cst => //; near=> n => /=; rewrite big1.
 Unshelve. all: by end_near. Qed.
@@ -584,7 +592,7 @@ Context d (R : realType) (T : semiRingOfSetsType d).
 Variable mu : {content set T -> \bar R}.
 
 HB.instance Definition _ := isOuterMeasure.Build
-  R T _ (@mu_ext0 _ _ _ _ (measure0 mu) (measure_ge0 mu))
+  R T (mu_ext mu) (@mu_ext0 _ _ _ _ (measure0 mu) (measure_ge0 mu))
       (mu_ext_ge0 (measure_ge0 mu))
       (le_mu_ext mu)
       (mu_ext_sigma_subadditive (measure_ge0 mu)).
@@ -725,9 +733,10 @@ Proof. exact: mu_ext_ge0. Qed.
 Local Lemma measure_extension_semi_sigma_additive :
   semi_sigma_additive measure_extension.
 Proof.
-move=> F mF tF mUF; rewrite /measure_extension.
-apply: caratheodory_measure_sigma_additive => //; last exact: sub_caratheodory.
-by move=> i; exact: (sub_caratheodory (mF i)).
+move=> F mF tF mUF.
+apply: (@measure_semi_sigma_additive _ _ _ (caratheodory_measure mu^*)) => //.
+  by move=> i; exact: (sub_caratheodory (mF i)).
+exact: sub_caratheodory.
 Qed.
 
 HB.instance Definition _ := isMeasure.Build _ _ _ measure_extension
@@ -788,7 +797,7 @@ Let measure_semi_sigma_additive :
   semi_sigma_additive completed_measure_extension.
 Proof.
 move=> F mF tF mUF; rewrite /completed_measure_extension.
-exact: caratheodory_measure_sigma_additive.
+exact: (@measure_semi_sigma_additive _ _ _ (caratheodory_measure mu^*%mu)).
 Qed.
 
 HB.instance Definition _ := isMeasure.Build _ _ _ completed_measure_extension