diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 2d85fdc0a..1c713c604 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -234,6 +234,24 @@ - in `measurable_structure.v`: + lemmas `countable_bigcap_measurable`, `countable_bigcup_measurable` +- in `lebesgue_stieltjes_measure.v`: + + module `MeasurableRocitv` + + definition `open_type` + + notations `.-open`, `.-open.-measurable` + + module `MeasurableRopen` + * definition `measurableTypeR` + + definition `lebesgue_display` + * definition `measurableR` + + lemmas `measurable_set1`, `measurable_itv` (also declared as hints) + + definition `ocitv_measure`, lemma `ocitv_measure_ext` + + module `MeasurableR` + + module `RGenOpenSets` + * lemma `measurableE` + + lemma `open_lebesgue_stieltjes_measure_unique` + +- in `real_interval.v`: + + lemma `set1_bigcap_oo` + ### Changed - in `realsum.v`: @@ -354,6 +372,15 @@ - in `classical_sets.v` + lemma `bigcupDr` -> `setD_bigcupr` (deprecating `bigcupDr`) +- moved from `measurable_realfun.v` to `lebesgue_stieltjes_measure.v` + + module `RGenOInfty` + + module `RGenInftyO` + + module `RGenCInfty` + + module `RGenOpens` + +- moved inside module `MeasurableRocitv` (`lebesgue_stieltjes_measure.v`): + + lemmas `measurable_set1`, `measurable_itv` + ### Renamed - in `tvs.v`: @@ -407,6 +434,9 @@ - in `functions.v` + lemma `scalrfctE` -> `scalerfctE` (deprecating `scalrfctE`) +- in `lebesgue_stieltjes_measure.v`: + + lemma `lebesgue_stieltjes_measure_unique` -> `ocitv_lebesgue_stieltjes_measure_unique` + ### Generalized - in `measurable_structure.v`: diff --git a/reals/real_interval.v b/reals/real_interval.v index b29819933..5775346a1 100644 --- a/reals/real_interval.v +++ b/reals/real_interval.v @@ -235,6 +235,18 @@ Qed. End set_ereal. +Lemma set1_bigcap_oo {R : realType} (x : R) : + [set x] = \bigcap_(k : nat) `]x - k.+1%:R^-1, x + k.+1%:R^-1[%classic. +Proof. +apply/seteqP; split => [_ -> k _|y xy] /=. + by rewrite in_itv/= ltrBlDr andbb ltrDl invr_gt0 ltr0n. +apply/eqP; rewrite eq_sym -subr_eq0 -normr_eq0 eq_le normr_ge0 andbT. +apply/ler_addgt0Pl => e e0; rewrite addr0. +have /= := xy (truncn e^-1) I. +rewrite in_itv/= -ltr_distlC => /ltW/le_trans; apply. +by rewrite invf_ple ?posrE ?ltr0n ?invr_gt0//; apply/ltW/truncnS_gt. +Qed. + Lemma set1_bigcap_oc (R : realType) (r : R) : [set r] = \bigcap_i `]r - i.+1%:R^-1, r]%classic. Proof. diff --git a/theories/borel_hierarchy.v b/theories/borel_hierarchy.v index 9fc7243db..3c11addd2 100644 --- a/theories/borel_hierarchy.v +++ b/theories/borel_hierarchy.v @@ -47,6 +47,8 @@ Proof. by exists (fun=> S)=> //; rewrite bigcup_const. Qed. End Gdelta_Fsigma. +Import MeasurableR. + Lemma Gdelta_measurable {R : realType} (S : set R) : Gdelta S -> measurable S. Proof. move=> [] B oB ->; apply: bigcapT_measurable => i. diff --git a/theories/ftc.v b/theories/ftc.v index ce2574b04..103f1a4e8 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -68,6 +68,8 @@ Notation mu := (@lebesgue_measure R). Local Open Scope ereal_scope. Implicit Types (f : R -> R) (a : itv_bound R). +Import MeasurableR. + Let FTC0 f a : mu.-integrable setT (EFin \o f) -> let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) f t)%R in forall x, a < BRight x -> lebesgue_pt f x -> @@ -328,6 +330,8 @@ End FTC. #[deprecated(since="mathcomp-analysis 1.17.0", note="renamed to `integrable_locally_restrict`")] Notation integrable_locally := integrable_locally_restrict (only parsing). +Import MeasurableR. + Definition parameterized_integral {R : realType} (mu : {measure set (measurableTypeR R) -> \bar R}) a x (f : R -> R) : R := @@ -524,6 +528,8 @@ rewrite mem_set ?mulr1 /=; first exact: subset_itv_oo_cc. exact: cvg_patch. Qed. +Import MeasurableR. + Corollary continuous_FTC2 f F a b : (a < b)%R -> {within `[a, b], continuous f} -> derivable_oo_LRcontinuous F a b -> @@ -772,6 +778,8 @@ Notation mu := lebesgue_measure. Local Open Scope ereal_scope. Implicit Types (F G f g : R -> R) (a b : R). +Import MeasurableR. + Lemma integration_by_parts F G f g a b : (a < b)%R -> {within `[a, b], continuous f} -> derivable_oo_LRcontinuous F a b -> @@ -824,6 +832,8 @@ Context {R : realType}. Notation mu := lebesgue_measure. Implicit Types (F G f g : R -> R) (a b : R). +Import MeasurableR. + Lemma Rintegration_by_parts F G f g a b : (a < b)%R -> {within `[a, b], continuous f} -> @@ -1030,6 +1040,8 @@ Context {R : realType}. Notation mu := lebesgue_measure. Implicit Types (F G f : R -> R) (a b : R). +Import MeasurableR. + Lemma integration_by_substitution_decreasing F G a b : (a <= b)%R -> {in `[a, b] &, {homo F : x y /~ (x < y)%R}} -> {in `]a, b[, continuous F^`()} -> @@ -1357,7 +1369,7 @@ transitivity (limn (fun n => rewrite -integral_bigsetU_EFin/=. - by move=> k; apply: measurableD => //; exact: bigsetU_measurable. - exact: iota_uniq. - - exact: (@sub_trivIset _ _ _ [set: nat]). + - exact: (@sub_trivIset _ _ _ setT). - apply/measurable_EFinP. apply: (measurable_funS (measurable_itv `]a, (a + n.+1%:R)%R[)). rewrite big_mkord -bigsetU_seqDU. @@ -1776,11 +1788,12 @@ Qed. End integration_by_substitution. - Section ge0_integration_by_substitution_shift. Context {R : realType}. Notation mu := (@lebesgue_measure R). +Import MeasurableR. + Lemma ge0_integration_by_substitution_shift_itvy (f : R -> R) (r e : R) : {within `[r + e, +oo[, continuous f} -> {in `]r + e, +oo[, forall x : R, 0 <= f x} -> @@ -1828,6 +1841,8 @@ Context {R : realType}. Let mu := (@lebesgue_measure R). Local Open Scope ereal_scope. +Import MeasurableR. + Lemma integration_by_substitution_onem (G : R -> R) (r : R) : (0 <= r <= 1)%R -> {within `[0%R, r], continuous G} -> @@ -1869,6 +1884,8 @@ Context {R : realType}. Let mu := @lebesgue_measure R. Local Open Scope ereal_scope. +Import MeasurableR. + Lemma ge0_symfun_integralT (f : R -> R) : (forall x, 0 <= f x)%R -> continuous f -> f =1 f \o -%R -> \int[mu]_x (f x)%:E = 2%:E * \int[mu]_(x in [set x | (0 <= x)%R]) (f x)%:E. @@ -1877,10 +1894,10 @@ move=> f0 cf evenf. have mf : measurable_fun [set: R] f by exact: continuous_measurable_fun. have mposnums : measurable [set x : R | 0 <= x]%R by rewrite -set_itvcy. rewrite -(setUv [set x : R | 0 <= x]%R) ge0_integral_setU//=. - exact: measurableC. - by apply/measurable_EFinP; rewrite setUv. - by move=> x _; rewrite lee_fin. - exact/disj_setPCl. +- exact: measurableC. +- by apply/measurable_EFinP; rewrite setUv. +- by move=> x _; rewrite lee_fin. +- exact/disj_setPCl. rewrite mule_natl mule2n; congr +%E. rewrite -set_itvcy// setCitvr. rewrite integral_itvbo_itvbc; first exact/measurable_EFinP/measurable_funTS. diff --git a/theories/gauss_integral.v b/theories/gauss_integral.v index 24f791266..b453d252b 100644 --- a/theories/gauss_integral.v +++ b/theories/gauss_integral.v @@ -41,6 +41,8 @@ by apply: (cvg_comp (fun x => x ^+ 2) (fun x => expR (- x))); [exact: cvgr_expr2|exact: cvgr_expR]. Qed. +Import MeasurableR. + Lemma measurable_gauss_fun : measurable_fun setT gauss_fun. Proof. by apply: measurableT_comp => //; exact: measurableT_comp. Qed. @@ -63,6 +65,8 @@ Implicit Type x : R. Let mu : {measure set _ -> \bar R} := @lebesgue_measure R. +Import MeasurableR. + Definition integral0y_gauss := \int[mu]_(x in `[0%R, +oo[) gauss_fun x. Let integral0y_gauss_ge0 : 0 <= integral0y_gauss. @@ -350,6 +354,8 @@ Context {R : realType}. Import gauss_integral_proof. Let mu := @lebesgue_measure R. +Import MeasurableR. + Lemma integral0y_gauss : (\int[mu]_(x in `[0%R, +oo[) (gauss_fun x)%:E)%E = (Num.sqrt pi / 2)%:E. Proof. diff --git a/theories/hoelder.v b/theories/hoelder.v index 003c63a01..0417243c7 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -357,11 +357,13 @@ Qed. End hoelder_conjugate. Section hoelder. -Context d {T : measurableType d} {R : realType}. -Variable mu : {measure set T -> \bar R}. +Context {d} {T : measurableType d} {R : realType} + (mu : {measure set T -> \bar R}). Local Open Scope ereal_scope. Implicit Types (p q : R) (f g : T -> R). +Import MeasurableR. + Let measurableT_comp_powR f p : measurable_fun [set: T] f -> measurable_fun setT (fun x => f x `^ p)%R. Proof. exact: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)). Qed. @@ -498,6 +500,8 @@ Section hoelder2. Context {R : realType}. Local Open Scope ring_scope. +Import MeasurableR. + Lemma hoelder2 (a1 a2 b1 b2 : R) (p q : R) : 0 <= a1 -> 0 <= a2 -> 0 <= b1 -> 0 <= b2 -> 0 < p -> 0 < q -> p^-1 + q^-1 = 1 -> @@ -534,6 +538,8 @@ Context {R : realType}. Local Open Scope ring_scope. Local Open Scope convex_scope. +Import MeasurableR. + Lemma convex_powR p : 1 <= p -> convex_function (`[0, +oo[%classic : set R) (@powR R ^~ p). Proof. @@ -579,8 +585,8 @@ Qed. End convex_powR. Section minkowski. -Context d (T : measurableType d) (R : realType). -Variable mu : {measure set T -> \bar R}. +Context {d} {T : measurableType d} {R : realType} + (mu : {measure set T -> \bar R}). Implicit Types (f g : T -> R) (p : R). Let convex_powR_abs_half f g p x : 1 <= p -> @@ -595,6 +601,8 @@ by apply: (convex_powR p1 (Itv01 _ _)) => //=; rewrite ?inE/= ?in_itv/= ?normr_ge0// ?invr_ge0// invf_le1 ?ler1n. Qed. +Import MeasurableR. + Let measurableT_comp_powR f p : measurable_fun setT f -> measurable_fun setT (fun x => f x `^ p)%R. Proof. exact: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)). Qed. @@ -788,6 +796,8 @@ Definition finite_norm d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}) (p : \bar R) (f : T -> R) := ('N[ mu ]_p [ EFin \o f ] < +oo)%E. +Import MeasurableR. + HB.mixin Record isLfunction d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E) (f : T -> R) & @MeasurableFun d _ T R f := { diff --git a/theories/independence.v b/theories/independence.v index 063012280..d65e088e1 100644 --- a/theories/independence.v +++ b/theories/independence.v @@ -427,8 +427,8 @@ Qed. End independent_generators. Section independent_RVs2. -Context {R : realType} d d' (T : measurableType d) (T' : measurableType d'). -Variable P : probability T R. +Context {R : realType} {d d'} {T : measurableType d} {T' : measurableType d'} + (P : probability T R). Definition independent_RVs2 (X Y : {mfun T >-> T'}) := independent_RVs P [set: bool] (fun b => if b then Y else X). @@ -436,10 +436,12 @@ Definition independent_RVs2 (X Y : {mfun T >-> T'}) := End independent_RVs2. Section independent_RVs2_properties. -Context {R : realType} d d' (T : measurableType d) (T' : measurableType d'). -Variable P : probability T R. +Context {R : realType} {d d'} {T : measurableType d} {T' : measurableType d'} + (P : probability T R). Local Open Scope ring_scope. +Import MeasurableR. + Lemma independent_RVs2_comp (X Y : {RV P >-> R}) (f g : {mfun R >-> R}) : independent_RVs2 P X Y -> independent_RVs2 P (f \o X) (g \o Y). Proof. @@ -517,10 +519,11 @@ HB.instance Definition _ (X Y : {RV P >-> T'}) := End pairRV. Section independent_RVs2_properties_realType. -Context {R : realType} d (T : measurableType d). -Variable P : probability T R. +Context {R : realType} {d} {T : measurableType d} (P : probability T R). Local Open Scope ereal_scope. +Import MeasurableR. + Lemma independent_RVs2_setI_preimage (X Y : {mfun T >-> R}) (A1 A2 : set R) : measurable A1 -> measurable A2 -> independent_RVs2 P X Y -> @@ -551,10 +554,11 @@ Qed. End independent_RVs2_properties_realType. Section product_expectation_over_product_measure. -Context {R : realType} d (T : measurableType d). -Variable P : probability T R. +Context {R : realType} {d} {T : measurableType d} (P : probability T R). Local Open Scope ereal_scope. +Import MeasurableR. + Lemma independent_Lfun1_expectation_product_measure_lty (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> (X : _ -> _) \in Lfun P 1 -> (Y : _ -> _) \in Lfun P 1 -> @@ -598,11 +602,11 @@ Qed. End product_expectation_over_product_measure. Section expectationM. -Context {R : realType} d (T : measurableType d). -Variable P : probability T R. +Context {R : realType} {d} {T : measurableType d} (P : probability T R). Local Open Scope ereal_scope. Import HBNNSimple. +Import MeasurableR. #[local] Lemma expectationM_nnsfun (f g : {nnsfun T >-> R}) : (forall y y', y \in range f -> y' \in range g -> @@ -773,11 +777,11 @@ Qed. End expectationM. Section product_expectation. -Context {R : realType} d (T : measurableType d). -Variable P : probability T R. +Context {R : realType} {d} {T : measurableType d} (P : probability T R). Local Open Scope ereal_scope. Import HBNNSimple. +Import MeasurableR. Lemma independent_Lfun1_expectationM_lty (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> diff --git a/theories/kernel.v b/theories/kernel.v index 7624108df..92c3b2dee 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -655,10 +655,11 @@ Qed. End measurable_fun_xsection_finite_kernel. Section measurable_fun_integral_finite_sfinite. -Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). -Variable k : X * Y -> \bar R. +Context {d d'} {X : measurableType d} {Y : measurableType d'} {R : realType} + (k : X * Y -> \bar R). Import HBNNSimple. +Import MeasurableR. Lemma measurable_fun_xsection_integral (l : X -> {measure set Y -> \bar R}) @@ -755,14 +756,16 @@ Arguments measurable_fun_integral_finite_kernel {_ _ _ _ _} k l. Arguments measurable_fun_integral_sfinite_kernel {_ _ _ _ _} k l. Section kdirac. -Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). -Variable f : X -> Y. +Context {d d'} {X : measurableType d} {Y : measurableType d'} {R : realType} + (f : X -> Y). Definition kdirac (mf : measurable_fun [set: X] f) (x : X) : {measure set Y -> \bar R} := dirac (f x). Hypothesis mf : measurable_fun [set: X] f. +Import MeasurableR. + Let measurable_fun_kdirac U : measurable U -> measurable_fun [set: X] (kdirac mf ^~ U). Proof. @@ -879,12 +882,14 @@ HB.instance Definition _ t := End fkadd. Section knormalize. -Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). -Variable f : R.-ker X ~> Y. +Context {d d'} {X : measurableType d} {Y : measurableType d'} {R : realType} + (f : R.-ker X ~> Y). Definition knormalize (P : probability Y R) : X -> {measure set Y -> \bar R} := fun x => mnormalize (f x) P. +Import MeasurableR. + Let measurable_knormalize (P : probability Y R) U : measurable U -> measurable_fun [set: X] (knormalize P ^~ U). Proof. @@ -926,6 +931,8 @@ HB.instance Definition _ (P : probability Y R):= End knormalize. +Import MeasurableR. + Lemma measurable_fun_mnormalize d d' (X : measurableType d) (Y : pmeasurableType d') (R : realType) (k : R.-ker X ~> Y) : measurable_fun [set: X] (fun x => mnormalize (k x) point : pprobability Y R). diff --git a/theories/lebesgue_integral_theory/giry.v b/theories/lebesgue_integral_theory/giry.v index e3c6b24c4..35bee8f84 100644 --- a/theories/lebesgue_integral_theory/giry.v +++ b/theories/lebesgue_integral_theory/giry.v @@ -96,11 +96,12 @@ End giry_def. Arguments giry_ev {d T R} mu A. Section giry_integral. -Context d (T : measurableType d) (R : realType). +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. +Import MeasurableR. (**md The idea is to reconstruct f from simple functions, then use measurability of giry_ev. Reference: Tom Avery. Codensity and the Giry monad. @@ -287,6 +288,7 @@ by apply: measurable_giry_int => //; exact: measurable_giry_ev. Qed. Import HBNNSimple. +Import MeasurableR. 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. @@ -451,8 +453,7 @@ End measurable_giry_prod. Section giry_prod_int. Context {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} - {R : realType}. -Variables (m1 : giry T1 R) (m2 : giry T2 R) (h : T1 * T2 -> \bar R). + {R : realType} (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 (m1, m2)) h = diff --git a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v index 82c8feb1e..22edbc7c2 100644 --- a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v +++ b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v @@ -106,6 +106,8 @@ Lemma Rintegral_ge0 D f : (forall x, D x -> 0 <= f x) -> 0 <= \int[mu]_(x in D) f x. Proof. by move=> f0; rewrite fine_ge0// integral_ge0. Qed. +Import MeasurableR. + Lemma le_normr_Rintegral D f : measurable D -> mu.-integrable D (EFin \o f) -> `|\int[mu]_(t in D) f t| <= \int[mu]_(t in D) `|f t|. Proof. @@ -197,6 +199,8 @@ Context {R : realType}. Notation mu := (@lebesgue_measure R). Implicit Type f : R -> R. +Import MeasurableR. + Lemma Rintegral_itvbo_itvbc (a : itv_bound R) (r : R) f : mu.-integrable [set` Interval a (BLeft r)] (EFin \o f) -> \int[mu]_(x in [set` Interval a (BLeft r)]) (f x) = diff --git a/theories/lebesgue_integral_theory/lebesgue_integrable.v b/theories/lebesgue_integral_theory/lebesgue_integrable.v index ca929f029..ffa046f9a 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integrable.v +++ b/theories/lebesgue_integral_theory/lebesgue_integrable.v @@ -283,6 +283,8 @@ case: fi => mf; apply: le_lt_trans; apply: ge0_le_integral => //. - by move=> x Dx; rewrite -/((abse \o f) x) -funeposDneg leeDl. Qed. +Import MeasurableR. + Lemma integrableMr (h : T -> R) g : measurable_fun D h -> [bounded h x | x in D] -> mu_int g -> mu_int ((EFin \o h) \* g). @@ -346,10 +348,12 @@ End integrable_theory. Arguments eq_integrable {d T R mu D} mD f. Section Rintegrable. -Context d {T : measurableType d} {R : realType}. -Variable mu : {measure set T -> \bar R}. +Context {d} {T : measurableType d} {R : realType} + (mu : {measure set T -> \bar R}). Implicit Types (D A B : set T) (f : T -> R). +Import MeasurableR. + Lemma integrable_norm D f : mu.-integrable D (EFin \o f) -> mu.-integrable D (EFin \o (normr \o f)). Proof. @@ -380,6 +384,8 @@ Proof. by move/integrable_funeneg => /[apply]; rewrite funerneg. Qed. End Rintegrable. +Import MeasurableR. + Lemma integrable_indic_itv {R : realType} (a b : R) (b0 b1 : bool) : let mu := lebesgue_measure in mu.-integrable setT (EFin \o \1_[set` Interval (BSide b0 a) (BSide b1 b)]). @@ -1068,7 +1074,7 @@ have nd_E : {homo E : n0 m / (n0 <= m)%N >-> (n0 <= m)%O}. rewrite set_lte_bigcup. have /cvg_lim h1 : (mu \o E) x @[x --> \oo]--> 0. by apply: cvg_near_cst; exact: nearW. -have := @nondecreasing_cvg_mu _ _ _ mu E mE (bigcupT_measurable E mE) nd_E. +have := @nondecreasing_cvg_measure _ _ _ mu E mE (bigcupT_measurable E mE) nd_E. by move/cvg_lim => h2; rewrite setI_bigcupr -h2// h1. Qed. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v index 36492890e..a95c9db3e 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v @@ -128,6 +128,7 @@ Variables m1 m2 : {measure set T -> \bar R}. Hypothesis m12 : forall S, measurable S -> m1 S <= m2 S. Import HBNNSimple. +Import MeasurableR. Lemma le_measure_sintegral (f : {nnsfun T >-> R}) : sintegral m1 f <= sintegral m2 f. @@ -164,6 +165,7 @@ Variables (m : {measure set T -> \bar R}). Variables (D : set T) (mD : measurable D) (f g : {nnsfun T >-> R}). Import HBNNSimple. +Import MeasurableR. Lemma sintegralD : sintegral m (f \+ g)%R = sintegral m f + sintegral m g. Proof. @@ -245,6 +247,8 @@ move=> n m nm; rewrite /fleg; apply/subsetPset => x /= cfg. by move: cfg => /le_trans; apply; exact: nd_g. Qed. +Import MeasurableR. + Let mfleg c n : measurable (fleg c n). Proof. rewrite /fleg [X in _ X](_ : _ = \big[setU/set0]_(y <- fset_set (range f)) @@ -508,8 +512,8 @@ End integral_indic. Section domain_change. Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType). -Variable mu : {measure set T -> \bar R}. +Context {d} {T : measurableType d} {R : realType} + (mu : {measure set T -> \bar R}). Lemma integral_mkcond D f : \int[mu]_(x in D) f x = \int[mu]_x (f \_ D) x. Proof. by rewrite /integral patch_setT. Qed. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v index cbe51946a..0621c3287 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v @@ -55,8 +55,9 @@ Local Open Scope classical_set_scope. Local Open Scope ring_scope. Section continuous_compact_integrable. -Context (rT : realType). +Context {rT : realType}. Let mu : measure _ _ := @lebesgue_measure rT. +Import MeasurableR. Let R : measurableType _ := measurableTypeR rT. Local Open Scope ereal_scope. @@ -76,6 +77,7 @@ End continuous_compact_integrable. Section continuous_density_L1. Context (rT : realType). Let mu : measure _ _ := @lebesgue_measure rT. +Import MeasurableR. Let R : measurableType _ := measurableTypeR rT. Local Open Scope ereal_scope. @@ -175,8 +177,9 @@ Qed. End continuous_density_L1. Section lebesgue_differentiation_continuous. -Context (rT : realType). +Context {rT : realType}. Let mu : measure _ _ := @lebesgue_measure rT. +Import MeasurableR. Let R : measurableType _ := measurableTypeR rT. Let ballE (x : R) (r : {posnum rT}) : @@ -212,7 +215,7 @@ have cptxr : compact `[x - r, x + r] := @segment_compact _ _ _. rewrite distrC subr0. have -> : \int[mu]_(z in ball x r) f z = \int[mu]_(z in `[x - r, x + r]) f z. rewrite ball_itv2 //; congr (fine _); rewrite -negligible_integral //. - - by apply/measurableU; exact: measurable_set1. + - exact/measurableU. - exact: (integrableS mA). - by rewrite measureU0//; exact: lebesgue_measure_set1. have r20 : 0 <= (r *+ 2)^-1 by rewrite invr_ge0 mulrn_wge0. @@ -260,6 +263,8 @@ Local Open Scope ereal_scope. Local Notation mu := lebesgue_measure. +Import MeasurableR. + Definition locally_integrable D f := [/\ measurable_fun D f, open D & forall K, K `<=` D -> compact K -> \int[mu]_(x in K) `|f x|%:E < +oo]. @@ -365,6 +370,8 @@ Local Open Scope ereal_scope. Local Notation mu := lebesgue_measure. +Import MeasurableR. + Definition iavg f A := (mu A)^-1 * \int[mu]_(y in A) `| (f y)%:E |. Lemma iavg0 f : iavg f set0 = 0. @@ -419,6 +426,8 @@ Definition HL_maximal f (x : R) : \bar R := Local Notation HL := HL_maximal. +Import MeasurableR. + Lemma HL_maximal_ge0 f D : locally_integrable D f -> forall x, 0 <= HL (f \_ D) x. Proof. @@ -611,6 +620,8 @@ Proof. by move=> r0; rewrite /davg/= (ball0 _ _).2//= iavg0. Qed. Lemma davg_ge0 f x (r : R) : 0 <= davg f x r. Proof. exact: iavg_ge0. Qed. +Import MeasurableR. + Lemma davgD f g (x r : R) : measurable_fun (ball x r) f -> measurable_fun (ball x r) g -> davg (f \+ g)%R x r <= (davg f x \+ davg g x) r. @@ -734,6 +745,8 @@ Local Notation "f ^*" := (lim_sup_davg f). Lemma lim_sup_davg_ge0 f x : 0 <= f^* x. Proof. by apply: limf_esup_ge0 => // => y; exact: iavg_ge0. Qed. +Import MeasurableR. + Lemma lim_sup_davg_le f g x (U : set R) : open_nbhs x U -> measurable U -> measurable_fun U f -> measurable_fun U g -> (f \+ g)%R^* x <= (f^* \+ g^*) x. @@ -836,6 +849,8 @@ End lim_sup_davg. Definition lebesgue_pt {R : realType} (f : R -> R) (x : R) := davg f x r @[r --> (0%R:R)^'+] --> 0%E. +Import MeasurableR. + Lemma continuous_lebesgue_pt {R : realType} (f : R -> R) x (U : set R) : open_nbhs x U -> measurable U -> measurable_fun U f -> {for x, continuous f} -> lebesgue_pt f x. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v b/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v index 5c49fd853..dcc3571ed 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v @@ -249,13 +249,14 @@ Qed. End dominated_convergence_theorem. Section simple_density_L1. -Context d (T : measurableType d) (R : realType). -Variables (mu : {measure set T -> \bar R}) (E : set T) (mE : measurable E). +Context {d} {T : measurableType d} {R : realType} + (mu : {measure set T -> \bar R}) (E : set T) (mE : measurable E). Local Open Scope ereal_scope. Import HBSimple. Import HBNNSimple. +Import MeasurableR. Let sfun_dense_L1_pos (f : T -> \bar R) : mu.-integrable E f -> (forall x, E x -> 0 <= f x) -> diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v index ae0c1570d..e1bb23655 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v @@ -293,11 +293,12 @@ End product_measure1. Section product_measure1E. Local Open Scope ereal_scope. -Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). -Variable m1 : {measure set T1 -> \bar R}. -Variable m2 : {sigma_finite_measure set T2 -> \bar R}. +Context {d1 d2} {T1 : measurableType d1} {T2 : measurableType d2} {R : realType} + (m1 : {measure set T1 -> \bar R}) (m2 : {sigma_finite_measure set T2 -> \bar R}). Implicit Types A : set (T1 * T2). +Import MeasurableR. + Lemma product_measure1E (A1 : set T1) (A2 : set T2) : measurable A1 -> measurable A2 -> (m1 \x m2) (A1 `*` A2) = m1 A1 * m2 A2. Proof. @@ -448,9 +449,11 @@ End product_measure2. Section product_measure2E. Local Open Scope ereal_scope. -Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). -Variable m1 : {sigma_finite_measure set T1 -> \bar R}. -Variable m2 : {measure set T2 -> \bar R}. +Context {d1 d2} {T1 : measurableType d1} {T2 : measurableType d2} {R : realType} + (m1 : {sigma_finite_measure set T1 -> \bar R}) + (m2 : {measure set T2 -> \bar R}). + +Import MeasurableR. Lemma product_measure2E (A1 : set T1) (A2 : set T2) (mA1 : measurable A1) (mA2 : measurable A2) : @@ -567,9 +570,10 @@ Qed. End indic_fubini_tonelli. Section sfun_fubini_tonelli. -Variable f : {nnsfun T1 * T2 >-> R}. +Context (f : {nnsfun T1 * T2 >-> R}). Import HBNNSimple. +Import MeasurableR. Let F := fubini_F m2 (EFin \o f). Let G := fubini_G m1 (EFin \o f). @@ -684,7 +688,7 @@ Qed. End sfun_fubini_tonelli. Section fubini_tonelli. -Variable f : T1 * T2 -> \bar R. +Context (f : T1 * T2 -> \bar R). Hypothesis mf : measurable_fun setT f. Hypothesis f0 : forall x, 0 <= f x. Let T : measurableType _ := (T1 * T2)%type. @@ -693,6 +697,7 @@ Let F := fubini_F m2 f. Let G := fubini_G m1 f. Import HBNNSimple. +Import MeasurableR. Let F_ (g : {nnsfun T >-> R}^nat) n x := \int[m2]_y (g n (x, y))%:E. Let G_ (g : {nnsfun T >-> R}^nat) n y := \int[m1]_x (g n (x, y))%:E. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v index c93a22e0f..db7889adb 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v @@ -42,10 +42,11 @@ Local Open Scope ring_scope. Section eq_measure_integral. Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType) (D : set T). +Context {d} {T : measurableType d} {R : realType} (D : set T). Implicit Types m : {measure set T -> \bar R}. Import HBNNSimple. +Import MeasurableR. Let eq_measure_integral0 m2 m1 (f : T -> \bar R) : (forall A, measurable A -> A `<=` D -> m1 A = m2 A) -> @@ -325,8 +326,8 @@ End ge0_integralZ. Section integralZl_indic. Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType). -Variables (m : {measure set T -> \bar R}) (D : set T) (mD : measurable D). +Context {d} {T : measurableType d} {R : realType} + (m : {measure set T -> \bar R}) (D : set T) (mD : measurable D). Lemma integralZl_indic (f : R -> set T) (k : R) : ((k < 0)%R -> f k = set0) -> measurable (f k) -> @@ -341,6 +342,7 @@ rewrite ge0_integralZl//; exact/measurable_EFinP. Qed. Import HBNNSimple. +Import MeasurableR. Lemma integralZl_indic_nnsfun (f : {nnsfun T >-> R}) (k : R) : \int[m]_(x in D) (k * \1_(f @^-1` [set k]) x)%:E = @@ -355,9 +357,9 @@ Arguments integralZl_indic {d T R m D} mD f. Section ge0_integral_mscale. Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType). -Variables (m : {measure set T -> \bar R}) (D : set T) (mD : measurable D). -Variables (k : {nonneg R}) (f : T -> \bar R). +Context {d} {T : measurableType d} {R : realType} + (m : {measure set T -> \bar R}) (D : set T) (mD : measurable D) + (k : {nonneg R}) (f : T -> \bar R). Let integral_mscale_indic E : measurable E -> \int[mscale k m]_(x in D) (\1_E x)%:E = @@ -365,6 +367,7 @@ Let integral_mscale_indic E : measurable E -> Proof. by move=> ?; rewrite !integral_indic. Qed. Import HBNNSimple. +Import MeasurableR. Let integral_mscale_nnsfun (h : {nnsfun T >-> R}) : \int[mscale k m]_(x in D) (h x)%:E = k%:num%:E * \int[m]_(x in D) (h x)%:E. @@ -513,13 +516,14 @@ End integral_cst. Section ge0_transfer. Local Open Scope ereal_scope. -Context d1 d2 (X : measurableType d1) (Y : measurableType d2) (R : realType). -Variables (phi : X -> Y) (mphi : measurable_fun setT phi). -Variables (mu : {measure set X -> \bar R}). +Context {d1 d2} {X : measurableType d1} {Y : measurableType d2} {R : realType} + (phi : X -> Y) (mphi : measurable_fun setT phi) + (mu : {measure set X -> \bar R}). Let mphi_mixin := isMeasurableFun.Build _ _ _ _ _ mphi. Let mphi_pack : {mfun _ >-> _} := HB.pack phi mphi_mixin. Import HBNNSimple. +Import MeasurableR. Lemma ge0_integral_pushforward D (f : Y -> \bar R) : measurable D -> measurable_fun D f -> {in D, forall y, 0 <= f y} -> @@ -573,6 +577,7 @@ Open Scope ereal_scope. Context {R : realType}. Local Notation mu := lebesgue_measure. +Import MeasurableR. Lemma lebesgue_measureN (A : set R) : measurable A -> pushforward mu (-%R : _ -> measurableTypeR R) A = mu A. @@ -597,10 +602,11 @@ End change_of_variable. Section integral_dirac. Local Open Scope ereal_scope. -Context d (T : measurableType d) (a : T) (R : realType). -Variables (D : set T) (mD : measurable D). +Context {d} {T : measurableType d} (a : T) {R : realType} + (D : set T) (mD : measurable D). Import HBNNSimple. +Import MeasurableR. Let ge0_integral_dirac (f : T -> \bar R) (mf : measurable_fun D f) (f0 : forall x, D x -> 0 <= f x) : @@ -657,8 +663,8 @@ Qed. Section integral_measure_sum_nnsfun. Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType). -Variables (m_ : {measure set T -> \bar R}^nat) (N : nat). +Context {d} {T : measurableType d} {R : realType} + (m_ : {measure set T -> \bar R}^nat) (N : nat). Let m := msum m_ N. Let integral_measure_sum_indic (E D : set T) (mE : measurable E) @@ -670,6 +676,7 @@ by rewrite integral_indic// setIT. Qed. Import HBNNSimple. +Import MeasurableR. Let integralT_measure_sum (f : {nnsfun T >-> R}) : \int[m]_x (f x)%:E = \sum_(n < N) \int[m_ n]_x (f x)%:E. @@ -776,8 +783,8 @@ Qed. Section integral_measure_series. Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType). -Variable m_ : {measure set T -> \bar R}^nat. +Context {d} {T : measurableType d} {R : realType} + (m_ : {measure set T -> \bar R}^nat). Let m := mseries m_ O. Let integral_measure_series_indic (D : set T) (mD : measurable D) : @@ -788,6 +795,7 @@ by rewrite integral_indic// setIT. Qed. Import HBNNSimple. +Import MeasurableR. Lemma integral_measure_series_nnsfun (D : set T) (mD : measurable D) (f : {nnsfun T >-> R}) : @@ -939,8 +947,8 @@ End subset_integral. Section integral_setU_EFin. Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType) - (mu : {measure set T -> \bar R}). +Context {d} {T : measurableType d} {R : realType} + (mu : {measure set T -> \bar R}). Lemma integral_setU (A B : set T) (f : T -> \bar R) : measurable A -> measurable B -> @@ -961,6 +969,8 @@ rewrite oppeD 1?addeACA//. by rewrite ge0_adde_def// inE integral_ge0. Qed. +Import MeasurableR. + Lemma __deprecated__integral_setU_EFin (A B : set T) (f : T -> R) : measurable A -> measurable B -> measurable_fun (A `|` B) f -> @@ -1078,10 +1088,12 @@ End integral_patch. Section ge0_cvgn_integral. Local Open Scope ereal_scope. -Context {R : realType}. -Variable mu : {measure set (@measurableTypeR R) -> \bar R}. +Import MeasurableR. +Context {R : realType} (mu : {measure set (@measurableTypeR R) -> \bar R}). Variable f : R -> R. Hypothesis f0 : (forall x, 0 <= f x)%R. + + Hypothesis mf : measurable_fun setT f. Lemma ge0_integral_ereal_sup : @@ -1171,6 +1183,8 @@ move: foo; rewrite integralE/= -fin_num_abs fin_numB => /andP[fpoo fnoo]. by rewrite lte_add_pinfty// ltey_eq ?fpoo ?fnoo. Qed. +Import MeasurableR. + Lemma integral_fin_num_abs d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}) (D : set T) (f : T -> R) : measurable D -> measurable_fun D f -> @@ -1300,17 +1314,16 @@ move=> mf; split=> [iDf0|Df0]. by rewrite (le_trans (ltW (truncnS_gt _))). by split => //; apply: contraTN nft => /eqP ->; rewrite abse0 -ltNge. transitivity (limn (fun n => mu (D `&` [set x | `|f x| >= n.+1%:R^-1%:E]))). - apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu. - - move=> i; apply: emeasurable_fun_c_infty => //. - exact: measurableT_comp. + apply/esym/cvg_lim => //; apply: nondecreasing_cvg_measure. + - by move=> i; apply: emeasurable_fun_c_infty=> //; exact: measurableT_comp. - apply: bigcupT_measurable => i. by apply: emeasurable_fun_c_infty => //; exact: measurableT_comp. - move=> m n mn; apply/subsetPset; apply: setIS => t /=. by apply: le_trans; rewrite lee_fin lef_pV2 // ?ler_nat // posrE. - by rewrite (_ : (fun _ => _) = cst 0) ?lim_cst//= funeqE => n /=; rewrite muDf. + by rewrite (_ : (fun _ => _) = cst 0) ?lim_cst//= funeqE => n/=; rewrite muDf. pose f_ := fun n x => mine `|f x| n%:R%:E. have -> : (fun x => `|f x|) = (fun x => limn (f_^~ x)). - rewrite funeqE => x; apply/esym/cvg_lim => //; apply/cvg_ballP => _/posnumP[e]. + rewrite funeqE => x; apply/esym/cvg_lim=> //; apply/cvg_ballP => _/posnumP[e]. near=> n; rewrite /ball /= /ereal_ball /= /f_. have [->|fxoo] := eqVneq `|f x|%E +oo. rewrite -[contract +oo](@divff _ (1 + n%:R)) ?nat1r//=. @@ -1604,8 +1617,8 @@ Notation integral_itv_obnd_cbnd := integral_itvob_itvcb (only parsing). Notation integral_itv_bndoo := integral_itvbb_itvoo (only parsing). Section ge0_nondecreasing_set_cvg_integral. -Context {d : measure_display} {T : measurableType d} {R : realType}. -Variables (F : (set T)^nat) (f : T -> \bar R) (mu : measure T R). +Context {d} {T : measurableType d} {R : realType} (F : (set T)^nat) + (f : T -> \bar R) (mu : measure T R). Local Open Scope ereal_scope. Hypotheses (nndF : nondecreasing_seq F) (mF : forall i, measurable (F i)). Hypothesis mf : forall i, measurable_fun (F i) f. diff --git a/theories/lebesgue_integral_theory/measurable_fun_approximation.v b/theories/lebesgue_integral_theory/measurable_fun_approximation.v index 3c02ce4dd..9ca587ff1 100644 --- a/theories/lebesgue_integral_theory/measurable_fun_approximation.v +++ b/theories/lebesgue_integral_theory/measurable_fun_approximation.v @@ -92,9 +92,8 @@ Qed. End dyadic_interval. Section approximation. -Context d (T : measurableType d) (R : realType). -Variables (D : set T) (mD : measurable D). -Variables (f : T -> \bar R) (mf : measurable_fun D f). +Context {d} {T : measurableType d} {R : realType} + (D : set T) (mD : measurable D) (f : T -> \bar R) (mf : measurable_fun D f). Local Notation I := (@dyadic_itv R). @@ -113,7 +112,7 @@ Definition approx : (T -> R)^nat := fun n x => Let mA n k : measurable (A n k). Proof. rewrite /A; case: ifPn => [kn|_]//; rewrite -preimage_comp. -by apply: mf => //; apply/measurable_image_EFin; exact: measurable_itv. +by apply: mf => //; exact/measurable_image_EFin. Qed. Let trivIsetA n : trivIset setT (A n). @@ -411,6 +410,7 @@ Context d (T : measurableType d) (R : realType). Implicit Types (D : set T) (f g : T -> \bar R). Import HBSimple. +Import MeasurableR. Lemma emeasurable_funD D f g : measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \+ g). @@ -563,6 +563,8 @@ Section measurable_sum. Context d (T : measurableType d) (R : realType). Implicit Types (D : set T) (f g : T -> R). +Import MeasurableR. + Lemma measurable_sum D I s (h : I -> T -> R) : (forall i, measurable_fun D (h i)) -> measurable_fun D (fun x => \sum_(i <- s) h i x). @@ -660,6 +662,8 @@ Qed. End emeasurable_fun_comparison. +Import MeasurableR. + Lemma measurable_poweR (R : realType) r : measurable_fun [set: \bar R] (poweR ^~ r). Proof. @@ -711,9 +715,11 @@ Let lusin_simple (f : {sfun R >-> rT}) (eps : rT) : (0 < eps)%R -> Proof. move: eps=> _/posnumP[eps]; have [N /card_fset_set rfN] := fimfunP f. pose Af x : set R := A `&` f @^-1` [set x]. -have mAf x : measurable (Af x) by exact: measurableI. +have mAf x : (@open R).-sigma.-measurable (Af x). + exact: measurableI. have finAf x : mu (Af x) < +oo. - by rewrite (le_lt_trans _ finA)// le_measure// ?inE//; exact: subIsetl. + rewrite (le_lt_trans _ finA)// le_measure// ?inE//. + - exact: subIsetl. have eNpos : (0 < eps%:num / N.+1%:R)%R by []. have dK' x := lebesgue_regularity_inner (mAf x) (finAf x) eNpos. pose dK x : set R := projT1 (cid (dK' x)); pose J i : set R := Af i `\` dK i. @@ -732,7 +738,8 @@ exists (\bigcup_(i in range f) dK i); split. case => ? [? _ <-] [[zab /= <- nfz]] ? [r _ <-]; split => //. by move: nfz; apply: contra_not => /[dup] /dKsub ->. apply: (@le_lt_trans _ _ (\sum_(i \in range f) mu (J i))). - by apply: content_sub_fsum => //; exact: fin_bigcup_measurable. + apply: content_sub_fsum => //. + exact: fin_bigcup_measurable. apply: le_lt_trans. apply: (@lee_fsum _ _ _ _ (fun=> (eps%:num / N.+1%:R)%:E * 1%:E)) => //. by move=> i ?; rewrite mule1; apply: ltW; have [_ _] := dkP i. diff --git a/theories/lebesgue_integral_theory/radon_nikodym.v b/theories/lebesgue_integral_theory/radon_nikodym.v index 644b3fe71..46363a4b6 100644 --- a/theories/lebesgue_integral_theory/radon_nikodym.v +++ b/theories/lebesgue_integral_theory/radon_nikodym.v @@ -133,15 +133,16 @@ Qed. End dominates_induced. Section integral_normr_continuous. -Context d (T : measurableType d) {R : realType} (mu : {measure set T -> \bar R}). Local Open Scope ereal_scope. - -Variable f : T -> R. +Context d (T : measurableType d) {R : realType} (mu : {measure set T -> \bar R}) + (f : T -> R). Hypothesis intf : mu.-integrable setT (EFin \o f). Let intnf : mu.-integrable setT (abse \o EFin \o f). Proof. exact: integrable_abse. Qed. +Import MeasurableR. + Lemma integral_normr_continuous (e : R) : (0 < e)%R -> exists d : R, (0 < d)%R /\ forall A, measurable A -> mu A < d%:E -> (\int[mu]_(x in A) `|f x| < e)%R. @@ -843,15 +844,16 @@ Proof. by rewrite /f; case: pselect => // numu _; case: cid => x []. Qed. End radon_nikodym_sigma_finite_def. Section integrableM. -Context d (T : measurableType d) (R : realType). -Variables (nu : {finite_measure set T -> \bar R}) - (mu : {sigma_finite_measure set T -> \bar R}). +Context {d} {T : measurableType d} {R : realType} + (nu : {finite_measure set T -> \bar R}) + (mu : {sigma_finite_measure set T -> \bar R}). Hypothesis numu : nu `<< mu. Implicit Types f : T -> \bar R. Local Notation "'d nu '/d mu" := (f nu mu). Import HBNNSimple. +Import MeasurableR. Lemma change_of_variables f E : (forall x, 0 <= f x) -> measurable E -> measurable_fun E f -> @@ -1105,10 +1107,9 @@ Qed. End radon_nikodym_lemmas. Section Radon_Nikodym_chain_rule. -Context d (T : measurableType d) (R : realType). -Variables (nu : {charge set T -> \bar R}) - (la : {sigma_finite_measure set T -> \bar R}) - (mu : {finite_measure set T -> \bar R}). +Context {d} {T : measurableType d} {R : realType} + (nu : {charge set T -> \bar R}) (la : {sigma_finite_measure set T -> \bar R}) + (mu : {finite_measure set T -> \bar R}). Lemma Radon_Nikodym_chain_rule : nu `<< mu -> mu `<< la -> ae_eq la setT ('d nu '/d la) diff --git a/theories/lebesgue_integral_theory/simple_functions.v b/theories/lebesgue_integral_theory/simple_functions.v index 8e1a5bd7e..7aa5da011 100644 --- a/theories/lebesgue_integral_theory/simple_functions.v +++ b/theories/lebesgue_integral_theory/simple_functions.v @@ -71,6 +71,7 @@ Local Open Scope classical_set_scope. Local Open Scope ring_scope. Module HBSimple. +Import MeasurableR. HB.structure Definition SimpleFun d (aT : sigmaRingType d) (rT : realType) := {f of @isMeasurableFun d _ aT rT f & @FiniteImage aT rT f}. @@ -94,6 +95,7 @@ Notation "[ 'nnsfun' 'of' f ]" := [the {nnsfun _ >-> _} of f] : form_scope. Section sfun_pred. Context {d} {aT : sigmaRingType d} {rT : realType}. +Import MeasurableR. Definition sfun : {pred _ -> _} := [predI @mfun _ _ aT rT & fimfun]. Definition sfun_key : pred_key sfun. Proof. exact. Qed. Canonical sfun_keyed := KeyedPred sfun_key. @@ -107,6 +109,7 @@ Notation T := {sfun aT >-> rT}. Notation sfun := (@sfun _ aT rT). Section Sub. Context (f : aT -> rT) (fP : f \in sfun). +Import MeasurableR. Definition sfun_Sub1_subproof := @isMeasurableFun.Build d _ aT rT f (set_mem (sub_sfun_mfun fP)). #[local] HB.instance Definition _ := sfun_Sub1_subproof. @@ -140,6 +143,8 @@ Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed. HB.instance Definition _ := [Choice of {sfun aT >-> rT} by <:]. +Import MeasurableR. + (* NB: already in cardinality.v *) HB.instance Definition _ x : @FImFun aT rT (cst x) := FImFun.on (cst x). @@ -194,6 +199,8 @@ Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed. Lemma sfunX f n : f ^+ n =1 (fun x => f x ^+ n). Proof. by move=> x; elim: n => [|n IHn]//; rewrite !exprS sfunM/= IHn. Qed. +Import MeasurableR. + HB.instance Definition _ f g := MeasurableFun.copy (f \+ g) (f + g). HB.instance Definition _ f g := MeasurableFun.copy (\- f) (- f). HB.instance Definition _ f g := MeasurableFun.copy (f \- g) (f - g). @@ -251,6 +258,7 @@ Section nnsfun_functions. Context d (T : measurableType d) (R : realType). Import HBNNSimple. +Import MeasurableR. Lemma cst_nnfun_subproof (x : {nonneg R}) : forall t : T, 0 <= cst x%:num t. Proof. by move=> /=. Qed. @@ -295,6 +303,7 @@ Context d (T : measurableType d) (R : realType). Variables f g : {nnsfun T >-> R}. Import HBNNSimple. +Import MeasurableR. HB.instance Definition _ := MeasurableFun.on (f \+ g). Definition add_nnsfun : {nnsfun T >-> R} := f \+ g. @@ -382,6 +391,7 @@ by rewrite fsbig_finite// -measure_fin_bigcup// -bigsetU_fset_set. Qed. Import HBNNSimple. +Import MeasurableR. Lemma additive_nnsfunr (g f : {nnsfun T >-> R}) x : \sum_(i \in range g) m (f @^-1` [set x] `&` (g @^-1` [set i])) = diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 8d55c854e..1cf57d073 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -339,15 +339,16 @@ End LebesgueMeasure. Definition lebesgue_measure {R : realType} : set R -> \bar R := lebesgue_stieltjes_measure idfun. +Import MeasurableRopen. HB.instance Definition _ (R : realType) := Measure.on (@lebesgue_measure R). HB.instance Definition _ (R : realType) := SigmaFiniteMeasure.on (@lebesgue_measure R). Lemma lebesgue_measure_unique {R : realType} - (mu : {measure set (measurableTypeR R) -> \bar R}) : + (mu : {measure set (MeasurableRopen.measurableTypeR R) -> \bar R}) : (forall X, ocitv X -> lebesgue_measure X = mu X) -> forall A, measurable A -> lebesgue_measure A = mu A. -Proof. exact: lebesgue_stieltjes_measure_unique. Qed. +Proof. exact: open_lebesgue_stieltjes_measure_unique. Qed. Definition completed_lebesgue_measure {R : realType} : set _ -> \bar R := completed_lebesgue_stieltjes_measure idfun. @@ -409,7 +410,8 @@ have mF_ m : mu (F_ m) < completed_mu E + m.+1%:R^-1%:E. pose F := \bigcap_n (F_ n). have FM : @measurable _ (measurableTypeR R) F. apply: bigcapT_measurable => k; apply: bigcupT_measurable => i. - by apply: sub_sigma_algebra; have [/(_ i)] := mA k. + have [/(_ i)] := mA k; rewrite -RGenOpenSets.measurableE=> maki _; + exact: sub_sigma_algebra. have EF : E `<=` F by exact: sub_bigcap. have muEF : completed_mu E = mu F. apply/eqP; rewrite eq_le le_outer_measure//=. @@ -444,7 +446,8 @@ have mG_ m : mu (G_ m) < completed_mu (F `\` E) + m.+1%:R^-1%:E. pose G := \bigcap_n (G_ n). have GM : @measurable _ (measurableTypeR R) G. apply: bigcapT_measurable => k; apply: bigcupT_measurable => i. - by apply: sub_sigma_algebra; have [/(_ i)] := mB k. + have [/(_ i)] := mB k; rewrite -RGenOpenSets.measurableE=> mbki _; + exact: sub_sigma_algebra. have FEG : F `\` E `<=` G by exact: sub_bigcap. have muG : mu G = 0. transitivity (completed_mu (F `\` E)). @@ -456,7 +459,7 @@ have muG : mu G = 0. rewrite (le_trans (ltW (mG_ n)))// leeD// lee_fin ltW//. by near: n; apply: near_infty_natSinv_lt. rewrite measureD//=. - + exact: sub_caratheodory. + + by apply: sub_caratheodory; rewrite RGenOpenSets.measurableE. + by move: mEoo; rewrite muEF. + by rewrite setIidr// muEF subee// ge0_fin_numE//; move: mEoo; rewrite muEF. apply: sub_sigma_algebra; exists (F `\` G); first exact: measurableD. @@ -519,9 +522,11 @@ Let calgebra_sub_cara : (completed_algebra_gen mu).-sigma.-measurable `<=` hlength^*%mu.-cara.-measurable. Proof. rewrite g_sigma_completed_algebra_genE => A -[/= X mX] [N negN] <-{A}. -apply: measurableU => //; first exact: sub_caratheodory. +apply: measurableU => //; first by apply: sub_caratheodory; + rewrite RGenOpenSets.measurableE. apply: negligible_sub_caratheodory; case: negN => /= B [mB B0 NB]. -by exists B; split => //=; exact: sub_caratheodory. +by exists B; split => //=; apply: sub_caratheodory; + rewrite RGenOpenSets.measurableE. Qed. Lemma completed_caratheodory_measurable : @@ -560,7 +565,8 @@ apply: (@measure_semi_sigma_additive _ _ _ (@lebesgue_measure R) move=> [X mX [X' mX']] XX'Fn. apply: measurable_image_fine. rewrite -XX'Fn. - apply: measurableU; first exact: measurable_image_EFin. + apply: measurableU; first by apply: measurable_image_EFin; + rewrite RGenOpenSets.measurableE/= in mX. by case: mX' => //; exact: measurableU. - move=> i j _ _ [x [[a [Fia aoo ax] [b [Fjb boo] bx]]]]. move: tF => /(_ i j Logic.I Logic.I); apply. @@ -577,7 +583,8 @@ apply: (@measure_semi_sigma_additive _ _ _ (@lebesgue_measure R) + by rewrite not_orP => -[]/(_ erefl). + by rewrite not_orP => -[]/(_ erefl). - move: mUF. - rewrite {1}/measurable /emeasurable /= => -[X mX [Y []]] {Y}. + rewrite {1}/measurable /emeasurable /= => -[X mX [Y []]] {Y}; + have moX : measurable X by rewrite -RGenOpenSets.measurableE. - rewrite setU0 => h. rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr]. move=> -[n _ [x [Fnx xoo <-{r}]]]. @@ -616,7 +623,7 @@ HB.instance Definition _ := isMeasure.Build _ _ _ elebesgue_measure End elebesgue_measure. Section lebesgue_measure_itv. -Variable R : realType. +Context {R : realType}. Let lebesgue_measure_itvoc (a b : R) : (lebesgue_measure (`]a, b] : set R) = wlength idfun `]a, b])%classic. @@ -630,9 +637,8 @@ Let lebesgue_measure_itvoo_subr1 (a : R) : Proof. rewrite itv_bnd_open_bigcup//; transitivity (limn (lebesgue_measure \o (fun k => `]a - 1, a - k.+1%:R^-1]%classic : set R))). - apply/esym/cvg_lim => //; apply: nondecreasing_cvg_measure. - - by move=> ?; exact: measurable_itv. - - by apply: bigcup_measurable => k _; exact: measurable_itv. + apply/esym/cvg_lim => //; apply: nondecreasing_cvg_measure => //. + - exact: bigcup_measurable. - move=> n m nm; apply/subsetPset => x /=; rewrite !in_itv/= => /andP[->/=]. by move/le_trans; apply; rewrite lerB// lef_pV2 ?ler_nat ?posrE. rewrite (_ : _ \o _ = (fun n => (1 - n.+1%:R^-1)%:E)). @@ -671,8 +677,7 @@ rewrite [X in lebesgue_measure X](_ : _ = \bigcup_(x in f @` A) rewrite eqEsubset; split => [r [n]|r [n]]. by move=> [t At ftn] Afnr; exists n => //=; exists t. by move=> [t At ftn] /= rAfn; exists n => //=; exists t. -rewrite measure_bigcup/=. - by move=> ? _; exact: measurable_set1. +rewrite measure_bigcup//=. move=> i j [r Ar <-] [s As <-]. by rewrite !pinvKV ?inE// => -[x [/= <- <-]]. apply: lim_near_cst => //. @@ -728,9 +733,8 @@ Let lebesgue_measure_itv_bnd_infty x (a : R) : Proof. rewrite itv_bndy_bigcup_BRight; transitivity (limn (lebesgue_measure \o (fun k => [set` Interval (BSide x a) (BRight (a + k%:R))] : set R))). - apply/esym/cvg_lim => //; apply: nondecreasing_cvg_measure. - + by move=> k; exact: measurable_itv. - + by apply: bigcup_measurable => k _; exact: measurable_itv. + apply/esym/cvg_lim => //; apply: nondecreasing_cvg_measure => //. + + exact: bigcup_measurable. + move=> m n mn; apply/subsetPset => r/=; rewrite !in_itv/= => /andP[->/=]. by move=> /le_trans; apply; rewrite lerD// ler_nat. rewrite (_ : _ \o _ = (fun k => k%:R%:E))//. @@ -744,9 +748,8 @@ Let lebesgue_measure_itv_infty_bnd y (b : R) : Proof. rewrite itvNy_bnd_bigcup_BLeft; transitivity (limn (lebesgue_measure \o (fun k => [set` Interval (BLeft (b - k%:R)) (BSide y b)] : set R))). - apply/esym/cvg_lim => //; apply: nondecreasing_cvg_measure. - + by move=> k; exact: measurable_itv. - + by apply: bigcup_measurable => k _; exact: measurable_itv. + apply/esym/cvg_lim => //; apply: nondecreasing_cvg_measure => //. + + exact: bigcup_measurable. + move=> m n mn; apply/subsetPset => r/=; rewrite !in_itv/= => /andP[+ ->]. by rewrite andbT; apply: le_trans; rewrite lerB// ler_nat. rewrite (_ : _ \o _ = (fun k : nat => k%:R%:E))//. @@ -902,7 +905,7 @@ split=> [[/= A [mA mA0 NA]]|N0]. - by apply/eqP; rewrite eq_le outer_measure_ge0 andbT -mA0 le_outer_measure. - have := @outer_measure_Gdelta N; rewrite N0 => -[F [oF NF mF0]]. exists (\bigcap_i F i); split => //=. - by apply: bigcapT_measurable => i; exact: open_measurable. + apply: bigcapT_measurable => i; exact: sub_sigma_algebra. Qed. End negligible_outer_measure. @@ -933,9 +936,7 @@ have muM n : mu (M n) <= mu (M' n) + (e2 n)%:E. apply: funext=> r /=; rewrite (@itv_splitU _ _ (BRight b)). by rewrite !bnd_simp (ltW alb)/= ltr_pwDr. by rewrite propeqE; split=> /orP. - rewrite measureU/=. - - by apply: sub_sigma_algebra; exact: is_ocitv. - - by apply: open_measurable; exact: interval_open. + rewrite measureU//=. - rewrite eqEsubset; split => // r []/andP [_ +] /andP[+ _] /=. by rewrite !bnd_simp => /le_lt_trans /[apply]; rewrite ltxx. - rewrite !lebesgue_measure_itv/= !lte_fin alb ltr_pwDr//=. @@ -948,9 +949,7 @@ exists U; have DU : D `<=` U. by case: covDM => /(_ n). rewrite /= !in_itv/= => /andP[ax xb]; rewrite ?inf_itv ?sup_itv//. by rewrite ax/= (le_lt_trans xb)// ltr_pwDr. -have mM n : measurable (M n). - rewrite /M; case: pselect; first by move=> /= _; exact: measurable0. - by move=> /= _; apply: open_measurable; apply: interval_open. +have mM n : measurable (M n) by rewrite /M; case: pselect => //=. have muU : mu U < mu D + eps%:E. apply: (@le_lt_trans _ _ (\sum_(n i _. rewrite /= -wlength_Rhull wlength_itv !er_map_idfun. - rewrite -lebesgue_measure_itv le_measure//= ?inE. - - by case: covDM => /(_ i) + _; exact: sub_sigma_algebra. - - exact: measurable_itv. + rewrite -lebesgue_measure_itv le_measure//= ?inE//. + - by case: covDM => /(_ i) + _; rewrite -RGenOpenSets.measurableE; + exact: sub_sigma_algebra. - exact: sub_Rhull. split => //. apply: bigcup_open => n _. @@ -1026,7 +1025,7 @@ wlog : eps epspos D mD finD / exists ab : R * R, D `<=` `[ab.1, ab.2]%classic. move=> z ; rewrite setDE setCI setCK => -[?|?]; by apply/propext; split => [[]|[[]]]. have mV : measurable V. - by apply: closed_measurable; apply: compact_closed => //; exact: Rhausdorff. + by apply: closed_measurable; apply: compact_closed => //; exact: Rhausdorff. rewrite [eps]splitr EFinD (measureU mu) // ?lteD //. - by apply: measurableD => //; exact: measurableI. - exact: measurableD. @@ -1046,10 +1045,10 @@ exists (`[a, b] `&` ~` U); split. rewrite [_ `&` ~` _ ](iffRL (disjoints_subset _ _)) ?setCK // set0U. move: mDeps; rewrite /D' ?setDE setCI setIUr setCK [U `&` D]setIC. move => /(le_lt_trans _); apply; apply: le_measure; last by move => ?; right. - by rewrite inE; apply: measurableI => //; exact: open_measurable. + rewrite inE; apply: measurableI => //; last by apply: open_measurable. rewrite inE; apply: measurableU. - by apply: measurableI; [exact: open_measurable|exact: measurableC]. - by apply: measurableI => //; exact: open_measurable. + by apply: measurableI; [exact: open_measurable|exact: measurableC]. +apply: measurableI => //; exact: sub_sigma_algebra. Qed. Let lebesgue_regularity_innerE_bounded (A : set R) : measurable A -> @@ -1157,15 +1156,17 @@ have EBr2 n : E n -> closure (B n) `<=` (ball (0:R) (r%:num + 2))%R. have := is_ball_closureP (ABV.1 n) Bnx. by move=> /le_trans; apply; rewrite VB1//; exact: DV. have measurable_closure (C : set R) : is_ball C -> measurable (closure C). - by move=> ballC; rewrite is_ball_closure//; exact: measurable_closed_ball. + by move=> ballC; rewrite is_ball_closure//; + apply: measurable_closed_ball. move: ABV => [is_ballB ABV]. have {}EBr2 : \esum_(i in E) mu (closure (B i)) <= mu (ball (0:R) (r%:num + 2))%R. rewrite -(set_mem_set E) -nneseries_esum// -measure_bigcup//. by move=> *; exact: measurable_closure. by apply: sub_trivIset tDB => ? []. - apply/le_measure; rewrite ?inE; [|exact: measurable_ball|exact: bigcup_sub]. - by apply: bigcup_measurable => *; exact: measurable_closure. + apply/le_measure; rewrite ?inE; + [|exact: measurable_ball|exact: bigcup_sub]. + apply: bigcup_measurable => *; apply: measurable_closure=>//. have finite_set_F i : finite_set (F i). apply: contrapT. pose M := (truncn ((r%:num + 2) *+ 2 / (1 / (2 ^ i.+1)%:R))).+1. @@ -1393,14 +1394,14 @@ Section vitali_theorem_corollary. Context {R : realType} (A : set R) (B : nat -> set R). Let vitali_cover_mclosure (F : set nat) k : - vitali_cover A B F -> (R.-ocitv.-measurable).-sigma.-measurable (closure (B k)). + vitali_cover A B F -> R.-open.-measurable (closure (B k)). Proof. case => + _ => /(_ k)/ballE ->. by rewrite closure_ballE; exact: measurable_closed_ball. Qed. Let vitali_cover_measurable (F : set nat) k : - vitali_cover A B F -> (R.-ocitv.-measurable).-sigma.-measurable (B k). + vitali_cover A B F -> R.-open.-measurable (B k). Proof. by case => + _ => /(_ k)/ballE ->; exact: measurable_ball. Qed. Let vitali_cover_ballE (F : set nat) n : diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index ef6c2c0e7..c5229505c 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint interval. From mathcomp Require Import archimedean. @@ -13,7 +13,7 @@ From mathcomp Require Import realfun. (* # Lebesgue Stieltjes Measure *) (* *) (* This file contains a formalization of the Lebesgue-Stieltjes measure using *) -(* the Measure Extension theorem from measure.v. *) +(* the Measure Extension theorem from `measure_theory`. *) (* *) (* References: *) (* - Achim Klenke. Probability Theory 2nd edition. 2014 *) @@ -26,24 +26,56 @@ From mathcomp Require Import realfun. (* functions (with R : numFieldType) *) (* The HB class is Cumulative. *) (* instance: idfun *) +(* cumulativeBounded R l r == type of cumulative functions f such that *) +(* f @ -oo --> l and f @ +oo --> r *) +(* The HB class is CumulativeBounded. *) +(* ``` *) +(* *) +(* The modules RGenOInfty, RGenInftyO, RGenCInfty, RGenOpens, ROpenSets *) +(* provide proofs of equivalence between the sigma-algebra generated by *) +(* open-closed intervals and the sigma-algebras generated by open rays, *) +(* closed rays, open intervals, and open sets. *) +(* *) +(* We distinguish in particular the sigma-algebras generated by ocitv and *) +(* and open sets for which we introduce the following definitions/notations: *) +(* ``` *) (* ocitv_type R == alias for R : realType *) (* ocitv == set of open-closed intervals ]x, y] where *) (* x and y are real numbers *) (* R.-ocitv == display for ocitv_type R *) (* R.-ocitv.-measurable == semiring of sets of open-closed intervals *) +(* open_type R == alias for R : realType *) +(* R.-open := sigma_display (@open R) *) +(* R.-open.-measurable == sigma-algebra generated by open sets *) +(* ``` *) +(* The modules `MeasurableRocitv` and `MeasurableRopen` contains resp. the *) +(* sigma-algebras generated from ocitv and open sets. They contain similar *) +(* definitions: *) +(* ``` *) +(* measurableTypeR R == measurableType generated by *) +(* R.-ocitv or R.-open *) +(* @lebesgue_display R == (measure_)display for the sigma-algebra *) +(* generated by R.-ocitv or R.-open *) +(* @measurableR R == measurable sets generated by *) +(* R.-ocitv or R.-open *) +(* ``` *) +(* The module `MeasurableR` contains the default sigma-algebra, which is *) +(* `MeasurableRopen`. The latter contains in addition: *) +(* ``` *) +(* ocitv_measure mu == measure over the sigma-algebra *) +(* generated by open sets built out of mu, *) +(* the same measure over the sigma-algebra *) +(* generated by ocitv *) +(* ``` *) +(* The last part of the file contains the construction of the Lebesgue- *) +(* Stieltjes measure: *) +(* ``` *) (* wlength f A := f b - f a with the hull of the set of real *) (* numbers A being delimited by a and b *) -(* @measurableTypeR R == measurableType generated by R.-ocitv *) -(* @lebesgue_display R == (measure_)display for the sigma-algebra *) -(* generated by R.-ocitv *) -(* @measurableR R == measurable sets generated by R.-ocitv *) (* lebesgue_stieltjes_measure f == Lebesgue-Stieltjes measure for f *) (* f is a cumulative function. *) (* completed_lebesgue_stieltjes_measure f == the completed Lebesgue-Stieltjes *) (* measure *) -(* cumulative_bounded R l r == type of cumulative functions f such that *) -(* f @ -oo --> l and f @ +oo --> r *) -(* The HB class is CumulativeBounded. *) (* ``` *) (* *) (******************************************************************************) @@ -61,8 +93,10 @@ Local Open Scope ring_scope. Reserved Notation "R .-ocitv" (at level 1, format "R .-ocitv"). Reserved Notation "R .-ocitv.-measurable" (at level 2, format "R .-ocitv.-measurable"). +Reserved Notation "R .-open" (at level 1, format "R .-open"). +Reserved Notation "R .-open.-measurable" + (at level 2, format "R .-open.-measurable"). -(* TODO: move? *) Notation right_continuous f := (forall x, f%function @ at_right x --> f%function x). @@ -108,7 +142,17 @@ Proof. by apply/right_continuousW => x; exact: cvg_id. Qed. HB.instance Definition _ := isCumulative.Build R _ R idfun id_nd id_rc. End id_is_cumulative. -(* /TODO: move? *) + +HB.mixin Record isCumulativeBounded (R : numFieldType) (l r : R) (f : R -> R) := { + cumulativeNy : f @ -oo --> l ; + cumulativey : f @ +oo --> r }. + +#[short(type=cumulativeBounded)] +HB.structure Definition CumulativeBounded (R : realFieldType) (l r : R) := + { f of isCumulativeBounded R l r f & Cumulative R f}. + +Arguments cumulativeNy {R l r} s. +Arguments cumulativey {R l r} s. Section itv_semiRingOfSets. Variable R : realType. @@ -180,7 +224,355 @@ Notation "R .-ocitv" := (ocitv_display R) : measure_display_scope. Notation "R .-ocitv.-measurable" := (measurable : set_system (ocitv_type R)) : classical_set_scope. -Local Open Scope measure_display_scope. +Module MeasurableRocitv. +Section measurableRocitv. +Context {R : realType}. + +Definition measurableTypeR := g_sigma_algebraType (@ocitv R). + +Definition lebesgue_display : measure_display := (@ocitv R).-sigma. + +Definition measurableR : set_system R := (@ocitv R).-sigma.-measurable. + +HB.instance Definition _ : Measurable lebesgue_display measurableTypeR := + Measurable.on measurableTypeR. +(* Presumably it is safe to use NFI here because morally R is unique + and nothing else can be used here *) +#[non_forgetful_inheritance] +HB.instance Definition _ := Measurable.copy R measurableTypeR. + +Lemma measurable_set1 (r : R) : measurable [set r]. +Proof. +rewrite set1_bigcap_oc; apply: bigcap_measurable => // k _. +by apply: sub_sigma_algebra; exact/is_ocitv. +Qed. +#[local] Hint Resolve measurable_set1 : core. + +Lemma measurable_itv (i : interval R) : measurable [set` i]. +Proof. +have moc (a b : R) : measurable `]a, b]. + by apply: sub_sigma_algebra; apply: is_ocitv. +have mopoo (x : R) : measurable `]x, +oo[. + by rewrite itv_bndy_bigcup_BRight; exact: bigcup_measurable. +have mnooc (x : R) : measurable `]-oo, x]. + by rewrite -setCitvr; exact/measurableC. +have ooE (a b : R) : `]a, b[%classic = `]a, b] `\ b. + by rewrite setDitv1r. +have moo (a b : R) : measurable `]a, b[ by rewrite ooE; exact: measurableD. +have mcc (a b : R) : measurable `[a, b]. + case: (boolP (a <= b)) => ab; last by rewrite set_itv_ge. + by rewrite -setU_1itvob//; apply/measurableU. +have mco (a b : R) : measurable `[a, b[. + case: (boolP (a < b)) => ab; last by rewrite set_itv_ge. + by rewrite -setU_1itvob//; apply/measurableU. +have oooE (b : R) : `]-oo, b[%classic = `]-oo, b] `\ b. + by rewrite setDitv1r. +case: i => [[[] a|[]] [[] b|[]]] => //; do ?by rewrite set_itv_ge. +- by rewrite -setU_1itvob//; exact/measurableU. +- by rewrite oooE; exact/measurableD. +- by rewrite set_itvNyy. +Qed. + +End measurableRocitv. +Arguments measurableTypeR : clear implicits. +#[global] +Hint Extern 0 (measurable (_ @^-1` [set _])) => + solve [apply: measurable_funPTI; exact: measurable_set1] : core. +#[global] +Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1] : core. +#[global] +Hint Extern 0 (measurable [set` _] ) => exact: measurable_itv : core. +End MeasurableRocitv. + +Module RGenOInfty. +Section rgenoinfty. +Context (R : realType). +Implicit Types x y z : R. + +Definition G := [set A | exists x, A = `]x, +oo[%classic]. + +Lemma measurable_itv_bnd_infty b x : + G.-sigma.-measurable [set` Interval (BSide b x) +oo%O]. +Proof. +case: b; last by apply: sub_sigma_algebra; eexists; reflexivity. +rewrite itvcyEbigcap; apply: bigcapT_measurable => k. +by apply: sub_sigma_algebra; eexists; reflexivity. +Qed. + +Lemma measurable_itv_bounded a b x : a != +oo%O -> + G.-sigma.-measurable [set` Interval a (BSide b x)]. +Proof. +case: a => [a r _|[_|//]]. + by rewrite set_itv_splitD; apply: measurableD => //; + exact: measurable_itv_bnd_infty. +by rewrite -setCitvr; apply: measurableC; exact: measurable_itv_bnd_infty. +Qed. + +Lemma measurableE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable. +Proof. +rewrite eqEsubset; split => A. + apply: smallest_sub; first exact: smallest_sigma_algebra. + by move=> I [x _ <-]; exact: measurable_itv_bounded. +by apply: smallest_sub; [exact: smallest_sigma_algebra|move=> A' /= [x ->]]. +Qed. + +End rgenoinfty. +End RGenOInfty. + +Module RGenInftyO. +Section rgeninftyo. +Context (R : realType). +Implicit Types x y z : R. + +Definition G := [set A | exists x, A = `]-oo, x[%classic]. + +Lemma measurable_itv_bnd_infty b x : + G.-sigma.-measurable [set` Interval -oo%O (BSide b x)]. +Proof. +case: b; first by apply sub_sigma_algebra; eexists; reflexivity. +rewrite -setCitvr itvoyEbigcup; apply/measurableC/bigcupT_measurable => n. +rewrite -setCitvl; apply: measurableC. +by apply: sub_sigma_algebra; eexists; reflexivity. +Qed. + +Lemma measurable_itv_bounded a b x : a != -oo%O -> + G.-sigma.-measurable [set` Interval (BSide b x) a]. +Proof. +case: a => [a r _|[//|_]]. + by rewrite set_itv_splitD; apply/measurableD => //; + rewrite -setCitvl; apply: measurableC; exact: measurable_itv_bnd_infty. +by rewrite -setCitvl; apply: measurableC; exact: measurable_itv_bnd_infty. +Qed. + +Lemma measurableE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable. +Proof. +rewrite eqEsubset; split => A. + apply: smallest_sub; first exact: smallest_sigma_algebra. + by move=> I [x _ <-]; exact: measurable_itv_bounded. +by apply: smallest_sub; [exact: smallest_sigma_algebra|move=> A' /= [x ->]]. +Qed. + +End rgeninftyo. +End RGenInftyO. + +Module RGenCInfty. +Section rgencinfty. +Context (R : realType). +Implicit Types x y z : R. + +Definition G : set_system R := [set A | exists x, A = `[x, +oo[%classic]. + +Lemma measurable_itv_bnd_infty b x : + G.-sigma.-measurable [set` Interval (BSide b x) +oo%O]. +Proof. +case: b; first by apply: sub_sigma_algebra; exists x; rewrite set_itvcy. +rewrite itvoyEbigcup; apply: bigcupT_measurable => k. +by apply: sub_sigma_algebra; eexists; reflexivity. +Qed. + +Lemma measurable_itv_bounded a b y : a != +oo%O -> + G.-sigma.-measurable [set` Interval a (BSide b y)]. +Proof. +case: a => [a r _|[_|//]]. + rewrite set_itv_splitD. + by apply: measurableD; exact: measurable_itv_bnd_infty. +by rewrite -setCitvr; apply: measurableC; exact: measurable_itv_bnd_infty. +Qed. + +Lemma measurableE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable. +Proof. +rewrite eqEsubset; split => A. + apply: smallest_sub; first exact: smallest_sigma_algebra. + by move=> I [x _ <-]; exact: measurable_itv_bounded. +by apply: smallest_sub; [exact: smallest_sigma_algebra|move=> A' /= [x ->]]. +Qed. + +End rgencinfty. +End RGenCInfty. + +Module RGenOpens. +Section rgenopens. +Context (R : realType). +Implicit Types x y z : R. + +Definition G := [set A | exists x y, A = `]x, y[%classic]. + +Local Lemma measurable_itvoo x y : G.-sigma.-measurable `]x, y[%classic. +Proof. by apply sub_sigma_algebra; eexists; eexists; reflexivity. Qed. + +Local Lemma measurable_itv_o_infty x : G.-sigma.-measurable `]x, +oo[%classic. +Proof. +rewrite itvbndyEbigcup; apply: bigcupT_measurable => i. +exact: measurable_itvoo. +Qed. + +Lemma measurable_itv_bnd_infty b x : + G.-sigma.-measurable [set` Interval (BSide b x) +oo%O]. +Proof. +case: b; last exact: measurable_itv_o_infty. +rewrite itvcyEbigcap; apply: bigcapT_measurable => k. +exact: measurable_itv_o_infty. +Qed. + +Lemma measurable_itv_infty_bnd b x : + G.-sigma.-measurable [set` Interval -oo%O (BSide b x)]. +Proof. +by rewrite -setCitvr; apply: measurableC; exact: measurable_itv_bnd_infty. +Qed. + +Lemma measurable_itv_bounded a x b y : + G.-sigma.-measurable [set` Interval (BSide a x) (BSide b y)]. +Proof. +move: a b => [] []; rewrite -[X in measurable X]setCK setCitv; + apply: measurableC; apply: measurableU; try solve[ + exact: measurable_itv_infty_bnd|exact: measurable_itv_bnd_infty]. +Qed. + +Lemma measurableE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable. +Proof. +rewrite eqEsubset; split => A. + apply: smallest_sub; first exact: smallest_sigma_algebra. + by move=> I [x _ <-]; exact: measurable_itv_bounded. +by apply: smallest_sub; [exact: smallest_sigma_algebra|move=> A' /= [x [y ->]]]. +Qed. + +End rgenopens. +End RGenOpens. + +Module RGenOpenSets. +Section rgenopensets. +Context (R : realType). +Implicit Types a b : R. +Import MeasurableRocitv. + +Lemma measurableE : (@ocitv R).-sigma.-measurable = open.-sigma.-measurable. +Proof. +rewrite eqEsubset; split; [rewrite RGenOpens.measurableE|]; + apply: sigma_algebra_subl=> U. +- rewrite /RGenOpens.G/= => -[a [b ->]]. + exact: sub_sigma_algebra. +- move=> oU. + rewrite (open_disjoint_itv_bigcup oU). + apply: sigma_algebra_bigcup => k. + have /is_intervalP -> := @open_disjoint_itv_is_interval _ U oU k. + exact: measurable_itv. +Qed. + +End rgenopensets. +End RGenOpenSets. + +Section open. +Context {R : realType}. + +Definition open_type : Type := R. + +HB.instance Definition _ := Pointed.on open_type. + +Let measurable : set_system R := @measurable _ (g_sigma_algebraType (@open R)). + +Let measurable0 : measurable set0. Proof. exact: measurable0. Qed. + +Let measurableC A : measurable A -> measurable (~` A). +Proof. by move=> /measurableC. Qed. + +Let measurable_bigcup (F : (set R)^nat) : (forall i, measurable (F i)) -> + measurable (\bigcup_i (F i)). +Proof. move=> mF; exact: bigcupT_measurable. Qed. + +HB.instance Definition _ := + @isMeasurable.Build (sigma_display (@open R)) + open_type measurable measurable0 measurableC measurable_bigcup. + +End open. + +Notation "R .-open" := (sigma_display (@open R)) : measure_display_scope. +Notation "R .-open.-measurable" := (measurable : set_system (@open_type R)) : + classical_set_scope. + +Module MeasurableRopen. +Section measurableRopen. +Context {R : realType}. + +Definition measurableTypeR := g_sigma_algebraType (@open R). + +Definition lebesgue_display : measure_display := R.-open. + +Definition measurableR : set_system R := R.-open.-measurable. + +HB.instance Definition _ : Measurable lebesgue_display measurableTypeR := + Measurable.on measurableTypeR. +(* Presumably it is safe to use NFI here because morally R is unique + and nothing else can be used here *) +#[non_forgetful_inheritance] +HB.instance Definition _ := Measurable.copy R measurableTypeR. + +Lemma measurable_set1 (r : R) : measurable [set r]. +Proof. +rewrite set1_bigcap_oo; apply: bigcap_measurable => // k _. +exact: sub_sigma_algebra. +Qed. +#[local] Hint Resolve measurable_set1 : core. + +Lemma measurable_itv (i : interval R) : measurable [set` i]. +Proof. +have := MeasurableRocitv.measurable_itv i. +rewrite /MeasurableRocitv.lebesgue_display. +by rewrite RGenOpenSets.measurableE. +Qed. + +End measurableRopen. +Arguments measurableTypeR : clear implicits. +#[global] +Hint Extern 0 (measurable (_ @^-1` [set _])) => + solve [apply: measurable_funPTI; exact: measurable_set1] : core. +#[global] +Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1] : core. +#[global] +Hint Extern 0 (measurable [set` _] ) => exact: measurable_itv : core. + +Lemma measurable_funP1 {d} {aT : measurableType d} {rT : realType} + (f : {mfun aT >-> rT}) D (y : rT) : + measurable D -> measurable (D `&` f @^-1` [set y]). +Proof. by move=> /(measurable_funP f); exact. Qed. +#[deprecated(since="mathcomp-analysis 1.13.0", use=measurable_funP1)] +Notation measurable_sfun_inP := measurable_funP1 (only parsing). +#[global] Hint Extern 0 (measurable (_ `&` _ @^-1` [set _])) => + solve [apply: measurable_funP1; assumption] : core. + +Section ocitv_measure. +Context {R : realType} (mu : measure (measurableTypeR R) R). + +Definition ocitv_measure : set (MeasurableRocitv.measurableTypeR R) -> \bar R := mu. + +Let measure0 : ocitv_measure set0 = 0. Proof. by rewrite /ocitv_measure measure0. Qed. + +Let measure_ge0 x : (0 <= ocitv_measure x)%E. +Proof. by rewrite /ocitv_measure measure_ge0. Qed. + +Let measure_semi_sigma_additive : semi_sigma_additive ocitv_measure. +Proof. +move=> F H1 H2 H3; apply: measure_semi_sigma_additive => //. +- move=> i; apply: H1; split => //=; first exact: sigma_algebra_measurable. + by rewrite -RGenOpenSets.measurableE; exact: sub_sigma_algebra. +- by rewrite -RGenOpenSets.measurableE. +Qed. + +HB.instance Definition _ := isMeasure.Build _ _ _ ocitv_measure + measure0 measure_ge0 measure_semi_sigma_additive. + +Lemma ocitv_measure_ext A : ocitv_measure A = mu A. Proof. by []. Qed. + +End ocitv_measure. + +End MeasurableRopen. + +Module MeasurableR. +Export MeasurableRopen. +End MeasurableR. + +Import MeasurableR. + +(* NB: Lebesgue-Stieltjes measure actually starts here... *) Section wlength. Context {R : realType}. @@ -497,14 +889,49 @@ move=> k; split => //; rewrite wlength_itv /= -EFinB. by case: ifP; rewrite ltey. Qed. -Definition lebesgue_stieltjes_measure (f : cumulative R R) := +Definition ocitv_lebesgue_stieltjes_measure (f : cumulative R R) := measure_extension (wlength f). +HB.instance Definition _ (f : cumulative R R) := Measure.on (ocitv_lebesgue_stieltjes_measure f). + +Let ocitv_sigmaT_finite_lebesgue_stieltjes_measure (f : cumulative R R) : + sigma_finite setT (ocitv_lebesgue_stieltjes_measure f). +Proof. +have := measure_extension_sigma_finite (wlength_sigma_finite f). +by move=> [X bX fX]; exists X. +Qed. + HB.instance Definition _ (f : cumulative R R) := - Measure.on (lebesgue_stieltjes_measure f). + @Measure_isSigmaFinite.Build _ _ _ (ocitv_lebesgue_stieltjes_measure f) + (ocitv_sigmaT_finite_lebesgue_stieltjes_measure f). + +Definition lebesgue_stieltjes_measure (f : cumulative R R) : + set (g_sigma_algebraType (@open R)) -> \bar R := + measure_extension (wlength f). + +Let lsm0 (f : cumulative R R) : lebesgue_stieltjes_measure f set0 = 0. +Proof. by[]. Qed. + +Let lsm_ge0 (f : cumulative R R) x : (0 <= lebesgue_stieltjes_measure f x)%E. +Proof. by[]. Qed. + +Let lsm_semi_sigma_additive (f : cumulative R R) : + semi_sigma_additive (lebesgue_stieltjes_measure f). +Proof. +by move=> /= F mF tF mbF; apply: measure_semi_sigma_additive=>//; +rewrite RGenOpenSets.measurableE/=; [move=> i; apply: (mF i)|apply: mbF]; +split=>//; exact: sigma_algebra_measurable. +Qed. + +HB.instance Definition _ (f : cumulative R R) := + isMeasure.Build _ _ _ (lebesgue_stieltjes_measure f) + (lsm0 f) (lsm_ge0 f) (@lsm_semi_sigma_additive f). Let sigmaT_finite_lebesgue_stieltjes_measure (f : cumulative R R) : sigma_finite setT (lebesgue_stieltjes_measure f). -Proof. exact/measure_extension_sigma_finite/wlength_sigma_finite. Qed. +Proof. +have := measure_extension_sigma_finite (wlength_sigma_finite f). +by move=> [X bX fX]; exists X=>// i; rewrite -RGenOpenSets.measurableE. +Qed. HB.instance Definition _ (f : cumulative R R) := @Measure_isSigmaFinite.Build _ _ _ (lebesgue_stieltjes_measure f) @@ -513,35 +940,36 @@ HB.instance Definition _ (f : cumulative R R) := End wlength_extension. Arguments lebesgue_stieltjes_measure {R}. -Definition measurableTypeR (R : realType) := - g_sigma_algebraType (@ocitv R). - -Section lebesgue_stieltjes_measure. +Section lebesgue_stieltjes_measure_unique. Context {R : realType}. -Definition lebesgue_display : measure_display := - (@ocitv R).-sigma. -Definition measurableR : set (set R) := - (@ocitv R).-sigma.-measurable. - -HB.instance Definition _ : Measurable lebesgue_display (measurableTypeR R) := - Measurable.on (measurableTypeR R). -(* Presumably it is safe to use NFI here because morally R is unique - and nothing else can be used here *) -#[non_forgetful_inheritance] -HB.instance Definition _ := Measurable.copy R (measurableTypeR R). - -Lemma lebesgue_stieltjes_measure_unique - (f : cumulative R R) (mu : {measure set R -> \bar R}) : +Lemma ocitv_lebesgue_stieltjes_measure_unique + (f : cumulative R R) + (mu : {measure set (MeasurableRocitv.measurableTypeR R) -> \bar R}) : (forall X, ocitv X -> lebesgue_stieltjes_measure f X = mu X) -> forall A : set R, measurable A -> lebesgue_stieltjes_measure f A = mu A. Proof. -move=> muE A mA; apply: measure_extension_unique => //=. +move=> muE A mA. +apply: measure_extension_unique => //=. exact: wlength_sigma_finite. by move=> X mX; rewrite -muE// -measurable_mu_extE. +by rewrite RGenOpenSets.measurableE. +Qed. + +Lemma open_lebesgue_stieltjes_measure_unique + (f : cumulative R R) + (mu : {measure set (MeasurableRopen.measurableTypeR R) -> \bar R}) : + (forall X, ocitv X -> lebesgue_stieltjes_measure f X = mu X) -> + forall A : set R, measurable A -> lebesgue_stieltjes_measure f A = mu A. +Proof. +move=> muE A mA; rewrite -ocitv_measure_ext. +apply: measure_extension_unique => //=. +- exact: wlength_sigma_finite. +- by move=> X mX; rewrite -muE// -measurable_mu_extE. +- by rewrite RGenOpenSets.measurableE. Qed. -End lebesgue_stieltjes_measure. +End lebesgue_stieltjes_measure_unique. Section completed_lebesgue_stieltjes_measure. Context {R : realType}. @@ -564,74 +992,6 @@ HB.instance Definition _ (f : cumulative R R) := End completed_lebesgue_stieltjes_measure. Arguments completed_lebesgue_stieltjes_measure {R}. -Section salgebra_R_ssets. -Variable R : realType. - -Lemma measurable_set1 (r : R) : measurable [set r]. -Proof. -rewrite set1_bigcap_oc; apply: bigcap_measurable => // k _. -by apply: sub_sigma_algebra; exact/is_ocitv. -Qed. -#[local] Hint Resolve measurable_set1 : core. - -Lemma measurable_itv (i : interval R) : measurable [set` i]. -Proof. -have moc (a b : R) : measurable `]a, b]. - by apply: sub_sigma_algebra; apply: is_ocitv. -have mopoo (x : R) : measurable `]x, +oo[. - by rewrite itv_bndy_bigcup_BRight; exact: bigcup_measurable. -have mnooc (x : R) : measurable `]-oo, x]. - by rewrite -setCitvr; exact/measurableC. -have ooE (a b : R) : `]a, b[%classic = `]a, b] `\ b. - by rewrite setDitv1r. -have moo (a b : R) : measurable `]a, b[. - by rewrite ooE; exact: measurableD. -have mcc (a b : R) : measurable `[a, b]. - case: (boolP (a <= b)) => ab; last by rewrite set_itv_ge. - by rewrite -setU_1itvob//; apply/measurableU. -have mco (a b : R) : measurable `[a, b[. - case: (boolP (a < b)) => ab; last by rewrite set_itv_ge. - by rewrite -setU_1itvob//; apply/measurableU. -have oooE (b : R) : `]-oo, b[%classic = `]-oo, b] `\ b. - by rewrite setDitv1r. -case: i => [[[] a|[]] [[] b|[]]] => //; do ?by rewrite set_itv_ge. -- by rewrite -setU_1itvob//; exact/measurableU. -- by rewrite oooE; exact/measurableD. -- by rewrite set_itvNyy. -Qed. -#[local] Hint Resolve measurable_itv : core. - -End salgebra_R_ssets. -#[global] -Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1] : core. -#[global] -Hint Extern 0 (measurable [set` _] ) => exact: measurable_itv : core. - -#[global] Hint Extern 0 (measurable (_ @^-1` [set _])) => - solve [apply: measurable_funPTI; exact: measurable_set1] : core. - -Lemma measurable_funP1 {d} {aT : measurableType d} {rT : realType} - (f : {mfun aT >-> rT}) D (y : rT) : - measurable D -> measurable (D `&` f @^-1` [set y]). -Proof. move=> mD; exact: measurable_funP. Qed. - -#[deprecated(since="mathcomp-analysis 1.13.0", note="renamed to `measurable_funP1`")] -Notation measurable_sfun_inP := measurable_funP1 (only parsing). - -#[global] Hint Extern 0 (measurable (_ `&` _ @^-1` [set _])) => - solve [apply: measurable_funP1; assumption] : core. - -HB.mixin Record isCumulativeBounded (R : numFieldType) (l r : R) (f : R -> R) := { - cumulativeNy : f @ -oo --> l ; - cumulativey : f @ +oo --> r }. - -#[short(type=cumulativeBounded)] -HB.structure Definition CumulativeBounded (R : realFieldType) (l r : R) := - { f of isCumulativeBounded R l r f & Cumulative R f}. - -Arguments cumulativeNy {R l r} s. -Arguments cumulativey {R l r} s. - Section probability_measure_of_lebesgue_stieltjes_mesure. Context {R : realType} (f : cumulativeBounded (0:R) (1:R)). Local Open Scope measure_display_scope. @@ -654,7 +1014,7 @@ have : (lsf \o I) n @[n --> \oo] --> 1%E. exact: cumulativeNy. by apply: (cvg_comp _ _ (@cvgr_idn R)); rewrite ninfty. have : (lsf \o I) n @[n --> \oo] --> lsf (\bigcup_n I n). - apply: nondecreasing_cvg_mu; rewrite /I//; first exact: bigcup_measurable. + apply: nondecreasing_cvg_measure; rewrite /I//; first exact: bigcup_measurable. by move=> *; apply/subsetPset/subset_itv; rewrite leBSide/= ?lerN2 ler_nat. exact: cvg_unique. Unshelve. all: end_near. Qed. diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index 1fdbbb44f..dd0c4d496 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -28,11 +28,6 @@ From mathcomp Require Import lebesgue_stieltjes_measure. (* measurables G of a sigma-algebra over R *) (* ``` *) (* *) -(* The modules RGenOInfty, RGenInftyO, RGenCInfty, RGenOpens provide proofs *) -(* of equivalence between the sigma-algebra generated by open-closed *) -(* intervals and the sigma-algebras generated by open rays, closed rays, and *) -(* open intervals. *) -(* *) (* The module NGenCInfty provides a proof of equivalence between the *) (* sigma-algebra for natural numbers and the sigma-algebra generated by *) (* closed rays. *) @@ -189,7 +184,7 @@ Qed. End puncture_ereal_itv. Section salgebra_R_ssets. -Variable R : realType. +Context {R : realType}. HB.instance Definition _ := (ereal_isMeasurable (R.-ocitv.-measurable)). (* NB: Until we dropped support for Coq 8.12, we were using @@ -205,19 +200,22 @@ This was producing a warning but the alternative was failing with Coq 8.12 with # Please report at http://coq.inria.fr/bugs/. *) +Import MeasurableR. + Lemma measurable_image_EFin (A : set R) : - measurableR A -> measurable (EFin @` A). + measurable A -> measurable (EFin @` A). Proof. -by move=> mA; exists A => //; exists set0; [constructor|rewrite setU0]. +move=> mA; exists A; first by rewrite RGenOpenSets.measurableE. +by exists set0; [constructor|rewrite setU0]. Qed. Lemma emeasurable_set1 (x : \bar R) : measurable [set x]. Proof. case: x => [r| |]. -- by rewrite -image_set1; apply: measurable_image_EFin; apply: measurable_set1. -- exists set0 => //; [exists [set +oo%E]; [by constructor|]]. +- by rewrite -image_set1; apply: measurable_image_EFin. +- exists set0 => //; [exists [set +oo%E]; first by constructor]. by rewrite image_set0 set0U. -- exists set0 => //; [exists [set -oo%E]; [by constructor|]]. +- exists set0 => //; [exists [set -oo%E]; first by constructor]. by rewrite image_set0 set0U. Qed. #[local] Hint Resolve emeasurable_set1 : core. @@ -226,7 +224,7 @@ Let emeasurable_itv_bndy b (y : \bar R) : measurable [set` Interval (BSide b y) +oo%O]. Proof. move: y => [y| |]. -- exists [set` Interval (BSide b y) +oo%O]; first exact: measurable_itv. +- exists [set` Interval (BSide b y) +oo%O]; first by []. by exists [set +oo%E]; [constructor|rewrite -punct_eitv_bndy]. - by case: b; rewrite ?itv_oyy ?itv_cyy. - case: b; first by rewrite itv_cNyy. @@ -251,24 +249,24 @@ Lemma measurable_image_fine (X : set \bar R) : measurable X -> Proof. case => Y mY [X' [ | <-{X} | <-{X} | <-{X} ]]. - rewrite setU0 => <-{X}. - rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split. + rewrite [X in measurable X](_ : _ = Y) -?RGenOpenSets.measurableE// predeqE => r; split. by move=> [x [[x' Yx' <-{x}/= _ <-//]]]. by move=> Yr; exists r%:E; split => [|[]//]; exists r. -- rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split. +- rewrite [X in measurable X](_ : _ = Y) -?RGenOpenSets.measurableE// predeqE => r; split. move=> [x [[[x' Yx' <- _ <-//]|]]]. by move=> <-; rewrite not_orP => -[]/(_ erefl). by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r. -- rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split. +- rewrite [X in measurable X](_ : _ = Y) -?RGenOpenSets.measurableE// predeqE => r; split. move=> [x [[[x' Yx' <-{x} _ <-//]|]]]. by move=> ->; rewrite not_orP => -[_]/(_ erefl). by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r. -- rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split. +- rewrite [X in measurable X](_ : _ = Y) -?RGenOpenSets.measurableE// predeqE => r; split. by rewrite setDUl setDv setU0 => -[_ [[x' Yx' <-]] _ <-]. by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r. Qed. Lemma measurable_ball (x : R) e : measurable (ball x e). -Proof. by rewrite ball_itv; exact: measurable_itv. Qed. +Proof. by rewrite ball_itv -?RGenOpenSets.measurableE//. Qed. Lemma measurable_closed_ball (x : R) r : measurable (closed_ball x r). Proof. @@ -278,8 +276,8 @@ Qed. End salgebra_R_ssets. #[global] Hint Extern 0 (measurable [set _]) => solve [apply: emeasurable_set1] : core. -#[global] -Hint Extern 0 (measurable [set` _] ) => exact: measurable_itv : core. + +Import MeasurableR. Lemma fine_measurable (R : realType) (D : set (\bar R)) : measurable D -> measurable_fun D fine. @@ -342,160 +340,6 @@ Qed. End measurable_fun_measurable. -Module RGenOInfty. -Section rgenoinfty. -Variable R : realType. -Implicit Types x y z : R. - -Definition G := [set A | exists x, A = `]x, +oo[%classic]. - -Lemma measurable_itv_bnd_infty b x : - G.-sigma.-measurable [set` Interval (BSide b x) +oo%O]. -Proof. -case: b; last by apply: sub_sigma_algebra; eexists; reflexivity. -rewrite itvcyEbigcap; apply: bigcapT_measurable => k. -by apply: sub_sigma_algebra; eexists; reflexivity. -Qed. - -Lemma measurable_itv_bounded a b x : a != +oo%O -> - G.-sigma.-measurable [set` Interval a (BSide b x)]. -Proof. -case: a => [a r _|[_|//]]. - by rewrite set_itv_splitD; apply: measurableD => //; - exact: measurable_itv_bnd_infty. -by rewrite -setCitvr; apply: measurableC; exact: measurable_itv_bnd_infty. -Qed. - -Lemma measurableE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable. -Proof. -rewrite eqEsubset; split => A. - apply: smallest_sub; first exact: smallest_sigma_algebra. - by move=> I [x _ <-]; exact: measurable_itv_bounded. -by apply: smallest_sub; [exact: smallest_sigma_algebra|move=> A' /= [x ->]]. -Qed. - -End rgenoinfty. -End RGenOInfty. - -Module RGenInftyO. -Section rgeninftyo. -Variable R : realType. -Implicit Types x y z : R. - -Definition G := [set A | exists x, A = `]-oo, x[%classic]. - -Lemma measurable_itv_bnd_infty b x : - G.-sigma.-measurable [set` Interval -oo%O (BSide b x)]. -Proof. -case: b; first by apply sub_sigma_algebra; eexists; reflexivity. -rewrite -setCitvr itvoyEbigcup; apply/measurableC/bigcupT_measurable => n. -rewrite -setCitvl; apply: measurableC. -by apply: sub_sigma_algebra; eexists; reflexivity. -Qed. - -Lemma measurable_itv_bounded a b x : a != -oo%O -> - G.-sigma.-measurable [set` Interval (BSide b x) a]. -Proof. -case: a => [a r _|[//|_]]. - by rewrite set_itv_splitD; apply/measurableD => //; - rewrite -setCitvl; apply: measurableC; exact: measurable_itv_bnd_infty. -by rewrite -setCitvl; apply: measurableC; exact: measurable_itv_bnd_infty. -Qed. - -Lemma measurableE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable. -Proof. -rewrite eqEsubset; split => A. - apply: smallest_sub; first exact: smallest_sigma_algebra. - by move=> I [x _ <-]; exact: measurable_itv_bounded. -by apply: smallest_sub; [exact: smallest_sigma_algebra|move=> A' /= [x ->]]. -Qed. - -End rgeninftyo. -End RGenInftyO. - -Module RGenCInfty. -Section rgencinfty. -Variable R : realType. -Implicit Types x y z : R. - -Definition G : set_system R := [set A | exists x, A = `[x, +oo[%classic]. - -Lemma measurable_itv_bnd_infty b x : - G.-sigma.-measurable [set` Interval (BSide b x) +oo%O]. -Proof. -case: b; first by apply: sub_sigma_algebra; exists x; rewrite set_itvcy. -rewrite itvoyEbigcup; apply: bigcupT_measurable => k. -by apply: sub_sigma_algebra; eexists; reflexivity. -Qed. - -Lemma measurable_itv_bounded a b y : a != +oo%O -> - G.-sigma.-measurable [set` Interval a (BSide b y)]. -Proof. -case: a => [a r _|[_|//]]. - rewrite set_itv_splitD. - by apply: measurableD; exact: measurable_itv_bnd_infty. -by rewrite -setCitvr; apply: measurableC; exact: measurable_itv_bnd_infty. -Qed. - -Lemma measurableE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable. -Proof. -rewrite eqEsubset; split => A. - apply: smallest_sub; first exact: smallest_sigma_algebra. - by move=> I [x _ <-]; exact: measurable_itv_bounded. -by apply: smallest_sub; [exact: smallest_sigma_algebra|move=> A' /= [x ->]]. -Qed. - -End rgencinfty. -End RGenCInfty. - -Module RGenOpens. -Section rgenopens. -Variable R : realType. -Implicit Types x y z : R. - -Definition G := [set A | exists x y, A = `]x, y[%classic]. - -Local Lemma measurable_itvoo x y : G.-sigma.-measurable `]x, y[%classic. -Proof. by apply sub_sigma_algebra; eexists; eexists; reflexivity. Qed. - -Local Lemma measurable_itv_o_infty x : G.-sigma.-measurable `]x, +oo[%classic. -Proof. -rewrite itvbndyEbigcup; apply: bigcupT_measurable => i. -exact: measurable_itvoo. -Qed. - -Lemma measurable_itv_bnd_infty b x : - G.-sigma.-measurable [set` Interval (BSide b x) +oo%O]. -Proof. -case: b; last exact: measurable_itv_o_infty. -rewrite itvcyEbigcap; apply: bigcapT_measurable => k. -exact: measurable_itv_o_infty. -Qed. - -Lemma measurable_itv_infty_bnd b x : - G.-sigma.-measurable [set` Interval -oo%O (BSide b x)]. -Proof. -by rewrite -setCitvr; apply: measurableC; exact: measurable_itv_bnd_infty. -Qed. - -Lemma measurable_itv_bounded a x b y : - G.-sigma.-measurable [set` Interval (BSide a x) (BSide b y)]. -Proof. -move: a b => [] []; rewrite -[X in measurable X]setCK setCitv; - apply: measurableC; apply: measurableU; try solve[ - exact: measurable_itv_infty_bnd|exact: measurable_itv_bnd_infty]. -Qed. - -Lemma measurableE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable. -Proof. -rewrite eqEsubset; split => A. - apply: smallest_sub; first exact: smallest_sigma_algebra. - by move=> I [x _ <-]; exact: measurable_itv_bounded. -by apply: smallest_sub; [exact: smallest_sigma_algebra|move=> A' /= [x [y ->]]]. -Qed. - -End rgenopens. -End RGenOpens. Section erealwithrays. Variable R : realType. Implicit Types (x y z : \bar R) (r s : R). @@ -708,7 +552,7 @@ End ErealGenInftyO. Lemma is_interval_measurable (R : realType) (I : set R) : is_interval I -> measurable I. -Proof. by move/is_intervalP => ->; exact: measurable_itv. Qed. +Proof. by move/is_intervalP => ->; rewrite -?RGenOpenSets.measurableE//. Qed. Section coutinuous_measurable. Variable R : realType. @@ -738,8 +582,12 @@ Qed. Lemma subspace_continuous_measurable_fun (D : set R) (f : subspace D -> R) : measurable D -> continuous f -> measurable_fun D f. Proof. -move=> mD /continuousP cf; apply: (measurability _ (RGenOpens.measurableE R)). -move=> _ [_ [a [b ->] <-]]; apply: open_measurable_subspace => //. +move=> mD /continuousP cf. +rewrite /measurable_fun -?RGenOpenSets.measurableE. +apply: (measurability _ (RGenOpens.measurableE R)). +move=> _ [_ [a [b ->] <-]]. +rewrite RGenOpenSets.measurableE. +apply: open_measurable_subspace => //. exact/cf/interval_open. Qed. @@ -778,13 +626,17 @@ Qed. Lemma normr_measurable D : measurable_fun D (@normr _ R). Proof. -move=> mD; apply: (measurability _ (RGenOInfty.measurableE R)) => //. +move=> mD. +rewrite -RGenOpenSets.measurableE. +apply: (measurability _ (RGenOInfty.measurableE R)) => //; last first. + by rewrite RGenOpenSets.measurableE. move=> /= _ [_ [x ->] <-]; apply: measurableI => //. + by rewrite RGenOpenSets.measurableE. have [x0|x0] := leP 0 x; last first. rewrite [X in measurable X](_ : _ = setT)// predeqE => r. by split => // _; rewrite /= in_itv /= andbT (lt_le_trans x0). -rewrite [X in measurable X](_ : _ = `]-oo, (- x)[ `|` `]x, +oo[)%classic; last first. - by apply: measurableU; apply: measurable_itv. +rewrite [X in measurable X](_ : _ = `]-oo, (- x)[ `|` `]x, +oo[); last first. + exact: measurableU. rewrite predeqE => r; split => [|[|]]; rewrite preimage_itv ?in_itv ?andbT/=. - have [r0|r0] := leP 0 r; [rewrite ger0_norm|rewrite ltr0_norm] => // xr; rewrite 2!in_itv/=. @@ -837,13 +689,15 @@ Implicit Types (D : set T) (f g : T -> R). Lemma measurable_funD D f g : measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \+ g). Proof. -move=> mf mg mD; apply: (measurability _ (RGenOInfty.measurableE R)) => //. +move=> mf mg mD. +rewrite -RGenOpenSets.measurableE. +apply: (measurability _ (RGenOInfty.measurableE R)) => //. move=> /= _ [_ [a ->] <-]; rewrite preimage_itvoy. rewrite [X in measurable X](_ : _ = \bigcup_(q : rat) ((D `&` [set x | ratr q < f x]) `&` (D `&` [set x | a - ratr q < g x]))); last first. apply: bigcupT_measurable_rat => q; apply: measurableI. - - by rewrite -preimage_itvoy; apply: mf => //; exact: measurable_itv. - - by rewrite -preimage_itvoy; apply: mg => //; exact: measurable_itv. + - by rewrite -preimage_itvoy; exact: mf. + - by rewrite -preimage_itvoy; exact: mg. rewrite predeqE => x; split => [|[r _] []/= [Dx rfx]] /= => [[Dx]|[_]]. rewrite -ltrBlDr => /rat_in_itvoo[r]; rewrite inE /= => /itvP h. exists r => //; rewrite setIACA setIid; split => //; split => /=. @@ -924,9 +778,11 @@ Lemma measurable_fun_sups D (h : (T -> R)^nat) n : (forall m, measurable_fun D (h m)) -> measurable_fun D (fun x => sups (h ^~ x) n). Proof. -move=> f_ub mf mD; apply: (measurability _ (RGenOInfty.measurableE R)) => //. -move=> _ [_ [x ->] <-]; rewrite sups_preimage // setI_bigcupr. -by apply: bigcup_measurable => k /= nk; apply: mf => //; exact: measurable_itv. +move=> f_ub mf mD. +rewrite -RGenOpenSets.measurableE. +apply: (measurability _ (RGenOInfty.measurableE R)) => //. +move=> _ [_ [x ->] <-]; rewrite sups_preimage// setI_bigcupr. +by apply: bigcup_measurable => k /= nk; exact: mf. Qed. Lemma measurable_fun_infs D (h : (T -> R)^nat) n : @@ -934,9 +790,11 @@ Lemma measurable_fun_infs D (h : (T -> R)^nat) n : (forall n, measurable_fun D (h n)) -> measurable_fun D (fun x => infs (h ^~ x) n). Proof. -move=> lb_f mf mD; apply: (measurability _ (RGenInftyO.measurableE R)) => //. +move=> lb_f mf mD. +rewrite -RGenOpenSets.measurableE. +apply: (measurability _ (RGenInftyO.measurableE R)) => //. move=> _ [_ [x ->] <-]; rewrite infs_preimage // setI_bigcupr. -by apply: bigcup_measurable => k /= nk; apply: mf => //; exact: measurable_itv. +by apply: bigcup_measurable => k /= nk; exact: mf. Qed. Lemma measurable_fun_limn_sup D (h : (T -> R)^nat) : @@ -1024,8 +882,11 @@ Lemma nondecreasing_measurable (D : set R) (f : R -> R) : measurable D -> nondecreasing_fun f -> measurable_fun D f. Proof. move=> mD f_nd. -apply: (measurability (@RGenCInfty.G R)) => [|/= _ [_] [r] -> <-]. - exact: RGenCInfty.measurableE. +rewrite /measurable_fun. +apply: (@measurability). + rewrite -RGenOpenSets.measurableE. + by rewrite RGenCInfty.measurableE. +move => /= _ [_] [r] -> <-. apply: measurableI => //; apply: is_interval_measurable => s t/=. rewrite !in_itv/= !andbT => fs ft u /andP[su ut]. by rewrite in_itv/= andbT (le_trans fs)// f_nd. @@ -1368,7 +1229,7 @@ Lemma EFin_measurable (D : set R) : measurable_fun D EFin. Proof. move=> mD; apply: (measurability _ (ErealGenOInfty.measurableE R)) => //. move=> /= _ [_ [x ->]] <-; apply: measurableI => //. -by rewrite preimage_itvoy EFin_itv; exact: measurable_itv. +by rewrite -RGenOpenSets.measurableE preimage_itvoy EFin_itv. Qed. Lemma abse_measurable (D : set (\bar R)) : measurable_fun D abse. @@ -1379,7 +1240,9 @@ rewrite [X in _ @^-1` X](punct_eitv_bndy _ x) preimage_setU setIUr. apply: measurableU; last first. by rewrite preimage_abse_pinfty; apply: measurableI => //; exact: measurableU. apply: measurableI => //; exists (normr @^-1` `]x, +oo[%classic). - by rewrite -[X in measurable X]setTI; exact: normr_measurable. + rewrite -[X in measurable X]setTI. + rewrite RGenOpenSets.measurableE. + exact: normr_measurable. exists set0; first by constructor. rewrite setU0 predeqE => -[y| |]; split => /= => -[r]; rewrite ?/= /= ?in_itv /= ?andbT => xr//. @@ -1411,7 +1274,9 @@ Lemma measurable_EFinP d (T : measurableType d) (R : realType) (D : set T) Proof. split=> [mf mD A mA|]; last by move=> mg; exact: measurableT_comp. rewrite [X in measurable X](_ : _ = D `&` (EFin \o g) @^-1` (EFin @` A)); last first. - by apply: mf => //; exists A => //; exists set0; [constructor|rewrite setU0]. + apply: mf => //; exists A => //. + by rewrite RGenOpenSets.measurableE//. + by exists set0; [constructor|rewrite setU0]. congr (_ `&` _);rewrite eqEsubset; split=> [|? []/= _ /[swap] -[->//]]. by move=> ? ?; exact: preimage_image. Qed. diff --git a/theories/measure_theory/measure_function.v b/theories/measure_theory/measure_function.v index 5178317cf..ca0ce40ff 100644 --- a/theories/measure_theory/measure_function.v +++ b/theories/measure_theory/measure_function.v @@ -1786,11 +1786,11 @@ have ndE : ndseq_closed E. - exact: bigcupT_measurable. - transitivity (limn (m1 \o A)). apply/esym/cvg_lim=>//. - exact/(nondecreasing_cvg_mu mA _ ndA)/bigcupT_measurable. + exact/(nondecreasing_cvg_measure mA _ ndA)/bigcupT_measurable. transitivity (limn (m2 \o A)). by apply/congr_lim/funext => n; have [] := EA n. apply/cvg_lim => //. - exact/(nondecreasing_cvg_mu mA _ ndA)/bigcupT_measurable. + exact/(nondecreasing_cvg_measure mA _ ndA)/bigcupT_measurable. - by apply: bigcup_sub => n; have [] := EA n. have sDHE : <> `<=` E. by apply: lambda_system_subset => //; split => //; [move=> ? []|split]. @@ -1821,7 +1821,7 @@ Lemma lim_sup_set_cvg F : (forall k, measurable (F k)) -> mu (\bigcup_(k >= 0) F k) < +oo -> mu (\bigcup_(k >= n) F k) @[n --> \oo] --> mu (lim_sup_set F). Proof. -move=> mF mFoo; apply: nonincreasing_cvg_mu => //. +move=> mF mFoo; apply: nonincreasing_cvg_measure => //. - by move=> i; apply: bigcup_measurable => k /= _; exact: mF. - apply: bigcap_measurable => // k _. by apply: bigcup_measurable => j /= _; exact: mF. @@ -1936,13 +1936,13 @@ have nd_g' : nondecreasing_seq g'. move=> A gA. have -> : A = \bigcup_n (g' n `&` A) by rewrite -setI_bigcupl g'_cover setTI. transitivity (lim (m1 (g' n `&` A) @[n --> \oo])). - apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu. + apply/esym/cvg_lim => //; apply: nondecreasing_cvg_measure. - by move=> n; apply: measurableI; exact/sGm. - by apply: bigcupT_measurable => k; apply: measurableI; exact/sGm. - by move=> ? ? ?; apply/subsetPset; apply: setSI; exact/subsetPset/nd_g'. transitivity (lim (m2 (g' n `&` A) @[n --> \oo])). by apply/congr_lim/funext => x; apply: sG'm1m2 => //; exact/sGm. -apply/cvg_lim => //; apply: nondecreasing_cvg_mu. +apply/cvg_lim => //; apply: nondecreasing_cvg_measure. - by move=> k; apply: measurableI => //; exact/sGm. - by apply: bigcupT_measurable => k; apply: measurableI; exact/sGm. - by move=> a b ab; apply/subsetPset; apply: setSI; exact/subsetPset/nd_g'. diff --git a/theories/pi_irrational.v b/theories/pi_irrational.v index 2ab999382..826419ef2 100644 --- a/theories/pi_irrational.v +++ b/theories/pi_irrational.v @@ -25,6 +25,8 @@ Import Order.TTheory GRing.Theory Num.Theory. Import numFieldNormedType.Exports. (* TODO: move *) +Import MeasurableR. + Lemma measurable_poly {R : realType} (p : {poly R}) (A : set R) : measurable_fun A (horner p). Proof. diff --git a/theories/probability_theory/bernoulli_distribution.v b/theories/probability_theory/bernoulli_distribution.v index bc2974b21..41c08fe9d 100644 --- a/theories/probability_theory/bernoulli_distribution.v +++ b/theories/probability_theory/bernoulli_distribution.v @@ -52,6 +52,8 @@ Qed. End bernoulli_pmf. +Import MeasurableR. + Lemma measurable_bernoulli_pmf {R : realType} D n : measurable_fun D (@bernoulli_pmf R ^~ n). Proof. diff --git a/theories/probability_theory/beta_distribution.v b/theories/probability_theory/beta_distribution.v index 9a879b144..fa3518dc4 100644 --- a/theories/probability_theory/beta_distribution.v +++ b/theories/probability_theory/beta_distribution.v @@ -52,6 +52,8 @@ apply: (@continuous_comp _ _ _ (@onem R) (fun x => x ^+ n)). exact: exprn_continuous. Qed. +Import MeasurableR. + Lemma onemXn_derivable n x : derivable (fun y => y.~ ^+ n) x 1. Proof. have := @derivableX _ _ (@onem R) n x 1. @@ -147,6 +149,8 @@ Qed. Lemma within_continuous_XMonemX A a b : {within A, continuous (XMonemX a b)}. Proof. by apply: continuous_in_subspaceT => x _; exact: continuous_XMonemX. Qed. +Import MeasurableR. + Lemma measurable_XMonemX A a b : measurable_fun A (XMonemX a b). Proof. apply/measurable_funM => //; apply/measurable_funX => //. @@ -201,6 +205,8 @@ Definition beta_fun a b : R := \int[mu]_x (XMonemX a.-1 b.-1 \_`[0,1]) x. Local Open Scope ereal_scope. +Import MeasurableR. + Lemma EFin_beta_fun a b : (beta_fun a b)%:E = \int[mu]_x (XMonemX a.-1 b.-1 \_`[0,1] x)%:E. Proof. @@ -229,11 +235,17 @@ under eq_Rintegral do rewrite XMonemX0n. by rewrite Rintegral_onemXn// prednK. Qed. +Import MeasurableR. + Lemma beta_fun00 : beta_fun 0 0 = 1%R. Proof. rewrite -[LHS]Rintegral_mkcond. under eq_Rintegral do rewrite XMonemX00. -by rewrite Rintegral_cst//= mul1r lebesgue_measure_itv/= lte01 EFinN sube0. +rewrite Rintegral_cst//=. +rewrite mul1r. +(* TODO: fixme *) +rewrite -/(lebesgue_measure). +by rewrite lebesgue_measure_itv/= lte01 EFinN sube0. Qed. Lemma beta_fun1Sn b : beta_fun 1 b.+1 = b.+1%:R^-1. @@ -340,13 +352,14 @@ End beta_fun. Section beta_pdf. Local Open Scope ring_scope. -Context {R : realType}. -Variables a b : nat. +Context {R : realType} (a b : nat). Local Notation XMonemX := (@XMonemX R). Definition beta_pdf t : R := XMonemX a.-1 b.-1 \_`[0, 1] t / beta_fun a b. +Import MeasurableR. + Lemma measurable_beta_pdf : measurable_fun [set: R] beta_pdf. Proof. apply: measurable_funM => //; apply/measurable_restrict => //. @@ -413,12 +426,13 @@ End beta_pdf. Section beta. Local Open Scope ring_scope. -Context {R : realType}. -Variables a b : nat. +Context {R : realType} (a b : nat). Local Notation mu := (@lebesgue_measure R). Local Notation XMonemX := (@XMonemX R). +Import MeasurableR. + Let beta_num (U : set (measurableTypeR R)) : \bar R := \int[mu]_(x in U) (XMonemX a.-1 b.-1 \_`[0,1] x)%:E. @@ -542,6 +556,8 @@ Qed. Local Open Scope ereal_scope. +Import MeasurableR. + Lemma integral_beta_prob_bernoulli_prob_lty {R : realType} a b (f : R -> R) U : measurable_fun [set: R] f -> (forall x : R, x \in `[0, 1]%R -> 0 <= f x <= 1)%R -> @@ -779,7 +795,7 @@ rewrite integralZr//=. - exact: integrableS (integrable_XMonemX_restrict _ _). transitivity ((\int[mu]_x ((@XMonemX R a.-1 b.-1 \_`[0,1] x)%:E - (@XMonemX R (a + c).-1 (b + d).-1 \_`[0,1] x)%:E)) * (beta_fun a b)^-1%:E)%E. - congr (_ * _)%E; rewrite [LHS]integral_mkcond/=; apply eq_integral => x _. + congr (_ * _)%E; rewrite [LHS]integral_mkcond/=; apply: eq_integral => x _. rewrite !patchE; case: ifPn => [->|]; last by rewrite EFinN subee. rewrite /onem -EFinM mulrBl mul1r EFinB EFinN; congr (_ - _)%E. rewrite XMonemXM. diff --git a/theories/probability_theory/binomial_distribution.v b/theories/probability_theory/binomial_distribution.v index 40d598cff..aebc45da4 100644 --- a/theories/probability_theory/binomial_distribution.v +++ b/theories/probability_theory/binomial_distribution.v @@ -48,6 +48,8 @@ Qed. End binomial_pmf. +Import MeasurableR. + Lemma measurable_binomial_pmf {R : realType} D n k : measurable_fun D (@binomial_pmf R n ^~ k). Proof. diff --git a/theories/probability_theory/exponential_distribution.v b/theories/probability_theory/exponential_distribution.v index a24385857..eefd883ab 100644 --- a/theories/probability_theory/exponential_distribution.v +++ b/theories/probability_theory/exponential_distribution.v @@ -55,6 +55,8 @@ apply: continuous_comp; last exact: continuous_expR. by apply: continuousM => //; apply: (@continuousN _ R^o); exact: cst_continuous. Qed. +Import MeasurableR. + Lemma measurable_exponential_pdf : measurable_fun [set: R] exponential_pdf. Proof. apply/measurable_restrict => //; apply: measurable_funTS. @@ -89,6 +91,8 @@ Unshelve. end_near. Qed. End exponential_pdf. +Import MeasurableR. + Definition exponential_prob {R : realType} (rate : R) := fun V => (\int[lebesgue_measure]_(x in V) (exponential_pdf rate x)%:E)%E. diff --git a/theories/probability_theory/normal_distribution.v b/theories/probability_theory/normal_distribution.v index c0f18215a..b19389cd7 100644 --- a/theories/probability_theory/normal_distribution.v +++ b/theories/probability_theory/normal_distribution.v @@ -57,6 +57,8 @@ Implicit Types m s x : R. Definition normal_fun m s x := expR (- (x - m) ^+ 2 / (s ^+ 2 *+ 2)). +Import MeasurableR. + Lemma measurable_normal_fun m s : measurable_fun [set: R] (normal_fun m s). Proof. apply: measurableT_comp => //=; apply: measurable_funM => //=. @@ -107,6 +109,8 @@ Proof. by rewrite mulr_ge0 ?normal_peak_ge0 ?expR_ge0. Qed. Lemma normal_pdf0_gt0 m s x : s != 0 -> 0 < normal_pdf0 m s x. Proof. by move=> s0; rewrite mulr_gt0 ?expR_gt0// normal_peak_gt0. Qed. +Import MeasurableR. + Lemma measurable_normal_pdf0 m s : measurable_fun setT (normal_pdf0 m s). Proof. by apply: measurable_funM => //=; exact: measurable_normal_fun. Qed. @@ -169,6 +173,8 @@ Lemma normal_pdf_sym m s x : s != 0 -> normal_pdf m s x = normal_pdf x s m. Proof. by move=> s0; rewrite !normal_pdfE// normal_fun_sym. Qed. +Import MeasurableR. + Lemma measurable_normal_pdf m s : measurable_fun setT (normal_pdf m s). Proof. rewrite /normal_pdf; have [_|s0] := eqVneq s 0; first exact: measurable_indic. @@ -192,6 +198,8 @@ Qed. End normal_density. +Import MeasurableR. + Definition normal_prob {R : realType} (m : R) (s : R) : set _ -> \bar R := fun V => (\int[lebesgue_measure]_(x in V) (normal_pdf m s x)%:E)%E. diff --git a/theories/probability_theory/poisson_distribution.v b/theories/probability_theory/poisson_distribution.v index f250b5295..135a6105a 100644 --- a/theories/probability_theory/poisson_distribution.v +++ b/theories/probability_theory/poisson_distribution.v @@ -44,6 +44,8 @@ Qed. End poisson_pmf. +Import MeasurableR. + Lemma measurable_poisson_pmf {R : realType} D k : measurable D -> measurable_fun D (@poisson_pmf R ^~ k). Proof. diff --git a/theories/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v index bd313f9b5..cad8a2cf7 100644 --- a/theories/probability_theory/random_variable.v +++ b/theories/probability_theory/random_variable.v @@ -80,6 +80,8 @@ Lemma notin_range_measure d d' (T : measurableType d) (T' : measurableType d') r \notin range X -> P (X @^-1` [set r]) = 0%E. Proof. by rewrite notin_setE => hr; rewrite preimage10. Qed. +Import MeasurableR. + Lemma probability_range d d' (T : measurableType d) (T' : measurableType d') (R : realType) (P : probability T R) (X : {RV P >-> R}) : P (X @^-1` range X) = 1%E. @@ -271,7 +273,7 @@ have cdf_n1 : cdf X n%:R @[n --> \oo] --> 1. have <- : \bigcup_n F n = setT. rewrite -preimage_bigcup -subTset => t _/=. by exists (truncn (X t)).+1; rewrite //= in_itv/= ltW// truncnS_gt. - apply: nondecreasing_cvg_mu => //; first exact: bigcup_measurable. + apply: nondecreasing_cvg_measure => //; first exact: bigcup_measurable. move=> n m nm; apply/subsetPset => x/=; rewrite !in_itv/= => /le_trans. by apply; rewrite ler_nat. by rewrite -(cvg_unique _ cdf_ns cdf_n1). @@ -293,7 +295,7 @@ have cdf_opp_n0 : (cdf X \o -%R) n%:R @[n --> \oo] --> 0. have <- : \bigcap_n F n = set0. rewrite -subset0 => t /(_ (Num.bound (X t)) I). by rewrite /F/= in_itv/= leNgt => /negP; apply; rewrite ltrNl ltrNbound. - apply: nonincreasing_cvg_mu => //=. + apply: nonincreasing_cvg_measure => //=. + by rewrite (le_lt_trans (probability_le1 _ _)) ?ltry. + exact: bigcap_measurable. + move=> m n mn; apply/subsetPset => x/=; rewrite !in_itv => /le_trans; apply. @@ -322,7 +324,7 @@ have cdf_na : cdf X (a + n.+1%:R^-1) @[n --> \oo] --> cdf X a. pose F n := X @^-1` `]-oo, (a + n.+1%:R^-1)%R]. suff : P (F n) @[n --> \oo] --> P (\bigcap_n F n). by rewrite [in X in _ --> X -> _]/F -preimage_bigcap -itvNycEbigcap. - apply: nonincreasing_cvg_mu => [| | |m n mn]. + apply: nonincreasing_cvg_measure => [| | |m n mn]. - by rewrite -ge0_fin_numE// fin_num_measure//; exact: measurable_funPTI. - by move=> ?; exact: measurable_funPTI. - by apply: bigcap_measurable => // ? _; exact: measurable_funPTI. @@ -360,7 +362,7 @@ have : lsf `]-n%:R, r] @[n --> \oo] --> (f r)%:E. apply: (cvg_comp _ _ (cvg_comp _ _ _ (cumulativeNy f))) => //. by apply: (cvg_comp _ _ cvgr_idn); rewrite ninfty. have : lsf `]- n%:R, r] @[n --> \oo] --> lsf (\bigcup_n `]-n%:R, r]%classic). - apply: nondecreasing_cvg_mu => //; first exact: bigcup_measurable. + apply: nondecreasing_cvg_measure => //; first exact: bigcup_measurable. by move=> *; apply/subsetPset/subset_itv; rewrite leBSide//= lerN2 ler_nat. exact: cvg_unique. Unshelve. all: by end_near. Qed. @@ -405,7 +407,7 @@ Let lscdf := lebesgue_stieltjes_measure fcdf. Lemma lebesgue_stieltjes_cdf_id (A : set _) (mA : measurable A) : lscdf A = P A. Proof. -apply: lebesgue_stieltjes_measure_unique => [I [[a b]]/= _ <- | //]. +apply: open_lebesgue_stieltjes_measure_unique => [I [[a b]]/= _ <- | //]. rewrite /lebesgue_stieltjes_measure /measure_extension/=. rewrite measurable_mu_extE/=; first exact: is_ocitv. have [ab | ba] := leP a b; last first. diff --git a/theories/probability_theory/uniform_distribution.v b/theories/probability_theory/uniform_distribution.v index 2220a980a..0f3d60a3b 100644 --- a/theories/probability_theory/uniform_distribution.v +++ b/theories/probability_theory/uniform_distribution.v @@ -31,7 +31,7 @@ Local Open Scope ring_scope. Section uniform_probability. Local Open Scope ring_scope. -Context (R : realType) (a b : R). +Context {R : realType} (a b : R). Definition uniform_pdf x := if a <= x <= b then (b - a)^-1 else 0. @@ -41,6 +41,8 @@ move=> ab; rewrite /uniform_pdf; case: ifPn => // axb. by rewrite invr_ge0// ltW// subr_gt0. Qed. +Import MeasurableR. + Lemma measurable_uniform_pdf : measurable_fun setT uniform_pdf. Proof. rewrite /uniform_pdf /=; apply: measurable_fun_if => //=. diff --git a/theories/realfun.v b/theories/realfun.v index dd0e368af..9119f22a4 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -2905,13 +2905,12 @@ Unshelve. all: by end_near. Qed. End lhopital_at_left. Section lhopital. -Context {R : realType}. -Variables (f df g dg : R -> R) (a b c : R) (l : R). -Hypothesis cab : c \in `]a, b[. -Hypotheses (fdf : forall x, x \in `]a, b[ `\ c -> is_derive x 1 f (df x)) - (gdg : forall x, x \in `]a, b[ `\ c -> is_derive x 1 g (dg x)). -Hypotheses (fa0 : f x @[x --> c] --> 0) (ga0 : g x @[x --> c] --> 0) - (cdg : forall x, x \in `]a, b[ `\ c -> dg x != 0). +Context {R : realType} (f df g dg : R -> R) (a b c : R) (l : R). +Hypotheses (cab : c \in `]a, b[) + (fdf : forall x, x \in `]a, b[ `\ c -> is_derive x 1 f (df x)) + (gdg : forall x, x \in `]a, b[ `\ c -> is_derive x 1 g (dg x)) + (fa0 : f x @[x --> c] --> 0) (ga0 : g x @[x --> c] --> 0) + (cdg : forall x, x \in `]a, b[ `\ c -> dg x != 0). Lemma lhopital : df x / dg x @[x --> c] --> l -> f x / g x @[x --> c^'] --> l. diff --git a/theories/trigo.v b/theories/trigo.v index 53f2dafff..e8da5963e 100644 --- a/theories/trigo.v +++ b/theories/trigo.v @@ -1127,7 +1127,7 @@ End oneDsqr. Hint Extern 0 (is_true (1 <= oneDsqr _)) => solve [apply: oneDsqr_ge1] : core. Section Atan. -Variable R : realType. +Context {R : realType}. Implicit Type x : R. (* Did not see how to use ITV like in the other *) @@ -1290,6 +1290,8 @@ rewrite /Rintegral (@continuous_FTC2 _ _ atan)//. - by rewrite atan0 sube0. Qed. +Import MeasurableR. + Lemma integral0y_oneDsqr : (\int[mu]_(x in `[0%R, +oo[) (oneDsqr x)^-1%:E = (pi / 2)%:E)%E. Proof.