diff --git a/CHANGELOG.md b/CHANGELOG.md index a3a1f0e547..9c4c1d90da 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,121 @@ # Changelog -Latest releases: [[1.7.0] - 2024-11-22](#170---2024-11-22) and [[1.6.0] - 2024-10-25](#160---2024-10-25) +Latest releases: [[1.8.0] - 2024-12-19](#180---2024-12-19), [[1.7.0] - 2024-11-22](#170---2024-11-22) and [[1.6.0] - 2024-10-25](#160---2024-10-25) + +## [1.8.0] - 2024-12-19 + +### Added + +- in `mathcomp_extra.v`: + + lemma `partition_disjoint_bigfcup` + +- in `constructive_ereal.v`: + + notations `\prod` in scope ereal_scope + + lemmas `prode_ge0`, `prode_fin_num` + +- in `num_topology.v`: + + lemma `in_continuous_mksetP` + +- in `normedtype.v`: + + lemmas `continuous_within_itvcyP`, `continuous_within_itvNycP` + +- in file `realfun.v`: + + lemma `cvg_nbhsP` + +- in `measure.v`: + + lemma `countable_bigcupT_measurable` + + definition `discrete_measurable` + + lemmas `discrete_measurable0`, `discrete_measurableC`, `discrete_measurableU` + +- in `lebesgue_measure.v`: + + lemma `measurable_indicP` + + lemma `measurable_powRr` + +- in `lebesgue_integral.v`: + + definition `dyadic_approx` (was `Let A`) + + definition `integer_approx` (was `Let B`) + + lemma `measurable_sum` + + lemma `integrable_indic` + + lemmas `integrable_pushforward`, `integral_pushforward` + + lemma `integral_measure_add` + +- in `probability.v`: + + lemma `expectation_def` + + notation `'M_` + + lemma `integral_distribution` (existing lemma `integral_distribution` has been renamed) + +### Changed + +- in `lebesgue_integrale.v` + + change implicits of `measurable_funP` + +### Renamed + +- in `classical_sets.v`: + + `preimage_itv_o_infty` -> `preimage_itvoy` + + `preimage_itv_c_infty` -> `preimage_itvcy` + + `preimage_itv_infty_o` -> `preimage_itvNyo` + + `preimage_itv_infty_c` -> `preimage_itvNyc` + +- in `constructive_ereal.v`: + + `maxeMr` -> `maxe_pMr` + + `maxeMl` -> `maxe_pMl` + + `mineMr` -> `mine_pMr` + + `mineMl` -> `mine_pMl` + +- file `homotopy_theory/path.v` -> `homotopy_theory/continuous_path.v` + +- in `lebesgue_measure.v`: + + `measurable_fun_indic` -> `measurable_indic` + + `emeasurable_fun_sum` -> `emeasurable_sum` + + `emeasurable_fun_fsum` -> `emeasurable_fsum` + + `ge0_emeasurable_fun_sum` -> `ge0_emeasurable_sum` + +- in `probability.v`: + + `expectationM` -> `expectationZl` + + `integral_distribution` -> `ge0_integral_distribution` + +### Generalized + +- in `sequences.v`: + + lemmas `cvg_restrict`, `cvg_centern`, `cvg_shiftn cvg_shiftS` + +- in `lebesgue_integral.v`: + + lemma `measurable_sfunP` + +- in `probability.v`: + + definition `random_variable` + + lemmas `notin_range_measure`, `probability_range` + + definition `distribution` + + lemma `probability_distribution`, `integral_distribution` + + mixin `MeasurableFun_isDiscrete` + + structure `discreteMeasurableFun` + + definition `discrete_random_variable` + + lemma `dRV_dom_enum` + + definitions `dRV_dom`, `dRV_enum`, `enum_prob` + + lemmas `distribution_dRV`, `sum_enum_prob` + +### Deprecated + +- in file `lebesgue_integral.v`: + + lemma `approximation` + +### Removed + +- in `constructive_ereal.v` + + notation `lee_opp` (deprecated since 0.6.5) + + notation `lte_opp` (deprecated since 0.6.5) + +- in `measure.v`: + + `dynkin_setI_bigsetI` (use `big_ind` instead) + +- in `lebesgue_measurable.v`: + + notation `measurable_fun_power_pos` (deprecated since 0.6.3) + + notation `measurable_power_pos` (deprecated since 0.6.4) + +- in `lebesgue_integral.v`: + + lemma `measurable_indic` (was uselessly specializing `measurable_fun_indic` (now `measurable_indic`) from `lebesgue_measure.v`) + + notation `measurable_fun_indic` (deprecation since 0.6.3) ## [1.7.0] - 2024-11-22 diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 96159a84cb..fc18624398 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,107 +4,82 @@ ### Added -- in `num_topology.v`: - + lemma `in_continuous_mksetP` +- in `mathcomp_extra.v`: + + lemmas `prodr_ile1`, `nat_int` - in `normedtype.v`: - + lemmas `continuous_within_itvcyP`, `continuous_within_itvNycP` + + lemma `scaler1` -- in `mathcomp_extra.v`: - + lemma `partition_disjoint_bigfcup` -- in `lebesgue_measure.v`: - + lemma `measurable_indicP` +- in `derive.v`: + + lemmas `horner0_ext`, `hornerD_ext`, `horner_scale_ext`, `hornerC_ext`, + `derivable_horner`, `derivE`, `continuous_horner` + + instance `is_derive_poly` - in `lebesgue_integral.v`: - + definition `dyadic_approx` (was `Let A`) - + definition `integer_approx` (was `Let B`) - + lemma `measurable_sum` - + lemma `integrable_indic` - -- in `constructive_ereal.v`: - + notations `\prod` in scope ereal_scope - + lemmas `prode_ge0`, `prode_fin_num` -- in `probability.v`: - + lemma `expectation_def` - + notation `'M_` + + lemmas `integral_fin_num_abs`, `Rintegral_cst`, `le_Rintegral` -- in `lebesgue_integral.v`: - + lemmas `integrable_pushforward`, `integral_pushforward` - + lemma `integral_measure_add` +- new file `pi_irrational.v`: + + lemmas `measurable_poly` + + definition `rational` + + module `pi_irrational` + + lemma `pi_irrationnal` + +- in `numfun.v` + + lemmas `funeposE`, `funenegE`, `funepos_comp`, `funeneg_comp` -- in `probability.v` - + lemma `integral_distribution` (existsing lemma `integral_distribution` has been renamed) +- in `classical_sets.v`: + + lemmas `xsectionE`, `ysectionE` -- in file `realfun.v`: - + lemma `cvg_nbhsP` +- in `derive.v`: + + lemmas `differentiable_subr_neq0`, `cauchy_MVT`, + `lhopital_right`, `lhopital_left` ### Changed - in `lebesgue_integrale.v` + change implicits of `measurable_funP` - -### Renamed -- in `lebesgue_measure.v`: - + `measurable_fun_indic` -> `measurable_indic` - + `emeasurable_fun_sum` -> `emeasurable_sum` - + `emeasurable_fun_fsum` -> `emeasurable_fsum` - + `ge0_emeasurable_fun_sum` -> `ge0_emeasurable_sum` -- in `probability.v`: - + `expectationM` -> `expectationZl` +- in `derive.v`: + + put the notation ``` ^`() ``` and ``` ^`( _ ) ``` in scope `classical_set_scope` -- in `classical_sets.v`: - + `preimage_itv_o_infty` -> `preimage_itvoy` - + `preimage_itv_c_infty` -> `preimage_itvcy` - + `preimage_itv_infty_o` -> `preimage_itvNyo` - + `preimage_itv_infty_c` -> `preimage_itvNyc` +- in `numfun.v` + + lock `funepos`, `funeneg` -- in `constructive_ereal.v`: - + `maxeMr` -> `maxe_pMr` - + `maxeMl` -> `maxe_pMl` - + `mineMr` -> `mine_pMr` - + `mineMl` -> `mine_pMl` +- moved from `lebesgue_integral.v` to `measure.v` and generalized + + lemmas `measurable_xsection`, `measurable_ysection` -- in `probability.v`: - + `integral_distribution` -> `ge0_integral_distribution` +### Renamed -- file `homotopy_theory/path.v` -> `homotopy_theory/continuous_path.v` +- in `measure.v` + + `preimage_class` -> `preimage_set_system` + + `image_class` -> `image_set_system` + + `preimage_classes` -> `g_sigma_preimageU` + + `preimage_class_measurable_fun` -> `preimage_set_system_measurable_fun` + + `sigma_algebra_preimage_class` -> `sigma_algebra_preimage` + + `sigma_algebra_image_class` -> `sigma_algebra_image` + + `sigma_algebra_preimage_classE` -> `g_sigma_preimageE` + + `preimage_classes_comp` -> `g_sigma_preimageU_comp` ### Generalized -- in `sequences.v`: - + lemmas `cvg_restrict`, `cvg_centern`, `cvg_shiftn cvg_shiftS` - -- in `probability.v`: - + definition `random_variable` - + lemmas `notin_range_measure`, `probability_range` - + definition `distribution` - + lemma `probability_distribution`, `integral_distribution` - + mixin `MeasurableFun_isDiscrete` - + structure `discreteMeasurableFun` - + definition `discrete_random_variable` - + lemma `dRV_dom_enum` - + definitions `dRV_dom`, `dRV_enum`, `enum_prob` - + lemmas `distribution_dRV`, `sum_enum_prob` - -- in `lebesgue_integral.v`: - + lemma `measurable_sfunP` - +- in `sequences.v`, + + generalized indexing from zero-based ones (`0 <= k < n` and `k [[T F]|T]; [left; exists (Empty.Pack F) | right; exists T]. Qed. + Lemma Ppointed : quasi_canonical Type pointedType. Proof. by apply: qcanon; elim/Peq; elim/eqPpointed => [[T F]|T]; @@ -3262,11 +3263,17 @@ Proof. by apply/idP/idP => [|]; [rewrite inE|rewrite /ysection !inE /= inE]. Qed Lemma ysectionP x y A : ysection A y x <-> A (x, y). Proof. by rewrite /ysection/= inE. Qed. +Lemma xsectionE A x : xsection A x = (fun y => (x, y)) @^-1` A. +Proof. by apply/seteqP; split => [y|y] /xsectionP. Qed. + +Lemma ysectionE A y : ysection A y = (fun x => (x, y)) @^-1` A. +Proof. by apply/seteqP; split => [x|x] /ysectionP. Qed. + Lemma xsection0 x : xsection set0 x = set0. -Proof. by rewrite predeqE /xsection => y; split => //=; rewrite inE. Qed. +Proof. by rewrite xsectionE preimage_set0. Qed. Lemma ysection0 y : ysection set0 y = set0. -Proof. by rewrite predeqE /ysection => x; split => //=; rewrite inE. Qed. +Proof. by rewrite ysectionE preimage_set0. Qed. Lemma in_xsectionX X1 X2 x : x \in X1 -> xsection (X1 `*` X2) x = X2. Proof. diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index f7c05dd232..7f5eeb3af2 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -501,6 +501,9 @@ End floor_ceil. #[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to `ceil_gt_int`")] Notation ceil_lt_int := ceil_gt_int (only parsing). +Lemma nat_int {R : archiNumDomainType} n : n%:R \is a @Num.int R. +Proof. by rewrite Num.Theory.intrEge0. Qed. + Section bijection_forall. Lemma bij_forall A B (f : A -> B) (P : B -> Prop) : @@ -573,3 +576,15 @@ by apply: contraNeq (disjF _ _ iK jK) _; rewrite -fsetI_eq0 eqFij fsetIid. Qed. End FsetPartitions. + +(* TODO: move to ssrnum *) +Lemma prodr_ile1 {R : realDomainType} (s : seq R) : + (forall x, x \in s -> 0 <= x <= 1)%R -> (\prod_(j <- s) j <= 1)%R. +Proof. +elim: s => [_ | y s ih xs01]; rewrite ?big_nil// big_cons. +have /andP[y0 y1] : (0 <= y <= 1)%R by rewrite xs01// mem_head. +rewrite mulr_ile1 ?andbT//. + rewrite big_seq prodr_ge0// => x xs. + by have := xs01 x; rewrite inE xs orbT => /(_ _)/andP[]. +by rewrite ih// => e xs; rewrite xs01// in_cons xs orbT. +Qed. diff --git a/reals_stdlib/Rstruct.v b/reals_stdlib/Rstruct.v index 998ed7690c..760cd14e50 100644 --- a/reals_stdlib/Rstruct.v +++ b/reals_stdlib/Rstruct.v @@ -25,7 +25,7 @@ liability. See the COPYING file for more details. (* # Compatibility with the real numbers of Coq *) (******************************************************************************) -From Coq Require Import Rdefinitions Raxioms RIneq Rbasic_fun Zwf. +From Coq Require Import ZArith Rdefinitions Raxioms RIneq Rbasic_fun Zwf. From Coq Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def. From Coq Require Import Rtrigo1 Reals. From mathcomp Require Import all_ssreflect ssralg poly mxpoly ssrnum. diff --git a/theories/Make b/theories/Make index de272b2319..35f6699fb2 100644 --- a/theories/Make +++ b/theories/Make @@ -56,5 +56,6 @@ lebesgue_stieltjes_measure.v convex.v charge.v kernel.v +pi_irrational.v all_analysis.v showcase/summability.v diff --git a/theories/all_analysis.v b/theories/all_analysis.v index 99bdb7e9d6..3eb98668dd 100644 --- a/theories/all_analysis.v +++ b/theories/all_analysis.v @@ -23,3 +23,4 @@ From mathcomp Require Export lebesgue_stieltjes_measure. From mathcomp Require Export convex. From mathcomp Require Export charge. From mathcomp Require Export kernel. +From mathcomp Require Export pi_irrational. diff --git a/theories/charge.v b/theories/charge.v index f232b0381d..64323cb44c 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -695,7 +695,7 @@ exists (D `\` Aoo). have cvg_nuA : (\sum_(0 <= i < n) nu (A_ (v i))) @[n --> \oo]--> nu Aoo. exact: charge_semi_sigma_additive. have nuAoo : 0 <= nu Aoo. - move/cvg_lim : cvg_nuA => <-//=; apply: nneseries_ge0 => n _. + move/cvg_lim : cvg_nuA => <-//=; apply: nneseries_ge0 => n _ _. exact: nuA_ge0. have A_cvg_0 : nu (A_ (v n)) @[n --> \oo] --> 0. rewrite [X in X @ _ --> _](_ : _ = (fun n => (fine (nu (A_ (v n))))%:E)); last first. @@ -853,7 +853,7 @@ move=> /cvg_ex[[l| |]]; first last. by rewrite leNgt => /negP; apply; rewrite ltNye_eq fin_num_measure. - move/cvg_lim => limoo. have := @npeseries_le0 _ (fun n => maxe (z_ (v n) * 2^-1%:E) (- 1%E)) xpredT 0. - by rewrite limoo// leNgt => /(_ (fun n _ => max_le0 n))/negP; apply. + by rewrite limoo// leNgt => /(_ (fun n _ _ => max_le0 n))/negP; exact. move/fine_cvgP => [Hfin cvgl]. have : cvg (series (fun n => fine (maxe (z_ (v n) * 2^-1%:E) (- 1%E))) n @[n --> \oo]). apply/cvg_ex; exists l; move: cvgl. diff --git a/theories/convex.v b/theories/convex.v index dde76d9a14..fbd28dd43d 100644 --- a/theories/convex.v +++ b/theories/convex.v @@ -226,7 +226,9 @@ have [c1 Ic1 Hc1] : exists2 c1, a < c1 < x & (f x - f a) / (x - a) = 'D_1 f c1. have := derivable_within_continuous HDf. rewrite continuous_open_subspace//; last exact: interval_open. by apply; rewrite inE/= in_itv/= ax. - by exists z => //; rewrite fxfa -mulrA divff ?mulr1// subr_eq0 gt_eqF. + exists z; first by []. + rewrite fxfa -mulrA divff; first exact: mulr1. + by rewrite subr_eq0 gt_eqF. have c1c2 : c1 < c2. by move: Ic2 Ic1 => /andP[+ _] => /[swap] /andP[_] /lt_trans; apply. have [d Id h] : @@ -245,7 +247,9 @@ have [d Id h] : + apply: cvg_at_left_filter. move: cDf; rewrite continuous_open_subspace//; last exact: interval_open. by apply; rewrite inE/= in_itv/= (andP Ic2).2 (lt_trans (andP Ic1).1). - by exists z => //; rewrite h -mulrA divff ?mulr1// subr_eq0 gt_eqF. + exists z; first by []. + rewrite h -mulrA divff; first exact: mulr1. + by rewrite subr_eq0 gt_eqF. have LfE : L x - f x = ((x - a) * (b - x)) / (b - a) * ((f b - f x) / (b - x)) - ((b - x) * factor a b x) * ((f x - f a) / (x - a)). diff --git a/theories/derive.v b/theories/derive.v index c368957b03..cd4147993e 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -3,7 +3,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import reals signed topology prodnormedzmodule tvs. -From mathcomp Require Import normedtype landau forms. +From mathcomp Require Import normedtype landau forms poly. (**md**************************************************************************) (* # Differentiation *) @@ -11,7 +11,8 @@ From mathcomp Require Import normedtype landau forms. (* This file provides a theory of differentiation. It includes the standard *) (* rules of differentiation (differential of a sum, of a product, of *) (* exponentiation, of the inverse, etc.) as well as standard theorems (the *) -(* Extreme Value Theorem, Rolle's theorem, the Mean Value Theorem). *) +(* Extreme Value Theorem, Rolle's theorem, the Mean Value Theorem, Cauchy's *) +(* mean value theorem, L'Hopital's rule). *) (* *) (* Parsable notations (in all of the following, f is not supposed to be *) (* differentiable): *) @@ -389,8 +390,8 @@ Proof. exact: iterSr. Qed. End DifferentialR2. -Notation "f ^` ()" := (derive1 f). -Notation "f ^` ( n )" := (derive1n n f). +Notation "f ^` ()" := (derive1 f) : classical_set_scope. +Notation "f ^` ( n )" := (derive1n n f) : classical_set_scope. Section DifferentialR3. Variable R : numFieldType. @@ -563,14 +564,14 @@ Proof. by move=> df dg; apply/diff_unique; have [] := dadd df dg. Qed. Lemma differentiableD (f g : V -> W) x : differentiable f x -> differentiable g x -> differentiable (f + g) x. Proof. -by move=> df dg; apply/diff_locallyP; rewrite diffD //; have := dadd df dg. +by move=> df dg; apply/diff_locallyP; rewrite diffD; have := dadd df dg. Qed. Global Instance is_diffD (f g df dg : V -> W) x : is_diff x f df -> is_diff x g dg -> is_diff x (f + g) (df + dg). Proof. move=> dfx dgx; apply: DiffDef; first exact: differentiableD. -by rewrite diffD // !diff_val. +by rewrite diffD; first (congr (_ + _); apply: diff_val). Qed. Lemma differentiable_sum n (f : 'I_n -> V -> W) (x : V) : @@ -606,7 +607,9 @@ Proof. by move=> dfx dgx; apply: is_diff_eq. Qed. Lemma diffB (f g : V -> W) x : differentiable f x -> differentiable g x -> 'd (f - g) x = 'd f x \- 'd g x :> (V -> W). -Proof. by move=> /differentiableP df /differentiableP dg; rewrite diff_val. Qed. +Proof. +by move=> /differentiableP df /differentiableP dg; rewrite [LHS]diff_val. +Qed. Lemma differentiableB (f g : V -> W) x : differentiable f x -> differentiable g x -> differentiable (f \- g) x. @@ -920,7 +923,9 @@ Qed. Lemma diffM (f g : V -> R) x : differentiable f x -> differentiable g x -> 'd (f * g) x = f x \*: 'd g x + g x \*: 'd f x :> (V -> R). -Proof. by move=> /differentiableP df /differentiableP dg; rewrite diff_val. Qed. +Proof. +by move=> /differentiableP df /differentiableP dg; rewrite [LHS]diff_val. +Qed. Lemma differentiableM (f g : V -> R) x : differentiable f x -> differentiable g x -> differentiable (f * g) x. @@ -1037,8 +1042,8 @@ Qed. Lemma deriv1E f x : derivable f x 1 -> 'd f x = ( *:%R^~ (f^`() x)) :> (R -> U). Proof. -pose d (h : R) := h *: f^`() x. -move=> df; have lin_scal : linear d by move=> ???; rewrite /d scalerDl scalerA. +pose d (h : R) := h *: (f^`() x)%classic. +move=> df; have lin_scal : linear d by move=> ? ? ?; rewrite /d scalerDl scalerA. pose scallM := GRing.isLinear.Build _ _ _ _ _ lin_scal. pose scalL : {linear _ -> _} := HB.pack d scallM. rewrite -/d -[d]/(scalL : _ -> _). @@ -1046,13 +1051,13 @@ by apply: diff_unique; [apply: scalel_continuous|apply: der1]. Qed. Lemma diff1E f x : - differentiable f x -> 'd f x = (fun h => h *: f^`() x) :> (R -> U). + differentiable f x -> 'd f x = (fun h => h *: f^`()%classic x) :> (R -> U). Proof. pose d (h : R) := h *: 'd f x 1. move=> df; have lin_scal : linear d by move=> ? ? ?; rewrite /d scalerDl scalerA. pose scallM := GRing.isLinear.Build _ _ _ _ _ lin_scal. pose scalL : {linear _ -> _} := HB.pack d scallM. -have -> : (fun h => h *: f^`() x) = scalL by rewrite derive1E'. +have -> : (fun h => h *: f^`()%classic x) = scalL by rewrite derive1E'. apply: diff_unique; first exact: scalel_continuous. apply/eqaddoE; have /diff_locally -> := df; congr (_ + _ + _). by rewrite funeqE => h /=; rewrite -{1}[h]mulr1 linearZ. @@ -1279,7 +1284,7 @@ evar (fg : R -> R); rewrite [X in X @ _](_ : _ = fg) /=; last first. rewrite scalerDr scalerA mulrC -scalerA. by rewrite [_ *: (g x *: _)]scalerA mulrC -scalerA /fg. apply: cvgD; last exact: cvgZr df. -apply: cvg_comp2 (@mul_continuous _ (_, _)) => /=; last exact: dg. +apply: cvg_comp2 (@scale_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 _ _ _).1. @@ -1598,6 +1603,237 @@ have [c cab D] := MVT altb fdrvbl fcont. by exists c => //; rewrite in_itv /= ltW (itvP cab). Qed. +Section Cauchy_MVT. +Context {R : realType}. +Variables (f df g dg : R -> R) (a b c : R). +Hypothesis ab : a < b. +Hypotheses (cf : {within `[a, b], continuous f}) + (cg : {within `[a, b], continuous g}). +Hypotheses (fdf : forall x, x \in `]a, b[%R -> is_derive x 1 f (df x)) + (gdg : forall x, x \in `]a, b[%R -> is_derive x 1 g (dg x)). +Hypotheses (dg0 : forall x, x \in `]a, b[%R -> dg x != 0). + +Lemma differentiable_subr_neq0 : g b - g a != 0. +Proof. +have [r] := MVT ab gdg cg; rewrite in_itv/= => /andP[ar rb] dgg. +by rewrite dgg mulf_neq0 ?dg0 ?in_itv/= ?ar//; rewrite subr_eq0 gt_eqF. +Qed. + +Lemma cauchy_MVT : + exists2 c, c \in `]a, b[%R & df c / dg c = (f b - f a) / (g b - g a). +Proof. +pose h x := f x - ((f b - f a) / (g b - g a)) * g x. +have hder x : x \in `]a, b[%R -> derivable h x 1. + move=> xab; apply: derivableB => /=. + exact: (@ex_derive _ _ _ _ _ _ _ (fdf xab)). + by apply: derivableM => //; exact: (@ex_derive _ _ _ _ _ _ _ (gdg xab)). +have ch : {within `[a, b], continuous h}. + rewrite continuous_subspace_in => x xab. + by apply: cvgB; [exact: cf|apply: cvgM; [exact: cvg_cst|exact: cg]]. +have /(Rolle ab hder ch)[x xab derh] : h a = h b. + rewrite /h; apply/eqP; rewrite subr_eq eq_sym -addrA eq_sym addrC -subr_eq. + rewrite -mulrN -mulrDr -(addrC (g a)) -[X in _ * X]opprB mulrN -mulrA. + by rewrite mulVf ?differentiable_subr_neq0// mulr1 opprB. +pose dh x := df x - (f b - f a) / (g b - g a) * dg x. +have his_der y : y \in `]a, b[%R -> is_derive x 1 h (dh x). + by move=> yab; apply: is_deriveB; [exact: fdf|apply: is_deriveZ; exact: gdg]. +exists x => //. +have := @derive_val _ R _ _ _ _ _ (his_der _ xab). +rewrite (@derive_val _ R _ _ _ _ _ derh) => /esym/eqP. +by rewrite subr_eq add0r => /eqP ->; rewrite -mulrA divff ?mulr1//; exact: dg0. +Qed. + +End Cauchy_MVT. + +Section lhopital. +Context {R : realType}. +Variables (f df g dg : R -> R) (a : R) (U : set R) (Ua : nbhs a U). +Hypotheses (fdf : forall x, x \in U -> is_derive x 1 f (df x)) + (gdg : forall x, x \in U -> is_derive x 1 g (dg x)). +Hypotheses (fa0 : f a = 0) (ga0 : g a = 0) + (cdg : \forall x \near a^', dg x != 0). + +Lemma lhopital_right (l : R) : + df x / dg x @[x --> a^'+] --> l -> f x / g x @[x --> a^'+] --> l. +Proof. +case: cdg => r/= r0 cdg'. +move: Ua; rewrite filter_of_nearI => -[D /= D0 aDU]. +near a^'+ => b. +have abf x : x \in `]a, b[%R -> {within `[a, x], continuous f}. + rewrite in_itv/= => /andP[ax xb]. + apply: derivable_within_continuous => y; rewrite in_itv/= => /andP[ay yx]. + apply: ex_derive. + apply: fdf. + rewrite inE; apply: aDU => /=. + rewrite ler0_norm? subr_le0//. + rewrite opprD opprK addrC ltrBlDr (le_lt_trans yx)// (lt_trans xb)//. + near: b; apply: nbhs_right_lt. + by rewrite ltrDr. +have abg x : x \in `]a, b[%R -> {within `[a, x], continuous g}. + rewrite in_itv/= => /andP[ax xb]. + apply: derivable_within_continuous => y; rewrite in_itv/= => /andP[ay yx]. + apply: ex_derive. + apply: gdg. + rewrite inE; apply: aDU => /=. + rewrite ler0_norm? subr_le0//. + rewrite opprD opprK addrC ltrBlDr (le_lt_trans yx)// (lt_trans xb)//. + near: b; apply: nbhs_right_lt. + by rewrite ltrDr. +have fdf' y : y \in `]a, b[%R -> is_derive y 1 f (df y). + rewrite in_itv/= => /andP[ay yb]; apply: fdf. + rewrite inE; apply: aDU => /=. + rewrite ltr0_norm ?subr_lt0//. + rewrite opprD opprK addrC ltrBlDr (lt_le_trans yb)//. + near: b; apply: nbhs_right_le. + by rewrite ltrDr. +have gdg' y : y \in `]a, b[%R -> is_derive y 1 g (dg y). + rewrite in_itv/= => /andP[ay yb]; apply: gdg. + rewrite inE; apply: aDU => /=. + rewrite ltr0_norm ?subr_lt0//. + rewrite opprD opprK addrC ltrBlDr (lt_le_trans yb)//. + near: b; apply: nbhs_right_le. + by rewrite ltrDr. +have {}dg0 y : y \in `]a, b[%R -> dg y != 0. + rewrite in_itv/= => /andP[ay yb]. + apply: (cdg' y) => /=; last by rewrite gt_eqF. + rewrite ltr0_norm; last by rewrite subr_lt0. + rewrite opprB ltrBlDl (lt_trans yb)//. + near: b; apply: nbhs_right_lt. + by rewrite ltrDl. +move=> fgal. +have L : \forall x \near a^'+, + exists2 c, c \in `]a, x[%R & df c / dg c = f x / g x. + near=> x. + have /andP[ax xb] : a < x < b by exact/andP. + have {}fdf' y : y \in `]a, x[%R -> is_derive y 1 f (df y). + rewrite !in_itv/= => /andP[ay yx]. + by apply: fdf'; rewrite in_itv/= ay/= (lt_trans yx). + have {}gdg' y : y \in `]a, x[%R -> is_derive y 1 g (dg y). + rewrite !in_itv/= => /andP[ay yx]. + by apply: gdg'; rewrite in_itv/= ay/= (lt_trans yx). + have {}dg0 y : y \in `]a, x[%R -> dg y != 0. + rewrite in_itv/= => /andP[ya yx]. + by apply: dg0; rewrite in_itv/= ya/= (lt_trans yx). + have {}axf : {within `[a, x], continuous f}. + rewrite continuous_subspace_in => y; rewrite inE/= in_itv/= => /andP[ay yx]. + by apply: abf; rewrite in_itv/= xb andbT. + have {}axg : {within `[a, x], continuous g}. + rewrite continuous_subspace_in => y; rewrite inE/= in_itv/= => /andP[ay yx]. + by apply: abg; rewrite in_itv/= xb andbT. + have := @cauchy_MVT _ f df g dg _ _ ax axf axg fdf' gdg' dg0. + by rewrite fa0 ga0 2!subr0. +apply/cvgrPdist_le => /= e e0. +move/cvgrPdist_le : fgal. +move=> /(_ _ e0)[r'/= r'0 fagl]. +case: L => d /= d0 L. +near=> t. +have /= := L t. +have atd : `|a - t| < d. + rewrite ltr0_norm; last by rewrite subr_lt0. + rewrite opprB ltrBlDl. + near: t; apply: nbhs_right_lt. + by rewrite ltrDl. +have at_ : a < t by []. +move=> /(_ atd)/(_ at_)[c]; rewrite in_itv/= => /andP[ac ct <-]. +apply: fagl => //=. +rewrite ltr0_norm; last by rewrite subr_lt0. +rewrite opprB ltrBlDl (lt_trans ct)//. +near: t; apply: nbhs_right_lt. +by rewrite ltrDl. +Unshelve. all: by end_near. Qed. + +Lemma lhopital_left (l : R) : + df x / dg x @[x --> a^'-] --> l -> f x / g x @[x --> a^'-] --> l. +Proof. +case: cdg => r/= r0 cdg'. +move: Ua; rewrite filter_of_nearI => -[D /= D0 aDU]. +near a^'- => b. +have baf x : x \in `]b, a[%R -> {within `[x, a], continuous f}. + rewrite in_itv/= => /andP[bx xa]. + apply: derivable_within_continuous => y; rewrite in_itv/= => /andP[xy ya]. + apply: ex_derive. + apply: fdf. + rewrite inE; apply: aDU => /=. + rewrite ger0_norm ?subr_ge0//. + rewrite ltrBlDr -ltrBlDl (lt_le_trans _ xy)// (le_lt_trans _ bx)//. + near: b; apply: nbhs_left_ge. + by rewrite ltrBlDl ltrDr. +have bag x : x \in `]b, a[%R -> {within `[x, a], continuous g}. + rewrite in_itv/= => /andP[bx xa]. + apply: derivable_within_continuous => y; rewrite in_itv/= => /andP[xy ya]. + apply: ex_derive. + apply: gdg. + rewrite inE; apply: aDU => /=. + rewrite ger0_norm ?subr_ge0//. + rewrite ltrBlDr -ltrBlDl (lt_le_trans _ xy)// (lt_trans _ bx)//. + near: b; apply: nbhs_left_gt. + by rewrite ltrBlDl ltrDr. +have fdf' y : y \in `]b, a[%R -> is_derive y 1 f (df y). + rewrite in_itv/= => /andP[by_ ya]; apply: fdf. + rewrite inE. + apply: aDU => /=. + rewrite gtr0_norm ?subr_gt0//. + rewrite ltrBlDl -ltrBlDr (le_lt_trans _ by_)//. + near: b; apply: nbhs_left_ge. + by rewrite ltrBlDr ltrDl. +have gdg' y : y \in `]b, a[%R -> is_derive y 1 g (dg y). + rewrite in_itv/= => /andP[by_ ya]; apply: gdg. + rewrite inE; apply: aDU => /=. + rewrite gtr0_norm ?subr_gt0//. + rewrite ltrBlDl -ltrBlDr (le_lt_trans _ by_)//. + near: b; apply: nbhs_left_ge. + by rewrite ltrBlDr ltrDl. +have {}dg0 y : y \in `]b, a[%R -> dg y != 0. + rewrite in_itv/= => /andP[by_ ya]. + apply: (cdg' y) => /=; last by rewrite lt_eqF. + rewrite gtr0_norm; last by rewrite subr_gt0. + rewrite ltrBlDr -ltrBlDl (lt_trans _ by_)//. + near: b; apply: nbhs_left_gt. + by rewrite ltrBlDl ltrDr. +move=> fgal. +have L : \forall x \near a^'-, + exists2 c, c \in `]x, a[%R & df c / dg c = f x / g x. + near=> x. + have /andP[bx xa] : b < x < a by exact/andP. + have {}fdf' y : y \in `]x, a[%R -> is_derive y 1 f (df y). + rewrite in_itv/= => /andP[xy ya]. + by apply: fdf'; rewrite in_itv/= ya andbT (lt_trans bx). + have {}gdg' y : y \in `]x, a[%R -> is_derive y 1 g (dg y). + rewrite in_itv/= => /andP[xy ya]. + by apply: gdg'; rewrite in_itv/= ya andbT (lt_trans _ xy). + have {}dg0 y : y \in `]x, a[%R -> dg y != 0. + rewrite in_itv/= => /andP[xy ya]. + by apply: dg0; rewrite in_itv/= ya andbT (lt_trans bx). + have {}xaf : {within `[x, a], continuous f}. + rewrite continuous_subspace_in => y; rewrite inE/= in_itv/= => /andP[xy ya]. + by apply: baf; rewrite in_itv/= bx. + have {}xag : {within `[x, a], continuous g}. + rewrite continuous_subspace_in => y; rewrite inE/= in_itv/= => /andP[xy ya]. + by apply: bag; rewrite in_itv/= bx. + have := @cauchy_MVT _ f df g dg _ _ xa xaf xag fdf' gdg' dg0. + by rewrite fa0 ga0 !sub0r divrN mulNr opprK. +apply/cvgrPdist_le => /= e e0. +move/cvgrPdist_le : fgal. +move=> /(_ _ e0)[r'/= r'0 fagl]. +case: L => d /= d0 L. +near=> t. +have /= := L t. +have atd : `|a - t| < d. + rewrite gtr0_norm; last by rewrite subr_gt0. + rewrite ltrBlDr -ltrBlDl. + near: t; apply: nbhs_left_gt. + by rewrite ltrBlDl ltrDr. +have ta : t < a by []. +move=> /(_ atd)/(_ ta)[c]; rewrite in_itv/= => /andP[tc ca <-]. +apply: fagl => //=. +rewrite gtr0_norm; last by rewrite subr_gt0. +rewrite ltrBlDr -ltrBlDl (lt_trans _ tc)//. +near: t; apply: nbhs_left_gt. +by rewrite ltrBlDl ltrDr. +Unshelve. all: by end_near. Qed. + +End lhopital. + Lemma ler0_derive1_nincr (R : realType) (f : R -> R) (a b : R) : (forall x, x \in `]a, b[%R -> derivable f x 1) -> (forall x, x \in `]a, b[%R -> f^`() x <= 0) -> @@ -1635,7 +1871,7 @@ Qed. Lemma derive1_comp (R : realFieldType) (f g : R -> R) x : derivable f x 1 -> derivable g (f x) 1 -> - (g \o f)^`() x = g^`() (f x) * f^`() x. + (g \o f)^`() x = g^`()%classic (f x) * f^`()%classic x. Proof. move=> /derivable1_diffP df /derivable1_diffP dg. rewrite derive1E'; last exact/differentiable_comp. @@ -1647,3 +1883,56 @@ Qed. Lemma trigger_derive (R : realType) (f : R -> R) x x1 y1 : is_derive x (1 : R) f x1 -> x1 = y1 -> is_derive x 1 f y1. Proof. by move=> Hi <-. Qed. + +Section derive_horner. +Variable (R : realFieldType). +Local Open Scope ring_scope. + +Lemma horner0_ext : horner (0 : {poly R}) = 0. +Proof. by apply/funext => y /=; rewrite horner0. Qed. + +Lemma hornerD_ext (p : {poly R}) r : + horner (p * 'X + r%:P) = horner (p * 'X) + horner (r%:P). +Proof. by apply/funext => y /=; rewrite !(hornerE,fctE). Qed. + +Lemma horner_scale_ext (p : {poly R}) : + horner (p * 'X) = (fun x => p.[x] * x)%R. +Proof. by apply/funext => y; rewrite !hornerE. Qed. + +Lemma hornerC_ext (r : R) : horner r%:P = cst r. +Proof. by apply/funext => y /=; rewrite !hornerE. Qed. + +Lemma derivable_horner (p : {poly R}) x : derivable (horner p) x 1. +Proof. +elim/poly_ind: p => [|p r ih]; first by rewrite horner0_ext. +rewrite hornerD_ext; apply: derivableD. +- rewrite horner_scale_ext/=. + by apply: derivableM; [exact:ih|exact:derivable_id]. +- by rewrite hornerC_ext; exact: derivable_cst. +Qed. + +Lemma derivE (p : {poly R}) : horner (p^`()) = (horner p)^`()%classic. +Proof. +apply/funext => x; elim/poly_ind: p => [|p r ih]. + by rewrite deriv0 hornerC horner0_ext derive1_cst. +rewrite derivD hornerD hornerD_ext. +rewrite derive1E deriveD//; [|exact: derivable_horner..]. +rewrite -!derive1E hornerC_ext derive1_cst addr0. +rewrite horner_scale_ext derive1E deriveM//; last exact: derivable_horner. +rewrite derive_id -derive1E -ih derivC horner0 addr0 derivM hornerD !hornerE. +by rewrite derivX hornerE mulr1 addrC mulrC scaler1. +Qed. + +Global Instance is_derive_poly (p : {poly R}) (x : R) : + is_derive x (1:R) (horner p) p^`().[x]. +Proof. +by apply: DeriveDef; [exact: derivable_horner|rewrite derivE derive1E]. +Qed. + +Lemma continuous_horner (p : {poly R}) : continuous (horner p). +Proof. +move=> /= x; apply/differentiable_continuous. +exact/derivable1_diffP/derivable_horner. +Qed. + +End derive_horner. diff --git a/theories/esum.v b/theories/esum.v index 57959228b9..8696387ac1 100644 --- a/theories/esum.v +++ b/theories/esum.v @@ -300,7 +300,8 @@ Lemma lee_sum_fset_lim (R : realType) (f : (\bar R)^nat) (F : {fset nat}) \sum_(i <- F | P i) f i <= \sum_(i f0; pose n := (\max_(k <- F) k).+1. -rewrite (le_trans (lee_sum_fset_nat F n _ _ _))//; last exact: nneseries_lim_ge. +rewrite (le_trans (lee_sum_fset_nat F n _ _ _))//; last first. + by apply: nneseries_lim_ge => i _; exact: f0. move=> k /= kF; rewrite /n big_seq_fsetE/=. by rewrite -[k]/(val [`kF]%fset) ltnS leq_bigmax. Qed. @@ -311,7 +312,7 @@ Lemma nneseries_esum (R : realType) (a : nat -> \bar R) (P : pred nat) : \sum_(i a0; apply/eqP; rewrite eq_le; apply/andP; split. - apply: (lime_le (is_cvg_nneseries_cond a0)); apply: nearW => n. + apply: (lime_le (is_cvg_nneseries_cond (fun n _ => a0 n))); apply: nearW => n. apply: ereal_sup_ubound; exists [set` [fset val i | i in 'I_n & P i]%fset]. split; first exact: finite_fset. by move=> /= k /imfsetP[/= i]; rewrite inE => + ->. @@ -536,7 +537,7 @@ Lemma summable_cvg (P : pred nat) (f : (\bar R)^nat) : cvg ((fun n => \sum_(0 <= k < n | P k) fine (f k))%R @ \oo). Proof. move=> f0 Pf; apply: nondecreasing_is_cvgn. - by apply: nondecreasing_series => n Pn; exact/fine_ge0/f0. + by apply: nondecreasing_series => n _ Pn; exact/fine_ge0/f0. exists (fine (\sum_(i x /= [n _ <-]. rewrite summable_fine_sum// -lee_fin fineK//; last first. by apply/sum_fin_numP => i ni Pi; rewrite fin_num_abs (summable_pinfty Pf). @@ -600,10 +601,8 @@ Unshelve. all: by end_near. Qed. Lemma summable_eseries_esum (f : nat -> \bar R) (P : pred nat) : summable P f -> \sum_(i Pfoo; rewrite -nneseries_esum; last first. - by move=> n Pn; rewrite /maxe; case: ifPn => //; rewrite -leNgt. -rewrite -nneseries_esum ?[LHS]summable_eseries//. -by move=> n Pn; rewrite /maxe; case: ifPn => //; rewrite leNgt. +move=> Pfoo. +by rewrite -nneseries_esum// -nneseries_esum// [LHS]summable_eseries. Qed. End summable_nat. @@ -620,7 +619,7 @@ Let ge0_esum_posneg D f : (forall x, D x -> 0 <= f x) -> Proof. move=> Sa; rewrite /esum_posneg [X in _ - X](_ : _ = 0) ?sube0; last first. by rewrite esum1// => x Sx; rewrite -[LHS]/(f^\- x) (ge0_funenegE Sa)// inE. -by apply: eq_esum => t St; apply/max_idPl; exact: Sa. +apply: eq_esum => t St; rewrite funeposE; apply/max_idPl; exact: Sa. Qed. Lemma esumB D f g : summable D f -> summable D g -> @@ -629,11 +628,11 @@ Lemma esumB D f g : summable D f -> summable D g -> \esum_(i in D) f i - \esum_(i in D) g i. Proof. move=> Df Dg f0 g0. -have /eqP : esum D (f \- g)^\+ + esum_posneg D g = esum D (f \- g)^\- + esum_posneg D f. - rewrite !ge0_esum_posneg// -!esumD//; last 2 first. - by move=> t Dt; rewrite le_max lexx orbT. - by move=> t Dt; rewrite le_max lexx orbT. - apply eq_esum => i Di; have [fg|fg] := leP 0 (f i - g i). +have /eqP : esum D (f \- g)^\+ + esum_posneg D g = + esum D (f \- g)^\- + esum_posneg D f. + rewrite !ge0_esum_posneg// -!esumD//. + apply eq_esum => i Di; rewrite funeposE funenegE. + have [fg|fg] := leP 0 (f i - g i). rewrite max_r 1?leeNl ?oppe0// add0e subeK//. by rewrite fin_num_abs (summable_pinfty Dg). rewrite add0e max_l; last by rewrite leeNr oppe0 ltW. @@ -651,7 +650,8 @@ rewrite [X in _ == X -> _]addeC -sube_eq; last 2 first. rewrite (@eq_esum _ _ _ _ (abse \o f))// -?summableE// => i Di. by rewrite /= gee0_abs// f0. rewrite -addeA addeCA eq_sym [X in _ == X -> _]addeC -sube_eq; last 2 first. - - rewrite ge0_esum_posneg// (@eq_esum _ _ _ _ (abse \o f))// -?summableE// => i Di. + - rewrite ge0_esum_posneg//. + rewrite (@eq_esum _ _ _ _ (abse \o f))// -?summableE// => i Di. by rewrite /= gee0_abs// f0. - rewrite fin_num_adde_defl// ge0_esum_posneg//. rewrite (@eq_esum _ _ _ _ (abse \o g))// -?summableE// => i Di. diff --git a/theories/kernel.v b/theories/kernel.v index 31d8ba8185..872dab1657 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -823,7 +823,7 @@ move=> U mU tU mUU; rewrite [X in _ --> X](_ : _ = apply: eq_integral => V _. by apply/esym/cvg_lim => //; exact/measure_semi_sigma_additive. apply/cvg_closeP; split. - by apply: is_cvg_nneseries => n _; exact: integral_ge0. + by apply: is_cvg_nneseries => n _ _; exact: integral_ge0. rewrite closeE// integral_nneseries// => n. exact: measurableT_comp (measurable_kernel k _ (mU n)) _. Qed. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 3ac62afdf6..8a966ebcba 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -1966,7 +1966,7 @@ rewrite [X in measurable_fun _ X](_ : _ = rewrite [X in measurable_fun _ X](_ : _ = (fun x => limn_esup (fun n => \sum_(0 <= i < n | P i) (h i) \_ D x))); last first. apply/funext=> x; rewrite is_cvg_limn_esupE//. - apply: is_cvg_nneseries_cond => n Pn; rewrite patchE. + apply: is_cvg_nneseries_cond => n _ Pn; rewrite patchE. by case: ifPn => // xD; rewrite h0//; exact/set_mem. apply: measurable_fun_limn_esup => k. under eq_fun do rewrite big_mkcond. @@ -2562,12 +2562,12 @@ Lemma integralN D (f : T -> \bar R) : Proof. have [f_fin _|] := boolP (\int[mu]_(x in D) f^\- x \is a fin_num). rewrite integralE// [in RHS]integralE// fin_num_oppeD ?fin_numN// oppeK addeC. - by rewrite funenegN. + by rewrite funenegN funeposN. rewrite fin_numE negb_and 2!negbK => /orP[nfoo|/eqP nfoo]. exfalso; move/negP : nfoo; apply; rewrite -leeNy_eq; apply/negP. by rewrite -ltNge (lt_le_trans _ (integral_ge0 _ _)). rewrite nfoo adde_defEninfty -leye_eq -ltNge ltey_eq => /orP[f_fin|/eqP pfoo]. - rewrite integralE [in RHS]integralE nfoo [in RHS]addeC/= funenegN. + rewrite integralE [in RHS]integralE funeposN nfoo [in RHS]addeC/= funenegN. by rewrite addye// eqe_oppLR/= (andP (eqbLR (fin_numE _) f_fin)).2. by rewrite integralE// [in RHS]integralE// funeposN funenegN nfoo pfoo. Qed. @@ -2926,7 +2926,7 @@ apply/eqP; rewrite eq_le; apply/andP; split; last first. by apply: leeDl; exact: integral_ge0. rewrite ge0_integralE//=; apply: ub_ereal_sup => /= _ [g /= gf] <-. rewrite -integralT_nnsfun (integral_measure_series_nnsfun _ mD). -apply: lee_nneseries => n _. +apply: lee_nneseries => [n _ _|n _]. by apply: integral_ge0 => // x _; rewrite lee_fin. rewrite [leRHS]integral_mkcond; apply: ge0_le_integral => //. - by move=> x _; rewrite lee_fin. @@ -3191,9 +3191,9 @@ move=> /integrableP[mf]; apply: le_lt_trans; apply: ge0_le_integral => //. - exact: measurable_funeneg. - exact: measurableT_comp. - move=> x Dx; have [fx0|/ltW fx0] := leP (f x) 0. - rewrite lee0_abs// /funeneg. + rewrite lee0_abs// funenegE. by move: fx0; rewrite -{1}oppe0 -leeNr => /max_idPl ->. - rewrite gee0_abs// /funeneg. + rewrite gee0_abs// funenegE. by move: (fx0); rewrite -{1}oppe0 -leeNl => /max_idPr ->. Qed. @@ -3204,9 +3204,9 @@ move=> /integrableP[mf]; apply: le_lt_trans; apply: ge0_le_integral => //. - exact: measurable_funepos. - exact: measurableT_comp. - move=> x Dx; have [fx0|/ltW fx0] := leP (f x) 0. - rewrite lee0_abs// /funepos. + rewrite lee0_abs// funeposE. by move: (fx0) => /max_idPr ->; rewrite -leeNr oppe0. - by rewrite gee0_abs// /funepos; move: (fx0) => /max_idPl ->. + by rewrite gee0_abs// funeposE; move: (fx0) => /max_idPl ->. Qed. Lemma integrable_neg_fin_num f : @@ -3586,25 +3586,24 @@ suff: \int[mu]_(x in D) ((g1 \+ g2)^\+ x) + \int[mu]_(x in D) (g1^\- x) + apply: lte_add_pinfty; last exact: integral_funeneg_lt_pinfty. apply: lte_add_pinfty; last exact: integral_funeneg_lt_pinfty. exact: integral_funepos_lt_pinfty (integrableD _ _ _). - rewrite adde_ge0//; last exact: integral_ge0. - by rewrite adde_ge0// integral_ge0. - - by rewrite fin_num_adde_defr. - rewrite -(addeA (\int[mu]_(x in D) (g1 \+ g2)^\+ x)). - rewrite (addeC (\int[mu]_(x in D) (g1 \+ g2)^\+ x)) -[eqbLHS]addeA. - rewrite (addeC (\int[mu]_(x in D) g1^\- x + \int[mu]_(x in D) g2^\- x)). - rewrite eq_sym -(sube_eq g12pos) ?fin_num_adde_defl// => /eqP <-. - rewrite fin_num_oppeD; last first. + apply: adde_ge0; last exact: integral_ge0. + by apply: adde_ge0; apply: integral_ge0. + - exact/fin_num_adde_defr/g12pos. + rewrite -[X in X - _ == _]addeA [X in X - _ == _]addeC -[eqbLHS]addeA. + rewrite [eqbLHS]addeC eq_sym. + rewrite -(sube_eq g12pos) ?fin_num_adde_defl// => /eqP g12E. + rewrite -{}[LHS]g12E fin_num_oppeD; last first. rewrite ge0_fin_numE; first exact: integral_funeneg_lt_pinfty if2. exact: integral_ge0. by rewrite addeACA (integralE _ _ g1) (integralE _ _ g2). have : (g1 \+ g2)^\+ \+ g1^\- \+ g2^\- = (g1 \+ g2)^\- \+ g1^\+ \+ g2^\+. rewrite funeqE => x. apply/eqP; rewrite -2!addeA [in eqbRHS]addeC -sube_eq; last 2 first. - by rewrite /funepos /funeneg -!fine_max. - by rewrite /funepos /funeneg -!fine_max. + by rewrite funeposE !funenegE -!fine_max. + by rewrite !funeposE funenegE -!fine_max. rewrite addeAC eq_sym -sube_eq; last 2 first. - by rewrite /funepos /funeneg -!fine_max. - by rewrite /funepos /funeneg -!fine_max. + by rewrite !funeposE -!fine_max. + by rewrite funeposE !funenegE -!fine_max. apply/eqP. rewrite -[LHS]/((g1^\+ \+ g2^\+ \- (g1^\- \+ g2^\-)) x) -funeD_posD. by rewrite -[RHS]/((_ \- _) x) -funeD_Dpos. @@ -3619,8 +3618,8 @@ rewrite (ge0_integralD mu mD); last 4 first. - by []. - exact/measurable_funepos/emeasurable_funD. - by []. - - exact/measurable_funepos/measurableT_comp. -move=> ->. + - exact/measurable_funeneg. +move=> g12E; rewrite {}[LHS]g12E. rewrite (ge0_integralD mu mD); last 4 first. - by move=> x _; exact: adde_ge0. - apply: emeasurable_funD; last exact: measurable_funepos. @@ -3683,6 +3682,18 @@ move: foo; rewrite integralE/= -fin_num_abs fin_numB => /andP[fpoo fnoo]. by rewrite lte_add_pinfty// ltey_eq ?fpoo ?fnoo. Qed. +Lemma integral_fin_num_abs d (T : measurableType d) (R : realType) + (mu : {measure set T -> \bar R}) (D : set T) (f : T -> R) : + measurable D -> measurable_fun D f -> + (\int[mu]_(x in D) `|(f x)%:E| < +oo)%E = + ((\int[mu]_(x in D) (f x)%:E)%E \is a fin_num). +Proof. +move=> mD mf; rewrite fin_num_abs; case H : LHS; apply/esym. +- by move: H => /abse_integralP ->//; exact/measurable_EFinP. +- apply: contraFF H => /abse_integralP; apply => //. + exact/measurable_EFinP. +Qed. + Section integral_patch. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) @@ -4111,11 +4122,11 @@ Local Open Scope ereal_scope. Lemma integral_pushforward : \int[pushforward mu mphi]_y f y = \int[mu]_x (f \o phi) x. Proof. -transitivity (\int[mu]_y ((f^\+ \o phi) \- (f^\- \o phi)) y); last first. - by apply: eq_integral => x _; rewrite [in RHS](funeposneg (f \o phi)). -rewrite integralB//; [|exact: integrable_funepos|exact: integrable_funeneg]. +rewrite integralE. +under [X in X - _]eq_integral do rewrite funepos_comp. +under [X in _ - X]eq_integral do rewrite funeneg_comp. rewrite -[X in _ = X - _]ge0_integral_pushforward//; last first. - exact: measurable_funepos. + exact/measurable_funepos. rewrite -[X in _ = _ - X]ge0_integral_pushforward//; last first. exact: measurable_funeneg. rewrite -integralB//=; last first. @@ -4323,16 +4334,15 @@ transitivity ((\sum_(i //. + apply: measurable_funeneg. by case/integrableP : fi. rewrite [X in X - _]nneseries_esum; last by move=> n _; exact: integral_ge0. rewrite [X in _ - X]nneseries_esum; last by move=> n _; exact: integral_ge0. rewrite set_true -esumB//=; last 4 first. - apply: integrable_summable => //; apply: integrable_funepos => //. exact: bigcup_measurable. - - apply: integrable_summable => //; apply: integrable_funepos => //. + - apply: integrable_summable => //; apply: integrable_funeneg => //. exact: bigcup_measurable. - - exact: integrableN. - by move=> n _; exact: integral_ge0. - by move=> n _; exact: integral_ge0. rewrite summable_eseries; last first. @@ -4642,6 +4652,32 @@ Qed. Lemma Rintegral_set0 f : \int[mu]_(x in set0) f x = 0. Proof. by rewrite /Rintegral integral_set0. Qed. +Lemma Rintegral_cst D : d.-measurable D -> + forall r, \int[mu]_(x in D) (cst r) x = r * fine (mu D). +Proof. +move=> mD r; rewrite /Rintegral/= integral_cst//. +have := leey (mu D); rewrite le_eqVlt => /predU1P[->/=|muy]; last first. + by rewrite fineM// ge0_fin_numE. +rewrite mulr_infty/=; have [_|r0|r0] := sgrP r. +- by rewrite mul0e/= mulr0. +- by rewrite mul1e/= mulr0. +- by rewrite mulN1e/= mulr0. +Qed. + +Lemma le_Rintegral D f1 f2 : measurable D -> + mu.-integrable D (EFin \o f1) -> + mu.-integrable D (EFin \o f2) -> + (forall x, D x -> f1 x <= f2 x) -> + \int[mu]_(x in D) f1 x <= \int[mu]_(x in D) f2 x. +Proof. +move=> mD mf1 mf2 f12; rewrite /Rintegral fine_le//. +- rewrite -integral_fin_num_abs//; first by case/integrableP : mf1. + by apply/measurable_EFinP; case/integrableP : mf1. +- rewrite -integral_fin_num_abs//; first by case/integrableP : mf2. + by apply/measurable_EFinP; case/integrableP : mf2. +- by apply/le_integral => // x xD; rewrite lee_fin f12//; exact/set_mem. +Qed. + End Rintegral. Section ae_ge0_le_integral. @@ -4763,24 +4799,6 @@ End integral_ae_eq. (** Product measure *) -Section measurable_section. -Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). -Implicit Types (A : set (T1 * T2)). - -Lemma measurable_xsection A x : measurable A -> measurable (xsection A x). -Proof. -move=> mA; rewrite (xsection_indic R) -(setTI (_ @^-1` _)). -exact: measurableT_comp. -Qed. - -Lemma measurable_ysection A y : measurable A -> measurable (ysection A y). -Proof. -move=> mA; rewrite (ysection_indic R) -(setTI (_ @^-1` _)). -exact: measurableT_comp. -Qed. - -End measurable_section. - Section ndseq_closed_B. Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). Implicit Types A : set (T1 * T2). @@ -5257,6 +5275,7 @@ have mfn : mu.-integrable E (fun z => `|f^\- z - (n_ n z)%:E|). apply/integrable_abse/integrableB => //; first exact: integrable_funeneg. exact: intn. rewrite -[x in (_ <= `|x|)%R]fineD // -integralD //. +move: finfn finfp => _ _. rewrite !ger0_norm ?fine_ge0 ?integral_ge0 ?fine_le//. - by apply: integral_fune_fin_num => //; exact/integrable_abse/mfpn. - by apply: integral_fune_fin_num => //; exact: integrableD. @@ -5360,8 +5379,9 @@ exists h; split => //; rewrite [eps%:num]splitr; apply: le_lt_trans. - apply: (measurable_funS mE) => //; do 2 apply: measurableT_comp => //. exact: measurable_funB. - by move=> z _; rewrite adde_ge0. - - apply: measurableT_comp => //; apply: measurable_funD => //; - apply: (measurable_funS mE) => //; (apply: measurableT_comp => //); + - apply: measurableT_comp => //; apply: measurable_funD; + apply: (measurable_funS mE (@subset_refl _ E)); + (apply: measurableT_comp => //); exact: measurable_funB. - move=> x _; rewrite -(subrK (g x) (f x)) -(addrA (_ + _)%R) lee_fin. by rewrite ler_normD. @@ -5536,15 +5556,16 @@ transitivity (\sum_(k \in range f) rewrite indic_fubini_tonelli1// -ge0_integralZl//; last by rewrite lee_fin. - exact: indic_measurable_fun_fubini_tonelli_F. - by move=> /= x _; exact: indic_fubini_tonelli_F_ge0. -rewrite -ge0_integral_fsum //; last 2 first. +rewrite -ge0_integral_fsum; last by []. + - apply: eq_integral => x _; rewrite sfun_fubini_tonelli_FE. + by under eq_fsbigr do rewrite indic_fubini_tonelli_FE//. + - by []. - by move=> r; apply/measurable_funeM/indic_measurable_fun_fubini_tonelli_F. - - move=> r x _; rewrite /fubini_F. - have [r0|r0] := leP 0%R r. - by rewrite mule_ge0//; exact: indic_fubini_tonelli_F_ge0. - rewrite integral0_eq ?mule0// => y _. - by rewrite preimage_nnfun0//= indicE in_set0. -apply: eq_integral => x _; rewrite sfun_fubini_tonelli_FE. -by under eq_fsbigr do rewrite indic_fubini_tonelli_FE//. +move=> r x _; rewrite /fubini_F. +have [r0|r0] := leP 0%R r. + by rewrite mule_ge0//; exact: indic_fubini_tonelli_F_ge0. +rewrite integral0_eq ?mule0// => y _. +by rewrite preimage_nnfun0//= indicE in_set0. Qed. Lemma sfun_fubini_tonelli2 : \int[m1 \x^ m2]_z (f z)%:E = \int[m2]_y G y. @@ -5563,15 +5584,16 @@ transitivity (\sum_(k \in range f) rewrite indic_fubini_tonelli2// -ge0_integralZl//; last by rewrite lee_fin. - exact: indic_measurable_fun_fubini_tonelli_G. - by move=> /= x _; exact: indic_fubini_tonelli_G_ge0. -rewrite -ge0_integral_fsum //; last 2 first. +rewrite -ge0_integral_fsum; last by []. + - apply: eq_integral => x _; rewrite sfun_fubini_tonelli_GE. + by under eq_fsbigr do rewrite indic_fubini_tonelli_GE//. + - by []. - by move=> r; apply/measurable_funeM/indic_measurable_fun_fubini_tonelli_G. - - move=> r y _; rewrite /fubini_G. - have [r0|r0] := leP 0%R r. - by rewrite mule_ge0//; exact: indic_fubini_tonelli_G_ge0. - rewrite integral0_eq ?mule0// => x _. - by rewrite preimage_nnfun0//= indicE in_set0. -apply: eq_integral => x _; rewrite sfun_fubini_tonelli_GE. -by under eq_fsbigr do rewrite indic_fubini_tonelli_GE//. +move=> r y _; rewrite /fubini_G. +have [r0|r0] := leP 0%R r. + by rewrite mule_ge0//; exact: indic_fubini_tonelli_G_ge0. +rewrite integral0_eq ?mule0// => x _. +by rewrite preimage_nnfun0//= indicE in_set0. Qed. Lemma sfun_fubini_tonelli : @@ -5778,7 +5800,12 @@ Let F := fubini_F m2 f. Let Fplus x := \int[m2]_y f^\+ (x, y). Let Fminus x := \int[m2]_y f^\- (x, y). -Let FE : F = Fplus \- Fminus. Proof. apply/funext=> x; exact: integralE. Qed. +Let FE : F = Fplus \- Fminus. +Proof. +apply/funext=> x; rewrite [LHS]integralE. +under eq_integral do rewrite funepos_comp/=. +by under [X in _ - X = _]eq_integral do rewrite funeneg_comp/=. +Qed. Let measurable_Fplus : measurable_fun setT Fplus. Proof. @@ -5799,15 +5826,18 @@ Qed. Let integrable_Fplus : m1.-integrable setT Fplus. Proof. apply/integrableP; split=> //. -apply: le_lt_trans (fubini1a.1 imf); apply: ge0_le_integral => //. -- exact: measurableT_comp. +apply: le_lt_trans (fubini1a.1 imf); apply: ge0_le_integral. +- by []. +- by []. +- by apply: measurableT_comp; last apply: measurable_Fplus. - by move=> x _; exact: integral_ge0. +- exact: measurable_fun1. - move=> x _; apply: le_trans. - apply: le_abse_integral => //; apply: measurable_funepos => //. - exact: measurableT_comp. + apply: le_abse_integral => //; apply: measurableT_comp => //. + exact: measurable_funepos. apply: ge0_le_integral => //. - apply: measurableT_comp => //. - by apply: measurable_funepos => //; exact: measurableT_comp. + by apply: measurableT_comp => //; exact: measurable_funepos. - by apply: measurableT_comp => //; exact/measurableT_comp. - by move=> y _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse leeDl. Qed. @@ -5819,11 +5849,11 @@ apply: le_lt_trans (fubini1a.1 imf); apply: ge0_le_integral => //. - exact: measurableT_comp. - by move=> *; exact: integral_ge0. - move=> x _; apply: le_trans. - apply: le_abse_integral => //; apply: measurable_funeneg => //. - exact: measurableT_comp. + apply: le_abse_integral => //; apply: measurableT_comp => //. + exact: measurable_funeneg. apply: ge0_le_integral => //. - + apply: measurableT_comp => //; apply: measurable_funeneg => //. - exact: measurableT_comp. + + apply: measurableT_comp => //; apply: measurableT_comp => //. + exact: measurable_funeneg. + by apply: measurableT_comp => //; exact: measurableT_comp. + by move=> y _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse leeDr. Qed. @@ -5836,7 +5866,12 @@ Let G := fubini_G m1 f. Let Gplus y := \int[m1]_x f^\+ (x, y). Let Gminus y := \int[m1]_x f^\- (x, y). -Let GE : G = Gplus \- Gminus. Proof. apply/funext=> x; exact: integralE. Qed. +Let GE : G = Gplus \- Gminus. +Proof. +apply/funext=> x; rewrite [LHS]integralE. +under eq_integral do rewrite funepos_comp/=. +by under [X in _ - X = _]eq_integral do rewrite funeneg_comp/=. +Qed. Let measurable_Gplus : measurable_fun setT Gplus. Proof. @@ -5854,15 +5889,18 @@ Proof. by rewrite GE; exact: emeasurable_funB. Qed. Let integrable_Gplus : m2.-integrable setT Gplus. Proof. apply/integrableP; split=> //. -apply: le_lt_trans (fubini1b.1 imf); apply: ge0_le_integral => //. -- exact: measurableT_comp. +apply: le_lt_trans (fubini1b.1 imf). apply: ge0_le_integral. +- by []. +- by []. +- by apply: measurableT_comp; last apply: measurable_Gplus. - by move=> *; exact: integral_ge0. +- exact: measurable_fun2. - move=> y _; apply: le_trans. - apply: le_abse_integral => //; apply: measurable_funepos => //. - exact: measurableT_comp. + apply: le_abse_integral => //; apply: measurableT_comp => //. + exact: measurable_funepos. apply: ge0_le_integral => //. - apply: measurableT_comp => //. - by apply: measurable_funepos => //; exact: measurableT_comp. + by apply: measurableT_comp => //; exact: measurable_funepos. - by apply: measurableT_comp => //; exact: measurableT_comp. - by move=> x _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse leeDl. Qed. @@ -5870,15 +5908,18 @@ Qed. Let integrable_Gminus : m2.-integrable setT Gminus. Proof. apply/integrableP; split=> //. -apply: le_lt_trans (fubini1b.1 imf); apply: ge0_le_integral => //. +apply: le_lt_trans (fubini1b.1 imf); apply: ge0_le_integral. +- by []. +- by []. - exact: measurableT_comp. - by move=> *; exact: integral_ge0. +- exact: measurable_fun2. - move=> y _; apply: le_trans. - apply: le_abse_integral => //; apply: measurable_funeneg => //. - exact: measurableT_comp. + apply: le_abse_integral => //; apply: measurableT_comp => //. + exact: measurable_funeneg. apply: ge0_le_integral => //. + apply: measurableT_comp => //. - by apply: measurable_funeneg => //; exact: measurableT_comp. + by apply: measurableT_comp => //; exact: measurable_funeneg. + by apply: measurableT_comp => //; exact: measurableT_comp. + by move=> x _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse leeDr. Qed. @@ -5973,7 +6014,7 @@ Qed. Lemma lebesgue_differentiation_continuous (f : R -> rT^o) (A : set R) (x : R) : open A -> mu.-integrable A (EFin \o f) -> {for x, continuous f} -> A x -> - (fun r => 1 / (r *+ 2) * \int[mu]_(z in ball x r) f z) @ 0^'+ --> + (fun r => (r *+ 2)^-1 * \int[mu]_(z in ball x r) f z) @ 0^'+ --> (f x : R^o). Proof. have ball_itvr r : 0 < r -> `[x - r, x + r] `\` ball x r = [set x + r; x - r]. @@ -6004,10 +6045,10 @@ have -> : \int[mu]_(z in ball x r) f z = \int[mu]_(z in `[x - r, x + r]) f z. - by apply/measurableU; exact: measurable_set1. - exact: (integrableS mA). - by rewrite measureU0//; exact: lebesgue_measure_set1. -have r20 : 0 <= 1 / (r *+ 2) by rewrite ?divr_ge0 // mulrn_wge0. -have -> : f x = 1 / (r *+ 2) * \int[mu]_(z in `[x - r, x + r]) cst (f x) z. - rewrite /Rintegral /= integral_cst /= ?ritv // mulrC mul1r. - by rewrite -mulrA divff ?mulr1//; apply: lt0r_neq0; rewrite mulrn_wgt0. +have r20 : 0 <= (r *+ 2)^-1 by rewrite invr_ge0 mulrn_wge0. +have -> : f x = (r *+ 2)^-1 * \int[mu]_(z in `[x - r, x + r]) cst (f x) z. + rewrite Rintegral_cst// ritv//= mulrA mulrAC mulVf ?mul1r//. + by apply: lt0r_neq0; rewrite mulrn_wgt0. have intRf : mu.-integrable `[x - r, x + r] (EFin \o f). exact: (@integrableS _ _ _ mu _ _ _ _ _ xrA intf). rewrite /= -mulrBr -fineB; first last. @@ -6021,7 +6062,7 @@ have int_fx : mu.-integrable `[x - r, x + r] (fun z => (f z - f x)%:E). under [fun z => (f z - _)%:E]eq_fun => ? do rewrite EFinB. rewrite integrableB// continuous_compact_integrable// => ?. exact: cvg_cst. -rewrite normrM [ `|_/_| ]ger0_norm // -fine_abse //; first last. +rewrite normrM ger0_norm // -fine_abse //; first last. by rewrite integral_fune_fin_num. suff : (\int[mu]_(z in `[(x - r)%R, (x + r)%R]) `|f z - f x|%:E <= (r *+ 2 * eps)%:E)%E. @@ -6031,7 +6072,7 @@ suff : (\int[mu]_(z in `[(x - r)%R, (x + r)%R]) `|f z - f x|%:E <= - by rewrite abse_fin_num integral_fune_fin_num. - by rewrite integral_fune_fin_num// integrable_abse. - by case/integrableP : int_fx. - rewrite div1r ler_pdivrMl ?mulrn_wgt0 // -[_ * _]/(fine (_%:E)). + rewrite ler_pdivrMl ?mulrn_wgt0 // -[_ * _]/(fine (_%:E)). by rewrite fine_le// integral_fune_fin_num// integrable_abse. apply: le_trans. - apply: (@integral_le_bound _ _ _ _ _ (fun z => (f z - f x)%:E) eps%:E) => //. @@ -6304,12 +6345,13 @@ have ? : k <= \int[mu]_(z in ball y (r + d)) `|(f z)%:E|. by apply: measurable_funTS; do 2 apply: measurableT_comp => //. have afxrdi : a%:E < (fine (mu (ball x (r + d))))^-1%:E * \int[mu]_(z in ball y (r + d)) `|(f z)%:E|. - by rewrite (lt_le_trans axrdk)// lee_wpmul2l// lee_fin invr_ge0// fine_ge0. + apply/(lt_le_trans axrdk)/lee_wpmul2l => //. + by rewrite lee_fin invr_ge0 fine_ge0. have /lt_le_trans : a%:E < iavg f (ball y (r + d)). apply: (lt_le_trans afxrdi); rewrite /iavg. do 2 (rewrite lebesgue_measure_ball; last by rewrite addr_ge0// ltW). - rewrite lee_wpmul2l// lee_fin invr_ge0// fine_ge0//= lee_fin pmulrn_rge0//. - by rewrite addr_gt0. + rewrite lee_wpmul2l ?lexx// lee_fin invr_ge0// fine_ge0//= lee_fin. + by rewrite pmulrn_rge0// addr_gt0. apply; apply: ereal_sup_ubound => /=. by exists (r + d)%R => //; rewrite in_itv/= andbT addr_gt0. Unshelve. all: by end_near. Qed. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 7491d4928d..108042b887 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1180,9 +1180,10 @@ Proof. move=> mf. exact: (@measurable_comp _ _ _ _ _ _ setT (fun x : R => x ^+ n) _ f). Qed. +#[deprecated(since="mathcomp-analysis 1.4.0", note="use `measurable_funX` instead")] +Notation measurable_fun_pow := measurable_funX (only parsing). -Lemma measurable_powR (R : realType) p : - measurable_fun [set: R] (@powR R ^~ p). +Lemma measurable_powR (R : realType) p : measurable_fun [set: R] (@powR R ^~ p). Proof. apply: measurable_fun_if => //. - apply: (measurable_fun_bool true). @@ -1194,14 +1195,20 @@ apply: measurable_fun_if => //. Qed. #[global] Hint Extern 0 (measurable_fun _ (@powR _ ^~ _)) => solve [apply: measurable_powR] : core. -#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_powR` instead")] -Notation measurable_fun_power_pos := measurable_powR (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.4", note="use `measurable_powR` instead")] -Notation measurable_power_pos := measurable_powR (only parsing). + +Lemma measurable_powRr {R : realType} b : measurable_fun [set: R] (@powR R b). +Proof. +rewrite /powR; apply: measurable_fun_if => //. +- rewrite preimage_true setTI/=. + case: (b == 0); rewrite ?set_true ?set_false. + + by apply: measurableT_comp => //; exact: measurable_fun_eqr. + + exact: measurable_fun_set0. +- rewrite preimage_false setTI; apply: measurableT_comp => //. + exact: mulrr_measurable. +Qed. + #[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_maxr` instead")] Notation measurable_fun_max := measurable_maxr (only parsing). -#[deprecated(since="mathcomp-analysis 1.4.0", note="use `measurable_funX` instead")] -Notation measurable_fun_pow := measurable_funX (only parsing). Module NGenCInfty. Section ngencinfty. @@ -1509,11 +1516,14 @@ Qed. Lemma measurable_funepos D (f : T -> \bar R) : measurable_fun D f -> measurable_fun D f^\+. -Proof. by move=> mf; exact: measurable_maxe. Qed. +Proof. by move=> mf; rewrite unlock; exact: measurable_maxe. Qed. Lemma measurable_funeneg D (f : T -> \bar R) : measurable_fun D f -> measurable_fun D f^\-. -Proof. by move=> mf; apply: measurable_maxe => //; exact: measurableT_comp. Qed. +Proof. +move=> mf; rewrite unlock; apply: measurable_maxe => //. +exact: measurableT_comp. +Qed. Lemma measurable_mine D (f g : T -> \bar R) : measurable_fun D f -> measurable_fun D g -> @@ -2910,7 +2920,7 @@ have [N F5e] : exists N, \sum_(N <= n //; first by move=> i _; exact: esum_ge0. + apply: lee_nneseries => //; first by move=> i *; exact: esum_ge0. move=> n Nn; rewrite measure_bigcup//=. - by rewrite nneseries_esum// set_mem_set. - by move=> i _; exact: measurable_closure. diff --git a/theories/measure.v b/theories/measure.v index 691b79f9ba..013b1a8047 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -45,12 +45,7 @@ From HB Require Import structures. (* *) (* ## Instances of mathematical structures *) (* ``` *) -(* discrete_measurable_unit == the measurableType corresponding to *) -(* [set: set unit] *) -(* discrete_measurable_bool == the measurableType corresponding to *) -(* [set: set bool] *) -(* discrete_measurable_nat == the measurableType corresponding to *) -(* [set: set nat] *) +(* discrete_measurable T == alias for the sigma-algebra [set: set T] *) (* setring G == the set of sets G contains the empty set, is *) (* closed by union, and difference (it is a ring *) (* of sets in the sense of ringOfSetsType) *) @@ -73,7 +68,7 @@ From HB Require Import structures. (* mu .-cara.-measurable == sigma-algebra of Caratheodory measurable sets *) (* ``` *) (* *) -(* ## Structures for functions on classes of sets *) +(* ## Structures for functions on set systems *) (* *) (* Hierarchy of contents, measures, s-finite/sigma-finite/finite measures, *) (* etc. Also contains a number of details about its implementation. *) @@ -202,8 +197,8 @@ From HB Require Import structures. (* lambda_system D G == G is a lambda_system of subsets of D *) (* <> == lambda-system generated by G on D *) (* <> := <> *) -(* monotone G == G is a monotone class *) -(* <> == monotone class generated by G *) +(* monotone G == G is a monotone set system *) +(* <> == monotone set system generated by G *) (* := smallest monotone G *) (* dynkin G == G is a set of sets that form a Dynkin *) (* system (or a d-system) *) @@ -214,17 +209,19 @@ From HB Require Import structures. (* ## Other measure-theoretic definitions *) (* *) (* ``` *) -(* measurable_fun D f == the function f with domain D is measurable *) -(* preimage_class D f G == class of the preimages by f of sets in G *) -(* image_class D f G == class of the sets with a preimage by f in G *) -(* sigma_subadditive mu == predicate defining sigma-subadditivity *) +(* measurable_fun D f == the function f with domain D is measurable *) +(* preimage_set_system D f G == set system of the preimages by f of sets in G *) +(* image_set_system D f G == set system of the sets with a preimage by f *) +(* in G *) +(* sigma_subadditive mu == predicate defining sigma-subadditivity *) (* subset_sigma_subadditive mu == alternative predicate defining *) -(* sigma-subadditivity *) -(* mu.-negligible A == A is mu negligible *) -(* measure_is_complete mu == the measure mu is complete *) -(* {ae mu, forall x, P x} == P holds almost everywhere for the measure mu, *) -(* declared as an instance of the type of filters *) -(* ae_eq D f g == f is equal to g almost everywhere *) +(* sigma-subadditivity *) +(* mu.-negligible A == A is mu negligible *) +(* measure_is_complete mu == the measure mu is complete *) +(* {ae mu, forall x, P x} == P holds almost everywhere for the measure mu, *) +(* declared as an instance of the type of *) +(* filters *) +(* ae_eq D f g == f is equal to g almost everywhere *) (* ``` *) (* *) (* ## Measure extension theorem *) @@ -262,7 +259,7 @@ From HB Require Import structures. (* *) (* ## Product of measurable spaces *) (* ``` *) -(* preimage_classes f1 f2 == sigma-algebra generated by the union of *) +(* g_sigma_preimageU f1 f2 == sigma-algebra generated by the union of *) (* the preimages by f1 and the preimages by *) (* f2 with f1 : T -> T1 and f : T -> T2, T1 *) (* and T2 being semiRingOfSetsType's *) @@ -350,7 +347,7 @@ Bind Scope measure_display_scope with measure_display. Local Open Scope classical_set_scope. Local Open Scope ring_scope. -Section classes. +Section set_systems. Context {T} (C : set (set T) -> Prop) (D : set T) (G : set (set T)). Definition setC_closed := forall A, G A -> G (~` A). @@ -416,7 +413,7 @@ Definition lambda_system := Definition monotone := ndseq_closed /\ niseq_closed. -End classes. +End set_systems. #[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `lambda_system`")] Notation monotone_class := lambda_system (only parsing). #[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `setSD_closed`")] @@ -1390,13 +1387,20 @@ Qed. End sigma_ring_lambda_system. -Lemma bigcupT_measurable_rat d (T : sigmaRingType d) (F : rat -> set T) : +Lemma countable_bigcupT_measurable d (T : sigmaRingType d) U + (F : U -> set T) : countable [set: U] -> (forall i, measurable (F i)) -> measurable (\bigcup_i F i). Proof. -move=> Fm; have /ppcard_eqP[f] := card_rat. -by rewrite (reindex_bigcup f^-1%FUN setT)//=; exact: bigcupT_measurable. +elim/Ppointed: U => U in F *; first by move=> *; rewrite empty_eq0 bigcup0. +move=> /countable_bijP[B] /ppcard_eqP[f] Fm. +rewrite (reindex_bigcup f^-1%FUN setT)//=; first exact: bigcupT_measurable. +exact: (@subl_surj _ _ B). Qed. +Lemma bigcupT_measurable_rat d (T : sigmaRingType d) (F : rat -> set T) : + (forall i, measurable (F i)) -> measurable (\bigcup_i F i). +Proof. exact/countable_bigcupT_measurable. Qed. + Section measurable_lemmas. Context d (T : measurableType d). Implicit Types (A B : set T) (F : (set T)^nat) (P : set nat). @@ -1413,67 +1417,35 @@ Qed. End measurable_lemmas. -Section discrete_measurable_unit. +Section discrete_measurable. +Context {T : Type}. -Definition discrete_measurable_unit : set (set unit) := [set: set unit]. +Definition discrete_measurable : set (set T) := [set: set T]. -Let discrete_measurable0 : discrete_measurable_unit set0. Proof. by []. Qed. +Lemma discrete_measurable0 : discrete_measurable set0. Proof. by []. Qed. -Let discrete_measurableC X : - discrete_measurable_unit X -> discrete_measurable_unit (~` X). +Lemma discrete_measurableC X : + discrete_measurable X -> discrete_measurable (~` 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). +Lemma discrete_measurableU (F : (set T)^nat) : + (forall i, discrete_measurable (F i)) -> + discrete_measurable (\bigcup_i F i). Proof. by []. Qed. -HB.instance Definition _ := @isMeasurable.Build default_measure_display unit - 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]. +End discrete_measurable. -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 - discrete_measurable_bool discrete_measurable0 +HB.instance Definition _ := @isMeasurable.Build default_measure_display + unit discrete_measurable discrete_measurable0 discrete_measurableC discrete_measurableU. -End discrete_measurable_bool. - -Section discrete_measurable_nat. - -Definition discrete_measurable_nat : set (set nat) := [set: set nat]. - -Let discrete_measurable_nat0 : discrete_measurable_nat set0. Proof. by []. Qed. - -Let discrete_measurable_natC X : - discrete_measurable_nat X -> discrete_measurable_nat (~` X). -Proof. by []. Qed. - -Let discrete_measurable_natU (F : (set nat)^nat) : - (forall i, discrete_measurable_nat (F i)) -> - discrete_measurable_nat (\bigcup_i F i). -Proof. by []. Qed. - -HB.instance Definition _ := isMeasurable.Build default_measure_display nat - discrete_measurable_nat0 discrete_measurable_natC discrete_measurable_natU. +HB.instance Definition _ := @isMeasurable.Build default_measure_display + bool discrete_measurable discrete_measurable0 + discrete_measurableC discrete_measurableU. -End discrete_measurable_nat. +HB.instance Definition _ := @isMeasurable.Build default_measure_display + nat discrete_measurable discrete_measurable0 + discrete_measurableC discrete_measurableU. Definition sigma_display {T} : set (set T) -> measure_display. Proof. exact. Qed. @@ -1725,26 +1697,27 @@ Notation measurable_funT_comp := measurableT_comp (only parsing). Section measurability. -Definition preimage_class (aT rT : Type) (D : set aT) (f : aT -> rT) +Definition preimage_set_system (aT rT : Type) (D : set aT) (f : aT -> rT) (G : set (set rT)) : set (set aT) := [set D `&` f @^-1` B | B in G]. (* f is measurable on the sigma-algebra generated by itself *) -Lemma preimage_class_measurable_fun d (aT : pointedType) (rT : measurableType d) - (D : set aT) (f : aT -> rT) : - measurable_fun (D : set (g_sigma_algebraType (preimage_class D f measurable))) f. +Lemma preimage_set_system_measurable_fun d (aT : pointedType) + (rT : measurableType d) (D : set aT) (f : aT -> rT) : + measurable_fun + (D : set (g_sigma_algebraType (preimage_set_system D f measurable))) f. Proof. by move=> mD A mA; apply: sub_sigma_algebra; exists A. Qed. -Lemma sigma_algebra_preimage_class (aT rT : Type) (G : set (set rT)) +Lemma sigma_algebra_preimage (aT rT : Type) (G : set (set rT)) (D : set aT) (f : aT -> rT) : - sigma_algebra setT G -> sigma_algebra D (preimage_class D f G). + sigma_algebra setT G -> sigma_algebra D (preimage_set_system D f G). Proof. case=> h0 hC hU; split; first by exists set0 => //; rewrite preimage_set0 setI0. -- move=> A; rewrite /preimage_class /= => -[B mB <-{A}]. +- move=> A; rewrite /preimage_set_system /= => -[B mB <-{A}]. exists (~` B); first by rewrite -setTD; exact: hC. rewrite predeqE => x; split=> [[Dx Bfx]|[Dx]]; first by split => // -[] _ /Bfx. by move=> /not_andP[]. -- move=> F; rewrite /preimage_class /= => mF. +- move=> F; rewrite /preimage_set_system /= => mF. have {}mF n : exists x, G x /\ D `&` f @^-1` x = F n. by have := mF n => -[B mB <-]; exists B. have [F' mF'] := @choice _ _ (fun x y => G y /\ D `&` f @^-1` y = F x) mF. @@ -1753,15 +1726,15 @@ case=> h0 hC hU; split; first by exists set0 => //; rewrite preimage_set0 setI0. exact: (mF' i).2. Qed. -Definition image_class (aT rT : Type) (D : set aT) (f : aT -> rT) +Definition image_set_system (aT rT : Type) (D : set aT) (f : aT -> rT) (G : set (set aT)) : set (set rT) := [set B : set rT | G (D `&` f @^-1` B)]. -Lemma sigma_algebra_image_class (aT rT : Type) (D : set aT) (f : aT -> rT) +Lemma sigma_algebra_image (aT rT : Type) (D : set aT) (f : aT -> rT) (G : set (set aT)) : - sigma_algebra D G -> sigma_algebra setT (image_class D f G). + sigma_algebra D G -> sigma_algebra setT (image_set_system D f G). Proof. -move=> [G0 GC GU]; split; rewrite /image_class. +move=> [G0 GC GU]; split; rewrite /image_set_system. - by rewrite /= preimage_set0 setI0. - move=> A /= GfAD; rewrite setTD -preimage_setC -setDE. rewrite (_ : _ `\` _ = D `\` (D `&` f @^-1` A)); first exact: GC. @@ -1771,47 +1744,60 @@ move=> [G0 GC GU]; split; rewrite /image_class. - by move=> F /= mF; rewrite preimage_bigcup setI_bigcupr; exact: GU. Qed. -Lemma sigma_algebra_preimage_classE aT (rT : pointedType) (D : set aT) +Lemma g_sigma_preimageE aT (rT : pointedType) (D : set aT) (f : aT -> rT) (G' : set (set rT)) : - <> = - preimage_class D f (G'.-sigma.-measurable). + <> = + preimage_set_system D f (G'.-sigma.-measurable). Proof. rewrite eqEsubset; split. have mG : sigma_algebra D - (preimage_class D f (G'.-sigma.-measurable)). - exact/sigma_algebra_preimage_class/sigma_algebra_measurable. - have subset_preimage : preimage_class D f G' `<=` - preimage_class D f (G'.-sigma.-measurable). - by move=> A [B CCB <-{A}]; exists B => //; apply: sub_sigma_algebra. + (preimage_set_system D f (G'.-sigma.-measurable)). + exact/sigma_algebra_preimage/sigma_algebra_measurable. + have subset_preimage : preimage_set_system D f G' `<=` + preimage_set_system D f (G'.-sigma.-measurable). + by move=> A [B CCB <-{A}]; exists B => //; exact: sub_sigma_algebra. exact: smallest_sub. -have G'pre A' : G' A' -> (preimage_class D f G') (D `&` f @^-1` A'). +have G'pre A' : G' A' -> (preimage_set_system D f G') (D `&` f @^-1` A'). by move=> ?; exists A'. -pose I : set (set aT) := <>. -have G'sfun : G' `<=` image_class D f I. +pose I : set (set aT) := <>. +have G'sfun : G' `<=` image_set_system D f I. by move=> A' /G'pre[B G'B h]; apply: sub_sigma_algebra; exists B. -have sG'sfun : <> `<=` image_class D f I. - apply: smallest_sub => //; apply: sigma_algebra_image_class. +have sG'sfun : <> `<=` image_set_system D f I. + apply: smallest_sub => //; apply: sigma_algebra_image. exact: smallest_sigma_algebra. by move=> _ [B mB <-]; exact: sG'sfun. Qed. Lemma measurability d d' (aT : measurableType d) (rT : measurableType d') (D : set aT) (f : aT -> rT) (G : set (set rT)) : - @measurable _ rT = <> -> preimage_class D f G `<=` @measurable _ aT -> + @measurable _ rT = <> -> preimage_set_system D f G `<=` @measurable _ aT -> measurable_fun D f. Proof. move=> sG_rT fG_aT mD. -suff h : preimage_class D f (@measurable _ rT) `<=` @measurable _ aT. +suff h : preimage_set_system D f (@measurable _ rT) `<=` @measurable _ aT. by move=> A mA; apply: h; exists A. -have -> : preimage_class D f (@measurable _ rT) = - <>. - by rewrite [in LHS]sG_rT [in RHS]sigma_algebra_preimage_classE. +have -> : preimage_set_system D f (@measurable _ rT) = + <>. + by rewrite [in LHS]sG_rT [in RHS]g_sigma_preimageE. apply: smallest_sub => //; split => //. - by move=> A mA; exact: measurableD. - by move=> F h; exact: bigcupT_measurable. Qed. End measurability. +#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `preimage_set_system`")] +Notation preimage_class := preimage_set_system (only parsing). +#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `image_set_system`")] +Notation image_class := image_set_system (only parsing). +#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `preimage_set_system_measurable_fun`")] +Notation preimage_class_measurable_fun := preimage_set_system_measurable_fun (only parsing). +#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `sigma_algebra_preimage`")] +Notation sigma_algebra_preimage_class := sigma_algebra_preimage (only parsing). +#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `sigma_algebra_image`")] +Notation sigma_algebra_image_class := sigma_algebra_image (only parsing). + +#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `g_sigma_preimageE`")] +Notation sigma_algebra_preimage_classE := g_sigma_preimageE (only parsing). Local Open Scope ereal_scope. @@ -3035,7 +3021,7 @@ apply: (@le_trans _ _ move=> XD; have Xm := decomp_measurable Dm XD. by apply: muS => // [i|]; [exact: mfD|exact: DXsub]. apply: lee_lim => /=; do ?apply: is_cvg_nneseries=> //. - by move=> n _; exact: sume_ge0. + by move=> n _ _; exact: sume_ge0. near=> n; rewrite [n in _ <= n]big_mkcond; apply: lee_sum => i _. rewrite ifT ?inE//. under eq_big_seq. @@ -4135,7 +4121,9 @@ Proof. by apply: filterS => x /[apply] /= ->. Qed. Lemma ae_eq_funeposneg f g : ae_eq f g <-> ae_eq f^\+ g^\+ /\ ae_eq f^\- g^\-. Proof. split=> [fg|[]]. - by rewrite /funepos /funeneg; split; apply: filterS fg => x /[apply] ->. + split; apply: filterS fg => x /[apply]. + by rewrite !funeposE => ->. + by rewrite !funenegE => ->. apply: filterS2 => x + + Dx => /(_ Dx) fg /(_ Dx) gf. by rewrite (funeposneg f) (funeposneg g) fg gf. Qed. @@ -4242,7 +4230,7 @@ have := outer_measure_sigma_subadditive mu (fun n => if n \in ~` `I_N then F n else set0). move/le_trans; apply. rewrite [in leRHS]eseries_cond [in leRHS]eseries_mkcondr; apply: lee_nneseries. -- by move=> k _; exact: outer_measure_ge0. +- by move=> k _ _; exact: outer_measure_ge0. - move=> k _; rewrite fun_if; case: ifPn => Nk; first by rewrite mem_not_I Nk. by rewrite mem_not_I (negbTE Nk) outer_measure0. Qed. @@ -4522,7 +4510,8 @@ suff : forall X, mu X = \sum_(k _) = fun n => \sum_(k < n) mu (A k)); last first. rewrite funeqE => n; rewrite big_mkord; apply: eq_bigr => i _; congr (mu _). by rewrite setIC; apply/setIidPl; exact: bigcup_sup. - move=> ->; have := fun n (_ : xpredT n) => outer_measure_ge0 mu (A n). + move=> ->. + have := fun n (_ : xpredT n) (_ : xpredT n) => outer_measure_ge0 mu (A n). move/(@is_cvg_nneseries _ _ _ 0) => /cvg_ex[l] hl. under [in X in _ --> X]eq_fun do rewrite -(big_mkord xpredT (mu \o A)). by move/cvg_lim : (hl) => ->. @@ -4699,9 +4688,9 @@ rewrite (_ : esum _ _ = \sum_(i ? ? _ _; exact: (@can_inj _ _ _ snd). by congr esum; rewrite predeqE => -[a b]; split; move=> [i _ <-]; exists i. apply: lee_lim. -- apply: is_cvg_nneseries => n _. - by apply: nneseries_ge0 => m _; exact: (muG_ge0 (n, m)). -- by apply: is_cvg_nneseries => n _; apply: adde_ge0 => //; exact: mu_ext_ge0. +- apply: is_cvg_nneseries => n *. + by apply: nneseries_ge0 => m *; exact: (muG_ge0 (n, m)). +- by apply: is_cvg_nneseries => n *; apply: adde_ge0 => //; exact: mu_ext_ge0. - by near=> n; apply: lee_sum => i _; exact: (PG i).2. Unshelve. all: by end_near. Qed. @@ -4783,11 +4772,11 @@ have G_E n : G_ n = [set g n `&` C | C in G]. by move=> X [GX Xgn] /=; exists X => //; rewrite setIidr. by rewrite /G_ => X [Y GY <-{X}]; split; [exact: setIG|apply: subIset; left]. have gIsGE n : [set g n `&` A | A in <>] = - <>. - rewrite sigma_algebra_preimage_classE eqEsubset; split. + <>. + rewrite g_sigma_preimageE eqEsubset; split. by move=> _ /= [Y sGY <-]; exists Y => //; rewrite preimage_id setIC. by move=> _ [Y mY <-] /=; exists Y => //; rewrite preimage_id setIC. -have preimg_gGE n : preimage_class (g n) id G = G_ n. +have preimg_gGE n : preimage_set_system (g n) id G = G_ n. rewrite eqEsubset; split => [_ [Y GY <-]|]. by rewrite preimage_id G_E /=; exists Y => //; rewrite setIC. by move=> X [GX Xgn]; exists X => //; rewrite preimage_id setIidr. @@ -4918,24 +4907,24 @@ apply: (@le_trans _ _ (limn BA + limn BNA)); [apply: leeD|]. apply: (@le_trans _ _ (mu_ext mu (\bigcup_k (B k `\` A)))). by apply: le_mu_ext; rewrite -setI_bigcupl; exact: setISS. exact: outer_measure_sigma_subadditive. -have ? : cvg (BNA @ \oo) by exact: is_cvg_nneseries. -have ? : cvg (BA @ \oo) by exact: is_cvg_nneseries. -have ? : cvg (eseries (Rmu \o B) @ \oo) by exact: is_cvg_nneseries. +have cBNA : cvg (BNA @ \oo) by exact: is_cvg_nneseries. +have cBA : cvg (BA @ \oo) by exact: is_cvg_nneseries. +have cB : cvg (eseries (Rmu \o B) @ \oo) by exact: is_cvg_nneseries. have [def|] := boolP (lim (BA @ \oo) +? lim (BNA @ \oo)); last first. rewrite /adde_def negb_and !negbK=> /orP[/andP[BAoo BNAoo]|/andP[BAoo BNAoo]]. - suff -> : limn (eseries (Rmu \o B)) = +oo by rewrite leey. - apply/eqP; rewrite -leye_eq -(eqP BAoo); apply/lee_lim => //. + apply/eqP; rewrite -leye_eq -(eqP BAoo); apply/(lee_lim cBA cB). near=> n; apply: lee_sum => m _; apply: le_measure; rewrite /mkset; by [rewrite inE; exact: measurableI | rewrite inE | apply: subIset; left]. - suff -> : limn (eseries (Rmu \o B)) = +oo by rewrite leey. - apply/eqP; rewrite -leye_eq -(eqP BNAoo); apply/lee_lim => //. + apply/eqP; rewrite -leye_eq -(eqP BNAoo); apply/(lee_lim cBNA cB). by near=> n; apply: lee_sum => m _; rewrite -setDE; apply: le_measure; rewrite /mkset ?inE//; apply: measurableD. -rewrite -limeD // (_ : (fun _ => _) = +rewrite -(limeD cBA cBNA) // (_ : (fun _ => _) = eseries (fun k => Rmu (B k `&` A) + Rmu (B k `&` ~` A))); last first. by rewrite funeqE => n; rewrite -big_split /=; exact: eq_bigr. apply/lee_lim => //. - by apply/is_cvg_nneseries => // n _; exact: adde_ge0. + by apply/is_cvg_nneseries => // n *; exact: adde_ge0. near=> n; apply: lee_sum => i _; rewrite -measure_semi_additive2. - apply: le_measure; rewrite /mkset ?inE//; [|by rewrite -setIUr setUCr setIT]. by apply: measurableU; [exact:measurableI|rewrite -setDE; exact:measurableD]. @@ -5037,21 +5026,24 @@ Qed. End completed_measure_extension. -Definition preimage_classes d1 d2 +Definition g_sigma_preimageU d1 d2 (T1 : semiRingOfSetsType d1) (T2 : semiRingOfSetsType d2) (T : Type) (f1 : T -> T1) (f2 : T -> T2) := - <>. + <>. +#[deprecated(since="mathcomp-analysis 1.9.0", + note="renamed to `g_sigma_preimageU`")] +Notation preimage_classes := g_sigma_preimageU (only parsing). Section product_lemma. Context d1 d2 (T1 : semiRingOfSetsType d1) (T2 : semiRingOfSetsType d2). Variables (T : pointedType) (f1 : T -> T1) (f2 : T -> T2). Variables (T3 : Type) (g : T3 -> T). -Lemma preimage_classes_comp : preimage_classes (f1 \o g) (f2 \o g) = - preimage_class setT g (preimage_classes f1 f2). +Lemma g_sigma_preimageU_comp : g_sigma_preimageU (f1 \o g) (f2 \o g) = + preimage_set_system setT g (g_sigma_preimageU f1 f2). Proof. -rewrite {1}/preimage_classes -sigma_algebra_preimage_classE; congr (<>). +rewrite {1}/g_sigma_preimageU -g_sigma_preimageE; congr (<>). rewrite predeqE => C; split. - move=> [[A mA <-{C}]|[A mA <-{C}]]. + by exists (f1 @^-1` A) => //; left; exists A => //; rewrite setTI. @@ -5062,6 +5054,9 @@ rewrite predeqE => C; split. Qed. End product_lemma. +#[deprecated(since="mathcomp-analysis 1.9.0", + note="renamed to `g_sigma_preimageU_comp`")] +Notation preimage_classes_comp := g_sigma_preimageU_comp (only parsing). Definition measure_prod_display : (measure_display * measure_display) -> measure_display. @@ -5072,21 +5067,22 @@ Context d1 d2 (T1 : semiRingOfSetsType d1) (T2 : semiRingOfSetsType d2). Let f1 := @fst T1 T2. Let f2 := @snd T1 T2. -Let prod_salgebra_set0 : preimage_classes f1 f2 (set0 : set (T1 * T2)). +Let prod_salgebra_set0 : g_sigma_preimageU f1 f2 (set0 : set (T1 * T2)). Proof. exact: sigma_algebra0. Qed. -Let prod_salgebra_setC A : preimage_classes f1 f2 A -> - preimage_classes f1 f2 (~` A). +Let prod_salgebra_setC A : g_sigma_preimageU f1 f2 A -> + g_sigma_preimageU f1 f2 (~` A). Proof. exact: sigma_algebraC. Qed. -Let prod_salgebra_bigcup (F : _^nat) : (forall i, preimage_classes f1 f2 (F i)) -> - preimage_classes f1 f2 (\bigcup_i (F i)). +Let prod_salgebra_bigcup (F : _^nat) : + (forall i, g_sigma_preimageU f1 f2 (F i)) -> + g_sigma_preimageU f1 f2 (\bigcup_i (F i)). Proof. exact: sigma_algebra_bigcup. Qed. HB.instance Definition _ := Pointed.on (T1 * T2)%type. HB.instance Definition prod_salgebra_mixin := @isMeasurable.Build (measure_prod_display (d1, d2)) - (T1 * T2)%type (preimage_classes f1 f2) + (T1 * T2)%type (g_sigma_preimageU f1 f2) (prod_salgebra_set0) (prod_salgebra_setC) (prod_salgebra_bigcup). End product_salgebra_instance. @@ -5121,14 +5117,14 @@ Proof. rewrite eqEsubset; split. apply: smallest_sub; first exact: smallest_sigma_algebra. rewrite subUset; split. - - have /subset_trans : preimage_class setT fst M1 `<=` M1xM2. + - have /subset_trans : preimage_set_system setT fst M1 `<=` M1xM2. by move=> _ [X MX <-]; exists X=> //; exists setT; rewrite /M2 // setIC//. by apply; exact: sub_sigma_algebra. - - have /subset_trans : preimage_class setT snd M2 `<=` M1xM2. + - have /subset_trans : preimage_set_system setT snd M2 `<=` M1xM2. by move=> _ [Y MY <-]; exists setT; rewrite /M1 //; exists Y. by apply; exact: sub_sigma_algebra. apply: smallest_sub; first exact: smallest_sigma_algebra. -by move=> _ [A MA] [B MB] <-; apply: measurableX => //; exact: sub_sigma_algebra. +by move=> _ [A ?] [B ?] <-; apply: measurableX => //; exact: sub_sigma_algebra. Qed. End product_salgebra_algebraOfSetsType. @@ -5173,8 +5169,8 @@ Context d d1 d2 (T : measurableType d) (T1 : measurableType d1) Lemma prod_measurable_funP (h : T -> T1 * T2) : measurable_fun setT h <-> measurable_fun setT (fst \o h) /\ measurable_fun setT (snd \o h). Proof. -apply: (@iff_trans _ (preimage_classes (fst \o h) (snd \o h) `<=` measurable)). -- rewrite preimage_classes_comp; split=> [mf A [C HC <-]|f12]; first exact: mf. +apply: (@iff_trans _ (g_sigma_preimageU (fst \o h) (snd \o h) `<=` measurable)). +- rewrite g_sigma_preimageU_comp; split=> [mf A [C HC <-]|f12]; first exact: mf. by move=> _ A mA; apply: f12; exists A. - split => [h12|[mf1 mf2]]. split => _ A mA; apply: h12; apply: sub_sigma_algebra; @@ -5257,6 +5253,27 @@ End partial_measurable_fun. #[global] Hint Extern 0 (measurable_fun _ (pair^~ _)) => solve [apply: measurable_pair2] : core. +Section measurable_section. +Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2). + +Lemma measurable_xsection (A : set (T1 * T2)) (x : T1) : + measurable A -> measurable (xsection A x). +Proof. +move=> mA; pose i (y : T2) := (x, y). +have mi : measurable_fun setT i by exact: measurable_pair1. +by rewrite xsectionE -[X in measurable X]setTI; exact: mi. +Qed. + +Lemma measurable_ysection (A : set (T1 * T2)) (y : T2) : + measurable A -> measurable (ysection A y). +Proof. +move=> mA; pose i (x : T1) := (x, y). +have mi : measurable_fun setT i by exact: measurable_pair2. +by rewrite ysectionE -[X in measurable X]setTI; exact: mi. +Qed. + +End measurable_section. + Section absolute_continuity. Context d (T : semiRingOfSetsType d) (R : realType). Implicit Types m : set T -> \bar R. diff --git a/theories/normedtype.v b/theories/normedtype.v index c8ffba17b8..b87600267c 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -986,6 +986,9 @@ Module Exports. Export numFieldTopology.Exports. HB.reexport. End Exports. End numFieldNormedType. Import numFieldNormedType.Exports. +Lemma scaler1 {R : numFieldType} h : h%:A = h :> R. +Proof. by rewrite /GRing.scale/= mulr1. Qed. + Lemma limf_esup_dnbhsN {R : realType} (f : R -> \bar R) (a : R) : limf_esup f a^' = limf_esup (fun x => f (- x)%R) (- a)%R^'. Proof. diff --git a/theories/numfun.v b/theories/numfun.v index 92f31a9c9c..acb61398b0 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -127,69 +127,85 @@ Proof. by apply/funext=> x; rewrite /patch/=; case: ifP; rewrite ?mule0. Qed. End erestrict_lemmas. -Section funposneg. -Local Open Scope ereal_scope. - +HB.lock Definition funepos T (R : realDomainType) (f : T -> \bar R) := fun x => maxe (f x) 0. +HB.lock Definition funeneg T (R : realDomainType) (f : T -> \bar R) := - fun x => maxe (- f x) 0. - -End funposneg. + fun x => maxe (oppe (f x)) 0. Notation "f ^\+" := (funepos f) : ereal_scope. Notation "f ^\-" := (funeneg f) : ereal_scope. Section funposneg_lemmas. Local Open Scope ereal_scope. -Variables (T : Type) (R : realDomainType) (D : set T). -Implicit Types (f g : T -> \bar R) (r : R). +Variables (T U : Type) (R : realDomainType) (D : set T). +Implicit Types (f g : T -> \bar R) (h : U -> T) (r : R). + +Lemma funeposE f x : f^\+ x = maxe (f x) 0. +Proof. by rewrite unlock. Qed. + +Lemma funenegE f x : f^\- x = maxe (- f x) 0. +Proof. by rewrite unlock. Qed. Lemma funepos_ge0 f x : 0 <= f^\+ x. -Proof. by rewrite /funepos /= le_max lexx orbT. Qed. +Proof. by rewrite funeposE le_max lexx orbT. Qed. Lemma funeneg_ge0 f x : 0 <= f^\- x. -Proof. by rewrite /funeneg le_max lexx orbT. Qed. +Proof. by rewrite funenegE le_max lexx orbT. Qed. -Lemma funeposN f : (\- f)^\+ = f^\-. Proof. exact/funext. Qed. +Lemma funeposN f : (\- f)^\+ = f^\-. +Proof. by apply/funext => x; rewrite funeposE funenegE. Qed. Lemma funenegN f : (\- f)^\- = f^\+. -Proof. by apply/funext => x; rewrite /funeneg oppeK. Qed. +Proof. by apply/funext => x; rewrite funeposE funenegE oppeK. Qed. + +Lemma funepos_comp f h : (f \o h)^\+ = f^\+ \o h. +Proof. by rewrite !unlock. Qed. + +Lemma funeneg_comp f h : (f \o h)^\- = f^\- \o h. +Proof. by rewrite !unlock. Qed. Lemma funepos_restrict f : (f \_ D)^\+ = (f^\+) \_ D. Proof. -by apply/funext => x; rewrite /patch/_^\+; case: ifP; rewrite //= maxxx. +by apply/funext => x; rewrite /patch !funeposE; case: ifP; rewrite //= maxxx. Qed. Lemma funeneg_restrict f : (f \_ D)^\- = (f^\-) \_ D. Proof. -by apply/funext => x; rewrite /patch/_^\-; case: ifP; rewrite //= oppr0 maxxx. +apply/funext => x; rewrite /patch !funenegE. +by case: ifP; rewrite //= oppr0 maxxx. Qed. Lemma ge0_funeposE f : (forall x, D x -> 0 <= f x) -> {in D, f^\+ =1 f}. -Proof. by move=> f0 x; rewrite inE => Dx; apply/max_idPl/f0. Qed. +Proof. by move=> f0 x; rewrite inE funeposE => Dx; apply/max_idPl/f0. Qed. Lemma ge0_funenegE f : (forall x, D x -> 0 <= f x) -> {in D, f^\- =1 cst 0}. Proof. -by move=> f0 x; rewrite inE => Dx; apply/max_idPr; rewrite leeNl oppe0 f0. +move=> f0 x; rewrite inE funenegE => Dx; apply/max_idPr. +by rewrite leeNl oppe0 f0. Qed. Lemma le0_funeposE f : (forall x, D x -> f x <= 0) -> {in D, f^\+ =1 cst 0}. -Proof. by move=> f0 x; rewrite inE => Dx; exact/max_idPr/f0. Qed. +Proof. by move=> f0 x; rewrite inE funeposE => Dx; exact/max_idPr/f0. Qed. Lemma le0_funenegE f : (forall x, D x -> f x <= 0) -> {in D, f^\- =1 \- f}. Proof. -by move=> f0 x; rewrite inE => Dx; apply/max_idPl; rewrite leeNr oppe0 f0. +move=> f0 x; rewrite inE funenegE => Dx; apply/max_idPl. +by rewrite leeNr oppe0 f0. Qed. Lemma ge0_funeposM r f : (0 <= r)%R -> (fun x => r%:E * f x)^\+ = (fun x => r%:E * (f^\+ x)). -Proof. by move=> ?; rewrite funeqE => x; rewrite /funepos maxe_pMr// mule0. Qed. +Proof. +move=> ?; rewrite funeqE => x. +by rewrite !funeposE maxe_pMr// mule0. +Qed. Lemma ge0_funenegM r f : (0 <= r)%R -> (fun x => r%:E * f x)^\- = (fun x => r%:E * (f^\- x)). Proof. -by move=> r0; rewrite funeqE => x; rewrite /funeneg -muleN maxe_pMr// mule0. +by move=> r0; rewrite funeqE => x; rewrite !funenegE -muleN maxe_pMr// mule0. Qed. Lemma le0_funeposM r f : (r <= 0)%R -> @@ -209,36 +225,36 @@ Qed. Lemma fune_abse f : abse \o f = f^\+ \+ f^\-. Proof. rewrite funeqE => x /=; have [fx0|/ltW fx0] := leP (f x) 0. -- rewrite lee0_abs// /funepos /funeneg. +- rewrite lee0_abs// funeposE funenegE. move/max_idPr : (fx0) => ->; rewrite add0e. by move: fx0; rewrite -{1}oppe0 leeNr => /max_idPl ->. -- rewrite gee0_abs// /funepos /funeneg; move/max_idPl : (fx0) => ->. +- rewrite gee0_abs// funeposE funenegE; move/max_idPl : (fx0) => ->. by move: fx0; rewrite -{1}oppe0 leeNl => /max_idPr ->; rewrite adde0. Qed. Lemma funeposneg f : f = (fun x => f^\+ x - f^\- x). Proof. -rewrite funeqE => x; rewrite /funepos /funeneg; have [|/ltW] := leP (f x) 0. +rewrite funeqE => x; rewrite funeposE funenegE; have [|/ltW] := leP (f x) 0. by rewrite -{1}oppe0 -leeNr => /max_idPl ->; rewrite oppeK add0e. by rewrite -{1}oppe0 -leeNl => /max_idPr ->; rewrite sube0. Qed. Lemma add_def_funeposneg f x : (f^\+ x +? - f^\- x). Proof. -by rewrite /funeneg /funepos; case: (f x) => [r| |]; +by rewrite funenegE funeposE; case: (f x) => [r| |]; [rewrite -fine_max/=|rewrite /maxe /= ltNyr|rewrite /maxe /= ltNyr]. Qed. Lemma funeD_Dpos f g : f \+ g = (f \+ g)^\+ \- (f \+ g)^\-. Proof. -apply/funext => x; rewrite /funepos /funeneg; have [|/ltW] := leP 0 (f x + g x). +apply/funext => x; rewrite funeposE funenegE; have [|/ltW] := leP 0 (f x + g x). - by rewrite -{1}oppe0 -leeNl => /max_idPr ->; rewrite sube0. - by rewrite -{1}oppe0 -leeNr => /max_idPl ->; rewrite oppeK add0e. Qed. Lemma funeD_posD f g : f \+ g = (f^\+ \+ g^\+) \- (f^\- \+ g^\-). Proof. -apply/funext => x; rewrite /funepos /funeneg. +apply/funext => x; rewrite !funeposE !funenegE. have [|fx0] := leP 0 (f x); last rewrite add0e. - rewrite -{1}oppe0 leeNl => /max_idPr ->; have [|/ltW] := leP 0 (g x). by rewrite -{1}oppe0 leeNl => /max_idPr ->; rewrite adde0 sube0. @@ -255,7 +271,7 @@ Qed. Lemma funepos_le f g : {in D, forall x, f x <= g x} -> {in D, forall x, f^\+ x <= g^\+ x}. Proof. -move=> fg x Dx; rewrite /funepos /maxe; case: ifPn => fx; case: ifPn => gx //. +move=> fg x Dx; rewrite !funeposE /maxe; case: ifPn => fx; case: ifPn => gx //. - by rewrite leNgt. - by move: fx; rewrite -leNgt => /(lt_le_trans gx); rewrite ltNge fg. - exact: fg. @@ -264,7 +280,7 @@ Qed. Lemma funeneg_le f g : {in D, forall x, f x <= g x} -> {in D, forall x, g^\- x <= f^\- x}. Proof. -move=> fg x Dx; rewrite /funeneg /maxe; case: ifPn => gx; case: ifPn => fx //. +move=> fg x Dx; rewrite !funenegE /maxe; case: ifPn => gx; case: ifPn => fx //. - by rewrite leNgt. - by move: gx; rewrite -leNgt => /(lt_le_trans fx); rewrite lteN2 ltNge fg. - by rewrite leeN2; exact: fg. @@ -365,7 +381,7 @@ Lemma xsection_indic (R : ringType) T1 T2 (A : set (T1 * T2)) x : xsection A x = (fun y => (\1_A (x, y) : R)) @^-1` [set 1]. Proof. apply/seteqP; split => [y/mem_set/=|y/=]; rewrite indicE. -by rewrite mem_xsection => ->. + by rewrite mem_xsection => ->. by rewrite /xsection/=; case: (_ \in _) => //= /esym/eqP /[!oner_eq0]. Qed. @@ -373,7 +389,7 @@ Lemma ysection_indic (R : ringType) T1 T2 (A : set (T1 * T2)) y : ysection A y = (fun x => (\1_A (x, y) : R)) @^-1` [set 1]. Proof. apply/seteqP; split => [x/mem_set/=|x/=]; rewrite indicE. -by rewrite mem_ysection => ->. + by rewrite mem_ysection => ->. by rewrite /ysection/=; case: (_ \in _) => //= /esym/eqP /[!oner_eq0]. Qed. diff --git a/theories/pi_irrational.v b/theories/pi_irrational.v new file mode 100644 index 0000000000..d070d0b31f --- /dev/null +++ b/theories/pi_irrational.v @@ -0,0 +1,433 @@ +From mathcomp Require Import all_ssreflect all_algebra archimedean finmap. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import cardinality fsbigop signed reals ereal topology. +From mathcomp Require Import normedtype sequences real_interval esum measure. +From mathcomp Require Import lebesgue_measure numfun realfun lebesgue_integral. +From mathcomp Require Import derive charge ftc trigo. + +(**md**************************************************************************) +(* # Formalisation of A simple proof that pi is irrational by Ivan Niven *) +(* *) +(* Reference: *) +(* - http://projecteuclid.org/download/pdf_1/euclid.bams/1183510788 *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Import Order.TTheory GRing.Theory Num.Theory. +Import numFieldNormedType.Exports. + +(* TODO: move *) +Lemma measurable_poly {R : realType} (p : {poly R}) (A : set R) : + measurable_fun A (horner p). +Proof. +apply/measurable_funTS; apply: continuous_measurable_fun. +exact/continuous_horner. +Qed. + +(* TODO: move somewhere to classical *) +Definition rational {R : realType} (x : R) := exists m n, x = (m%:R / n%:R)%R. + +Module pi_irrational. +Local Open Scope ring_scope. + +Lemma exp_fact (R : realType) (r : R) : + (r ^+ n / n`!%:R @[n --> \oo] --> 0)%classic. +Proof. +by apply/cvg_series_cvg_0; exact: is_cvg_series_exp_coeff. +Qed. + +Section algebraic_part. +Context {R : realType}. +Variables na nb n : nat. +Hypothesis nb0 : nb != 0%N. + +Definition a : R := na%:R. + +Definition b : R := nb%:R. + +Definition f : {poly R} := n`!%:R^-1 *: ('X^n * (a%:P - b *: 'X) ^+ n). + +Definition F : {poly R} := \sum_(i < n.+1) (-1)^i *: f^`(i.*2). + +Let b0 : b != 0. Proof. by rewrite pnatr_eq0. Qed. + +Let P1_size : size (a%:P - b *: 'X) = 2. +Proof. +have hs : size (- (b *: 'X)) = 2%N. + by rewrite size_opp (* TODO: size_opp -> sizeN *) size_scale ?b0// size_polyX. +by rewrite addrC size_addl hs ?size_polyC//; case: (a != 0). +Qed. + +Let P1_lead_coef : lead_coef (a%:P - b *: 'X) = - b. +Proof. +rewrite addrC lead_coefDl. + by rewrite lead_coefN lead_coefZ lead_coefX mulr1. +by rewrite size_opp size_scale ?b0// size_polyX size_polyC; case: (a != 0). +Qed. + +Let P_size : size ((a%:P - b*:'X) ^+ n) = n.+1. +Proof. +elim : n => [|n0 Hn0]; first by rewrite expr0 size_polyC oner_neq0. +rewrite exprS size_proper_mul; first by rewrite P1_size /= Hn0. +by rewrite lead_coef_exp P1_lead_coef -exprS expf_neq0 // oppr_eq0 b0. +Qed. + +Let comp_poly_exprn (p q : {poly R}) i : p ^+ i \Po q = (p \Po q) ^+ i. +Proof. +elim: i => [|i ih]; first by rewrite !expr0 comp_polyC. +by rewrite !exprS comp_polyM ih. +Qed. + +Let f_int i : n`!%:R * f`_i \is a Num.int. +Proof. +rewrite /f coefZ mulrA divff ?mul1r ?pnatr_eq0 ?gtn_eqF ?fact_gt0//. +apply/polyOverP => /=; rewrite rpredM ?rpredX ?polyOverX//=. +by rewrite rpredB ?polyOverC ?polyOverZ ?polyOverX//= nat_int. +Qed. + +Let f_small_coef0 i : (i < n)%N -> f`_i = 0. +Proof. +move=> ni; rewrite /f coefZ; apply/eqP. +rewrite mulf_eq0 invr_eq0 pnatr_eq0 gtn_eqF ?fact_gt0//=. +by rewrite coefXnM ni. +Qed. + +Let derive_f_0_int i : f^`(i).[0] \is a Num.int. +Proof. +rewrite horner_coef0 coef_derivn addn0 ffactnn. +have [/f_small_coef0 ->|/bin_fact <-] := ltnP i n. + by rewrite mul0rn // int_Qint. +by rewrite mulnCA -mulr_natl natrM mulrAC rpredM ?f_int ?nat_int. +Qed. + +Lemma F0_int : F.[0] \is a Num.int. +Proof. +rewrite /F horner_sum rpred_sum //= => i _. +by rewrite !hornerE rpredM//= -exprnP rpredX// rpredN int_num1. +Qed. + +Definition pirat := a / b. + +Let pf_sym : f \Po (pirat%:P - 'X) = f. +Proof. +rewrite /f comp_polyZ; congr *:%R. +rewrite comp_polyM !comp_poly_exprn comp_polyB comp_polyC !comp_polyZ. +rewrite !comp_polyX scalerBr. +have bap : b%:P * pirat%:P = a%:P. + by rewrite polyCM mulrC -mulrA -polyCM mulVf ?b0 // mulr1. +suff -> : a%:P - (b *: pirat%:P - b *: 'X) = b%:P * 'X. + rewrite exprMn mulrA mulrC; congr *%R. + rewrite -exprMn; congr (_ ^+ _). + rewrite mulrBl /pirat mul_polyC -bap (mulrC b%:P); congr (_ - _)%R. + by rewrite mul_polyC. + by rewrite mulrC mul_polyC. +by rewrite -mul_polyC bap opprB addrCA subrr addr0 mul_polyC. +Qed. + +Let derivn_fpix i : f^`(i) \Po (pirat%:P - 'X) = (-1) ^+ i *: f^`(i). +Proof. +elim:i ; first by rewrite /= expr0 scale1r pf_sym. +move=> i Hi. +rewrite [in RHS]derivnS exprS mulN1r scaleNr -(derivZ ((-1) ^+ i)) -Hi. +by rewrite deriv_comp derivB derivX -derivnS derivC sub0r mulrN1 opprK. +Qed. + +Lemma FPi_int : F.[pirat] \is a Num.int. +Proof. +rewrite /F horner_sum rpred_sum // => i _ ; rewrite !hornerE rpredM //=. + by rewrite -exprnP rpredX// (_ : -1 = (-1)%:~R)// intr_int. +move: (derivn_fpix i.*2). +rewrite -mul2n mulnC exprM sqrr_sign scale1r => <-. +by rewrite horner_comp !hornerE subrr derive_f_0_int. +Qed. + +Lemma D2FDF : F^`(2) + F = f. +Proof. +rewrite /F linear_sum /=. +rewrite (eq_bigr (fun i : 'I_n.+1 => ((-1)^i *: f^`(i.+1.*2)%N))); last first. + by move=> i _ ;rewrite !derivZ. +rewrite [X in _ + X]big_ord_recl/=. +rewrite -exprnP expr0 scale1r (addrC f) addrA -[X in _ = X]add0r. +congr (_ + _). +rewrite big_ord_recr addrC addrA -big_split big1=>[| i _]. + rewrite add0r /=; apply/eqP; rewrite scaler_eq0 -derivnS derivn_poly0. + by rewrite deriv0 eqxx orbT. + suff -> : size f = (n + n.+1)%N by rewrite addnS addnn. + rewrite /f size_scale; last first. + by rewrite invr_neq0 // pnatr_eq0 -lt0n (fact_gt0 n). + rewrite size_monicM ?monicXn //; last by rewrite -size_poly_eq0 P_size. + by rewrite size_polyXn P_size. +rewrite /bump /= -scalerDl. +apply/eqP; rewrite scaler_eq0 /bump -exprnP add1n exprSr. +by rewrite mulrN1 addrC subr_eq0 eqxx orTb. +Qed. + +End algebraic_part. + +Section analytic_part. +Context {R : realType}. +Let mu := @lebesgue_measure R. +Variable na nb : nat. +Hypothesis nb0 : nb != 0%N. + +Let pirat : R := pirat na nb. + +Let a : R := a na. + +Let b : R := b nb. + +Let f := @f R na nb. + +Let abx_gt0 x : 0 < x < pirat -> 0 < a - b * x. +Proof. +move=> /andP[x0]; rewrite subr_gt0. +rewrite /pirat /pirat ltr_pdivlMr 1?mulrC//. +by rewrite ltr0n lt0n. +Qed. + +Let abx_ge0 x : 0 <= x <= pirat -> 0 <= a - b * x. +Proof. +move=> /andP[x0 xpi]; rewrite subr_ge0. +rewrite -ler_pdivlMl//; last by rewrite /b ltr0n lt0n. +by rewrite mulrC. +Qed. + +Let fsin n := fun x : R => (f n).[x] * sin x. + +Let F := @F R na nb. + +Let fsin_antiderivative n : + (fun x => (horner (F n))^`()%classic x * sin x - (F n).[x] * cos x)^`()%classic = + fsin n. +Proof. +apply/funext => x/=. +rewrite derive1E/= deriveD//=; last first. + apply: derivableM; last exact: ex_derive. + by rewrite -derivE; exact: derivable_horner. +rewrite deriveM//; last by rewrite -derivE; exact: derivable_horner. +rewrite deriveN//= deriveM// !derive_val opprD -addrA addrC !addrA. +rewrite scalerN opprK -addrA [X in (_ + X = _)%R](_ : _ = 0%R); last first. + rewrite addrC derivE. + by apply/eqP; rewrite subr_eq0 [eqbLHS]mulrC. +rewrite addr0 -derive1E. +have := @D2FDF R na _ n nb0. +rewrite -/F derivSn /fsin -/f => <-. +rewrite -!derivE derivn1. +rewrite [X in (X + _ = _)%R](_ : _ = (F n)^`()^`().[x]%R * sin x)%R; last first. + by rewrite mulrC. +by rewrite -mulrDl hornerD. +Qed. + +Definition intfsin n := \int[mu]_(x in `[0, pi]) (fsin n x). + +Local Open Scope classical_set_scope. + +Let cfsin n (A : set R) : {within A, continuous (fsin n)}. +Proof. +apply/continuous_subspaceT => /= x. +by apply: cvgM => /=; [exact: continuous_horner|exact: continuous_sin]. +Qed. + +Goal forall (p : {poly R}) c, p.[x] @[x --> c^'+] --> p.[c]. +by move=> p c; apply: cvg_at_right_filter; exact: continuous_horner. +Qed. + +Let intfsinE n : intfsin n = (F n).[pi] + (F n).[0]. +Proof. +rewrite /intfsin /Rintegral. +set h := fun x => (derive1 (fun x => (F n).[x]) x * sin x - (F n).[x] * cos x). +rewrite (@continuous_FTC2 _ _ h). +- rewrite /h sin0 cospi cos0 sinpi !mulr0 !add0r mulr1 mulrN1 !opprK EFinN. + by rewrite oppeK -EFinD. +- by rewrite pi_gt0. +- exact: cfsin. +- split=> [x x0pi| |]. + + by apply: derivableB => //; apply: derivableM => //; rewrite -derivE. + + apply: cvgB. + by rewrite -derivE; apply: cvgM => //; apply: cvg_at_right_filter; + [exact: continuous_horner|exact: continuous_sin]. + by apply: cvgM => //; apply: cvg_at_right_filter; + [exact: continuous_horner|exact: continuous_cos]. + + apply: cvgB => //. + by rewrite -derivE; apply: cvgM => //; apply: cvg_at_left_filter; + [exact: continuous_horner|exact: continuous_sin]. + by apply: cvgM => //; apply: cvg_at_left_filter; + [exact: continuous_horner|exact: continuous_cos]. +- by move=> x x0pi; rewrite fsin_antiderivative. +Qed. + +Hypothesis piratE : pirat = pi. + +Lemma intfsin_int n : intfsin n \is a Num.int. +Proof. by rewrite intfsinE rpredD ?F0_int -?piratE ?FPi_int. Qed. + +Let f0 x : (f 0).[x] = 1. +Proof. by rewrite /f /pi_irrational.f fact0 !expr0 invr1 mulr1 !hornerE. Qed. + +Let fsin_bounded n (x : R) : (0 < n)%N -> 0 < x < pi -> + 0 < fsin n x < (pi ^+ n * a ^+ n) / n`!%:R. +Proof. +move=> n0 /andP[x0 xpi]. +have sinx0 : 0 < sin x by rewrite sin_gt0_pi// x0. +apply/andP; split. + rewrite mulr_gt0// /f !hornerE/= mulr_gt0//. + by rewrite mulr_gt0 ?invr_gt0 ?ltr0n ?fact_gt0// exprn_gt0. + by rewrite exprn_gt0// abx_gt0// x0 piratE. +rewrite /fsin !hornerE/= -2!mulrA mulrC ltr_pM2r ?invr_gt0 ?ltr0n ?fact_gt0//. +rewrite -!exprMn [in ltRHS]mulrC mulrA -exprMn. +have ? : 0 <= a - b * x by rewrite abx_ge0 ?piratE// (ltW x0) ltW. +have ? : x * (a - b * x) < a * pi. + rewrite [ltRHS]mulrC ltr_pM//; first exact/ltW. + by rewrite ltrBlDl //ltrDr mulr_gt0// lt0r /b pnatr_eq0 nb0/=. +have := sin_le1 x; rewrite le_eqVlt => /predU1P[x1|x1]. +- by rewrite x1 mulr1 ltrXn2r ?gtn_eqF// mulr_ge0//; exact/ltW. +- rewrite -[ltRHS]mulr1 ltr_pM//. + + by rewrite exprn_ge0// mulr_ge0//; exact/ltW. + + exact/ltW. + + by rewrite ltrXn2r ?gtn_eqF// mulr_ge0//; exact/ltW. +Qed. + +Let intsin : (\int[mu]_(x in `[0%R, pi]) (sin x)%:E = 2%:E)%E. +Proof. +rewrite (@continuous_FTC2 _ _ (- cos)) ?pi_gt0//. +- by rewrite /= !EFinN cos0 cospi !EFinN oppeK. +- exact/continuous_subspaceT/continuous_sin. +- split. + + by move=> x x0pi; exact/derivableN/derivable_cos. + + by apply: cvgN; apply: cvg_at_right_filter; exact: continuous_cos. + + by apply: cvgN; apply: cvg_at_left_filter; exact: continuous_cos. + + by move=> x x0pi; rewrite derive1E deriveN// derive_val opprK. +Qed. + +Let integrable_fsin n : mu.-integrable `[0%R, pi] (EFin \o fsin n). +Proof. +apply: continuous_compact_integrable; first exact: segment_compact. +exact: cfsin. +Qed. + +Let small_ballS (m : R := pi / 2) (d := pi / 4) : + closed_ball m d `<=` `]0%R, pi[. +Proof. +move=> z; rewrite closed_ball_itv/=; last by rewrite divr_gt0// pi_gt0. +rewrite in_itv/= => /andP[mdz zmd]; rewrite in_itv/=; apply/andP; split. + rewrite (lt_le_trans _ mdz)// subr_gt0. + by rewrite ltr_pM2l// ?pi_gt0// ltf_pV2// ?posrE// ltr_nat. +rewrite (le_lt_trans zmd)// -mulrDr gtr_pMr// ?pi_gt0//. +by rewrite -ltrBrDl [X in _ < X - _](splitr 1) div1r addrK ltf_pV2 ?posrE// ltr_nat. +(* that would be immediate with lra... *) +Qed. + +Let min_fsin (m : R := pi / 2) (d := pi / 4) n : (0 < n)%N -> + exists2 r : R, 0 < r & forall x, x \in closed_ball m d -> r <= fsin n x. +Proof. +move=> n0; have mdmd : m - d <= m + d. + by rewrite lerBlDr -addrA lerDl -mulr2n mulrn_wge0// divr_ge0// pi_ge0. +have cf : {within `[m - d, m + d], continuous (fsin n)}. + exact: cfsin. +have [c cmd Hc] := @EVT_min R (fsin n) _ _ mdmd cf. +exists (fsin n c). + have /(_ _)/andP[]// := @fsin_bounded n c n0. + have := @small_ballS c; rewrite /=in_itv/=; apply. + by rewrite closed_ball_itv//= divr_gt0// pi_gt0. +move=> x /set_mem; rewrite closed_ball_itv//=; first exact: Hc. +by rewrite divr_gt0// pi_gt0. +Qed. + +Lemma intfsin_gt0 n : 0 < intfsin n. +Proof. +rewrite fine_gt0//; have [->|n0] := eqVneq n 0. + rewrite /fsin; under eq_integral do rewrite f0 mul1r. + by rewrite intsin ltry andbT. +have fsin_ge0 (x : R) : 0 <= x <= pi -> (0 <= (fsin n x)%:E)%E. + move=> /andP[x0 xpi]; rewrite lee_fin mulr_ge0//. + rewrite !hornerE mulr_ge0//=. + by rewrite mulr_ge0// exprn_ge0. + by rewrite exprn_ge0// abx_ge0// piratE x0. + by rewrite sin_ge0_pi// x0. +apply/andP; split. + rewrite -lt0n in n0. + have [r r0] := @min_fsin _ n0. + pose m : R := pi / 2; pose d : R := pi / 4 => rn. + apply: (@lt_le_trans _ _ (\int[mu]_(x in closed_ball m d) r%:E))%E. + rewrite integral_cst//=; last exact: measurable_closed_ball. + rewrite mule_gt0// lebesgue_measure_closed_ball//. + by rewrite lte_fin mulrn_wgt0// divr_gt0// pi_gt0. + by rewrite divr_ge0// pi_ge0. + apply: (@le_trans _ _ (\int[mu]_(x in (closed_ball m d)) (fsin n x)%:E))%E. + apply: ge0_le_integral => //=. + - exact: measurable_closed_ball. + - by move=> x _; rewrite lee_fin ltW. + - move=> x /small_ballS/= /[!in_itv]/= /andP[x0 xpi]. + by rewrite fsin_ge0// (ltW x0)/= ltW. + - case/integrableP : (integrable_fsin n) => + _. + apply: measurable_funS => // x ix. + exact: subset_itv_oo_cc (small_ballS ix). + - by move=> x /mem_set /rn; rewrite lee_fin. + apply: ge0_subset_integral => //=. + - exact: measurable_closed_ball. + - by case/integrableP : (integrable_fsin n). + - by move=> x ix; exact: subset_itv_oo_cc (small_ballS ix). +case/integrableP : (integrable_fsin n) => ? /=. +apply: le_lt_trans; apply: ge0_le_integral => //=. +- apply/measurable_EFinP => /=; apply/measurableT_comp => //. + exact/measurable_EFinP. +- by move=> x x0pi; rewrite lee_fin ler_norm. +Qed. + +Lemma intfsin_small (e : R) : 0 < e -> \forall n \near \oo, 0 < intfsin n < e. +Proof. +move=> e0; near=> n. +rewrite intfsin_gt0/=. +apply: (@le_lt_trans _ _ + (\int[mu]_(x in `[0, pi]) ((pi ^+ n * a ^+ n) / n`!%:R))). + apply: le_Rintegral => //=. + - apply/continuous_compact_integrable; first exact: segment_compact. + by apply/continuous_subspaceT => x; exact: cvg_cst. + - move=> x. + have ? : 0 <= pi ^+ n * a ^+ n / n`!%:R :> R. + by rewrite mulr_ge0// mulr_ge0// exprn_ge0// pi_ge0. + rewrite in_itv/= => /andP[]. + rewrite le_eqVlt => /predU1P[<- _|x0]; first by rewrite /fsin sin0 !hornerE. + rewrite le_eqVlt => /predU1P[->|xpi]; first by rewrite /fsin sinpi mulr0. + have n0 : (0 < n)%N by near: n; exists 1%N. + have /(_ _)/andP[|//] := @fsin_bounded _ x n0. + + by rewrite x0. + + by move=> _ /ltW. +rewrite Rintegral_cst//= lebesgue_measure_itv/= lte_fin pi_gt0/=. +rewrite subr0 mulrAC -exprMn (mulrC _ pi) -mulrA. +near: n. +have : pi * (pi * a) ^+ n / n`!%:R @[n --> \oo] --> (0:R). + rewrite -[X in _ --> X](mulr0 pi). + under eq_fun do rewrite -mulrA. + by apply: cvgMr; exact: exp_fact. +move/cvgrPdist_lt => /(_ e e0)[k _]H. +near=> n. +have {H} := H n. +rewrite sub0r normrN ger0_norm; last first. + by rewrite !mulr_ge0 ?pi_ge0// exprn_ge0// mulr_ge0// pi_ge0. +rewrite mulrA; apply. +by near: n; exists k. +Unshelve. all: by end_near. Qed. + +End analytic_part. + +End pi_irrational. + +Lemma pi_irrationnal {R : realType} : ~ rational (pi : R). +Proof. +move=> [a [b]]; have [->|b0 piratE] := eqVneq b O. + by rewrite invr0 mulr0; apply/eqP; rewrite gt_eqF// pi_gt0. +have [N _] := pi_irrational.intfsin_small b0 (esym piratE) (@ltr01 R). +near \oo%classic => n. +have Nn : (N <= n)%N by near: n; exists N. +have := @pi_irrational.intfsin_int R _ _ b0 (esym piratE) n. +rewrite intrEge0; last by rewrite ltW// pi_irrational.intfsin_gt0. +move=> + /(_ n Nn). +move/natrP => [k] ->. +rewrite ltr0n ltrn1. +by case: k. +Unshelve. all: by end_near. Qed. diff --git a/theories/probability.v b/theories/probability.v index 11f4d758c4..1ff17ee469 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -594,8 +594,9 @@ have h (Y : {RV P >-> R}) : - by move=> r _; exact: sqr_ge0. - move=> x y; rewrite !nnegrE => x0 y0. by rewrite ler_sqr. - apply: expectation_le => //. + apply: expectation_le. - by apply: measurableT_comp => //; exact: measurableT_comp. + - by []. - by move=> x /=; exact: sqr_ge0. - by move=> x /=; exact: sqr_ge0. - by apply/aeW => t /=; rewrite real_normK// num_real. diff --git a/theories/realfun.v b/theories/realfun.v index a9764f421f..610ed1ed53 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -41,7 +41,6 @@ From mathcomp Require Import sequences real_interval. (* lime_sup f a/lime_inf f a == limit sup/inferior of the extended real- *) (* valued function f at point a *) (* ``` *) -(* *) (******************************************************************************) Set Implicit Arguments. @@ -2454,7 +2453,7 @@ case=> ? [l + <- <-]; rewrite -/(total_variation x b f). move: l => [|i j]. by move=> /itv_partition_nil /eqP; rewrite lt_eqF. move=> [/= /andP[xi ij /eqP ijb]] tv_eps. -apply: filter_app (nbhs_right_ge _). +apply: (filter_app _ _ (nbhs_right_ge _)). apply: filter_app (nbhs_right_lt xi). have e20 : 0 < eps%:num / 2 by []. move/cvgrPdist_lt/(_ (eps%:num/2) e20) : ctsf; apply: filter_app. @@ -2552,7 +2551,7 @@ have /near_eq_cvg/cvg_trans : {near (- x)^'+, (fun t => fine (TV (- b) (- a) (f \o -%R)) - fine (TV (- b) t (f \o -%R))) =1 (fine \o (TV a)^~ f) \o -%R}. apply: filter_app (nbhs_right_lt xa). - apply: filter_app (nbhs_right_ge _). + apply: (filter_app _ _ (nbhs_right_ge _)). near=> t => xt ta; have ? : -b <= t by exact: (le_trans bx). have ? : t <= -a by exact: ltW. apply/eqP; rewrite eq_sym -subr_eq opprK addrC. diff --git a/theories/sequences.v b/theories/sequences.v index 285fb6255c..e520f2c9a1 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -951,13 +951,15 @@ rewrite -(subrr (limn (series u_))). by apply: cvgB => //; rewrite ?cvg_shiftS. Qed. -Lemma nondecreasing_series (R : numFieldType) (u_ : R ^nat) (P : pred nat) : - (forall n, P n -> 0 <= u_ n)%R -> - nondecreasing_seq (fun n=> \sum_(0 <= k < n | P k) u_ k)%R. +Lemma nondecreasing_series (R : numFieldType) (u_ : R ^nat) (P : pred nat) m : + (forall n, (m <= n)%N -> P n -> 0 <= u_ n)%R -> + nondecreasing_seq (fun n=> \sum_(m <= k < n | P k) u_ k)%R. Proof. move=> u_ge0; apply/nondecreasing_seqP => n. -rewrite [in leRHS]big_mkcond [in leRHS]big_nat_recr//=. -by rewrite -[in leRHS]big_mkcond/= lerDl; case: ifPn => //; exact: u_ge0. +have [mn|nm] := leqP m n. + rewrite [leRHS]big_mkcond/= [leRHS]big_nat_recr//=. + by rewrite -[in leRHS]big_mkcond/= lerDl; case: ifPn => //; exact: u_ge0. +by rewrite (big_geq (ltnW _)) // big_geq. Qed. Lemma increasing_series (R : numFieldType) (u_ : R ^nat) : @@ -1546,9 +1548,9 @@ Proof. by move=> ?; apply/cvg_ex; eexists; apply: ereal_nonincreasing_cvgn. Qed. (* NB: see also nondecreasing_series *) Lemma ereal_nondecreasing_series (R : realDomainType) (u_ : (\bar R)^nat) - (P : pred nat) : (forall n, P n -> 0 <= u_ n) -> - nondecreasing_seq (fun n => \sum_(0 <= i < n | P i) u_ i). -Proof. by move=> u_ge0 n m nm; rewrite lee_sum_nneg_natr// => k _ /u_ge0. Qed. + (P : pred nat) N : (forall n, (N <= n)%N -> P n -> 0 <= u_ n) -> + nondecreasing_seq (fun n => \sum_(N <= i < n | P i) u_ i). +Proof. by move=> u_ge0 n m nm; rewrite lee_sum_nneg_natr. Qed. Lemma congr_lim (R : numFieldType) (f g : nat -> \bar R) : f = g -> limn f = limn g. @@ -1558,12 +1560,14 @@ Lemma eseries_cond {R : numFieldType} (f : (\bar R)^nat) P N : \sum_(N <= i n /=; apply: big_nat_widenl. Qed. -Lemma eseries_mkcondl {R : numFieldType} (f : (\bar R)^nat) P Q : - \sum_(i n; rewrite big_mkcondl. Qed. -Lemma eseries_mkcondr {R : numFieldType} (f : (\bar R)^nat) P Q : - \sum_(i n; rewrite big_mkcondr. Qed. Lemma eq_eseriesr (R : numFieldType) (f g : (\bar R)^nat) (P : pred nat) {N} : @@ -1571,8 +1575,8 @@ Lemma eq_eseriesr (R : numFieldType) (f g : (\bar R)^nat) (P : pred nat) {N} : \sum_(N <= i efg; apply/congr_lim/funext => n; exact: eq_bigr. Qed. -Lemma eq_eseriesl (R : realFieldType) (P Q : pred nat) (f : (\bar R)^nat) : - P =1 Q -> \sum_(i \sum_(N <= i efg; apply/congr_lim/funext => n; apply: eq_bigl. Qed. Arguments eq_eseriesl {R P} Q. @@ -1617,9 +1621,9 @@ Qed. End ereal_series. -Lemma nneseries_lim_ge (R : realType) (u_ : (\bar R)^nat) (P : pred nat) k : - (forall n, P n -> 0 <= u_ n) -> - \sum_(0 <= i < k | P i) u_ i <= \sum_(i P n -> 0 <= u_ n) -> + \sum_(m <= i < k | P i) u_ i <= \sum_(m <= i -> //. by apply: ereal_sup_ubound; exists k. @@ -1663,36 +1667,36 @@ Lemma is_cvg_ereal_npos_natsum m : (forall n, (m <= n)%N -> u_ n <= 0) -> cvgn (fun n => \sum_(m <= i < n) u_ i). Proof. by move=> u_le0; apply: is_cvg_ereal_npos_natsum_cond => n /u_le0. Qed. -Lemma is_cvg_nneseries_cond P N : (forall n, P n -> 0 <= u_ n) -> +Lemma is_cvg_nneseries_cond P N : (forall n, (N <= n)%N -> P n -> 0 <= u_ n) -> cvgn (fun n => \sum_(N <= i < n | P i) u_ i). Proof. -by move=> u_ge0; apply: is_cvg_ereal_nneg_natsum_cond => n _; exact: u_ge0. +by move=> u_ge0; apply: is_cvg_ereal_nneg_natsum_cond => n Nn; exact: u_ge0. Qed. -Lemma is_cvg_npeseries_cond P N : (forall n, P n -> u_ n <= 0) -> +Lemma is_cvg_npeseries_cond P N : (forall n, (N <= n)%N -> P n -> u_ n <= 0) -> cvgn (fun n => \sum_(N <= i < n | P i) u_ i). -Proof. by move=> u_le0; apply: is_cvg_ereal_npos_natsum_cond => n _ /u_le0. Qed. +Proof. by move=> u_le0; exact: is_cvg_ereal_npos_natsum_cond. Qed. -Lemma is_cvg_nneseries P N : (forall n, P n -> 0 <= u_ n) -> +Lemma is_cvg_nneseries P N : (forall n, (N <= n)%N -> P n -> 0 <= u_ n) -> cvgn (fun n => \sum_(N <= i < n | P i) u_ i). Proof. by move=> ?; exact: is_cvg_nneseries_cond. Qed. -Lemma is_cvg_npeseries P N : (forall n, P n -> u_ n <= 0) -> +Lemma is_cvg_npeseries P N : (forall n, (N <= n)%N -> P n -> u_ n <= 0) -> cvgn (fun n => \sum_(N <= i < n | P i) u_ i). Proof. by move=> ?; exact: is_cvg_npeseries_cond. Qed. -Lemma nneseries_ge0 P N : (forall n, P n -> 0 <= u_ n) -> +Lemma nneseries_ge0 P N : (forall n, (N <= n)%N -> P n -> 0 <= u_ n) -> 0 <= \sum_(N <= i u0; apply: (lime_ge (is_cvg_nneseries u0)). -by apply: nearW => k; rewrite sume_ge0. +move=> u0; apply: (lime_ge (is_cvg_nneseries u0)); apply: nearW => k. +by rewrite big_nat_cond sume_ge0// => n /andP[/andP[+ _]]; exact: u0. Qed. -Lemma npeseries_le0 P N : (forall n : nat, P n -> u_ n <= 0) -> +Lemma npeseries_le0 P N : (forall n : nat, (N <= n)%N -> P n -> u_ n <= 0) -> \sum_(N <= i u0; apply: (lime_le (is_cvg_npeseries u0)). -by apply: nearW => k; rewrite sume_le0. +move=> u0; apply: (lime_le (is_cvg_npeseries u0)); apply: nearW => k. +by rewrite big_nat_cond sume_le0// => n /andP[/andP[+ _]]; exact: u0. Qed. End cvg_eseries. @@ -1718,32 +1722,21 @@ Lemma nneseriesZl (R : realType) (f : nat -> \bar R) (P : pred nat) x N : (forall i, P i -> 0 <= f i) -> (\sum_(N <= i f0; rewrite -limeMl//; last exact: is_cvg_nneseries. +move=> f0; rewrite -limeMl//; last by apply: is_cvg_nneseries => n _; exact: f0. by apply/congr_lim/funext => /= n; rewrite ge0_sume_distrr. Qed. Lemma adde_def_nneseries (R : realType) (f g : (\bar R)^nat) - (P Q : pred nat) : - (forall n, P n -> 0 <= f n) -> (forall n, Q n -> 0 <= g n) -> - (\sum_(i P n -> 0 <= f n) -> + (forall n, (m <= n)%N -> Q n -> 0 <= g n) -> + (\sum_(m <= i f0 g0; rewrite /adde_def !negb_and; apply/andP; split; apply/orP. -- by right; apply/eqP => Qg; have := nneseries_ge0 0 g0; rewrite Qg. -- by left; apply/eqP => Pf; have := nneseries_ge0 0 f0; rewrite Pf. +- by right; apply/eqP => Qg; have := nneseries_ge0 m g0; rewrite Qg. +- by left; apply/eqP => Pf; have := nneseries_ge0 m f0; rewrite Pf. Qed. -Lemma __deprecated__ereal_cvgPpinfty (R : realFieldType) (u_ : (\bar R)^nat) : - u_ @ \oo --> +oo <-> (forall A, (0 < A)%R -> \forall n \near \oo, A%:E <= u_ n). -Proof. -by split=> [/cvgeyPge//|u_ge]; apply/cvgeyPgey; near=> x; apply: u_ge. -Unshelve. all: by end_near. Qed. - -Lemma __deprecated__ereal_cvgPninfty (R : realFieldType) (u_ : (\bar R)^nat) : - u_ @ \oo --> -oo <-> (forall A, (A < 0)%R -> \forall n \near \oo, u_ n <= A%:E). -Proof. -by split=> [/cvgeNyPle//|u_ge]; apply/cvgeNyPleNy; near=> x; apply: u_ge. -Unshelve. all: by end_near. Qed. - Lemma __deprecated__ereal_squeeze (R : realType) (f g h : (\bar R)^nat) : (\forall x \near \oo, f x <= g x <= h x) -> forall (l : \bar R), f @ \oo --> l -> h @ \oo --> l -> g @ \oo --> l. @@ -1758,13 +1751,13 @@ by rewrite gt_eqF// (lt_le_trans _ (u_ge0 _ Pn)). Qed. Lemma lee_nneseries (R : realType) (u v : (\bar R)^nat) (P : pred nat) N : - (forall i, P i -> 0 <= u i) -> + (forall i, (N <= i)%N -> P i -> 0 <= u i) -> (forall n, P n -> u n <= v n) -> \sum_(N <= i u0 Puv; apply: lee_lim. -- by apply: is_cvg_ereal_nneg_natsum_cond => n ? /u0; exact. -- apply: is_cvg_ereal_nneg_natsum_cond => n _ Pn. +- by apply: is_cvg_ereal_nneg_natsum_cond => n Nn /u0; exact. +- apply: is_cvg_ereal_nneg_natsum_cond => n Nn Pn. by rewrite (le_trans _ (Puv _ Pn))// u0. - by near=> n; apply: lee_sum => k; exact: Puv. Unshelve. all: by end_near. Qed. @@ -1777,9 +1770,9 @@ Lemma subset_lee_nneseries (R : realType) (u : (\bar R)^nat) (P Q : pred nat) Proof. move=> Pu PQ; apply: lee_lim. - apply: ereal_nondecreasing_is_cvgn => a b ab. - by apply: lee_sum_nneg_natr => // n Mn /PQ; exact: Pu. + by apply: lee_sum_nneg_natr => // n Mn Pn; apply: Pu => //; exact: PQ. - apply: ereal_nondecreasing_is_cvgn => a b ab. - by apply: lee_sum_nneg_natr => // n Mn; exact: Pu. + by apply: lee_sum_nneg_natr => // n Mn Pn; apply: Pu => //; exact: PQ. - near=> n; apply: lee_sum_nneg_subset => //. by move=> i; rewrite inE => /andP[iP iQ]; exact: Pu. Unshelve. all: by end_near. Qed. @@ -1951,7 +1944,8 @@ have : cvg (\sum_(0 <= k < n | P k) f k @[n --> \oo]). by apply: lee_sum_nneg_natr => n _; exact: f0. move/cvg_ex => [[l fl||/cvg_lim fnoo]] /=; last 2 first. - by move/cvg_lim => fpoo; rewrite fpoo// in foo. - - have : 0 <= \sum_(k n _; exact: f0. by rewrite fnoo. rewrite [X in X @ _ --> _](_ : _ = fun N => l%:E - \sum_(0 <= k < N | P k) f k). apply/cvgeNP; rewrite oppe0. @@ -1959,38 +1953,42 @@ rewrite [X in X @ _ --> _](_ : _ = fun N => l%:E - \sum_(0 <= k < N | P k) f k). exact/cvge_sub0. apply/funext => N; apply/esym/eqP; rewrite sube_eq//. by rewrite addeC -nneseries_split_cond//; exact/eqP/esym/cvg_lim. -by rewrite ge0_adde_def//= ?inE; [exact: nneseries_ge0|exact: sume_ge0]. +rewrite ge0_adde_def//= ?inE; last exact: sume_ge0. +by apply: nneseries_ge0 => n Nn; exact: f0. Qed. -Lemma nneseriesD (R : realType) (f g : nat -> \bar R) (P : pred nat) : - (forall i, P i -> 0 <= f i) -> (forall i, P i -> 0 <= g i) -> - \sum_(i \bar R) (P : pred nat) N : + (forall i, (N <= i)%N -> P i -> 0 <= f i) -> + (forall i, (N <= i)%N -> P i -> 0 <= g i) -> + \sum_(N <= i f_eq0 g_eq0. -transitivity (limn (fun n => \sum_(0 <= i < n | P i) f i + - \sum_(0 <= i < n | P i) g i)). +transitivity (limn (fun n => \sum_(N <= i < n | P i) f i + + \sum_(N <= i < n | P i) g i)). by apply/congr_lim/funext => n; rewrite big_split. rewrite limeD /adde_def //=; do ? exact: is_cvg_nneseries. by rewrite ![_ == -oo]gt_eqF ?andbF// (@lt_le_trans _ _ 0) ?[_ < _]real0// nneseries_ge0. Qed. -Lemma nneseries_sum_nat (R : realType) n (f : nat -> nat -> \bar R) : +Lemma nneseries_sum_nat (R : realType) m n (f : nat -> nat -> \bar R) N : (forall i j, 0 <= f i j) -> - \sum_(j f0; elim: n => [|n IHn]. +move=> f0; elim: n => [|n ih]. by rewrite big_geq// eseries0// => i; rewrite big_geq. -rewrite big_nat_recr// -IHn/= -nneseriesD//; last by move=> i; rewrite sume_ge0. -by apply/congr_lim/funext => m; apply: eq_bigr => i _; rewrite big_nat_recr. +have [mn|nm] := leqP m n. + rewrite big_nat_recr// -ih/= -nneseriesD//; last by move=> i; rewrite sume_ge0. + by apply/congr_lim/funext => ?; apply: eq_bigr => i _; rewrite big_nat_recr. +by rewrite big_geq// eseries0// => i; rewrite big_geq. Qed. Lemma nneseries_sum I (r : seq I) (P : {pred I}) [R : realType] - [f : I -> nat -> \bar R] : (forall i j, P i -> 0 <= f i j) -> - \sum_(j nat -> \bar R] N : (forall i j, P i -> 0 <= f i j) -> + \sum_(N <= j f_ge0; case Dr : r => [|i r']; rewrite -?{}[_ :: _]Dr. by rewrite big_nil eseries0// => i; rewrite big_nil. @@ -2026,12 +2024,6 @@ by move/(lt_le_trans Ml); rewrite ltxx. Unshelve. all: by end_near. Qed. End sequences_ereal. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="use `cvgeyPge` or a variant instead")] -Notation ereal_cvgPpinfty := __deprecated__ereal_cvgPpinfty (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", - note="use `cvgeNyPle` or a variant instead")] -Notation ereal_cvgPninfty := __deprecated__ereal_cvgPninfty (only parsing). #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `squeeze_cvge` and generalized")] Notation ereal_squeeze := __deprecated__ereal_squeeze (only parsing). @@ -2099,12 +2091,6 @@ Notation ereal_nonincreasing_cvg := ereal_nonincreasing_cvgn (only parsing). #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `ereal_nonincreasing_is_cvgn`")] Notation ereal_nonincreasing_is_cvg := ereal_nonincreasing_is_cvgn (only parsing). -#[deprecated(since="analysis 0.6.0", note="Use eseries0 instead.")] -Notation nneseries0 := eseries0 (only parsing). -#[deprecated(since="analysis 0.6.0", note="Use eq_eseriesr instead.")] -Notation eq_nneseries := eq_eseriesr (only parsing). -#[deprecated(since="analysis 0.6.0", note="Use eseries_pred0 instead.")] -Notation nneseries_pred0 := eseries_pred0 (only parsing). Arguments nneseries_split {R f} _ _. diff --git a/theories/trigo.v b/theories/trigo.v index 5da3ff7cee..18735a73a4 100644 --- a/theories/trigo.v +++ b/theories/trigo.v @@ -482,7 +482,7 @@ rewrite -seriesN lt_sum_lim_series //. move=> d. rewrite /cos_coeff' 2!exprzD_nat (exprSz _ d.*2) -[in (-1) ^ d.*2](muln2 d). rewrite -(exprnP _ (d * 2)) (exprM (-1)) sqrr_sign 2!mulr1 -exprSzr. -rewrite (_ : 4 = 2 * 2)%N // -(exprnP _ (2 * 2)) (exprM (-1)) sqrr_sign. +rewrite -[4%Z]/(_ (2 * 2))%N -(exprnP _ (2 * 2)) (exprM (-1)) sqrr_sign. rewrite mul1r [(-1) ^ 3](_ : _ = -1) ?mulN1r ?mulNr ?opprK; last first. by rewrite -exprnP 2!exprS expr1 mulrN1 opprK mulr1. rewrite subr_gt0.