From 32abf24e48eafeca061a69f2d769505656bf1447 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 13 May 2024 17:31:35 +0900 Subject: [PATCH 1/3] FTC1 corollary Co-authored-by: Zachary Stone --- CHANGELOG_UNRELEASED.md | 54 +++++ classical/classical_sets.v | 33 +-- classical/set_interval.v | 6 + theories/charge.v | 244 +++++++++++++++++++++- theories/ereal.v | 11 + theories/ftc.v | 278 +++++++++++++++++++++++++- theories/lebesgue_integral.v | 378 +++++++++++++++++++---------------- theories/lebesgue_measure.v | 4 +- theories/measure.v | 82 ++++++-- theories/normedtype.v | 6 + theories/numfun.v | 32 ++- 11 files changed, 914 insertions(+), 214 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 6ebeba83c3..4c50968597 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -52,6 +52,54 @@ + lemmas `subspace_pm_ball_center`, `subspace_pm_ball_sym`, `subspace_pm_ball_triangle`, `subspace_pm_entourage` turned into local `Let`'s +- in `classical_sets.v`: + + lemmas `setC_I`, `bigcup_subset` + +- in `set_interval.v`: + + lemma `interval_set1` + +- in `normedtype.v`: + + lemma `nbhs_right_ltDr` + +- in `numfun.v`: + + lemma `epatch_indic` + + lemma `restrict_normr` + + lemmas `funepos_le`, `funeneg_le` + +- in `ereal.v`: + + lemmas `restrict_EFin` + +- in `measure.v`: + + definition `lim_sup_set` + + lemmas `lim_sup_set_ub`, `lim_sup_set_cvg`, `lim_sup_set_cvg0` + +- in `lebesgue_integral.v`: + + lemma `integral_Sset1` + + lemma `integralEpatch` + + lemma `integrable_restrict` + + lemma `le_integral` + + lemma `null_set_integral` + + lemma `EFin_normr_Rintegral` + +- in `charge.v`: + + definition `charge_variation` + + lemmas `abse_charge_variation`, `charge_variation_continuous` + + definition `induced` + + lemmas `semi_sigma_additive_nng_induced`, `dominates_induced`, `integral_normr_continuous` + +- in `ftc.v`: + + definition `indefinite_integral` + + lemmas `indefinite_integral_near_left`, + `indefinite_integral_cvg_left`, `indefinite_integral_cvg_at_left` + + corollary `continuous_FTC2` + +### Changed + +- in `lebesgue_integral.v`: + + lemma `measurable_int`: argument `mu` now explicit + +- moved from `lebesgue_integral.v` to `ereal.v`: + + lemma `funID` - in `reals.v`: + definitions `Rceil`, `Rfloor` @@ -94,6 +142,8 @@ + `lee_ndivr_mull` -> `lee_ndivrMl` + `lee_ndivr_mulr` -> `lee_ndivrMr` + `eqe_pdivr_mull` -> `eqe_pdivrMl` +- in `measure.v`: + + `measurable_restrict` -> `measurable_restrictT` - in `ftc.v`: + `FTC1` -> `FTC1_lebesgue_pt` @@ -142,6 +192,8 @@ - in `constructive_ereal.v`: + lemmas `leeN2`, `lteN2` generalized from `realDomainType` to `numDomainType` +- in `measure.v`: + + lemma `measurable_restrict` ### Deprecated @@ -149,6 +201,8 @@ + `floor_le` (use `ge_floor` instead) + `le_floor` (use `Num.Theory.floor_le` instead) + `le_ceil` (use `ceil_ge` instead) +- in `lebesgue_integral.v`: + + lemmas `integralEindic`, `integral_setI_indic` - in `constructive_ereal.v`: + lemmas `lte_opp2`, `lee_opp2` (use `lteN2`, `leeN2` instead) diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 90d18a5156..3336927866 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -248,18 +248,24 @@ Reserved Notation "A `\ b" (at level 50, left associativity). Reserved Notation "A `+` B" (at level 54, left associativity). Reserved Notation "A +` B" (at level 54, left associativity). *) -Reserved Notation "\bigcup_ ( i 'in' P ) F" - (at level 41, F at level 41, i, P at level 50, - format "'[' \bigcup_ ( i 'in' P ) '/ ' F ']'"). -Reserved Notation "\bigcup_ ( i : T ) F" - (at level 41, F at level 41, i at level 50, - format "'[' \bigcup_ ( i : T ) '/ ' F ']'"). Reserved Notation "\bigcup_ ( i < n ) F" (at level 41, F at level 41, i, n at level 50, format "'[' \bigcup_ ( i < n ) '/ ' F ']'"). Reserved Notation "\bigcup_ ( i >= n ) F" (at level 41, F at level 41, i, n at level 50, format "'[' \bigcup_ ( i >= n ) '/ ' F ']'"). +Reserved Notation "\bigcap_ ( i < n ) F" + (at level 41, F at level 41, i, n at level 50, + format "'[' \bigcap_ ( i < n ) '/ ' F ']'"). +Reserved Notation "\bigcap_ ( i >= n ) F" + (at level 41, F at level 41, i, n at level 50, + format "'[' \bigcap_ ( i >= n ) '/ ' F ']'"). +Reserved Notation "\bigcup_ ( i 'in' P ) F" + (at level 41, F at level 41, i, P at level 50, + format "'[' \bigcup_ ( i 'in' P ) '/ ' F ']'"). +Reserved Notation "\bigcup_ ( i : T ) F" + (at level 41, F at level 41, i at level 50, + format "'[' \bigcup_ ( i : T ) '/ ' F ']'"). Reserved Notation "\bigcup_ i F" (at level 41, F at level 41, i at level 0, format "'[' \bigcup_ i '/ ' F ']'"). @@ -269,12 +275,6 @@ Reserved Notation "\bigcap_ ( i 'in' P ) F" Reserved Notation "\bigcap_ ( i : T ) F" (at level 41, F at level 41, i at level 50, format "'[' \bigcap_ ( i : T ) '/ ' F ']'"). -Reserved Notation "\bigcap_ ( i < n ) F" - (at level 41, F at level 41, i, n at level 50, - format "'[' \bigcap_ ( i < n ) '/ ' F ']'"). -Reserved Notation "\bigcap_ ( i >= n ) F" - (at level 41, F at level 41, i, n at level 50, - format "'[' \bigcap_ ( i >= n ) '/ ' F ']'"). Reserved Notation "\bigcap_ i F" (at level 41, F at level 41, i at level 0, format "'[' \bigcap_ i '/ ' F ']'"). @@ -1207,6 +1207,11 @@ Proof. by move=> k; apply/val_inj. Qed. Lemma IIordK {n} : cancel (@IIord n) ordII. Proof. by move=> k; apply/val_inj. Qed. +Lemma setC_I n : ~` `I_n = [set k | n <= k]. +Proof. +by apply/seteqP; split => [x /negP|x /= nx]; last apply/negP; rewrite -leqNgt. +Qed. + Lemma mem_not_I N n : (n \in ~` `I_N) = (N <= n). Proof. by rewrite in_setC /mkset /in_mem /mem /= /in_set asboolb -leqNgt. Qed. @@ -1937,6 +1942,10 @@ Proof. by move=> FG; apply: bigcup_sub => i Pi + /(FG _ Pi); apply: bigcup_sup. Qed. +Lemma bigcup_subset P Q F : P `<=` Q -> + \bigcup_(i in P) F i `<=` \bigcup_(i in Q) F i. +Proof. by move=> PQ t [i /PQ Qi Fit]; exists i. Qed. + Lemma subset_bigcap P F G : (forall i, P i -> F i `<=` G i) -> \bigcap_(i in P) F i `<=` \bigcap_(i in P) G i. Proof. diff --git a/classical/set_interval.v b/classical/set_interval.v index ae2387d384..549604f8aa 100644 --- a/classical/set_interval.v +++ b/classical/set_interval.v @@ -70,6 +70,12 @@ by move: b0 b1 => [] [] /=; [exact: subset_itv_oo_co|exact: subset_itv_oo_cc| exact: subset_refl|exact: subset_itv_oo_oc]. Qed. +Lemma interval_set1 x : `[x, x]%classic = [set x] :> set T. +Proof. +apply/seteqP; split => [y/=|y <-]; last by rewrite /= in_itv/= lexx. +by rewrite in_itv/= => /andP[yx xy]; apply/eqP; rewrite eq_le yx xy. +Qed. + Lemma set_itvoo x y : `]x, y[%classic = [set z | (x < z < y)%O]. Proof. by []. Qed. diff --git a/theories/charge.v b/theories/charge.v index 9a9c35efd0..743c458d1c 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -51,12 +51,14 @@ Require Import esum measure realfun lebesgue_measure lebesgue_integral. (* hahn_decomposition nu P N == the full set can be decomposed in P and N, *) (* a positive set and a negative set for the *) (* charge nu *) -(* jordan_pos nu nuPN == the charge obtained by restricting the charge *) +(* jordan_pos nuPN == the charge obtained by restricting the charge *) (* nu to the positive set P of the Hahn *) (* decomposition nuPN: hahn_decomposition nu P N *) -(* jordan_neg nu nuPN == the charge obtained by restricting the charge *) +(* jordan_neg nuPN == the charge obtained by restricting the charge *) (* nu to the positive set N of the Hahn *) (* decomposition nuPN: hahn_decomposition nu P N *) +(* charge_variation nuPN == variation of the charge nu *) +(* := jordan_pos nuPN \+ jordan_neg nuPN *) (* 'd nu '/d mu == Radon-Nikodym derivative of nu w.r.t. mu *) (* (the scope is charge_scope) *) (* ``` *) @@ -993,6 +995,228 @@ Qed. End jordan_decomposition. +Section charge_variation. +Context d (T : measurableType d) (R : realType). +Variable nu : {charge set T -> \bar R}. +Variables (P N : set T) (nuPN : hahn_decomposition nu P N). +Local Open Scope ereal_scope. + +Definition charge_variation := jordan_pos nuPN \+ jordan_neg nuPN. + +End charge_variation. + +Section charge_variation. +Context {R : realType} d (T : measurableType d). +Variable nu : {charge set T -> \bar R}. +Variables (P N : set T) (nuPN : hahn_decomposition nu P N). + +Local Notation mu := (charge_variation nuPN). + +Let mu0 : mu set0 = 0. Proof. by rewrite /mu !charge0 add0e. Qed. + +Let mu_ge0 x : (0 <= mu x)%E. Proof. by rewrite adde_ge0. Qed. + +Let mu_sigma_additive : semi_sigma_additive mu. +Proof. +move=> F mF tF mUF; under eq_fun do rewrite big_split; apply: cvgeD => //=. +- by rewrite ge0_adde_def// inE. +- exact: measure_semi_sigma_additive. +- exact: measure_semi_sigma_additive. +Qed. + +HB.instance Definition _ := isMeasure.Build _ _ _ mu + mu0 mu_ge0 mu_sigma_additive. + +Let mu_fin A : d.-measurable A -> mu A \is a fin_num. +Proof. by move=> mA; rewrite /mu fin_numD !fin_num_measure. Qed. + +HB.instance Definition _ := isCharge.Build _ _ _ mu + mu0 mu_fin mu_sigma_additive. + +End charge_variation. + +Lemma abse_charge_variation d (T : measurableType d) (R : realType) + (nu : {charge set T -> \bar R}) P N (PN : hahn_decomposition nu P N) A : + measurable A -> `|nu A| <= charge_variation PN A. +Proof. +move=> mA. +rewrite (jordan_decomp PN mA) /cadd/= /cscale/= mulN1e /charge_variation. +by rewrite (le_trans (lee_abs_sub _ _))// !gee0_abs. +Qed. + +Section charge_variation_continuous. +Local Open Scope ereal_scope. +Context {R : realType} d (T : measurableType d). +Variable nu : {charge set T -> \bar R}. +Variables (P N : set T) (nuPN : hahn_decomposition nu P N). + +Lemma dominates_charge_variation (mu : {measure set T -> \bar R}) : + nu `<< mu -> charge_variation nuPN `<< mu. +Proof. +move=> numu A mA muA0. +rewrite /charge_variation/= (jordan_pos_dominates nuPN numu)// add0e. +by rewrite (jordan_neg_dominates nuPN numu). +Qed. + +Lemma charge_variation_continuous (mu : {measure set T -> \bar R}) : + nu `<< mu -> forall e : R, (0 < e)%R -> + exists d : R, (0 < d)%R /\ + forall A, measurable A -> mu A < d%:E -> charge_variation nuPN A < e%:E. +Proof. +move=> numu; apply/not_forallP => -[e] /not_implyP[e0] /forallNP H. +have {H} : forall n, exists A, + [/\ measurable A, mu A < (2 ^- n.+1)%:E & charge_variation nuPN A >= e%:E]. + move=> n; have /not_andP[|] := H (2 ^- n.+1); first by rewrite invr_gt0. + move=> /existsNP[A] /not_implyP[mA] /not_implyP[Aab] /negP. + by rewrite -leNgt => eint; exists A. +move=> /choice[F /= H]. +have mF i : measurable (F i) by have [] := H i. +have : mu (lim_sup_set F) = 0. + apply: lim_sup_set_cvg0 => //. + have h : \sum_(0 <= n < k) (1 / 2 ^+ n.+1)%:E @[k --> \oo] --> (1 : \bar R). + apply/fine_cvgP; split. + apply: nearW => /= n; rewrite sum_fin_num//. + by apply/allP => /= r /mapP[/= k _] ->. + under eq_fun do rewrite sumEFin. + have := @cvg_geometric_series_half R 1 0; rewrite {1}/series/= expr0 divr1. + by under eq_fun do under eq_bigr do rewrite addn1 natrX. + apply: (@le_lt_trans _ _ (\sum_(0 <= n /= n; apply: lee_sum => i _. + by have [_ /ltW + _] := H i; rewrite div1r. + by move/cvg_lim : h => ->//; rewrite ltry. +have : measurable (lim_sup_set F). + by apply: bigcap_measurable => // k _; exact: bigcup_measurable. +move=> /(dominates_charge_variation numu) /[apply]. +apply/eqP; rewrite neq_lt// ltNge measure_ge0//=. +suff : charge_variation nuPN (lim_sup_set F) >= e%:E by exact: lt_le_trans. +have echarge n : e%:E <= charge_variation nuPN (\bigcup_(j >= n) F j). + have [_ _ /le_trans] := H n; apply. + rewrite le_measure// ?inE//; first exact: bigcup_measurable. + by apply: bigcup_sup => //=. +have /(_ _ _)/cvg_lim <-// := @lim_sup_set_cvg _ _ _ (charge_variation nuPN) F. + apply: lime_ge. + apply: ereal_nonincreasing_is_cvgn => a b ab. + rewrite le_measure ?inE//; [exact: bigcup_measurable| + exact: bigcup_measurable|]. + by apply: bigcup_subset => n/=; exact: leq_trans. + by apply: nearW => k; exact: echarge. +by rewrite -ge0_fin_numE// fin_num_measure//; exact: bigcup_measurable. +Qed. + +End charge_variation_continuous. + +Definition induced d (T : measurableType d) {R : realType} + (mu : {measure set T -> \bar R}) (f : T -> \bar R) + (intf : mu.-integrable [set: T] f) := + fun A => (\int[mu]_(t in A) f t)%E. + +Section induced_charge. +Context d (T : measurableType d) {R : realType} (mu : {measure set T -> \bar R}). +Local Open Scope ereal_scope. + +Lemma semi_sigma_additive_nng_induced (f : T -> \bar R) : + measurable_fun setT f -> (forall x, 0 <= f x) -> + semi_sigma_additive (fun A => \int[mu]_(t in A) f t). +Proof. +move=> mf f0 /= F mF tF mUF; rewrite ge0_integral_bigcup//=; last first. + exact: measurable_funTS. +by apply: is_cvg_ereal_nneg_natsum_cond => // n _ _; exact: integral_ge0. +Qed. + +Variable f : T -> \bar R. +Hypothesis intf : mu.-integrable setT f. + +Local Notation nu := (induced intf). + +Let nu0 : nu set0 = 0. Proof. by rewrite /nu integral_set0. Qed. + +Let finnu A : measurable A -> nu A \is a fin_num. +Proof. +by move=> mA; apply: integral_fune_fin_num => //=; exact: integrableS intf. +Qed. + +Let snu : semi_sigma_additive nu. +Proof. +move=> /= F mF tF mUF; set SF := (f in f n @[n --> \oo] --> _). +rewrite (_ : SF = fun n => + \sum_(0 <= i < n) (\int[mu]_(x in F i) f^\+ x) - + \sum_(0 <= i < n) (\int[mu]_(x in F i) f^\- x)); last first. + apply/funext => n; rewrite /SF; under eq_bigr do rewrite /nu integralE. + rewrite big_split/= sumeN//= => i j _ _. + rewrite fin_num_adde_defl// integral_fune_fin_num//= integrable_funeneg//=. + exact: integrableS intf. +rewrite /nu integralE; apply: cvgeD. +- rewrite fin_num_adde_defr// integral_fune_fin_num//=. + by apply: integrable_funepos => //=; exact: integrableS intf. +- apply/semi_sigma_additive_nng_induced => //. + by apply: measurable_funepos; exact: (measurable_int mu). +- apply/cvgeN/semi_sigma_additive_nng_induced => //=. + by apply: measurable_funeneg; exact: (measurable_int mu). +Qed. + +HB.instance Definition _ := isCharge.Build _ _ _ nu nu0 finnu snu. + +End induced_charge. + +Section dominates_induced. +Context d (T : measurableType d) {R : realType} (mu : {measure set T -> \bar R}). +Local Open Scope ereal_scope. + +Variable f : T -> \bar R. +Hypothesis intf : mu.-integrable setT f. + +Let intnf : mu.-integrable [set: T] (abse \o f). +Proof. exact: integrable_abse. Qed. + +Lemma dominates_induced : induced intnf `<< mu. +Proof. +move=> /= A mA muA. +rewrite /induced; apply/eqP; rewrite -abse_eq0 eq_le abse_ge0 andbT. +rewrite (le_trans (le_abse_integral _ _ _))//=. + by case/integrableP : intnf => /= + _; exact: measurable_funTS. +rewrite le_eqVlt; apply/orP; left; apply/eqP. +under eq_integral do rewrite abse_id. +by apply: null_set_integral => //=; exact: integrableS intnf. +Qed. + +End dominates_induced. + +Section integral_normr_continuous. +Context d (T : measurableType d) {R : realType} (mu : {measure set T -> \bar R}). +Local Open Scope ereal_scope. + +Variable f : T -> R. +Hypothesis intf : mu.-integrable setT (EFin \o f). + +Let intnf : mu.-integrable setT (abse \o EFin \o f). +Proof. exact: integrable_abse. Qed. + +Lemma integral_normr_continuous (e : R) : (0 < e)%R -> + exists d : R, (0 < d)%R /\ + forall A, measurable A -> mu A < d%:E -> (\int[mu]_(x in A) `|f x| < e)%R. +Proof. +move=> e0; have [P [N pn]] := Hahn_decomposition (induced intnf). +have [r [r0 re]] := charge_variation_continuous pn (dominates_induced intf) e0. +exists r; split => //= A mA Ad. +have {re} := re _ mA Ad. +rewrite -lte_fin; apply: le_lt_trans. +rewrite /Rintegral fineK; last first. + have : mu.-integrable A (abse \o EFin \o f) by exact: integrableS intnf. + move/integrableP : intf => -[_ intfoo _]. + rewrite ge0_fin_numE//=; last exact: integral_ge0. + apply: le_lt_trans intfoo. + apply: ge0_subset_integral => //=. + apply: measurableT_comp => //. + by case/integrableP : intnf => /= /EFin_measurable_fun. +rewrite -[leLHS](gee0_abs)//; last exact: integral_ge0. +exact: (le_trans _ (abse_charge_variation _ _)). +Qed. + +End integral_normr_continuous. + (* We put definitions and lemmas used only in the proof of the Radon-Nikodym theorem as Definition's and Lemma's in the following modules. See https://staff.aist.go.jp/reynald.affeldt/documents/measure-ppl2023.pdf @@ -1734,9 +1958,11 @@ rewrite integralZl_indic_nnsfun => //. under eq_integral do rewrite EFinM -muleA. rewrite ge0_integralZl//. - under eq_integral do rewrite muleC. - by rewrite -integral_setI_indic// -f_integral// integral_indic// setIC. + rewrite (eq_integral (g \_ (h n @^-1` [set r]))); last first. + by move=> x xE; rewrite epatch_indic. + by rewrite -integral_mkcondr -f_integral// integral_indic// setIC. - apply: emeasurable_funM; first exact/EFin_measurable_fun. - exact/measurable_funTS/(measurable_int (f_integrable _)). + exact/measurable_funTS/(measurable_int _ (f_integrable _)). - by move=> t Et; rewrite mule_ge0// ?lee_fin//; exact: f_ge0. - by move: rhn; rewrite inE => -[t _ <-]; rewrite lee_fin. Qed. @@ -1745,13 +1971,13 @@ Lemma integrableM f E : (forall x, 0 <= f x) -> measurable E -> nu.-integrable E f -> mu.-integrable E (f \* 'd nu '/d mu). Proof. move=> f0 mE intEf; apply/integrableP; split. - apply: emeasurable_funM; first exact: (@measurable_int _ _ _ nu). - exact/measurable_funTS/(measurable_int (f_integrable _)). + apply: emeasurable_funM; first exact: (measurable_int nu). + exact/measurable_funTS/(measurable_int _ (f_integrable _)). under eq_integral. move=> x _; rewrite gee0_abs; last first. by apply: mule_ge0=> //; exact: f_ge0. over. -rewrite change_of_variables//; last exact: (@measurable_int _ _ _ nu). +rewrite change_of_variables//; last exact: (measurable_int nu). by move/integrableP : intEf=> [mf +]; under eq_integral do rewrite gee0_abs//. Qed. @@ -1770,14 +1996,14 @@ Lemma chain_rule E : nu `<< mu -> mu `<< la -> measurable E -> Proof. move=> numu mula mE; have nula := measure_dominates_trans numu mula. have mf : measurable_fun E ('d nu '/d mu). - exact/measurable_funTS/(measurable_int (f_integrable _)). + exact/measurable_funTS/(measurable_int _ (f_integrable _)). have [h [ndh hf]] := approximation mE mf (fun x _ => f_ge0 numu x). apply: integral_ae_eq => //. - apply: (integrableS measurableT) => //. apply: f_integrable. exact: (measure_dominates_trans numu mula). - apply: emeasurable_funM => //. - exact/measurable_funTS/(measurable_int (f_integrable _)). + exact/measurable_funTS/(measurable_int _ (f_integrable _)). - move=> A AE mA; rewrite change_of_variables//. + by rewrite -!f_integral. + exact: f_ge0. diff --git a/theories/ereal.v b/theories/ereal.v index 0ae89ce348..d7fdf10fbd 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -347,6 +347,13 @@ End DualAddTheory. HB.instance Definition _ (R : numDomainType) := isPointed.Build (\bar R) 0%E. +Lemma funID {aT : pointedType} (D : set aT) {R : numDomainType} + (f : aT -> \bar R) : f = (f \_ ~` D) \+ (f \_ D). +Proof. +by apply/funext => x; rewrite !patchE in_setC; case: ifPn => [xD|/negPn ->]; + rewrite ?(negbTE xD) ?(addr0,add0r). +Qed. + Section ereal_supremum. Variable R : realFieldType. Local Open Scope classical_set_scope. @@ -596,6 +603,10 @@ Proof. by apply/funext=> t; rewrite /restrict/=; case: ifPn => // _; rewrite abse0. Qed. +Lemma restrict_EFin T (R : numFieldType) (f : T -> R) (D : set T) : + (EFin \o f) \_ D = EFin \o (f \_ D). +Proof. by apply/funext => x; rewrite /= !patchE; case: ifPn. Qed. + Section SignedRealFieldStability. Context {R : realFieldType}. diff --git a/theories/ftc.v b/theories/ftc.v index ab9f19614b..4456b039c5 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -5,11 +5,13 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality fsbigop . Require Import signed reals ereal topology normedtype sequences real_interval. Require Import esum measure lebesgue_measure numfun realfun lebesgue_integral. -Require Import derive. +Require Import derive charge. (**md**************************************************************************) (* # Fundamental Theorem of Calculus for the Lebesgue Integral *) (* *) +(* indefinite_integral mu a x f := \int[mu]_(t \in `[a, x] f t) *) +(* *) (******************************************************************************) Set Implicit Arguments. @@ -230,3 +232,277 @@ by split; [exact: dfx|rewrite f'xE]. Unshelve. all: by end_near. Qed. End FTC. + +Definition indefinite_integral {R : realType} + (mu : {measure set (g_sigma_algebraType (R.-ocitv.-measurable)) -> \bar R}) + a x (f : R -> R) : R := + (\int[mu]_(t in `[a, x]) f t)%R. + +Section indefinite_integral_continuous. +Context {R : realType}. +Notation mu := (@lebesgue_measure R). + +Let int := (indefinite_integral mu). + +Lemma indefinite_integral_near_left (a b : R) (e : R) (f : R -> R) : + a < b -> 0 < e -> mu.-integrable `[a, b] (EFin \o f) -> + \forall c \near a, `| int a c f | < e. +Proof. +move=> ab e0 intf. +have : mu.-integrable setT (EFin \o f \_`[a, b]). + by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setTI. +move=> /integral_normr_continuous /(_ _ e0)[d [d0 /=]] ifab. +near=> c. +have [ca|ca] := leP c a. + rewrite /int /indefinite_integral/= /Rintegral. + rewrite (integral_Sset1 a) ?fine0 ?normr0//. + move: ca; rewrite le_eqVlt => /predU1P[->|ca]; first by rewrite interval_set1. + by rewrite set_itv_ge//= bnd_simp -ltNge. +have /ifab : (mu `[a, c] < d%:E)%E. + rewrite lebesgue_measure_itv/= lte_fin ca -EFinD lte_fin. + by move: ca; near: c; exact: nbhs_right_ltDr. +move=> /(_ (measurable_itv _)) {ifab}. +apply: le_lt_trans. +have acbc : `[a, c] `<=` `[a, b]. + rewrite (@itv_bndbnd_setU _ _ (BLeft a) (BRight c) (BRight b))// bnd_simp. + exact: ltW. + by move: ca; near: c; exact: nbhs_right_le. +rewrite -lee_fin fineK; last first. + apply: integral_fune_fin_num => //=. + rewrite (_ : (fun _ => _) = abse \o ((EFin \o f) \_ `[a, b])); last first. + by apply/funext => x /=; rewrite restrict_EFin. + apply/integrable_abse/integrable_restrict => //=. + by rewrite setIidl//; exact: integrableS intf. +rewrite [leRHS]integralEpatch//= [in leRHS]integralEpatch//=. +under [in leRHS]eq_integral. + move=> /= x xac. + rewrite -patch_setI setIid restrict_EFin/= restrict_normr/=. + rewrite -patch_setI setIidl//. + over. +rewrite /= [leRHS](_ : _ = \int[mu]_(x in `[a, c]) `| f x |%:E)%E; last first. + rewrite [RHS]integralEpatch//=; apply: eq_integral => x xac/=. + by rewrite restrict_EFin/= restrict_normr. +set rhs : \bar R := leRHS. +have [->|rhsoo] := eqVneq rhs +oo%E; first by rewrite leey. +rewrite /int /indefinite_integral /= /Rintegral. +set lhs := (\int[mu]_(_ in _) _)%E. +have [->|lhsNoo] := eqVneq lhs -oo%E; first by rewrite /= normr0 integral_ge0. +have lhsoo : lhs != +oo%E. + apply: contra rhsoo => /eqP lhsoo. + rewrite -leye_eq -lhsoo; apply: le_integral => //=. + - exact: integrableS intf. + - rewrite [X in integrable _ _ X](_ : _ = abse \o EFin \o f)//. + by apply: integrable_abse => /=; exact: integrableS intf. + - by move=> x _; rewrite lee_fin ler_norm. +rewrite [leLHS](_ : _ = `| lhs |)%E//; last first. + by move: lhsNoo lhsoo; rewrite /lhs /rhs; case: integral. +apply: (le_trans (le_abse_integral _ _ _)) => //=. +by apply: (measurable_funS _ acbc) => //; exact: measurable_int intf. +Unshelve. all: by end_near. Qed. + +Lemma indefinite_integral_cvg_left a b (f : R -> R) : a < b -> + mu.-integrable `[a, b] (EFin \o f) -> + int a x f @[x --> a] --> int a a f. +Proof. +move=> ab intf. +pose fab := f \_ `[a, b]. +have intfab : mu.-integrable `[a, b] (EFin \o fab). + by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setIidr. +apply/cvgrPdist_le => /= e e0; rewrite near_simpl; near=> x. +rewrite {1}/int /indefinite_integral /Rintegral /=. +rewrite (integral_Sset1 a) ?interval_set1// fine0 sub0r normrN. +apply/ltW. +by near: x; exact: (@indefinite_integral_near_left _ b). +Unshelve. all: by end_near. Qed. + +Lemma indefinite_integral_cvg_at_left a b (f : R -> R) : a < b -> + mu.-integrable `[a, b] (EFin \o f) -> + int a x f @[x --> b^'-] --> int a b f. +Proof. +move=> ab intf. +pose fab := f \_ `[a, b]. +have /= int_normr_cont : forall e : R, 0 < e -> + exists d : R, 0 < d /\ + forall A, measurable A -> (mu A < d%:E)%E -> \int[mu]_(x in A) `|fab x| < e. + rewrite /= => e e0; apply: integral_normr_continuous => //=. + by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setTI. +have intfab : mu.-integrable `[a, b] (EFin \o fab). + by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setIidr. +rewrite /int /indefinite_integral; apply/cvgrPdist_le => /= e e0. +have [d [d0 /= {}int_normr_cont]] := int_normr_cont _ e0. +near=> x. +rewrite [in X in X - _](@itv_bndbnd_setU _ _ _ (BRight x))//; + [|by rewrite bnd_simp ltW..]. +rewrite {1}/Rintegral integral_setU_EFin//=; last 2 first. + rewrite -itv_bndbnd_setU// ?bnd_simp; last 2 first. + by near: x; exact: nbhs_left_ge. + exact/ltW. + by apply/EFin_measurable_fun; apply: measurable_int intf. + apply/disj_set2P; rewrite -subset0 => z/=; rewrite !in_itv/= => -[/andP[_]]. + by rewrite leNgt => /negbTE ->. +have xbab : `]x, b] `<=` `[a, b]. + move=> z/=; rewrite !in_itv/= => /andP[xz ->/=]. + rewrite andbT (le_trans _ (ltW xz))//. + by near: x; exact: nbhs_left_ge. +rewrite /Rintegral fineD; last 2 first. + - rewrite fin_num_abs (le_lt_trans (le_abse_integral _ _ _)) //=. + + case/integrableP : intf => + _. + apply: measurable_funS => // z/=; rewrite !in_itv/= => /andP[->/=]. + by move=> /le_trans; apply. + + apply: integral_fune_lt_pinfty => //=. + rewrite [X in _.-integrable _ X](_ : _ = abse \o (EFin \o f))//. + apply/integrable_abse/(integrableS _ _ _ intf) => //. + move=> z/=; rewrite !in_itv/= => /andP[->/=]. + by move=> /le_trans; apply. + - rewrite fin_num_abs (le_lt_trans (le_abse_integral _ _ _)) //=. + + by case/integrableP : intf => + _; exact: measurable_funS. + + apply: integral_fune_lt_pinfty => //=. + rewrite [X in _.-integrable _ X](_ : _ = abse \o (EFin \o f))//. + exact/integrable_abse/(integrableS _ _ _ intf). +rewrite -addrAC subrr add0r. +rewrite [X in fine X](_ : _ = + (\int[mu]_(x0 in `]x, b]) (fab x0)%:E))%E//; last first. + apply: eq_integral => //= z. + rewrite inE/= in_itv/= => /andP[xz zb]. + rewrite /fab patchE ifT// inE/= in_itv/=. + rewrite zb andbT (le_trans _ (ltW xz))//. + by near: x; exact: nbhs_left_ge. +apply: ltW. +rewrite -lte_fin EFin_normr_Rintegral//=; last exact: integrableS intfab. +rewrite (le_lt_trans (le_abse_integral _ _ _))//=. + case/integrableP : intf => /EFin_measurable_fun mf _. + apply/measurableT_comp => //; apply/measurable_restrict => //=. + by rewrite setIidl//; exact: measurable_funS mf. +rewrite -[ltLHS]fineK//. +- rewrite lte_fin int_normr_cont// lebesgue_measure_itv/= lte_fin. + rewrite ifT// -EFinD lte_fin. + near: x; exists d => // z; rewrite /ball_/= => + zb. + by rewrite gtr0_norm// ?subr_gt0. +- rewrite ge0_fin_numE//; last exact: integral_ge0. + apply: integral_fune_lt_pinfty => //=. + rewrite [X in _.-integrable _ X](_ : _ = abse \o (EFin \o fab))//. + by apply: integrable_abse; exact: integrableS intfab. +Unshelve. all: by end_near. Qed. + +End indefinite_integral_continuous. + +Section corollary_FTC1. +Context {R : realType}. +Notation mu := lebesgue_measure. +Local Open Scope ereal_scope. +Implicit Types (f : R -> R) (a b : R). + +Corollary continuous_FTC2 f F a b : (a < b)%R -> {in `[a, b], continuous f} -> + derivable_oo_continuous_bnd F a b -> + {in `]a, b[, F^`() =1 f} -> + (\int[mu]_(x in `[a, b]) (f x)%:E = (F b)%:E - (F a)%:E)%E. +Proof. +move=> ab cf dF F'f. +pose fab := f \_ `[a, b]. +pose G x : R := (\int[mu]_(t in `[a, x]) fab t)%R. +have iabf : mu.-integrable `[a, b] (EFin \o f). + apply: continuous_compact_integrable; first exact: segment_compact. + by apply: continuous_in_subspaceT => x /[!inE] => /cf. +have ifab : mu.-integrable setT (EFin \o fab). + by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setTI. +have G'f : {in `]a, b[, forall x, G^`() x = fab x /\ derivable G x 1}. + move=> x /[!in_itv]/= /andP[ax xb]. + have := @continuous_FTC1 _ _ (BLeft a) ifab x. + rewrite /= lte_fin => /(_ ax). + have : {for x, continuous fab}. + have /cf xf : x \in `[a, b] by rewrite in_itv/= (ltW ax) (ltW xb). + rewrite /prop_for /continuous_at {2}/fab/= patchE. + rewrite mem_set ?mulr1 /=; last by rewrite in_itv/= (ltW ax) (ltW xb). + apply: cvg_trans xf; apply: near_eq_cvg; rewrite !near_simpl; near=> z. + rewrite /fab/= patchE mem_set ?mulr1//=. + near: z; have := @near_in_itv R a b x. + rewrite in_itv/= ax xb => /(_ isT). + by apply: filterS => z; exact: subset_itv_oo_cc. + by move=> /[swap] /[apply] -[]. +have F'G'0 : {in `]a, b[, (F^`() - G^`() =1 cst 0)%R}. + move=> x xab; rewrite !fctE (G'f x xab).1 /fab. + by rewrite patchE mem_set/= ?F'f ?subrr//; exact: subset_itv_oo_cc. +have [k FGk] : exists k : R, {in `]a, b[, (F - G =1 cst k)%R}. + have : {in `]a, b[ &, forall x y, (F x - G x = F y - G y)%R}. + move=> x y xab yab. + wlog xLy : x y xab yab / (x <= y)%R. + move=> abFG; have [|/ltW] := leP x y; first exact: abFG. + by move/abFG => /(_ yab xab). + move: xLy; rewrite le_eqVlt => /predU1P[->//|xy]. + have [| |] := @MVT _ (F \- G)%R (F^`() - G^`())%R x y xy. + - move=> z zxy; have zab : z \in `]a, b[. + rewrite !in_itv/=; move: zxy; rewrite in_itv/= => /andP[xz zy]. + rewrite (le_lt_trans _ xz)//= ?(lt_le_trans zy)//=. + + by move: yab; rewrite in_itv/= => /andP[_ /ltW]. + + by move: xab; rewrite in_itv/= => /andP[/ltW]. + have Fz1 : derivable F z 1. + by case: dF => /= + _ _; apply; rewrite inE in zab. + have Gz1 : derivable G z 1 by have [|] := G'f z. + apply: DeriveDef. + + by apply: derivableB; [exact: Fz1|exact: Gz1]. + + by rewrite deriveB -?derive1E; [by []|exact: Fz1|exact: Gz1]. + - apply: derivable_within_continuous => z zxy. + apply: derivableB. + + case: dF => /= + _ _; apply. + rewrite in_itv/=; move: zxy; rewrite in_itv/= => /andP[xz zy]. + rewrite (lt_le_trans _ xz)/= ?(le_lt_trans zy)//=. + * by move: yab; rewrite in_itv/= => /andP[]. + * by move: xab; rewrite in_itv/= => /andP[]. + + apply: (G'f _ _).2; rewrite in_itv/=; apply/andP; split. + * move: zxy; rewrite in_itv/= => /andP[+ _]; apply: lt_le_trans. + by move: xab; rewrite in_itv/= => /andP[]. + * move: zxy; rewrite in_itv/= => /andP[_]; move=> /le_lt_trans; apply. + by move: yab; rewrite in_itv/= => /andP[]. + - move=> z zxy; rewrite F'G'0. + by rewrite /cst/= mul0r => /eqP; rewrite subr_eq0 => /eqP. + rewrite !in_itv/=; move: zxy; rewrite in_itv/= => /andP[xz zy]. + rewrite (le_lt_trans _ xz)//= ?(lt_le_trans zy)//=. + * by move: yab; rewrite in_itv/= => /andP[_ /ltW]. + * by move: xab; rewrite in_itv/= => /andP[/ltW]. + move=> H; pose c := (a + b) / 2. + exists (F c - G c)%R => u /(H u c); apply. + by rewrite in_itv/= midf_lt//= midf_lt. +have [c GFc] : exists c : R, forall x, x \in `]a, b[ -> (F x - G x)%R = c. + by exists k => x xab; rewrite -[k]/(cst k x) -(FGk x xab). +have Ga0 : G a = 0%R by rewrite /G/= interval_set1// /Rintegral integral_set1. +case: (dF) => _ Fa Fb. +have GacFa : G x @[x --> a^'+] --> (- c + F a)%R. + have Fap : Filter a^'+ by exact: at_right_proper_filter. + have GFac : (G x - F x)%R @[x --> a^'+] --> (- c)%R. + apply/cvgrPdist_le => /= e e0; near=> t. + rewrite opprB GFc; last by rewrite in_itv/=; apply/andP. + by rewrite addrC subrr normr0 ltW. + have := @cvgD _ _ _ _ Fap _ _ _ _ GFac Fa. + rewrite (_ : (G \- F)%R + F = G)//. + by apply/funext => x/=; rewrite subrK. +have GbcFb : G x @[x --> b^'-] --> (- c + F b)%R. + have Fbn : Filter b^'- by exact: at_left_proper_filter. + have GFbc : (G x - F x)%R @[x --> b^'-] --> (- c)%R. + apply/cvgrPdist_le => /= e e0; near=> t. + rewrite opprB GFc; last by rewrite in_itv/=; apply/andP. + by rewrite addrC subrr normr0 ltW. + have := @cvgD _ _ _ _ Fbn _ _ _ _ GFbc Fb. + rewrite (_ : (G \- F)%R + F = G)//. + by apply/funext => x/=; rewrite subrK. +have contF : {within `[a, b], continuous F}. + apply/continuous_within_itvP => //; split => // z zab. + apply/differentiable_continuous/derivable1_diffP. + by case: dF => /= + _ _; exact. +have iabfab : mu.-integrable `[a, b] (EFin \o fab). + by rewrite -restrict_EFin; apply/integrable_restrict => //; rewrite setIidr. +have Ga : G x @[x --> a^'+] --> G a. + by have /left_right_continuousP[] := indefinite_integral_cvg_left ab iabfab. +have Gb : G x @[x --> b^'-] --> G b. + exact: (indefinite_integral_cvg_at_left ab iabfab). +have cE : c = F a. + apply/eqP;rewrite -(opprK c) eq_sym -addr_eq0 addrC. + by have := cvg_unique _ GacFa Ga; rewrite Ga0 => ->. +have GbFbc : G b = (F b - c)%R. + by have := cvg_unique _ GbcFb Gb; rewrite addrC => ->. +rewrite -EFinB -cE -GbFbc /G/= /Rintegral/= fineK//. + rewrite integralEpatch//=. + by under eq_integral do rewrite restrict_EFin. +exact: integral_fune_fin_num. +Unshelve. all: by end_near. Qed. + +End corollary_FTC1. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 7bf196baca..32b518904b 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -1550,7 +1550,7 @@ Proof. rewrite integral_mkcond erestrict_scale [in RHS]integral_mkcond => k0. set h1 := f1 \_ D. have h10 x : 0 <= h1 x by apply: erestrict_ge0. -have mh1 : measurable_fun setT h1 by apply/(measurable_restrict _ mD). +have mh1 : measurable_fun setT h1 by exact/(measurable_restrictT _ _).1. have [g [nd_g gh1]] := approximation measurableT mh1 (fun x _ => h10 x). pose kg := fun n => scale_nnsfun (g n) k0. rewrite (@nd_ge0_integral_lim _ _ _ mu (fun x => k%:E * h1 x) kg). @@ -1589,8 +1589,8 @@ rewrite !(integral_mkcond D) erestrictD. set h1 := f1 \_ D; set h2 := f2 \_ D. have h10 x : 0 <= h1 x by apply: erestrict_ge0. have h20 x : 0 <= h2 x by apply: erestrict_ge0. -have mh1 : measurable_fun setT h1 by apply/(measurable_restrict _ mD). -have mh2 : measurable_fun setT h2 by apply/(measurable_restrict _ mD). +have mh1 : measurable_fun setT h1 by exact/(measurable_restrictT _ _).1. +have mh2 : measurable_fun setT h2 by exact/(measurable_restrictT _ _).1. have [g1 [nd_g1 gh1]] := approximation measurableT mh1 (fun x _ => h10 x). have [g2 [nd_g2 gh2]] := approximation measurableT mh2 (fun x _ => h20 x). pose g12 := fun n => add_nnsfun (g1 n) (g2 n). @@ -1623,10 +1623,10 @@ move=> f12; rewrite !(integral_mkcond D). set h1 := f1 \_ D; set h2 := f2 \_ D. have h10 x : 0 <= h1 x by apply: erestrict_ge0. have h20 x : 0 <= h2 x by apply: erestrict_ge0. -have mh1 : measurable_fun setT h1 by apply/(measurable_restrict _ mD). -have mh2 : measurable_fun setT h2 by apply/(measurable_restrict _ mD). +have mh1 : measurable_fun setT h1 by exact/(measurable_restrictT _ _).1. +have mh2 : measurable_fun setT h2 by exact/(measurable_restrictT _ _).1. have h12 x : h1 x <= h2 x by apply: lee_restrict. -have [g1 [nd_g1 /(_ _ Logic.I)gh1]] := +have [g1 [nd_g1 /(_ _ Logic.I) gh1]] := approximation measurableT mh1 (fun x _ => h10 _). rewrite (nd_ge0_integral_lim _ h10 (fun x => lef_at x nd_g1) gh1)//. apply: lime_le. @@ -1824,9 +1824,9 @@ move=> A mA; wlog NAnoo: A mD mf mg mA / ~ (A -oo) => [hwlogA|]. apply: measurableU; last by apply: hwlogA=> //; [exact: measurableD|case=>/=]. have -> : (f \+ g) @^-1` [set -oo] = f @^-1` [set -oo] `|` g @^-1` [set -oo]. apply/seteqP; split=> x /= => [/eqP|[]]; rewrite /preimage/=. - - by rewrite adde_eq_ninfty => /orP[] /eqP->; [left|right]. - - by move->. - - by move->; rewrite addeC. + - by rewrite adde_eq_ninfty => /orP[] /eqP ->; [left|right]. + - by move=> ->. + - by move=> ->; rewrite addeC. by rewrite setIUr; apply: measurableU; [apply: mf|apply: mg]. have-> : D `&` (f \+ g) @^-1` A = (D `&` [set x | f x +? g x]) `&` (f \+ g) @^-1` A. @@ -1862,12 +1862,11 @@ exact: emeasurable_fun_sum. Qed. Lemma ge0_emeasurable_fun_sum D (h : nat -> (T -> \bar R)) (P : pred nat) : - (forall k x, D x -> P k -> 0 <= h k x) -> (forall k, P k -> measurable_fun D (h k)) -> + (forall k x, D x -> P k -> 0 <= h k x) -> + (forall k, P k -> measurable_fun D (h k)) -> measurable_fun D (fun x => \sum_(i h0 mh. -move=> mD; move: (mD). -apply/(@measurable_restrict _ _ _ _ _ setT) => //. +move=> h0 mh mD; move: (mD); apply/measurable_restrictT => //. rewrite [X in measurable_fun _ X](_ : _ = (fun x => \sum_(0 <= i x/=; rewrite /patch; case: ifPn => // xD. @@ -1880,10 +1879,9 @@ rewrite [X in measurable_fun _ X](_ : _ = apply: measurable_fun_limn_esup => k. under eq_fun do rewrite big_mkcond. apply: emeasurable_fun_sum => n. -have [|] := boolP (n \in P). - rewrite /in_mem/= => Pn; rewrite Pn. - by apply/(measurable_restrict (h n)) => //; exact: mh. -by rewrite /in_mem/= => /negbTE ->. +have [|] := boolP (n \in P); last by rewrite /in_mem/= => /negbTE ->. +rewrite /in_mem/= => Pn; rewrite Pn. +by apply/(measurable_restrictT _ _).1 => //; exact: mh. Qed. Lemma emeasurable_funB D f g : @@ -2042,7 +2040,7 @@ Let g n := (g' n \_ D). Let g0 n x : 0 <= g n x. Proof. exact/erestrict_ge0/g'0. Qed. Let mg n : measurable_fun setT (g n). -Proof. exact/(measurable_restrict _ mD). Qed. +Proof. exact/(measurable_restrictT _ _).1. Qed. Let nd_g x : nondecreasing_seq (g^~ x). Proof. @@ -2799,7 +2797,7 @@ rewrite [leRHS]integral_mkcond; apply: ge0_le_integral => //. - by move=> x _; rewrite lee_fin. - exact/EFin_measurable_fun. - by move=> x _; rewrite erestrict_ge0. -- exact/(measurable_restrict _ mD). +- exact/(measurable_restrictT _ mD). Qed. End ge0_integral_measure_series. @@ -2824,13 +2822,11 @@ transitivity (\int[mu]_(x in A `|` B) ((f \_ A) x + (f \_ B) x)). rewrite ge0_integralD//; last 5 first. - exact: measurableU. - by move=> x _; apply: erestrict_ge0 => y Ay; apply: f0; left. - - have : measurable_fun A f. - by apply: measurable_funS mf; [exact: measurableU|exact: subsetUl]. - by apply/(measurable_restrict _ _ _ _).1 => //; exact: measurableU. + - apply/measurable_restrict => //; first exact: measurableU. + apply: measurable_funS mf; [exact: measurableU|exact: subIsetl]. - by move=> x _; apply: erestrict_ge0 => y By; apply: f0; right. - - have : measurable_fun B f. - by apply: measurable_funS mf; [exact: measurableU|exact: subsetUr]. - by apply/(measurable_restrict _ _ _ _).1 => //; exact: measurableU. + - apply/measurable_restrict => //; first exact: measurableU. + apply: measurable_funS mf; [exact: measurableU|exact: subIsetl]. by rewrite -integral_mkcondl setIC setUK -integral_mkcondl setKU. Qed. @@ -2940,6 +2936,7 @@ Proof. by rewrite unlock; apply/(iffP (asboolP _)). Qed. Lemma measurable_int d T R mu D f : @integrable d T R mu D f -> measurable_fun D f. Proof. by rewrite unlock => /asboolP[]. Qed. +Arguments measurable_int {d T R} mu {D f}. Section integrable_theory. Local Open Scope ereal_scope. @@ -3107,16 +3104,16 @@ Lemma integrableMr (h : T -> R) g : Proof. move=> mh [M [Mreal Mh]] gi; apply/integrableP; split. by apply: emeasurable_funM => //; [exact: measurableT_comp| - exact: (measurable_int gi)]. + exact: measurable_int gi]. under eq_integral do rewrite abseM. have: \int[mu]_(x in D) (`|M + 1|%:E * `|g x|) < +oo. rewrite ge0_integralZl ?lte_mul_pinfty//; first by case/integrableP : gi. by apply: measurableT_comp => //; exact: measurable_int gi. apply/le_lt_trans/ge0_le_integral => //. -- apply/emeasurable_funM; last exact/measurableT_comp/(measurable_int gi). +- apply/emeasurable_funM; last exact/measurableT_comp/(measurable_int _ gi). exact/EFin_measurable_fun/measurableT_comp. - apply/emeasurable_funM => //; apply/measurableT_comp => //. - exact: (measurable_int gi). + exact: measurable_int gi. - move=> x Dx; rewrite lee_wpmul2r//= lee_fin Mh//=. by rewrite (lt_le_trans _ (ler_norm _))// ltrDl. Qed. @@ -3129,6 +3126,30 @@ move=> fi mh mg; rewrite /is_true -(integrableMr mh mg fi). by apply/congr1/funext => ?; rewrite muleC. Qed. +Lemma integrable_restrict (E : set T) (mE : d.-measurable E) f : + integrable mu (E `&` D) f <-> integrable mu E (f \_ D). +Proof. +split; move=> /integrableP[mf intfoo]; apply/integrableP; split. +- exact/measurable_restrict. +- by move: intfoo; rewrite integral_mkcondr/= restrict_abse. +- exact/measurable_restrict. +- by move: intfoo; rewrite integral_mkcondr/= restrict_abse. +Qed. + +Lemma le_integral f g : mu_int f -> mu_int g -> + {in D, forall x, f x <= g x} -> \int[mu]_(x in D) f x <= \int[mu]_(x in D) g x. +Proof. +move=> intf intg fg; rewrite integralE [leRHS]integralE leeB//. +- apply: ge0_le_integral => //. + + by move/integrableP : intf => [+ _]; exact: measurable_funepos. + + by move/integrableP : intg => [+ _]; exact: measurable_funepos. + + by move=> x /mem_set; exact: funepos_le. +- apply: ge0_le_integral => //. + + by move/integrableP : intg => [+ _]; exact: measurable_funeneg. + + by move/integrableP : intf => [+ _]; exact: measurable_funeneg. + + by move=> x /mem_set; exact: funeneg_le. +Qed. + End integrable_theory. Notation "mu .-integrable" := (integrable mu) : type_scope. Arguments eq_integrable {d T R mu D} mD f. @@ -3222,7 +3243,7 @@ transitivity (\int[mu]_x limn (f_ ^~ x)). rewrite integral_mkcond; apply: eq_integral => x _. by apply/esym/cvg_lim => //; exact: lim_f_. rewrite monotone_convergence//; last 3 first. - - move=> n; apply/(measurable_restrict f) => //. + - move=> n; apply/(measurable_restrictT f) => //. by apply: bigsetU_measurable => k _; exact: mF. move: mf; apply/measurable_funS =>//; first exact: bigcup_measurable. by rewrite big_mkord; exact: bigsetU_bigcup. @@ -3259,10 +3280,8 @@ move=> mD. rewrite unlock; apply: asbool_equiv; rewrite [in X in X <-> _]integral_mkcond. under [in X in X <-> _]eq_integral do rewrite restrict_abse. split => [|] [mf foo]. -- by split; [exact/(measurable_restrict _ _ _ _).1| - exact: le_lt_trans foo]. -- by split; [exact/(measurable_restrict _ _ measurableT _).2| - exact: le_lt_trans foo]. +- by split; [exact/(measurable_restrictT _ _).1| exact: le_lt_trans foo]. +- by split; [exact/(measurable_restrictT _ _).2| exact: le_lt_trans foo]. Qed. End integrable_lemmas. @@ -3297,7 +3316,7 @@ have [muD0|muD0] := eqVneq (mu D) 0. pose E := [set x | `|f x| = +oo /\ D x ]. have mE : measurable E. rewrite (_ : E = D `&` f @^-1` [set -oo; +oo]). - by apply: (measurable_int fint) => //; exact: measurableU. + by apply: (measurable_int _ fint) => //; exact: measurableU. rewrite /E predeqE => t; split=> [[/eqP]|[Dt [|]/= ->//]]. by rewrite eqe_absl leey andbT /preimage/= => /orP[|]/eqP; tauto. have [ET|ET] := eqVneq E setT. @@ -3321,7 +3340,7 @@ have [M M0 muM] : exists2 M, (0 <= M)%R & apply: ge0_le_integral => //. - by move=> *; rewrite lee_fin /indic. - exact/EFin_measurable_fun/measurableT_comp. - - by apply: measurableT_comp => //; apply: measurable_int fint. + - by apply: measurableT_comp => //; exact: measurable_int fint. - move=> x Dx; rewrite /= indicE. have [|xE] := boolP (x \in E); last by rewrite mule0. by rewrite /E inE /= => -[->]; rewrite leey. @@ -3492,6 +3511,18 @@ by rewrite -ge0_integralD // -?fune_abse//; [exact: measurable_funepos | exact: measurable_funeneg]. Qed. +Lemma EFin_normr_Rintegral d (T : measurableType d) {R : realType} + (mu : {measure set T -> \bar R}) (A : set T) (f : T -> R) : measurable A -> + mu.-integrable A (EFin \o f) -> + `| \int[mu]_(x in A) f x |%:E = `| \int[mu]_(x in A) (f x)%:E |%E. +Proof. +move=> mA /integrableP[mf intfoo]; rewrite -[RHS]fineK. +- rewrite /= fine_abse// fin_num_abs. + exact: (le_lt_trans (le_abse_integral _ _ _)). +- rewrite abse_fin_num fin_num_abs. + exact: (le_lt_trans (le_abse_integral _ _ _)). +Qed. + Lemma abse_integralP d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}) (D : set T) (f : T -> \bar R) : measurable D -> measurable_fun D f -> @@ -3505,24 +3536,32 @@ move: foo; rewrite integralE/= -fin_num_abs fin_numB => /andP[fpoo fnoo]. by rewrite lte_add_pinfty// ltey_eq ?fpoo ?fnoo. Qed. -Section integral_indic. +Section integral_patch. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}). -Lemma integral_setI_indic (E D : set T) (mD : measurable D) (f : T -> \bar R) : +Lemma __deprecated__integral_setI_indic (E D : set T) (mD : measurable D) (f : T -> \bar R) : measurable E -> \int[mu]_(x in E `&` D) f x = \int[mu]_(x in E) (f x * (\1_D x)%:E). Proof. -move=> mE; rewrite integral_mkcondr; apply: eq_integral => x xE. -by rewrite indic_restrict /patch; case: ifPn; rewrite ?mule1 ?mule0. +move=> mE; rewrite integral_mkcondr. +by under eq_integral do rewrite epatch_indic. Qed. -Lemma integralEindic (D : set T) (mD : measurable D) (f : T -> \bar R) : +Lemma __deprecated__integralEindic (D : set T) (mD : measurable D) (f : T -> \bar R) : \int[mu]_(x in D) f x = \int[mu]_(x in D) (f x * (\1_D x)%:E). -Proof. by rewrite -integral_setI_indic// setIid. Qed. +Proof. by rewrite -__deprecated__integral_setI_indic// setIid. Qed. -End integral_indic. +Lemma integralEpatch (D : set T) (mD : measurable D) (f : T -> \bar R) : + \int[mu]_(x in D) f x = \int[mu]_(x in D) (f \_ D) x. +Proof. by rewrite -[in LHS](setIid D) integral_mkcondr. Qed. + +End integral_patch. +#[deprecated(since="mathcomp-analysis 1.3.0", note="use `integral_mkcondr` instead")] +Notation integral_setI_indic := __deprecated__integral_setI_indic (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="use `integralEpatch` instead")] +Notation integralEindic := __deprecated__integralEindic (only parsing). Section ae_eq_integral. Local Open Scope ereal_scope. @@ -3552,8 +3591,7 @@ have : 0 <= \int[mu]_(x in D) `|f x| <= `|M|%:E * mu Df_neq0. - exact: measurableT_comp. - by move=> x Dx; rewrite mule_ge0// lee_fin. - by apply: emeasurable_funM => //; exact: measurableT_comp. - - move=> x Dx. - rewrite (le_trans (le_f_M _ Dx))// lee_fin /f' indicE. + - move=> x Dx; rewrite (le_trans (le_f_M _ Dx))// lee_fin /f' indicE. by case: (_ \in _) => //; rewrite ?mulr1 ?mulr0// ler_norm. have -> : mu Df_neq0 = 0. apply: (subset_measure0 _ _ _ mN0) => //. @@ -3640,26 +3678,14 @@ Lemma integral_abs_eq0 D (N : set T) (f : T -> \bar R) : measurable N -> measurable D -> N `<=` D -> measurable_fun D f -> mu N = 0 -> \int[mu]_(x in N) `|f x| = 0. Proof. -move=> mN mD ND mf muN0; rewrite integralEindic//. -rewrite (eq_integral (fun x => `|f x * (\1_N x)%:E|)); last first. - by move=> t _; rewrite abseM (@gee0_abs _ (\1_N t)%:E)// lee_fin. +move=> mN mD ND mf muN0; rewrite integralEpatch//. +rewrite (eq_integral (abse \o (f \_ N))); last first. + by move=> t _; rewrite restrict_abse. apply/ae_eq_integral_abs => //. - apply: emeasurable_funM => //; first exact: (measurable_funS mD). - exact/EFin_measurable_fun. -exists N; split => // t /= /not_implyP[_]; rewrite indicE. -by have [|] := boolP (t \in N); rewrite ?inE ?mule0. -Qed. - -Lemma funID (N : set T) (mN : measurable N) (f : T -> \bar R) : - let oneCN := [the {nnsfun T >-> R} of mindic R (measurableC mN)] in - let oneN := [the {nnsfun T >-> R} of mindic R mN] in - f = (fun x => f x * (oneCN x)%:E) \+ (fun x => f x * (oneN x)%:E). -Proof. -move=> oneCN oneN; rewrite funeqE => x. -rewrite /oneCN /oneN/= /mindic !indicE. -have [xN|xN] := boolP (x \in N). - by rewrite mule1 in_setC xN mule0 add0e. -by rewrite in_setC xN mule0 adde0 mule1. + apply/measurable_restrict => //; rewrite setIidr//. + exact: (measurable_funS mD). +exists N; split => // t /= /not_implyP[_]. +by rewrite patchE; case: ifPn => //; rewrite inE. Qed. Lemma negligible_integrable (D N : set T) (f : T -> \bar R) : @@ -3668,35 +3694,29 @@ Lemma negligible_integrable (D N : set T) (f : T -> \bar R) : Proof. move=> mN mD mf muN0. pose mCN := measurableC mN. -pose oneCN : {nnsfun T >-> R} := [the {nnsfun T >-> R} of mindic R mCN]. -pose oneN : {nnsfun T >-> R} := [the {nnsfun T >-> R} of mindic R mN]. -have /integrableP intone : mu.-integrable D (fun x => f x * (oneN x)%:E). +have /integrableP intone : mu.-integrable D (f \_ N). apply/integrableP; split. - apply: emeasurable_funM=> //; apply/EFin_measurable_fun. - exact: measurable_funTS. - rewrite (eq_integral (fun x => `|f x| * (\1_N x)%:E)); last first. - by move=> t _; rewrite abseM (@gee0_abs _ (\1_N t)%:E) // lee_fin. - rewrite -integral_setI_indic// (@integral_abs_eq0 D)//. - - exact: measurableI. - - by apply: (subset_measure0 _ _ _ muN0) => //; exact: measurableI. -have h1 : mu.-integrable D f <-> mu.-integrable D (fun x => f x * (oneCN x)%:E). - split=> [/integrableP intf | /integrableP intCf]. + by apply/measurable_restrict => //; exact: measurable_funS mf. + rewrite (eq_integral ((abse \o f) \_ N)); last first. + by move=> t _; rewrite restrict_abse. + rewrite -integral_mkcondr (@integral_abs_eq0 D)//; first exact: measurableI. + by apply: (subset_measure0 _ _ _ muN0) => //; exact: measurableI. +have h1 : mu.-integrable D f <-> mu.-integrable D (f \_ ~` N). + split=> [/integrableP intf|/integrableP intCf]. apply/integrableP; split. - apply: emeasurable_funM=> //; apply/EFin_measurable_fun => //. - exact: measurable_funTS. - rewrite (eq_integral (fun x => `|f x| * (\1_(~` N) x)%:E)); last first. - by move=> t _; rewrite abseM (@gee0_abs _ (\1_(~` N) t)%:E) // lee_fin. - rewrite -integral_setI_indic//; case: intf => _; apply: le_lt_trans. - by apply: ge0_subset_integral => //; [exact:measurableI| - exact:measurableT_comp]. - apply/integrableP; split => //; rewrite (funID mN f) -/oneCN -/oneN. - have ? : measurable_fun D (fun x : T => f x * (oneCN x)%:E). - by apply: emeasurable_funM=> //; exact/EFin_measurable_fun/measurable_funTS. - have ? : measurable_fun D (fun x : T => f x * (oneN x)%:E). - apply: emeasurable_funM => //. - exact/EFin_measurable_fun/measurable_funTS. + by apply/measurable_restrict => //; exact: measurable_funS mf. + rewrite (eq_integral ((abse \o f) \_ ~` N)); last first. + by move=> t _; rewrite restrict_abse. + rewrite -integral_mkcondr; case: intf => _; apply: le_lt_trans. + by apply: ge0_subset_integral => //=; [exact:measurableI| + exact:measurableT_comp]. + apply/integrableP; split => //; rewrite (funID N f). + have ? : measurable_fun D (f \_ ~` N). + by apply/measurable_restrict => //; exact: measurable_funS mf. + have ? : measurable_fun D (f \_ N). + by apply/measurable_restrict => //; exact: measurable_funS mf. apply: (@le_lt_trans _ _ - (\int[mu]_(x in D) (`|f x * (oneCN x)%:E| + `|f x * (oneN x)%:E|))). + (\int[mu]_(x in D) (`|(f \_ ~` N) x| + `|(f \_ N) x|))). apply: ge0_le_integral => //. - by apply: measurableT_comp => //; exact: emeasurable_funD. - by move=> ? ?; apply: adde_ge0. @@ -3704,23 +3724,21 @@ have h1 : mu.-integrable D f <-> mu.-integrable D (fun x => f x * (oneCN x)%:E). - by move=> *; rewrite lee_abs_add. rewrite ge0_integralD//; [|exact: measurableT_comp|exact: measurableT_comp]. by apply: lte_add_pinfty; [case: intCf|case: intone]. -have h2 : mu.-integrable (D `\` N) f <-> - mu.-integrable D (fun x => f x * (oneCN x)%:E). - split=> [/integrableP intCf | /integrableP intCf]; apply/integrableP. +have h2 : mu.-integrable (D `\` N) f <-> mu.-integrable D (f \_ ~` N). + split=> [/integrableP intCf|/integrableP intCf]; apply/integrableP. split. - apply: emeasurable_funM=> //; apply/EFin_measurable_fun => //. - exact: measurable_funTS. - rewrite (eq_integral (fun x => `|f x| * (\1_(~` N) x)%:E)); last first. - by move=> t _; rewrite abseM (@gee0_abs _ (\1_(~` N) t)%:E)// lee_fin. - rewrite -integral_setI_indic //; case: intCf => _; apply: le_lt_trans. - apply: ge0_subset_integral => //; [exact: measurableI|exact: measurableD|]. + by apply/measurable_restrict => //; exact: measurable_funS mf. + rewrite (eq_integral ((abse \o f) \_ ~` N)); last first. + by move=> t _; rewrite restrict_abse. + rewrite -integral_mkcondr //; case: intCf => _; apply: le_lt_trans. + apply: ge0_subset_integral => //=; [exact: measurableI|exact: measurableD|]. by apply: measurableT_comp => //; apply: measurable_funS mf => // ? []. split. move=> mDN A mA; rewrite setDE (setIC D) -setIA; apply: measurableI => //. exact: mf. - rewrite integral_setI_indic//. - case: intCf => _; rewrite (eq_integral (fun x => `|f x| * (\1_(~` N) x)%:E))//. - by move=> t _; rewrite abseM (@gee0_abs _ (\1_(~` N) t)%:E)// lee_fin. + rewrite integral_mkcondr/=. + under eq_integral do rewrite restrict_abse. + by case: intCf. by apply: (iff_trans h1); exact: iff_sym. Qed. @@ -3730,16 +3748,14 @@ Lemma ge0_negligible_integral (D N : set T) (f : T -> \bar R) : mu N = 0 -> \int[mu]_(x in D) f x = \int[mu]_(x in D `\` N) f x. Proof. move=> mN mD mf f0 muN0. -rewrite {1}(funID mN f) ge0_integralD//; last 4 first. - - by move=> x Dx; apply: mule_ge0 => //; [exact: f0|rewrite lee_fin]. - - apply: emeasurable_funM=> //; apply/EFin_measurable_fun=> //. - exact: measurable_funTS. - - by move=> x Dx; apply: mule_ge0 => //; [exact: f0|rewrite lee_fin]. - - apply: emeasurable_funM=> //; apply/EFin_measurable_fun=> //. - exact: measurable_funTS. -rewrite -integral_setI_indic//; last exact: measurableC. -rewrite -integral_setI_indic// [X in _ + X = _](_ : _ = 0) ?adde0//. -rewrite (eq_integral (abse \o f)); last first. +rewrite {1}(funID N f) ge0_integralD//; last 4 first. + - by move=> x Dx; rewrite patchE; case: ifPn => // _; exact: f0. + - apply/measurable_restrict => //; first exact/measurableC. + exact: measurable_funS mf. + - by move=> x Dx; rewrite patchE; case: ifPn => // _; exact: f0. + - by apply/measurable_restrict => //; exact: measurable_funS mf. +rewrite -integral_mkcondr [X in _ + X = _](_ : _ = 0) ?adde0//. +rewrite -integral_mkcondr (eq_integral (abse \o f)); last first. move=> x; rewrite in_setI => /andP[xD xN]. by rewrite /= gee0_abs// f0//; rewrite inE in xD. rewrite (@integral_abs_eq0 D)//; first exact: measurableI. @@ -3752,19 +3768,17 @@ Lemma ge0_ae_eq_integral (D : set T) (f g : T -> \bar R) : ae_eq D f g -> \int[mu]_(x in D) (f x) = \int[mu]_(x in D) (g x). Proof. move=> mD mf mg f0 g0 [N [mN N0 subN]]. -rewrite integralEindic// [RHS]integralEindic//. +rewrite integralEpatch// [RHS]integralEpatch//. rewrite (ge0_negligible_integral mN)//; last 2 first. - - by apply: emeasurable_funM => //; exact/EFin_measurable_fun. - - by move=> x Dx; apply: mule_ge0 => //; [exact: f0|rewrite lee_fin]. + - by apply/measurable_restrict => //; rewrite setIidr. + - by move=> x Dx; rewrite /= patchE (mem_set Dx) f0. rewrite [RHS](ge0_negligible_integral mN)//; last 2 first. - - by apply: emeasurable_funM => //; exact/EFin_measurable_fun. - - by move=> x Dx; apply: mule_ge0 => //; [exact: g0|rewrite lee_fin]. -- apply: eq_integral => x;rewrite in_setD => /andP[_ xN]. - apply: contrapT; rewrite indicE; have [|?] := boolP (x \in D). - rewrite inE => Dx; rewrite !mule1. - move: xN; rewrite notin_setE; apply: contra_not => fxgx; apply: subN => /=. - exact/not_implyP. - by rewrite !mule0. + - by apply/measurable_restrict => //; rewrite setIidr. + - by move=> x Dx; rewrite /= patchE (mem_set Dx) g0. +apply: eq_integral => x;rewrite in_setD => /andP[_ xN]. +apply: contrapT; rewrite !patchE; case: ifPn => xD //. +move: xN; rewrite notin_setE; apply: contra_not => fxgx; apply: subN => /=. +by apply/not_implyP; split => //; exact/set_mem. Qed. Lemma ae_eq_integral (D : set T) (g f : T -> \bar R) : @@ -3877,7 +3891,7 @@ have ig1 : mu.-integrable D (EFin \o g1). rewrite /g1 funeqE => x //=; rewrite !/restrict; case: ifPn => //. rewrite 2!in_setI => /andP[/andP[xA f1xfin] _] /=. by rewrite fineK//; rewrite inE in f1xfin. -have mg1 := measurable_int ig1. +have mg1 := measurable_int _ ig1. have ig2 : mu.-integrable D (EFin \o g2). rewrite (_ : _ \o _ = f2 \_ (A `&` B)) //. apply: (integrableS measurableT)=>//; apply/(integrable_mkcond _ _).1 => //. @@ -3885,7 +3899,7 @@ have ig2 : mu.-integrable D (EFin \o g2). rewrite /g2 funeqE => x //=; rewrite !/restrict; case: ifPn => //. rewrite in_setI => /andP[_]; rewrite in_setI => /andP[xB f2xfin] /=. by rewrite fineK//; rewrite inE in f2xfin. -have mg2 := measurable_int ig2. +have mg2 := measurable_int _ ig2. transitivity (\int[mu]_(x in D) (EFin \o (g1 \+ g2)%R) x). apply: ae_eq_integral => //. - exact: emeasurable_funD. @@ -3946,9 +3960,16 @@ move=> mN mD mf muN0; rewrite [f]funeposneg ?integralB //; first last. - apply: (integrableS mD) => //; first exact: measurableD. exact: integrable_funepos. - exact: measurableD. -congr (_ - _); apply: ge0_negligible_integral => //; apply: measurable_int. - exact: (integrable_funepos mD mf). -exact: (integrable_funeneg mD mf). +congr (_ - _); apply: ge0_negligible_integral => //; apply: (measurable_int mu). + exact: integrable_funepos. +exact: integrable_funeneg. +Qed. + +Lemma null_set_integral (N : set T) (f : T -> \bar R) : + measurable N -> mu.-integrable N f -> + mu N = 0 -> \int[mu]_(x in N) f x = 0. +Proof. +by move=> mN intf ?; rewrite (negligible_integral mN mN)// setDv integral_set0. Qed. End negligible_integral. @@ -4175,7 +4196,7 @@ Qed. Let mgg n : measurable_fun D (fun x => 2%:E * g x - g_ n x). Proof. -apply/emeasurable_funB => //; [by apply/measurable_funeM/(measurable_int ig)|]. +apply/emeasurable_funB => //; [by apply/measurable_funeM/(measurable_int _ ig)|]. by apply/measurableT_comp => //; exact: emeasurable_funB. Qed. @@ -4282,8 +4303,8 @@ have f_g' n x : D x -> `|f_' n x| <= g' x. apply: contrapT => fg; move: xN; apply/negP; rewrite negbK inE; left; right. by apply: subN2 => /= /(_ n Dx). have mu_ n : measurable_fun D (f_' n). - apply/(measurable_restrict (f_ n) (measurableD mD mN) _ _).1 => //. - by apply: measurable_funS (mf_ _) => // x []. + apply/measurable_restrict => //; first exact: measurableD. + exact: measurable_funS (mf_ _). have ig' : mu.-integrable D g'. apply: (integrableS measurableT) => //. apply/(integrable_mkcond g (measurableD mD mN)).1. @@ -4307,8 +4328,8 @@ split. rewrite [X in X @ \oo --> _ -> _](_ : _ = X) //. apply/funext => n; apply: ae_eq_integral => //. + apply: measurableT_comp => //; apply: emeasurable_funB => //. - apply/(measurable_restrict _ (measurableD _ _) _ _).1 => //. - by apply: (measurable_funS mD) => // x []. + apply/measurable_restrict => //; first exact: measurableD. + exact: (measurable_funS mD). + by rewrite /g_; apply: measurableT_comp => //; exact: emeasurable_funB. + exists N; split => //; rewrite -(setCK N); apply: subsetC => x /= Nx Dx. by rewrite /f_' /f' /restrict mem_set. @@ -4320,8 +4341,8 @@ split. by rewrite /f_' /restrict mem_set. set Y := (X in _ -> _ --> X); rewrite [X in _ --> X -> _](_ : _ = Y) //. apply: ae_eq_integral => //. - apply/(measurable_restrict _ (measurableD _ _) _ _).1 => //. - by apply: (measurable_funS mD) => // x []. + apply/measurable_restrict => //; first exact: measurableD. + exact: (measurable_funS mD). exists N; split => //; rewrite -(setCK N); apply: subsetC => x /= Nx Dx. by rewrite /f' /restrict mem_set. Qed. @@ -4381,8 +4402,8 @@ Let integral_measure_lt (D : set T) (mD : measurable D) (g f : T -> \bar R) : mu (D `&` [set x | g x < f x]) = 0. Proof. move=> itf itg fg; pose E j := D `&` [set x | f x - g x >= j.+1%:R^-1%:E]. -have msf := measurable_int itf. -have msg := measurable_int itg. +have msf := measurable_int _ itf. +have msg := measurable_int _ itg. have mE j : measurable (E j). rewrite /E; apply: emeasurable_fun_le => //. by apply/(emeasurable_funD msf)/measurableT_comp => //; case: mg. @@ -4424,7 +4445,7 @@ Lemma integral_ae_eq (D : set T) (mD : measurable D) (g f : T -> \bar R) : \int[mu]_(x in E) f x = \int[mu]_(x in E) g x) -> ae_eq mu D f g. Proof. -move=> fi mg fg; have mf := measurable_int fi; have gi : mu.-integrable D g. +move=> fi mg fg; have mf := measurable_int _ fi; have gi : mu.-integrable D g. apply/integrableP; split => //; apply/abse_integralP => //; rewrite -fg//. by apply/abse_integralP => //; case/integrableP : fi. have mugf : mu (D `&` [set x | g x < f x]) = 0 by apply: integral_measure_lt. @@ -5104,20 +5125,18 @@ Proof. by apply: integral_ge0 => // y _; rewrite lee_fin. Qed. Lemma indic_fubini_tonelli_FE : F = m2 \o xsection A. Proof. -rewrite funeqE => x; rewrite /= -(setTI (xsection _ _)). -rewrite -integral_indic//; last exact: measurable_xsection. -rewrite /F /fubini_F -(setTI (xsection _ _)). -rewrite integral_setI_indic; [|exact: measurable_xsection|by []]. -by apply: eq_integral => y _ /=; rewrite indicT mul1e /f !indicE mem_xsection. +apply/funext => x/=. +rewrite -[RHS]mul1e -integral_cst//; last exact: measurable_xsection. +rewrite /F /fubini_F /f [in RHS]integral_mkcond. +by apply: eq_integral => y _ /=; rewrite patchE mem_xsection indicE; case: ifPn. Qed. Lemma indic_fubini_tonelli_GE : G = m1 \o ysection A. Proof. -rewrite funeqE => y; rewrite /= -(setTI (ysection _ _)). -rewrite -integral_indic//; last exact: measurable_ysection. -rewrite /F /fubini_F -(setTI (ysection _ _)). -rewrite integral_setI_indic; [|exact: measurable_ysection|by []]. -by apply: eq_integral => x _ /=; rewrite indicT mul1e /f 2!indicE mem_ysection. +apply/funext => x/=. +rewrite -[RHS]mul1e -integral_cst//; last exact: measurable_ysection. +rewrite /G /fubini_G /f [in RHS]integral_mkcond. +by apply: eq_integral => y _ /=; rewrite patchE mem_ysection indicE; case: ifPn. Qed. Lemma indic_measurable_fun_fubini_tonelli_F : measurable_fun setT F. @@ -5811,9 +5830,9 @@ Qed. Lemma iavg_restrict f D A : measurable D -> measurable A -> iavg (f \_ D) A = ((fine (mu A))^-1)%:E * \int[mu]_(y in D `&` A) `|f y|%:E. Proof. -move=> mD mA; rewrite /iavg setIC integral_setI_indic//=; congr *%E. +move=> mD mA; rewrite /iavg setIC [in RHS]integral_mkcondr/=; congr *%E. apply: eq_integral => /= y yx1. -by rewrite patch_indic/= normrM EFinM (@ger0_norm _ (\1_D _)). +by rewrite [in RHS]restrict_EFin/= restrict_normr. Qed. Lemma iavgD f g A : measurable A -> mu A < +oo -> @@ -6259,12 +6278,17 @@ Context {R : realType}. Local Notation mu := (@lebesgue_measure R). Local Open Scope ereal_scope. -Lemma integral_set1 (f : R -> \bar R) (r : R) : \int[mu]_(x in [set r]) f x = 0. +Lemma integral_Sset1 (f : R -> \bar R) A (r : R) : A `<=` [set r] -> + (\int[mu]_(x in A) f x = 0)%E. Proof. +move=> Ar; have [->|->] := subset_set1 Ar; first by rewrite integral_set0. rewrite (eq_integral (cst (f r)))/=; last by move=> x; rewrite inE/= => ->. by rewrite integral_cst//= lebesgue_measure_set1 mule0. Qed. +Lemma integral_set1 (f : R -> \bar R) (r : R) : \int[mu]_(x in [set r]) f x = 0. +Proof. exact: (integral_Sset1 _ (@subset_refl _ _)). Qed. + Lemma ge0_integral_closed_ball (r : R) (r0 : (0 < r)%R) (f : R -> \bar R) : measurable_fun (closed_ball 0%R r : set R^o) f -> (forall x, x \in closed_ball 0%R r -> 0 <= f x) -> @@ -6321,6 +6345,7 @@ move=> mf; have [rb|rb] := leP (BRight r) b. Qed. End lebesgue_measure_integral. +Arguments integral_Sset1 {R f A} r. Section lebesgue_differentiation. Context {R : realType}. @@ -6361,7 +6386,7 @@ Unshelve. all: by end_near. Qed. Let lebesgue_differentiation_bounded f : let B k : set R^o := ball 0%R k.+1.*2%:R in - let f_ k := (f \* \1_(B k))%R in + let f_ k := f \_ (B k) in (forall k, mu.-integrable setT (EFin \o f_ k)) -> forall k, {ae mu, forall x, B k x -> lebesgue_pt (f_ k) x}. Proof. @@ -6390,9 +6415,10 @@ have intg n : mu.-integrable (B k) (EFin \o g_ n). by rewrite /g_ /sval /=; case: cid => // x []. have ifg_ub n : \int[mu]_(z in B k) `|f_ k z - g_ n z|%:E <= n.+1%:R^-1%:E. by rewrite /g_ /sval /=; case: cid => // x []. -pose g_B n := (g_ n \* \1_(B k))%R. +pose g_B n := g_ n \_ (B k). have cg_B n : {in B k, continuous (g_B n)}. - by move=> x xBk; apply: cvgM => //; [exact: cg_|exact: cvg_indic]. + move=> x xBk; rewrite /g_B patch_indic/=. + by apply: cvgM => //; [exact: cg_|exact: cvg_indic]. pose f_g_Be n : set _ := [set x | `| (f_ k \- g_B n) x |%:E >= (e / 2)%:E]. pose HLf_g_Be n : set _ := [set x | HL_maximal (f_ k \- g_B n)%R x > (e / 2)%:E]. @@ -6403,19 +6429,21 @@ have mfg n : measurable_fun setT (f_ k \- g_ n)%R. by apply: continuous_measurable_fun; exact: cg_. have locg_B n : locally_integrable [set: R] (g_B n). split; [|exact: openT|]. - - by apply: measurable_funM => //; exact: continuous_measurable_fun. + - apply/(measurable_restrictT _ _).1 => //. + exact: measurable_funS (continuous_measurable_fun (cg_ n)). - move=> K _ cK. rewrite (@le_lt_trans _ _ (\int[mu]_(x in K) `|g_ n x|%:E))//; last first. have : {within K, continuous (g_ n)} by apply: continuous_subspaceT. by move/(continuous_compact_integrable cK) => /integrableP[_ /=]. apply: ge0_le_integral => //=. + exact: compact_measurable. - + do 2 apply: measurableT_comp => //; apply: measurable_funM => //. - by apply: measurable_funTS; exact: continuous_measurable_fun. + + do 2 apply: measurableT_comp => //; apply/measurable_restrict => //. + exact: compact_measurable. + exact: measurable_funS (continuous_measurable_fun (cg_ n)). + do 2 apply: measurableT_comp => //; apply: measurable_funTS. exact: continuous_measurable_fun. - + move=> /= x Kx; rewrite /g_B /= indicE. - by case: (_ \in _); rewrite ?mulr1 ?mulr0 ?normr0 ?lee_fin. + + move=> /= x Kx; rewrite /g_B patchE; case: ifPn => //=. + by rewrite normr0 lee_fin. have locf_g_B n : locally_integrable setT (f_ k \- g_B n)%R. apply: locally_integrableB => //; split. + by move/EFin_measurable_fun : mf. @@ -6460,12 +6488,11 @@ suff: mu Ee = 0 by exists Ee. have HL_null n : mu (HLf_g_Be n) <= (3%:R / (e / 2))%:E * n.+1%:R^-1%:E. rewrite (le_trans (maximal_inequality _ _ )) ?divr_gt0//. rewrite lee_pmul2l ?lte_fin ?divr_gt0//. - set h := fun x => `|(f_ k \- g_ n) x|%:E * (\1_(B k) x)%:E. + set h := (fun x => `|(f_ k \- g_ n) x|%:E) \_ (B k). rewrite (@eq_integral _ _ _ mu setT h)//=. - by rewrite -integral_setI_indic//= setTI; exact: ifg_ub. - move=> x _; rewrite /h -EFinM /f_ /g_B -/(B k) /=. - rewrite -mulrBl normrM (@ger0_norm _ (\1_(B k) x))//. - by rewrite indicE; case: (_ \in _) => /=; rewrite !(mulr1, mulr0). + by rewrite -integral_mkcond/=; exact: ifg_ub. + move=> x _; rewrite /h restrict_EFin restrict_normr/= /g_B /f_ !patchE. + by case: ifPn => /=; [rewrite patchE => ->|rewrite subrr]. have fgn_null n : mu [set x | `|(f_ k \- g_B n) x|%:E >= (e / 2)%:E] <= (e / 2)^-1%:E * n.+1%:R^-1%:E. rewrite lee_pdivlMl ?invr_gt0 ?divr_gt0// -[X in mu X]setTI. @@ -6474,12 +6501,11 @@ have fgn_null n : mu [set x | `|(f_ k \- g_B n) x|%:E >= (e / 2)%:E] <= (EFin \o (f_ k \- g_B n)%R) (e / 2) id) => //=. by apply: measurableT_comp => //; case: (locf_g_B n). by rewrite divr_gt0. - set h := fun x => `|(f_ k \- g_ n) x|%:E * (\1_(B k) x)%:E. + set h := (fun x => `|(f_ k \- g_ n) x|%:E) \_ (B k). rewrite (@eq_integral _ _ _ mu setT h)//=. - by rewrite -integral_setI_indic//= setTI; exact: ifg_ub. - move=> x _; rewrite /h -EFinM /f_ /g_B -/(B k) /=. - rewrite -mulrBl normrM (@ger0_norm _ (\1_(B k) x))//. - by rewrite indicE; case: (_ \in _) => /=; rewrite !(mulr1,mulr0). + by rewrite -integral_mkcond/=; exact: ifg_ub. + move=> x _; rewrite /h restrict_EFin restrict_normr/= /g_B /f_ !patchE. + by case: ifPn => /=; [rewrite patchE => ->|rewrite subrr]. apply/eqP; rewrite eq_le measure_ge0 andbT. apply/lee_addgt0Pr => r r0; rewrite add0e. have incl n : Ee `<=` B k `&` (HLf_g_Be n `|` f_g_Be n) by move=> ?; apply. @@ -6508,16 +6534,15 @@ Lemma lebesgue_differentiation f : locally_integrable setT f -> Proof. move=> locf. pose B k : set R^o := ball 0%R (k.+1.*2)%:R. -pose fk k := (f \* \1_(B k))%R. +pose fk k := f \_ (B k). have mfk k : mu.-integrable setT (EFin \o fk k). case: locf => mf _ intf. apply/integrableP; split => /=. - apply/EFin_measurable_fun/measurable_funM => //. - by apply: measurable_indic; exact: measurable_ball. - under eq_integral do - rewrite /fk /= normrM EFinM indicE//= (@ger0_norm _ (_ \in _)%:R)//. - rewrite -integral_setI_indic//=; last exact: measurable_ball. - rewrite setTI -ge0_integral_closed_ball//. + by apply/EFin_measurable_fun/(measurable_restrictT _ _).1 => //=; + [exact: measurable_ball|exact: measurable_funS mf]. + rewrite (_ : (fun x => _) = (EFin \o normr \o f) \_ (B k)); last first. + by apply/funext => x; rewrite restrict_EFin/= restrict_normr. + rewrite -integral_mkcond/= -ge0_integral_closed_ball//. by rewrite intf//; exact: closed_ballR_compact. by apply: measurable_funTS; do 2 apply: measurableT_comp. have suf k : {ae mu, forall x, B k x -> lebesgue_pt (fk k) x}. @@ -6535,8 +6560,7 @@ have fE y k r : (ball 0%R k.+1%:R) y -> (r < 1)%R -> forall t, ball y r t -> f t = fk k t. rewrite /ball/= sub0r normrN => yk1 r1 t. rewrite ltr_distlC => /andP[xrt txr]. - rewrite /fk /= indicE mem_set ?mulr1//=. - rewrite /B /ball/= sub0r normrN. + rewrite /fk patchE mem_set// /B /ball/= sub0r normrN. have [t0|t0] := leP 0%R t. rewrite ger0_norm// (lt_le_trans txr)// -lerBrDr. rewrite (le_trans (ler_norm _))// (le_trans (ltW yk1))// -lerBlDr. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 473f9ac807..48b1ab735b 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1817,8 +1817,8 @@ rewrite (_ : [set~ 0] = `]-oo, 0[ `|` `]0, +oo[); last first. by rewrite -(setCitv `[0, 0]); apply/seteqP; split => [|]x/=; rewrite in_itv/= -eq_le eq_sym; [move/eqP/negbTE => ->|move/negP/eqP]. apply/measurable_funU => //; split. -- apply/(@measurable_restrict _ _ _ _ _ setT) => //. - rewrite (_ : _ \_ _ = cst (0:R))//; apply/funext => y; rewrite patchE. +- apply/measurable_restrictT => //=. + rewrite (_ : _ \_ _ = cst 0)//; apply/funext => y; rewrite patchE. by case: ifPn => //; rewrite inE/= in_itv/= => y0; rewrite ln0// ltW. - have : {in `]0, +oo[%classic, continuous (@ln R)}. by move=> x; rewrite inE/= in_itv/= andbT => x0; exact: continuous_ln. diff --git a/theories/measure.v b/theories/measure.v index e560b76172..f5d3173fb8 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -149,6 +149,8 @@ From HB Require Import structures. (* pset == the sets mset U r with U measurable and *) (* r \in [0,1] *) (* pprobability == the measurable type generated by pset *) +(* lim_sup_set F == limit superior (or upper limit) of a *) +(* sequence of sets F *) (* {outer_measure set T -> \bar R} == type of an outer measure over sets *) (* of elements of type T : Type where R is *) (* expected to be a numFieldType *) @@ -1551,19 +1553,25 @@ Lemma measurable_funTS D (f : T1 -> T2) : measurable_fun [set: T1] f -> measurable_fun D f. Proof. exact: measurable_funS. Qed. -Lemma measurable_restrict D E (f : T1 -> T2) : - measurable D -> measurable E -> D `<=` E -> - measurable_fun D f <-> measurable_fun E (f \_ D). +Lemma measurable_restrict D E (f : T1 -> T2) : measurable D -> measurable E -> + measurable_fun (E `&` D) f <-> measurable_fun E (f \_ D). Proof. -move=> mD mE DE; split => mf _ /= X mX. -- rewrite preimage_restrict; apply/measurableI => //. - by apply/measurableU/mf => //; case: ifP => // _; apply: measurableC. -- have := mf mE _ mX; rewrite preimage_restrict. - case: ifP => ptX; last first. - rewrite set0U => /(measurableI _ _ mD). - by rewrite (setIA D) (setIidl DE) setIA setIid. - rewrite setUIr setvU setTI => /(measurableI _ _ mD). - by rewrite setIA (setIidl DE) setIUr setICr set0U. +move=> mD mE; split => mf _ /= Y mY. +- rewrite preimage_restrict; case: ifPn => ptX; last first. + by rewrite set0U setIA; apply: mf => //; exact: measurableI. + rewrite setIUr; apply: measurableU. + by apply: measurableI => //; exact: measurableC. + by rewrite setIA; apply: mf => //; exact: measurableI. +- have := mf mE _ mY; rewrite preimage_restrict; case: ifP => ptY; last first. + by rewrite set0U setIA. + rewrite setUIr setvU setTI setIUr => /(measurableI _ _ mD). + by rewrite setIUr setIA setIAC setICr set0I set0U setICA setIA. +Qed. + +Lemma measurable_restrictT D (f : T1 -> T2) : measurable D -> + measurable_fun D f <-> measurable_fun [set: T1] (f \_ D). +Proof. +by move=> mD; have := measurable_restrict f mD measurableT; rewrite setTI. Qed. Lemma measurable_fun_ifT (g h : T1 -> T2) (f : T1 -> bool) @@ -3690,6 +3698,56 @@ Qed. End measure_continuity. +Definition lim_sup_set T (F : (set T)^nat) := \bigcap_n \bigcup_(j >= n) F j. + +Section borel_cantelli_realFieldType. +Context d (T : measurableType d) {R : realFieldType} + (mu : {measure set T -> \bar R}). +Implicit Types F : (set T)^nat. +Local Open Scope ereal_scope. + +Lemma lim_sup_set_ub F n : (forall k, measurable (F k)) -> + mu (lim_sup_set F) <= mu (\bigcup_(k >= n) F k). +Proof. +move=> mF; rewrite /lim_sup_set le_measure// ?inE/=. +- by apply: bigcap_measurable => // k _; exact: bigcup_measurable. +- exact: bigcup_measurable. +- exact: bigcap_inf. +Qed. + +Lemma lim_sup_set_cvg F : (forall k, measurable (F k)) -> + mu (\bigcup_(k >= 0) F k) < +oo -> + mu (\bigcup_(k >= n) F k) @[n --> \oo] --> mu (lim_sup_set F). +Proof. +move=> mF mFoo; apply: nonincreasing_cvg_mu => //. +- by move=> i; apply: bigcup_measurable => k /= _; exact: mF. +- apply: bigcap_measurable => // k _. + by apply: bigcup_measurable => j /= _; exact: mF. +- move=> m n mn; apply/subsetPset => t [k /= nk Akt]. + by exists k => //=; rewrite (leq_trans mn). +Qed. + +End borel_cantelli_realFieldType. + +Section borel_cantelli. +Context d (T : measurableType d) {R : realType} (mu : {measure set T -> \bar R}). +Implicit Types F : (set T)^nat. +Local Open Scope ereal_scope. + +Lemma lim_sup_set_cvg0 F : (forall k, measurable (F k)) -> + \sum_(n mu (lim_sup_set F) = 0. +Proof. +move=> mF bigUoo; apply/eqP; rewrite eq_le measure_ge0 andbT. +have /cvg_lim <- // : (\sum_(i <= n \oo] --> 0%E. + exact: nneseries_tail_cvg. +apply: lime_ge; first by apply/cvg_ex; exists 0; exact: nneseries_tail_cvg. +apply: nearW => n; rewrite (le_trans (lim_sup_set_ub mu n mF))//. +by apply: measure_sigma_subadditive_tail => //; + [exact: bigcup_measurable|rewrite -setC_I]. +Qed. + +End borel_cantelli. + Section g_sigma_algebra_measure_unique_trace. Context d (R : realType) (T : measurableType d). Variables (G : set (set T)) (D : set T) (mD : measurable D). diff --git a/theories/normedtype.v b/theories/normedtype.v index 8184ed7ccc..0bc32779b5 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -1286,6 +1286,12 @@ move=> xz; exists (z - x) => //=; first by rewrite subr_gt0. by move=> y /= + xy; rewrite distrC ?ger0_norm ?subr_ge0 1?ltW// ltrD2r. Qed. +Lemma nbhs_right_ltDr x e : 0 < e -> \forall y \near x ^'+, y - x < e. +Proof. +move=> e0; near=> y; rewrite ltrBlDr; near: y. +by apply: nbhs_right_lt; rewrite ltrDr. +Unshelve. all: by end_near. Qed. + Lemma nbhs_right_le x z : x < z -> \forall y \near x^'+, y <= z. Proof. by move=> xz; near do apply/ltW; apply: nbhs_right_lt. Unshelve. all: by end_near. Qed. diff --git a/theories/numfun.v b/theories/numfun.v index 4b41a20f76..5cc723fde3 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -73,6 +73,11 @@ Lemma ler_restrict D f g : (forall x, D x -> f x <= g x) -> forall x, (f \_ D) x <= (g \_ D) x. Proof. by move=> f0 x; rewrite /patch; case: ifP => // /set_mem/f0->. Qed. +Lemma restrict_normr D f : (normr \o f) \_ D = normr \o (f \_ D). +Proof. +by apply/funext => t; rewrite /= !patchE; case: ifPn =>// tD; rewrite ger0_norm. +Qed. + End restrict_lemmas. Lemma erestrict_ge0 {aT} {rT : numFieldType} (D : set aT) (f : aT -> \bar rT) : @@ -246,6 +251,24 @@ have [|fx0] := leP 0 (f x); last rewrite add0e. + by rewrite /maxe /=; case: (f x) fx0. 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 //. +- by rewrite leNgt. +- by move: fx; rewrite -leNgt => /(lt_le_trans gx); rewrite ltNge fg. +- exact: fg. +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 //. +- by rewrite leNgt. +- by move: gx; rewrite -leNgt => /(lt_le_trans fx); rewrite lteN2 ltNge fg. +- by rewrite leeN2; exact: fg. +Qed. + End funposneg_lemmas. #[global] Hint Extern 0 (is_true (0%R <= _ ^\+ _)%E) => solve [apply: funepos_ge0] : core. @@ -323,10 +346,17 @@ End indic_lemmas. Lemma patch_indic T {R : numFieldType} (f : T -> R) (D : set T) : f \_ D = (f \* \1_D)%R. Proof. -apply/funext => x /=; rewrite /patch /= indicE. +apply/funext => x /=; rewrite patchE /= indicE. by case: ifPn => _; rewrite ?(mulr1, mulr0). Qed. +Lemma epatch_indic T (R : numDomainType) (f : T -> \bar R) (D : set T) : + (f \_ D = f \* (EFin \o \1_D))%E. +Proof. +apply/funext => x; rewrite patchE/= indicE. +by case: ifPn => /=; rewrite ?mule1// mule0. +Qed. + 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. From f52a8ff5d4cf9ab935675e6a92cb8ac49cf05a73 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 5 Jul 2024 23:54:53 +0900 Subject: [PATCH 2/3] continuity of the parameterized integral on the interval --- CHANGELOG_UNRELEASED.md | 17 ++- classical/set_interval.v | 45 +++++++ theories/ftc.v | 226 ++++++++++++++++++++--------------- theories/lebesgue_integral.v | 126 ++++++++++++++++++- theories/normedtype.v | 20 ++++ 5 files changed, 331 insertions(+), 103 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4c50968597..9f0d4b2266 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -38,6 +38,16 @@ - in `realfun.v`: + lemma `nondecreasing_at_left_is_cvgr` +- in `set_interval.v`: + + lemmas `subset_itvl`, `subset_itvr`, `subset_itvS` + +- in `normedtype.v`: + + lemmas `nbhs_lt`, `nbhs_le` + +- in `lebesgue_integral.v`: + + lemmas `eq_Rintegral`, `Rintegral_mkcond`, `Rintegral_mkcondr`, `Rintegral_mkcondl`, + `le_normr_integral`, `Rintegral_setU_EFin`, `Rintegral_set0`, `Rintegral_itv_bndo_bndc`, + `Rintegral_itv_obnd_cbnd`, `Rintegral_set1`, `Rintegral_itvB` - in `constructive_ereal.v`: + lemmas `lteD2rE`, `leeD2rE` @@ -88,9 +98,10 @@ + lemmas `semi_sigma_additive_nng_induced`, `dominates_induced`, `integral_normr_continuous` - in `ftc.v`: - + definition `indefinite_integral` - + lemmas `indefinite_integral_near_left`, - `indefinite_integral_cvg_left`, `indefinite_integral_cvg_at_left` + + definition `parameterized_integral` + + lemmas `parameterized_integral_near_left`, + `parameterized_integral_left`, `parameterized_integral_cvg_at_left`, + `parameterized_integral_continuous` + corollary `continuous_FTC2` ### Changed diff --git a/classical/set_interval.v b/classical/set_interval.v index 549604f8aa..098ec28f65 100644 --- a/classical/set_interval.v +++ b/classical/set_interval.v @@ -70,6 +70,51 @@ by move: b0 b1 => [] [] /=; [exact: subset_itv_oo_co|exact: subset_itv_oo_cc| exact: subset_refl|exact: subset_itv_oo_oc]. Qed. +Lemma subset_itvl (a b c : itv_bound T) : (b <= c)%O -> + [set` Interval a b] `<=` [set` Interval a c]. +Proof. +case: c => [[|] c bc x/=|[//|_] x/=]. +- rewrite !in_itv/= => /andP[->/=]. + case: b bc => [[|]/=|[|]//] b bc. + by move=> /lt_le_trans; exact. + by move=> /le_lt_trans; exact. +- rewrite !in_itv/= => /andP[->/=]. + case: b bc => [[|]/=|[|]//] b bc. + by move=> /ltW /le_trans; apply. + by move=> /le_trans; apply. +- by move: x; rewrite le_ninfty => /eqP ->. +- by rewrite !in_itv/=; case: a => [[|]/=|[|]//] a /andP[->]. +Qed. + +Lemma subset_itvr (a b c : itv_bound T) : (c <= a)%O -> + [set` Interval a b] `<=` [set` Interval c b]. +Proof. +move=> ac x/=; rewrite !in_itv/= => /andP[ax ->]; rewrite andbT. +move: c a ax ac => [[|] c [[|]/= a ax|[|]//=]|[//|]]; rewrite ?bnd_simp. +- by move=> /le_trans; exact. +- by move=> /le_trans; apply; exact/ltW. +- by move=> /lt_le_trans; exact. +- by move=> /le_lt_trans; exact. +- by move=> [[|]|[|]//]. +Qed. + +Lemma subset_itvS (a b : itv_bound T) (c e : T) : + (BLeft c <= a)%O -> (b <= BRight e)%O -> + [set` Interval a b] `<=` [set` `[c, e]]. +Proof. +move=> ca be z/=; rewrite !in_itv/= => /andP[az zb]. +case: a ca az => [[|]/=|[|]//] a; rewrite bnd_simp => ca az. + rewrite (le_trans ca az)/=. + move: b be zb => [[|]/= b|[|]//]; rewrite bnd_simp => be. + by move=> /ltW/le_trans; exact. + by move=> /le_trans; exact. +move/ltW in az. +rewrite (le_trans ca az)/=. +move: b be zb => [[|]/= b|[|]//]; rewrite bnd_simp => be. + by move=> /ltW/le_trans; exact. +by move=> /le_trans; exact. +Qed. + Lemma interval_set1 x : `[x, x]%classic = [set x] :> set T. Proof. apply/seteqP; split => [y/=|y <-]; last by rewrite /= in_itv/= lexx. diff --git a/theories/ftc.v b/theories/ftc.v index 4456b039c5..38e865a94a 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -10,7 +10,7 @@ Require Import derive charge. (**md**************************************************************************) (* # Fundamental Theorem of Calculus for the Lebesgue Integral *) (* *) -(* indefinite_integral mu a x f := \int[mu]_(t \in `[a, x] f t) *) +(* parameterized_integral mu a x f := \int[mu]_(t \in `[a, x] f t) *) (* *) (******************************************************************************) @@ -165,7 +165,7 @@ apply: cvg_at_right_left_dnbhs. suff: ((d n)^-1 * - fine (\int[mu]_(y in E x n) (f y)%:E))%R @[n --> \oo] --> f x. apply: cvg_trans; apply: near_eq_cvg; near=> n; congr (_ *: _). - rewrite /F/= /Rintegral -fineN -fineB; last 2 first. + rewrite /F -fineN -fineB; last 2 first. by apply: integral_fune_fin_num => //; exact: integrableS intf. by apply: integral_fune_fin_num => //; exact: integrableS intf. by congr fine => /=; apply/esym; rewrite (addrC _ x); near: n. @@ -233,40 +233,34 @@ Unshelve. all: by end_near. Qed. End FTC. -Definition indefinite_integral {R : realType} +Definition parameterized_integral {R : realType} (mu : {measure set (g_sigma_algebraType (R.-ocitv.-measurable)) -> \bar R}) a x (f : R -> R) : R := (\int[mu]_(t in `[a, x]) f t)%R. -Section indefinite_integral_continuous. +Section parameterized_integral_continuous. Context {R : realType}. Notation mu := (@lebesgue_measure R). -Let int := (indefinite_integral mu). +Let int := (parameterized_integral mu). -Lemma indefinite_integral_near_left (a b : R) (e : R) (f : R -> R) : +Lemma parameterized_integral_near_left (a b : R) (e : R) (f : R -> R) : a < b -> 0 < e -> mu.-integrable `[a, b] (EFin \o f) -> - \forall c \near a, `| int a c f | < e. + \forall c \near a, a <= c -> `| int a c f | < e. Proof. move=> ab e0 intf. -have : mu.-integrable setT (EFin \o f \_`[a, b]). +have : mu.-integrable setT (EFin \o f \_ `[a, b]). by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setTI. move=> /integral_normr_continuous /(_ _ e0)[d [d0 /=]] ifab. -near=> c. -have [ca|ca] := leP c a. - rewrite /int /indefinite_integral/= /Rintegral. - rewrite (integral_Sset1 a) ?fine0 ?normr0//. - move: ca; rewrite le_eqVlt => /predU1P[->|ca]; first by rewrite interval_set1. - by rewrite set_itv_ge//= bnd_simp -ltNge. +near=> c => ac. have /ifab : (mu `[a, c] < d%:E)%E. - rewrite lebesgue_measure_itv/= lte_fin ca -EFinD lte_fin. - by move: ca; near: c; exact: nbhs_right_ltDr. + rewrite lebesgue_measure_itv/= lte_fin. + case: ifPn => // {}ac; rewrite -EFinD lte_fin. + by move: ac; near: c; exact: nbhs_right_ltDr. move=> /(_ (measurable_itv _)) {ifab}. apply: le_lt_trans. have acbc : `[a, c] `<=` `[a, b]. - rewrite (@itv_bndbnd_setU _ _ (BLeft a) (BRight c) (BRight b))// bnd_simp. - exact: ltW. - by move: ca; near: c; exact: nbhs_right_le. + by apply: subset_itvl; rewrite bnd_simp; move: ac; near: c; exact: nbhs_le. rewrite -lee_fin fineK; last first. apply: integral_fune_fin_num => //=. rewrite (_ : (fun _ => _) = abse \o ((EFin \o f) \_ `[a, b])); last first. @@ -282,45 +276,36 @@ under [in leRHS]eq_integral. rewrite /= [leRHS](_ : _ = \int[mu]_(x in `[a, c]) `| f x |%:E)%E; last first. rewrite [RHS]integralEpatch//=; apply: eq_integral => x xac/=. by rewrite restrict_EFin/= restrict_normr. +rewrite /int /parameterized_integral /=. +apply: (@le_trans _ _ ((\int[mu]_(t in `[a, c]) `|f t|))%:E). + by apply: le_normr_integral => //; exact: integrableS intf. set rhs : \bar R := leRHS. have [->|rhsoo] := eqVneq rhs +oo%E; first by rewrite leey. -rewrite /int /indefinite_integral /= /Rintegral. -set lhs := (\int[mu]_(_ in _) _)%E. -have [->|lhsNoo] := eqVneq lhs -oo%E; first by rewrite /= normr0 integral_ge0. -have lhsoo : lhs != +oo%E. - apply: contra rhsoo => /eqP lhsoo. - rewrite -leye_eq -lhsoo; apply: le_integral => //=. - - exact: integrableS intf. - - rewrite [X in integrable _ _ X](_ : _ = abse \o EFin \o f)//. - by apply: integrable_abse => /=; exact: integrableS intf. - - by move=> x _; rewrite lee_fin ler_norm. -rewrite [leLHS](_ : _ = `| lhs |)%E//; last first. - by move: lhsNoo lhsoo; rewrite /lhs /rhs; case: integral. -apply: (le_trans (le_abse_integral _ _ _)) => //=. -by apply: (measurable_funS _ acbc) => //; exact: measurable_int intf. +rewrite /rhs /Rintegral -/rhs. +rewrite fineK// fin_numE rhsoo andbT -ltNye (@lt_le_trans _ _ 0%E)//. +exact: integral_ge0. Unshelve. all: by end_near. Qed. -Lemma indefinite_integral_cvg_left a b (f : R -> R) : a < b -> +Lemma parameterized_integral_cvg_left a b (f : R -> R) : a < b -> mu.-integrable `[a, b] (EFin \o f) -> - int a x f @[x --> a] --> int a a f. + int a x f @[x --> a] --> 0. Proof. -move=> ab intf. -pose fab := f \_ `[a, b]. +move=> ab intf; pose fab := f \_ `[a, b]. have intfab : mu.-integrable `[a, b] (EFin \o fab). by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setIidr. apply/cvgrPdist_le => /= e e0; rewrite near_simpl; near=> x. -rewrite {1}/int /indefinite_integral /Rintegral /=. -rewrite (integral_Sset1 a) ?interval_set1// fine0 sub0r normrN. -apply/ltW. -by near: x; exact: (@indefinite_integral_near_left _ b). +rewrite {1}/int /parameterized_integral sub0r normrN. +have [|xa] := leP a x. + move=> ax; apply/ltW; move: ax. + by near: x; exact: (@parameterized_integral_near_left _ b). +by rewrite set_itv_ge ?Rintegral_set0 ?normr0 ?(ltW e0)// -leNgt bnd_simp. Unshelve. all: by end_near. Qed. -Lemma indefinite_integral_cvg_at_left a b (f : R -> R) : a < b -> +Lemma parameterized_integral_cvg_at_left a b (f : R -> R) : a < b -> mu.-integrable `[a, b] (EFin \o f) -> int a x f @[x --> b^'-] --> int a b f. Proof. -move=> ab intf. -pose fab := f \_ `[a, b]. +move=> ab intf; pose fab := f \_ `[a, b]. have /= int_normr_cont : forall e : R, 0 < e -> exists d : R, 0 < d /\ forall A, measurable A -> (mu A < d%:E)%E -> \int[mu]_(x in A) `|fab x| < e. @@ -328,63 +313,105 @@ have /= int_normr_cont : forall e : R, 0 < e -> by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setTI. have intfab : mu.-integrable `[a, b] (EFin \o fab). by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setIidr. -rewrite /int /indefinite_integral; apply/cvgrPdist_le => /= e e0. +rewrite /int /parameterized_integral; apply/cvgrPdist_le => /= e e0. have [d [d0 /= {}int_normr_cont]] := int_normr_cont _ e0. near=> x. rewrite [in X in X - _](@itv_bndbnd_setU _ _ _ (BRight x))//; [|by rewrite bnd_simp ltW..]. -rewrite {1}/Rintegral integral_setU_EFin//=; last 2 first. +rewrite Rintegral_setU_EFin//=; last 2 first. rewrite -itv_bndbnd_setU// ?bnd_simp; last 2 first. by near: x; exact: nbhs_left_ge. exact/ltW. - by apply/EFin_measurable_fun; apply: measurable_int intf. apply/disj_set2P; rewrite -subset0 => z/=; rewrite !in_itv/= => -[/andP[_]]. by rewrite leNgt => /negbTE ->. have xbab : `]x, b] `<=` `[a, b]. - move=> z/=; rewrite !in_itv/= => /andP[xz ->/=]. - rewrite andbT (le_trans _ (ltW xz))//. + by apply: subset_itvr; rewrite bnd_simp; near: x; exact: nbhs_left_ge. +rewrite -addrAC subrr add0r (le_trans (le_normr_integral _ _))//. + exact: integrableS intf. +rewrite [leLHS](_ : _ = (\int[mu]_(t in `]x, b]) normr (fab t)))//; last first. + apply: eq_Rintegral => //= z; rewrite inE/= in_itv/= => /andP[xz zb]. + rewrite /fab patchE ifT// inE/= in_itv/= zb andbT (le_trans _ (ltW xz))//. by near: x; exact: nbhs_left_ge. -rewrite /Rintegral fineD; last 2 first. - - rewrite fin_num_abs (le_lt_trans (le_abse_integral _ _ _)) //=. - + case/integrableP : intf => + _. - apply: measurable_funS => // z/=; rewrite !in_itv/= => /andP[->/=]. - by move=> /le_trans; apply. - + apply: integral_fune_lt_pinfty => //=. - rewrite [X in _.-integrable _ X](_ : _ = abse \o (EFin \o f))//. - apply/integrable_abse/(integrableS _ _ _ intf) => //. - move=> z/=; rewrite !in_itv/= => /andP[->/=]. - by move=> /le_trans; apply. - - rewrite fin_num_abs (le_lt_trans (le_abse_integral _ _ _)) //=. - + by case/integrableP : intf => + _; exact: measurable_funS. - + apply: integral_fune_lt_pinfty => //=. - rewrite [X in _.-integrable _ X](_ : _ = abse \o (EFin \o f))//. - exact/integrable_abse/(integrableS _ _ _ intf). -rewrite -addrAC subrr add0r. -rewrite [X in fine X](_ : _ = - (\int[mu]_(x0 in `]x, b]) (fab x0)%:E))%E//; last first. - apply: eq_integral => //= z. - rewrite inE/= in_itv/= => /andP[xz zb]. - rewrite /fab patchE ifT// inE/= in_itv/=. - rewrite zb andbT (le_trans _ (ltW xz))//. - by near: x; exact: nbhs_left_ge. -apply: ltW. -rewrite -lte_fin EFin_normr_Rintegral//=; last exact: integrableS intfab. -rewrite (le_lt_trans (le_abse_integral _ _ _))//=. - case/integrableP : intf => /EFin_measurable_fun mf _. - apply/measurableT_comp => //; apply/measurable_restrict => //=. - by rewrite setIidl//; exact: measurable_funS mf. -rewrite -[ltLHS]fineK//. -- rewrite lte_fin int_normr_cont// lebesgue_measure_itv/= lte_fin. - rewrite ifT// -EFinD lte_fin. - near: x; exists d => // z; rewrite /ball_/= => + zb. - by rewrite gtr0_norm// ?subr_gt0. -- rewrite ge0_fin_numE//; last exact: integral_ge0. - apply: integral_fune_lt_pinfty => //=. - rewrite [X in _.-integrable _ X](_ : _ = abse \o (EFin \o fab))//. - by apply: integrable_abse; exact: integrableS intfab. +apply/ltW/int_normr_cont => //. +rewrite lebesgue_measure_itv/= lte_fin. +rewrite ifT// -EFinD lte_fin. +near: x; exists d => // z; rewrite /ball_/= => + zb. +by rewrite gtr0_norm// ?subr_gt0. Unshelve. all: by end_near. Qed. -End indefinite_integral_continuous. +Lemma parameterized_integral_continuous a b (f : R -> R) : a < b -> + mu.-integrable `[a, b] (EFin \o f) -> + {within `[a,b], continuous (fun x => int a x f)}. +Proof. +move=> ab intf; apply/(continuous_within_itvP _ ab); split; last first. + split; last exact: parameterized_integral_cvg_at_left. + apply/cvg_at_right_filter. + rewrite {2}/int /parameterized_integral interval_set1 Rintegral_set1. + exact: (parameterized_integral_cvg_left ab). +pose fab := f \_ `[a, b]. +have /= int_normr_cont : forall e : R, 0 < e -> + exists d : R, 0 < d /\ + forall A, measurable A -> (mu A < d%:E)%E -> \int[mu]_(x in A) `|fab x| < e. + rewrite /= => e e0; apply: integral_normr_continuous => //=. + by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setTI. +have intfab : mu.-integrable `[a, b] (EFin \o fab). + by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setIidr. +rewrite /int /parameterized_integral => z; rewrite in_itv/= => /andP[az zb]. +apply/cvgrPdist_le => /= e e0. +rewrite near_simpl. +have [d [d0 /= {}int_normr_cont]] := int_normr_cont _ e0. +near=> x. +have [xz|xz|->] := ltgtP x z; last by rewrite subrr normr0 ltW. +- have ax : a < x. + move: xz; near: x. + exists `|z - a| => /=; first by rewrite gtr0_norm ?subr_gt0. + move=> y /= + yz. + do 2 rewrite gtr0_norm ?subr_gt0//. + rewrite ltrBlDr -ltrBlDl; apply: le_lt_trans. + by rewrite opprB addrCA subrr addr0. + rewrite Rintegral_itvB//; last 3 first. + by apply: integrableS intf => //; apply: subset_itvl; exact: ltW. + by rewrite bnd_simp ltW. + exact: ltW. + have xzab : `]x, z] `<=` `[a, b]. + by apply: subset_itvS; rewrite bnd_simp; exact/ltW. + apply: (le_trans (le_normr_integral _ _)) => //; first exact: integrableS intf. + rewrite -(setIidl xzab) Rintegral_mkcondr/=. + under eq_Rintegral do rewrite restrict_normr. + apply/ltW/int_normr_cont => //. + rewrite lebesgue_measure_itv/= lte_fin xz -EFinD lte_fin ltrBlDl. + move: xz; near: x. + exists (d / 2); first by rewrite /= divr_gt0. + move=> x/= /[swap] xz. + rewrite gtr0_norm ?subr_gt0// ltrBlDl => /lt_le_trans; apply. + by rewrite lerD2l ler_pdivrMr// ler_pMr// ler1n. ++ have ax : a < x by rewrite (lt_trans az). + have xb : x < b. + move: xz; near: x. + exists `|b - z|; first by rewrite /= gtr0_norm ?subr_gt0. + move=> y /= + yz. + by rewrite ltr0_norm ?subr_lt0// gtr0_norm ?subr_gt0// opprB ltrBlDr subrK. + rewrite -opprB normrN Rintegral_itvB ?bnd_simp; last 3 first. + by apply: integrableS intf => //; apply: subset_itvl; exact: ltW. + exact/ltW. + exact/ltW. + rewrite Rintegral_itv_obnd_cbnd//; last first. + by apply: integrableS intf => //; apply: subset_itvS => //; exact/ltW. + have zxab : `[z, x] `<=` `[a, b]. + by apply: subset_itvS; rewrite bnd_simp; exact/ltW. + apply: (le_trans (le_normr_integral _ _)) => //; first exact: integrableS intf. + rewrite -(setIidl zxab) Rintegral_mkcondr/=. + under eq_Rintegral do rewrite restrict_normr. + apply/ltW/int_normr_cont => //. + rewrite lebesgue_measure_itv/= lte_fin xz -EFinD lte_fin ltrBlDl. + move: xz; near: x. + exists (d / 2); first by rewrite /= divr_gt0. + move=> x/= /[swap] xz. + rewrite ltr0_norm ?subr_lt0// opprB ltrBlDl => /lt_le_trans; apply. + by rewrite lerD2l ler_pdivrMr// ler_pMr// ler1n. +Unshelve. all: by end_near. Qed. + +End parameterized_integral_continuous. Section corollary_FTC1. Context {R : realType}. @@ -431,10 +458,9 @@ have [k FGk] : exists k : R, {in `]a, b[, (F - G =1 cst k)%R}. move: xLy; rewrite le_eqVlt => /predU1P[->//|xy]. have [| |] := @MVT _ (F \- G)%R (F^`() - G^`())%R x y xy. - move=> z zxy; have zab : z \in `]a, b[. - rewrite !in_itv/=; move: zxy; rewrite in_itv/= => /andP[xz zy]. - rewrite (le_lt_trans _ xz)//= ?(lt_le_trans zy)//=. - + by move: yab; rewrite in_itv/= => /andP[_ /ltW]. + move: z zxy; apply: subset_itvW => //. + by move: xab; rewrite in_itv/= => /andP[/ltW]. + + by move: yab; rewrite in_itv/= => /andP[_ /ltW]. have Fz1 : derivable F z 1. by case: dF => /= + _ _; apply; rewrite inE in zab. have Gz1 : derivable G z 1 by have [|] := G'f z. @@ -464,7 +490,7 @@ have [k FGk] : exists k : R, {in `]a, b[, (F - G =1 cst k)%R}. by rewrite in_itv/= midf_lt//= midf_lt. have [c GFc] : exists c : R, forall x, x \in `]a, b[ -> (F x - G x)%R = c. by exists k => x xab; rewrite -[k]/(cst k x) -(FGk x xab). -have Ga0 : G a = 0%R by rewrite /G/= interval_set1// /Rintegral integral_set1. +have Ga0 : G a = 0%R by rewrite /G interval_set1// Rintegral_set1. case: (dF) => _ Fa Fb. have GacFa : G x @[x --> a^'+] --> (- c + F a)%R. have Fap : Filter a^'+ by exact: at_right_proper_filter. @@ -485,21 +511,25 @@ have GbcFb : G x @[x --> b^'-] --> (- c + F b)%R. rewrite (_ : (G \- F)%R + F = G)//. by apply/funext => x/=; rewrite subrK. have contF : {within `[a, b], continuous F}. - apply/continuous_within_itvP => //; split => // z zab. + apply/(continuous_within_itvP _ ab); split; last exact: (conj Fa Fb). + move=> z zab. apply/differentiable_continuous/derivable1_diffP. - by case: dF => /= + _ _; exact. + by case: dF => /= dF _ _; apply: dF. have iabfab : mu.-integrable `[a, b] (EFin \o fab). by rewrite -restrict_EFin; apply/integrable_restrict => //; rewrite setIidr. have Ga : G x @[x --> a^'+] --> G a. - by have /left_right_continuousP[] := indefinite_integral_cvg_left ab iabfab. + have := parameterized_integral_cvg_left ab iabfab. + rewrite (_ : 0 = G a)%R. + by move=> /left_right_continuousP[]. + by rewrite /G interval_set1 Rintegral_set1. have Gb : G x @[x --> b^'-] --> G b. - exact: (indefinite_integral_cvg_at_left ab iabfab). + exact: (parameterized_integral_cvg_at_left ab iabfab). have cE : c = F a. - apply/eqP;rewrite -(opprK c) eq_sym -addr_eq0 addrC. + apply/eqP; rewrite -(opprK c) eq_sym -addr_eq0 addrC. by have := cvg_unique _ GacFa Ga; rewrite Ga0 => ->. have GbFbc : G b = (F b - c)%R. by have := cvg_unique _ GbcFb Gb; rewrite addrC => ->. -rewrite -EFinB -cE -GbFbc /G/= /Rintegral/= fineK//. +rewrite -EFinB -cE -GbFbc /G /Rintegral/= fineK//. rewrite integralEpatch//=. by under eq_integral do rewrite restrict_EFin. exact: integral_fune_fin_num. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 32b518904b..0a8b66a1db 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -2919,9 +2919,9 @@ Definition Rintegral (D : set T) (f : T -> R) := End Rintegral. Notation "\int [ mu ]_ ( x 'in' D ) f" := - (Rintegral [the measure _ _ of mu] D (fun x => f)) : ring_scope. + (Rintegral mu D (fun x => f)) : ring_scope. Notation "\int [ mu ]_ x f" := - (Rintegral [the measure _ _ of mu] setT (fun x => f)) : ring_scope. + (Rintegral mu setT (fun x => f)) : ring_scope. HB.lock Definition integrable {d} {T : measurableType d} {R : realType} (mu : set T -> \bar R) D f := @@ -4349,6 +4349,74 @@ Qed. End dominated_convergence_theorem. +Section Rintegral. +Context d {T : measurableType d} {R : realType}. +Variable mu : {measure set T -> \bar R}. + +Lemma eq_Rintegral D g f : {in D, f =1 g} -> + \int[mu]_(x in D) f x = \int[mu]_(x in D) g x. +Proof. +move=> fg; rewrite /Rintegral; congr fine. +by apply: eq_integral => /= x xD; rewrite fg. +Qed. + +Lemma Rintegral_mkcond D f : \int[mu]_(x in D) f x = \int[mu]_x (f \_ D) x. +Proof. +rewrite {1}/Rintegral integral_mkcond/=. +by under eq_integral do rewrite restrict_EFin. +Qed. + +Lemma Rintegral_mkcondr D P f : + \int[mu]_(x in D `&` P) f x = \int[mu]_(x in D) (f \_ P) x. +Proof. +rewrite {1}/Rintegral integral_mkcondr. +by under eq_integral do rewrite restrict_EFin. +Qed. + +Lemma Rintegral_mkcondl D P f : + \int[mu]_(x in P `&` D) f x = \int[mu]_(x in D) (f \_ P) x. +Proof. by rewrite setIC Rintegral_mkcondr. Qed. + +Lemma le_normr_integral A f : measurable A -> mu.-integrable A (EFin \o f) -> + (`|\int[mu]_(t in A) f t| <= \int[mu]_(t in A) `|f t|)%R. +Proof. +move=> mA /integrableP[mf ifoo]. +rewrite -lee_fin; apply: le_trans. + apply: (le_trans _ (le_abse_integral mu mA mf)). + rewrite /abse. + have [/fineK <-//|] := boolP (\int[mu]_(x in A) (EFin \o f) x \is a fin_num)%E. + by rewrite fin_numEn => /orP[|] /eqP ->; rewrite leey. +rewrite /Rintegral. +move: ifoo. +rewrite -ge0_fin_numE; last exact: integral_ge0. +move/fineK ->. +by apply: ge0_le_integral => //=; do 2 apply: measurableT_comp => //; + exact/EFin_measurable_fun. +Qed. + +Lemma Rintegral_setU_EFin (A B : set T) (f : T -> R) : + d.-measurable A -> d.-measurable B -> + mu.-integrable (A `|` B) (EFin \o f) -> [disjoint A & B] -> + \int[mu]_(x in (A `|` B)) f x = \int[mu]_(x in A) f x + \int[mu]_(x in B) f x. +Proof. +move=> mA mB mf AB; rewrite /Rintegral integral_setU_EFin//; last first. + exact/EFin_measurable_fun/(measurable_int mu). +have mAf : mu.-integrable A (EFin \o f). + by apply: integrableS mf => //; exact: measurableU. +have mBf : mu.-integrable B (EFin \o f). + by apply: integrableS mf => //; exact: measurableU. +move/integrableP : mAf => [mAf itAfoo]. +move/integrableP : mBf => [mBf itBfoo]. +rewrite fineD//. +- by rewrite fin_num_abs (le_lt_trans _ itAfoo)//; exact: le_abse_integral. +- by rewrite fin_num_abs (le_lt_trans _ itBfoo)//; exact: le_abse_integral. +Qed. + +Lemma Rintegral_set0 (f : T -> R) : (\int[mu]_(x in set0) f x = 0)%R. +Proof. by rewrite /Rintegral integral_set0. Qed. + +End Rintegral. + Section ae_ge0_le_integral. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType). @@ -6347,6 +6415,60 @@ Qed. End lebesgue_measure_integral. Arguments integral_Sset1 {R f A} r. +Section Rintegral_lebesgue_measure. +Context {R : realType}. +Notation mu := (@lebesgue_measure R). +Implicit Type f : R -> R. + +Lemma Rintegral_itv_bndo_bndc (a : itv_bound R) (r : R) f : + mu.-integrable [set` Interval a (BRight r)] (EFin \o f) -> + \int[mu]_(x in [set` Interval a (BLeft r)]) (f x) = + \int[mu]_(x in [set` Interval a (BRight r)]) (f x). +Proof. +move=> mf; rewrite /Rintegral integral_itv_bndo_bndc//. +by apply/EFin_measurable_fun; exact: (measurable_int mu). +Qed. + +Lemma Rintegral_itv_obnd_cbnd (r : R) (b : itv_bound R) f : + mu.-integrable [set` Interval (BLeft r) b] (EFin \o f) -> + \int[mu]_(x in [set` Interval (BRight r) b]) (f x) = + \int[mu]_(x in [set` Interval (BLeft r) b]) (f x). +Proof. +move=> mf; rewrite /Rintegral integral_itv_obnd_cbnd//. +by apply/EFin_measurable_fun; exact: (measurable_int mu). +Qed. + +Lemma Rintegral_set1 f (r : R) : \int[mu]_(x in [set r]) f x = 0. +Proof. by rewrite /Rintegral integral_set1. Qed. + +Lemma Rintegral_itvB f (a b : itv_bound R) x : + mu.-integrable [set` (Interval a b)] (EFin \o f) -> + (a <= BRight x)%O -> (BRight x <= b)%O -> + \int[mu]_(t in [set` Interval a b]) f t - + \int[mu]_(t in [set` Interval a (BRight x)]) f t = + \int[mu]_(x in [set` Interval (BRight x) b]) f x. +Proof. +move=> itf; rewrite le_eqVlt => /predU1P[ax|ax xb]. + rewrite ax => _; rewrite [in X in _ - X]set_itv_ge ?bnd_simp//. + by rewrite Rintegral_set0 subr0. +rewrite (@itv_bndbnd_setU _ _ _ (BLeft x)); last 2 first. + by case: a ax {itf} => -[]//. + by rewrite (le_trans _ xb)// bnd_simp. +rewrite Rintegral_setU_EFin//=. +- rewrite addrAC Rintegral_itv_bndo_bndc//; last first. + by apply: integrableS itf => //; exact: subset_itvl. + rewrite subrr add0r Rintegral_itv_obnd_cbnd//. + apply: integrableS itf => //; apply: subset_itvr. + by case: a ax => -[]. +- rewrite -itv_bndbnd_setU//. + by case: a ax {itf} => -[]//. + by rewrite (le_trans _ xb)// bnd_simp. +- apply/disj_setPS => y; rewrite /= !in_itv/= => -[/andP[_ yx] /andP[]]. + by rewrite leNgt yx. +Qed. + +End Rintegral_lebesgue_measure. + Section lebesgue_differentiation. Context {R : realType}. Local Notation mu := (@lebesgue_measure R). diff --git a/theories/normedtype.v b/theories/normedtype.v index 0bc32779b5..79849cd5d0 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -1139,6 +1139,26 @@ Proof. by move=> Lf /continuity_pt_cvg; apply. Qed. End analysis_struct. +Section nbhs_lt_le. +Context {R : realType}. +Implicit Types x z : R. + +Lemma nbhs_lt x z : x < z -> \forall y \near x, x <= y -> y < z. +Proof. +move=> xz; near=> y. +rewrite le_eqVlt => /predU1P[<-//|]. +near: y; exists (z - x) => /=; first by rewrite subr_gt0. +move=> y/= /[swap] xy; rewrite ltr0_norm ?subr_lt0//. +by rewrite opprD addrC ltrBlDr subrK opprK. +Unshelve. all: by end_near. Qed. + +Lemma nbhs_le x z : x < z -> \forall y \near x, x <= y -> y <= z. +Proof. +by move=> xz; apply: filterS (nbhs_lt xz) => y /[apply] /ltW. +Qed. + +End nbhs_lt_le. + Section open_closed_sets. (* TODO: duplicate theory within the subspace topology of Num.real in a numDomainType *) From 39d9d05733f002e89952a8259e0e35e8bd8f3ff8 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 18 Jul 2024 21:32:58 +0900 Subject: [PATCH 3/3] changelog, doc, fixes --- CHANGELOG_UNRELEASED.md | 11 +++++------ theories/charge.v | 18 +++++++++++++----- theories/ftc.v | 8 +++++++- theories/lebesgue_stieltjes_measure.v | 4 +++- theories/measure.v | 3 ++- 5 files changed, 30 insertions(+), 14 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 9f0d4b2266..568d574377 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -56,12 +56,6 @@ - in `mathcomp_extra.v`: + lemma `invf_ltp` -### Changed - -- in `topology.v`: - + lemmas `subspace_pm_ball_center`, `subspace_pm_ball_sym`, - `subspace_pm_ball_triangle`, `subspace_pm_entourage` turned - into local `Let`'s - in `classical_sets.v`: + lemmas `setC_I`, `bigcup_subset` @@ -106,6 +100,11 @@ ### Changed +- in `topology.v`: + + lemmas `subspace_pm_ball_center`, `subspace_pm_ball_sym`, + `subspace_pm_ball_triangle`, `subspace_pm_entourage` turned + into local `Let`'s + - in `lebesgue_integral.v`: + lemma `measurable_int`: argument `mu` now explicit diff --git a/theories/charge.v b/theories/charge.v index 743c458d1c..0e35a7dd72 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -13,7 +13,11 @@ Require Import esum measure realfun lebesgue_measure lebesgue_integral. (* NB: See CONTRIBUTING.md for an introduction to HB concepts and commands. *) (* *) (* This file contains a formalization of charges (a.k.a. signed measures) and *) -(* their theory (Hahn decomposition theorem, etc.). *) +(* their theory (Hahn decomposition theorem, Radon-Nikodym derivative, etc.). *) +(* *) +(* Reference: *) +(* - Y. Ishiguro, R. Affeldt. The Radon-Nikodym Theorem and the Lebesgue- *) +(* Stieltjes measure in Coq. Computer Software 41(2) 2024 *) (* *) (* ## Structures for functions on classes of sets *) (* ``` *) @@ -59,6 +63,10 @@ Require Import esum measure realfun lebesgue_measure lebesgue_integral. (* decomposition nuPN: hahn_decomposition nu P N *) (* charge_variation nuPN == variation of the charge nu *) (* := jordan_pos nuPN \+ jordan_neg nuPN *) +(* induced intf == charge induced by a function f : T -> \bar R *) +(* R has type realType; T is a measurableType. *) +(* intf is a proof that f is integrable over *) +(* [set: T] *) (* 'd nu '/d mu == Radon-Nikodym derivative of nu w.r.t. mu *) (* (the scope is charge_scope) *) (* ``` *) @@ -1073,12 +1081,12 @@ move=> /choice[F /= H]. have mF i : measurable (F i) by have [] := H i. have : mu (lim_sup_set F) = 0. apply: lim_sup_set_cvg0 => //. - have h : \sum_(0 <= n < k) (1 / 2 ^+ n.+1)%:E @[k --> \oo] --> (1 : \bar R). + have h : \sum_(0 <= n < k) (1 / 2 ^+ n.+1)%:E @[k --> \oo] --> (1%E : \bar R). apply/fine_cvgP; split. apply: nearW => /= n; rewrite sum_fin_num//. by apply/allP => /= r /mapP[/= k _] ->. - under eq_fun do rewrite sumEFin. have := @cvg_geometric_series_half R 1 0; rewrite {1}/series/= expr0 divr1. + under [in X in _ -> X]eq_fun do rewrite sumEFin. by under eq_fun do under eq_bigr do rewrite addn1 natrX. apply: (@le_lt_trans _ _ (\sum_(0 <= n = e%:E by exact: lt_le_trans. have echarge n : e%:E <= charge_variation nuPN (\bigcup_(j >= n) F j). have [_ _ /le_trans] := H n; apply. rewrite le_measure// ?inE//; first exact: bigcup_measurable. - by apply: bigcup_sup => //=. -have /(_ _ _)/cvg_lim <-// := @lim_sup_set_cvg _ _ _ (charge_variation nuPN) F. + by apply: bigcup_sup => /=. +have /(_ _ _)/cvg_lim <-// := lim_sup_set_cvg (charge_variation nuPN) F. apply: lime_ge. apply: ereal_nonincreasing_is_cvgn => a b ab. rewrite le_measure ?inE//; [exact: bigcup_measurable| diff --git a/theories/ftc.v b/theories/ftc.v index 38e865a94a..5d0138223c 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -10,6 +10,12 @@ Require Import derive charge. (**md**************************************************************************) (* # Fundamental Theorem of Calculus for the Lebesgue Integral *) (* *) +(* NB: See CONTRIBUTING.md for an introduction to HB concepts and commands. *) +(* *) +(* This file provides a proof of the first fundamental theorem of calculus *) +(* for the Lebesgue integral. We derive from this theorem a corollary to *) +(* compute the definite integral of continuous functions. *) +(* *) (* parameterized_integral mu a x f := \int[mu]_(t \in `[a, x] f t) *) (* *) (******************************************************************************) @@ -341,7 +347,7 @@ Unshelve. all: by end_near. Qed. Lemma parameterized_integral_continuous a b (f : R -> R) : a < b -> mu.-integrable `[a, b] (EFin \o f) -> - {within `[a,b], continuous (fun x => int a x f)}. + {within `[a, b], continuous (fun x => int a x f)}. Proof. move=> ab intf; apply/(continuous_within_itvP _ ab); split; last first. split; last exact: parameterized_integral_cvg_at_left. diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index a65d2e14c1..958eab237f 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -13,8 +13,10 @@ Require Import real_interval measure realfun. (* This file contains a formalization of the Lebesgue-Stieltjes measure using *) (* the Measure Extension theorem from measure.v. *) (* *) -(* Reference: *) +(* References: *) (* - Achim Klenke, Probability Theory 2nd edition, 2014 *) +(* - Y. Ishiguro, R. Affeldt. The Radon-Nikodym Theorem and the Lebesgue- *) +(* Stieltjes measure in Coq. Computer Software 41(2) 2024 *) (* *) (* ``` *) (* right_continuous f == the function f is right-continuous *) diff --git a/theories/measure.v b/theories/measure.v index f5d3173fb8..75180d0987 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -3701,7 +3701,7 @@ End measure_continuity. Definition lim_sup_set T (F : (set T)^nat) := \bigcap_n \bigcup_(j >= n) F j. Section borel_cantelli_realFieldType. -Context d (T : measurableType d) {R : realFieldType} +Context {d} {T : measurableType d} {R : realFieldType} (mu : {measure set T -> \bar R}). Implicit Types F : (set T)^nat. Local Open Scope ereal_scope. @@ -3728,6 +3728,7 @@ move=> mF mFoo; apply: nonincreasing_cvg_mu => //. Qed. End borel_cantelli_realFieldType. +Arguments lim_sup_set_cvg {d T R} mu F. Section borel_cantelli. Context d (T : measurableType d) {R : realType} (mu : {measure set T -> \bar R}).