diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 347d0c429f..75f735281e 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -33,6 +33,11 @@ - in `lebesgue_integral.v` + lemmas `integral0_eq`, `fubini_tonelli` +- in `classical_sets.v`: + + lemma `trivIset_mkcond` +- in `numfun.v`: + + lemmas `xsection_indic`, `ysection_indic` + ### Changed - in `fsbigop.v`: @@ -55,6 +60,10 @@ - in `measurable.v`: + `measurable_fun_comp` -> `measurable_funT_comp` +- in `numfun.v`: + + `IsNonNegFun` -> `isNonNegFun` +- in `lebesgue_integral.v`: + + `IsMeasurableFunP` -> `isMeasurableFun` ### Generalized @@ -64,6 +73,8 @@ + lemma `measurable_fun_comp` - in `lebesgue_integral.v`: + lemma `measurable_sfunP` +- in `measure.v`: + + lemma `measure_bigcup` generalized, ### Deprecated diff --git a/classical/classical_sets.v b/classical/classical_sets.v index b417770d53..e101dd10a1 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -2382,6 +2382,15 @@ Section partitions. Definition trivIset T I (D : set I) (F : I -> set T) := forall i j : I, D i -> D j -> F i `&` F j !=set0 -> i = j. +Lemma trivIset_mkcond T I (D : set I) (F : I -> set T) : + trivIset D F <-> trivIset setT (fun i => if i \in D then F i else set0). +Proof. +split=> [tA i j _ _|tA i j Di Dj]; last first. + by have := tA i j Logic.I Logic.I; rewrite !mem_set. +case: ifPn => iD; last by rewrite set0I => -[]. +by case: ifPn => [jD /tA|jD]; [apply; exact: set_mem|rewrite setI0 => -[]]. +Qed. + Lemma trivIset_set0 {I T} (D : set I) : trivIset D (fun=> set0 : set T). Proof. by move=> i j Di Dj; rewrite setI0 => /set0P; rewrite eqxx. Qed. @@ -2429,14 +2438,14 @@ apply/trivIsetP => -[/=|]; rewrite /bigcup2 /=. by move=> [//|j _ _ _]; rewrite setI0. Qed. -Lemma trivIset_image (T I I' : Type) (D : set I) (f : I -> I') (F : I' -> set T) : +Lemma trivIset_image T I I' (D : set I) (f : I -> I') (F : I' -> set T) : trivIset D (F \o f) -> trivIset (f @` D) F. Proof. by move=> trivF i j [{}i Di <-] [{}j Dj <-] Ffij; congr (f _); apply: trivF. Qed. Arguments trivIset_image {T I I'} D f F. -Lemma trivIset_comp (T I I' : Type) (D : set I) (f : I -> I') (F : I' -> set T) : +Lemma trivIset_comp T I I' (D : set I) (f : I -> I') (F : I' -> set T) : {in D &, injective f} -> trivIset D (F \o f) = trivIset (f @` D) F. Proof. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 741686c22d..67193fb8f0 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -65,12 +65,12 @@ Reserved Notation "mu .-integrable" (at level 2, format "mu .-integrable"). #[global] Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1] : core. -HB.mixin Record IsMeasurableFun d (aT : measurableType d) (rT : realType) +HB.mixin Record isMeasurableFun d (aT : measurableType d) (rT : realType) (f : aT -> rT) := { measurable_funP : measurable_fun setT f }. HB.structure Definition MeasurableFun d aT rT := - {f of @IsMeasurableFun d aT rT f}. + {f of @isMeasurableFun d aT rT f}. Reserved Notation "{ 'mfun' aT >-> T }" (at level 0, format "{ 'mfun' aT >-> T }"). Reserved Notation "[ 'mfun' 'of' f ]" @@ -80,7 +80,7 @@ Notation "[ 'mfun' 'of' f ]" := [the {mfun _ >-> _} of f] : form_scope. #[global] Hint Resolve measurable_funP : core. HB.structure Definition SimpleFun d (aT : measurableType d) (rT : realType) := - {f of @IsMeasurableFun d aT rT f & @FiniteImage aT rT f}. + {f of @isMeasurableFun d aT rT f & @FiniteImage aT rT f}. Reserved Notation "{ 'sfun' aT >-> T }" (at level 0, format "{ 'sfun' aT >-> T }"). Reserved Notation "[ 'sfun' 'of' f ]" @@ -115,7 +115,7 @@ Notation T := {mfun aT >-> rT}. Notation mfun := (@mfun _ aT rT). Section Sub. Context (f : aT -> rT) (fP : f \in mfun). -Definition mfun_Sub_subproof := @IsMeasurableFun.Build d aT rT f (set_mem fP). +Definition mfun_Sub_subproof := @isMeasurableFun.Build d aT rT f (set_mem fP). #[local] HB.instance Definition _ := mfun_Sub_subproof. Definition mfun_Sub := [mfun of f]. End Sub. @@ -140,7 +140,7 @@ Canonical mfuneqType := EqType {mfun aT >-> rT} mfuneqMixin. Definition mfunchoiceMixin := [choiceMixin of {mfun aT >-> rT} by <:]. Canonical mfunchoiceType := ChoiceType {mfun aT >-> rT} mfunchoiceMixin. -Lemma cst_mfun_subproof x : @IsMeasurableFun d aT rT (cst x). +Lemma cst_mfun_subproof x : @isMeasurableFun d aT rT (cst x). Proof. by split; apply: measurable_fun_cst. Qed. HB.instance Definition _ x := @cst_mfun_subproof x. Definition cst_mfun x := [the {mfun aT >-> rT} of cst x]. @@ -199,7 +199,7 @@ Proof. by rewrite /mindic funeqE => t; rewrite indicE. Qed. HB.instance Definition _ (D : set aT) (mD : measurable D) : @FImFun aT rT (mindic mD) := FImFun.on (mindic mD). Lemma indic_mfun_subproof (D : set aT) (mD : measurable D) : - @IsMeasurableFun d aT rT (mindic mD). + @isMeasurableFun d aT rT (mindic mD). Proof. split=> mA /= B mB; rewrite preimage_indic. case: ifPn => B1; case: ifPn => B0 //. @@ -216,7 +216,7 @@ Definition indic_mfun (D : set aT) (mD : measurable D) := HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst_mfun k). Definition scale_mfun k f := [the {mfun aT >-> rT} of k \o* f]. -Lemma max_mfun_subproof f g : @IsMeasurableFun d aT rT (f \max g). +Lemma max_mfun_subproof f g : @isMeasurableFun d aT rT (f \max g). Proof. by split; apply: measurable_fun_max. Qed. HB.instance Definition _ f g := max_mfun_subproof f g. Definition max_mfun f g := [the {mfun aT >-> _} of f \max g]. @@ -247,7 +247,7 @@ Notation sfun := (@sfun _ aT rT). Section Sub. Context (f : aT -> rT) (fP : f \in sfun). Definition sfun_Sub1_subproof := - @IsMeasurableFun.Build d aT rT f (set_mem (sub_sfun_mfun fP)). + @isMeasurableFun.Build d aT rT f (set_mem (sub_sfun_mfun fP)). #[local] HB.instance Definition _ := sfun_Sub1_subproof. Definition sfun_Sub2_subproof := @FiniteImage.Build aT rT f (set_mem (sub_sfun_fimfun fP)). @@ -391,7 +391,7 @@ Qed. Section nnsfun_functions. Context d (T : measurableType d) (R : realType). -Lemma cst_nnfun_subproof (x : {nonneg R}) : @IsNonNegFun T R (cst x%:num). +Lemma cst_nnfun_subproof (x : {nonneg R}) : @isNonNegFun T R (cst x%:num). Proof. by split=> /=. Qed. HB.instance Definition _ x := @cst_nnfun_subproof x. @@ -399,7 +399,7 @@ Definition cst_nnsfun (r : {nonneg R}) := [the {nnsfun T >-> R} of cst r%:num]. Definition nnsfun0 : {nnsfun T >-> R} := cst_nnsfun 0%R%:nng. -Lemma indic_nnfun_subproof (D : set T) : @IsNonNegFun T R (\1_D). +Lemma indic_nnfun_subproof (D : set T) : @isNonNegFun T R (\1_D). Proof. by split=> //=; rewrite /indic. Qed. HB.instance Definition _ D := @indic_nnfun_subproof D. @@ -412,15 +412,15 @@ Arguments nnsfun0 {d T R}. Section nnfun_bin. Variables (T : Type) (R : numDomainType) (f g : {nnfun T >-> R}). -Lemma add_nnfun_subproof : @IsNonNegFun T R (f \+ g). +Lemma add_nnfun_subproof : @isNonNegFun T R (f \+ g). Proof. by split => x; rewrite addr_ge0//; apply/fun_ge0. Qed. HB.instance Definition _ := add_nnfun_subproof. -Lemma mul_nnfun_subproof : @IsNonNegFun T R (f \* g). +Lemma mul_nnfun_subproof : @isNonNegFun T R (f \* g). Proof. by split => x; rewrite mulr_ge0//; apply/fun_ge0. Qed. HB.instance Definition _ := mul_nnfun_subproof. -Lemma max_nnfun_subproof : @IsNonNegFun T R (f \max g). +Lemma max_nnfun_subproof : @isNonNegFun T R (f \max g). Proof. by split => x /=; rewrite /maxr; case: ifPn => _; apply: fun_ge0. Qed. HB.instance Definition _ := max_nnfun_subproof. @@ -687,7 +687,7 @@ Context d (T : measurableType d) (R : realType) (m : {measure set T -> \bar R}). Variables f g : {nnsfun T >-> R}. Hypothesis fg : forall x, f x <= g x. -Let fgnn : @IsNonNegFun T R (g \- f). +Let fgnn : @isNonNegFun T R (g \- f). Proof. by split=> x; rewrite subr_ge0 fg. Qed. #[local] HB.instance Definition _ := fgnn. @@ -1784,7 +1784,7 @@ End ge0_integral_sum. Section ge0_integral_fsum. Local Open Scope ereal_scope. -Variables (d : measure_display) (T : measurableType d) (R : realType). +Context d (T : measurableType d) (R : realType). Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D). Variables (I : choiceType) (f : I -> (T -> \bar R)). Hypothesis mf : forall n, measurable_fun D (f n). @@ -2288,9 +2288,9 @@ End integral_cst. Section transfer. Local Open Scope ereal_scope. -Variables (d1 d2 : _) (X : measurableType d1) (Y : measurableType d2). +Context d1 d2 (X : measurableType d1) (Y : measurableType d2) (R : realType). Variables (phi : X -> Y) (mphi : measurable_fun setT phi). -Variables (R : realType) (mu : {measure set X -> \bar R}). +Variables (mu : {measure set X -> \bar R}). Lemma integral_pushforward (f : Y -> \bar R) : measurable_fun setT f -> (forall y, 0 <= f y) -> @@ -4072,45 +4072,25 @@ End dominated_convergence_theorem. (******************************************************************************) Section measurable_section. -Variables (d1 d2 : measure_display). -Variables (T1 : measurableType d1) (T2 : measurableType d2). +Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). Implicit Types (A : set (T1 * T2)). -Variable R : realType. - Lemma measurable_xsection A x : measurable A -> measurable (xsection A x). Proof. -move=> mA. -pose f : T1 * T2 -> \bar R := EFin \o indic_nnsfun R mA. -have mf : measurable_fun setT f by exact/EFin_measurable_fun/measurable_funP. -have _ : (fun y => (y \in xsection A x)%:R%:E) = f \o (fun y => (x, y)). - by apply/funext => y/=; rewrite mem_xsection. -have -> : xsection A x = (fun y => f (x, y)) @^-1` [set 1%E]. - apply/funext => y/=; rewrite -(in_setE (xsection A x)) mem_xsection. - rewrite /f/= mindicE//; apply/propext; split=> [->//|[]]. - by case: (_ \in _)=> // /esym/eqP; rewrite oner_eq0. -by rewrite -(setTI (_ @^-1` _)); exact: measurable_fun_prod1. +move=> mA; rewrite (xsection_indic R) -(setTI (_ @^-1` _)). +by apply: measurable_fun_prod1 => //; exact/measurable_fun_indic. Qed. Lemma measurable_ysection A y : measurable A -> measurable (ysection A y). Proof. -move=> mA. -pose f : T1 * T2 -> \bar R := EFin \o indic_nnsfun R mA. -have mf : measurable_fun setT f by apply/EFin_measurable_fun/measurable_funP. -have _ : (fun x => (x \in ysection A y)%:R%:E) = f \o (fun x => (x, y)). - by apply/funext => x/=; rewrite mem_ysection. -have -> : ysection A y = (fun x => f (x, y)) @^-1` [set 1%E]. - apply/funext => x/=; rewrite -(in_setE (ysection A y)) mem_ysection. - rewrite /f/= mindicE//; apply/propext; split=> [->//|[]]. - by case: (_ \in _)=> // /esym/eqP; rewrite oner_eq0. -by rewrite -(setTI (_ @^-1` _)); exact: measurable_fun_prod2. +move=> mA; rewrite (ysection_indic R) -(setTI (_ @^-1` _)). +by apply: measurable_fun_prod2 => //; exact/measurable_fun_indic. Qed. End measurable_section. Section ndseq_closed_B. -Variables (d1 d2 : measure_display). -Variables (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). +Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). Implicit Types A : set (T1 * T2). Section xsection. @@ -4134,7 +4114,7 @@ Qed. End xsection. Section ysection. -Variables (m1 : {measure set T1 -> \bar R}). +Variable m1 : {measure set T1 -> \bar R}. Let psi A := m1 \o ysection A. Let B := [set A | measurable A /\ measurable_fun setT (psi A)]. @@ -4156,8 +4136,7 @@ End ysection. End ndseq_closed_B. Section measurable_prod_subset. -Variables (d1 d2 : measure_display). -Variables (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). +Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). Implicit Types A : set (T1 * T2). Section xsection. @@ -4245,9 +4224,8 @@ End ysection. End measurable_prod_subset. Section measurable_fun_xsection. -Variables (d1 d2 : measure_display). -Variables (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). -Variables (m2 : {measure set T2 -> \bar R}). +Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). +Variable m2 : {measure set T2 -> \bar R}. Hypothesis sf_m2 : sigma_finite setT m2. Implicit Types A : set (T1 * T2). @@ -4286,9 +4264,8 @@ Qed. End measurable_fun_xsection. Section measurable_fun_ysection. -Variables (d1 d2 : measure_display). -Variables (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). -Variables (m1 : {measure set T1 -> \bar R}). +Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). +Variable m1 : {measure set T1 -> \bar R}. Hypothesis sf_m1 : sigma_finite setT m1. Implicit Types A : set (T1 * T2). @@ -4334,8 +4311,7 @@ Definition product_measure1 d1 d2 Section product_measure1. Local Open Scope ereal_scope. -Variables (d1 d2 : measure_display). -Variables (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). +Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). Variables (m1 : {measure set T1 -> \bar R}) (m2 : {measure set T2 -> \bar R}). Hypothesis sm2 : sigma_finite setT m2. Implicit Types A : set (T1 * T2). @@ -4343,10 +4319,7 @@ Implicit Types A : set (T1 * T2). Notation pm1 := (product_measure1 m1 sm2). Let pm10 : pm1 set0 = 0. -Proof. -rewrite /pm1 (eq_integral (cst 0)) ?integral0//= => x _. -by rewrite xsection0 measure0. -Qed. +Proof. by rewrite /pm1 integral0_eq// => x/= _; rewrite xsection0 measure0. Qed. Let pm1_ge0 A : 0 <= pm1 A. Proof. @@ -4355,15 +4328,16 @@ Qed. Let pm1_sigma_additive : semi_sigma_additive pm1. Proof. -move=> F mF tF mUF; have -> : pm1 (\bigcup_n F n) = \sum_(n x _; apply/esym/cvg_lim => //=. - rewrite xsection_bigcup. - apply: (measure_sigma_additive _ (trivIset_xsection tF)). - by move=> ?; exact: measurable_xsection. - by rewrite integral_nneseries // => n; apply: measurable_fun_xsection => // /[!inE]. -apply/cvg_closeP; split; last by rewrite closeE. -by apply: is_cvg_nneseries => *; exact: integral_ge0. +move=> F mF tF mUF. +rewrite [X in _ --> X](_ : _ = \sum_(n *; exact: integral_ge0. +rewrite -integral_nneseries //; last first. + by move=> n; apply: measurable_fun_xsection => // /[!inE]. +apply: eq_integral => x _; apply/esym/cvg_lim => //=. +rewrite xsection_bigcup. +apply: (measure_sigma_additive _ (trivIset_xsection tF)) => ?. +exact: measurable_xsection. Qed. HB.instance Definition _ := isMeasure.Build _ _ _ pm1 @@ -4373,8 +4347,7 @@ End product_measure1. Section product_measure1E. Local Open Scope ereal_scope. -Variables (d1 d2 : measure_display). -Variables (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). +Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). Variables (m1 : {measure set T1 -> \bar R}) (m2 : {measure set T2 -> \bar R}). Hypothesis sm2 : sigma_finite setT m2. Implicit Types A : set (T1 * T2). @@ -4398,8 +4371,7 @@ End product_measure1E. Section product_measure_unique. Local Open Scope ereal_scope. -Variables (d1 d2 : measure_display). -Variables (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). +Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). Variables (m1 : {measure set T1 -> \bar R}) (m2 : {measure set T2 -> \bar R}). Hypotheses (sm1 : sigma_finite setT m1) (sm2 : sigma_finite setT m2). @@ -4451,8 +4423,7 @@ Definition product_measure2 d1 d2 Section product_measure2. Local Open Scope ereal_scope. -Variables (d1 d2 : measure_display). -Variables (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). +Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). Variables (m1 : {measure set T1 -> \bar R}) (m2 : {measure set T2 -> \bar R}). Hypothesis sm1 : sigma_finite setT m1. Implicit Types A : set (T1 * T2). @@ -4460,10 +4431,7 @@ Implicit Types A : set (T1 * T2). Notation pm2 := (product_measure2 sm1 m2). Let pm20 : pm2 set0 = 0. -Proof. -rewrite /pm2 (eq_integral (cst 0)) ?integral0//= => y _. -by rewrite ysection0 measure0. -Qed. +Proof. by rewrite /pm2 integral0_eq// => y/= _; rewrite ysection0 measure0. Qed. Let pm2_ge0 A : 0 <= pm2 A. Proof. @@ -4473,14 +4441,13 @@ Qed. Let pm2_sigma_additive : semi_sigma_additive pm2. Proof. move=> F mF tF mUF. -have -> : pm2 (\bigcup_n F n) = \sum_(n y _; apply/esym/cvg_lim => //=. - rewrite ysection_bigcup. - apply: (measure_sigma_additive _ (trivIset_ysection tF)). - by move=> ?; apply: measurable_ysection. - rewrite integral_nneseries // => n; apply: measurable_fun_ysection => //. - by rewrite inE. +rewrite [X in _ --> X](_ : _ = \sum_(n n; apply: measurable_fun_ysection => //; rewrite inE. + apply: eq_integral => y _; apply/esym/cvg_lim => //=. + rewrite ysection_bigcup. + apply: (measure_sigma_additive _ (trivIset_ysection tF)) => ?. + exact: measurable_ysection. apply/cvg_closeP; split; last by rewrite closeE. by apply: is_cvg_nneseries => *; exact: integral_ge0. Qed. @@ -4492,8 +4459,7 @@ End product_measure2. Section product_measure2E. Local Open Scope ereal_scope. -Variables (d1 d2 : measure_display). -Variables (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). +Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). Variables (m1 : {measure set T1 -> \bar R}) (m2 : {measure set T2 -> \bar R}). Hypothesis sm1 : sigma_finite setT m1. @@ -4517,8 +4483,7 @@ End product_measure2E. Section fubini_functions. Local Open Scope ereal_scope. -Variables (d1 d2 : measure_display). -Variables (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). +Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). Variables (m1 : {measure set T1 -> \bar R}) (m2 : {measure set T2 -> \bar R}). Variable f : T1 * T2 -> \bar R. @@ -4529,8 +4494,7 @@ End fubini_functions. Section fubini_tonelli. Local Open Scope ereal_scope. -Variables (d1 d2 : measure_display). -Variables (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). +Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). Variables (m1 : {measure set T1 -> \bar R}) (m2 : {measure set T2 -> \bar R}). Hypotheses (sm1 : sigma_finite setT m1) (sm2 : sigma_finite setT m2). @@ -4654,7 +4618,7 @@ by apply/measurable_funeM/measurable_fun_ysection => // /[!inE]. Qed. Let EFinf x : (f x)%:E = - \sum_(k \in range f) k%:E * (\1_(f @^-1` [set k]) x)%:E. + \sum_(k \in range f) k%:E * (\1_(f @^-1` [set k]) x)%:E. Proof. by rewrite fsumEFin //= fimfunE. Qed. Lemma sfun_fubini_tonelli1 : \int[m]_z (f z)%:E = \int[m1]_x F x. @@ -4864,16 +4828,18 @@ Arguments measurable_fun_fubini_tonelli_G {d1 d2 T1 T2 R m1} sm1 f. Section fubini. Local Open Scope ereal_scope. -Variables (d1 d2 : measure_display). -Variables (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). +Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). Variables (m1 : {measure set T1 -> \bar R}) (m2 : {measure set T2 -> \bar R}). Hypotheses (sm1 : sigma_finite setT m1) (sm2 : sigma_finite setT m2). Variable f : T1 * T2 -> \bar R. -Hypothesis mf : measurable_fun setT f. Let m := product_measure1 m1 sm2. HB.instance Definition _ := Measure.on m. +Hypothesis imf : m.-integrable setT f. +Let mf : measurable_fun setT f := imf.1. + +(* NB: only relies on mf *) Lemma fubini1a : m.-integrable setT f <-> \int[m1]_x \int[m2]_y `|f (x, y)| < +oo. Proof. @@ -4901,8 +4867,7 @@ Proof. apply: (measurable_fun_fubini_tonelli_G _ (abse \o f)) => //=. exact: measurable_funT_comp. Qed. - -Hypothesis imf : m.-integrable setT f. +(* /NB: only relies on mf *) Lemma ae_integrable1 : {ae m1, forall x, m2.-integrable setT (fun y => f (x, y))}. diff --git a/theories/measure.v b/theories/measure.v index 2cd64ffb60..b805949b55 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -1537,6 +1537,9 @@ Proof. by move=> Am Atriv /measure_semi_sigma_additive/cvg_lim<-//. Qed. End measure_lemmas. +#[global] Hint Extern 0 (_ set0 = 0) => solve [apply: measure0] : core. +#[global] Hint Extern 0 (is_true (0 <= _)) => solve [apply: measure_ge0] : core. + Section measure_lemmas. Context d (R : realFieldType) (T : measurableType d). Variable mu : {measure set T -> \bar R}. @@ -1546,20 +1549,21 @@ Proof. by rewrite -semi_sigma_additiveE //; apply: measure_semi_sigma_additive. Qed. -Lemma measure_bigcup A : (forall i : nat, measurable (A i)) -> - trivIset setT A -> - mu (\bigcup_n A n) = \sum_(i measurable (F i)) -> + trivIset D F -> mu (\bigcup_(n in D) F n) = \sum_(i Am Atriv; rewrite measure_semi_bigcup//; exact: bigcupT_measurable. +move=> mF tF; rewrite bigcup_mkcond measure_semi_bigcup. +- by rewrite [in RHS]eseries_mkcond; apply: eq_eseries => n _; case: ifPn. +- by move=> i; case: ifPn => // /set_mem; exact: mF. +- by move/trivIset_mkcond : tF. +- by rewrite -bigcup_mkcond; apply: bigcup_measurable. Qed. End measure_lemmas. -Arguments measure_bigcup {d R T} mu A. +Arguments measure_bigcup {d R T} _ _. -#[global] Hint Extern 0 (_ set0 = 0) => solve [apply: measure0] : core. #[global] Hint Extern 0 (sigma_additive _) => solve [apply: measure_sigma_additive] : core. -#[global] Hint Extern 0 (is_true (0 <= _)) => solve [apply: measure_ge0] : core. Definition finite_measure d (T : measurableType d) (R : numDomainType) (mu : set T -> \bar R) := @@ -2798,7 +2802,6 @@ move=> suf X; apply/eqP; rewrite eq_le; apply/andP; split; Qed. Section caratheodory_theorem_sigma_algebra. - Variables (R : realType) (T : Type) (mu : {outer_measure set T -> \bar R}). Lemma outer_measure_bigcup_lim (A : (set T) ^nat) X : @@ -3508,7 +3511,7 @@ by rewrite /Hahn_ext /= measurable_mu_extE //; [exact: (mS i).2 | exact: (mS i).1]. Qed. -Lemma Hahn_ext_unique : @sigma_finite _ _ T setT mu -> +Lemma Hahn_ext_unique : sigma_finite [set: T] mu -> (forall mu' : {measure set I -> \bar R}, (forall X, d.-measurable X -> mu X = mu' X) -> (forall X, (d.-measurable).-sigma.-measurable X -> Hahn_ext X = mu' X)). @@ -3519,6 +3522,7 @@ apply: (@measure_unique _ _ [the measurableType _ of I] d.-measurable F) => //. - by move=> A Am; rewrite /= /Hahn_ext measurable_mu_extE// mu'mu. - by move=> k; rewrite /= /Hahn_ext measurable_mu_extE. Qed. + End Hahn_extension. Lemma caratheodory_measurable_mu_ext d (R : realType) (T : measurableType d) diff --git a/theories/numfun.v b/theories/numfun.v index e4d9707de5..f53c1744d3 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -30,10 +30,10 @@ Import numFieldTopology.Exports. Local Open Scope classical_set_scope. Local Open Scope ring_scope. -HB.mixin Record IsNonNegFun (aT : Type) (rT : numDomainType) (f : aT -> rT) := { +HB.mixin Record isNonNegFun (aT : Type) (rT : numDomainType) (f : aT -> rT) := { fun_ge0 : forall x, (0 <= f x)%R }. -HB.structure Definition NonNegFun aT rT := {f of @IsNonNegFun aT rT f}. +HB.structure Definition NonNegFun aT rT := {f of @isNonNegFun aT rT f}. Reserved Notation "{ 'nnfun' aT >-> T }" (at level 0, format "{ 'nnfun' aT >-> T }"). Reserved Notation "[ 'nnfun' 'of' f ]" @@ -253,29 +253,19 @@ Definition indic {T} {R : ringType} (A : set T) (x : T) : R := (x \in A)%:R. Reserved Notation "'\1_' A" (at level 8, A at level 2, format "'\1_' A") . Notation "'\1_' A" := (indic A) : ring_scope. -Lemma indicE {T} {R : ringType} (A : set T) (x : T) : - indic A x = (x \in A)%:R :> R. -Proof. by []. Qed. +Section indic_lemmas. +Context (T : Type) (R : ringType). +Implicit Types A D : set T. -Lemma indicT {T} {R : ringType} : \1_[set: T] = cst (1 : R). +Lemma indicE A (x : T) : \1_A x = (x \in A)%:R :> R. Proof. by []. Qed. + +Lemma indicT : \1_[set: T] = cst (1 : R). Proof. by apply/funext=> x; rewrite indicE in_setT. Qed. -Lemma indic0 {T} {R : ringType} : \1_(@set0 T) = cst (0 : R). +Lemma indic0 : \1_(@set0 T) = cst (0 : R). Proof. by apply/funext=> x; rewrite indicE in_set0. Qed. -Lemma indic_restrict {T : pointedType} {R : numFieldType} (A : set T) : - \1_A = 1 \_ A :> (T -> R). -Proof. by apply/funext => x; rewrite indicE /patch; case: ifP. Qed. - -Lemma restrict_indic T (R : numFieldType) (E A : set T) : - (\1_E \_ A) = \1_(E `&` A) :> (T -> R). -Proof. -apply/funext => x; rewrite /restrict 2!indicE. -case: ifPn => [|] xA; first by rewrite in_setI xA andbT. -by rewrite in_setI (negbTE xA) andbF. -Qed. - -Lemma preimage_indic (T : Type) (R : ringType) (D : set T) (B : set R) : +Lemma preimage_indic D (B : set R) : \1_D @^-1` B = if 1 \in B then (if 0 \in B then setT else D) else (if 0 \in B then ~` D else set0). Proof. @@ -294,7 +284,7 @@ rewrite /preimage/= /indic; apply/seteqP; split => x; by rewrite inE in B0. Qed. -Lemma image_indic T (R : ringType) (D A : set T) : +Lemma image_indic D A : \1_D @` A = (if A `\` D != set0 then [set 0] else set0) `|` (if A `&` D != set0 then [set 1 : R] else set0). Proof. @@ -305,19 +295,48 @@ by move=> []; case: ifPn; rewrite ?negbK// => /set0P[t [At Dt]] ->; exists t => //; case: (boolP (t \in D)); rewrite ?(inE, notin_set). Qed. -Lemma image_indic_sub T (R : ringType) (D A : set T) : - \1_D @` A `<=` [set (0 : R); 1]. +Lemma image_indic_sub D A : \1_D @` A `<=` ([set 0; 1] : set R). Proof. by rewrite image_indic; do ![case: ifP=> //= _] => // t []//= ->; [left|right]. Qed. -Lemma fimfunE T (R : ringType) (f : {fimfun T >-> R}) x : +Lemma fimfunE (f : {fimfun T >-> R}) x : f x = \sum_(y \in range f) (y * \1_(f @^-1` [set y]) x). Proof. rewrite (fsbigD1 (f x))// /= indicE mem_set// mulr1 fsbig1 ?addr0//. by move=> y [fy /= /nesym yfx]; rewrite indicE memNset ?mulr0. Qed. +End indic_lemmas. + +Lemma xsection_indic (R : ringType) T1 T2 (A : set (T1 * T2)) x : + xsection A x = (fun y => (\1_A (x, y) : R)) @^-1` [set 1]. +Proof. +apply/seteqP; split => [y/mem_set/=|y/=]; rewrite indicE. +by rewrite mem_xsection => ->. +by rewrite /xsection/=; case: (_ \in _) => //= /esym/eqP /[!oner_eq0]. +Qed. + +Lemma ysection_indic (R : ringType) T1 T2 (A : set (T1 * T2)) y : + ysection A y = (fun x => (\1_A (x, y) : R)) @^-1` [set 1]. +Proof. +apply/seteqP; split => [x/mem_set/=|x/=]; rewrite indicE. +by rewrite mem_ysection => ->. +by rewrite /ysection/=; case: (_ \in _) => //= /esym/eqP /[!oner_eq0]. +Qed. + +Lemma indic_restrict {T : pointedType} {R : numFieldType} (A : set T) : + \1_A = 1 \_ A :> (T -> R). +Proof. by apply/funext => x; rewrite indicE /patch; case: ifP. Qed. + +Lemma restrict_indic T (R : numFieldType) (E A : set T) : + (\1_E \_ A) = \1_(E `&` A) :> (T -> R). +Proof. +apply/funext => x; rewrite /restrict 2!indicE. +case: ifPn => [|] xA; first by rewrite in_setI xA andbT. +by rewrite in_setI (negbTE xA) andbF. +Qed. + Section ring. Context (aT : pointedType) (rT : ringType).