diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4c7a5478f..7e0cd97e3 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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`: diff --git a/theories/homotopy_theory/continuous_path.v b/theories/homotopy_theory/continuous_path.v index b10955873..781736996 100644 --- a/theories/homotopy_theory/continuous_path.v +++ b/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. diff --git a/theories/kernel.v b/theories/kernel.v index 5edc7088e..50ed6a78e 100644 --- a/theories/kernel.v +++ b/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. diff --git a/theories/measure_theory/measure_extension.v b/theories/measure_theory/measure_extension.v index 46efc6837..5a802172d 100644 --- a/theories/measure_theory/measure_extension.v +++ b/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,20 +418,24 @@ 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 _) = 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