diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4d8fa452a..7f3039228 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -71,10 +71,12 @@ - in `classical_sets.v`: + lemmas `properW`, `properxx` - in file `lebesgue_integral.v`, - + new lemmas `integral_le_bound`, `open_itvoo_subset`, - `open_itvcc_subset`, `continuous_compact_integrable`, and + + new lemmas `integral_le_bound`, `continuous_compact_integrable`, and `lebesgue_differentiation_continuous`. +- in `normedtype.v`: + + lemmas `open_itvoo_subset`, `open_itvcc_subset` + ### Changed - `mnormalize` moved from `kernel.v` to `measure.v` and generalized diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 1341ea5d2..d4fa3655d 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -4223,6 +4223,22 @@ Qed. End ae_ge0_le_integral. +Section integral_bounded. +Context d {T : measurableType d} {R : realType}. +Variable mu : {measure set T -> \bar R}. +Local Open Scope ereal_scope. + +Lemma integral_le_bound (D : set T) (f : T -> \bar R) (M : \bar R) : + measurable D -> measurable_fun D f -> 0 <= M -> + {ae mu, forall x, D x -> `|f x| <= M} -> + \int[mu]_(x in D) `|f x| <= M * mu D. +Proof. +move=> mD mf M0 dfx; rewrite -integral_cst => //. +by apply: ae_ge0_le_integral => //; exact: measurableT_comp. +Qed. + +End integral_bounded. + Section integral_ae_eq. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}). @@ -5346,121 +5362,83 @@ Qed. End sfinite_fubini. Arguments sfinite_Fubini {d d' X Y R} m1 m2 f. -Section integral_bounded. - -Lemma integral_le_bound d (R : realType) (T : measurableType d) - (mu : {measure set T -> \bar R}) (D : set T) (f : T -> \bar R) (M : R) : - measurable D -> measurable_fun D f -> - (0 <= M%:E)%E -> ({ae mu, forall x, D x -> `|f x| <= M%:E})%E -> - (\int[mu]_(x in D) `|f x| <= M%:E * mu D)%E. -Proof. -move=> mD intf M0 dfx; rewrite -integral_cst => //. -apply: ae_ge0_le_integral => //. -by apply: measurableT_comp => //; case/integrableP:intf. -Qed. - -End integral_bounded. - -Lemma open_itvoo_subset {R : realType} (A : set R) (x : R) : - open A -> A x -> \forall r \near 0^'+, `]x-r, x+r[ `<=` A. -Proof. -move=> oA Ax; case/(_ _ Ax): oA => _/posnumP[r] /subset_ball_prop_in_itv xrA. -exists r%:num => //= k; rewrite /= distrC subr0 set_itvoo => /ltr_normlW kr k0. -apply: (subset_trans _ xrA); apply: subset_itvW. - by apply: ler_sub => //; apply: ltW. -by apply: ler_add => //; apply: ltW. -Qed. - -Lemma open_itvcc_subset {R : realType} (A : set R) (x : R) : - open A -> A x -> \forall r \near 0^'+, `[x-r, x+r] `<=` A. -Proof. -move=> oA Ax; case/(_ _ Ax): oA => _/posnumP[r]. -have -> : (r%:num = 2 * (r%:num/2)) by rewrite mulrC -mulrA mulVf // mulr1. -move/subset_ball_prop_in_itvcc => xrA; exists (r%:num/2) => //= k. -rewrite /= distrC subr0 set_itvcc => /ltr_normlW kr k0. -move=> z /andP [xkz zxk]; apply: xrA => //; rewrite in_itv /=. -apply/andP; split. - by apply: (le_trans _ xkz); apply: ler_sub => //; exact: ltW. -by apply: (le_trans zxk); apply: ler_add => //; exact: ltW. -Qed. - Section lebesgue_differentiation. Context (rT : realType). Let mu := [the measure _ _ of @lebesgue_measure rT]. Let R := [the measurableType _ of measurableTypeR rT]. -Lemma continuous_compact_integrable (f : R -> R^o) (A : set R^o): +Lemma continuous_compact_integrable (f : R -> R^o) (A : set R^o) : compact A -> {within A, continuous f} -> mu.-integrable A (EFin \o f). Proof. -move=> cptA ctsfA; apply/integrableP; have mA : measurable A. - by apply:closed_measurable; apply: compact_closed => //; exact: Rhausdorff. -split. - by apply: measurableT_comp => //; apply: subspace_continuous_measurable_fun. +move=> cptA ctsfA; have mA := compact_measurable cptA; apply/integrableP; split. + by apply: measurableT_comp => //; exact: subspace_continuous_measurable_fun. have /compact_bounded [M [_ mrt]] := continuous_compact ctsfA cptA. apply: le_lt_trans. - apply (@integral_le_bound _ _ _ _ _ _ (`|M| + 1)) => //. - by apply: measurableT_comp => //; apply: subspace_continuous_measurable_fun. - apply: aeW => /= z Az; rewrite lee_fin; apply: mrt => //. - apply: (@lt_le_trans _ _ (M + 1)); by rewrite ?ltr_addl // ler_add// ler_norm. -case/compact_bounded: cptA => N [_ N1x]; have AN1: A `<=` `[- (`|N|+1), `|N|+1]. - move=> z Az; rewrite set_itvcc /= -ler_norml; apply: N1x => //. - by apply: (@lt_le_trans _ _ (N + 1)); rewrite ?ltr_addl // ler_add// ler_norm. + apply (@integral_le_bound _ _ _ _ _ _ (`|M| + 1)%:E) => //. + by apply: measurableT_comp => //; exact: subspace_continuous_measurable_fun. + by apply: aeW => /= z Az; rewrite lee_fin mrt // ltr_spaddr// ler_norm. +case/compact_bounded : cptA => N [_ N1x]. +have AN1 : A `<=` `[- (`|N| + 1), `|N| + 1]. + by move=> z Az; rewrite set_itvcc /= -ler_norml N1x// ltr_spaddr// ler_norm. apply: (@le_lt_trans _ _ (_ * _)%E). by rewrite lee_pmul; last by apply: (le_measure _ _ _ AN1); rewrite inE. -by rewrite /= lebesgue_measure_itv hlength_itv /= -fun_if -EFinM ltry. +by rewrite /= lebesgue_measure_itv hlength_itv /= -fun_if -EFinM ltry. Qed. Lemma lebesgue_differentiation_continuous (f : R -> rT^o) (A : set R) (x : R) : - open A -> mu.-integrable A (EFin \o f) -> {for x, continuous f} -> A x -> - (fun r => 1/(2*r) * \int[mu]_(z in `[x-r,x+r]) f z) @ 0^'+ --> (f x:R^o). -Proof. -have ritv r : 0 < r -> mu (`[x-r,x+r]%classic) = (2*r)%:E. + open A -> mu.-integrable A (EFin \o f) -> {for x, continuous f} -> A x -> + (fun r => 1 / (2 * r) * \int[mu]_(z in `[x - r, x + r]) f z) @ 0^'+ --> + (f x : R^o). +Proof. +have ritv r : 0 < r -> mu (`[x - r, x + r]%classic) = (2 * r)%:E. move=> /gt0_cp rE; rewrite /= lebesgue_measure_itv hlength_itv /= lte_fin. rewrite ler_lt_add // ?rE // -EFinD; congr (_ _). by rewrite opprB addrAC [_ - _]addrC addrA subrr add0r mulr2n mulrDl ?mul1r. -move=> oA intf ctsfx Ax; apply: (@cvg_zero rT [pseudoMetricNormedZmodType R of rT^o]). -apply/cvgrPdist_le => eps epos; have := @nbhs_right_gt rT 0; apply: filter_app. -have ? : Filter (nbhs (0:R)^'+) by exact: at_right_proper_filter. -move/cvgrPdist_le/(_ eps epos)/at_right_in_segment : ctsfx; apply: filter_app. -apply: (filter_app _ _ (open_itvcc_subset oA Ax)). -have mA : measurable A by exact: open_measurable. +move=> oA intf ctsfx Ax. +apply: (@cvg_zero rT [pseudoMetricNormedZmodType R of rT^o]). +apply/cvgrPdist_le => eps epos; apply: filter_app (@nbhs_right_gt rT 0). +have ? : Filter (nbhs (0 : R)^'+) := at_right_proper_filter 0. +move/cvgrPdist_le/(_ eps epos)/at_right_in_segment : ctsfx; apply: filter_app. +apply: filter_app (open_itvcc_subset oA Ax). +have mA : measurable A := open_measurable oA. near=> r => xrA; rewrite addrfctE opprfctE => feps rp. -have cptxr : compact `[x-r, x + r] by exact: segment_compact. -rewrite distrC subr0; have r20 : 0 <= 1/(2*r) by rewrite ?divr_ge0 // ?mulr_ge0. -have -> : f x = 1/(2*r) * \int[mu]_(z in `[x-r,x+r]) cst (f x) z. - rewrite /Rintegral /= integral_cst // ritv //= [f x * _]mulrC mulrA. - by rewrite div1r mulVr ?mul1r ?unitfE ?mulf_neq0. -have intRf : mu.-integrable `[x-r, x+r] (EFin \o f). +have cptxr : compact `[x - r, x + r] := @segment_compact _ _ _. +rewrite distrC subr0. +have r20 : 0 <= 1 / (2 * r) by rewrite ?divr_ge0 // ?mulr_ge0. +have -> : f x = 1 / (2 * r) * \int[mu]_(z in `[x - r, x + r]) cst (f x) z. + rewrite /Rintegral /= integral_cst // ritv //=. + by rewrite mulrC mul1r -mulrA divff ?mulr1// mulf_neq0. +have intRf : mu.-integrable `[x - r, x + r] (EFin \o f). exact: (@integrableS _ _ _ mu _ _ _ _ _ xrA intf). rewrite /= -mulrBr -fineB; first last. -- rewrite integral_fune_fin_num // continuous_compact_integrable //. - by move=> ?; exact: cvg_cst. -- by rewrite integral_fune_fin_num //. +- rewrite integral_fune_fin_num// continuous_compact_integrable// => ?. + exact: cvg_cst. +- by rewrite integral_fune_fin_num. rewrite -integralB_EFin //; first last. -- by apply: continuous_compact_integrable => // ?; exact: cvg_cst. + by apply: continuous_compact_integrable => // ?; exact: cvg_cst. under [fun _ => adde _ _ ]eq_fun => ? do rewrite -EFinD. -have int_fx : mu.-integrable `[(x - r)%R, (x + r)%R] (fun z => (f z - f x)%:E). +have int_fx : mu.-integrable `[x - r, x + r] (fun z => (f z - f x)%:E). under [fun z => (f z - _)%:E]eq_fun => ? do rewrite EFinB. - apply: integrableB => //; apply: continuous_compact_integrable =>//. - by move=> ?; exact: cvg_cst. + rewrite integrableB// continuous_compact_integrable// => ?. + exact: cvg_cst. rewrite normrM [ `|_/_| ]ger0_norm // -fine_abse //; first last. by rewrite integral_fune_fin_num. -suff : (\int[mu]_(z in `[(x-r)%R,(x+r)%R]) `|(f z - f x)|%:E <= +suff : (\int[mu]_(z in `[(x - r)%R, (x + r)%R]) `|(f z - f x)|%:E <= (2 * r * eps)%:E)%E. move=> intfeps; apply: le_trans. apply: (ler_pmul r20 _ (le_refl _)); first exact: fine_ge0. apply: fine_le; last apply: le_abse_integral => //. - by rewrite abse_fin_num; exact: integral_fune_fin_num. - by apply: integral_fune_fin_num => //; exact: integrable_abse. - - by case/integrableP:int_fx. + - by case/integrableP: int_fx. rewrite div1r ler_pdivr_mull -[_ * _]/(fine (_%:E)); last exact: mulr_gt0. by rewrite fine_le // integral_fune_fin_num // integrable_abse. apply: le_trans. - apply:(@integral_le_bound _ _ _ _ _ (fun z => (f z - f x)%:E) eps) => //. + apply: (@integral_le_bound _ _ _ _ _ (fun z => (f z - f x)%:E) eps%:E) => //. - by case/integrableP: int_fx. - exact: ltW. - by apply: aeW => ? ?; rewrite /= lee_fin distrC; apply: feps. by rewrite ritv //= -EFinM lee_fin mulrC. Unshelve. all: by end_near. Qed. -End lebesgue_differentiation. \ No newline at end of file +End lebesgue_differentiation. diff --git a/theories/normedtype.v b/theories/normedtype.v index 7d0e15850..e6ac94fe1 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -1951,6 +1951,33 @@ End at_left_right. Notation "x ^'-" := (at_left x) : classical_set_scope. Notation "x ^'+" := (at_right x) : classical_set_scope. +Section open_itv_subset. +Context {R : realType}. +Variables (A : set R) (x : R). + +Lemma open_itvoo_subset : + open A -> A x -> \forall r \near 0^'+, `]x - r, x + r[ `<=` A. +Proof. +move=> /[apply] -[] _/posnumP[r] /subset_ball_prop_in_itv xrA. +exists r%:num => //= k; rewrite /= distrC subr0 set_itvoo => /ltr_normlW kr k0. +by apply/(subset_trans _ xrA)/subset_itvW; + [rewrite ler_sub//; exact: ltW | rewrite ler_add//; exact: ltW]. +Qed. + +Lemma open_itvcc_subset : + open A -> A x -> \forall r \near 0^'+, `[x - r, x + r] `<=` A. +Proof. +move=> /[apply] -[] _/posnumP[r]. +have -> : r%:num = 2 * (r%:num / 2) by rewrite mulrCA divff// mulr1. +move/subset_ball_prop_in_itvcc => /= xrA; exists (r%:num / 2) => //= k. +rewrite /= distrC subr0 set_itvcc => /ltr_normlW kr k0. +move=> z /andP [xkz zxk]; apply: xrA => //; rewrite in_itv/=; apply/andP; split. + by rewrite (le_trans _ xkz)// ler_sub// ltW. +by rewrite (le_trans zxk)// ler_add// ltW. +Qed. + +End open_itv_subset. + Section at_left_right_topologicalType. Variables (R : numFieldType) (V : topologicalType) (f : R -> V) (x : R).