diff --git a/CHANGELOG.md b/CHANGELOG.md index 4a5b57ca1..62d5ebc18 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,96 @@ # Changelog -Lastest releases: [[0.5.3] - 2022-08-10](#053---2022-08-10) and [[0.5.2] - 2022-06-08](#052---2022-07-08) +Lastest releases: [[0.5.4] - 2022-09-07](#055---2022-09-07) and [[0.5.3] - 2022-08-10](#053---2022-08-10) + +## [0.5.4] - 2022-09-07 + +### Added + +- in `mathcomp_extra.v`: + + defintion `onem` and notation ``` `1- ``` + + lemmas `onem0`, `onem1`, `onemK`, `onem_gt0`, `onem_ge0`, `onem_le1`, `onem_lt1`, + `onemX_ge0`, `onemX_lt1`, `onemD`, `onemMr`, `onemM` + + lemmas `natr1`, `nat1r` +- in `classical_sets.v`: + + lemmas `subset_fst_set`, `subset_snd_set`, `fst_set_fst`, `snd_set_snd`, + `fset_setM`, `snd_setM`, `fst_setMR` + + lemmas `xsection_snd_set`, `ysection_fst_set` +- in `constructive_ereal.v`: + + lemmas `ltNye_eq`, `sube_lt0`, `subre_lt0`, `suber_lt0`, `sube_ge0` + + lemmas `dsubre_gt0`, `dsuber_gt0`, `dsube_gt0`, `dsube_le0` +- in `signed.v`: + + lemmas `onem_PosNum`, `onemX_NngNum` +- in `fsbigop.v`: + + lemmas `lee_fsum_nneg_subset`, `lee_fsum` +- in `topology.v`: + + lemma `near_inftyS` + + lemma `continuous_closedP`, `closedU`, `pasting` + + lemma `continuous_inP` + + lemmas `open_setIS`, `open_setSI`, `closed_setIS`, `closed_setSI` +- in `normedtype.v`: + + definitions `contraction` and `is_contraction` + + lemma `contraction_fixpoint_unique` +- in `sequences.v`: + + lemmas `contraction_dist`, `contraction_cvg`, + `contraction_cvg_fixed`, `banach_fixed_point`, + `contraction_unique` +- in `derive.v`: + + lemma `diff_derivable` +- in `measure.v`: + + lemma `measurable_funTS` +- in `lebesgue_measure.v`: + + lemma `measurable_fun_fine` + + lemma `open_measurable_subspace` + + lemma ``subspace_continuous_measurable_fun`` + + corollary `open_continuous_measurable_fun` + + Hint about `measurable_fun_normr` +- in `lebesgue_integral.v`: + + lemma `measurable_fun_indic` + + lemma `ge0_integral_mscale` + + lemma `integral_pushforward` + +### Changed + +- in `esum.v`: + + definition `esum` +- moved from `lebesgue_integral.v` to `classical_sets.v`: + + `mem_set_pair1` -> `mem_xsection` + + `mem_set_pair2` -> `mem_ysection` +- in `derive.v`: + + generalized `is_diff_scalel` +- in `measure.v`: + + generalize `measurable_uncurry` +- in `lebesgue_measure.v`: + + `pushforward` requires a proof that its argument is measurable +- in `lebesgue_integral.v`: + + change implicits of `integralM_indic` + +### Renamed + +- in `constructive_ereal.v`: + + `lte_pinfty_eq` -> `ltey_eq` + + `le0R` -> `fine_ge0` + + `lt0R` -> `fine_gt0` +- in `ereal.v`: + + `lee_pinfty_eq` -> `leye_eq` + + `lee_ninfty_eq` -> `leeNy_eq` +- in `esum.v`: + + `esum0` -> `esum1` +- in `sequences.v`: + + `nneseries_lim_ge0` -> `nneseries_ge0` +- in `measure.v`: + + `ring_fsets` -> `ring_finite_set` + + `discrete_measurable` -> `discrete_measurable_nat` + + `cvg_mu_inc` -> `nondecreasing_cvg_mu` +- in `lebesgue_integral.v`: + + `muleindic_ge0` -> `nnfun_muleindic_ge0` + + `mulem_ge0` -> `mulemu_ge0` + + `nnfun_mulem_ge0` -> `nnsfun_mulemu_ge0` + +### Removed + +- in `esum.v`: + + lemma `fsetsP`, `sum_fset_set` ## [0.5.3] - 2022-08-10 diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 99aa513be..a3ee55697 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -3,49 +3,15 @@ ## [Unreleased] ### Added -- in `normedtype.v`: - + definitions `contraction` and `is_contraction` - + lemma `contraction_fixpoint_unique` - -- in `constructive_ereal.v`: - + lemmas `ltNye_eq`, `sube_lt0`, `subre_lt0`, `suber_lt0`, `sube_ge0` - + lemmas `dsubre_gt0`, `dsuber_gt0`, `dsube_gt0`, `dsube_le0` - - in `topology.v`: - + lemma `near_inftyS` -- in `sequences.v`: - + lemmas `contraction_dist`, `contraction_cvg`, - `contraction_cvg_fixed`, `banach_fixed_point`, - `contraction_unique` -- in `mathcomp_extra.v`: - + defintion `onem` and notation ``` `1- ``` - + lemmas `onem0`, `onem1`, `onemK`, `onem_gt0`, `onem_ge0`, `onem_le1`, `onem_lt1`, - `onemX_ge0`, `onemX_lt1`, `onemD`, `onemMr`, `onemM` -- in `signed.v`: - + lemmas `onem_PosNum`, `onemX_NngNum` + + lemmas `continuous_subspaceT`, `subspaceT_continuous` ### Changed -- in `measure.v`: - + generalize `measurable_uncurry` - ### Renamed -- in `constructive_ereal.v`: - + `lte_pinfty_eq` -> `ltey_eq` -- in `sequences.v`: - + `nneseries_lim_ge0` -> `nneseries_ge0` -- in `constructive_ereal.v`: - + `le0R` -> `fine_ge0` - + `lt0R` -> `fine_gt0` -- in `measure.v`: - + `ring_fsets` -> `ring_finite_set` - + `discrete_measurable` -> `discrete_measurable_nat` -- in `ereal.v`: - + `lee_pinfty_eq` -> `leye_eq` - + `lee_ninfty_eq` -> `leeNy_eq` -- in `measure.v`: - + `cvg_mu_inc` -> `nondecreasing_cvg_mu` +- in `topology.v`: + + renamed `continuous_subspaceT` to `continuous_in_subspaceT` ### Removed diff --git a/INSTALL.md b/INSTALL.md index 5b0c85aac..19435cf87 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -5,7 +5,7 @@ - [The Coq Proof Assistant version ≥ 8.13](https://coq.inria.fr) - [Mathematical Components version ≥ 1.13.0](https://github.com/math-comp/math-comp) - [Finmap library version ≥ 1.5.1](https://github.com/math-comp/finmap) -- [Hierarchy builder version >= 1.2.0](https://github.com/math-comp/hierarchy-builder) +- [Hierarchy builder version >= 1.3.0](https://github.com/math-comp/hierarchy-builder) These requirements can be installed in a custom way, or through [opam](https://opam.ocaml.org/) (the recommended way) using @@ -47,7 +47,7 @@ $ opam install coq-mathcomp-analysis ``` To install a precise version, type, say ``` -$ opam install coq-mathcomp-analysis.0.5.3 +$ opam install coq-mathcomp-analysis.0.5.4 ``` 4. Everytime you want to work in this same context, you need to type ``` diff --git a/README.md b/README.md index 723f921bc..c7748564f 100644 --- a/README.md +++ b/README.md @@ -33,7 +33,7 @@ the Coq proof-assistant and using the Mathematical Components library. - Pierre-Yves Strub (initial) - Laurent Théry - License: [CeCILL-C](LICENSE) -- Compatible Coq versions: Coq 8.14 to 8.15 (or dev) +- Compatible Coq versions: Coq 8.14 to 8.16 (or dev) - Additional dependencies: - [MathComp ssreflect 1.13 or later](https://math-comp.github.io) - [MathComp fingroup 1.13 or later](https://math-comp.github.io) diff --git a/_CoqProject b/_CoqProject index 9adc71f2f..600698fb5 100644 --- a/_CoqProject +++ b/_CoqProject @@ -32,6 +32,9 @@ theories/derive.v theories/measure.v theories/numfun.v theories/lebesgue_integral.v +theories/kernel.v +theories/prob_lang.v +theories/wip.v theories/summability.v theories/functions.v theories/signed.v diff --git a/coq-mathcomp-analysis.opam b/coq-mathcomp-analysis.opam index dacb81fa1..3e8ca66e9 100644 --- a/coq-mathcomp-analysis.opam +++ b/coq-mathcomp-analysis.opam @@ -18,7 +18,7 @@ the Coq proof-assistant and using the Mathematical Components library.""" build: [make "-j%{jobs}%"] install: [make "install"] depends: [ - "coq" { (>= "8.14" & < "8.16~") | (= "dev") } + "coq" { (>= "8.14" & < "8.17~") | (= "dev") } "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.16~") | (= "dev") } "coq-mathcomp-fingroup" { (>= "1.13.0" & < "1.16~") | (= "dev") } "coq-mathcomp-algebra" { (>= "1.13.0" & < "1.16~") | (= "dev") } diff --git a/meta.yml b/meta.yml index 9690e63d3..9223c2079 100644 --- a/meta.yml +++ b/meta.yml @@ -49,8 +49,8 @@ license: file: LICENSE supported_coq_versions: - text: Coq 8.14 to 8.15 (or dev) - opam: '{ (>= "8.14" & < "8.16~") | (= "dev") }' + text: Coq 8.14 to 8.16 (or dev) + opam: '{ (>= "8.14" & < "8.17~") | (= "dev") }' tested_coq_opam_versions: - version: '1.13.0-coq-8.14' diff --git a/theories/Rstruct.v b/theories/Rstruct.v index 0a7d9c6a0..18941ddfe 100644 --- a/theories/Rstruct.v +++ b/theories/Rstruct.v @@ -503,15 +503,19 @@ Section bigmaxr. Context {R : realDomainType}. (* bigop pour le max pour des listes non vides ? *) +#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")] Definition bigmaxr (r : R) s := \big[Num.max/head r s]_(i <- s) i. +#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")] Lemma bigmaxr_nil (x0 : R) : bigmaxr x0 [::] = x0. Proof. by rewrite /bigmaxr /= big_nil. Qed. +#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")] Lemma bigmaxr_un (x0 x : R) : bigmaxr x0 [:: x] = x. Proof. by rewrite /bigmaxr /= big_cons big_nil maxxx. Qed. (* previous definition *) +#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")] Lemma bigmaxrE (r : R) s : bigmaxr r s = foldr Num.max (head r s) (behead s). Proof. rewrite (_ : bigmaxr _ _ = if s isn't h :: t then r else \big[Num.max/h]_(i <- s) i). @@ -520,6 +524,7 @@ rewrite (_ : bigmaxr _ _ = if s isn't h :: t then r else \big[Num.max/h]_(i <- s by case: s => //=; rewrite /bigmaxr big_nil. Qed. +#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")] Lemma bigrmax_dflt (x y : R) s : Num.max x (\big[Num.max/x]_(j <- y :: s) j) = Num.max x (\big[Num.max/y]_(i <- y :: s) i). Proof. @@ -528,10 +533,12 @@ by rewrite !big_cons !big_nil maxxx maxCA maxxx maxC. by rewrite big_cons maxCA IH maxCA [in RHS]big_cons IH. Qed. +#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")] Lemma bigmaxr_cons (x0 x y : R) lr : bigmaxr x0 (x :: y :: lr) = Num.max x (bigmaxr x0 (y :: lr)). Proof. by rewrite [y :: lr]lock /bigmaxr /= -lock big_cons bigrmax_dflt. Qed. +#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")] Lemma bigmaxr_ler (x0 : R) s i : (i < size s)%N -> (nth x0 s i) <= (bigmaxr x0 s). Proof. @@ -542,6 +549,7 @@ by rewrite big_cons bigrmax_dflt le_maxr orbC IH. Qed. (* Compatibilité avec l'addition *) +#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")] Lemma bigmaxr_addr (x0 : R) lr (x : R) : bigmaxr (x0 + x) (map (fun y : R => y + x) lr) = (bigmaxr x0 lr) + x. Proof. @@ -550,6 +558,7 @@ elim: t h => /= [|h' t IH] h; first by rewrite ?(big_cons,big_nil) -addr_maxl. by rewrite [in RHS]big_cons bigrmax_dflt addr_maxl -IH big_cons bigrmax_dflt. Qed. +#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")] Lemma bigmaxr_mem (x0 : R) lr : (0 < size lr)%N -> bigmaxr x0 lr \in lr. Proof. rewrite /bigmaxr; case: lr => // h t _. @@ -560,6 +569,7 @@ rewrite big_cons bigrmax_dflt inE eq_le; case: lerP => /=. Qed. (* TODO: bigmaxr_morph? *) +#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")] Lemma bigmaxr_mulr (A : finType) (s : seq A) (k : R) (x : A -> R) : 0 <= k -> bigmaxr 0 (map (fun i => k * x i) s) = k * bigmaxr 0 (map x s). Proof. @@ -569,6 +579,7 @@ by rewrite !bigmaxr_un. by rewrite bigmaxr_cons {}ih bigmaxr_cons maxr_pmulr. Qed. +#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")] Lemma bigmaxr_index (x0 : R) lr : (0 < size lr)%N -> (index (bigmaxr x0 lr) lr < size lr)%N. Proof. @@ -577,6 +588,7 @@ move: (@bigmaxr_mem x0 (h :: t) isT). by rewrite ltnS index_mem inE /= eq_sym H. Qed. +#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")] Lemma bigmaxr_lerP (x0 : R) lr (x : R) : (0 < size lr)%N -> reflect (forall i, (i < size lr)%N -> (nth x0 lr i) <= x) ((bigmaxr x0 lr) <= x). @@ -586,6 +598,7 @@ move=> lr_size; apply: (iffP idP) => [le_x i i_size | H]. by move/(nthP x0): (bigmaxr_mem x0 lr_size) => [i i_size <-]; apply: H. Qed. +#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")] Lemma bigmaxr_ltrP (x0 : R) lr (x : R) : (0 < size lr)%N -> reflect (forall i, (i < size lr)%N -> (nth x0 lr i) < x) ((bigmaxr x0 lr) < x). @@ -595,6 +608,7 @@ move=> lr_size; apply: (iffP idP) => [lt_x i i_size | H]. by move/(nthP x0): (bigmaxr_mem x0 lr_size) => [i i_size <-]; apply: H. Qed. +#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")] Lemma bigmaxrP (x0 : R) lr (x : R) : (x \in lr /\ forall i, (i < size lr) %N -> (nth x0 lr i) <= x) -> (bigmaxr x0 lr = x). Proof. @@ -614,6 +628,7 @@ apply/negP => /eqP H; apply: neq_i; rewrite -H eq_sym; apply/eqP. by apply: index_uniq. Qed. *) +#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")] Lemma bigmaxr_lerif (x0 : R) lr : uniq lr -> forall i, (i < size lr)%N -> (nth x0 lr i) <= (bigmaxr x0 lr) ?= iff (i == index (bigmaxr x0 lr) lr). @@ -625,9 +640,11 @@ by apply: bigmaxr_mem; apply: (leq_trans _ i_size). Qed. (* bigop pour le max pour des listes non vides ? *) +#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")] Definition bmaxrf n (f : {ffun 'I_n.+1 -> R}) := bigmaxr (f ord0) (codom f). +#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")] Lemma bmaxrf_ler n (f : {ffun 'I_n.+1 -> R}) i : (f i) <= (bmaxrf f). Proof. @@ -637,6 +654,7 @@ suff -> : nth (f ord0) (codom f) i = f i; first by []. by rewrite /codom (nth_map ord0) ?size_enum_ord // nth_ord_enum. Qed. +#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")] Lemma bmaxrf_index n (f : {ffun 'I_n.+1 -> R}) : (index (bmaxrf f) (codom f) < n.+1)%N. Proof. @@ -646,11 +664,14 @@ rewrite [in X in (_ < X)%N](_ : n.+1 = size (codom f)); last first. by apply: bigmaxr_index; rewrite size_codom card_ord. Qed. +#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")] Definition index_bmaxrf n f := Ordinal (@bmaxrf_index n f). +#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")] Lemma ordnat i n (ord_i : (i < n)%N) : i = Ordinal ord_i :> nat. Proof. by []. Qed. +#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")] Lemma eq_index_bmaxrf n (f : {ffun 'I_n.+1 -> R}) : f (index_bmaxrf f) = bmaxrf f. Proof. @@ -661,6 +682,7 @@ move/(nth_index (f ord0)) => <-; rewrite (nth_map ord0). by rewrite size_enum_ord; apply: bmaxrf_index. Qed. +#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")] Lemma bmaxrf_lerif n (f : {ffun 'I_n.+1 -> R}) : injective f -> forall i, (f i) <= (bmaxrf f) ?= iff (i == index_bmaxrf f). diff --git a/theories/classical_sets.v b/theories/classical_sets.v index e14ea7e3e..4bd42aff8 100644 --- a/theories/classical_sets.v +++ b/theories/classical_sets.v @@ -2907,6 +2907,31 @@ End Exports. End SetOrder. Export SetOrder.Exports. +Section product. +Variables (T1 T2 : Type). +Implicit Type A B : set (T1 * T2). + +Lemma subset_fst_set : {homo @fst_set T1 T2 : A B / A `<=` B}. +Proof. by move=> A B AB x [y Axy]; exists y; exact/AB. Qed. + +Lemma subset_snd_set : {homo @snd_set T1 T2 : A B / A `<=` B}. +Proof. by move=> A B AB x [y Axy]; exists y; exact/AB. Qed. + +Lemma fst_set_fst A : A `<=` A.`1 \o fst. Proof. by move=> [x y]; exists y. Qed. + +Lemma snd_set_snd A: A `<=` A.`2 \o snd. Proof. by move=> [x y]; exists x. Qed. + +Lemma fst_setM (X : set T1) (Y : set T2) : (X `*` Y).`1 `<=` X. +Proof. by move=> x [y [//]]. Qed. + +Lemma snd_setM (X : set T1) (Y : set T2) : (X `*` Y).`2 `<=` Y. +Proof. by move=> x [y [//]]. Qed. + +Lemma fst_setMR (X : set T1) (Y : T1 -> set T2) : (X `*`` Y).`1 `<=` X. +Proof. by move=> x [y [//]]. Qed. + +End product. + Section section. Variables (T1 T2 : Type). Implicit Types (A : set (T1 * T2)) (x : T1) (y : T2). @@ -2915,6 +2940,18 @@ Definition xsection A x := [set y | (x, y) \in A]. Definition ysection A y := [set x | (x, y) \in A]. +Lemma xsection_snd_set A x : xsection A x `<=` A.`2. +Proof. by move=> y Axy; exists x; rewrite /xsection/= inE in Axy. Qed. + +Lemma ysection_fst_set A y : ysection A y `<=` A.`1. +Proof. by move=> x Axy; exists y; rewrite /ysection/= inE in Axy. Qed. + +Lemma mem_xsection x y A : (y \in xsection A x) = ((x, y) \in A). +Proof. by apply/idP/idP => [|]; [rewrite inE|rewrite /xsection !inE /= inE]. Qed. + +Lemma mem_ysection x y A : (x \in ysection A y) = ((x, y) \in A). +Proof. by apply/idP/idP => [|]; [rewrite inE|rewrite /ysection !inE /= inE]. Qed. + Lemma xsection0 x : xsection set0 x = set0. Proof. by rewrite predeqE /xsection => y; split => //=; rewrite inE. Qed. @@ -2923,16 +2960,14 @@ Proof. by rewrite predeqE /ysection => x; split => //=; rewrite inE. Qed. Lemma in_xsectionM X1 X2 x : x \in X1 -> xsection (X1 `*` X2) x = X2. Proof. -move=> xX1; rewrite /xsection predeqE => y /=; split; rewrite inE. - by move=> []. -by move=> X2y; split => //=; rewrite inE in xX1. +move=> xX1; apply/seteqP; split=> [y /xsection_snd_set|]; first exact: snd_setM. +by move=> y X2y; rewrite /xsection/= inE; split=> //=; rewrite inE in xX1. Qed. Lemma in_ysectionM X1 X2 y : y \in X2 -> ysection (X1 `*` X2) y = X1. Proof. -move=> yX2; rewrite /ysection predeqE => x /=; split; rewrite inE. - by move=> []. -by move=> X1x; split => //=; rewrite inE in yX2. +move=> yX2; apply/seteqP; split=> [x /ysection_fst_set|]; first exact: fst_setM. +by move=> x X1x; rewrite /ysection/= inE; split=> //=; rewrite inE in yX2. Qed. Lemma notin_xsectionM X1 X2 x : x \notin X1 -> xsection (X1 `*` X2) x = set0. diff --git a/theories/derive.v b/theories/derive.v index eeedb6157..f7e6aa632 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -655,13 +655,13 @@ apply: DiffDef; first exact/linear_differentiable/scaler_continuous. by rewrite diff_lin //; apply: scaler_continuous. Qed. -Global Instance is_diff_scalel (x k : R) : +Global Instance is_diff_scalel (k : R) (x : V) : is_diff k ( *:%R ^~ x) ( *:%R ^~ x). Proof. -have -> : *:%R ^~ x = GRing.scale_linear R x. - by rewrite funeqE => ? /=; rewrite [_ *: _]mulrC. -apply: DiffDef; first exact/linear_differentiable/scaler_continuous. -by rewrite diff_lin //; apply: scaler_continuous. +have sx_lin : linear ( *:%R ^~ x) by move=> u y z; rewrite scalerDl scalerA. +have -> : *:%R ^~ x = Linear sx_lin by rewrite funeqE. +apply: DiffDef; first exact/linear_differentiable/scalel_continuous. +by rewrite diff_lin//; apply: scalel_continuous. Qed. Lemma differentiable_coord m n (M : 'M[R]_(m.+1, n.+1)) i j : @@ -1007,10 +1007,11 @@ Proof. by move=> /differentiableP df; rewrite diff_val. Qed. End DifferentialR3_numFieldType. -Section Derive. -Variables (R : numFieldType) (V W : normedModType R). +Section DeriveRU. +Variables (R : numFieldType) (U : normedModType R). +Implicit Types f : R -> U. -Let der1 (U : normedModType R) (f : R -> U) x : derivable f x 1 -> +Let der1 f x : derivable f x 1 -> f \o shift x = cst (f x) + ( *:%R^~ (f^`() x)) +o_ (0 : R) id. Proof. move=> df; apply/eqaddoE; have /derivable_nbhsP := df. @@ -1019,20 +1020,19 @@ have -> : (fun h => (f \o shift x) h%:A) = f \o shift x. by rewrite derive1E =>->. Qed. -Lemma deriv1E (U : normedModType R) (f : R -> U) x : - derivable f x 1 -> 'd f x = ( *:%R^~ (f^`() x)) :> (R -> U). +Lemma deriv1E f x : derivable f x 1 -> 'd f x = ( *:%R^~ (f^`() x)) :> (R -> U). Proof. move=> df; have lin_scal : linear (fun h : R => h *: f^`() x). - by move=> ???; rewrite scalerDl scalerA. + by move=> ? ? ?; rewrite scalerDl scalerA. have -> : (fun h => h *: f^`() x) = Linear lin_scal by []. by apply: diff_unique; [apply: scalel_continuous|apply: der1]. Qed. -Lemma diff1E (U : normedModType R) (f : R -> U) x : +Lemma diff1E f x : differentiable f x -> 'd f x = (fun h => h *: f^`() x) :> (R -> U). Proof. move=> df; have lin_scal : linear (fun h : R => h *: 'd f x 1). - by move=> ???; rewrite scalerDl scalerA. + by move=> ? ? ?; rewrite scalerDl scalerA. have -> : (fun h => h *: f^`() x) = Linear lin_scal. by rewrite derive1E'. apply: diff_unique; first exact: scalel_continuous. @@ -1040,8 +1040,7 @@ apply/eqaddoE; have /diff_locally -> := df; congr (_ + _ + _). by rewrite funeqE => h /=; rewrite -{1}[h]mulr1 linearZ. Qed. -Lemma derivable1_diffP (U : normedModType R) (f : R -> U) x : - derivable f x 1 <-> differentiable f x. +Lemma derivable1_diffP f x : derivable f x 1 <-> differentiable f x. Proof. split=> dfx. by apply/diff_locallyP; rewrite deriv1E //; split; @@ -1052,7 +1051,13 @@ have -> : (fun h => (f \o shift x) h%:A) = f \o shift x. by have /diff_locally := dfx; rewrite diff1E // derive1E =>->. Qed. -Lemma derivable1P (U : normedModType R) (f : V -> U) x v : +End DeriveRU. + +Section DeriveVW. +Variables (R : numFieldType) (V W : normedModType R). +Implicit Types f : V -> W. + +Lemma derivable1P f x v : derivable f x v <-> derivable (fun h : R => f (h *: v + x)) 0 1. Proof. rewrite /derivable; set g1 := fun h => h^-1 *: _; set g2 := fun h => h^-1 *: _. @@ -1060,19 +1065,32 @@ suff -> : g1 = g2 by []. by rewrite funeqE /g1 /g2 => h /=; rewrite addr0 scale0r add0r [_%:A]mulr1. Qed. -Lemma derivableP (U : normedModType R) (f : V -> U) x v : - derivable f x v -> is_derive x v f ('D_v f x). +Lemma derivableP f x v : derivable f x v -> is_derive x v f ('D_v f x). Proof. by move=> df; apply: DeriveDef. Qed. -Global Instance is_derive_cst (U : normedModType R) (a : U) (x v : V) : - is_derive x v (cst a) 0. +Lemma diff_derivable f a v : differentiable f a -> derivable f a v. +Proof. +move=> dfa; apply/derivable1P/derivable1_diffP. +by apply: differentiable_comp; rewrite ?scale0r ?add0r. +Qed. + +Global Instance is_derive_cst (a : W) (x v : V) : is_derive x v (cst a) 0. Proof. apply: DeriveDef; last by rewrite deriveE // diff_val. -apply/derivable1P/derivable1_diffP. -by have -> : (fun h => cst a (h *: v + x)) = cst a by rewrite funeqE. +exact/diff_derivable. Qed. -Fact der_add (f g : V -> W) (x v : V) : derivable f x v -> derivable g x v -> +Lemma is_derive_eq f (x v : V) (df f' : W) : + is_derive x v f f' -> f' = df -> is_derive x v f df. +Proof. by move=> ? <-. Qed. + +End DeriveVW. + +Section Derive_lemmasVW. +Variables (R : numFieldType) (V W : normedModType R). +Implicit Types f g : V -> W. + +Fact der_add f g (x v : V) : derivable f x v -> derivable g x v -> (fun h => h^-1 *: (((f + g) \o shift x) (h *: v) - (f + g) x)) @ 0^' --> 'D_v f x + 'D_v g x. Proof. @@ -1083,50 +1101,50 @@ evar (fg : R -> W); rewrite [X in X @ _](_ : _ = fg) /=; last first. exact: cvgD. Qed. -Lemma deriveD (f g : V -> W) (x v : V) : derivable f x v -> derivable g x v -> +Lemma deriveD f g (x v : V) : derivable f x v -> derivable g x v -> 'D_v (f + g) x = 'D_v f x + 'D_v g x. Proof. by move=> df dg; apply: cvg_map_lim (der_add df dg). Qed. -Lemma derivableD (f g : V -> W) (x v : V) : +Lemma derivableD f g (x v : V) : derivable f x v -> derivable g x v -> derivable (f + g) x v. Proof. move=> df dg; apply/cvg_ex; exists (derive f x v + derive g x v). exact: der_add. Qed. -Global Instance is_deriveD (f g : V -> W) (x v : V) (df dg : W) : +Global Instance is_deriveD f g (x v : V) (df dg : W) : is_derive x v f df -> is_derive x v g dg -> is_derive x v (f + g) (df + dg). Proof. move=> dfx dgx; apply: DeriveDef; first exact: derivableD. by rewrite deriveD // !derive_val. Qed. -Global Instance is_derive_sum n (f : 'I_n -> V -> W) (x v : V) - (df : 'I_n -> W) : (forall i, is_derive x v (f i) (df i)) -> - is_derive x v (\sum_(i < n) f i) (\sum_(i < n) df i). +Global Instance is_derive_sum n (h : 'I_n -> V -> W) (x v : V) + (dh : 'I_n -> W) : (forall i, is_derive x v (h i) (dh i)) -> + is_derive x v (\sum_(i < n) h i) (\sum_(i < n) dh i). Proof. -elim: n f df => [f df dfx|f df dfx n ihn]. +elim: n h dh => [h dh dhx|h dh dhx n ihn]. by rewrite !big_ord0 //; apply: is_derive_cst. by rewrite !big_ord_recr /=; apply: is_deriveD. Qed. -Lemma derivable_sum n (f : 'I_n -> V -> W) (x v : V) : - (forall i, derivable (f i) x v) -> derivable (\sum_(i < n) f i) x v. +Lemma derivable_sum n (h : 'I_n -> V -> W) (x v : V) : + (forall i, derivable (h i) x v) -> derivable (\sum_(i < n) h i) x v. Proof. -move=> df; suff : forall i, is_derive x v (f i) ('D_v (f i) x) by []. +move=> df; suff : forall i, is_derive x v (h i) ('D_v (h i) x) by []. by move=> ?; apply: derivableP. Qed. -Lemma derive_sum n (f : 'I_n -> V -> W) (x v : V) : - (forall i, derivable (f i) x v) -> - 'D_v (\sum_(i < n) f i) x = \sum_(i < n) 'D_v (f i) x. +Lemma derive_sum n (h : 'I_n -> V -> W) (x v : V) : + (forall i, derivable (h i) x v) -> + 'D_v (\sum_(i < n) h i) x = \sum_(i < n) 'D_v (h i) x. Proof. -move=> df; suff dfx : forall i, is_derive x v (f i) ('D_v (f i) x). +move=> df; suff dfx : forall i, is_derive x v (h i) ('D_v (h i) x). by rewrite derive_val. by move=> ?; apply: derivableP. Qed. -Fact der_opp (f : V -> W) (x v : V) : derivable f x v -> +Fact der_opp f (x v : V) : derivable f x v -> (fun h => h^-1 *: (((- f) \o shift x) (h *: v) - (- f) x)) @ 0^' --> - 'D_v f x. Proof. @@ -1135,65 +1153,67 @@ move=> df; evar (g : R -> W); rewrite [X in X @ _](_ : _ = g) /=; last first. exact: cvgN. Qed. -Lemma deriveN (f : V -> W) (x v : V) : derivable f x v -> +Lemma deriveN f (x v : V) : derivable f x v -> 'D_v (- f) x = - 'D_v f x. Proof. by move=> df; apply: cvg_map_lim (der_opp df). Qed. -Lemma derivableN (f : V -> W) (x v : V) : +Lemma derivableN f (x v : V) : derivable f x v -> derivable (- f) x v. Proof. by move=> df; apply/cvg_ex; exists (- 'D_v f x); apply: der_opp. Qed. -Global Instance is_deriveN (f : V -> W) (x v : V) (df : W) : +Global Instance is_deriveN f (x v : V) (df : W) : is_derive x v f df -> is_derive x v (- f) (- df). Proof. move=> dfx; apply: DeriveDef; first exact: derivableN. by rewrite deriveN // derive_val. Qed. -Lemma is_derive_eq (V' W' : normedModType R) (f : V' -> W') (x v : V') - (df f' : W') : is_derive x v f f' -> f' = df -> is_derive x v f df. -Proof. by move=> ? <-. Qed. - -Global Instance is_deriveB (f g : V -> W) (x v : V) (df dg : W) : +Global Instance is_deriveB f g (x v : V) (df dg : W) : is_derive x v f df -> is_derive x v g dg -> is_derive x v (f - g) (df - dg). Proof. by move=> ??; apply: is_derive_eq. Qed. -Lemma deriveB (f g : V -> W) (x v : V) : derivable f x v -> derivable g x v -> +Lemma deriveB f g (x v : V) : derivable f x v -> derivable g x v -> 'D_v (f - g) x = 'D_v f x - 'D_v g x. Proof. by move=> /derivableP df /derivableP dg; rewrite derive_val. Qed. -Lemma derivableB (f g : V -> W) (x v : V) : +Lemma derivableB f g (x v : V) : derivable f x v -> derivable g x v -> derivable (f - g) x v. Proof. by move=> /derivableP df /derivableP dg. Qed. -Fact der_scal (f : V -> W) (k : R) (x v : V) : derivable f x v -> +Fact der_scal f (k : R) (x v : V) : derivable f x v -> (fun h => h^-1 *: ((k \*: f \o shift x) (h *: v) - (k \*: f) x)) @ (0 : R)^' --> k *: 'D_v f x. Proof. -move=> df; evar (g : R -> W); rewrite [X in X @ _](_ : _ = g) /=; last first. - rewrite funeqE => h. - by rewrite scalerBr !scalerA mulrC -!scalerA -!scalerBr /g. +move=> df; evar (h : R -> W); rewrite [X in X @ _](_ : _ = h) /=; last first. + rewrite funeqE => r. + by rewrite scalerBr !scalerA mulrC -!scalerA -!scalerBr /h. exact: cvgZr. Qed. -Lemma deriveZ (f : V -> W) (k : R) (x v : V) : derivable f x v -> +Lemma deriveZ f (k : R) (x v : V) : derivable f x v -> 'D_v (k \*: f) x = k *: 'D_v f x. Proof. by move=> df; apply: cvg_map_lim (der_scal df). Qed. -Lemma derivableZ (f : V -> W) (k : R) (x v : V) : +Lemma derivableZ f (k : R) (x v : V) : derivable f x v -> derivable (k \*: f) x v. Proof. by move=> df; apply/cvg_ex; exists (k *: 'D_v f x); apply: der_scal. Qed. -Global Instance is_deriveZ (f : V -> W) (k : R) (x v : V) (df : W) : +Global Instance is_deriveZ f (k : R) (x v : V) (df : W) : is_derive x v f df -> is_derive x v (k \*: f) (k *: df). Proof. move=> dfx; apply: DeriveDef; first exact: derivableZ. by rewrite deriveZ // derive_val. Qed. -Fact der_mult (f g : V -> R) (x v : V) : +End Derive_lemmasVW. + +Section Derive_lemmasVR. +Variables (R : numFieldType) (V : normedModType R). +Implicit Types f g : V -> R. + +Fact der_mult f g (x v : V) : derivable f x v -> derivable g x v -> (fun h => h^-1 *: (((f * g) \o shift x) (h *: v) - (f * g) x)) @ (0 : R)^' --> f x *: 'D_v g x + g x *: 'D_v f x. @@ -1210,22 +1230,21 @@ apply: cvgD; last exact: cvgZr df. apply: cvg_comp2 (@mul_continuous _ (_, _)) => /=; last exact: dg. suff : {for 0, continuous (fun h : R => f(h *: v + x))}. by move=> /continuous_withinNx; rewrite scale0r add0r. -exact/differentiable_continuous/derivable1_diffP/derivable1P. +exact/differentiable_continuous/derivable1_diffP/(derivable1P _ _ _).1. Qed. -Lemma deriveM (f g : V -> R) (x v : V) : - derivable f x v -> derivable g x v -> +Lemma deriveM f g (x v : V) : derivable f x v -> derivable g x v -> 'D_v (f * g) x = f x *: 'D_v g x + g x *: 'D_v f x. Proof. by move=> df dg; apply: cvg_map_lim (der_mult df dg). Qed. -Lemma derivableM (f g : V -> R) (x v : V) : +Lemma derivableM f g (x v : V) : derivable f x v -> derivable g x v -> derivable (f * g) x v. Proof. move=> df dg; apply/cvg_ex; exists (f x *: 'D_v g x + g x *: 'D_v f x). exact: der_mult. Qed. -Global Instance is_deriveM (f g : V -> R) (x v : V) (df dg : R) : +Global Instance is_deriveM f g (x v : V) (df dg : R) : is_derive x v f df -> is_derive x v g dg -> is_derive x v (f * g) (f x *: dg + g x *: df). Proof. @@ -1233,7 +1252,7 @@ move=> dfx dgx; apply: DeriveDef; first exact: derivableM. by rewrite deriveM // !derive_val. Qed. -Global Instance is_deriveX (f : V -> R) n (x v : V) (df : R) : +Global Instance is_deriveX f n (x v : V) (df : R) : is_derive x v f df -> is_derive x v (f ^+ n.+1) ((n.+1%:R * f x ^+n) *: df). Proof. move=> dfx; elim: n => [|n ihn]; first by rewrite expr1 expr0 mulr1 scale1r. @@ -1242,17 +1261,14 @@ rewrite scalerA -scalerDl mulrCA -[f x * _]exprS. by rewrite [in LHS]mulr_natl exprfctE -mulrSr mulr_natl. Qed. -Lemma derivableX (f : V -> R) n (x v : V) : - derivable f x v -> derivable (f ^+ n.+1) x v. +Lemma derivableX f n (x v : V) : derivable f x v -> derivable (f ^+ n.+1) x v. Proof. by move/derivableP. Qed. -Lemma deriveX (f : V -> R) n (x v : V) : - derivable f x v -> +Lemma deriveX f n (x v : V) : derivable f x v -> 'D_v (f ^+ n.+1) x = (n.+1%:R * f x ^+ n) *: 'D_v f x. Proof. by move=> /derivableP df; rewrite derive_val. Qed. -Fact der_inv (f : V -> R) (x v : V) : - f x != 0 -> derivable f x v -> +Fact der_inv f (x v : V) : f x != 0 -> derivable f x v -> (fun h => h^-1 *: (((fun y => (f y)^-1) \o shift x) (h *: v) - (f x)^-1)) @ (0 : R)^' --> - (f x) ^-2 *: 'D_v f x. Proof. @@ -1281,23 +1297,22 @@ rewrite -scalerA [_ *: f _]mulVf // [_%:A]mulr1. by rewrite mulrC -scalerA [_ *: f _]mulVf // [_%:A]mulr1. Unshelve. all: by end_near. Qed. -Lemma deriveV (f : V -> R) x v : f x != 0 -> derivable f x v -> +Lemma deriveV f x v : f x != 0 -> derivable f x v -> 'D_v (fun y => (f y)^-1) x = - (f x) ^- 2 *: 'D_v f x. Proof. by move=> fxn0 df; apply: cvg_map_lim (der_inv fxn0 df). Qed. -Lemma derivableV (f : V -> R) (x v : V) : +Lemma derivableV f (x v : V) : f x != 0 -> derivable f x v -> derivable (fun y => (f y)^-1) x v. Proof. move=> df dg; apply/cvg_ex; exists (- (f x) ^- 2 *: 'D_v f x). exact: der_inv. Qed. -End Derive. - -Lemma derive1_cst (R : numFieldType) (V : normedModType R) (k : V) t : - (cst k)^`() t = 0. +Lemma derive1_cst (k : V) t : (cst k)^`() t = 0. Proof. by rewrite derive1E derive_val. Qed. +End Derive_lemmasVR. + Lemma EVT_max (R : realType) (f : R -> R) (a b : R) : (* TODO : Filter not infered *) a <= b -> {within `[a, b], continuous f} -> exists2 c, c \in `[a, b]%R & forall t, t \in `[a, b]%R -> f t <= f c. @@ -1492,7 +1507,7 @@ have gdrvbl x : x \in `]a, b[%R -> derivable g x 1. by move=> /fdrvbl dfx; apply: derivableB => //; exact/derivable1_diffP. have gcont : {within `[a, b], continuous g}. move=> x; apply: continuousD _ ; first by move=>?; exact: fcont. - by apply/continuousN/continuous_subspaceT => ? ?; exact: scalel_continuous. + by apply/continuousN/continuous_subspaceT=> ?; exact: scalel_continuous. have gaegb : g a = g b. rewrite /g -![(_ - _ : _ -> _) _]/(_ - _). apply/eqP; rewrite -subr_eq /= opprK addrAC -addrA -scalerBl. @@ -1569,13 +1584,10 @@ Section is_derive_instances. Variables (R : numFieldType) (V : normedModType R). Lemma derivable_cst (x : V) : derivable (fun=> x) 0 1. -Proof. exact/derivable1_diffP/differentiable_cst. Qed. +Proof. exact/diff_derivable. Qed. Lemma derivable_id (x v : V) : derivable id x v. -Proof. -apply/derivable1P/derivableD; last exact/derivable_cst. -exact/derivable1_diffP/differentiableZl. -Qed. +Proof. exact/diff_derivable. Qed. Global Instance is_derive_id (x v : V) : is_derive x v id v. Proof. @@ -1584,7 +1596,7 @@ by rewrite deriveE// (@diff_lin _ _ _ [linear of idfun]). Qed. Global Instance is_deriveNid (x v : V) : is_derive x v -%R (- v). -Proof. by apply: is_deriveN. Qed. +Proof. exact: is_deriveN. Qed. End is_derive_instances. diff --git a/theories/ereal.v b/theories/ereal.v index 9bcf26b7c..8aec80000 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -1126,20 +1126,16 @@ case: x => /= [x [_/posnumP[d] dP] |[d [dreal dP]] |[d [dreal dP]]]; last 2 firs by rewrite Znat_def floor_ge0 le_maxr lexx orbC. exists N.+1 => // n ltNn; apply: dP. have /le_lt_trans : (d <= Num.max d 0)%R by rewrite le_maxr lexx. - apply; apply: lt_le_trans (lt_succ_floor _) _; rewrite Nfloor. - by rewrite -(@natrD R N 1) ler_nat addn1. + by apply; rewrite (lt_le_trans (lt_succ_floor _))// Nfloor natr1 ler_nat. have /ZnatP [N Nfloor] : floor (Num.max (- d)%R 0%R) \is a Znat. by rewrite Znat_def floor_ge0 le_maxr lexx orbC. exists N.+1 => // n ltNn; apply: dP; rewrite lte_fin ltr_oppl. have /le_lt_trans : (- d <= Num.max (- d) 0)%R by rewrite le_maxr lexx. - apply; apply: lt_le_trans (lt_succ_floor _) _; rewrite Nfloor. - by rewrite -(@natrD R N 1) ler_nat addn1. + by apply; rewrite (lt_le_trans (lt_succ_floor _))// Nfloor natr1 ler_nat. have /ZnatP [N Nfloor] : floor (d%:num^-1) \is a Znat. by rewrite Znat_def floor_ge0. -exists N => // n leNn; have gt0Sn : (0 < n%:R + 1 :> R)%R. - by apply: ltr_spaddr => //; exact/ler0n. -apply: dP; last first. - by rewrite eq_sym addrC -subr_eq subrr eq_sym; apply/invr_neq0/lt0r_neq0. +exists N => // n leNn; apply: dP; last first. + by rewrite eq_sym addrC -subr_eq subrr eq_sym; exact/invr_neq0/lt0r_neq0. rewrite /= opprD addrA subrr distrC subr0 gtr0_norm; last by rewrite invr_gt0. rewrite -[ltLHS]mulr1 ltr_pdivr_mull // -ltr_pdivr_mulr // div1r. by rewrite (lt_le_trans (lt_succ_floor _))// Nfloor ler_add// ler_nat. diff --git a/theories/esum.v b/theories/esum.v index 3e01f55ff..88cebfb0b 100644 --- a/theories/esum.v +++ b/theories/esum.v @@ -35,20 +35,17 @@ Section set_of_fset_in_a_set. Variable (T : choiceType). Implicit Type S : set T. -Definition fsets S : set {fset T} := [set F : {fset T} | [set` F] `<=` S]. +Definition fsets S : set (set T) := [set F | finite_set F /\ F `<=` S]. -Lemma fsets_set0 S : fsets S fset0. Proof. by []. Qed. +Lemma fsets_set0 S : fsets S set0. Proof. by split. Qed. -Lemma fsets_self (F : {fset T}) : fsets [set x | x \in F] F. -Proof. by []. Qed. +Lemma fsets_self (F : set T) : finite_set F -> fsets F F. +Proof. by move=> finF; split. Qed. -Lemma fsetsP S (F : {fset T}) : [set` F] `<=` S <-> fsets S F. -Proof. by []. Qed. - -Lemma fsets0 : fsets set0 = [set fset0]. +Lemma fsets0 : fsets set0 = [set set0]. Proof. rewrite predeqE => A; split => [|->]; last exact: fsets_set0. -by rewrite /fsets /= subset0 => /eqP; rewrite set_fset_eq0 => /eqP. +by rewrite /fsets/= subset0 => -[]. Qed. End set_of_fset_in_a_set. @@ -57,15 +54,15 @@ Section esum. Variables (R : realFieldType) (T : choiceType). Implicit Types (S : set T) (a : T -> \bar R). -Definition esum S a := ereal_sup [set \sum_(x <- A) a x | A in fsets S]. +Definition esum S a := ereal_sup [set \sum_(x \in A) a x | A in fsets S]. Local Notation "\esum_ ( i 'in' P ) A" := (esum P (fun i => A)). Lemma esum_set0 a : \esum_(i in set0) a i = 0. Proof. rewrite /esum fsets0 [X in ereal_sup X](_ : _ = [set 0%E]) ?ereal_sup1//. -rewrite predeqE => x; split; first by move=> [_ /= ->]; rewrite big_seq_fset0. -by move=> -> /=; exists fset0 => //; rewrite big_seq_fset0. +apply/seteqP; split=> [x [_ /= ->]|x]; first by rewrite fsbig_set0. +by move=> -> /=; exists set0 => //; rewrite fsbig_set0. Qed. End esum. @@ -76,61 +73,55 @@ Section esum_realType. Variables (R : realType) (T : choiceType). Implicit Types (a : T -> \bar R). -Lemma esum_ge0 (S : set T) a : (forall x, S x -> 0 <= a x) -> 0 <= \esum_(i in S) a i. +Lemma esum_ge0 (S : set T) a : + (forall x, S x -> 0 <= a x) -> 0 <= \esum_(i in S) a i. Proof. -move=> a0. -by apply: ereal_sup_ub; exists fset0; [exact: fsets_set0|rewrite big_nil]. +move=> a0; apply: ereal_sup_ub. +by exists set0; [exact: fsets_set0|rewrite fsbig_set0]. Qed. -Lemma esum_fset (F : {fset T}) a : (forall i, i \in F -> 0 <= a i) -> - \esum_(i in [set` F]) a i = \sum_(i <- F) a i. +Lemma esum_fset (F : set T) a : finite_set F -> + (forall i, i \in F -> 0 <= a i) -> + \esum_(i in F) a i = \sum_(i \in F) a i. Proof. -move=> f0; apply/eqP; rewrite eq_le; apply/andP; split; last first. +move=> finF f0; apply/eqP; rewrite eq_le; apply/andP; split; last first. by apply ereal_sup_ub; exists F => //; exact: fsets_self. -apply ub_ereal_sup => /= ? -[F' F'F <-]; apply/lee_sum_nneg_subfset. - exact/fsetsP. -by move=> t; rewrite inE => /andP[_ /f0]. +apply ub_ereal_sup => /= ? -[F' [finF' F'F] <-]. +apply/lee_fsum_nneg_subset => //; first exact/subsetP. +by move=> t; rewrite inE/= => /andP[_] /f0. Qed. Lemma esum_set1 t a : 0 <= a t -> \esum_(i in [set t]) a i = a t. Proof. -by move=> ?; rewrite -set_fset1 esum_fset ?big_seq_fset1// => t' /[!inE] /eqP->. -Qed. - -Lemma sum_fset_set (A : set T) a : finite_set A -> - (forall i, A i -> 0 <= a i) -> - \sum_(i <- fset_set A) a i = \esum_(i in A) a i. -Proof. -move=> Afin a0; rewrite -esum_fset => [|i]; rewrite ?fset_setK//. -by rewrite in_fset_set ?inE//; apply: a0. +by move=> ?; rewrite esum_fset// ?fset_set1// ?fsbig_set1// => t' /[!inE] ->. Qed. Lemma fsbig_esum (A : set T) a : finite_set A -> (forall x, 0 <= a x) -> \sum_(x \in A) (a x) = \esum_(x in A) a x. -Proof. by move=> *; rewrite fsbig_finite//= sum_fset_set. Qed. +Proof. by move=> *; rewrite esum_fset. Qed. + End esum_realType. Lemma esum_ge [R : realType] [T : choiceType] (I : set T) (a : T -> \bar R) x : - (exists2 X : {fset T}, fsets I X & x <= \sum_(i <- X) a i) -> + (exists2 X : set T, fsets I X & x <= \sum_(i \in X) a i) -> x <= \esum_(i in I) a i. Proof. by move=> [X IX /le_trans->//]; apply: ereal_sup_ub => /=; exists X. Qed. -Lemma esum0 [R : realFieldType] [I : choiceType] (D : set I) (a : I -> \bar R) : +Lemma esum1 [R : realFieldType] [I : choiceType] (D : set I) (a : I -> \bar R) : (forall i, D i -> a i = 0) -> \esum_(i in D) a i = 0. Proof. move=> a0; rewrite /esum (_ : [set _ | _ in _] = [set 0]) ?ereal_sup1//. -apply/seteqP; split=> x //= => [[X XI] <-|->]. - by rewrite big_seq_cond big1// => i /andP[Xi _]; rewrite a0//; apply: XI. -by exists fset0; rewrite ?big_seq_fset0. +apply/seteqP; split=> x //= => [[X [finX XI]] <-|->]. + by rewrite fsbig1// => i /XI/a0. +by exists set0; rewrite ?fsbig_set0//; exact: fsets_set0. Qed. Lemma le_esum [R : realType] [T : choiceType] (I : set T) (a b : T -> \bar R) : (forall i, I i -> a i <= b i) -> \esum_(i in I) a i <= \esum_(i in I) b i. Proof. -move=> le_ab; rewrite ub_ereal_sup => //= _ [X XI] <-; rewrite esum_ge//. -exists X => //; rewrite big_seq_cond [x in _ <= x]big_seq_cond lee_sum => // i. -by rewrite andbT => /XI /le_ab. +move=> le_ab; rewrite ub_ereal_sup => //= _ [X [finX XI]] <-; rewrite esum_ge//. +by exists X => //; apply: lee_fsum => // t /XI /le_ab. Qed. Lemma eq_esum [R : realType] [T : choiceType] (I : set T) (a b : T -> \bar R) : @@ -143,46 +134,46 @@ Lemma esumD [R : realType] [T : choiceType] (I : set T) (a b : T -> \bar R) : \esum_(i in I) (a i + b i) = \esum_(i in I) a i + \esum_(i in I) b i. Proof. move=> ag0 bg0; apply/eqP; rewrite eq_le; apply/andP; split. - rewrite ub_ereal_sup//= => x [X XI] <-; rewrite big_split/=. + rewrite ub_ereal_sup//= => x [X [finX XI]] <-; rewrite fsbig_split//=. by rewrite lee_add// ereal_sup_ub//=; exists X. wlog : a b ag0 bg0 / \esum_(i in I) a i \isn't a fin_num => [saoo|]; last first. move=> /fin_numPn[->|/[dup] aoo ->]; first by rewrite leNye. rewrite (@le_trans _ _ +oo)//; first by rewrite /adde/=; case: esum. rewrite leye_eq; apply/eqP/eq_infty => y; rewrite esum_ge//. have : y%:E < \esum_(i in I) a i by rewrite aoo// ltey. - move=> /ereal_sup_gt[_ [X XI] <-] /ltW yle; exists X => //=. - rewrite (le_trans yle)// big_split lee_addl// big_seq_cond sume_ge0 => // i. - by rewrite andbT => /XI; apply: bg0. + move=> /ereal_sup_gt[_ [X [finX XI]] <-] /ltW yle; exists X => //=. + rewrite (le_trans yle)// fsbig_split// lee_addl// fsume_ge0// => // i. + by move=> /XI; exact: bg0. case: (boolP (\esum_(i in I) a i \is a fin_num)) => sa; last exact: saoo. case: (boolP (\esum_(i in I) b i \is a fin_num)) => sb; last first. by rewrite addeC (eq_esum (fun _ _ => addeC _ _)) saoo. -rewrite -lee_subr_addr// ub_ereal_sup//= => _ [X XI] <-. -have saX : \sum_(i <- X) a i \is a fin_num. +rewrite -lee_subr_addr// ub_ereal_sup//= => _ [X [finX XI]] <-. +have saX : \sum_(i \in X) a i \is a fin_num. apply: contraTT sa => /fin_numPn[] sa. - suff : \sum_(i <- X) a i >= 0 by rewrite sa. - by rewrite big_seq_cond sume_ge0 => // i; rewrite ?andbT => /XI/ag0. + suff : \sum_(i \in X) a i >= 0 by rewrite sa. + by rewrite fsume_ge0// => i /XI/ag0. apply/fin_numPn; right; apply/eqP; rewrite -leye_eq esum_ge//. by exists X; rewrite // sa. -rewrite lee_subr_addr// addeC -lee_subr_addr// ub_ereal_sup//= => _ [Y YI] <-. -rewrite lee_subr_addr// addeC esum_ge//; exists (X `|` Y)%fset. - by move=> i/=; rewrite inE => /orP[/XI|/YI]. -rewrite big_split/= lee_add//=. - rewrite lee_sum_nneg_subfset//=; first exact/fsubsetP/fsubsetUl. - by move=> x; rewrite !inE/= => /andP[/negPf->]/= => /YI/ag0. -rewrite lee_sum_nneg_subfset//=; first exact/fsubsetP/fsubsetUr. -by move=> x; rewrite !inE/= => /andP[/negPf->]/orP[]// => /XI/bg0. -Qed. - -Lemma esum_mkcond [R : realType] [T : choiceType] (I : set T) (a : T -> \bar R) : +rewrite lee_subr_addr// addeC -lee_subr_addr// ub_ereal_sup//= => _ [Y [finY YI]] <-. +rewrite lee_subr_addr// addeC esum_ge//; exists (X `|` Y). + by split; [rewrite finite_setU|rewrite subUset]. +rewrite fsbig_split ?finite_setU//= lee_add// lee_fsum_nneg_subset//= ?finite_setU//. +- exact/subsetP/subsetUl. +- by move=> x; rewrite !inE in_setU andb_orr andNb/= => /andP[_] /[!inE] /YI/ag0. +- exact/subsetP/subsetUr. +- by move=> x; rewrite !inE in_setU andb_orr andNb/= orbF => /andP[_] /[!inE] /XI/bg0. +Qed. + +Lemma esum_mkcond [R : realType] [T : choiceType] (I : set T) + (a : T -> \bar R) : \esum_(i in I) a i = \esum_(i in [set: T]) if i \in I then a i else 0. Proof. -apply/eqP; rewrite eq_le !ub_ereal_sup//= => _ [X XI] <-; rewrite -?big_mkcond//=. - rewrite big_fset_condE/=; set Y := [fset _ | _ in X & _]%fset. - rewrite ereal_sup_ub//; exists Y => //= i /=. - by rewrite 2!inE/= => /andP[_]; rewrite inE. -rewrite ereal_sup_ub//; exists X => //; rewrite -big_mkcond/=. -rewrite big_seq_cond [RHS]big_seq_cond; apply: eq_bigl => i. -by case: (boolP (i \in X)) => //= /XI Ii; apply/mem_set. +apply/eqP; rewrite eq_le !ub_ereal_sup//= => _ [X [finX XI]] <-. + rewrite -big_mkcond/= big_fset_condE/=; set Y := [fset _ | _ in _ & _]%fset. + rewrite ereal_sup_ub//=; exists [set` Y]; last by rewrite fsbig_finite// set_fsetK. + by split => // i/=; rewrite !inE/= => /andP[_]; rewrite inE. +rewrite ereal_sup_ub//; exists X => //; apply: eq_fsbigr => x; rewrite inE => Xx. +by rewrite ifT// inE; exact: XI. Qed. Lemma esum_mkcondr [R : realType] [T : choiceType] (I J : set T) (a : T -> \bar R) : @@ -217,7 +208,7 @@ Lemma esum_sum [R : realType] [T1 T2 : choiceType] \sum_(j <- r | P j) \esum_(i in I) a i j. Proof. move=> a_ge0; elim: r => [|j r IHr]; rewrite ?(big_nil, big_cons)// -?IHr. - by rewrite esum0// => i; rewrite big_nil. + by rewrite esum1// => i; rewrite big_nil. case: (boolP (P j)) => Pj; last first. by apply: eq_esum => i Ii; rewrite big_cons (negPf Pj). have aj_ge0 i : I i -> a i j >= 0 by move=> ?; apply: a_ge0. @@ -231,39 +222,47 @@ Lemma esum_esum [R : realType] [T1 T2 : choiceType] \esum_(i in I) \esum_(j in J i) a i j = \esum_(k in I `*`` J) a k.1 k.2. Proof. move=> a_ge0; apply/eqP; rewrite eq_le; apply/andP; split. - apply: ub_ereal_sup => /= _ [X IX] <-. - under eq_bigr do rewrite esum_mkcond. - rewrite -esum_sum; last by move=> i j _ _; case: ifP. + apply: ub_ereal_sup => /= _ [X [finX XI]] <-. + under eq_fsbigr do rewrite esum_mkcond. + rewrite fsbig_finite//= -esum_sum; last by move=> i j _ _; case: ifP. under eq_esum do rewrite -big_mkcond/=. - apply: ub_ereal_sup => /= _ [Y _ <-]; apply: ereal_sup_ub => /=. - exists [fset z | z in X `*` Y & z.2 \in J z.1]%fset => //=. - move=> z/=; rewrite !inE/= -andbA => /and3P[Xz1 Yz2 zJ]. - by split; [exact: IX | rewrite inE in zJ]. - rewrite (exchange_big_dep xpredT)//= pair_big_dep_cond/=. - apply: eq_fbigl => -[/= k1 k2]; rewrite !inE -andbA. - apply/idP/imfset2P => /= [/and3P[kX kY kJ]|]. - exists k1; rewrite ?(andbT, inE)//=. - by exists k2; rewrite ?(andbT, inE)//= kY kJ. - by move=> [{}k1 + [{}k2 + [-> ->]]]; rewrite !inE andbT => -> /andP[-> ->]. -apply: ub_ereal_sup => _ /= [X/= XIJ] <-; apply: esum_ge. -pose X1 := [fset x.1 | x in X]%fset. -pose X2 := [fset x.2 | x in X]%fset. -exists X1; first by move=> x/= /imfsetP[z /= zX ->]; have [] := XIJ z. -apply: (@le_trans _ _ (\sum_(i <- X1) \sum_(j <- X2 | j \in J i) a i j)). + apply: ub_ereal_sup => /= _ [Y [finY _] <-]; apply: ereal_sup_ub => /=. + set XYJ := [set z | z \in X `*` Y /\ z.2 \in J z.1]. + have ? : finite_set XYJ. + apply: sub_finite_set (finite_setM finX finY) => z/=. + by rewrite /XYJ/= in_setM => -[/andP[] /[!inE]]. + exists XYJ => /=; first by split => //= z; rewrite /XYJ/= 2!inE=> -[[/XI]]. + rewrite [in RHS]fsbig_finite//= (exchange_big_dep xpredT)// pair_big_dep_cond. + rewrite fsbig_finite//; apply: eq_fbigl => -[/= x y]; rewrite in_fset_set//. + apply/idP/imfset2P. + rewrite /XYJ !inE/= !inE/= -andA => -[Xx [Yy Jxy]]. + exists x; first by rewrite !inE in_fset_set// mem_set. + by exists y => //; rewrite !inE mem_set// in_fset_set// mem_set. + move=> [t1]; rewrite !inE andbT/= in_fset_set// inE => Xt1. + by move=> [t2]; rewrite !inE in_fset_set /XYJ//= =>/andP[/[!inE] ? ?] [-> ->]. +apply: ub_ereal_sup => _ /= [X/= [finX XIJ]] <-; apply: esum_ge. +exists X.`1; first by split=> [|x [y /XIJ[]//]]; exact: finite_set_fst. +apply: (@le_trans _ _ + (\sum_(i <- fset_set X.`1) \sum_(j <- fset_set X.`2 | j \in J i) a i j)). rewrite pair_big_dep_cond//=; set Y := Imfset.imfset2 _ _ _ _. rewrite [leRHS](big_fsetID _ (mem X))/=. - rewrite (_ : [fset x | x in Y & x \in X] = Y `&` X)%fset; last first. - by apply/fsetP => x; rewrite 2!inE. - rewrite (fsetIidPr _); first by rewrite lee_addl// sume_ge0. - apply/fsubsetP => -[i j] Xij; apply/imfset2P. - exists i => //=; rewrite ?inE ?andbT//=. - by apply/imfsetP; exists (i, j). - exists j => //; rewrite !inE/=; have /XIJ[/= _ Jij] := Xij. - by apply/andP; split; rewrite ?inE//; apply/imfsetP; exists (i, j). -rewrite big_mkcond [leRHS]big_mkcond. -apply: lee_sum => i Xi; rewrite ereal_sup_ub => //=. -exists [fset j in X2 | j \in J i]%fset; last by rewrite -big_fset_condE. -by move=> j/=; rewrite !inE => /andP[_]; rewrite inE. + rewrite (_ : [fset x | x in Y & x \in X] = Y `&` fset_set X)%fset; last first. + by apply/fsetP => x; rewrite 2!inE/= in_fset_set. + rewrite (fsetIidPr _); first by rewrite fsbig_finite// lee_addl// sume_ge0. + apply/fsubsetP => -[i j]; rewrite in_fset_set// inE => Xij; apply/imfset2P. + exists i => /=. + rewrite !inE/= in_fset_set//; last exact: finite_set_fst. + by rewrite andbT mem_set//; move/fst_set_fst : Xij. + exists j => //; rewrite !inE/= in_fset_set; last exact: finite_set_snd. + rewrite mem_set/=; last by move/snd_set_snd : Xij. + by rewrite mem_set//; move/XIJ : Xij => []. +rewrite -fsbig_finite; last exact: finite_set_fst. +apply lee_fsum=> [|i Xi]; first exact: finite_set_fst. +rewrite ereal_sup_ub => //=; have ? : finite_set (X.`2 `&` J i). + by apply: finite_setI; left; exact: finite_set_snd. +exists (X.`2 `&` J i) => //. +rewrite [in RHS]big_fset_condE/= fsbig_finite//; apply eq_fbigl => j. +by rewrite in_fset_set// !inE/= in_setI in_fset_set//; exact: finite_set_snd. Qed. Lemma lee_sum_fset_nat (R : realDomainType) @@ -301,13 +300,14 @@ Lemma nneseries_esum (R : realType) (a : nat -> \bar R) (P : pred nat) : Proof. move=> a0; apply/eqP; rewrite eq_le; apply/andP; split. apply: (ereal_lim_le (is_cvg_nneseries_cond a0)); apply: nearW => n. - apply: ereal_sup_ub => /=; exists [fset val i | i in 'I_n & P i]%fset. + apply: ereal_sup_ub => /=; exists [set` [fset val i | i in 'I_n & P i]%fset]. + split; first exact: finite_fset. by move=> /= k /imfsetP[/= i]; rewrite inE => + ->. - rewrite big_imfset/=; last by move=> ? ? ? ? /val_inj. + rewrite fsbig_finite//= set_fsetK big_imfset/=; last by move=> ? ? ? ? /val_inj. by rewrite big_filter big_enum_cond/= big_mkord. -apply: ub_ereal_sup => _ [/= F /fsetsP PF <-]. -rewrite -(big_rmcond_in P)/=; last by move=> i /PF ->. -by apply: lee_sum_fset_lim. +apply: ub_ereal_sup => _ [/= F [finF PF] <-]. +rewrite fsbig_finite//= -(big_rmcond_in P)/=; first exact: lee_sum_fset_lim. +by move=> k; rewrite in_fset_set// inE => /PF ->. Qed. Lemma reindex_esum (R : realType) (T T' : choiceType) @@ -325,16 +325,18 @@ gen have le_esum : T T' a P Q e / apply/eqP; rewrite eq_le le_esum//=. rewrite [leRHS](_ : _ = \esum_(j in Q) a (e (e^-1%FUN j))); last first. by apply: eq_esum => i Qi; rewrite invK ?inE. - by rewrite le_esum => //= i Qi; rewrite a_ge0//; apply: funS. -rewrite ub_ereal_sup => //= _ [X XQ <-]; rewrite ereal_sup_ub => //=. -exists (e^-1 @` X)%fset; first by move=> _ /imfsetP[t' /= /XQ Qt' ->]; apply: funS. -rewrite big_imfset => //=; last first. - by move=> x y /XQ Qx /XQ Qy /(congr1 e); rewrite !invK ?inE. -by apply: eq_big_seq => i /XQ Qi; rewrite invK ?inE. + by rewrite le_esum => //= i Qi; rewrite a_ge0//; exact: funS. +rewrite ub_ereal_sup => //= _ [X [finX XQ] <-]; rewrite ereal_sup_ub => //=. +exists [set` (e^-1 @` (fset_set X))%fset]. + split=> [|t /= /imfsetP[t'/=]]; first exact: finite_fset. + by rewrite in_fset_set// inE => /XQ Qt' ->; exact: funS. +rewrite fsbig_finite//= set_fsetK big_imfset => //=; last first. + move=> x y; rewrite !in_fset_set// !inE => /XQ ? /XQ ? /(congr1 e). + by rewrite !invK ?inE. +by rewrite -fsbig_finite//; apply eq_fsbigr=> x /[!inE]/XQ ?; rewrite invK ?inE. Qed. Arguments reindex_esum {R T T'} P Q e a. - Section nneseries_interchange. Local Open Scope ereal_scope. @@ -600,7 +602,7 @@ Let ge0_esum_posneg D f : (forall x, D x -> 0 <= f x) -> esum_posneg D f = \esum_(x in D) f x. Proof. move=> Sa; rewrite /esum_posneg [X in _ - X](_ : _ = 0) ?sube0; last first. - by rewrite esum0// => x Sx; rewrite -[LHS]/(f^\- x) (ge0_funenegE Sa)// inE. + by rewrite esum1// => x Sx; rewrite -[LHS]/(f^\- x) (ge0_funenegE Sa)// inE. by apply: eq_esum => t St; apply/max_idPl; exact: Sa. Qed. diff --git a/theories/exp.v b/theories/exp.v index 0731429b4..3bfbcde94 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -132,9 +132,9 @@ rewrite mulrBr mulrC divfK //. case: n => [|n]. by rewrite !expr0 !(mul0r, mulr0, subr0, subrr, big_geq). rewrite subrXX addrK -mulrBr; congr (_ * _). -rewrite -(big_mkord xpredT (fun i : nat => (h + z) ^+ (n - i) * z ^+ i)). +rewrite -(big_mkord xpredT (fun i => (h + z) ^+ (n - i) * z ^+ i)). rewrite big_nat_recr //= subnn expr0 -addrA -mulrBl. -rewrite -add1n natrD opprD addrA subrr sub0r mulNr. +rewrite -nat1r opprD addrA subrr sub0r mulNr. rewrite mulr_natl -[in X in _ *+ X](subn0 n) -sumr_const_nat -sumrB. rewrite pseries_diffs_P1 mulr_sumr !big_mkord; apply: eq_bigr => i _. rewrite mulrCA; congr (_ * _). @@ -394,7 +394,7 @@ Qed. Lemma expRMm n x : expR (n%:R * x) = expR x ^+ n. Proof. elim: n x => [x|n IH x] /=; first by rewrite mul0r expr0 expR0. -by rewrite exprS -add1n natrD mulrDl mul1r expRD IH. +by rewrite exprS -nat1r mulrDl mul1r expRD IH. Qed. Lemma expR_gt1 x: (1 < expR x) = (0 < x). @@ -442,7 +442,7 @@ Proof. move=> x_ge1; have x_ge0 : 0 <= x by apply: le_trans x_ge1. have [x1 x1Ix| |x1 _ /eqP] := @IVT _ (fun y => expR y - x) _ _ 0 x_ge0. - apply: continuousB => // y1; last exact: cst_continuous. - by apply/continuous_subspaceT=> ? _; exact: continuous_expR. + by apply/continuous_subspaceT=> ?; exact: continuous_expR. - rewrite expR0; have [_| |] := ltrgtP (1- x) (expR x - x). + by rewrite subr_le0 x_ge1 subr_ge0 (le_trans _ (expR_ge1Dx _)) ?ler_addr. + by rewrite ltr_add2r expR_lt1 ltNge x_ge0. @@ -606,7 +606,7 @@ Qed. Lemma exp_fun_mulrn a n : 0 < a -> exp_fun a n%:R = a ^+ n. Proof. move=> a0; elim: n => [|n ih]; first by rewrite mulr0n expr0 exp_funr0. -by rewrite -addn1 natrD exp_funD // exprD ih exp_funr1. +by rewrite -natr1 exprSr exp_funD// ih exp_funr1. Qed. End ExpFun. diff --git a/theories/fsbigop.v b/theories/fsbigop.v index c1f0ec728..e812a1376 100644 --- a/theories/fsbigop.v +++ b/theories/fsbigop.v @@ -425,6 +425,25 @@ Arguments reindex_fsbigT {R idx op I J} _ _. #[deprecated(note="use reindex_fsbigT instead")] Notation reindex_inside_setT := reindex_fsbigT. +Lemma lee_fsum_nneg_subset {R : realDomainType} [T : choiceType] [A B : set T] + [f : T -> \bar R] : finite_set A -> finite_set B -> + {subset A <= B} -> {in [predD B & A], forall t : T, 0 <= f t}%E -> + (\sum_(t \in A) f t <= \sum_(t \in B) f t)%E. +Proof. +move=> finA finB AB f0; rewrite !fsbig_finite//=; apply: lee_sum_nneg_subfset. + by apply/fsubsetP; rewrite -fset_set_sub//; apply/subsetP. +by move=> t; rewrite !inE !in_fset_set// => /f0. +Qed. + +Lemma lee_fsum [R : realDomainType] [T : choiceType] (I : set T) + (a b : T -> \bar R) : finite_set I -> + (forall i, I i -> a i <= b i)%E -> (\sum_(i \in I) a i <= \sum_(i \in I) b i)%E. +Proof. +move=> finI ab. +rewrite !fsbig_finite// big_seq [in leRHS]big_seq lee_sum //. +by move=> i; rewrite in_fset_set// inE; exact: ab. +Qed. + Lemma ge0_mule_fsumr (T : choiceType) (R : realDomainType) (x : \bar R) (F : T -> \bar R) (P : set T) : (forall i : T, 0 <= F i)%E -> (x * (\sum_(i \in P) F i) = \sum_(i \in P) x * F i)%E. diff --git a/theories/kernel.v b/theories/kernel.v new file mode 100644 index 000000000..d84168a0d --- /dev/null +++ b/theories/kernel.v @@ -0,0 +1,1432 @@ +(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. +From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +Require Import mathcomp_extra boolp classical_sets signed functions cardinality. +Require Import reals ereal topology normedtype sequences esum measure. +Require Import lebesgue_measure fsbigop numfun lebesgue_integral. + +(******************************************************************************) +(* Kernels *) +(* *) +(* This file provides a formation of kernels and extends the theory of *) +(* measures with, e.g., Tonelli-Fubini's theorem for s-finite measures. *) +(* The main result is the fact that s-finite kernels are stable by *) +(* composition. *) +(* *) +(* finite_measure mu == the measure mu is finite *) +(* sfinite_measure mu == the measure mu is s-finite *) +(* R.-ker X ~> Y == kernel *) +(* kseries == countable sum of kernels *) +(* R.-sfker X ~> Y == s-finite kernel *) +(* R.-fker X ~> Y == finite kernel *) +(* R.-spker X ~> Y == subprobability kernel *) +(* R.-pker X ~> Y == probability kernel *) +(* kprobability m == kernel defined by a probability measure *) +(* kdirac mf == kernel defined by a measurable function *) +(* kadd k1 k2 == lifting of the addition of measures to kernels *) +(* mnormalize f == normalization of a kernel to a probability *) +(* l \; k == composition of kernels *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import numFieldTopology.Exports. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. +Local Open Scope ereal_scope. + +(* PR 516 in progress *) +HB.mixin Record isProbability (d : measure_display) (T : measurableType d) + (R : realType) (P : set T -> \bar R) of isMeasure d R T P := + { probability_setT : P setT = 1%E }. + +#[short(type=probability)] +HB.structure Definition Probability (d : measure_display) (T : measurableType d) + (R : realType) := + {P of isProbability d T R P & isMeasure d R T P }. + +Section probability_lemmas. +Variables (d : _) (T : measurableType d) (R : realType) (P : probability T R). + +Lemma probability_le1 (A : set T) : measurable A -> (P A <= 1)%E. +Proof. +move=> mA; rewrite -(@probability_setT _ _ _ P). +by apply: le_measure => //; rewrite ?in_setE. +Qed. + +End probability_lemmas. +(* /PR 516 in progress *) + +(* TODO: PR*) +Lemma setT0 (T : pointedType) : setT != set0 :> set T. +Proof. by apply/eqP => /seteqP[] /(_ point) /(_ Logic.I). Qed. + +Lemma set_unit (A : set unit) : A = set0 \/ A = setT. +Proof. +have [->|/set0P[[] Att]] := eqVneq A set0; [by left|right]. +by apply/seteqP; split => [|] []. +Qed. + +Lemma set_boolE (B : set bool) : [\/ B == [set true], B == [set false], B == set0 | B == setT]. +Proof. +have [Bt|Bt] := boolP (true \in B). + have [Bf|Bf] := boolP (false \in B). + have -> : B = setT. + by apply/seteqP; split => // -[] _; [rewrite inE in Bt| rewrite inE in Bf]. + by apply/or4P; rewrite eqxx/= !orbT. + have -> : B = [set true]. + apply/seteqP; split => -[]//=. + by rewrite notin_set in Bf. + by rewrite inE in Bt. + by apply/or4P; rewrite eqxx. +have [Bf|Bf] := boolP (false \in B). + have -> : B = [set false]. + apply/seteqP; split => -[]//=. + by rewrite notin_set in Bt. + by rewrite inE in Bf. + by apply/or4P; rewrite eqxx/= orbT. +have -> : B = set0. + apply/seteqP; split => -[]//=. + by rewrite notin_set in Bt. + by rewrite notin_set in Bf. +by apply/or4P; rewrite eqxx/= !orbT. +Qed. + +Lemma xsection_preimage_snd (X Y Z : Type) (f : Y -> Z) (A : set Z) (x : X) : + xsection ((f \o snd) @^-1` A) x = f @^-1` A. +Proof. by apply/seteqP; split; move=> y/=; rewrite /xsection/= inE. Qed. + +Canonical unit_pointedType := PointedType unit tt. + +Section discrete_measurable_unit. + +Definition discrete_measurable_unit : set (set unit) := [set: set unit]. + +Let discrete_measurable0 : discrete_measurable_unit set0. Proof. by []. Qed. + +Let discrete_measurableC X : + discrete_measurable_unit X -> discrete_measurable_unit (~` X). +Proof. by []. Qed. + +Let discrete_measurableU (F : (set unit)^nat) : + (forall i, discrete_measurable_unit (F i)) -> + discrete_measurable_unit (\bigcup_i F i). +Proof. by []. Qed. + +HB.instance Definition _ := @isMeasurable.Build default_measure_display unit + (Pointed.class _) discrete_measurable_unit discrete_measurable0 + discrete_measurableC discrete_measurableU. + +End discrete_measurable_unit. + +Section discrete_measurable_bool. + +Definition discrete_measurable_bool : set (set bool) := [set: set bool]. + +Let discrete_measurable0 : discrete_measurable_bool set0. Proof. by []. Qed. + +Let discrete_measurableC X : + discrete_measurable_bool X -> discrete_measurable_bool (~` X). +Proof. by []. Qed. + +Let discrete_measurableU (F : (set bool)^nat) : + (forall i, discrete_measurable_bool (F i)) -> + discrete_measurable_bool (\bigcup_i F i). +Proof. by []. Qed. + +HB.instance Definition _ := @isMeasurable.Build default_measure_display bool + (Pointed.class _) discrete_measurable_bool discrete_measurable0 + discrete_measurableC discrete_measurableU. + +End discrete_measurable_bool. + +Lemma measurable_curry (T1 T2 : Type) (d : _) (T : semiRingOfSetsType d) + (G : T1 * T2 -> set T) (x : T1 * T2) : + measurable (G x) <-> measurable (curry G x.1 x.2). +Proof. by case: x. Qed. + +Lemma emeasurable_itv (R : realType) (i : nat) : + measurable (`[(i%:R)%:E, (i.+1%:R)%:E[%classic : set \bar R). +Proof. +rewrite -[X in measurable X]setCK. +apply: measurableC. +rewrite set_interval.setCitv /=. +apply: measurableU. + exact: emeasurable_itv_ninfty_bnd. +exact: emeasurable_itv_bnd_pinfty. +Qed. + +Lemma measurable_fun_fst (d1 d2 : _) (T1 : measurableType d1) + (T2 : measurableType d2) : measurable_fun setT (@fst T1 T2). +Proof. +have := @measurable_fun_id _ [the measurableType _ of (T1 * T2)%type] setT. +by move=> /prod_measurable_funP[]. +Qed. + +Lemma measurable_fun_snd (d1 d2 : _) (T1 : measurableType d1) + (T2 : measurableType d2) : measurable_fun setT (@snd T1 T2). +Proof. +have := @measurable_fun_id _ [the measurableType _ of (T1 * T2)%type] setT. +by move=> /prod_measurable_funP[]. +Qed. + +Definition swap (T1 T2 : Type) (x : T1 * T2) := (x.2, x.1). + +Lemma measurable_fun_swap d d' (X : measurableType d) (Y : measurableType d') : + measurable_fun [set: X * Y] (@swap X Y). +Proof. +by apply/prod_measurable_funP => /=; split; + [exact: measurable_fun_snd|exact: measurable_fun_fst]. +Qed. + +Section measurable_fun_pair. +Variables (d d2 d3 : _) (X : measurableType d) (Y : measurableType d2) + (Z : measurableType d3). + +Lemma measurable_fun_pair (f : X -> Y) (g : X -> Z) : + measurable_fun setT f -> measurable_fun setT g -> + measurable_fun setT (fun x => (f x, g x)). +Proof. by move=> mf mg; apply/prod_measurable_funP. Qed. + +End measurable_fun_pair. + +Section measurable_fun_comp. +Variables (d1 d2 d3 : measure_display). +Variables (T1 : measurableType d1). +Variables (T2 : measurableType d2). +Variables (T3 : measurableType d3). + +(* NB: this generalizes MathComp-Analysis' measurable_fun_comp *) +Lemma measurable_fun_comp' F (f : T2 -> T3) E (g : T1 -> T2) : + measurable F -> + g @` E `<=` F -> + measurable_fun F f -> measurable_fun E g -> measurable_fun E (f \o g). +Proof. +move=> mF FgE mf mg /= mE A mA. +rewrite comp_preimage. +rewrite [X in measurable X](_ : _ = E `&` g @^-1` (F `&` f @^-1` A)); last first. + apply/seteqP; split=> [|? [?] []//]. + by move=> x/= [Ex Afgx]; split => //; split => //; exact: FgE. +by apply/mg => //; exact: mf. +Qed. + +End measurable_fun_comp. + +Lemma measurable_fun_if (d d' : _) (X : measurableType d) + (Y : measurableType d') (x y : X -> Y) D (md : measurable D) + (f : X -> bool) (mf : measurable_fun setT f) : + measurable_fun (D `&` (f @^-1` [set true])) x -> + measurable_fun (D `&` (f @^-1` [set false])) y -> + measurable_fun D (fun t => if f t then x t else y t). +Proof. +move=> mx my /= _ B mB. +have mDf : measurable (D `&` [set b | f b]). + apply: measurableI => //. + rewrite [X in measurable X](_ : _ = f @^-1` [set true])//. + by have := mf measurableT [set true]; rewrite setTI; exact. +have := mx mDf _ mB. +have mDNf : measurable (D `&` f @^-1` [set false]). + apply: measurableI => //. + by have := mf measurableT [set false]; rewrite setTI; exact. +have := my mDNf _ mB. +move=> yB xB. +rewrite (_ : _ @^-1` B = + ((f @^-1` [set true]) `&` (x @^-1` B) `&` (f @^-1` [set true])) `|` + ((f @^-1` [set false]) `&` (y @^-1` B) `&` (f @^-1` [set false]))); last first. + apply/seteqP; split=> [t /=| t]. + by case: ifPn => ft; [left|right]. + by move=> /= [|]; case: ifPn => ft; case=> -[]. +rewrite setIUr; apply: measurableU. +- rewrite -(setIid D) -(setIA D) setICA setIA. + by apply: measurableI => //; rewrite setIA. +- rewrite -(setIid D) -(setIA D) setICA setIA. + by apply: measurableI => //; rewrite setIA. +Qed. + +Lemma measurable_fun_ifT (d d' : _) (X : measurableType d) + (Y : measurableType d') (x y : X -> Y) (f : X -> bool) + (mf : measurable_fun setT f) : + measurable_fun setT x -> measurable_fun setT y -> + measurable_fun setT (fun t => if f t then x t else y t). +Proof. +by move=> mx my; apply: measurable_fun_if => //; + [exact: measurable_funS mx|exact: measurable_funS my]. +Qed. + +Lemma measurable_fun_if_pair (d d' : _) (X : measurableType d) + (Y : measurableType d') (x y : X -> Y) : + measurable_fun setT x -> measurable_fun setT y -> + measurable_fun setT (fun tb => if tb.2 then x tb.1 else y tb.1). +Proof. +move=> mx my. +have {}mx : measurable_fun [set: X * bool] (x \o fst). + by apply: measurable_fun_comp => //; exact: measurable_fun_fst. +have {}my : measurable_fun [set: X * bool] (y \o fst). + by apply: measurable_fun_comp => //; exact: measurable_fun_fst. +by apply: measurable_fun_ifT => //=; exact: measurable_fun_snd. +Qed. + +Lemma measurable_fun_opp (R : realType) : measurable_fun [set: R] -%R. +Proof. +apply: continuous_measurable_fun. +by have := (@opp_continuous R [the normedModType R of R^o]). +Qed. + +Lemma integral_eq0 d (T : measurableType d) (R : realType) + (mu : {measure set T -> \bar R}) (D : set T) f : + (forall x, D x -> f x = 0) -> \int[mu]_(x in D) f x = 0. +Proof. +move=> f0; under eq_integral. + by move=> x /[1!inE] /f0 ->; over. +by rewrite integral0. +Qed. + +Lemma dirac0 d (T : measurableType d) (R : realFieldType) (a : T) : + \d_a set0 = 0%E :> \bar R. +Proof. by rewrite /dirac indic0. Qed. + +Lemma diracT d (T : measurableType d) (R : realFieldType) (a : T) : + \d_a setT = 1%E :> \bar R. +Proof. by rewrite /dirac indicT. Qed. + +Section fubini_tonelli. +Local Open Scope ereal_scope. +Variables (d1 d2 : measure_display). +Variables (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). +Variables (m1 : {measure set T1 -> \bar R}) (m2 : {measure set T2 -> \bar R}). +Hypotheses (sm1 : sigma_finite setT m1) (sm2 : sigma_finite setT m2). +Variables (f : T1 * T2 -> \bar R) (f0 : forall xy, 0 <= f xy). +Variables (mf : measurable_fun setT f). + +Lemma fubini_tonelli : + \int[m1]_x \int[m2]_y f (x, y) = \int[m2]_y \int[m1]_x f (x, y). +Proof. by rewrite -fubini_tonelli1// fubini_tonelli2. Qed. + +End fubini_tonelli. +(* /TODO: PR *) + +Definition finite_measure d (T : measurableType d) (R : realType) + (mu : set T -> \bar R) := + mu setT < +oo. + +Definition sfinite_measure d (T : measurableType d) (R : realType) + (mu : set T -> \bar R) := + exists2 mu_ : {measure set T -> \bar R}^nat, + forall n, finite_measure (mu_ n) & forall U, measurable U -> mu U = mseries mu_ 0 U. + +Lemma finite_measure_sigma_finite d (T : measurableType d) (R : realType) + (mu : {measure set T -> \bar R}) : + finite_measure mu -> sigma_finite setT mu. +Proof. +exists (fun i => if i \in [set 0%N] then setT else set0). + by rewrite -bigcup_mkcondr setTI bigcup_const//; exists 0%N. +move=> n; split; first by case: ifPn. +by case: ifPn => // _; rewrite ?measure0//; exact: finite_measure. +Qed. + +Section sfinite_fubini. +Variables (d d' : _) (X : measurableType d) (Y : measurableType d') (R : realType). +Variables (m1 : {measure set X -> \bar R}) (sfm1 : sfinite_measure m1). +Variables (m2 : {measure set Y -> \bar R}) (sfm2 : sfinite_measure m2). +Variables (f : X * Y -> \bar R) (f0 : forall xy, 0 <= f xy). +Variable (mf : measurable_fun setT f). + +Lemma sfinite_fubini : + \int[m1]_x \int[m2]_y f (x, y) = \int[m2]_y \int[m1]_x f (x, y). +Proof. +have [m1_ fm1 m1E] := sfm1. +have [m2_ fm2 m2E] := sfm2. +rewrite [LHS](eq_measure_integral [the measure _ _ of mseries m1_ 0]); last first. + by move=> A mA _; rewrite m1E. +transitivity (\int[[the measure _ _ of mseries m1_ 0]]_x + \int[[the measure _ _ of mseries m2_ 0]]_y f (x, y)). + by apply eq_integral => x _; apply: eq_measure_integral => U mA _; rewrite m2E. +transitivity (\sum_(n t _; exact: integral_ge0. + rewrite [X in measurable_fun _ X](_ : _ = + fun x => \sum_(n x. + by rewrite ge0_integral_measure_series//; exact/measurable_fun_prod1. + apply: ge0_emeasurable_fun_sum; first by move=> k x; exact: integral_ge0. + move=> k; apply: measurable_fun_fubini_tonelli_F => //=. + exact: finite_measure_sigma_finite. + apply: eq_nneseries => n _; apply eq_integral => x _. + by rewrite ge0_integral_measure_series//; exact/measurable_fun_prod1. +transitivity (\sum_(n n _. + rewrite integral_sum//. + move=> m; apply: measurable_fun_fubini_tonelli_F => //=. + exact: finite_measure_sigma_finite. + by move=> m x _; exact: integral_ge0. +transitivity (\sum_(n n _; apply eq_nneseries => m _. + by rewrite fubini_tonelli//; exact: finite_measure_sigma_finite. +transitivity (\sum_(n n _ /=. rewrite ge0_integral_measure_series//. + by move=> y _; exact: integral_ge0. + apply: measurable_fun_fubini_tonelli_G => //=. + by apply: finite_measure_sigma_finite; exact: fm1. +transitivity (\int[[the measure _ _ of mseries m2_ 0]]_y \sum_(n n; apply: measurable_fun_fubini_tonelli_G => //=. + by apply: finite_measure_sigma_finite; exact: fm1. + by move=> n y _; exact: integral_ge0. +transitivity (\int[[the measure _ _ of mseries m2_ 0]]_y + \int[[the measure _ _ of mseries m1_ 0]]_x f (x, y)). + apply eq_integral => y _. + by rewrite ge0_integral_measure_series//; exact/measurable_fun_prod2. +transitivity (\int[m2]_y \int[mseries m1_ 0]_x f (x, y)). + by apply eq_measure_integral => A mA _ /=; rewrite m2E. +by apply eq_integral => y _; apply eq_measure_integral => A mA _ /=; rewrite m1E. +Qed. + +End sfinite_fubini. +Arguments sfinite_fubini {d d' X Y R m1} _ {m2} _ f. + +Reserved Notation "R .-ker X ~> Y" (at level 42, format "R .-ker X ~> Y"). +Reserved Notation "R .-sfker X ~> Y" (at level 42, format "R .-sfker X ~> Y"). +Reserved Notation "R .-fker X ~> Y" (at level 42, format "R .-fker X ~> Y"). +Reserved Notation "R .-spker X ~> Y" (at level 42, format "R .-spker X ~> Y"). +Reserved Notation "R .-pker X ~> Y" (at level 42, format "R .-pker X ~> Y"). + +HB.mixin Record isKernel d d' (X : measurableType d) (Y : measurableType d') + (R : realType) (k : X -> {measure set Y -> \bar R}) := + { measurable_kernel : forall U, measurable U -> measurable_fun setT (k ^~ U) }. + +#[short(type=kernel)] +HB.structure Definition Kernel + d d' (X : measurableType d) (Y : measurableType d') (R : realType) := + { k & isKernel _ _ X Y R k }. +Notation "R .-ker X ~> Y" := (kernel X Y R). + +Arguments measurable_kernel {_ _ _ _ _} _. + +Section kseries. +Variables (d d' : measure_display) (R : realType). +Variables (X : measurableType d) (Y : measurableType d'). +Variable k : (R.-ker X ~> Y)^nat. + +Definition kseries : X -> {measure set Y -> \bar R} := + fun x => [the measure _ _ of mseries (k ^~ x) 0]. + +Lemma measurable_fun_kseries (U : set Y) : + measurable U -> + measurable_fun setT (kseries ^~ U). +Proof. +move=> mU. +by apply: ge0_emeasurable_fun_sum => // n; exact/measurable_kernel. +Qed. + +HB.instance Definition _ := + isKernel.Build _ _ _ _ _ kseries measurable_fun_kseries. + +End kseries. + +Lemma integral_kseries + (d d' : _) (X : measurableType d) (Y : measurableType d') + (R : realType) (k : (R.-ker X ~> Y)^nat) (f : Y -> \bar R) x : + (forall y, 0 <= f y) -> + measurable_fun setT f -> + \int[kseries k x]_y (f y) = \sum_(i f0 mf; rewrite /kseries/= ge0_integral_measure_series. +Qed. + +Section measure_fam_uub. +Variables (d d' : _) (X : measurableType d) (Y : measurableType d'). +Variables (R : numFieldType) (k : X -> {measure set Y -> \bar R}). + +Definition measure_fam_uub := exists r, forall x, k x [set: Y] < r%:E. + +Lemma measure_fam_uubP : measure_fam_uub <-> + exists r : {posnum R}, forall x, k x [set: Y] < r%:num%:E. +Proof. +split => [|] [r kr]; last by exists r%:num. +suff r_gt0 : (0 < r)%R by exists (PosNum r_gt0). +by rewrite -lte_fin; apply: (le_lt_trans _ (kr point)). +Qed. + +End measure_fam_uub. + +HB.mixin Record Kernel_isSFinite_subdef + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) (k : X -> {measure set Y -> \bar R}) := { + sfinite_subdef : exists2 s : (R.-ker X ~> Y)^nat, + forall n, measure_fam_uub (s n) & + forall x U, measurable U -> k x U = kseries s x U }. + +#[short(type=sfinite_kernel)] +HB.structure Definition SFiniteKernel + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) := + {k of Kernel_isSFinite_subdef _ _ X Y R k & isKernel d d' X Y R k }. +Notation "R .-sfker X ~> Y" := (sfinite_kernel X Y R). + +Arguments sfinite_subdef {_ _ _ _ _} _. + +HB.mixin Record SFiniteKernel_isFinite + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) (k : X -> {measure set Y -> \bar R}) := + { measure_uub : measure_fam_uub k }. + +#[short(type=finite_kernel)] +HB.structure Definition FiniteKernel + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) := + {k of SFiniteKernel_isFinite _ _ X Y R k & @SFiniteKernel _ _ X Y R k }. +Notation "R .-fker X ~> Y" := (finite_kernel X Y R). + +Arguments measure_uub {_ _ _ _ _} _. + +HB.factory Record Kernel_isFinite d d' (X : measurableType d) + (Y : measurableType d') (R : realType) (k : X -> {measure set Y -> \bar R}) of isKernel _ _ _ _ _ k := { + measure_uub : measure_fam_uub k }. + +Section kzero. +Variables (d d' : _) (X : measurableType d) (Y : measurableType d'). +Variable R : realType. + +Definition kzero : X -> {measure set Y -> \bar R} := + fun _ : X => [the measure _ _ of mzero]. + +Let measurable_fun_kzero U : measurable U -> + measurable_fun setT (kzero ^~ U). +Proof. by move=> ?/=; exact: measurable_fun_cst. Qed. + +HB.instance Definition _ := + @isKernel.Build _ _ X Y R kzero measurable_fun_kzero. + +(*Let kernel_from_mzero_sfinite0 : exists2 s : (R.-ker T' ~> T)^nat, forall n, measure_fam_uub (s n) & + forall x U, measurable U -> kernel_from_mzero x U = kseries s x U. +Proof. +exists (fun=> [the _.-ker _ ~> _ of kernel_from_mzero]). + move=> _. + by exists 1%R => y; rewrite /= /mzero. +by move=> t U mU/=; rewrite /mseries nneseries0. +Qed. + +HB.instance Definition _ := + @isSFinite0.Build _ _ _ T R kernel_from_mzero + kernel_from_mzero_sfinite0.*) + +Lemma kzero_uub : measure_fam_uub kzero. +Proof. by exists 1%R => /= t; rewrite /mzero/=. Qed. + +(*HB.instance Definition _ := + @SFiniteKernel_isFinite.Build _ _ _ T R kernel_from_mzero + kernel_from_mzero_uub.*) + +End kzero. + +HB.builders Context d d' (X : measurableType d) (Y : measurableType d') + (R : realType) k of Kernel_isFinite d d' X Y R k. + +Lemma sfinite_finite : + exists2 k_ : (R.-ker _ ~> _)^nat, forall n, measure_fam_uub (k_ n) & + forall x U, measurable U -> k x U = [the measure _ _ of mseries (k_ ^~ x) 0] U. +Proof. +exists (fun n => if n is O then [the _.-ker _ ~> _ of k] else + [the _.-ker _ ~> _ of @kzero _ _ X Y R]). + by case => [|_]; [exact: measure_uub|exact: kzero_uub]. +move=> t U mU/=; rewrite /mseries. +rewrite (nneseries_split 1%N)// big_ord_recl/= big_ord0 adde0. +rewrite ereal_series (@eq_nneseries _ _ (fun=> 0%E)); last by case. +by rewrite nneseries0// adde0. +Qed. + +HB.instance Definition _ := @Kernel_isSFinite_subdef.Build d d' X Y R k sfinite_finite. + +HB.instance Definition _ := @SFiniteKernel_isFinite.Build d d' X Y R k measure_uub. + +HB.end. + +Section sfinite. +Variables (d d' : _) (X : measurableType d) (Y : measurableType d'). +Variables (R : realType) (k : R.-sfker X ~> Y). + +Let s : (X -> {measure set Y -> \bar R})^nat := + let: exist2 x _ _ := cid2 (sfinite_subdef k) in x. + +Let ms n : @isKernel d d' X Y R (s n). +Proof. +split; rewrite /s; case: cid2 => /= s' s'_uub kE. +exact: measurable_kernel. +Qed. + +HB.instance Definition _ n := ms n. + +Let s_uub n : measure_fam_uub (s n). +Proof. by rewrite /s; case: cid2. Qed. + +HB.instance Definition _ n := + @Kernel_isFinite.Build d d' X Y R (s n) (s_uub n). + +Lemma sfinite : exists s : (R.-fker X ~> Y)^nat, + forall x U, measurable U -> k x U = kseries s x U. +Proof. +exists (fun n => [the _.-fker _ ~> _ of s n]) => x U mU. +by rewrite /s /= /s; by case: cid2 => ? ? ->. +Qed. + +End sfinite. + +HB.instance Definition _ (d d' : _) (X : measurableType d) + (Y : measurableType d') (R : realType) := + @Kernel_isFinite.Build _ _ _ _ R (@kzero _ _ X Y R) + (@kzero_uub _ _ X Y R). + +HB.factory Record Kernel_isSFinite d d' (X : measurableType d) + (Y : measurableType d') (R : realType) (k : X -> {measure set Y -> \bar R}) + of isKernel _ _ _ _ _ k := { + sfinite : exists s : (R.-fker X ~> Y)^nat, + forall x U, measurable U -> k x U = kseries s x U }. + +HB.builders Context d d' (X : measurableType d) (Y : measurableType d') + (R : realType) k of Kernel_isSFinite d d' X Y R k. + +Lemma sfinite_subdef : Kernel_isSFinite_subdef d d' X Y R k. +Proof. +split; have [s sE] := sfinite; exists s => //. +by move=> n; exact: measure_uub. +Qed. + +HB.instance Definition _ := (*@isSFinite0.Build d d' X Y R k*) sfinite_subdef. + +HB.end. + +HB.mixin Record FiniteKernel_isSubProbability + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) (k : X -> {measure set Y -> \bar R}) := + { sprob_kernel : ereal_sup [set k x [set: Y] | x in setT] <= 1}. + +#[short(type=sprobability_kernel)] +HB.structure Definition SubProbabilityKernel + (d d' : _) (X : measurableType d) (Y : measurableType d') + (R : realType) := + {k of FiniteKernel_isSubProbability _ _ X Y R k & + @FiniteKernel _ _ X Y R k}. +Notation "R .-spker X ~> Y" := (sprobability_kernel X Y R). + +HB.factory Record Kernel_isSubProbability + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) (k : X -> {measure set Y -> \bar R}) of isKernel _ _ X Y R k := + { sprob_kernel : ereal_sup [set k x [set: Y] | x in setT] <= 1}. + +HB.builders Context d d' (X : measurableType d) (Y : measurableType d') + (R : realType) k of Kernel_isSubProbability d d' X Y R k. + +Let finite : @Kernel_isFinite d d' X Y R k. +Proof. +split; exists 2%R => /= ?; rewrite (@le_lt_trans _ _ 1%:E) ?lte_fin ?ltr1n//. +by rewrite (le_trans _ sprob_kernel)//; exact: ereal_sup_ub. +Qed. + +HB.instance Definition _ := finite. + +HB.instance Definition _ := @FiniteKernel_isSubProbability.Build _ _ _ _ _ k sprob_kernel. + +HB.end. + +HB.mixin Record SubProbability_isProbability + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) (k : X -> {measure set Y -> \bar R}) := + { prob_kernel : forall x, k x [set: Y] = 1}. + +#[short(type=probability_kernel)] +HB.structure Definition ProbabilityKernel + (d d' : _) (X : measurableType d) (Y : measurableType d') + (R : realType) := + {k of SubProbability_isProbability _ _ X Y R k & + @SubProbabilityKernel _ _ X Y R k}. +Notation "R .-pker X ~> Y" := (probability_kernel X Y R). + +HB.factory Record Kernel_isProbability + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) (k : X -> {measure set Y -> \bar R}) of isKernel _ _ X Y R k := + { prob_kernel : forall x, k x setT = 1 }. + +HB.builders Context d d' (X : measurableType d) (Y : measurableType d') + (R : realType) k of Kernel_isProbability d d' X Y R k. + +Let sprob_kernel : @Kernel_isSubProbability d d' X Y R k. +Proof. +by split; apply: ub_ereal_sup => x [y _ <-{x}]; rewrite prob_kernel. +Qed. + +HB.instance Definition _ := sprob_kernel. + +HB.instance Definition _ := @SubProbability_isProbability.Build _ _ _ _ _ k prob_kernel. + +HB.end. + +Lemma finite_kernel_measure (d d' : _) (X : measurableType d) + (Y : measurableType d') (R : realType) (k : R.-fker X ~> Y) (x : X) : + finite_measure (k x). +Proof. +have [r k_r] := measure_uub k. +by rewrite /finite_measure (@lt_trans _ _ r%:E) ?ltey. +Qed. + +Lemma sfinite_kernel_measure (d d' : _) (X : measurableType d) + (Y : measurableType d') (R : realType) (k : R.-sfker X ~> Y) (x : X) : + sfinite_measure (k x). +Proof. +have [k_ k_E] := sfinite k. +exists (fun n => k_ n x); last by move=> A mA; rewrite k_E. +move=> n; rewrite /finite_measure. +exact: finite_kernel_measure. +Qed. + +(* see measurable_prod_subset in lebesgue_integral.v; + the differences between the two are: + - m2 is a kernel instead of a measure (the proof uses the + measurability of each measure of the family) + - as a consequence, m2D_bounded holds for all x *) +Section measurable_prod_subset_kernel. +Variables (d d' : _) (X : measurableType d) (Y : measurableType d') + (R : realType). +Implicit Types A : set (X * Y). + +Section xsection_kernel. +Variable (k : R.-ker X ~> Y) (D : set Y) (mD : measurable D). +Let kD x := mrestr (k x) mD. +HB.instance Definition _ x := Measure.on (kD x). +Let phi A := fun x => kD x (xsection A x). +Let XY := [set A | measurable A /\ measurable_fun setT (phi A)]. + +Let phiM (A : set X) B : phi (A `*` B) = (fun x => kD x B * (\1_A x)%:E). +Proof. +rewrite funeqE => x; rewrite indicE /phi/=. +have [xA|xA] := boolP (x \in A); first by rewrite mule1 in_xsectionM. +by rewrite mule0 notin_xsectionM// set0I measure0. +Qed. + +Lemma measurable_prod_subset_xsection_kernel : + (forall x, exists M, forall X, measurable X -> kD x X < M%:E) -> + measurable `<=` XY. +Proof. +move=> kD_ub; rewrite measurable_prod_measurableType. +set C := [set A `*` B | A in measurable & B in measurable]. +have CI : setI_closed C. + move=> _ _ [X1 mX1 [X2 mX2 <-]] [Y1 mY1 [Y2 mY2 <-]]. + exists (X1 `&` Y1); first exact: measurableI. + by exists (X2 `&` Y2); [exact: measurableI|rewrite setMI]. +have CT : C setT by exists setT => //; exists setT => //; rewrite setMTT. +have CXY : C `<=` XY. + move=> _ [A mA [B mB <-]]; split; first exact: measurableM. + rewrite phiM. + apply: emeasurable_funM => //; first exact/measurable_kernel/measurableI. + by apply/EFin_measurable_fun; rewrite (_ : \1_ _ = mindic R mA). +suff monoB : monotone_class setT XY by exact: monotone_class_subset. +split => //; [exact: CXY| |exact: xsection_ndseq_closed]. +move=> A B BA [mA mphiA] [mB mphiB]; split; first exact: measurableD. +suff : phi (A `\` B) = (fun x => phi A x - phi B x). + by move=> ->; exact: emeasurable_funB. +rewrite funeqE => x; rewrite /phi/= xsectionD// measureD. +- by rewrite setIidr//; exact: le_xsection. +- exact: measurable_xsection. +- exact: measurable_xsection. +- have [M kM] := kD_ub x. + rewrite (lt_le_trans (kM (xsection A x) _)) ?leey//. + exact: measurable_xsection. +Qed. + +End xsection_kernel. + +End measurable_prod_subset_kernel. + +(* see measurable_fun_xsection in lebesgue_integral.v + the difference is that this section uses a finite kernel m2 + instead of a sigma-finite measure m2 *) +Section measurable_fun_xsection_finite_kernel. +Variables (d d' : _) (X : measurableType d) (Y : measurableType d') + (R : realType). +Variables (k : R.-fker X ~> Y). +Implicit Types A : set (X * Y). + +Let phi A := fun x => k x (xsection A x). +Let XY := [set A | measurable A /\ measurable_fun setT (phi A)]. + +Lemma measurable_fun_xsection_finite_kernel A : + A \in measurable -> measurable_fun setT (phi A). +Proof. +move: A; suff : measurable `<=` XY by move=> + A; rewrite inE => /[apply] -[]. +move=> /= A mA; rewrite /XY/=; split => //; rewrite (_ : phi _ = + (fun x => mrestr (k x) measurableT (xsection A x))); last first. + by apply/funext => x//=; rewrite /mrestr setIT. +apply measurable_prod_subset_xsection_kernel => // x. +have [r hr] := measure_uub k; exists r => B mB. +by rewrite (le_lt_trans _ (hr x)) // /mrestr /= setIT le_measure// inE. +Qed. + +End measurable_fun_xsection_finite_kernel. + +Section measurable_fun_integral_finite_sfinite. +Variables (d d' : _) (X : measurableType d) (Y : measurableType d') + (R : realType). +Variable k : X * Y -> \bar R. + +Lemma measurable_fun_xsection_integral + (l : X -> {measure set Y -> \bar R}) + (k_ : ({nnsfun [the measurableType _ of (X * Y)%type] >-> R})^nat) + (ndk_ : nondecreasing_seq (k_ : (X * Y -> R)^nat)) + (k_k : forall z, EFin \o (k_ ^~ z) --> k z) : + (forall n r, measurable_fun setT (fun x => l x (xsection (k_ n @^-1` [set r]) x))) -> + measurable_fun setT (fun x => \int[l x]_y k (x, y)). +Proof. +move=> h. +rewrite (_ : (fun x => _) = + (fun x => elim_sup (fun n => \int[l x]_y (k_ n (x, y))%:E))); last first. + apply/funext => x. + transitivity (lim (fun n => \int[l x]_y (k_ n (x, y))%:E)); last first. + rewrite is_cvg_elim_supE//. + apply: ereal_nondecreasing_is_cvg => m n mn. + apply: ge0_le_integral => //. + - by move=> y _; rewrite lee_fin. + - exact/EFin_measurable_fun/measurable_fun_prod1. + - by move=> y _; rewrite lee_fin. + - exact/EFin_measurable_fun/measurable_fun_prod1. + - by move=> y _; rewrite lee_fin; exact/lefP/ndk_. + rewrite -monotone_convergence//. + - by apply: eq_integral => y _; apply/esym/cvg_lim => //; exact: k_k. + - by move=> n; exact/EFin_measurable_fun/measurable_fun_prod1. + - by move=> n y _; rewrite lee_fin. + - by move=> y _ m n mn; rewrite lee_fin; exact/lefP/ndk_. +apply: measurable_fun_elim_sup => n. +rewrite [X in measurable_fun _ X](_ : _ = (fun x => \int[l x]_y + (\sum_(r <- fset_set (range (k_ n)))(*TODO: upd when PR 743 is merged*) + r * \1_(k_ n @^-1` [set r]) (x, y))%:E)); last first. + by apply/funext => x; apply: eq_integral => y _; rewrite fimfunE. +rewrite [X in measurable_fun _ X](_ : _ = (fun x => + \sum_(r <- fset_set (range (k_ n)))(*TODO: upd when PR 743 is merged*) + (\int[l x]_y (r * \1_(k_ n @^-1` [set r]) (x, y))%:E))); last first. + apply/funext => x; rewrite -ge0_integral_sum//. + - by apply: eq_integral => y _; rewrite sumEFin. + - move=> r. + apply/EFin_measurable_fun/measurable_funrM/measurable_fun_prod1 => /=. + rewrite (_ : \1_ _ = mindic R (measurable_sfunP (k_ n) r))//. + exact/measurable_funP. + - by move=> m y _; rewrite nnfun_muleindic_ge0. +apply emeasurable_fun_sum => r. +rewrite [X in measurable_fun _ X](_ : _ = (fun x => r%:E * + \int[l x]_y (\1_(k_ n @^-1` [set r]) (x, y))%:E)); last first. + apply/funext => x; under eq_integral do rewrite EFinM. + have [r0|r0] := leP 0%R r. + rewrite ge0_integralM//; last by move=> y _; rewrite lee_fin. + apply/EFin_measurable_fun/measurable_fun_prod1 => /=. + rewrite (_ : \1_ _ = mindic R (measurable_sfunP (k_ n) r))//. + exact/measurable_funP. + rewrite integral_eq0; last first. + by move=> y _; rewrite preimage_nnfun0// indic0 mule0. + by rewrite integral_eq0 ?mule0// => y _; rewrite preimage_nnfun0// indic0. +apply/measurable_funeM. +rewrite (_ : (fun x => _) = (fun x => l x (xsection (k_ n @^-1` [set r]) x))). + exact/h. +apply/funext => x; rewrite integral_indic//; last first. + rewrite (_ : (fun x => _) = xsection (k_ n @^-1` [set r]) x). + exact: measurable_xsection. + by rewrite /xsection; apply/seteqP; split=> y/= /[!inE]. +congr (l x _); apply/funext => y1/=; rewrite /xsection/= inE. +by apply/propext; tauto. +Qed. + +Lemma measurable_fun_integral_finite_kernel (l : R.-fker X ~> Y) + (k0 : forall z, 0 <= k z) (mk : measurable_fun setT k) : + measurable_fun setT (fun x => \int[l x]_y k (x, y)). +Proof. +have [k_ [ndk_ k_k]] := approximation measurableT mk (fun x _ => k0 x). +apply: (measurable_fun_xsection_integral ndk_ (k_k ^~ Logic.I)) => n r. +have [l_ hl_] := measure_uub l. +by apply: measurable_fun_xsection_finite_kernel => // /[!inE]. +Qed. + +Lemma measurable_fun_integral_sfinite_kernel (l : R.-sfker X ~> Y) + (k0 : forall t, 0 <= k t) (mk : measurable_fun setT k) : + measurable_fun setT (fun x => \int[l x]_y k (x, y)). +Proof. +have [k_ [ndk_ k_k]] := approximation measurableT mk (fun xy _ => k0 xy). +apply: (measurable_fun_xsection_integral ndk_ (k_k ^~ Logic.I)) => n r. +have [l_ hl_] := sfinite l. +rewrite (_ : (fun x => _) = + (fun x => mseries (l_ ^~ x) 0 (xsection (k_ n @^-1` [set r]) x))); last first. + by apply/funext => x; rewrite hl_//; exact/measurable_xsection. +apply: ge0_emeasurable_fun_sum => // m. +by apply: measurable_fun_xsection_finite_kernel => // /[!inE]. +Qed. + +End measurable_fun_integral_finite_sfinite. +Arguments measurable_fun_xsection_integral {_ _ _ _ _} k l. +Arguments measurable_fun_integral_finite_kernel {_ _ _ _ _} k l. +Arguments measurable_fun_integral_sfinite_kernel {_ _ _ _ _} k l. + +Section kprobability. +Variables (d d' : _) (X : measurableType d) (Y : measurableType d'). +Variables (R : realType) (P : probability Y R). + +Definition kprobability : X -> {measure set Y -> \bar R} := fun=> P. + +Let measurable_fun_kprobability U : measurable U -> + measurable_fun setT (kprobability ^~ U). +Proof. by move=> mU; exact: measurable_fun_cst. Qed. + +HB.instance Definition _ := + @isKernel.Build _ _ X Y R kprobability measurable_fun_kprobability. + +Let kprobability_prob x : kprobability x setT = 1. +Proof. by rewrite /kprobability/= probability_setT. Qed. + +HB.instance Definition _ := + @Kernel_isProbability.Build _ _ X Y R kprobability kprobability_prob. + +End kprobability. + +Section kdirac. +Variables (d d' : _) (X : measurableType d) (Y : measurableType d'). +Variables (R : realType) (f : X -> Y). + +Definition kdirac (mf : measurable_fun setT f) + : X -> {measure set Y -> \bar R} := + fun x : X => [the measure _ _ of dirac (f x)]. + +Hypothesis mf : measurable_fun setT f. + +Let measurable_fun_kdirac U : measurable U -> + measurable_fun setT (kdirac mf ^~ U). +Proof. +move=> mU; apply/EFin_measurable_fun. +by rewrite (_ : (fun x => _) = mindic R mU \o f)//; exact/measurable_fun_comp. +Qed. + +HB.instance Definition _ := isKernel.Build _ _ _ _ _ (kdirac mf) + measurable_fun_kdirac. + +Let kdirac_prob x : kdirac mf x setT = 1. +Proof. by rewrite /kdirac/= diracT. Qed. + +HB.instance Definition _ := Kernel_isProbability.Build _ _ _ _ _ + (kdirac mf) kdirac_prob. + +End kdirac. +Arguments kdirac {d d' X Y R f}. + +Section kadd. +Variables (d d' : _) (X : measurableType d) (Y : measurableType d'). +Variables (R : realType) (k1 k2 : R.-ker X ~> Y). + +Definition kadd : X -> {measure set Y -> \bar R} := + fun x => [the measure _ _ of measure_add (k1 x) (k2 x)]. + +Let measurable_fun_kadd U : measurable U -> + measurable_fun setT (kadd ^~ U). +Proof. +move=> mU; rewrite /kadd. +rewrite (_ : (fun _ => _) = (fun x => k1 x U + k2 x U)); last first. + by apply/funext => x; rewrite -measure_addE. +by apply: emeasurable_funD; exact/measurable_kernel. +Qed. + +HB.instance Definition _ := + @isKernel.Build _ _ _ _ _ kadd measurable_fun_kadd. +End kadd. + +Section sfkadd. +Variables (d d' : _) (X : measurableType d) (Y : measurableType d'). +Variables (R : realType) (k1 k2 : R.-sfker X ~> Y). + +Let sfinite_kadd : exists2 k_ : (R.-ker _ ~> _)^nat, forall n, measure_fam_uub (k_ n) & + forall x U, measurable U -> + kadd k1 k2 x U = [the measure _ _ of mseries (k_ ^~ x) 0] U. +Proof. +have [f1 hk1] := sfinite k1. +have [f2 hk2] := sfinite k2. +exists (fun n => [the _.-ker _ ~> _ of kadd (f1 n) (f2 n)]). + move=> n. + have [r1 f1r1] := measure_uub (f1 n). + have [r2 f2r2] := measure_uub (f2 n). + exists (r1 + r2)%R => x/=. + by rewrite /msum !big_ord_recr/= big_ord0 add0e EFinD lte_add. +move=> x U mU. +rewrite /kadd/=. +rewrite -/(measure_add (k1 x) (k2 x)) measure_addE. +rewrite /mseries. +rewrite hk1//= hk2//= /mseries. +rewrite -nneseriesD//. +apply: eq_nneseries => n _. +by rewrite -/(measure_add (f1 n x) (f2 n x)) measure_addE. +Qed. + +HB.instance Definition _ t := + Kernel_isSFinite_subdef.Build _ _ _ _ R (kadd k1 k2) sfinite_kadd. +End sfkadd. + +Section fkadd. +Variables (d d' : _) (X : measurableType d) (Y : measurableType d'). +Variables (R : realType) (k1 k2 : R.-fker X ~> Y). + +Let kadd_finite_uub : measure_fam_uub (kadd k1 k2). +Proof. +have [f1 hk1] := measure_uub k1; have [f2 hk2] := measure_uub k2. +exists (f1 + f2)%R => x; rewrite /kadd /=. +rewrite -/(measure_add (k1 x) (k2 x)). +by rewrite measure_addE EFinD; exact: lte_add. +Qed. + +HB.instance Definition _ t := + Kernel_isFinite.Build _ _ _ _ R (kadd k1 k2) kadd_finite_uub. +End fkadd. + +(* TODO: move *) +Section kernel_measurable_preimage. +Variables (d d' : _) (T : measurableType d) (T' : measurableType d'). +Variable R : realType. + +Lemma measurable_eq_cst (f : R.-ker T ~> T') k : + measurable [set t | f t setT == k]. +Proof. +rewrite [X in measurable X](_ : _ = (f ^~ setT) @^-1` [set k]); last first. + by apply/seteqP; split => t/= /eqP. +have /(_ measurableT [set k]) := measurable_kernel f setT measurableT. +by rewrite setTI; exact. +Qed. + +Lemma measurable_neq_cst (f : R.-ker T ~> T') k : + measurable [set t | f t setT != k]. +Proof. +rewrite [X in measurable X](_ : _ = (f ^~ setT) @^-1` [set~ k]); last first. + by apply/seteqP; split => t /eqP. +have /(_ measurableT [set~ k]) := measurable_kernel f setT measurableT. +by rewrite setTI; apply => //; exact: measurableC. +Qed. + +End kernel_measurable_preimage. + +(* TODO: move *) +Lemma measurable_fun_eq_cst (d d' : _) (T : measurableType d) + (T' : measurableType d') (R : realType) (f : R.-ker T ~> T') k : + measurable_fun setT (fun t => f t setT == k). +Proof. +move=> _ /= B mB; rewrite setTI. +have [/eqP->|/eqP->|/eqP->|/eqP->] := set_boolE B. +- exact: measurable_eq_cst. +- rewrite (_ : _ @^-1` _ = [set b | f b setT != k]); last first. + by apply/seteqP; split => [t /negbT//|t /negbTE]. + exact: measurable_neq_cst. +- by rewrite preimage_set0. +- by rewrite preimage_setT. +Qed. + +Section mnormalize. +Variables (d d' : _) (X : measurableType d) (Y : measurableType d'). +Variables (R : realType) (f : X -> {measure set Y -> \bar R}). +Variable P : probability Y R. + +Definition mnormalize x U := + let evidence := f x [set: Y] in + if (evidence == 0) || (evidence == +oo) then P U + else f x U * (fine evidence)^-1%:E. + +Let mnormalize0 x : mnormalize x set0 = 0. +Proof. +by rewrite /mnormalize; case: ifPn => // _; rewrite measure0 mul0e. +Qed. + +Let mnormalize_ge0 x U : 0 <= mnormalize x U. +Proof. by rewrite /mnormalize; case: ifPn => //; case: ifPn. Qed. + +Lemma mnormalize_sigma_additive x : semi_sigma_additive (mnormalize x). +Proof. +move=> F mF tF mUF; rewrite /mnormalize/=. +case: ifPn => [_|_]. + exact: measure_semi_sigma_additive. +rewrite (_ : (fun n => _) = ((fun n => \sum_(0 <= i < n) f x (F i)) \* + cst ((fine (f x setT))^-1)%:E)); last first. + by apply/funext => n; rewrite -ge0_sume_distrl. +by apply: ereal_cvgMr => //; exact: measure_semi_sigma_additive. +Qed. + +HB.instance Definition _ x := isMeasure.Build _ _ _ (mnormalize x) + (mnormalize0 x) (mnormalize_ge0 x) (@mnormalize_sigma_additive x). + +Lemma mnormalize1 x : mnormalize x setT = 1. +Proof. +rewrite /mnormalize; case: ifPn; first by rewrite probability_setT. +rewrite negb_or => /andP[ft0 ftoo]. +have ? : f x setT \is a fin_num. + by rewrite ge0_fin_numE// lt_neqAle ftoo/= leey. +by rewrite -{1}(@fineK _ (f x setT))// -EFinM divrr// ?unitfE fine_eq0. +Qed. + +HB.instance Definition _ x := + isProbability.Build _ _ _ (mnormalize x) (mnormalize1 x). + +End mnormalize. + +Section knormalize. +Variables (d d' : _) (X : measurableType d) (Y : measurableType d'). +Variables (R : realType) (f : R.-ker X ~> Y). + +Definition knormalize (P : probability Y R) := + fun t => [the measure _ _ of mnormalize f P t]. + +Variable P : probability Y R. + +Let measurable_fun_knormalize U : + measurable U -> measurable_fun setT (knormalize P ^~ U). +Proof. +move=> mU; rewrite /knormalize/= /mnormalize /=. +rewrite (_ : (fun _ => _) = (fun x => + if f x setT == 0 then P U else if f x setT == +oo then P U + else f x U * (fine (f x setT))^-1%:E)); last first. + apply/funext => x; case: ifPn => [/orP[->//|->]|]; first by case: ifPn. + by rewrite negb_or=> /andP[/negbTE -> /negbTE ->]. +apply: measurable_fun_if => //; + [exact: measurable_fun_eq_cst|exact: measurable_fun_cst|]. +apply: measurable_fun_if => //. +- rewrite setTI [X in measurable X](_ : _ = [set t | f t setT != 0]). + exact: measurable_neq_cst. + by apply/seteqP; split => [x /negbT//|x /negbTE]. +- exact: measurable_fun_eq_cst. +- exact: measurable_fun_cst. +- apply: emeasurable_funM. + by have := measurable_kernel f U mU; exact: measurable_funS. + apply/EFin_measurable_fun. + apply: (@measurable_fun_comp' _ _ _ _ _ _ [set r : R | r != 0%R]) => //. + + exact: open_measurable. + + move=> /= r [t] [] [_ ft0] ftoo ftr; apply/eqP => r0. + move: (ftr); rewrite r0 => /eqP; rewrite fine_eq0 ?ft0//. + by rewrite ge0_fin_numE// lt_neqAle leey ftoo. + + apply: open_continuous_measurable_fun => //; apply/in_setP => x /= x0. + exact: inv_continuous. + + apply: measurable_fun_comp => /=; first exact: measurable_fun_fine. + by have := measurable_kernel f _ measurableT; exact: measurable_funS. +Qed. + +HB.instance Definition _ := isKernel.Build _ _ _ _ R (knormalize P) + measurable_fun_knormalize. + +Let knormalize1 x : knormalize P x setT = 1. +Proof. +rewrite /knormalize/= /mnormalize. +case: ifPn => [_|]; first by rewrite probability_setT. +rewrite negb_or => /andP[fx0 fxoo]. +have ? : f x setT \is a fin_num by rewrite ge0_fin_numE// lt_neqAle fxoo/= leey. +rewrite -{1}(@fineK _ (f x setT))//=. +by rewrite -EFinM divrr// ?lte_fin ?ltr1n// ?unitfE fine_eq0. +Qed. + +HB.instance Definition _ := + @Kernel_isProbability.Build _ _ _ _ _ (knormalize P) knormalize1. + +End knormalize. + +Section kcomp_def. +Variables (d1 d2 d3 : _) (X : measurableType d1) (Y : measurableType d2) + (Z : measurableType d3) (R : realType). +Variable l : X -> {measure set Y -> \bar R}. +Variable k : (X * Y)%type -> {measure set Z -> \bar R}. + +Definition kcomp x U := \int[l x]_y k (x, y) U. + +End kcomp_def. + +Section kcomp_is_measure. +Variables (d1 d2 d3 : _) (X : measurableType d1) (Y : measurableType d2) + (Z : measurableType d3) (R : realType). +Variable l : R.-ker X ~> Y. +Variable k : R.-ker [the measurableType _ of (X * Y)%type] ~> Z. + +Local Notation "l \; k" := (kcomp l k). + +Let kcomp0 x : (l \; k) x set0 = 0. +Proof. +by rewrite /kcomp (eq_integral (cst 0)) ?integral0// => y _; rewrite measure0. +Qed. + +Let kcomp_ge0 x U : 0 <= (l \; k) x U. Proof. exact: integral_ge0. Qed. + +Let kcomp_sigma_additive x : semi_sigma_additive ((l \; k) x). +Proof. +move=> U mU tU mUU; rewrite [X in _ --> X](_ : _ = + \int[l x]_y (\sum_(n V _. + by apply/esym/cvg_lim => //; exact/measure_semi_sigma_additive. +apply/cvg_closeP; split. + by apply: is_cvg_nneseries => n _; exact: integral_ge0. +rewrite closeE// integral_sum// => n. +by have /measurable_fun_prod1 := measurable_kernel k _ (mU n). +Qed. + +HB.instance Definition _ x := isMeasure.Build _ R _ + ((l \; k) x) (kcomp0 x) (kcomp_ge0 x) (@kcomp_sigma_additive x). + +Definition mkcomp : X -> {measure set Z -> \bar R} := + fun x => [the measure _ _ of (l \; k) x]. + +End kcomp_is_measure. + +Notation "l \; k" := (mkcomp l k). + +Module KCOMP_FINITE_KERNEL. + +Section kcomp_finite_kernel_kernel. +Variables (d d' d3 : _) (X : measurableType d) (Y : measurableType d') + (Z : measurableType d3) (R : realType) (l : R.-fker X ~> Y) + (k : R.-ker [the measurableType _ of (X * Y)%type] ~> Z). + +Lemma measurable_fun_kcomp_finite U : + measurable U -> measurable_fun setT ((l \; k) ^~ U). +Proof. +move=> mU; apply: (measurable_fun_integral_finite_kernel (k ^~ U)) => //=. +exact/measurable_kernel. +Qed. + +HB.instance Definition _ := + isKernel.Build _ _ X Z R (l \; k) measurable_fun_kcomp_finite. + +End kcomp_finite_kernel_kernel. + +Section kcomp_finite_kernel_finite. +Variables (d d' d3 : _) (X : measurableType d) (Y : measurableType d') + (Z : measurableType d3) (R : realType). +Variable l : R.-fker X ~> Y. +Variable k : R.-fker [the measurableType _ of (X * Y)%type] ~> Z. + +Let mkcomp_finite : measure_fam_uub (l \; k). +Proof. +have /measure_fam_uubP[r hr] := measure_uub k. +have /measure_fam_uubP[s hs] := measure_uub l. +apply/measure_fam_uubP; exists (PosNum [gt0 of (r%:num * s%:num)%R]) => x /=. +apply: (@le_lt_trans _ _ (\int[l x]__ r%:num%:E)). + apply: ge0_le_integral => //. + - have /measurable_fun_prod1 := measurable_kernel k _ measurableT. + exact. + - exact/measurable_fun_cst. + - by move=> y _; exact/ltW/hr. +by rewrite integral_cst//= EFinM lte_pmul2l. +Qed. + +HB.instance Definition _ := + Kernel_isFinite.Build _ _ X Z R (l \; k) mkcomp_finite. + +End kcomp_finite_kernel_finite. +End KCOMP_FINITE_KERNEL. + +Section kcomp_sfinite_kernel. +Variables (d d' d3 : _) (X : measurableType d) (Y : measurableType d') + (Z : measurableType d3) (R : realType). +Variable l : R.-sfker X ~> Y. +Variable k : R.-sfker [the measurableType _ of (X * Y)%type] ~> Z. + +Import KCOMP_FINITE_KERNEL. + +Lemma mkcomp_sfinite : exists k_ : (R.-fker X ~> Z)^nat, forall x U, measurable U -> + (l \; k) x U = kseries k_ x U. +Proof. +have [k_ hk_] := sfinite k; have [l_ hl_] := sfinite l. +have [kl hkl] : exists kl : (R.-fker X ~> Z) ^nat, forall x U, + \esum_(i in setT) (l_ i.2 \; k_ i.1) x U = \sum_(i [the _.-fker _ ~> _ of l_ (f i).2 \; k_ (f i).1]) => x U. + by rewrite (reindex_esum [set: nat] _ f)// nneseries_esum// fun_true. +exists kl => x U mU. +transitivity (([the _.-ker _ ~> _ of kseries l_] \; + [the _.-ker _ ~> _ of kseries k_]) x U). + rewrite /= /kcomp [in RHS](eq_measure_integral (l x)); last first. + by move=> *; rewrite hl_. + by apply: eq_integral => y _; rewrite hk_. +rewrite /= /kcomp/= integral_sum//=; last first. + by move=> n; have /measurable_fun_prod1 := measurable_kernel (k_ n) _ mU; exact. +transitivity (\sum_(i i _; rewrite integral_kseries//. + by have /measurable_fun_prod1 := measurable_kernel (k_ i) _ mU; exact. +rewrite /mseries -hkl/=. +rewrite (_ : setT = setT `*`` (fun=> setT)); last by apply/seteqP; split. +rewrite -(@esum_esum _ _ _ _ _ (fun i j => (l_ j \; k_ i) x U))//. +rewrite nneseries_esum; last by move=> n _; exact: nneseries_ge0. +by rewrite fun_true; apply: eq_esum => /= i _; rewrite nneseries_esum// fun_true. +Qed. + +Lemma measurable_fun_mkcomp_sfinite U : measurable U -> + measurable_fun setT ((l \; k) ^~ U). +Proof. +move=> mU; apply: (measurable_fun_integral_sfinite_kernel (k ^~ U)) => //. +exact/measurable_kernel. +Qed. + +End kcomp_sfinite_kernel. + +Module KCOMP_SFINITE_KERNEL. +Section kcomp_sfinite_kernel. +Variables (d d' d3 : _) (X : measurableType d) (Y : measurableType d') + (Z : measurableType d3) (R : realType). +Variable l : R.-sfker X ~> Y. +Variable k : R.-sfker [the measurableType _ of (X * Y)%type] ~> Z. + +HB.instance Definition _ := + isKernel.Build _ _ X Z R (l \; k) (measurable_fun_mkcomp_sfinite l k). + +#[export] +HB.instance Definition _ := + Kernel_isSFinite.Build _ _ X Z R (l \; k) (mkcomp_sfinite l k). + +End kcomp_sfinite_kernel. +End KCOMP_SFINITE_KERNEL. +HB.export KCOMP_SFINITE_KERNEL. + +Section measurable_fun_preimage_integral. +Variables (d d' : _) (X : measurableType d) (Y : measurableType d') + (R : realType). +Variables (k : Y -> \bar R) + (k_ : ({nnsfun Y >-> R}) ^nat) + (ndk_ : nondecreasing_seq (k_ : (Y -> R)^nat)) + (k_k : forall z, setT z -> EFin \o (k_ ^~ z) --> k z). + +Let k_2 : (X * Y -> R)^nat := fun n => k_ n \o snd. + +Let k_2_ge0 n x : (0 <= k_2 n x)%R. Proof. by []. Qed. + +HB.instance Definition _ n := @IsNonNegFun.Build _ _ _ (k_2_ge0 n). + +Let mk_2 n : measurable_fun setT (k_2 n). +Proof. by apply: measurable_fun_comp => //; exact: measurable_fun_snd. Qed. + +HB.instance Definition _ n := @IsMeasurableFun.Build _ _ _ _ (mk_2 n). + +Let fk_2 n : finite_set (range (k_2 n)). +Proof. +have := @fimfunP _ _ (k_ n). +suff : range (k_ n) = range (k_2 n) by move=> <-. +by apply/seteqP; split => r [y ?] <-; [exists (point, y)|exists y.2]. +Qed. + +HB.instance Definition _ n := @FiniteImage.Build _ _ _ (fk_2 n). + +Lemma measurable_fun_preimage_integral (l : X -> {measure set Y -> \bar R}) : + (forall n r, measurable_fun setT (l ^~ (k_ n @^-1` [set r]))) -> + measurable_fun setT (fun x => \int[l x]_z k z). +Proof. +move=> h; apply: (measurable_fun_xsection_integral (k \o snd) l + (fun n => [the {nnsfun _ >-> _} of k_2 n])) => /=. +- by rewrite /k_2 => m n mn; apply/lefP => -[x y] /=; exact/lefP/ndk_. +- by move=> [x y]; exact: k_k. +- move=> n r _ /= B mB. + have := h n r measurableT B mB; rewrite !setTI. + suff : (l ^~ (k_ n @^-1` [set r])) @^-1` B = + (fun x => l x (xsection (k_2 n @^-1` [set r]) x)) @^-1` B by move=> ->. + by apply/seteqP; split => x/=; rewrite xsection_preimage_snd. +Qed. + +End measurable_fun_preimage_integral. + +Lemma measurable_fun_integral_kernel + d d' (X : measurableType d) (Y : measurableType d') (R : realType) + (l : X -> {measure set Y -> \bar R}) + (ml : forall U, measurable U -> measurable_fun setT (l ^~ U)) + (* NB: l is really just a kernel *) + (k : Y -> \bar R) (k0 : forall z, 0 <= k z) (mk : measurable_fun setT k) : + measurable_fun setT (fun x => \int[l x]_y k y). +Proof. +have [k_ [ndk_ k_k]] := approximation measurableT mk (fun x _ => k0 x). +by apply: (measurable_fun_preimage_integral ndk_ k_k) => n r; exact/ml. +Qed. + +Section integral_kcomp. +Variables (d d2 d3 : _) (X : measurableType d) (Y : measurableType d2) + (Z : measurableType d3) (R : realType). +Variable l : R.-sfker X ~> Y. +Variables k : R.-sfker [the measurableType _ of (X * Y)%type] ~> Z. + +Let integral_kcomp_indic x E (mE : measurable E) : + \int[(l \; k) x]_z (\1_E z)%:E = \int[l x]_y (\int[k (x, y)]_z (\1_E z)%:E). +Proof. +rewrite integral_indic//= /kcomp. +by apply eq_integral => y _; rewrite integral_indic. +Qed. + +Let integral_kcomp_nnsfun x (f : {nnsfun Z >-> R}) : + \int[(l \; k) x]_z (f z)%:E = \int[l x]_y (\int[k (x, y)]_z (f z)%:E). +Proof. +under [in LHS]eq_integral do rewrite fimfunE -sumEFin. +rewrite ge0_integral_sum//; last 2 first. + - move=> r; apply/EFin_measurable_fun/measurable_funrM. + have fr : measurable (f @^-1` [set r]) by exact/measurable_sfunP. + by rewrite (_ : \1__ = mindic R fr). + - by move=> r z _; rewrite EFinM nnfun_muleindic_ge0. +under [in RHS]eq_integral. + move=> y _. + under eq_integral. + by move=> z _; rewrite fimfunE -sumEFin; over. + rewrite /= ge0_integral_sum//; last 2 first. + - move=> r; apply/EFin_measurable_fun/measurable_funrM. + have fr : measurable (f @^-1` [set r]) by exact/measurable_sfunP. + by rewrite (_ : \1__ = mindic R fr). + - by move=> r z _; rewrite EFinM nnfun_muleindic_ge0. + under eq_bigr. + move=> r _. + rewrite (integralM_indic _ (fun r => f @^-1` [set r]))//; last first. + by move=> r0; rewrite preimage_nnfun0. + rewrite integral_indic// setIT. + over. + over. +rewrite /= ge0_integral_sum//; last 2 first. + - move=> r; apply: measurable_funeM. + have := measurable_kernel k (f @^-1` [set r]) (measurable_sfunP f r). + by move=> /measurable_fun_prod1; exact. + - move=> n y _. + have := mulemu_ge0 (fun n => f @^-1` [set n]). + by apply; exact: preimage_nnfun0. +apply eq_bigr => r _. +rewrite (integralM_indic _ (fun r => f @^-1` [set r]))//; last first. + exact: preimage_nnfun0. +rewrite /= integral_kcomp_indic; last exact/measurable_sfunP. +have [r0|r0] := leP 0%R r. + rewrite ge0_integralM//; last first. + have := measurable_kernel k (f @^-1` [set r]) (measurable_sfunP f r). + by move/measurable_fun_prod1; exact. + by congr (_ * _); apply eq_integral => y _; rewrite integral_indic// setIT. +rewrite integral_eq0 ?mule0; last first. + by move=> y _; rewrite integral_eq0// => z _; rewrite preimage_nnfun0// indic0. +by rewrite integral_eq0// => y _; rewrite preimage_nnfun0// measure0 mule0. +Qed. + +Lemma integral_kcomp x f : (forall z, 0 <= f z) -> measurable_fun setT f -> + \int[(l \; k) x]_z f z = \int[l x]_y (\int[k (x, y)]_z f z). +Proof. +move=> f0 mf. +have [f_ [ndf_ f_f]] := approximation measurableT mf (fun z _ => f0 z). +transitivity (\int[(l \; k) x]_z (lim (EFin \o f_^~ z))). + by apply/eq_integral => z _; apply/esym/cvg_lim => //=; exact: f_f. +rewrite monotone_convergence//; last 3 first. + by move=> n; exact/EFin_measurable_fun. + by move=> n z _; rewrite lee_fin. + by move=> z _ a b /ndf_ /lefP ab; rewrite lee_fin. +rewrite (_ : (fun _ => _) = + (fun n => \int[l x]_y (\int[k (x, y)]_z (f_ n z)%:E)))//; last first. + by apply/funext => n; rewrite integral_kcomp_nnsfun. +transitivity (\int[l x]_y lim (fun n => \int[k (x, y)]_z (f_ n z)%:E)). + rewrite -monotone_convergence//; last 3 first. + - move=> n; apply: measurable_fun_integral_kernel => //. + + move=> U mU; have := measurable_kernel k _ mU. + by move=> /measurable_fun_prod1; exact. + + by move=> z; rewrite lee_fin. + + exact/EFin_measurable_fun. + - by move=> n y _; apply integral_ge0 => // z _; rewrite lee_fin. + - move=> y _ a b ab; apply: ge0_le_integral => //. + + by move=> z _; rewrite lee_fin. + + exact/EFin_measurable_fun. + + by move=> z _; rewrite lee_fin. + + exact/EFin_measurable_fun. + + by move: ab => /ndf_ /lefP ab z _; rewrite lee_fin. +apply eq_integral => y _; rewrite -monotone_convergence//; last 3 first. + - by move=> n; exact/EFin_measurable_fun. + - by move=> n z _; rewrite lee_fin. + - by move=> z _ a b /ndf_ /lefP; rewrite lee_fin. +by apply eq_integral => z _; apply/cvg_lim => //; exact: f_f. +Qed. + +End integral_kcomp. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 36183f2cd..8cf3524e0 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -330,6 +330,13 @@ Definition max_mfun f g := [the {mfun aT >-> _} of f \max g]. End ring. Arguments indic_mfun {d aT rT} _. +Lemma measurable_fun_indic (d : measure_display) (T : measurableType d) + (R : realType) (D A : set T) : measurable A -> + measurable_fun D (\1_A : T -> R). +Proof. +by move=> mA; apply/measurable_funTS; rewrite (_ : \1__ = mindic R mA). +Qed. + Section sfun_pred. Context {d} {aT : measurableType d} {rT : realType}. Definition sfun : {pred _ -> _} := [predI @mfun _ aT rT & fimfun]. @@ -626,33 +633,33 @@ Section mulem_ge0. Local Open Scope ereal_scope. Let mulef_ge0 (R : realDomainType) x (f : R -> \bar R) : - (forall x, 0 <= f x) -> ((x < 0)%R -> f x = 0) -> 0 <= x%:E * f x. + 0 <= f x -> ((x < 0)%R -> f x = 0) -> 0 <= x%:E * f x. Proof. move=> A0 xA /=; have [x0|x0] := ltP x 0%R; first by rewrite (xA x0) mule0. by rewrite mule_ge0. Qed. -Lemma muleindic_ge0 d (T : measurableType d) (R : realDomainType) +Lemma nnfun_muleindic_ge0 d (T : measurableType d) (R : realDomainType) (f : {nnfun T >-> R}) r z : 0 <= r%:E * (\1_(f @^-1` [set r]) z)%:E. Proof. apply: (@mulef_ge0 _ _ (fun r => (\1_(f @^-1` [set r]) z)%:E)). - by move=> x; rewrite lee_fin /indic. + by rewrite lee_fin// indicE. by move=> r0; rewrite preimage_nnfun0// indic0. Qed. -Lemma mulem_ge0 d (T : measurableType d) (R : realType) +Lemma mulemu_ge0 d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}) x (A : R -> set T) : ((x < 0)%R -> A x = set0) -> 0 <= x%:E * mu (A x). Proof. by move=> xA; rewrite (@mulef_ge0 _ _ (mu \o _))//= => /xA ->; rewrite measure0. Qed. -Arguments mulem_ge0 {d T R mu x} A. +Global Arguments mulemu_ge0 {d T R mu x} A. -Lemma nnfun_mulem_ge0 d (T : measurableType d) (R : realType) - (mu : {measure set T -> \bar R})(f : {nnsfun T >-> R}) x : +Lemma nnsfun_mulemu_ge0 d (T : measurableType d) (R : realType) + (mu : {measure set T -> \bar R}) (f : {nnsfun T >-> R}) x : 0 <= x%:E * mu (f @^-1` [set x]). Proof. -by apply: (mulem_ge0 (fun x => f @^-1` [set x])); exact: preimage_nnfun0. +by apply: (mulemu_ge0 (fun x => f @^-1` [set x])); exact: preimage_nnfun0. Qed. End mulem_ge0. @@ -694,7 +701,7 @@ by case: ifPn => [/[!inE] <-|]; rewrite ?mul0e// measure0 mule0. Qed. Lemma sintegral_ge0 (f : {nnsfun T >-> R}) : 0 <= sintegral mu f. -Proof. by rewrite sintegralE fsume_ge0// => r _; exact: nnfun_mulem_ge0. Qed. +Proof. by rewrite sintegralE fsume_ge0// => r _; exact: nnsfun_mulemu_ge0. Qed. Lemma sintegral_indic (A : set T) : sintegral mu \1_A = mu A. Proof. @@ -742,7 +749,7 @@ transitivity (\sum_(x \in [set: R]) r%:E * (x%:E * m (f @^-1` [set x]))). rewrite (reindex_fsbigT (fun x => r * x)%R)//; last first. by exists ( *%R r ^-1)%R; [exact: mulKf|exact: mulVKf]. by apply: eq_fsbigr => x; rewrite mulrAC divrr ?unitfE// mul1r muleA EFinM. -by rewrite ge0_mule_fsumr// => x; exact: nnfun_mulem_ge0. +by rewrite ge0_mule_fsumr// => x; exact: nnsfun_mulemu_ge0. Qed. End sintegralrM. @@ -844,7 +851,7 @@ rewrite /fleg [X in _ X](_ : _ = \big[setU/set0]_(y <- fset_set (range f)) \big[setU/set0]_(x <- fset_set (range (g n)) | c * y <= x) (f @^-1` [set y] `&` (g n @^-1` [set x]))). apply: bigsetU_measurable => r _; apply: bigsetU_measurable => r' crr'. - by apply: measurableI; apply/measurable_sfunP. + exact/measurableI/measurable_sfunP. rewrite predeqE => t; split => [/= cfgn|]. - rewrite -bigcup_set; exists (f t); first by rewrite /= in_fset_set//= mem_set. rewrite -bigcup_set_cond; exists (g n t) => //=. @@ -924,7 +931,7 @@ rewrite [X in X --> _](_ : _ = fun n => \sum_(x <- fset_set (range f)) by rewrite mulr0 => /esym/eqP; rewrite (negbTE r0). by rewrite /preimage/= => -[fxr cnx]; rewrite mindicE mem_set// mulr1. rewrite sintegralE fsbig_finite//=; apply: ereal_lim_sum => [r n _|r _]. - apply: (@mulem_ge0 _ _ _ _ _ (fun x => f @^-1` [set x] `&` fleg c n)) => r0. + apply: (mulemu_ge0 (fun x => f @^-1` [set x] `&` fleg c n)) => r0. by rewrite preimage_nnfun0// set0I. apply: ereal_cvgrM => //; rewrite [X in _ --> X](_ : _ = mu (\bigcup_n (f @^-1` [set r] `&` fleg c n))); last first. @@ -1221,7 +1228,7 @@ rewrite predeqE => r; split => [/= /[!in_itv]/= /andP[nr rn1]|]. rewrite ler_pdivr_mulr// (le_trans _ (floor_le _))//. by rewrite -(@gez0_abs (floor _))// floor_ge0 mulr_ge0// (le_trans _ nr). rewrite ltr_pdivl_mulr// (lt_le_trans (lt_succ_floor _))//. - rewrite -[in leRHS]addn1 natrD ler_add2r// -(@gez0_abs (floor _))// floor_ge0. + rewrite -[in leRHS]natr1 ler_add2r// -(@gez0_abs (floor _))// floor_ge0. by rewrite mulr_ge0// (le_trans _ nr). - rewrite -bigcup_set => -[/= k] /[!mem_index_iota] /andP[nk kn]. rewrite in_itv /= => /andP[knr rkn]; rewrite in_itv /=; apply/andP; split. @@ -1374,7 +1381,7 @@ have xAnK : x \in A n (Ordinal K). rewrite ler_pdivr_mulr// (le_trans _ (floor_le _))//. by rewrite -(@gez0_abs (floor _))// floor_ge0 mulr_ge0// ltW. rewrite ltr_pdivl_mulr// (lt_le_trans (lt_succ_floor _))//. - rewrite -[in leRHS]addn1 natrD ler_add2r// -{1}(@gez0_abs (floor _))//. + rewrite -[in leRHS]natr1 ler_add2r// -{1}(@gez0_abs (floor _))//. by rewrite floor_ge0// mulr_ge0// ltW. have /[!mem_index_enum]/(_ isT) := An0 (Ordinal K). apply/negP. @@ -1490,7 +1497,7 @@ have : fine (f x) < n%:R. near: n. exists `|floor (fine (f x))|.+1%N => //= p /=. rewrite -(@ler_nat R); apply: lt_le_trans. - rewrite -addn1 natrD (_ : `| _ |%:R = (floor (fine (f x)))%:~R); last first. + rewrite -natr1 (_ : `| _ |%:R = (floor (fine (f x)))%:~R); last first. by rewrite -[in RHS](@gez0_abs (floor _))// floor_ge0//; exact/fine_ge0/f0. by rewrite lt_succ_floor. rewrite -lte_fin (fineK fxfin) => fxn. @@ -1502,8 +1509,7 @@ rewrite (@le_lt_trans _ _ (1 / 2 ^+ n)) //. rewrite ler_subr_addl -mulrBl -lee_fin (fineK fxfin) -rfx lee_fin. rewrite (le_trans _ k1)// ler_pmul2r// -(@natrB _ _ 1) // ler_nat subn1. by rewrite leq_pred. - rewrite ler_subl_addr -mulrDl -lee_fin -(natrD _ 1) add1n. - by rewrite fineK// ltW// -rfx lte_fin. + by rewrite ler_subl_addr -mulrDl -lee_fin nat1r fineK// ltW// -rfx lte_fin. by near: n; exact: near_infty_natSinv_expn_lt. Unshelve. all: by end_near. Qed. @@ -1768,8 +1774,7 @@ wlog fg : D mD mf mg mfg / forall x, D x -> f x +? g x => [hwlogD|]; last first. have [f_ f_cvg] := approximation_sfun mD mf. have [g_ g_cvg] := approximation_sfun mD mg. apply: (emeasurable_fun_cvg (fun n x => (f_ n x + g_ n x)%:E)) => //. - move=> n; apply/EFin_measurable_fun. - by apply: (@measurable_funS _ _ _ _ setT) => //; exact: measurable_funD. + by move=> n; apply/EFin_measurable_fun/measurable_funTS/measurable_funD. move=> x Dx; under eq_fun do rewrite EFinD. by apply: ereal_cvgD; [exact: fg|exact: f_cvg|exact: g_cvg]. move=> A mA; wlog NAnoo: A mD mf mg mA / ~ (A -oo) => [hwlogA|]. @@ -1847,7 +1852,7 @@ wlog fg : D mD mf mg mfg / forall x, D x -> f x *? g x => [hwlogM|]; last first. have [g_ g_cvg] := approximation_sfun mD mg. apply: (emeasurable_fun_cvg (fun n x => (f_ n x * g_ n x)%:E)) => //. move=> n; apply/EFin_measurable_fun. - by apply: measurable_funM => //; exact: (@measurable_funS _ _ _ _ setT). + by apply: measurable_funM => //; exact: measurable_funTS. move=> x Dx; under eq_fun do rewrite EFinM. by apply: ereal_cvgM; [exact: fg|exact: f_cvg|exact: g_cvg]. move=> A mA; wlog NA0: A mD mf mg mA / ~ (A 0) => [hwlogA|]. @@ -2146,6 +2151,118 @@ Unshelve. all: by end_near. Qed. End ge0_integralM. +Section integral_indic. +Local Open Scope ereal_scope. +Variables (d : measure_display) (T : measurableType d) (R : realType) + (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D). + +Lemma integral_indic (E : set T) : measurable E -> + \int[mu]_(x in D) (\1_E x)%:E = mu (E `&` D). +Proof. +move=> mE; rewrite (_ : \1_E = indic_nnsfun R mE)// integral_nnsfun//=. +by rewrite restrict_indic sintegral_indic//; exact: measurableI. +Qed. + +End integral_indic. + +Section integralM_indic. +Local Open Scope ereal_scope. +Variables (d : measure_display) (T : measurableType d) (R : realType). +Variables (m : {measure set T -> \bar R}) (D : set T) (mD : measurable D). + +Lemma integralM_indic (f : R -> set T) (k : R) : + ((k < 0)%R -> f k = set0) -> measurable (f k) -> + \int[m]_(x in D) (k * \1_(f k) x)%:E = + k%:E * \int[m]_(x in D) (\1_(f k) x)%:E. +Proof. +move=> fk0 mfk; have [k0|k0] := ltP k 0%R. + rewrite (eq_integral (cst 0%E)) ?integral0 ?mule0; last first. + by move=> x _; rewrite fk0// indic0 mulr0. + rewrite (eq_integral (cst 0%E)) ?integral0 ?mule0// => x _. + by rewrite fk0// indic0. +under eq_integral do rewrite EFinM. +rewrite ge0_integralM//. +- exact/EFin_measurable_fun/measurable_fun_indic. +- by move=> y _; rewrite lee_fin. +Qed. + +Lemma integralM_indic_nnsfun (f : {nnsfun T >-> R}) (k : R) : + \int[m]_(x in D) (k * \1_(f @^-1` [set k]) x)%:E = + k%:E * \int[m]_(x in D) (\1_(f @^-1` [set k]) x)%:E. +Proof. +rewrite (@integralM_indic (fun k => f @^-1` [set k]))// => k0. +by rewrite preimage_nnfun0. +Qed. + +End integralM_indic. +Arguments integralM_indic {d T R m D} mD f. + +Section integral_mscale. +Local Open Scope ereal_scope. +Variables (d : measure_display) (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). + +Let integral_mscale_indic E : measurable E -> + \int[mscale k m]_(x in D) (\1_E x)%:E = + k%:num%:E * \int[m]_(x in D) (\1_E x)%:E. +Proof. by move=> ?; rewrite !integral_indic. Qed. + +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. +Proof. +under [LHS]eq_integral do rewrite fimfunE -sumEFin. +rewrite [LHS]ge0_integral_sum//; last 2 first. + - move=> r. + exact/EFin_measurable_fun/measurable_funrM/measurable_fun_indic. + - by move=> n x _; rewrite EFinM nnfun_muleindic_ge0. +rewrite -[RHS]ge0_integralM//; last 2 first. + - exact/EFin_measurable_fun/measurable_funTS. + - by move=> x _; rewrite lee_fin. +under [RHS]eq_integral. + move=> x xD; rewrite fimfunE -sumEFin ge0_sume_distrr//; last first. + by move=> r _; rewrite EFinM nnfun_muleindic_ge0. + over. +rewrite [RHS]ge0_integral_sum//; last 2 first. + - move=> r; apply/EFin_measurable_fun/measurable_funrM/measurable_funrM. + exact/measurable_fun_indic. + - by move=> n x _; rewrite EFinM mule_ge0// nnfun_muleindic_ge0. +apply eq_bigr => r _; rewrite ge0_integralM//. +- by rewrite !integralM_indic_nnsfun//= integral_mscale_indic// muleCA. +- exact/EFin_measurable_fun/measurable_funrM/measurable_fun_indic. +- by move=> t _; rewrite nnfun_muleindic_ge0. +Qed. + +Lemma ge0_integral_mscale (mf : measurable_fun D f) : + (forall x, D x -> 0 <= f x) -> + \int[mscale k m]_(x in D) f x = k%:num%:E * \int[m]_(x in D) f x. +Proof. +move=> f0; have [f_ [ndf_ f_f]] := approximation mD mf f0. +transitivity (lim (fun n => \int[mscale k m]_(x in D) (f_ n x)%:E)). + rewrite -monotone_convergence//=. + - by apply eq_integral => x /[!inE] xD; apply/esym/cvg_lim => //=; exact: f_f. + - by move=> n; exact/EFin_measurable_fun/measurable_funTS. + - by move=> n x _; rewrite lee_fin. + - by move=> x _ a b /ndf_ /lefP; rewrite lee_fin. +rewrite (_ : \int[m]_(x in D) _ = + lim (fun n => \int[m]_(x in D) (f_ n x)%:E)); last first. + rewrite -monotone_convergence//=. + - by apply: eq_integral => x /[!inE] xD; apply/esym/cvg_lim => //; exact: f_f. + - by move=> n; exact/EFin_measurable_fun/measurable_funTS. + - by move=> n x _; rewrite lee_fin. + - by move=> x _ a b /ndf_ /lefP; rewrite lee_fin. +rewrite -ereal_limrM//. + by congr (lim _); apply/funext => n /=; rewrite integral_mscale_nnsfun. +apply/ereal_nondecreasing_is_cvg => a b ab; apply ge0_le_integral => //. +- by move=> x _; rewrite lee_fin. +- exact/EFin_measurable_fun/measurable_funTS. +- by move=> x _; rewrite lee_fin. +- exact/EFin_measurable_fun/measurable_funTS. + by move=> x _; rewrite lee_fin; move/ndf_ : ab => /lefP. +Qed. + +End integral_mscale. + Section fatou. Local Open Scope ereal_scope. Variables (d : measure_display) (T : measurableType d) (R : realType). @@ -2272,50 +2389,56 @@ Qed. End integral_cst. -Section integral_ind. -Local Open Scope ereal_scope. -Variables (d : measure_display) (T : measurableType d) (R : realType). -Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D). - -Lemma integral_indic (E : set T) : measurable E -> - \int[mu]_(x in D) (\1_E x)%:E = mu (E `&` D). -Proof. -move=> mE; rewrite (_ : \1_E = indic_nnsfun R mE)// integral_nnsfun//=. -by rewrite restrict_indic sintegral_indic//; exact: measurableI. -Qed. - -End integral_ind. - -Section integralM_indic. +Section transfer. Local Open Scope ereal_scope. -Variables (d : measure_display) (T : measurableType d) (R : realType). -Variables (m : {measure set T -> \bar R}) (D : set T) (mD : measurable D). - -Lemma integralM_indic (f : R -> set T) (k : R) : - ((k < 0)%R -> f k = set0) -> measurable (f k) -> - \int[m]_(x in D) (k * \1_(f k) x)%:E = k%:E * \int[m]_(x in D) (\1_(f k) x)%:E. -Proof. -move=> fk0 mfk; have [k0|k0] := ltP k 0%R. - rewrite (eq_integral (cst 0%E)) ?integral0 ?mule0; last first. - by move=> x _; rewrite fk0// indic0 mulr0. - rewrite (eq_integral (cst 0%E)) ?integral0 ?mule0// => x _. - by rewrite fk0// indic0. -under eq_integral do rewrite EFinM. -rewrite ge0_integralM//. -- apply/EFin_measurable_fun/(@measurable_funS _ _ _ _ setT) => //. - by rewrite (_ : \1_(f k) = mindic R mfk). -- by move=> y _; rewrite lee_fin. -Qed. +Variables (d1 d2 : _) (X : measurableType d1) (Y : measurableType d2). +Variables (phi : X -> Y) (mphi : measurable_fun setT phi). +Variables (R : realType) (mu : {measure set X -> \bar R}). -Lemma integralM_indic_nnsfun (f : {nnsfun T >-> R}) (k : R) : - \int[m]_(x in D) (k * \1_(f @^-1` [set k]) x)%:E = - k%:E * \int[m]_(x in D) (\1_(f @^-1` [set k]) x)%:E. +Lemma integral_pushforward (f : Y -> \bar R) : + measurable_fun setT f -> (forall y, 0 <= f y) -> + \int[pushforward mu mphi]_y f y = \int[mu]_x (f \o phi) x. Proof. -rewrite (@integralM_indic (fun k => f @^-1` [set k]))// => k0. -by rewrite preimage_nnfun0. +move=> mf f0. +have [f_ [ndf_ f_f]] := approximation measurableT mf (fun t _ => f0 t). +transitivity (lim (fun n => \int[pushforward mu mphi]_x (f_ n x)%:E)). + rewrite -monotone_convergence//. + - by apply: eq_integral => y _; apply/esym/cvg_lim => //; exact: f_f. + - by move=> n; exact/EFin_measurable_fun. + - by move=> n y _; rewrite lee_fin. + - by move=> y _ m n mn; rewrite lee_fin; apply/lefP/ndf_. +rewrite (_ : (fun _ => _) = (fun n => \int[mu]_x (EFin \o f_ n \o phi) x)). + rewrite -monotone_convergence//; last 3 first. + - move=> n /=; apply: measurable_fun_comp; first exact: measurable_fun_EFin. + by apply: measurable_fun_comp => //; exact: measurable_sfun. + - by move=> n x _ /=; rewrite lee_fin. + - by move=> x _ m n mn; rewrite lee_fin; exact/lefP/ndf_. + by apply: eq_integral => x _ /=; apply/cvg_lim => //; exact: f_f. +apply/funext => n. +have mfnphi r : measurable (f_ n @^-1` [set r] \o phi). + rewrite -[_ \o _]/(phi @^-1` (f_ n @^-1` [set r])) -(setTI (_ @^-1` _)). + exact/mphi. +transitivity (\sum_(k <- fset_set (range (f_ n))) + \int[mu]_x (k * \1_((f_ n @^-1` [set k]) \o phi) x)%:E). + under eq_integral do rewrite fimfunE -sumEFin. + rewrite ge0_integral_sum//; last 2 first. + - move=> y; apply/EFin_measurable_fun; apply: measurable_funM. + exact: measurable_fun_cst. + by rewrite (_ : \1_ _ = mindic R (measurable_sfunP (f_ n) y)). + - by move=> y x _; rewrite nnfun_muleindic_ge0. + apply eq_bigr => r _; rewrite integralM_indic_nnsfun// integral_indic//=. + rewrite (integralM_indic _ (fun r => f_ n @^-1` [set r] \o phi))//. + by congr (_ * _); rewrite [RHS](@integral_indic). + by move=> r0; rewrite preimage_nnfun0. +rewrite -ge0_integral_sum//; last 2 first. + - move=> r; apply/EFin_measurable_fun; apply: measurable_funM. + exact: measurable_fun_cst. + by rewrite (_ : \1_ _ = mindic R (mfnphi r)). + - by move=> r x _; rewrite nnfun_muleindic_ge0. +by apply eq_integral => x _; rewrite sumEFin -fimfunE. Qed. -End integralM_indic. +End transfer. Section integral_dirac. Local Open Scope ereal_scope. @@ -2331,7 +2454,7 @@ transitivity (lim (fun n => \int[\d_ a]_(x in D) (f_ n x)%:E)). rewrite -monotone_convergence//. - apply: eq_integral => x Dx; apply/esym/cvg_lim => //; apply: f_f. by rewrite inE in Dx. - - by move=> n; apply/EFin_measurable_fun; exact/(@measurable_funS _ _ _ _ setT). + - by move=> n; apply/EFin_measurable_fun; exact/measurable_funTS. - by move=> *; rewrite lee_fin. - by move=> x _ m n mn; rewrite lee_fin; exact/lefP/ndf_. rewrite (_ : (fun _ => _) = (fun n => (f_ n a)%:E)). @@ -2345,11 +2468,8 @@ rewrite ge0_integral_sum//. rewrite big1_fset ?adde0// => r; rewrite !inE => /andP[rfna _] _. rewrite integral_indic//= diracE memNset ?mule0//. by apply/not_andP; left; exact/nesym/eqP. -- move=> r; apply/EFin_measurable_fun. - apply: measurable_funM => //; first exact: measurable_fun_cst. - apply: (@measurable_funS _ _ _ _ setT) => //. - by rewrite (_ : \1_ _ = mindic R (measurable_sfunP (f_ n) r)). -- by move=> r x _; rewrite muleindic_ge0. +- by move=> r; exact/EFin_measurable_fun/measurable_funrM/measurable_fun_indic. +- by move=> r x _; rewrite nnfun_muleindic_ge0. Qed. Lemma integral_dirac (f : T -> \bar R) (mf : measurable_fun D f) : @@ -2386,10 +2506,8 @@ Proof. under eq_integral do rewrite fimfunE -sumEFin. rewrite ge0_integral_sum//; last 2 first. - move=> r /=; apply: measurable_fun_comp => //. - apply: measurable_funM => //. - exact: measurable_fun_cst. - by rewrite (_ : \1_ _ = mindic R (measurable_sfunP f r)). - - by move=> r t _; rewrite EFinM muleindic_ge0. + exact/measurable_funrM/measurable_fun_indic. + - by move=> r t _; rewrite EFinM nnfun_muleindic_ge0. transitivity (\sum_(i <- fset_set (range f)) (\sum_(n < N) i%:E * \int[m_ n]_x (\1_(f @^-1` [set i]) x)%:E)). apply eq_bigr => r _. @@ -2443,7 +2561,7 @@ rewrite big_ord_recr/= -ih. rewrite (_ : _ m_ N.+1 = measure_add [the measure _ _ of msum m_ N] (m_ N)); last first. by apply/funext => A; rewrite measure_addE /msum/= big_ord_recr. have mf_ n : measurable_fun D (fun x => (f_ n x)%:E). - by apply: (@measurable_funS _ _ _ _ setT) => //; exact/EFin_measurable_fun. + exact/measurable_funTS/EFin_measurable_fun. have f_ge0 n x : D x -> 0 <= (f_ n x)%:E by move=> Dx; rewrite lee_fin. have cvg_f_ (m : {measure set T -> \bar R}) : cvg (fun x => \int[m]_(x0 in D) (f_ x x0)%:E). apply: ereal_nondecreasing_is_cvg => a b ab. @@ -2498,11 +2616,9 @@ Lemma integral_measure_series_nnsfun (D : set T) (mD : measurable D) Proof. under eq_integral do rewrite fimfunE -sumEFin. rewrite ge0_integral_sum//; last 2 first. - - move=> r /=. - apply: measurable_fun_comp => //. - apply: measurable_funM => //; first exact: measurable_fun_cst. - by rewrite (_ : \1_ _ = mindic R (measurable_sfunP f r)). - - by move=> r t _; rewrite EFinM muleindic_ge0. + - move=> r /=; apply: measurable_fun_comp => //. + exact/measurable_funrM/measurable_fun_indic. + - by move=> r t _; rewrite EFinM nnfun_muleindic_ge0. transitivity (\sum_(i <- fset_set (range f)) (\sum_(n r _. @@ -2977,17 +3093,13 @@ have [M M0 muM] : exists2 M, (0 <= M)%R & exists (fine (\int[mu]_(x in D) `|f x|)); first exact/fine_ge0/integral_ge0. move=> n. rewrite -integral_indic// -ge0_integralM//; last 2 first. - - apply: measurable_fun_comp=> //; apply: (@measurable_funS _ _ _ _ setT)=>//. - by rewrite (_ : \1_ _ = indic_nnsfun R mE). + - by apply: measurable_fun_comp=> //; exact/measurable_fun_indic. - by move=> *; rewrite lee_fin. rewrite fineK//; last first. by case: fint => _ foo; rewrite ge0_fin_numE//; exact: integral_ge0. apply: ge0_le_integral => //. - by move=> *; rewrite lee_fin /indic. - - apply/EFin_measurable_fun; apply: measurable_funM=>//. - + exact: measurable_fun_cst. - + apply: (@measurable_funS _ _ _ _ setT)=>//. - by rewrite (_ : \1_ _ = indic_nnsfun R mE)//. + - exact/EFin_measurable_fun/measurable_funrM/measurable_fun_indic. - by apply: measurable_fun_comp => //; case: fint. - move=> x Dx; rewrite /= indicE. have [|xE] := boolP (x \in E); last by rewrite mule0. @@ -3001,7 +3113,7 @@ apply/negP; rewrite -ltNge. rewrite -[X in _ * X](@fineK _ (mu (E `&` D))); last first. by rewrite fin_numElt muEDoo andbT (lt_le_trans _ (measure_ge0 _ _)). rewrite lte_fin -ltr_pdivr_mulr. - rewrite -addn1 natrD natr_absz ger0_norm. + rewrite -natr1 natr_absz ger0_norm. by rewrite (le_lt_trans (ceil_ge _))// ltr_addl. by rewrite ceil_ge0// divr_ge0//; apply/le0R/measure_ge0; exact: measurableI. rewrite -lte_fin fineK. @@ -3289,16 +3401,13 @@ have le_f_M t : D t -> `|f t| <= M%:E * (f' t)%:E. have : 0 <= \int[mu]_(x in D) `|f x| <= `|M|%:E * mu Df_neq0. rewrite integral_ge0//= /Df_neq0 -{2}(setIid D) setIAC -integral_indic//. rewrite -/Df_neq0 -ge0_integralM//; last 2 first. - - apply: measurable_fun_comp=> //; apply: (@measurable_funS _ _ _ _ setT) => //. - by rewrite (_ : \1_ _ = mindic R mDf_neq0). - - by move=> x Dx; rewrite lee_fin. + - by apply: measurable_fun_comp=> //; exact: measurable_fun_indic. + - by move=> x ?; rewrite lee_fin. apply: ge0_le_integral => //. - exact: measurable_fun_comp. - by move=> x Dx; rewrite mule_ge0// lee_fin. - apply: emeasurable_funM; first exact: measurable_fun_cst. - apply: measurable_fun_comp => //. - apply: (@measurable_funS _ _ _ _ setT)=> //. - by rewrite (_ : \1_ _ = mindic R mDf_neq0)//. + by apply: measurable_fun_comp => //; exact: measurable_fun_indic. - move=> x Dx. rewrite (le_trans (le_f_M _ Dx))// lee_fin /f' indicE. by case: (_ \in _) => //; rewrite ?mulr1 ?mulr0// ler_norm. @@ -3332,7 +3441,7 @@ move=> mf; split=> [iDf0|Df0]. - rewrite inE unitfE fine_eq0 // abse_eq0 ft0/=; apply/fine_gt0. by rewrite lt_neqAle abse_ge0 -ge0_fin_numE// eq_sym abse_eq0 ft0. - by rewrite inE unitfE invr_eq0 pnatr_eq0 /= invr_gt0. - rewrite invrK /m -addn1 natrD natr_absz ger0_norm ?ceil_ge0//. + rewrite invrK /m -natr1 natr_absz ger0_norm ?ceil_ge0//. apply: (@le_trans _ _ ((fine `|f t|)^-1 + 1)%R); first by rewrite ler_addl. by rewrite ler_add2r// ceil_ge. by split => //; apply: contraTN nft => /eqP ->; rewrite abse0 -ltNge. @@ -3353,9 +3462,9 @@ have -> : (fun x => `|f x|) = (fun x => lim (f_^~ x)). rewrite /= (@ger0_norm _ n%:R)// ger0_norm; last first. by rewrite subr_ge0 ler_pdivr_mulr ?mul1r ?ler_addr. rewrite -{1}(@divrr _ (1 + n%:R)%R) ?unitfE; last first. - by rewrite gt_eqF// {1}(_ : 1 = 1%:R)%R // -natrD add1n. + by rewrite gt_eqF// {1}(_ : 1 = 1%:R)%R // natrS. rewrite -mulrBl addrK ltr_pdivr_mulr; last first. - by rewrite {1}(_ : 1 = 1%:R)%R // -natrD add1n. + by rewrite {1}(_ : 1 = 1%:R)%R // natrS. rewrite mulrDr mulr1 ltr_spsaddl// -ltr_pdivr_mull// mulr1. near: n. exists `|ceil (1 + e%:num^-1)|%N => // n /=. @@ -3409,9 +3518,8 @@ move=> mN mD ND mf muN0; rewrite integralEindic//. rewrite (eq_integral (fun x => `|f x * (\1_N x)%:E|)); last first. by move=> t _; rewrite abseM (@gee0_abs _ (\1_N t)%:E)// lee_fin. apply/ae_eq_integral_abs => //. - apply: emeasurable_funM => //; first exact: (@measurable_funS _ _ _ _ D). - apply/EFin_measurable_fun/(@measurable_funS _ _ _ _ setT) => //. - by rewrite (_ : \1_N = mindic R mN). + apply: emeasurable_funM => //; first exact: (measurable_funS mD). + exact/EFin_measurable_fun/measurable_fun_indic. exists N; split => // t /= /not_implyP[_]; rewrite indicE. by have [|] := boolP (t \in N); rewrite ?inE ?mule0. Qed. @@ -3439,7 +3547,7 @@ pose oneN : {nnsfun T >-> R} := [the {nnsfun T >-> R} of mindic R mN]. have intone : mu.-integrable D (fun x => f x * (oneN x)%:E). split. apply: emeasurable_funM=> //; apply/EFin_measurable_fun. - exact: (@measurable_funS _ _ _ _ setT). + exact: measurable_funTS. rewrite (eq_integral (fun x => `|f x| * (\1_N x)%:E)); last first. by move=> t _; rewrite abseM (@gee0_abs _ (\1_N t)%:E) // lee_fin. rewrite -integral_setI_indic// (@integral_abs_eq0 D)//. @@ -3449,18 +3557,17 @@ have h1 : mu.-integrable D f <-> mu.-integrable D (fun x => f x * (oneCN x)%:E). split=> [intf|intCf]. split. apply: emeasurable_funM=> //; apply/EFin_measurable_fun => //. - exact: (@measurable_funS _ _ _ _ setT). + exact: measurable_funTS. rewrite (eq_integral (fun x => `|f x| * (\1_(~` N) x)%:E)); last first. by move=> t _; rewrite abseM (@gee0_abs _ (\1_(~` N) t)%:E) // lee_fin. rewrite -integral_setI_indic//; case: intf => _; apply: le_lt_trans. by apply: subset_integral => //; [exact:measurableI|exact:measurable_fun_comp]. split => //; rewrite (funID mN f) -/oneCN -/oneN. have ? : measurable_fun D (fun x : T => f x * (oneCN x)%:E). - apply: emeasurable_funM=> //. - by apply/EFin_measurable_fun; exact: (@measurable_funS _ _ _ _ setT). + by apply: emeasurable_funM=> //; exact/EFin_measurable_fun/measurable_funTS. have ? : measurable_fun D (fun x : T => f x * (oneN x)%:E). apply: emeasurable_funM => //. - by apply/EFin_measurable_fun; apply: (@measurable_funS _ _ _ _ setT). + exact/EFin_measurable_fun/measurable_funTS. apply: (@le_lt_trans _ _ (\int[mu]_(x in D) (`|f x * (oneCN x)%:E| + `|f x * (oneN x)%:E|))). apply: ge0_le_integral => //. @@ -3475,7 +3582,7 @@ have h2 : mu.-integrable (D `\` N) f <-> split=> [intCf|intCf]. split. apply: emeasurable_funM=> //; apply/EFin_measurable_fun => //. - exact: (@measurable_funS _ _ _ _ setT). + exact: measurable_funTS. rewrite (eq_integral (fun x => `|f x| * (\1_(~` N) x)%:E)); last first. by move=> t _; rewrite abseM (@gee0_abs _ (\1_(~` N) t)%:E)// lee_fin. rewrite -integral_setI_indic //; case: intCf => _; apply: le_lt_trans. @@ -3499,10 +3606,10 @@ move=> mN mD mf f0 muN0. rewrite {1}(funID mN f) ge0_integralD//; last 4 first. - by move=> x Dx; apply: mule_ge0 => //; [exact: f0|rewrite lee_fin]. - apply: emeasurable_funM=> //; apply/EFin_measurable_fun=> //. - exact: (@measurable_funS _ _ _ _ setT). + exact: measurable_funTS. - by move=> x Dx; apply: mule_ge0 => //; [exact: f0|rewrite lee_fin]. - apply: emeasurable_funM=> //; apply/EFin_measurable_fun=> //. - exact: (@measurable_funS _ _ _ _ setT). + exact: measurable_funTS. rewrite -integral_setI_indic//; last exact: measurableC. rewrite -integral_setI_indic// [X in _ + X = _](_ : _ = 0) ?adde0//. rewrite (eq_integral (abse \o f)); last first. @@ -3520,12 +3627,12 @@ Proof. move=> mD mf mg f0 g0 [N [mN N0 subN]]. rewrite integralEindic// [RHS]integralEindic//. rewrite (negligible_integral mN)//; last 2 first. - - apply: emeasurable_funM => //; apply/EFin_measurable_fun. - by apply: (@measurable_funS _ _ _ _ setT) => //; rewrite (_ : \1_D = mindic R mD). + - apply: emeasurable_funM => //. + exact/EFin_measurable_fun/measurable_fun_indic. - by move=> x Dx; apply: mule_ge0 => //; [exact: f0|rewrite lee_fin]. rewrite [RHS](negligible_integral mN)//; last 2 first. - - apply: emeasurable_funM => //; apply/EFin_measurable_fun. - by apply: (@measurable_funS _ _ _ _ setT) => //; rewrite (_ : \1_D = mindic R mD). + - apply: emeasurable_funM => //. + exact/EFin_measurable_fun/measurable_fun_indic. - by move=> x Dx; apply: mule_ge0 => //; [exact: g0|rewrite lee_fin]. - apply: eq_integral => x;rewrite in_setD => /andP[_ xN]. apply: contrapT; rewrite indicE; have [|?] := boolP (x \in D). @@ -3682,7 +3789,7 @@ Proof. have -> : \sum_(n \bar R. rewrite nneseries_esum// (_ : [set _ | _] = setT); last exact/seteqP. rewrite [in LHS](esumID A)// !setTI [X in _ + X](_ : _ = 0) ?adde0//. - by apply esum0 => i Ai; rewrite /= /dirac indicE memNset. + by apply esum1 => i Ai; rewrite /= /dirac indicE memNset. rewrite /counting/=; case: ifPn => /asboolP finA. by rewrite -finite_card_dirac. by rewrite infinite_card_dirac. @@ -3973,9 +4080,6 @@ have f_g' n x : D x -> `|f_' n x| <= g' x. have [/=|/= xN] := boolP (x \in N); first by rewrite normr0. apply: contrapT => fg; move: xN; apply/negP; rewrite negbK inE; left; right. by apply: subN2 => /= /(_ n Dx). -have ? : measurable_fun D (\1_(D `\` N) : T -> R). - apply: (@measurable_funS _ _ _ _ setT) => //. - by rewrite (_ : \1_ _ = mindic R (measurableD mD mN)). have mu_ n : measurable_fun D (f_' n). apply/(measurable_restrict (f_ n) (measurableD mD mN) _ _).1 => //. by apply: measurable_funS (mf_ _) => // x []. @@ -4001,7 +4105,7 @@ split. apply/funext => n; apply: ae_eq_integral => //. + apply: measurable_fun_comp => //; apply: emeasurable_funB => //. apply/(measurable_restrict _ (measurableD _ _) _ _).1 => //. - by apply: (@measurable_funS _ _ _ _ D) => // x []. + by apply: (measurable_funS mD) => // x []. + by rewrite /g_; apply: measurable_fun_comp => //; exact: emeasurable_funB. + exists N; split => //; rewrite -(setCK N); apply: subsetC => x /= Nx Dx. by rewrite /f_' /f' /restrict mem_set. @@ -4013,7 +4117,7 @@ split. set Y := (X in _ -> _ --> X); rewrite [X in _ --> X -> _](_ : _ = Y) //. apply: ae_eq_integral => //. apply/(measurable_restrict _ (measurableD _ _) _ _).1 => //. - by apply: (@measurable_funS _ _ _ _ D) => // x []. + by apply: (measurable_funS mD) => // x []. exists N; split => //; rewrite -(setCK N); apply: subsetC => x /= Nx Dx. by rewrite /f' /restrict mem_set. Qed. @@ -4029,29 +4133,19 @@ Variables (d1 d2 : measure_display). Variables (T1 : measurableType d1) (T2 : measurableType d2). Implicit Types (A : set (T1 * T2)). -Lemma mem_set_pair1 x y A : - (y \in [set y' | (x, y') \in A]) = ((x, y) \in A). -Proof. by apply/idP/idP => [|]; [rewrite inE|rewrite !inE /= inE]. Qed. - -Lemma mem_set_pair2 x y A : - (x \in [set x' | (x', y) \in A]) = ((x, y) \in A). -Proof. by apply/idP/idP => [|]; [rewrite inE|rewrite 2!inE /= inE]. Qed. - Variable R : realType. Lemma measurable_xsection A x : measurable A -> measurable (xsection A x). Proof. move=> mA. pose f : T1 * T2 -> \bar R := EFin \o indic_nnsfun R mA. -have mf : measurable_fun setT f by apply/EFin_measurable_fun/measurable_funP. +have mf : measurable_fun setT f by exact/EFin_measurable_fun/measurable_funP. have _ : (fun y => (y \in xsection A x)%:R%:E) = f \o (fun y => (x, y)). - rewrite funeqE => y /=; rewrite /xsection /f. - by rewrite /= /mindic indicE/= mem_set_pair1. + by apply/funext => y/=; rewrite mem_xsection. have -> : xsection A x = (fun y => f (x, y)) @^-1` [set 1%E]. - rewrite predeqE => y; split; rewrite /xsection /preimage /= /f. - by rewrite /= /mindic indicE/= => ->. - rewrite /= /mindic indicE. - by case: (_ \in _) => //= -[] /eqP; rewrite eq_sym oner_eq0. + apply/funext => y/=; rewrite -(in_setE (xsection A x)) mem_xsection. + rewrite /f/= mindicE//; apply/propext; split=> [->//|[]]. + by case: (_ \in _)=> // /esym/eqP; rewrite oner_eq0. by rewrite -(setTI (_ @^-1` _)); exact: measurable_fun_prod1. Qed. @@ -4061,26 +4155,28 @@ move=> mA. pose f : T1 * T2 -> \bar R := EFin \o indic_nnsfun R mA. have mf : measurable_fun setT f by apply/EFin_measurable_fun/measurable_funP. have _ : (fun x => (x \in ysection A y)%:R%:E) = f \o (fun x => (x, y)). - rewrite funeqE => x /=; rewrite /ysection /f. - by rewrite /= /mindic indicE mem_set_pair2. + by apply/funext => x/=; rewrite mem_ysection. have -> : ysection A y = (fun x => f (x, y)) @^-1` [set 1%E]. - rewrite predeqE => x; split; rewrite /ysection /preimage /= /f. - by rewrite /= /mindic indicE => ->. - rewrite /= /mindic indicE. - by case: (_ \in _) => //= -[] /eqP; rewrite eq_sym oner_eq0. + apply/funext => x/=; rewrite -(in_setE (ysection A y)) mem_ysection. + rewrite /f/= mindicE//; apply/propext; split=> [->//|[]]. + by case: (_ \in _)=> // /esym/eqP; rewrite oner_eq0. by rewrite -(setTI (_ @^-1` _)); exact: measurable_fun_prod2. Qed. End measurable_section. Section ndseq_closed_B. -Variables (d1 d2 : measure_display). -Variables (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). +Variables (d1 d2 : _) (T1 : measurableType d1) (T2 : measurableType d2) + (R : realType). Implicit Types A : set (T1 * T2). Section xsection. -Variables (pt2 : T2) (m2 : {measure set T2 -> \bar R}). -Let phi A := m2 \o xsection A. +Variables (pt2 : T2) (m2 : T1 -> {measure set T2 -> \bar R}). +(* the generalization from m2 : {measure set T2 -> \bar R}t to + T1 -> {measure set T2 -> \bar R} is needed to develop the theory + of kernels; the original type was sufficient for the the development + of the theory of integration *) +Let phi A x := m2 x (xsection A x). Let B := [set A | measurable A /\ measurable_fun setT (phi A)]. Lemma xsection_ndseq_closed : ndseq_closed B. @@ -4091,9 +4187,8 @@ have phiF x : (fun i => phi (F i) x) --> phi (\bigcup_i F i) x. rewrite /phi /= xsection_bigcup; apply: nondecreasing_cvg_mu. - by move=> n; apply: measurable_xsection; case: (BF n). - by apply: bigcupT_measurable => i; apply: measurable_xsection; case: (BF i). - - move=> m n mn; apply/subsetPset => y; rewrite /xsection/= !inE. - by have /subsetPset FmFn := ndF _ _ mn; exact: FmFn. -apply: (emeasurable_fun_cvg (phi \o F)). + - by move=> m n mn; exact/subsetPset/le_xsection/subsetPset/ndF. +apply: (emeasurable_fun_cvg (phi \o F)) => //. - by move=> i; have [] := BF i. - by move=> x _; exact: phiF. Qed. @@ -4112,9 +4207,8 @@ have psiF x : (fun i => psi (F i) x) --> psi (\bigcup_i F i) x. rewrite /psi /= ysection_bigcup; apply: nondecreasing_cvg_mu. - by move=> n; apply: measurable_ysection; case: (BF n). - by apply: bigcupT_measurable => i; apply: measurable_ysection; case: (BF i). - - move=> m n mn; apply/subsetPset => y; rewrite /ysection/= !inE. - by have /subsetPset FmFn := ndF _ _ mn; exact: FmFn. -apply: (emeasurable_fun_cvg (psi \o F)). + - by move=> m n mn; exact/subsetPset/le_ysection/subsetPset/ndF. +apply: (emeasurable_fun_cvg (psi \o F)) => //. - by move=> i; have [] := BF i. - by move=> x _; exact: psiF. Qed. @@ -4151,8 +4245,7 @@ have CB : C `<=` B. rewrite funeqE => x; rewrite indicE /phi /m2/= /mrestr. have [xX1|xX1] := boolP (x \in X1); first by rewrite mule1 in_xsectionM. by rewrite mule0 notin_xsectionM// set0I measure0. - apply/measurable_funeM/EFin_measurable_fun. - by rewrite (_ : \1_ _ = mindic R mX1). + exact/measurable_funeM/EFin_measurable_fun/measurable_fun_indic. suff monoB : monotone_class setT B by exact: monotone_class_subset. split => //; [exact: CB| |exact: xsection_ndseq_closed]. move=> X Y XY [mX mphiX] [mY mphiY]; split; first exact: measurableD. @@ -4193,8 +4286,7 @@ have CB : C `<=` B. rewrite funeqE => y; rewrite indicE /psi /m1/= /mrestr. have [yX2|yX2] := boolP (y \in X2); first by rewrite mule1 in_ysectionM. by rewrite mule0 notin_ysectionM// set0I measure0. - apply/measurable_funeM/EFin_measurable_fun. - by rewrite (_ : \1_ _ = mindic R mX2). + exact/measurable_funeM/EFin_measurable_fun/measurable_fun_indic. suff monoB : monotone_class setT B by exact: monotone_class_subset. split => //; [exact: CB| |exact: ysection_ndseq_closed]. move=> X Y XY [mX mphiX] [mY mphiY]; split; first exact: measurableD. @@ -4361,7 +4453,7 @@ rewrite (_ : (fun _ => _) = fun x => m2 A2 * (\1_A1 x)%:E); last first. [rewrite in_xsectionM// mule1|rewrite mule0 notin_xsectionM]. rewrite ge0_integralM//. - by rewrite muleC integral_indic// setIT. -- by apply: measurable_fun_comp => //; rewrite (_ : \1_ _ = mindic R mA1). +- by apply: measurable_fun_comp => //; exact/measurable_fun_indic. - by move=> x _; rewrite lee_fin. Qed. @@ -4475,7 +4567,7 @@ have mA1A2 : measurable (A1 `*` A2) by apply: measurableM. transitivity (\int[m2]_y (m1 \o ysection (A1 `*` A2)) y) => //. rewrite (_ : _ \o _ = fun y => m1 A1 * (\1_A2 y)%:E). rewrite ge0_integralM//; last 2 first. - - by apply: measurable_fun_comp => //; rewrite (_ : \1_ _ = mindic R mA2). + - by apply: measurable_fun_comp => //; exact/measurable_fun_indic. - by move=> y _; rewrite lee_fin. by rewrite integral_indic ?setIT ?mul1e. rewrite funeqE => y; rewrite indicE. @@ -4529,10 +4621,7 @@ rewrite funeqE => x; rewrite /= -(setTI (xsection _ _)). rewrite -integral_indic//; last exact: measurable_xsection. rewrite /F /fubini_F -(setTI (xsection _ _)). rewrite integral_setI_indic; [|exact: measurable_xsection|by []]. -apply: eq_integral => y _ /=; rewrite indicT mul1e /f !indicE. -have [|] /= := boolP (y \in xsection _ _). - by rewrite inE /xsection /= => ->. -by rewrite /xsection /= notin_set /= => /negP/negbTE ->. +by apply: eq_integral => y _ /=; rewrite indicT mul1e /f !indicE mem_xsection. Qed. Lemma indic_fubini_tonelli_GE : G = m1 \o ysection A. @@ -4541,10 +4630,7 @@ rewrite funeqE => y; rewrite /= -(setTI (ysection _ _)). rewrite -integral_indic//; last exact: measurable_ysection. rewrite /F /fubini_F -(setTI (ysection _ _)). rewrite integral_setI_indic; [|exact: measurable_ysection|by []]. -apply: eq_integral => x _ /=; rewrite indicT mul1e /f 2!indicE. -have [|] /= := boolP (x \in ysection _ _). - by rewrite inE /xsection /= => ->. -by rewrite /xsection /= notin_set /= => /negP/negbTE ->. +by apply: eq_integral => x _ /=; rewrite indicT mul1e /f 2!indicE mem_ysection. Qed. Lemma indic_measurable_fun_fubini_tonelli_F : measurable_fun setT F. @@ -4590,16 +4676,13 @@ rewrite funeqE => x; rewrite /F /fubini_F [in LHS]/=. under eq_fun do rewrite fimfunE -sumEFin. rewrite ge0_integral_sum //; last 2 first. - move=> i; apply/EFin_measurable_fun => //; apply: measurable_funrM => //. - apply/measurable_fun_prod1 => //. - (*NB: we shouldn't need the following rewriting*) - by rewrite (_ : \1_ _ = mindic R (measurable_sfunP f i)). - - by move=> r y _; rewrite EFinM; exact: muleindic_ge0. + exact/measurable_fun_prod1/measurable_fun_indic. + - by move=> r y _; rewrite EFinM nnfun_muleindic_ge0. apply: eq_fbigr => i; rewrite in_fset_set// inE => -[/= t _ <-{i} _]. under eq_fun do rewrite EFinM. rewrite ge0_integralM//; last by rewrite lee_fin. - by rewrite -/((m2 \o xsection _) x) -indic_fubini_tonelli_FE. -- apply/EFin_measurable_fun/measurable_fun_prod1. - by rewrite (_ : \1_ _ = mindic R (measurable_sfunP f (f t))). +- exact/EFin_measurable_fun/measurable_fun_prod1/measurable_fun_indic. - by move=> y _; rewrite lee_fin. Qed. @@ -4616,15 +4699,13 @@ rewrite funeqE => y; rewrite /G /fubini_G [in LHS]/=. under eq_fun do rewrite fimfunE -sumEFin. rewrite ge0_integral_sum //; last 2 first. - move=> i; apply/EFin_measurable_fun => //; apply: measurable_funrM => //. - apply/measurable_fun_prod2 => //. - by rewrite (_ : \1_ _ = mindic R (measurable_sfunP f i)). - - by move=> r x _; rewrite EFinM; exact: muleindic_ge0. + exact/measurable_fun_prod2/measurable_fun_indic. + - by move=> r x _; rewrite EFinM nnfun_muleindic_ge0. apply: eq_fbigr => i; rewrite in_fset_set// inE => -[/= t _ <-{i} _]. under eq_fun do rewrite EFinM. rewrite ge0_integralM//; last by rewrite lee_fin. - by rewrite -/((m1 \o ysection _) y) -indic_fubini_tonelli_GE. -- apply/EFin_measurable_fun/measurable_fun_prod2. - by rewrite (_ : \1_ _ = mindic R (measurable_sfunP f (f t))). +- exact/EFin_measurable_fun/measurable_fun_prod2/measurable_fun_indic. - by move=> x _; rewrite lee_fin. Qed. @@ -4642,15 +4723,14 @@ Lemma sfun_fubini_tonelli1 : \int[m]_z (f z)%:E = \int[m1]_x F x. Proof. under [LHS]eq_integral do rewrite EFinf; rewrite ge0_integral_sum //; last 2 first. - - move=> r; apply/EFin_measurable_fun/measurable_funrM => //. - by rewrite (_ : \1_ _ = mindic R (measurable_sfunP f r)). - - by move=> r /= z _; exact: muleindic_ge0. + - move=> r. + exact/EFin_measurable_fun/measurable_funrM/measurable_fun_indic. + - by move=> r /= z _; exact: nnfun_muleindic_ge0. transitivity (\sum_(k <- fset_set (range f)) \int[m1]_x (k%:E * (fubini_F m2 (EFin \o \1_(f @^-1` [set k])) x))). apply: eq_fbigr => i; rewrite in_fset_set// inE => -[z _ <-{i} _]. rewrite ge0_integralM//; last 3 first. - - apply/EFin_measurable_fun. - by rewrite (_ : \1_ _ = mindic R (measurable_sfunP f (f z)))//. + - exact/EFin_measurable_fun/measurable_fun_indic. - by move=> /= x _; rewrite lee_fin. - by rewrite lee_fin. rewrite indic_fubini_tonelli1// -ge0_integralM//; last by rewrite lee_fin. @@ -4671,15 +4751,14 @@ Lemma sfun_fubini_tonelli2 : \int[m']_z (f z)%:E = \int[m2]_y G y. Proof. under [LHS]eq_integral do rewrite EFinf; rewrite ge0_integral_sum //; last 2 first. - - move=> i; apply/EFin_measurable_fun/measurable_funrM => //. - by rewrite (_ : \1_ _ = mindic R (measurable_sfunP f i)). - - by move=> r /= z _; exact: muleindic_ge0. + - move=> i. + exact/EFin_measurable_fun/measurable_funrM/measurable_fun_indic. + - by move=> r /= z _; exact: nnfun_muleindic_ge0. transitivity (\sum_(k <- fset_set (range f)) \int[m2]_x (k%:E * (fubini_G m1 (EFin \o \1_(f @^-1` [set k])) x))). apply: eq_fbigr => i; rewrite in_fset_set// inE => -[z _ <-{i} _]. rewrite ge0_integralM//; last 3 first. - - apply/EFin_measurable_fun. - by rewrite (_ : \1_ _ = mindic R (measurable_sfunP f (f z))). + - exact/EFin_measurable_fun/measurable_fun_indic. - by move=> /= x _; rewrite lee_fin. - by rewrite lee_fin. rewrite indic_fubini_tonelli2// -ge0_integralM//; last by rewrite lee_fin. @@ -4701,27 +4780,25 @@ Proof. under eq_integral do rewrite EFinf. under [RHS]eq_integral do rewrite EFinf. rewrite ge0_integral_sum //; last 2 first. - - move=> i; apply/EFin_measurable_fun/measurable_funrM => //. - by rewrite (_ : \1_ _ = mindic R (measurable_sfunP f i)). - - by move=> r z _; exact: muleindic_ge0. + - move=> i. + exact/EFin_measurable_fun/measurable_funrM/measurable_fun_indic. + - by move=> r z _; exact: nnfun_muleindic_ge0. transitivity (\sum_(k <- fset_set (range f)) k%:E * \int[m']_z ((EFin \o \1_(f @^-1` [set k])) z)). apply: eq_fbigr => i; rewrite in_fset_set// inE => -[t _ <- _]. rewrite ge0_integralM//; last 3 first. - - apply/EFin_measurable_fun. - by rewrite (_ : \1_ _ = mindic R (measurable_sfunP f (f t))). + - exact/EFin_measurable_fun/measurable_fun_indic. - by move=> /= x _; rewrite lee_fin. - by rewrite lee_fin. rewrite indic_fubini_tonelli1// indic_fubini_tonelli//. by rewrite -indic_fubini_tonelli2. apply/esym; rewrite ge0_integral_sum //; last 2 first. - - move=> i; apply/EFin_measurable_fun/measurable_funrM => //. - by rewrite (_ : \1_ _ = mindic R (measurable_sfunP f i)). - - by move=> r z _; exact: muleindic_ge0. + - move=> i. + exact/EFin_measurable_fun/measurable_funrM/measurable_fun_indic. + - by move=> r z _; exact: nnfun_muleindic_ge0. apply: eq_fbigr => i; rewrite in_fset_set// inE => -[x _ <- _]. rewrite ge0_integralM//; last by rewrite lee_fin. -- apply/EFin_measurable_fun. - by rewrite (_ : \1_ _ = mindic R (measurable_sfunP f (f x))). +- exact/EFin_measurable_fun/measurable_fun_indic. - by move=> /= y _; rewrite lee_fin. Qed. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 3870ffd81..6c5421d8a 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -370,7 +370,8 @@ move=> /(_ _ _ _)/Box[]//=; apply: le_le_trans. rewrite hlength_itv ?lte_fin -?EFinD/= -addrA -opprD. by case: ltP => //; rewrite lee_fin subr_le0. rewrite nneseries_esum//; last by move=> *; rewrite adde_ge0//= ?lee_fin. -rewrite esum_ge//; exists X => //; rewrite fsbig_finite// ?set_fsetK//=. +rewrite esum_ge//; exists [set` X] => //; rewrite fsbig_finite// ?set_fsetK//=. +rewrite fsbig_finite//= set_fsetK//. rewrite lee_sum // => i _; rewrite ?AE// !hlength_itv/= ?lte_fin -?EFinD/=. do !case: ifPn => //= ?; do ?by rewrite ?adde_ge0 ?lee_fin// ?subr_ge0// ?ltW. by rewrite addrAC. @@ -561,8 +562,7 @@ move=> x rx; apply/esym/eqP; rewrite eq_le (itvP (rx 0%N _))// andbT. apply/ler_addgt0Pl => e e_gt0; rewrite -ler_subl_addl ltW//. have := rx `|floor e^-1%R|%N I; rewrite /= in_itv => /andP[/le_lt_trans->]//. rewrite ler_add2l ler_opp2 -lef_pinv ?invrK//; last by rewrite qualifE. -rewrite -addn1 natrD natr_absz ger0_norm ?floor_ge0 ?invr_ge0 1?ltW//. -by rewrite lt_succ_floor. +by rewrite -natr1 natr_absz ger0_norm ?floor_ge0 ?invr_ge0 1?ltW// lt_succ_floor. Qed. Lemma itv_bnd_open_bigcup (R : realType) b (r s : R) : @@ -575,7 +575,7 @@ apply/seteqP; split => [x/=|]; last first. rewrite in_itv/= => /andP[sx xs]; exists `|ceil ((s - x)^-1)|%N => //=. rewrite in_itv/= sx/= ler_subr_addl addrC -ler_subr_addl. rewrite -[in X in _ <= X](invrK (s - x)) ler_pinv. -- rewrite -addn1 natrD natr_absz ger0_norm; last first. +- rewrite -natr1 natr_absz ger0_norm; last first. by rewrite ceil_ge0// invr_ge0 subr_ge0 ltW. by rewrite (@le_trans _ _ (ceil (s - x)^-1)%:~R)// ?ler_addl// ceil_ge. - by rewrite inE unitfE ltr0n andbT pnatr_eq0. @@ -834,6 +834,22 @@ End salgebra_R_ssets. Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1| apply: emeasurable_set1] : core. +Lemma measurable_fun_fine (R : realType) (D : set (\bar R)) : measurable D -> + measurable_fun D fine. +Proof. +move=> mD _ /= B mB; rewrite [X in measurable X](_ : _ `&` _ = if 0%R \in B then + D `&` ((EFin @` B) `|` [set -oo; +oo]%E) else D `&` EFin @` B); last first. + apply/seteqP; split=> [[r [Dr Br]|[Doo B0]|[Doo B0]]|[r| |]]. + - by case: ifPn => _; split => //; left; exists r. + - by rewrite mem_set//; split => //; right; right. + - by rewrite mem_set//; split => //; right; left. + - by case: ifPn => [_ [Dr [[s + [sr]]|[]//]]|_ [Dr [s + [sr]]]]; rewrite sr. + - by case: ifPn => [/[!inE] B0 [Doo [[]//|]] [//|_]|B0 [Doo//] []]. + - by case: ifPn => [/[!inE] B0 [Doo [[]//|]] [//|_]|B0 [Doo//] []]. +case: ifPn => B0; apply/measurableI => //; last exact: measurable_EFin. +by apply: measurableU; [exact: measurable_EFin|exact: measurableU]. +Qed. + Section lebesgue_measure_itv. Variable R : realType. @@ -1470,12 +1486,32 @@ move=> q; case: ifPn => // qfab; apply: is_interval_measurable => //. exact: is_interval_bigcup_ointsub. Qed. -Lemma continuous_measurable_fun (f : R -> R) : continuous f -> - measurable_fun setT f. +Lemma open_measurable_subspace (D : set R) (U : set (subspace D)) : + measurable D -> open U -> measurable (D `&` U). Proof. -move=> /continuousP cf; apply: (measurability (RGenOpens.measurableE R)). -move=> _ [_ [a [b ->] <-]]; rewrite setTI. -by apply: open_measurable; exact/cf/interval_open. +move=> mD /open_subspaceP [V [oV] VD]; rewrite setIC -VD. +by apply: measurableI => //; exact: open_measurable. +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 => //. +by exact/cf/interval_open. +Qed. + +Corollary open_continuous_measurable_fun (D : set R) (f : R -> R) : + open D -> {in D, continuous f} -> measurable_fun D f. +Proof. +move=> oD; rewrite -(continuous_open_subspace f oD). +by apply: subspace_continuous_measurable_fun; exact: open_measurable. +Qed. + +Lemma continuous_measurable_fun (f : R -> R) : + continuous f -> measurable_fun setT f. +Proof. +by move=> cf; apply: open_continuous_measurable_fun => //; exact: openT. Qed. End coutinuous_measurable. @@ -1504,6 +1540,9 @@ Qed. End standard_measurable_fun. +#[global] Hint Extern 0 (measurable_fun _ normr) => + solve [exact: measurable_fun_normr] : core. + Section measurable_fun_realType. Variables (d : measure_display) (T : measurableType d) (R : realType). Implicit Types (D : set T) (f g : T -> R). diff --git a/theories/mathcomp_extra.v b/theories/mathcomp_extra.v index 9a16c6f75..47bf46425 100644 --- a/theories/mathcomp_extra.v +++ b/theories/mathcomp_extra.v @@ -148,6 +148,12 @@ Proof. by move->. Qed. Lemma eqbRL (b1 b2 : bool) : b1 = b2 -> b2 -> b1. Proof. by move->. Qed. +Lemma natr1 (R : ringType) (n : nat) : (n%:R + 1 = n.+1%:R :> R)%R. +Proof. by rewrite GRing.mulrSr. Qed. + +Lemma nat1r (R : ringType) (n : nat) : (1 + n%:R = n.+1%:R :> R)%R. +Proof. by rewrite GRing.mulrS. Qed. + (***************************) (* MathComp 1.15 additions *) (***************************) diff --git a/theories/measure.v b/theories/measure.v index d96c859b9..5b3f2d9dc 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -84,7 +84,8 @@ From HB Require Import structures. (* isMeasure == factory corresponding to the type of measures *) (* Measure == structure corresponding to measures *) (* *) -(* pushforward f m == pushforward/image measure of m by f *) +(* pushforward mf m == pushforward/image measure of m by f, where mf is a *) +(* proof that f is measurable *) (* \d_a == Dirac measure *) (* msum mu n == the measure corresponding to the sum of the measures *) (* mu_0, ..., mu_{n-1} *) @@ -959,7 +960,7 @@ split. Qed. Lemma measurable_funS (E D : set T1) (f : T1 -> T2) : - measurable E -> D `<=` E -> measurable_fun E f -> + measurable E -> D `<=` E -> measurable_fun E f -> measurable_fun D f. Proof. move=> mE DE mf mD; have mC : measurable (E `\` D) by exact: measurableD. @@ -969,6 +970,10 @@ suff -> : D `|` (E `\` D) = E by move=> [[]] //. by rewrite setDUK. Qed. +Lemma measurable_funTS (D : set T1) (f : T1 -> T2) : + measurable_fun setT f -> measurable_fun D f. +Proof. exact: measurable_funS. Qed. + Lemma measurable_fun_ext (D : set T1) (f g : T1 -> T2) : {in D, f =1 g} -> measurable_fun D f -> measurable_fun D g. Proof. @@ -1457,18 +1462,19 @@ Section pushforward_measure. Local Open Scope ereal_scope. Variables (d d' : measure_display). Variables (T1 : measurableType d) (T2 : measurableType d') (f : T1 -> T2). -Hypothesis mf : measurable_fun setT f. Variables (R : realFieldType) (m : {measure set T1 -> \bar R}). -Definition pushforward A := m (f @^-1` A). +Definition pushforward (mf : measurable_fun setT f) A := m (f @^-1` A). + +Hypothesis mf : measurable_fun setT f. -Let pushforward0 : pushforward set0 = 0. +Let pushforward0 : pushforward mf set0 = 0. Proof. by rewrite /pushforward preimage_set0 measure0. Qed. -Let pushforward_ge0 A : 0 <= pushforward A. +Let pushforward_ge0 A : 0 <= pushforward mf A. Proof. by apply: measure_ge0; rewrite -[X in measurable X]setIT; apply: mf. Qed. -Let pushforward_sigma_additive : semi_sigma_additive pushforward. +Let pushforward_sigma_additive : semi_sigma_additive (pushforward mf). Proof. move=> F mF tF mUF; rewrite /pushforward preimage_bigcup. apply: measure_semi_sigma_additive. @@ -1479,7 +1485,7 @@ apply: measure_semi_sigma_additive. Qed. HB.instance Definition _ := isMeasure.Build _ _ _ - pushforward pushforward0 pushforward_ge0 pushforward_sigma_additive. + (pushforward mf) pushforward0 pushforward_ge0 pushforward_sigma_additive. End pushforward_measure. @@ -1532,7 +1538,7 @@ Lemma finite_card_dirac (A : set T) : finite_set A -> \esum_(i in A) \d_ i A = (#|` fset_set A|%:R)%:E :> \bar R. Proof. move=> finA. -rewrite -sum_fset_set// big_seq_cond (eq_bigr (fun=> 1)) -?big_seq_cond. +rewrite esum_fset// fsbig_finite// big_seq_cond (eq_bigr (fun=> 1)) -?big_seq_cond. by rewrite card_fset_sum1// natr_sum -sumEFin. by move=> i; rewrite andbT in_fset_set//= /dirac indicE => ->. Qed. @@ -1542,12 +1548,13 @@ Lemma infinite_card_dirac (A : set T) : infinite_set A -> Proof. move=> infA; apply/eq_pinftyP => r r0. have [B BA Br] := infinite_set_fset `|ceil r| infA. -apply: esum_ge; exists B => //; apply: (@le_trans _ _ `|ceil r|%:R%:E). +apply: esum_ge; exists [set` B] => //; apply: (@le_trans _ _ `|ceil r|%:R%:E). by rewrite lee_fin natr_absz gtr0_norm ?ceil_gt0// ceil_ge. move: Br; rewrite -(@ler_nat R) -lee_fin => /le_trans; apply. -rewrite big_seq (eq_bigr (cst 1))/=; last first. - by move=> i Bi; rewrite /dirac indicE mem_set//; exact: BA. -by rewrite -big_seq card_fset_sum1 sumEFin natr_sum. +rewrite fsbig_finite// big_seq (eq_bigr (cst 1))/=; last first. + move=> i; rewrite in_fset_set// inE/= => Bi; rewrite diracE mem_set//. + exact: BA. +by rewrite -big_seq card_fset_sum1 sumEFin natr_sum// set_fsetK. Qed. End dirac_lemmas. diff --git a/theories/prob_lang.v b/theories/prob_lang.v new file mode 100644 index 000000000..ccae7124b --- /dev/null +++ b/theories/prob_lang.v @@ -0,0 +1,952 @@ +From HB Require Import structures. +From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +From mathcomp Require Import rat. +Require Import mathcomp_extra boolp classical_sets signed functions cardinality. +Require Import reals ereal topology normedtype sequences esum measure. +Require Import lebesgue_measure fsbigop numfun lebesgue_integral exp kernel. + +(******************************************************************************) +(* Semantics of a programming language PPL using s-finite kernels *) +(* *) +(* bernoulli r1 == Bernoulli probability with r1 a proof that *) +(* r : {nonneg R} is smaller than 1 *) +(* *) +(* sample P == sample according to the probability P *) +(* letin l k == execute l, augment the context, and execute k *) +(* ret mf == access the context with f and return the result *) +(* score mf == observe t from d, where f is the density of d and *) +(* t occurs in f *) +(* e.g., score (r e^(-r * t)) = observe t from exp(r) *) +(* pnormalize k P == normalize the kernel k into a probability kernel, *) +(* P is a default probability in case normalization is *) +(* not possible *) +(* ite mf k1 k2 == access the context with the boolean function f and *) +(* behaves as k1 or k2 according to the result *) +(* *) +(* poisson == Poisson distribution function *) +(* exp_density == density function for exponential distribution *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Import Order.TTheory GRing.Theory Num.Def Num.ExtraDef Num.Theory. +Import numFieldTopology.Exports. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. +Local Open Scope ereal_scope. + +(* TODO: PR *) +Lemma onem1' (R : numDomainType) (p : R) : (p + `1- p = 1)%R. +Proof. by rewrite /onem addrCA subrr addr0. Qed. + +Lemma onem_nonneg_proof (R : numDomainType) (p : {nonneg R}) : + (p%:num <= 1 -> 0 <= `1-(p%:num))%R. +Proof. by rewrite /onem/= subr_ge0. Qed. + +Definition onem_nonneg (R : numDomainType) (p : {nonneg R}) + (p1 : (p%:num <= 1)%R) := + NngNum (onem_nonneg_proof p1). + +Lemma expR_ge0 (R : realType) (x : R) : (0 <= expR x)%R. +Proof. by rewrite ltW// expR_gt0. Qed. +(* /TODO: PR *) + +Section bernoulli. +Variables (R : realType) (p : {nonneg R}) (p1 : (p%:num <= 1)%R). +Local Open Scope ring_scope. + +Definition mbernoulli : set _ -> \bar R := + measure_add + [the measure _ _ of mscale p [the measure _ _ of dirac true]] + [the measure _ _ of mscale (onem_nonneg p1) [the measure _ _ of dirac false]]. + +HB.instance Definition _ := Measure.on mbernoulli. + +Local Close Scope ring_scope. + +Let mbernoulli_setT : mbernoulli [set: _] = 1. +Proof. +rewrite /mbernoulli/= /measure_add/= /msum 2!big_ord_recr/= big_ord0 add0e/=. +by rewrite /mscale/= !diracT !mule1 -EFinD onem1'. +Qed. + +HB.instance Definition _ := + @isProbability.Build _ _ R mbernoulli mbernoulli_setT. + +Definition bernoulli := [the probability _ _ of mbernoulli]. + +End bernoulli. + +Section mscore. +Variables (d : _) (T : measurableType d). +Variables (R : realType) (f : T -> R). + +Definition mscore t : {measure set _ -> \bar R} := + let p := NngNum (normr_ge0 (f t)) in + [the measure _ _ of mscale p [the measure _ _ of dirac tt]]. + +Lemma mscoreE t U : mscore t U = if U == set0 then 0 else `| (f t)%:E |. +Proof. +rewrite /mscore/= /mscale/=; have [->|->] := set_unit U. + by rewrite eqxx dirac0 mule0. +by rewrite diracT mule1 (negbTE (setT0 _)). +Qed. + +Lemma measurable_fun_mscore U : measurable_fun setT f -> + measurable_fun setT (mscore ^~ U). +Proof. +move=> mr; under eq_fun do rewrite mscoreE/=. +have [U0|U0] := eqVneq U set0; first exact: measurable_fun_cst. +by apply: measurable_fun_comp => //; exact: measurable_fun_comp. +Qed. + +End mscore. + +(* decomposition of score into finite kernels *) +Module SCORE. +Section score. +Variables (R : realType) (d : _) (T : measurableType d). +Variables (r : T -> R). + +Definition k (mr : measurable_fun setT r) (i : nat) : T -> set unit -> \bar R := + fun t U => + if i%:R%:E <= mscore r t U < i.+1%:R%:E then + mscore r t U + else + 0. + +Hypothesis mr : measurable_fun setT r. + +Lemma k0 i t : k mr i t (set0 : set unit) = 0 :> \bar R. +Proof. by rewrite /k measure0; case: ifP. Qed. + +Lemma k_ge0 i t B : 0 <= k mr i t B. +Proof. by rewrite /k; case: ifP. Qed. + +Lemma k_sigma_additive i t : semi_sigma_additive (k mr i t). +Proof. +move=> /= F mF tF mUF; rewrite /k /=. +have [F0|] := eqVneq (\bigcup_n F n) set0. + rewrite F0 measure0 (_ : (fun _ => _) = cst 0). + by case: ifPn => _; exact: cvg_cst. + apply/funext => k; rewrite big1// => n _. + by move: F0 => /bigcup0P -> //; rewrite measure0; case: ifPn. +move=> UF0; move: (UF0). +move=> /eqP/bigcup0P/existsNP[m /not_implyP[_ /eqP Fm0]]. +rewrite [in X in _ --> X]mscoreE (negbTE UF0). +rewrite -(cvg_shiftn m.+1)/=. +case: ifPn => ir. + rewrite (_ : (fun _ => _) = cst `|(r t)%:E|); first exact: cvg_cst. + apply/funext => n. + rewrite big_mkord (bigD1 (widen_ord (leq_addl n _) (Ordinal (ltnSn m))))//=. + rewrite [in X in X + _]mscoreE (negbTE Fm0) ir big1 ?adde0// => /= j jk. + rewrite mscoreE; have /eqP -> : F j == set0. + have [/eqP//|Fjtt] := set_unit (F j). + move/trivIsetP : tF => /(_ j m Logic.I Logic.I jk). + by rewrite Fjtt setTI => /eqP; rewrite (negbTE Fm0). + by rewrite eqxx; case: ifP. +rewrite (_ : (fun _ => _) = cst 0); first exact: cvg_cst. +apply/funext => n. +rewrite big_mkord (bigD1 (widen_ord (leq_addl n _) (Ordinal (ltnSn m))))//=. +rewrite [in X in if X then _ else _]mscoreE (negbTE Fm0) (negbTE ir) add0e. +rewrite big1//= => j jm. +rewrite mscoreE; have /eqP -> : F j == set0. + have [/eqP//|Fjtt] := set_unit (F j). + move/trivIsetP : tF => /(_ j m Logic.I Logic.I jm). + by rewrite Fjtt setTI => /eqP; rewrite (negbTE Fm0). +by rewrite eqxx; case: ifP. +Qed. + +HB.instance Definition _ i t := isMeasure.Build _ _ _ + (k mr i t) (k0 i t) (k_ge0 i t) (@k_sigma_additive i t). + +Lemma measurable_fun_k i U : measurable U -> measurable_fun setT (k mr i ^~ U). +Proof. +move=> /= mU; rewrite /k /=. +rewrite (_ : (fun x : T => _) = + (fun x => if i%:R%:E <= x < i.+1%:R%:E then x else 0) \o (mscore r ^~ U)) //. +apply: measurable_fun_comp => /=; last exact/measurable_fun_mscore. +pose A : _ -> \bar R := + fun x => x * (\1_(`[i%:R%:E, i.+1%:R%:E [%classic : set (\bar R)) x)%:E. +rewrite (_ : (fun x => _) = A); last first. + apply/funext => x; rewrite /A; case: ifPn => ix. + by rewrite indicE/= mem_set ?mule1. + by rewrite indicE/= memNset ?mule0// /= in_itv/=; exact/negP. +rewrite {}/A. +apply emeasurable_funM => /=; first exact: measurable_fun_id. +apply/EFin_measurable_fun. +have mi : measurable (`[i%:R%:E, i.+1%:R%:E[%classic : set (\bar R)). + exact: emeasurable_itv. +by rewrite (_ : \1__ = mindic R mi). +Qed. + +Definition mk i t := [the measure _ _ of k mr i t]. + +HB.instance Definition _ i := + isKernel.Build _ _ _ _ R (mk i) (measurable_fun_k i). + +Lemma mk_uub (i : nat) : measure_fam_uub (mk i). +Proof. +exists i.+1%:R => /= t; rewrite /k mscoreE setT_unit. +by case: ifPn => //; case: ifPn => // _ /andP[]. +Qed. + +HB.instance Definition _ i := + @Kernel_isFinite.Build _ _ _ _ R (mk i) (mk_uub i). + +End score. +End SCORE. + +Section kscore. +Variables (R : realType) (d : _) (T : measurableType d) (r : T -> R). + +Definition kscore (mr : measurable_fun setT r) + : T -> {measure set _ -> \bar R} := + fun t => [the measure _ _ of mscore r t]. + +Variable (mr : measurable_fun setT r). + +Let measurable_fun_kscore U : measurable U -> + measurable_fun setT (kscore mr ^~ U). +Proof. by move=> /= _; exact: measurable_fun_mscore. Qed. + +HB.instance Definition _ := isKernel.Build _ _ T _ R + (kscore mr) measurable_fun_kscore. + +Import SCORE. + +Let sfinite_kscore : exists k : (R.-fker T ~> _)^nat, + forall x U, measurable U -> + kscore mr x U = [the measure _ _ of mseries (k ^~ x) 0] U. +Proof. +rewrite /=. +exists (fun i => [the R.-fker _ ~> _ of mk mr i]) => /= t U mU. +rewrite /mseries /kscore/= mscoreE; case: ifPn => [/eqP U0|U0]. + by apply/esym/nneseries0 => i _; rewrite U0 measure0. +rewrite /mk /= /k /= mscoreE (negbTE U0). +apply/esym/cvg_lim => //. +rewrite -(cvg_shiftn `|floor (fine `|(r t)%:E|)|%N.+1)/=. +rewrite (_ : (fun _ => _) = cst `|(r t)%:E|); first exact: cvg_cst. +apply/funext => n. +pose floor_r := widen_ord (leq_addl n `|floor `|r t| |.+1) + (Ordinal (ltnSn `|floor `|r t| |)). +rewrite big_mkord (bigD1 floor_r)//= ifT; last first. + rewrite lee_fin lte_fin; apply/andP; split. + by rewrite natr_absz (@ger0_norm _ (floor `|r t|)) ?floor_ge0 ?floor_le. + rewrite -addn1 natrD natr_absz. + by rewrite (@ger0_norm _ (floor `|r t|)) ?floor_ge0 ?lt_succ_floor. +rewrite big1 ?adde0//= => j jk. +rewrite ifF// lte_fin lee_fin. +move: jk; rewrite neq_ltn/= => /orP[|] jr. +- suff : (j.+1%:R <= `|r t|)%R by rewrite leNgt => /negbTE ->; rewrite andbF. + rewrite (_ : j.+1%:R = j.+1%:~R)// floor_ge_int. + move: jr; rewrite -lez_nat => /le_trans; apply. + by rewrite -[leRHS](@ger0_norm _ (floor `|r t|)) ?floor_ge0. +- suff : (`|r t| < j%:R)%R by rewrite ltNge => /negbTE ->. + move: jr; rewrite -ltz_nat -(@ltr_int R) (@gez0_abs (floor `|r t|)) ?floor_ge0//. + by rewrite ltr_int -floor_lt_int. +Qed. + +HB.instance Definition _ := + @Kernel_isSFinite.Build _ _ _ _ _ (kscore mr) sfinite_kscore. + +End kscore. + +(* decomposition of ite into s-finite kernels *) +Module ITE. +Section kiteT. +Variables (d d' : _) (X : measurableType d) (Y : measurableType d'). +Variables (R : realType) (k : R.-ker X ~> Y). + +Definition kiteT : X * bool -> {measure set Y -> \bar R} := + fun xb => if xb.2 then k xb.1 else [the measure _ _ of mzero]. + +Let measurable_fun_kiteT U : measurable U -> measurable_fun setT (kiteT ^~ U). +Proof. +move=> /= mcU; rewrite /kiteT. +rewrite (_ : (fun _ => _) = (fun x => if x.2 then k x.1 U + else [the {measure set Y -> \bar R} of mzero] U)); last first. + by apply/funext => -[t b]/=; case: ifPn. +apply: (@measurable_fun_if_pair _ _ _ _ (k ^~ U) (fun=> mzero U)). + exact/measurable_kernel. +exact: measurable_fun_cst. +Qed. + +#[export] +HB.instance Definition _ := isKernel.Build _ _ _ _ R kiteT measurable_fun_kiteT. +End kiteT. + +Section sfkiteT. +Variables (d d' : _) (X : measurableType d) (Y : measurableType d'). +Variables (R : realType) (k : R.-sfker X ~> Y). + +Let sfinite_kiteT : exists2 k_ : (R.-ker _ ~> _)^nat, + forall n, measure_fam_uub (k_ n) & + forall x U, measurable U -> + kiteT k x U = [the measure _ _ of mseries (k_ ^~ x) 0] U. +Proof. +have [k_ hk /=] := sfinite k. +exists (fun n => [the _.-ker _ ~> _ of kiteT (k_ n)]) => /=. + move=> n; have /measure_fam_uubP[r k_r] := measure_uub (k_ n). + by exists r%:num => /= -[x []]; rewrite /kiteT//= /mzero//. +move=> [x b] U mU; rewrite /kiteT; case: ifPn => hb. + by rewrite hk. +by rewrite /mseries nneseries0. +Qed. + +(*Let sfinite_kiteT : exists k_ : (R.-fker _ ~> _)^nat, + forall x U, measurable U -> + kiteT k x U = [the measure _ _ of mseries (k_ ^~ x) 0] U. +Proof. +have [k_ hk /=] := sfinite k. +exists (fun n => [the _.-fker _ ~> _ of kiteT (k_ n)]) => b U mU. +rewrite /kiteT; case: ifPn => hb. + rewrite /mseries hk//= /mseries. + apply: eq_nneseries => n _. + by rewrite /kiteT hb. +rewrite /= /mseries nneseries0// => n _. +by rewrite /kiteT (negbTE hb). +Qed.*) + +(* NB: we could also want to use Kernel_isSFinite *) +#[export] +HB.instance Definition _ t := @Kernel_isSFinite_subdef.Build _ _ _ _ _ + (kiteT k) sfinite_kiteT. +End sfkiteT. + +Section fkiteT. +Variables (d d' : _) (X : measurableType d) (Y : measurableType d'). +Variables (R : realType) (k : R.-fker X ~> Y). + +Let kiteT_uub : measure_fam_uub (kiteT k). +Proof. +have /measure_fam_uubP[M hM] := measure_uub k. +exists M%:num => /= -[]; rewrite /kiteT => t [|]/=; first exact: hM. +by rewrite /= /mzero. +Qed. + +#[export] +HB.instance Definition _ t := Kernel_isFinite.Build _ _ _ _ R (kiteT k) kiteT_uub. +End fkiteT. + +Section kiteF. +Variables (d d' : _) (X : measurableType d) (Y : measurableType d'). +Variables (R : realType) (k : R.-ker X ~> Y). + +Definition kiteF : X * bool -> {measure set Y -> \bar R} := + fun xb => if ~~ xb.2 then k xb.1 else [the measure _ _ of mzero]. + +Let measurable_fun_kiteF U : measurable U -> measurable_fun setT (kiteF ^~ U). +Proof. +move=> /= mcU; rewrite /kiteF. +rewrite (_ : (fun x => _) = (fun x => if x.2 then [the measure _ _ of mzero] U else k x.1 U)); last first. + apply/funext => -[t b]/=. + by rewrite if_neg//; case: ifPn. +apply: (@measurable_fun_if_pair _ _ _ _ (fun=> mzero U) (k ^~ U)). + exact: measurable_fun_cst. +exact/measurable_kernel. +Qed. + +#[export] +HB.instance Definition _ := isKernel.Build _ _ _ _ R kiteF measurable_fun_kiteF. + +End kiteF. + +Section sfkiteF. +Variables (d d' : _) (X : measurableType d) (Y : measurableType d'). +Variables (R : realType) (k : R.-sfker X ~> Y). + +Let sfinite_kiteF : exists2 k_ : (R.-ker _ ~> _)^nat, + forall n, measure_fam_uub (k_ n) & + forall x U, measurable U -> + kiteF k x U = [the measure _ _ of mseries (k_ ^~ x) 0] U. +Proof. +have [k_ hk /=] := sfinite k. +exists (fun n => [the _.-ker _ ~> _ of kiteF (k_ n)]) => /=. + move=> n; have /measure_fam_uubP[r k_r] := measure_uub (k_ n). + by exists r%:num => /= -[x []]; rewrite /kiteF//= /mzero//. +move=> [x b] U mU; rewrite /kiteF; case: ifPn => hb. + by rewrite hk. +by rewrite /mseries nneseries0. +Qed. + +(*Let sfinite_kiteF : exists k_ : (R.-fker _ ~> _)^nat, + forall x U, measurable U -> + kiteF k x U = [the measure _ _ of mseries (k_ ^~ x) 0] U. +Proof. +have [k_ hk] := sfinite k. +exists (fun n => [the finite_kernel _ _ _ of kiteF (k_ n)]) => b U mU. +rewrite /= /kiteF /=; case: ifPn => hb. + by rewrite /mseries hk//= /mseries/=. +by rewrite /= /mseries nneseries0. +Qed. +*) + +#[export] +HB.instance Definition _ := @Kernel_isSFinite_subdef.Build _ _ _ _ _ + (kiteF k) sfinite_kiteF. + +End sfkiteF. + +Section fkiteF. +Variables (d d' : _) (X : measurableType d) (Y : measurableType d'). +Variables (R : realType) (k : R.-fker X ~> Y). + +Let kiteF_uub : measure_fam_uub (kiteF k). +Proof. +have /measure_fam_uubP[M hM] := measure_uub k. +exists M%:num => /= -[]; rewrite /kiteF/= => t. +by case => //=; rewrite /mzero. +Qed. + +#[export] +HB.instance Definition _ := Kernel_isFinite.Build _ _ _ _ R (kiteF k) kiteF_uub. + +End fkiteF. + +(*Module Exports. +HB.reexport. +End Exports.*) +End ITE. +(*Export ITE.Exports.*) + +Section ite. +Variables (d d' : _) (T : measurableType d) (T' : measurableType d'). +Variables (R : realType) (f : T -> bool) (u1 u2 : R.-sfker T ~> T'). + +Definition mite (mf : measurable_fun setT f) : T -> set T' -> \bar R := + fun t => if f t then u1 t else u2 t. + +Variables mf : measurable_fun setT f. + +Let mite0 t : mite mf t set0 = 0. +Proof. by rewrite /mite; case: ifPn => //. Qed. + +Let mite_ge0 t (U : set _) : 0 <= mite mf t U. +Proof. by rewrite /mite; case: ifPn => //. Qed. + +Let mite_sigma_additive t : semi_sigma_additive (mite mf t). +Proof. +by rewrite /mite; case: ifPn => ft; exact: measure_semi_sigma_additive. +Qed. + +HB.instance Definition _ t := isMeasure.Build _ _ _ (mite mf t) + (mite0 t) (mite_ge0 t) (@mite_sigma_additive t). + +Import ITE. + +Definition kite := + [the R.-sfker _ ~> _ of kdirac mf] \; + [the R.-sfker _ ~> _ of kadd + [the R.-sfker _ ~> T' of kiteT u1] + [the R.-sfker _ ~> T' of kiteF u2] ]. + +End ite. + +(* wip *) +Section dist_salgebra_instance. +Variables (d : measure_display) (T : measurableType d) (R : realType). +Variables p0 : probability T R. + +Definition prob_pointed := Pointed.Class + (Choice.Class gen_eqMixin (Choice.Class gen_eqMixin gen_choiceMixin)) p0. + +Canonical probability_eqType := EqType (probability T R) prob_pointed. +Canonical probability_choiceType := ChoiceType (probability T R) prob_pointed. +Canonical probability_ptType := PointedType (probability T R) prob_pointed. + +Definition mset (U : set T) (r : R) := [set mu : probability T R | mu U < r%:E]. + +Definition pset : set (set (probability T R)) := + [set mset U r | r in `[0%R,1%R]%classic & U in @measurable d T]. + +Definition sset := [the measurableType pset.-sigma of salgebraType pset]. + +End dist_salgebra_instance. + +Section insn2. +Variables (d d' : _) (X : measurableType d) (Y : measurableType d'). +Variable R : realType. + +Definition ret (f : X -> Y) (mf : measurable_fun setT f) := + locked [the R.-sfker X ~> Y of kdirac mf]. + +Definition sample (P : probability Y R) := + locked [the R.-pker X ~> Y of kprobability P] . + +Definition normalize (k : R.-sfker X ~> Y) P x := + locked [the probability _ _ of mnormalize k P x]. + +Definition ite (f : X -> bool) (mf : measurable_fun setT f) + (k1 k2 : R.-sfker X ~> Y):= + locked [the R.-sfker X ~> Y of kite k1 k2 mf]. + +End insn2. +Arguments ret {d d' X Y R f} mf. +Arguments sample {d d' X Y R}. + +Section insn2_lemmas. +Variables (d d' : _) (X : measurableType d) (Y : measurableType d'). +Variable R : realType. + +Lemma retE (f : X -> Y) (mf : measurable_fun setT f) x : + ret mf x = \d_(f x) :> (_ -> \bar R). +Proof. by rewrite [in LHS]/ret; unlock. Qed. + +Lemma sampleE (P : probability Y R) (x : X) : sample P x = P. +Proof. by rewrite [in LHS]/sample; unlock. Qed. + +Lemma normalizeE (f : R.-sfker X ~> Y) P x U : + normalize f P x U = + if (f x [set: Y] == 0) || (f x [set: Y] == +oo) then P U + else f x U * ((fine (f x [set: Y]))^-1)%:E. +Proof. +by rewrite /normalize; unlock => /=; rewrite /mnormalize; case: ifPn. +Qed. + +Lemma iteE (f : X -> bool) (mf : measurable_fun setT f) + (k1 k2 : R.-sfker X ~> Y) x : + ite mf k1 k2 x = if f x then k1 x else k2 x. +Proof. +apply/eq_measure/funext => U. +rewrite /ite; unlock => /=. +rewrite /kcomp/= integral_dirac//=. +rewrite indicT mul1e. +rewrite -/(measure_add (ITE.kiteT k1 (x, f x)) (ITE.kiteF k2 (x, f x))). +rewrite measure_addE. +rewrite /ITE.kiteT /ITE.kiteF/=. +by case: ifPn => fx /=; rewrite /mzero ?(adde0,add0e). +Qed. + +End insn2_lemmas. + +Section insn3. +Variables (R : realType). +Variables (d d' d3 : _) (X : measurableType d) (Y : measurableType d') + (Z : measurableType d3). + +Definition letin (l : R.-sfker X ~> Y) + (k : R.-sfker [the measurableType (d, d').-prod of (X * Y)%type] ~> Z) := + locked [the R.-sfker X ~> Z of l \; k]. + +End insn3. + +Section insn3_lemmas. +Variables (R : realType). +Variables (d d' d3 : _) (X : measurableType d) (Y : measurableType d') + (Z : measurableType d3). + +Lemma letinE (l : R.-sfker X ~> Y) + (k : R.-sfker [the measurableType (d, d').-prod of (X * Y)%type] ~> Z) x U : + letin l k x U = \int[l x]_y k (x, y) U. +Proof. by rewrite /letin; unlock. Qed. + +End insn3_lemmas. + +(* rewriting laws *) +Section letin_return. +Variables (d d' d3 : _) (R : realType) (X : measurableType d) + (Y : measurableType d') (Z : measurableType d3). + +Lemma letin_kret (k : R.-sfker X ~> Y) + (f : X * Y -> Z) (mf : measurable_fun setT f) x U : + measurable U -> + letin k (ret mf) x U = k x (curry f x @^-1` U). +Proof. +move=> mU; rewrite letinE. +under eq_integral do rewrite retE. +rewrite integral_indic ?setIT//. +move/measurable_fun_prod1 : mf => /(_ x measurableT U mU). +by rewrite setTI. +Qed. + +Lemma letin_retk + (f : X -> Y) (mf : measurable_fun setT f) + (k : R.-sfker [the measurableType _ of (X * Y)%type] ~> Z) + x U : measurable U -> + letin (ret mf) k x U = k (x, f x) U. +Proof. +move=> mU; rewrite letinE retE integral_dirac ?indicT ?mul1e//. +have /measurable_fun_prod1 := measurable_kernel k _ mU. +exact. +Qed. + +End letin_return. + +Section insn1. +Variables (R : realType) (d : _) (X : measurableType d). + +Definition score (f : X -> R) (mf : measurable_fun setT f) := + [the R.-sfker X ~> _ of kscore mf]. + +End insn1. + +Module Notations. + +Notation var1of2 := (@measurable_fun_fst _ _ _ _). +Notation var2of2 := (@measurable_fun_snd _ _ _ _). +Notation var1of3 := (measurable_fun_comp (@measurable_fun_fst _ _ _ _) + (@measurable_fun_fst _ _ _ _)). +Notation var2of3 := (measurable_fun_comp (@measurable_fun_snd _ _ _ _) + (@measurable_fun_fst _ _ _ _)). +Notation var3of3 := (@measurable_fun_snd _ _ _ _). + +Notation mR := Real_sort__canonical__measure_Measurable. +Notation munit := Datatypes_unit__canonical__measure_Measurable. +Notation mbool := Datatypes_bool__canonical__measure_Measurable. + +End Notations. + +Section insn1_lemmas. +Import Notations. +Variables (R : realType) (d : _) (T : measurableType d). + +Let kcomp_scoreE d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) + (g : R.-sfker [the measurableType _ of (T1 * unit)%type] ~> T2) + f (mf : measurable_fun setT f) r U : + (score mf \; g) r U = `|f r|%:E * g (r, tt) U. +Proof. +rewrite /= /kcomp /kscore /= ge0_integral_mscale//=. +by rewrite integral_dirac// indicT mul1e. +Qed. + +Lemma scoreE d' (T' : measurableType d') (x : T * T') (U : set T') (f : R -> R) + (r : R) (r0 : (0 <= r)%R) + (f0 : (forall r, 0 <= r -> 0 <= f r)%R) (mf : measurable_fun setT f) : + score (measurable_fun_comp mf var2of2) + (x, r) (curry (snd \o fst) x @^-1` U) = + (f r)%:E * \d_x.2 U. +Proof. by rewrite /score/= /mscale/= ger0_norm// f0. Qed. + +Lemma score_score (f : R -> R) (g : R * unit -> R) + (mf : measurable_fun setT f) + (mg : measurable_fun setT g) x U : + letin (score mf) (score mg) x U = + score (measurable_funM mf (measurable_fun_prod2 tt mg)) x U. +Proof. +rewrite {1}/letin; unlock. +by rewrite kcomp_scoreE/= /mscale/= diracE normrM muleA EFinM. +Qed. + +End insn1_lemmas. + +Section letin_ite. +Variables (R : realType) (d d2 d3 : _) (T : measurableType d) + (T2 : measurableType d2) (Z : measurableType d3) + (k1 k2 : R.-sfker T ~> Z) (u : R.-sfker [the measurableType _ of (T * Z)%type] ~> T2) + (f : T -> bool) (mf : measurable_fun setT f) + (t : T) (U : set T2). + +Lemma letin_iteT : f t -> letin (ite mf k1 k2) u t U = letin k1 u t U. +Proof. +move=> ftT. +rewrite !letinE/=. +apply eq_measure_integral => V mV _. +by rewrite iteE ftT. +Qed. + +Lemma letin_iteF : ~~ f t -> letin (ite mf k1 k2) u t U = letin k2 u t U. +Proof. +move=> ftF. +rewrite !letinE/=. +apply eq_measure_integral => V mV _. +by rewrite iteE (negbTE ftF). +Qed. + +End letin_ite. + +Section letinC. +Variables (d d1 : _) (X : measurableType d) (Y : measurableType d1). +Variables (R : realType) (d' : _) (Z : measurableType d'). + +Import Notations. + +Variables (t : R.-sfker Z ~> X) + (t' : R.-sfker [the measurableType _ of (Z * Y)%type] ~> X) + (tt' : forall y, t =1 fun z => t' (z, y)) + (u : R.-sfker Z ~> Y) + (u' : R.-sfker [the measurableType _ of (Z * X)%type] ~> Y) + (uu' : forall x, u =1 fun z => u' (z, x)). + +Lemma letinC z A : measurable A -> + letin t + (letin u' + (ret (measurable_fun_pair var2of3 var3of3))) z A = + letin u + (letin t' + (ret (measurable_fun_pair var3of3 var2of3))) z A. +Proof. +move=> mA. +rewrite !letinE. +under eq_integral. + move=> x _. + rewrite letinE/= -uu'. + under eq_integral do rewrite retE /=. + over. +rewrite (sfinite_fubini _ _ (fun x => \d_(x.1, x.2) A ))//; last 3 first. + exact: sfinite_kernel_measure. + exact: sfinite_kernel_measure. + apply/EFin_measurable_fun => /=; rewrite (_ : (fun x => _) = mindic R mA)//. + by apply/funext => -[]. +apply eq_integral => y _. +by rewrite letinE/= -tt'; apply eq_integral => // x _; rewrite retE. +Qed. + +End letinC. + +(* sample programs *) + +Section constants. +Variable R : realType. +Local Open Scope ring_scope. + +Lemma onem27 : `1- (2 / 7%:R) = (5%:R / 7%:R)%:nng%:num :> R. +Proof. by apply/eqP; rewrite subr_eq/= -mulrDl -natrD divrr// unitfE. Qed. + +Lemma p27 : (2 / 7%:R)%:nng%:num <= 1 :> R. +Proof. by rewrite /= lter_pdivr_mulr// mul1r ler_nat. Qed. + +End constants. +Arguments p27 {R}. + +Section poisson. +Variable R : realType. +Local Open Scope ring_scope. + +(* density function for Poisson *) +Definition poisson k r : R := r ^+ k / k`!%:R^-1 * expR (- r). + +Lemma poisson_ge0 k r : 0 <= r -> 0 <= poisson k r. +Proof. +move=> r0; rewrite /poisson mulr_ge0 ?expR_ge0//. +by rewrite mulr_ge0// exprn_ge0. +Qed. + +Lemma poisson_gt0 k r : 0 < r -> 0 < poisson k.+1 r. +Proof. +move=> r0; rewrite /poisson mulr_gt0 ?expR_gt0//. +by rewrite divr_gt0// ?exprn_gt0// invr_gt0 ltr0n fact_gt0. +Qed. + +Lemma mpoisson k : measurable_fun setT (poisson k). +Proof. +apply: measurable_funM => /=. + apply: measurable_funM => //=; last exact: measurable_fun_cst. + exact/measurable_fun_exprn/measurable_fun_id. +apply: measurable_fun_comp; last exact: measurable_fun_opp. +by apply: continuous_measurable_fun; exact: continuous_expR. +Qed. + +Definition poisson3 := poisson 4 3. (* 0.168 *) +Definition poisson10 := poisson 4 10. (* 0.019 *) + +End poisson. + +Section exponential. +Variable R : realType. +Local Open Scope ring_scope. + +(* density function for exponential *) +Definition exp_density x r : R := r * expR (- r * x). + +Lemma exp_density_gt0 x r : 0 < r -> 0 < exp_density x r. +Proof. by move=> r0; rewrite /exp_density mulr_gt0// expR_gt0. Qed. + +Lemma exp_density_ge0 x r : 0 <= r -> 0 <= exp_density x r. +Proof. by move=> r0; rewrite /exp_density mulr_ge0// expR_ge0. Qed. + +Lemma mexp_density x : measurable_fun setT (exp_density x). +Proof. +apply: measurable_funM => /=; first exact: measurable_fun_id. +apply: measurable_fun_comp. + by apply: continuous_measurable_fun; exact: continuous_expR. +apply: measurable_funM => /=; first exact: measurable_fun_opp. +exact: measurable_fun_cst. +Qed. + +End exponential. + +Section cst_fun. +Variables (R : realType) (d : _) (T : measurableType d). + +Definition kn (n : nat) := @measurable_fun_cst _ _ T _ setT (n%:R : R). +Definition k3 : measurable_fun _ _ := kn 3. +Definition k10 : measurable_fun _ _ := kn 10. + +End cst_fun. +Arguments k3 {R d T}. +Arguments k10 {R d T}. + +Lemma letin_sample_bernoulli (R : realType) (d d' : _) (T : measurableType d) + (T' : measurableType d') (r : {nonneg R}) (r1 : (r%:num <= 1)%R) + (u : R.-sfker [the measurableType _ of (T * bool)%type] ~> T') x y : + letin (sample (bernoulli r1)) u x y = + r%:num%:E * u (x, true) y + (`1- (r%:num : R))%:E * u (x, false) y. +Proof. +rewrite letinE/= sampleE. +rewrite ge0_integral_measure_sum// 2!big_ord_recl/= big_ord0 adde0/=. +by rewrite !ge0_integral_mscale//= !integral_dirac//= indicT 2!mul1e. +Qed. + +Section sample_and_return. +Import Notations. +Variables (R : realType) (d : _) (T : measurableType d). + +Definition sample_and_return : R.-sfker T ~> _ := + letin + (sample (bernoulli p27)) (* T -> B *) + (ret var2of2) (* T * B -> B *). + +Lemma sample_and_returnE t U : sample_and_return t U = + (2 / 7)%:E * \d_true U + (5 / 7)%:E * \d_false U. +Proof. +rewrite /sample_and_return. +rewrite letin_sample_bernoulli/=. +rewrite !retE. +by rewrite onem27. +Qed. + +End sample_and_return. + +(* trivial example *) +Section sample_and_branch. +Import Notations. +Variables (R : realType) (d : _) (T : measurableType d). + +(* let x = sample (bernoulli (2/7)) in + let r = case x of {(1, _) => return (k3()), (2, _) => return (k10())} in + return r *) + +Definition sample_and_branch : + R.-sfker T ~> mR R := + letin + (sample (bernoulli p27)) (* T -> B *) + (ite var2of2 (ret k3) (ret k10)). + +Lemma sample_and_branchE t U : sample_and_branch t U = + (2 / 7)%:E * \d_(3 : R) U + + (5 / 7)%:E * \d_(10 : R) U. +Proof. +rewrite /sample_and_branch letin_sample_bernoulli/=. +rewrite !iteE/= !retE. +by rewrite onem27. +Qed. + +End sample_and_branch. + +Section staton_bus. +Import Notations. +Variables (R : realType) (d : _) (T : measurableType d) (h : R -> R). +Hypothesis mh : measurable_fun setT h. +Definition kstaton_bus : R.-sfker T ~> mbool := + letin (sample (bernoulli p27)) + (letin + (letin (ite var2of2 (ret k3) (ret k10)) + (score (measurable_fun_comp mh var3of3))) + (ret var2of3)). + +Definition staton_bus := normalize kstaton_bus. + +End staton_bus. + +(* let x = sample (bernoulli (2/7)) in + let r = case x of {(1, _) => return (k3()), (2, _) => return (k10())} in + let _ = score (1/4! r^4 e^-r) in + return x *) +Section staton_bus_poisson. +Import Notations. +Variables (R : realType) (d : _) (T : measurableType d). +Let poisson4 := @poisson R 4%N. +Let mpoisson4 := @mpoisson R 4%N. + +Definition kstaton_bus_poisson : R.-sfker (mR R) ~> mbool := + kstaton_bus _ mpoisson4. + +Let kstaton_bus_poissonE t U : kstaton_bus_poisson t U = + (2 / 7)%:E * (poisson4 3)%:E * \d_true U + + (5 / 7)%:E * (poisson4 10)%:E * \d_false U. +Proof. +rewrite /kstaton_bus. +rewrite letin_sample_bernoulli. +rewrite -!muleA; congr (_ * _ + _ * _). +- rewrite letin_kret//. + rewrite letin_iteT//. + rewrite letin_retk//. + by rewrite scoreE//= => r r0; exact: poisson_ge0. +- by rewrite onem27. + rewrite letin_kret//. + rewrite letin_iteF//. + rewrite letin_retk//. + by rewrite scoreE//= => r r0; exact: poisson_ge0. +Qed. + +(* true -> 2/7 * 0.168 = 2/7 * 3^4 e^-3 / 4! *) +(* false -> 5/7 * 0.019 = 5/7 * 10^4 e^-10 / 4! *) + +Lemma staton_busE P (t : R) U : + let N := ((2 / 7) * poisson4 3 + + (5 / 7) * poisson4 10)%R in + staton_bus mpoisson4 P t U = + ((2 / 7)%:E * (poisson4 3)%:E * \d_true U + + (5 / 7)%:E * (poisson4 10)%:E * \d_false U) * N^-1%:E. +Proof. +rewrite /staton_bus normalizeE /= !kstaton_bus_poissonE !diracT !mule1 ifF //. +apply/negbTE; rewrite gt_eqF// lte_fin. +by rewrite addr_gt0// mulr_gt0//= ?divr_gt0// ?ltr0n// poisson_gt0// ltr0n. +Qed. + +End staton_bus_poisson. + +(* let x = sample (bernoulli (2/7)) in + let r = case x of {(1, _) => return (k3()), (2, _) => return (k10())} in + let _ = score (r e^-(15/60 r)) in + return x *) +Section staton_bus_exponential. +Import Notations. +Variables (R : realType) (d : _) (T : measurableType d). +Let exp1560 := @exp_density R (ratr (15%:Q / 60%:Q)). +Let mexp1560 := @mexp_density R (ratr (15%:Q / 60%:Q)). + +(* 15/60 = 0.25 *) + +Definition kstaton_bus_exponential : R.-sfker (mR R) ~> mbool := + kstaton_bus _ mexp1560. + +Let kstaton_bus_exponentialE t U : kstaton_bus_exponential t U = + (2 / 7)%:E * (exp1560 3)%:E * \d_true U + + (5 / 7)%:E * (exp1560 10)%:E * \d_false U. +Proof. +rewrite /kstaton_bus. +rewrite letin_sample_bernoulli. +rewrite -!muleA; congr (_ * _ + _ * _). +- rewrite letin_kret//. + rewrite letin_iteT//. + rewrite letin_retk//. + rewrite scoreE//= => r r0; exact: exp_density_ge0. +- by rewrite onem27. + rewrite letin_kret//. + rewrite letin_iteF//. + rewrite letin_retk//. + by rewrite scoreE//= => r r0; exact: exp_density_ge0. +Qed. + +(* true -> 5/7 * 0.019 = 5/7 * 10^4 e^-10 / 4! *) +(* false -> 2/7 * 0.168 = 2/7 * 3^4 e^-3 / 4! *) + +Lemma staton_bus_exponentialE P (t : R) U : + let N := ((2 / 7) * exp1560 3 + + (5 / 7) * exp1560 10)%R in + staton_bus mexp1560 P t U = + ((2 / 7)%:E * (exp1560 3)%:E * \d_true U + + (5 / 7)%:E * (exp1560 10)%:E * \d_false U) * N^-1%:E. +Proof. +rewrite /staton_bus. +rewrite normalizeE /= !kstaton_bus_exponentialE !diracT !mule1 ifF //. +apply/negbTE; rewrite gt_eqF// lte_fin. +by rewrite addr_gt0// mulr_gt0//= ?divr_gt0// ?ltr0n// exp_density_gt0 ?ltr0n. +Qed. + +End staton_bus_exponential. diff --git a/theories/realfun.v b/theories/realfun.v index 91af1dc51..f32caccf1 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -32,7 +32,7 @@ Implicit Types (a b : R) (f g : R -> R). Lemma continuous_subspace_itv (I : interval R) (f : R -> R) : {in I, continuous f} -> {within [set` I], continuous f}. Proof. -move=> ctsf; apply: continuous_subspaceT => x Ix; apply: ctsf. +move=> ctsf; apply: continuous_in_subspaceT => x Ix; apply: ctsf. by move: Ix; rewrite inE. Qed. @@ -51,10 +51,10 @@ gen have main : f / forall c, {in I, continuous f} -> {in I &, injective f} -> have intP := interval_is_interval aI bI. have cI : c \in I by rewrite intP// (ltW aLc) ltW. have ctsACf : {within `[a, c], continuous f}. - apply: continuous_subspaceT => x; rewrite inE => /itvP axc; apply: fC. + apply: continuous_in_subspaceT => x; rewrite inE => /itvP axc; apply: fC. by rewrite intP// axc/= (le_trans _ (ltW cLb))// axc. have ctsCBf : {within `[c,b], continuous f}. - apply: continuous_subspaceT => x; rewrite inE => /itvP axc; apply: fC. + apply: continuous_in_subspaceT => x; rewrite inE => /itvP axc; apply: fC. by rewrite intP// axc andbT (le_trans (ltW aLc)) ?axc. have [aLb alb'] : a < b /\ a <= b by rewrite ltW (lt_trans aLc). have [faLfc|fcLfa|/eqP faEfc] /= := ltrgtP (f a) (f c). @@ -487,7 +487,7 @@ move=> Hd. wlog xLy : x y / x <= y by move=> H; case: (leP x y) => [/H |/ltW /H]. rewrite -(subKr (f y) (f x)). have [| _ _] := MVT_segment xLy; last by rewrite mul0r => ->; rewrite subr0. -apply/continuous_subspaceT => r _. +apply/continuous_subspaceT=> r. exact/differentiable_continuous/derivable1_diffP. Qed. diff --git a/theories/reals.v b/theories/reals.v index c301b5a46..0ff1b78ea 100644 --- a/theories/reals.v +++ b/theories/reals.v @@ -726,7 +726,7 @@ Proof. move=> yx; exists `|floor (x - y)^-1|%N. rewrite -ltr_subr_addl -{2}(invrK (x - y)%R) ltf_pinv ?qualifE ?ltr0n//. by rewrite invr_gt0 subr_gt0. -rewrite -addn1 natrD natr_absz ger0_norm. +rewrite -natr1 natr_absz ger0_norm. by rewrite floor_ge0 invr_ge0 subr_ge0 ltW. by rewrite -RfloorE lt_succ_Rfloor. Qed. diff --git a/theories/sequences.v b/theories/sequences.v index 61275f94f..5f76422e1 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -1204,7 +1204,7 @@ have /uoo[N _ NuA] : \oo [set m | `|ceil A|.+1 <= m]%N by exists `|ceil A|.+1. near=> n; have /NuA : (N <= n)%N by near: n; exact: nbhs_infty_ge. rewrite /= -(ler_nat R); apply: le_trans. have [A0|A0] := leP 0%R A; last by rewrite (le_trans (ltW A0)). -by rewrite -addn1 natrD natr_absz ger0_norm// ?ceil_ge0// ler_paddr// ceil_ge. +by rewrite -natr1 natr_absz ger0_norm// ?ceil_ge0// ler_paddr// ceil_ge. Unshelve. all: by end_near. Qed. Lemma nat_cvgPpinfty (u : nat^nat) : diff --git a/theories/set_interval.v b/theories/set_interval.v index dcd8df8d9..558a3b143 100644 --- a/theories/set_interval.v +++ b/theories/set_interval.v @@ -413,7 +413,7 @@ Proof. rewrite predeqE => y; split=> /=; last first. by move=> [n _]/=; rewrite in_itv => /andP[xy yn]; rewrite in_itv /= xy. rewrite in_itv /= andbT => xy; exists (`|floor y|%N.+1) => //=. -rewrite in_itv /= xy /= -addn1 natrD. +rewrite in_itv /= xy /= -natr1. have [y0|y0] := ltP 0 y; last by rewrite (le_lt_trans y0)// ltr_spaddr. by rewrite natr_absz ger0_norm ?lt_succ_floor// floor_ge0 ltW. Qed. diff --git a/theories/topology.v b/theories/topology.v index 1aec5e675..8a3f69ccb 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -2127,7 +2127,7 @@ move=> N_gt0 P [n _ Pn]; exists (n * N)%N => //= m. by rewrite /= -leq_divRL//; apply: Pn. Qed. -Lemma near_inftyS (P : set nat) : +Lemma near_inftyS (P : set nat) : (\forall x \near \oo, P (S x)) -> (\forall x \near \oo, P x). Proof. case=> N _ NPS; exists (S N) => // [[]]; rewrite /= ?ltn0 //. Qed. @@ -2507,6 +2507,18 @@ by move=> /(filterI FAu_) => /filter_ex[t [Au_t u_Bt]]; exists (u_ t). Qed. Arguments closed_cvg {T V F FF u_} _ _ _ _ _. +Lemma continuous_closedP (S T : topologicalType) (f : S -> T) : + continuous f <-> forall A, closed A -> closed (f @^-1` A). +Proof. +rewrite continuousP; split=> ctsf ? ?. + by rewrite -openC preimage_setC; apply ctsf; rewrite openC. +by rewrite -closedC preimage_setC; apply ctsf; rewrite closedC. +Qed. + +Lemma closedU (T : topologicalType) (D E : set T) : + closed D -> closed E -> closed (D `|` E). +Proof. by rewrite -?openC setCU; exact: openI. Qed. + Section closure_lemmas. Variable T : topologicalType. Implicit Types E A B U : set T. @@ -5691,6 +5703,29 @@ Lemma closed_subspaceW (U : set T) : closed (U : set T) -> closed (U : set (subspace A)). Proof. by move=> /closed_openC/open_subspaceW/open_closedC; rewrite setCK. Qed. +Lemma open_setIS (U : set (subspace A)) : open A -> + open (U `&` A : set T) = open U. +Proof. +move=> oA; apply/propext; rewrite open_subspaceP. +split=> [|[V [oV <-]]]; last exact: openI. +by move=> oUA; exists (U `&` A); rewrite -setIA setIid. +Qed. + +Lemma open_setSI (U : set (subspace A)) : open A -> open (A `&` U) = open U. +Proof. by move=> oA; rewrite -setIC open_setIS. Qed. + +Lemma closed_setIS (U : set (subspace A)) : closed A -> + closed (U `&` A : set T) = closed U. +Proof. +move=> oA; apply/propext; rewrite closed_subspaceP. +split=> [|[V [oV <-]]]; last exact: closedI. +by move=> oUA; exists (U `&` A); rewrite -setIA setIid. +Qed. + +Lemma closed_setSI (U : set (subspace A)) : + closed A -> closed (A `&` U) = closed U. +Proof. by move=> oA; rewrite -setIC closed_setIS. Qed. + Lemma closure_subspaceW (U : set T) : U `<=` A -> closure (U : set (subspace A)) = closure (U : set T) `&` A. Proof. @@ -5729,6 +5764,110 @@ Qed. End Subspace. +Global Instance subspace_filter {T : topologicalType} + (A : set T) (x : subspace A) : + Filter (nbhs_subspace x) := nbhs_subspace_filter x. + +Global Instance subspace_proper_filter {T : topologicalType} + (A : set T) (x : subspace A) : + ProperFilter (nbhs_subspace x) := nbhs_subspace_filter x. + +Notation "{ 'within' A , 'continuous' f }" := + (continuous (f : subspace A -> _)). + +Section SubspaceRelative. +Context {T : topologicalType}. +Implicit Types (U : topologicalType) (A B : set T). + +Lemma nbhs_subspace_subset A B (x : T) : + A `<=` B -> nbhs (x : subspace B) `<=` nbhs (x : subspace A). +Proof. +rewrite /nbhs //= => AB; case: (nbhs_subspaceP A); case: (nbhs_subspaceP B). +- by move=> ? ?; apply: within_subset => //=; exact: (nbhs_filter x). +- by move=> ? /AB. +- by move=> Bx ? W /nbhs_singleton /(_ Bx) ? ? ->. +- by move=> ? ?. +Qed. + +Lemma continuous_subspaceW {U} A B (f : T -> U) : + A `<=` B -> + {within B, continuous f} -> {within A, continuous f}. +Proof. +by move=> ? ctsF ? ? ?; apply: (@nbhs_subspace_subset A B) => //; exact: ctsF. +Qed. + +Lemma nbhs_subspaceT (x : T) : nbhs (x : subspace setT) = nbhs x. +Proof. +rewrite {1}/nbhs //=; have [_|] := nbhs_subspaceP (@setT T); last by cbn. +rewrite eqEsubset withinE; split => [W [V nbhsV]|W ?]; last by exists W. +by rewrite 2!setIT => ->. +Qed. + +Lemma continuous_subspaceT_for {U} A (f : T -> U) (x : T) : + A x -> {for x, continuous f} -> {for x, continuous (f : subspace A -> U)}. +Proof. +rewrite /filter_of/nbhs/=/prop_for => inA ctsf. +have [_|//] := nbhs_subspaceP A x. +apply: (cvg_trans _ ctsf); apply: cvg_fmap2; apply: cvg_within. +by rewrite /subspace; exact: nbhs_filter. +Qed. + +Lemma continuous_in_subspaceT {U} A (f : T -> U) : + {in A, continuous f} -> {within A, continuous f}. +Proof. +rewrite continuous_subspace_in ?in_setP => ctsf t At. +by apply continuous_subspaceT_for => //=; apply: ctsf. +Qed. + +Lemma continuous_subspaceT{U} A (f : T -> U) : + continuous f -> {within A, continuous f}. +Proof. +move=> ctsf; rewrite continuous_subspace_in => ? ?. +exact: continuous_in_subspaceT => ? ?. +Qed. + +Lemma continuous_open_subspace {U} A (f : T -> U) : + open A -> {within A, continuous f} = {in A, continuous f}. +Proof. +rewrite openE continuous_subspace_in /= => oA; rewrite propeqE ?in_setP. +by split => + x /[dup] Ax /oA Aox => /(_ _ Ax); + rewrite /filter_of -(nbhs_subspace_interior Aox). +Qed. + +Lemma continuous_inP {U} A (f : T -> U) : open A -> + {in A, continuous f} <-> forall X, open X -> open (A `&` f @^-1` X). +Proof. +move=> oA; rewrite -continuous_open_subspace// continuousP. +by under eq_forall do rewrite -open_setSI//. +Qed. + +Lemma pasting {U} A B (f : T -> U) : closed A -> closed B -> + {within A, continuous f} -> {within B, continuous f} -> + {within A `|` B, continuous f}. +Proof. +move=> ? ? ctsA ctsB; apply/continuous_closedP => W oW. +case/continuous_closedP/(_ _ oW)/closed_subspaceP: ctsA => V1 [? V1W]. +case/continuous_closedP/(_ _ oW)/closed_subspaceP: ctsB => V2 [? V2W]. +apply/closed_subspaceP; exists ((V1 `&` A) `|` (V2 `&` B)); split. + by apply: closedU; exact: closedI. +rewrite [RHS]setIUr -V2W -V1W eqEsubset; split=> ?. + by case=> [[][]] ? ? [] ?; [left | left | right | right]; split. +by case=> [][] ? ?; split=> []; [left; split | left | right; split | right]. +Qed. + +Lemma subspaceT_continuous {U} A (B : set U) (f : {fun A >-> B}) : + {within A, continuous f} -> continuous (f : subspace A -> subspace B). +Proof. +move=> /continuousP ctsf; apply/continuousP => O /open_subspaceP [V [oV VBOB]]. +rewrite -open_subspaceIT; apply/open_subspaceP. +case/open_subspaceP: (ctsf _ oV) => W [oW fVA]; exists W; split => //. +rewrite fVA -setIA setIid eqEsubset; split => x [fVx Ax]; split => //. +- by have /[!VBOB]-[] : (V `&` B) (f x) by split => //; exact: funS. +- by have /[!esym VBOB]-[] : (O `&` B) (f x) by split => //; exact: funS. +Qed. + +End SubspaceRelative. + Section SubspaceUniform. Local Notation "A ^-1" := ([set xy | A (xy.2, xy.1)]) : classical_set_scope. Context {X : uniformType} (A : set X). @@ -5837,71 +5976,6 @@ Canonical subspace_pseudoMetricType := End SubspacePseudoMetric. -Global Instance subspace_filter {T : topologicalType} - (A : set T) (x : subspace A) : - Filter (nbhs_subspace x) := nbhs_subspace_filter x. - -Global Instance subspace_proper_filter {T : topologicalType} - (A : set T) (x : subspace A) : - ProperFilter (nbhs_subspace x) := nbhs_subspace_filter x. - -Notation "{ 'within' A , 'continuous' f }" := - (continuous (f : (subspace A) -> _)). - -Section SubspaceRelative. -Context {T : topologicalType}. -Implicit Types (U : topologicalType) (A B : set T). - -Lemma nbhs_subspace_subset A B (x : T) : - A `<=` B -> nbhs (x : subspace B) `<=` nbhs (x : subspace A). -Proof. -rewrite /nbhs //= => AB; case: (nbhs_subspaceP A); case: (nbhs_subspaceP B). -- by move=> ? ?; apply: within_subset => //=; exact: (nbhs_filter x). -- by move=> ? /AB. -- by move=> Bx ? W /nbhs_singleton /(_ Bx) ? ? ->. -- by move=> ? ?. -Qed. - -Lemma continuous_subspaceW {U} A B (f : T -> U) : - A `<=` B -> - {within B, continuous f} -> {within A, continuous f}. -Proof. -by move=> ? ctsF ? ? ?; apply: (@nbhs_subspace_subset A B) => //; exact: ctsF. -Qed. - -Lemma nbhs_subspaceT (x : T) : nbhs (x : subspace setT) = nbhs (x) . -Proof. -rewrite {1}/nbhs //=; have [_|] := nbhs_subspaceP (@setT T); last by cbn. -rewrite eqEsubset withinE; split => [W [V nbhsV]|W ?]; last by exists W. -by rewrite 2!setIT => ->. -Qed. - -Lemma continuous_subspaceT_for {U} A (f : T -> U) (x : T) : - A x -> {for x, continuous f} -> {for x, continuous (f : subspace A -> U)}. -Proof. -rewrite /filter_of/nbhs/=/prop_for => inA ctsf. -have [_|//] := nbhs_subspaceP A x. -apply: (cvg_trans _ ctsf); apply: cvg_fmap2; apply: cvg_within. -by rewrite /subspace; exact: nbhs_filter. -Qed. - -Lemma continuous_subspaceT {U} A (f : T -> U) : - {in A, continuous f} -> {within A, continuous f}. -Proof. -rewrite continuous_subspace_in ?in_setP => ctsf t At. -by apply continuous_subspaceT_for => //=; apply: ctsf. -Qed. - -Lemma continuous_open_subspace {U} A (f : T -> U) : - @open T A -> {within A, continuous f} = {in A, continuous f}. -Proof. -rewrite openE continuous_subspace_in /= => oA; rewrite propeqE ?in_setP. -by split => + x /[dup] Ax /oA Aox; rewrite /filter_of /= => /(_ _ Ax); - rewrite -(nbhs_subspace_interior Aox). -Qed. - -End SubspaceRelative. - Lemma continuous_compact {T U : topologicalType} (f : T -> U) A : {within A, continuous f} -> compact A -> compact (f @` A). Proof. @@ -5995,7 +6069,7 @@ Lemma continuous_localP {X Y : topologicalType} (f : X -> Y) : forall (x : X), \forall U \near powerset_filter_from (nbhs x), {within U, continuous f}. Proof. -split; first by move=> ? ?; near=> U; apply: continuous_subspaceT => ? ?; exact. +split; first by move=> ? ?; near=> U; apply: continuous_subspaceT=> ?; exact. move=> + x => /(_ x)/near_powerset_filter_fromP. case; first by move=> ? ?; exact: continuous_subspaceW. move=> U nbhsU wctsf; wlog oU : U wctsf nbhsU / open U. @@ -6121,7 +6195,7 @@ Lemma precompact_pointwise_precompact (W : set {family compact, X -> Y}) : Proof. move=> + x; rewrite ?precompactE => pcptW. have : compact (prod_topo_apply x @` (closure W)). - apply: continuous_compact => //; apply: continuous_subspaceT => g _. + apply: continuous_compact => //; apply: continuous_subspaceT=> g. move=> E nbhsE; have := (@prod_topo_apply_continuous _ _ x g E nbhsE). exact: (@pointwise_cvg_compact_family _ _ (nbhs g)). move=> /[dup]/(compact_closed hsdf)/closure_id -> /subclosed_compact. @@ -6252,7 +6326,7 @@ apply/continuous_localP => x'; apply/near_powerset_filter_fromP. by move=> ? ?; exact: continuous_subspaceW. case: (@lcptX x') => // U; rewrite withinET => nbhsU [cptU _]. exists U => //; apply: (uniform_limit_continuous_subspace PG _ _). - by near=> g; apply: continuous_subspaceT => + _; near: g; exact: GW. + by near=> g; apply: continuous_subspaceT; near: g; exact: GW. by move/fam_cvgP/(_ _ cptU) : Gf. Unshelve. end_near. Qed. diff --git a/theories/trigo.v b/theories/trigo.v index 3a50493a0..d2bd4069b 100644 --- a/theories/trigo.v +++ b/theories/trigo.v @@ -560,10 +560,9 @@ Qed. Lemma cos_exists : exists2 pih : R, 1 <= pih <= 2 & cos pih = 0. Proof. have /IVT[] : minr (cos 1) (cos 2) <= (0 : R) <= maxr (cos 1) (cos 2). - - rewrite /minr /maxr ltNge (ltW (lt_trans cos2_lt0 cos1_gt0))/=. - by rewrite (ltW cos2_lt0)/= (ltW cos1_gt0). + - by rewrite le_maxr (ltW cos1_gt0) le_minl (ltW cos2_lt0) orbC. - by rewrite ler1n. - - by move=> *; apply/continuous_subspaceT=> ? _; exact: continuous_cos. + - by apply/continuous_subspaceT => ?; exact: continuous_cos. by move=> pih /itvP pihI chpi_eq0; exists pih; rewrite ?pihI. Qed. @@ -577,7 +576,7 @@ case: (x =P y) => // /eqP xDy. have xLLs : x < y by rewrite le_eqVlt (negPf xDy) in xLy. have /(Rolle xLLs)[x1 _|x1|x1 x1I [_ x1D]] : cos x = cos y by rewrite cy0. - exact: derivable_cos. -- by apply/continuous_subspaceT=> ? _; exact: continuous_cos. +- by apply/continuous_subspaceT => ?; exact: continuous_cos. - have [_ /esym/eqP] := is_derive_cos x1; rewrite x1D oppr_eq0 => /eqP Hs. suff : 0 < sin x1 by rewrite Hs ltxx. apply/sin2_gt0/andP; split. @@ -641,13 +640,13 @@ wlog : x / 0 <= x => [Hw|x_ge0]. move=> /andP[x_gt0 xLpi2]; case: (ler0P (cos x)) => // cx_le0. have /IVT[]// : minr (cos 0) (cos x) <= 0 <= maxr (cos 0) (cos x). by rewrite cos0 /minr /maxr !ifN ?cx_le0 //= -leNgt (le_trans cx_le0). -- by move=> *; apply/continuous_subspaceT=> ? _; apply: continuous_cos. -move=> x1 /itvP Hx1 cx1_eq0. +- by apply/continuous_subspaceT => ?; exact: continuous_cos. +move=> x1 /itvP xx1 cx1_eq0. suff x1E : x1 = pi/2. - have : x1 < pi / 2 by apply: le_lt_trans xLpi2; rewrite Hx1. + have : x1 < pi / 2 by apply: le_lt_trans xLpi2; rewrite xx1. by rewrite x1E ltxx. apply: cos_02_uniq=> //; last by case pihalf_02_cos_pihalf => _ ->. - by rewrite Hx1 ltW // (lt_trans _ pihalf_lt2) // (le_lt_trans _ xLpi2) // Hx1. + by rewrite xx1 ltW // (lt_trans _ pihalf_lt2) // (le_lt_trans _ xLpi2) // xx1. by rewrite divr_ge0 ?(ltW pihalf_lt2)// pi_ge0. Qed. @@ -732,7 +731,7 @@ move=> x y; rewrite !in_itv/= le_eqVlt; case: eqP => [<- _|_] /=. rewrite y_gt0; apply/idP. suff : cos y != 1 by case: ltrgtP (cos_le1 y). rewrite -cos0 eq_sym; apply/eqP => /Rolle [||x1|x1 /itvP x1I [_ x1D]] //. - by apply/continuous_subspaceT=> ? _; exact: continuous_cos. + by apply/continuous_subspaceT => ?; exact: continuous_cos. case: (is_derive_cos x1) => _ /eqP; rewrite x1D eq_sym oppr_eq0 => /eqP s_eq0. suff : 0 < sin x1 by rewrite s_eq0 ltxx. by apply: sin_gt0_pi; rewrite x1I /= (lt_le_trans (_ : _ < y)) ?x1I // yI. @@ -747,7 +746,7 @@ rewrite le_eqVlt; case: eqP => /= [-> _ | _ /andP[y_gt0 y_ltpi]]. rewrite cospi x_ltpi; apply/idP. suff : cos x != -1 by case: ltrgtP (cos_geN1 x). rewrite -cospi; apply/eqP => /Rolle [||x1|x1 /itvP x1I [_ x1D]] //. - by apply/continuous_subspaceT=> ? _; exact: continuous_cos. + by apply/continuous_subspaceT => ?; exact: continuous_cos. case: (is_derive_cos x1) => _ /eqP; rewrite x1D eq_sym oppr_eq0 => /eqP s_eq0. suff : 0 < sin x1 by rewrite s_eq0 ltxx. by apply: sin_gt0_pi; rewrite x1I /= (lt_le_trans (_ : _ < x)) ?x1I. @@ -757,8 +756,8 @@ wlog xLy : x y x_gt0 x_ltpi y_gt0 y_ltpi / x <= y => [H | ]. case: (x =P y) => [->| /eqP xDy]; first by rewrite ltxx. have xLLs : x < y by rewrite le_eqVlt (negPf xDy) in xLy. rewrite xLLs -subr_gt0 -opprB; rewrite -subr_gt0 in xLLs; apply/idP. -have [x1|z /itvP zI ->] := @MVT_segment _ cos (-sin) _ _ xLy. - by apply/continuous_subspaceT=> ? _; exact: continuous_cos. +have [x1|z /itvP zI ->] := @MVT_segment _ cos (- sin) _ _ xLy. + by apply/continuous_subspaceT => ?; exact: continuous_cos. rewrite -mulNr opprK mulr_gt0 //; apply: sin_gt0_pi. by rewrite (lt_le_trans x_gt0) ?zI //= (le_lt_trans _ y_ltpi) ?zI. Qed. @@ -870,8 +869,7 @@ Proof. by move=> /is_derive_tan[]. Qed. Lemma ltr_tan : {in `](- (pi/2)), (pi/2)[ &, {mono tan : x y / x < y}}. Proof. -move=> x y. -wlog xLy : x y / x <= y => [H | ] xB yB. +move=> x y; wlog xLy : x y / x <= y => [H xB yB|/itvP xB /itvP yB]. case: (lerP x y) => [/H //->//|yLx]. by rewrite !ltNge ltW ?(ltW yLx) // H // ltW. case: (x =P y) => [->| /eqP xDy]; first by rewrite ltxx. @@ -879,16 +877,14 @@ have xLLs : x < y by rewrite le_eqVlt (negPf xDy) in xLy. rewrite -subr_gt0 xLLs; rewrite -subr_gt0 in xLLs; apply/idP. have [x1 /itvP x1I|z |] := @MVT_segment _ tan (fun x => (cos x) ^-2) _ _ xLy. - apply: is_derive_tan. - rewrite gt_eqF // cos_gt0_pihalf // (@lt_le_trans _ _ x) ?x1I ?(itvP xB)//=. - by rewrite (@le_lt_trans _ _ y) ?x1I ?(itvP yB). -- apply/continuous_subspaceT=> ? inI; apply: continuous_tan. - rewrite /= inE /<=%O/= in inI; move/andP: inI => /= [? ?]. - rewrite gt_eqF // cos_gt0_pihalf // (@lt_le_trans _ _ x) ?zI ?(itvP xB)//=. - rewrite (@le_lt_trans _ _ y) ?zI ?(itvP yB) //. + rewrite gt_eqF // cos_gt0_pihalf // (@lt_le_trans _ _ x) ?x1I ?xB//=. + by rewrite (@le_lt_trans _ _ y) ?x1I ?yB. +- apply/continuous_in_subspaceT => ? -/[!(@mem_setE R)] /itvP inI. + apply: continuous_tan; rewrite gt_eqF// cos_gt0_pihalf//. + by rewrite (@lt_le_trans _ _ x) ?xB ?inI// (@le_lt_trans _ _ y) ?yB ?inI. - move=> x1 /itvP x1I ->. rewrite mulr_gt0 // invr_gt0 // exprn_gte0 // cos_gt0_pihalf //. - rewrite (@lt_le_trans _ _ x) ?x1I ?(itvP xB)//=. - by rewrite (@le_lt_trans _ _ y) ?x1I ?(itvP yB). + by rewrite (@lt_le_trans _ _ x) ?x1I ?xB//= (@le_lt_trans _ _ y) ?x1I ?yB. Qed. Lemma tan_inj : {in `](- (pi/2)), (pi/2)[ &, injective tan}. @@ -917,7 +913,7 @@ have /(IVT (@pi_ge0 _))[] // : minr (f 0) (f pi) <= 0 <= maxr (f 0) (f pi). rewrite /f cos0 cospi /minr /maxr ltr_add2r -subr_lt0 opprK (_ : 1 + 1 = 2)//. by rewrite ltrn0 subr_le0 subr_ge0. - move=> y y0pi. - by apply: continuousB; apply/continuous_subspaceT=> ? ?; + by apply: continuousB; apply/continuous_in_subspaceT => ? ?; [exact: continuous_cos|exact: cst_continuous]. - rewrite /f => x1 /itvP x1I /eqP; rewrite subr_eq0 => /eqP cosx1E. by case: (He x1); rewrite !x1I. @@ -1043,7 +1039,7 @@ have /IVT[] // : rewrite /f sinN sin_pihalf /minr /maxr ltr_add2r -subr_gt0 opprK. by rewrite (_ : 1 + 1 = 2)// ltr0n/= subr_le0 subr_ge0. - by rewrite -subr_ge0 opprK -splitr pi_ge0. -- by move=> *; apply: continuousB; apply/continuous_subspaceT=> ? ?; +- by move=> *; apply: continuousB; apply/continuous_in_subspaceT => ? ?; [exact: continuous_sin| exact: cst_continuous]. - rewrite /f => x1 /itvP x1I /eqP; rewrite subr_eq0 => /eqP sinx1E. by case: (He x1); rewrite !x1I. diff --git a/theories/wip.v b/theories/wip.v new file mode 100644 index 000000000..c31538faa --- /dev/null +++ b/theories/wip.v @@ -0,0 +1,152 @@ +From HB Require Import structures. +From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +From mathcomp Require Import rat. +Require Import mathcomp_extra boolp classical_sets signed functions cardinality. +Require Import reals ereal topology normedtype sequences esum measure. +Require Import lebesgue_measure fsbigop numfun lebesgue_integral exp kernel. +Require Import trigo prob_lang. + +(******************************************************************************) +(* Semantics of a programming language PPL using s-finite kernels (wip) *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Import Order.TTheory GRing.Theory Num.Def Num.ExtraDef Num.Theory. +Import numFieldTopology.Exports. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. +Local Open Scope ereal_scope. + +Section gauss. +Variable R : realType. +Local Open Scope ring_scope. + +(* density function for gauss *) +Definition gauss_density m s x : R := + (s * sqrtr (pi *+ 2))^-1 * expR (- ((x - m) / s) ^+ 2 / 2%:R). + +Lemma gauss_density_ge0 m s x : 0 <= s -> 0 <= gauss_density m s x. +Proof. by move=> s0; rewrite mulr_ge0 ?expR_ge0// invr_ge0 mulr_ge0. Qed. + +Lemma gauss_density_gt0 m s x : 0 < s -> 0 < gauss_density m s x. +Proof. +move=> s0; rewrite mulr_gt0 ?expR_gt0// invr_gt0 mulr_gt0//. +by rewrite sqrtr_gt0 pmulrn_rgt0// pi_gt0. +Qed. + +Definition gauss01_density : R -> R := gauss_density 0 1. + +Lemma gauss01_densityE x : + gauss01_density x = (sqrtr (pi *+ 2))^-1 * expR (- (x ^+ 2) / 2%:R). +Proof. by rewrite /gauss01_density /gauss_density mul1r subr0 divr1. Qed. + +Definition mgauss01 (V : set R) := + \int[lebesgue_measure]_(x in V) (gauss01_density x)%:E. + +Lemma measurable_fun_gauss_density m s : + measurable_fun setT (gauss_density m s). +Proof. +apply: measurable_funM; first exact: measurable_fun_cst. +apply: measurable_fun_comp => /=. + by apply: continuous_measurable_fun; apply continuous_expR. +apply: measurable_funM; last exact: measurable_fun_cst. +apply: measurable_fun_comp => /=; first exact: measurable_fun_opp. +apply: measurable_fun_exprn. +apply: measurable_funM => /=; last exact: measurable_fun_cst. +apply: measurable_funD => //; first exact: measurable_fun_id. +exact: measurable_fun_cst. +Qed. + +Let mgauss010 : mgauss01 set0 = 0%E. +Proof. by rewrite /mgauss01 integral_set0. Qed. + +Let mgauss01_ge0 A : (0 <= mgauss01 A)%E. +Proof. +by rewrite /mgauss01 integral_ge0//= => x _; rewrite lee_fin gauss_density_ge0. +Qed. + +Axiom integral_gauss01_density : + \int[lebesgue_measure]_x (gauss01_density x)%:E = 1%E. + +Let mgauss01_sigma_additive : semi_sigma_additive mgauss01. +Proof. +move=> /= F mF tF mUF. +rewrite /mgauss01/= integral_bigcup//=; last first. + split. + apply/EFin_measurable_fun. + exact: measurable_funS (measurable_fun_gauss_density 0 1). + rewrite (_ : (fun x => _) = (EFin \o gauss01_density)); last first. + by apply/funext => x; rewrite gee0_abs// lee_fin gauss_density_ge0. + apply: le_lt_trans. + apply: (@subset_integral _ _ _ _ _ setT) => //=. + apply/EFin_measurable_fun. + exact: measurable_fun_gauss_density. + by move=> ? _; rewrite lee_fin gauss_density_ge0. + by rewrite integral_gauss01_density// ltey. +apply: is_cvg_ereal_nneg_natsum_cond => n _ _. +by apply: integral_ge0 => /= x ?; rewrite lee_fin gauss_density_ge0. +Qed. + +HB.instance Definition _ := isMeasure.Build _ _ _ + mgauss01 mgauss010 mgauss01_ge0 mgauss01_sigma_additive. + +Let mgauss01_setT : mgauss01 [set: _] = 1%E. +Proof. by rewrite /mgauss01 integral_gauss01_density. Qed. + +HB.instance Definition _ := @isProbability.Build _ _ R mgauss01 mgauss01_setT. + +Definition gauss01 := [the probability _ _ of mgauss01]. + +End gauss. + +Section gauss_lebesgue. +Import Notations. +Variables (R : realType) (d : _) (T : measurableType d). + +Let f1 (x : R) := (gauss01_density x) ^-1. + +Let mf1 : measurable_fun setT f1. +Proof. +apply: (measurable_fun_comp' (F := [set r : R | r != 0%R])) => //. +- exact: open_measurable. +- by move=> /= r [t _ <-]; rewrite gt_eqF// gauss_density_gt0. +- apply: open_continuous_measurable_fun => //. + by apply/in_setP => x /= x0; exact: inv_continuous. +- exact: measurable_fun_gauss_density. +Qed. + +Variable mu : {measure set mR R -> \bar R}. + +Definition staton_lebesgue : R.-sfker T ~> _ := + letin (sample (@gauss01 R)) + (letin + (score (measurable_fun_comp mf1 var2of2)) + (ret var2of3)). + +Lemma staton_lebesgueE x U : measurable U -> + staton_lebesgue x U = lebesgue_measure U. +Proof. +move=> mU; rewrite [in LHS]/staton_lebesgue/=. +rewrite [in LHS]letinE. +rewrite [in LHS]/sample. +unlock. +rewrite [in LHS]/=. +transitivity (\int[@mgauss01 R]_(y in U) (f1 y)%:E). + rewrite -[in RHS](setTI U) integral_setI_indic//=. + apply: eq_integral => /= r _. + rewrite letinE/= ge0_integral_mscale//= ger0_norm//; last first. + by rewrite invr_ge0// gauss_density_ge0. + by rewrite integral_dirac// indicT mul1e retE/= diracE indicE. +transitivity (\int[lebesgue_measure]_(x in U) (gauss01_density x * f1 x)%:E). + admit. +transitivity (\int[lebesgue_measure]_(x in U) (\1_U x)%:E). + apply: eq_integral => /= y yU. + by rewrite /f1 divrr ?indicE ?yU// unitfE gt_eqF// gauss_density_gt0. +by rewrite integral_indic//= setIid. +Abort. + +End gauss_lebesgue.