From 0e947534b9024286c6a4f78a03802f28e588a684 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 11 Jan 2024 16:25:01 +0900 Subject: [PATCH 1/6] lebesgue differentiation, ftc, lebesgue's density --- theories/charge.v | 2 +- theories/lebesgue_integral.v | 1167 +++++++++++++++++++++++++++++++++- theories/realfun.v | 2 +- 3 files changed, 1163 insertions(+), 8 deletions(-) diff --git a/theories/charge.v b/theories/charge.v index d94d9cf2f8..49759ecf32 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -669,7 +669,7 @@ have [v [v0 Pv]] : {v : nat -> elt_type | v 0%N = exist _ (A0, d_ set0, A0) (And4 mA0 A0D (d_ge0 set0) A0d0) /\ forall n, elt_rel (v n) (v n.+1)}. apply: dependent_choice_Type => -[[[A' ?] U] [/= mA' A'D]]. - have [A1 [mA1 A1DU A1t1] ] := next_elt U. + have [A1 [mA1 A1DU A1t1]] := next_elt U. have A1D : A1 `<=` D by apply: (subset_trans A1DU); apply: subDsetl. by exists (exist _ (A1, d_ U, U `|` A1) (And4 mA1 A1D (d_ge0 U) A1t1)). have Ubig n : U_ (v n) = \big[setU/set0]_(i < n.+1) A_ (v i). diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index a10b224384..718e31ad19 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -4,7 +4,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. 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 function_spaces. +Require Import esum measure lebesgue_measure numfun realfun function_spaces. (**md**************************************************************************) (* # Lebesgue Integral *) @@ -58,6 +58,12 @@ Require Import esum measure lebesgue_measure numfun function_spaces. (* HL_maximal == the Hardy–Littlewood maximal operator *) (* input: real number-valued function *) (* output: extended real number-valued function *) +(* davg f x r == "deviated average" of the real-valued function *) +(* f over ball x r *) +(* lim_sup_davg f x := lime_sup (davg f x) 0 *) +(* lebesgue_pt f x == Lebesgue point at x of the real-valued *) +(* function f *) +(* nicely_shrinking x E == the sequence of sets E is nicely shrinking to x *) (* ```` *) (* *) (******************************************************************************) @@ -1809,7 +1815,7 @@ exists (\bigcup_(i in range f) dK i); split. by apply: continuous_subspaceT => ?; exact: cvg_cst. Qed. -Let measurable_almost_continuous' (f : R -> R) (eps : rT) : +Let measurable_almost_continuous' (f : rT -> rT) (eps : rT) : (0 < eps)%R -> measurable_fun A f -> exists K, [/\ measurable K, K `<=` A, mu (A `\` K) < eps%:E & {within K, continuous f}]. @@ -1852,7 +1858,7 @@ near_simpl; apply: nearW => // n; apply: (@continuous_subspaceW _ _ _ (gK n)). by have [] := projT2 (cid (gK' n)). Qed. -Lemma measurable_almost_continuous (f : R -> R) (eps : rT) : +Lemma measurable_almost_continuous (f : rT -> rT) (eps : rT) : (0 < eps)%R -> measurable_fun A f -> exists K, [/\ compact K, K `<=` A, mu (A `\` K) < eps%:E & {within K, continuous f}]. @@ -2973,8 +2979,10 @@ Definition Rintegral (D : set T) (f : T -> R) := End Rintegral. -Notation "\int [ mu ]_ ( x 'in' D ) f" := (Rintegral mu D (fun x => f)) : ring_scope. -Notation "\int [ mu ]_ x f" := (Rintegral mu setT (fun x => f)) : ring_scope. +Notation "\int [ mu ]_ ( x 'in' D ) f" := + (Rintegral [the measure _ _ of mu] D (fun x => f)) : ring_scope. +Notation "\int [ mu ]_ x f" := + (Rintegral [the measure _ _ of mu] setT (fun x => f)) : ring_scope. HB.lock Definition integrable {d} {T : measurableType d} {R : realType} (mu : set T -> \bar R) D f := @@ -5000,7 +5008,7 @@ move=> cptA ctsfA; apply: measurable_bounded_integrable. by exists M; split; rewrite ?num_real // => ? ? ? ?; exact: mrt. Qed. -Lemma approximation_continuous_integrable (E : set R) (f : R -> R^o): +Lemma approximation_continuous_integrable (E : set _) (f : rT -> rT): measurable E -> mu E < +oo -> mu.-integrable E (EFin \o f) -> exists g_ : (rT -> rT)^nat, [/\ forall n, continuous (g_ n), @@ -6039,3 +6047,1150 @@ rewrite -ge0_integral_bigsetU//=. Qed. End hardy_littlewood. + +(* PR to MahtComp in progress *) +Lemma invf_plt (F : numFieldType) : + {in Num.pos &, forall x y : F, (x^-1 < y)%R = (y^-1 < x)%R}. +Proof. +by move=> x y ? ?; rewrite -[in LHS](@invrK _ y) ltf_pV2// posrE invr_gt0. +Qed. + +(* TODO: move near setUitv1 in set_interval.v *) +Lemma setDitv1r d (R : porderType d) x (r : R) : + ([set` Interval x (BRight r)] `\ r = [set` Interval x (BLeft r)])%classic. +Proof. +apply/seteqP; split => [z|z] /=; rewrite !in_itv/=. + by move=> [/andP[-> /= zr] /eqP rz]; rewrite lt_neqAle rz. +by rewrite lt_neqAle => /andP[-> /andP[/eqP ? ->]]. +Qed. + +Lemma setDitv1l d (R : porderType d) x (r : R) : + ([set` Interval (BLeft r) x] `\ r = [set` Interval (BRight r) x])%classic. +Proof. +apply/seteqP; split => [z|z] /=; rewrite !in_itv/=. + move=> [/andP[rz ->]]; rewrite andbT => /eqP. + by rewrite lt_neqAle eq_sym => ->. +move=> /andP[]; rewrite lt_neqAle => /andP[rz zr ->]. +by rewrite andbT; split => //; exact/nesym/eqP. +Qed. + +Lemma closed_ball_itv {R : realFieldType} (x s : R) (s0 : (0 < s)%R) : + closed_ball x s = `[x - s, x + s]%classic. +Proof. +rewrite (closed_ballE (x:R^o) s0)/= /closed_ball_/=. +by rewrite set_itvE; apply/seteqP; split => t/=; rewrite ler_distlC. +Qed. + +Lemma ball_itv {R : realFieldType} (x s : R) : + ball x s = `]x - s, x + s[%classic. +Proof. +rewrite -(@ball_normE _ R^o) /ball_ set_itvE. +by apply/seteqP; split => t/=; rewrite ltr_distlC. +Qed. + +Lemma closed_ball_ball {R : realFieldType} (x s : R) (s0 : (0 < s)%R) : + closed_ball x s = [set (x - s)%R] `|` ball x s `|` [set (x + s)%R]. +Proof. +rewrite closed_ball_itv// -(@setU1itv _ _ _ (x - s)%R); last first. + by rewrite bnd_simp lerBlDr -addrA lerDl ltW// addr_gt0. +rewrite -(@setUitv1 _ _ _ (x + s)%R); last first. + by rewrite bnd_simp ltrBlDr -addrA ltrDl addr_gt0. +by rewrite ball_itv setUA. +Qed. + +Lemma abs_ceil_ge (R : realType) (x : R) : (`|x| <= `|ceil x|.+1%:R)%R. +Proof. +rewrite -natr1 natr_absz; have [x0|x0] := ltP 0%R x. + by rewrite !gtr0_norm ?ceil_gt0// (le_trans (ceil_ge _))// lerDl. +by rewrite !ler0_norm ?ceil_le0// /ceil opprK; exact/ltW/lt_succ_floor. +Qed. + +Lemma nbhs_infty_ger {R : realType} (r : R) : + \forall n \near \oo, (r <= n%:R)%R. +Proof. +exists (`|ceil r|)%N => // n /=; rewrite -(ler_nat R); apply: le_trans. +by rewrite (le_trans (ceil_ge _))// natr_absz ler_int ler_norm. +Qed. + +Lemma nbhs0_ltW (R : realFieldType) (x : R) : (0 < x)%R -> + \forall r \near nbhs (0%R:R), (r <= x)%R. +Proof. +exists x => // y; rewrite /ball/= sub0r normrN => /ltW. +by apply: le_trans; rewrite ler_norm. +Qed. + +Lemma nbhs0_lt (R : realType) (x : R) : (0 < x)%R -> + \forall r \near nbhs (0%R:R), (r < x)%R. +Proof. +exists x => // z /=; rewrite sub0r normrN. +by apply: le_lt_trans; rewrite ler_norm. +Qed. + +Lemma cvg_indic {R : realFieldType} (x : R^o) k : + x \in (ball 0 k : set R^o) -> + \1_(ball 0 k : set R^o) y @[y --> x] --> (\1_(ball 0 k) x : R). +Proof. +move=> xB; apply/(@cvgrPdist_le _ R^o) => /= e e0; near=> t. +rewrite !indicE xB/= mem_set//=; first by rewrite subrr normr0// ltW. +near: t. +rewrite inE /ball /= sub0r normrN in xB. +exists ((k - `|x|)/2) => /=; first by rewrite divr_gt0// subr_gt0. +rewrite /ball_/= => z /= h; rewrite /ball/= sub0r normrN. +rewrite -(subrK x z) (le_lt_trans (ler_normD _ _))//. +rewrite -ltrBrDr distrC (lt_le_trans h)//. +by rewrite ler_pdivrMr//= ler_pMr// ?subr_gt0// ler1n. +Unshelve. all: by end_near. Qed. + +Section davg. +Context {R : realType}. +Local Notation mu := (@lebesgue_measure R). +Local Open Scope ereal_scope. +Implicit Types f g : R -> R. + +Definition davg f x (r : R) := iavg (center (f x) \o f) (ball x r). + +Lemma davg0 f x (r : R) : (r <= 0)%R -> davg f x r = 0. +Proof. by move=> r0; rewrite /davg/= (ball0 _ _).2//= iavg0. Qed. + +Lemma davgD f g (x r : R) : + measurable_fun (ball x r) f -> measurable_fun (ball x r) g -> + davg (f \+ g)%R x r <= (davg f x \+ davg g x) r. +Proof. +move=> mf mg; rewrite (le_trans _ (iavgD _ _ _ _)) //. +- rewrite le_eqVlt; apply/orP; left; apply/eqP => /=; congr iavg. + by apply/funext => e /=; rewrite opprD addrACA. +- exact: measurable_ball. +- have [r0|r0] := leP r 0%R; first by rewrite (ball0 _ _).2// measure0. + by rewrite (lebesgue_measure_ball _ (ltW r0)) ltry. +- exact: measurable_funB. +- exact: measurable_funB. +Qed. + +Let continuous_integralB_fin_num f x : + measurable_fun setT f -> {for x, continuous f} -> + \forall t \near 0%R, + \int[mu]_(y in ball x t) `|(f y)%:E - (f x)%:E| \is a fin_num. +Proof. +move=> mf /cvgrPdist_le fx. +near (0%R:R)^'+ => e. +have e0 : (0 < e)%R by near: e; exact: nbhs_right_gt. +have [r /= r0] := fx _ e0. +move=> {}fx; near=> t. +rewrite ge0_fin_numE ?integral_ge0//. +rewrite (@le_lt_trans _ _ (\int[mu]_(y in ball x r) `|f y - f x|%:E))//. + apply: subset_integral => //=. + - exact: measurable_ball. + - exact: measurable_ball. + - do 2 apply: measurableT_comp => //=; apply: measurable_funB => //. + exact: measurable_funS mf. + - by apply: le_ball; near: t; exact: nbhs0_ltW. +rewrite (@le_lt_trans _ _ (\int[mu]_(y in ball x r) e%:E))//=. + apply: ge0_le_integral => //=. + - exact: measurable_ball. + - do 2 apply: measurableT_comp => //=; apply: measurable_funB => //. + exact: measurable_funS mf. + - by rewrite lee_fin ltW. + - by move=> y xry; rewrite lee_fin distrC; exact: fx. +rewrite integral_cst// ?mul1e. + rewrite [X in _ * X](_ : _ = mu (ball x r))//. + by rewrite lebesgue_measure_ball// ?ltry// ltW. +exact: measurable_ball. +Unshelve. all: by end_near. Qed. + +Let continuous_davg_fin_num f x : + measurable_fun setT f -> {for x, continuous f} -> + \forall A \near 0%R, davg f x A \is a fin_num. +Proof. +move=> mf fx. +have [e /= e0 exf] := continuous_integralB_fin_num mf fx. +move/cvgrPdist_le in fx. +near (0%R:R)^'+ => r. +have r0 : (0 < r)%R by near: r; exact: nbhs_right_gt. +have [d /= d0] := fx _ e0. +move=> {}fx; near=> t. +have [t0|t0] := leP t 0%R; first by rewrite davg0. +by rewrite fin_numM// exf//=. +Unshelve. all: by end_near. Qed. + +(* TODO: should this be proved without the two Let's above? *) +Lemma continuous_cvg_davg (E : set R) (f : R -> R) : + measurable_fun setT f -> {in E, continuous f} -> + {in E, forall x, davg f x r @[r --> 0%R] --> 0}. +Proof. +move=> mf cf x Ex; apply/fine_cvgP => //; split. + by apply: (@continuous_davg_fin_num) => //; exact: cf. +apply/cvgrPdist_le => e e0. +have /cvgrPdist_le /= fx := cf _ Ex. +have [r /= r0] := fx _ e0 => xrf. +have [d /= d0 dfx] := continuous_davg_fin_num mf (cf _ Ex). +near=> t. +have [t0|t0] := leP t 0%R; first by rewrite /= davg0//= subrr normr0 ltW. +rewrite sub0r normrN /= ger0_norm; last first. + rewrite fine_ge0// mule_ge0//; last exact: integral_ge0. + by rewrite lee_fin invr_ge0// fine_ge0. +rewrite -lee_fin fineK//; last by rewrite dfx//= sub0r normrN gtr0_norm. +rewrite /davg/= /iavg/= lee_pdivr_mull//; last first. + by rewrite fine_gt0// lebesgue_measure_ball// ?ltry ?lte_fin ?mulrn_wgt0 ?ltW. +rewrite (@le_trans _ _ (\int[mu]_(y in ball x t) e%:E))//. + apply: ge0_le_integral => //=. + - exact: measurable_ball. + - do 2 apply: measurableT_comp => //=; apply: measurable_funB => //. + exact: measurable_funS mf. + - by move=> y xty; rewrite lee_fin ltW. + - move=> y xty; rewrite lee_fin distrC xrf//. + by apply: (lt_le_trans xty); near: t; exact: nbhs0_ltW. +rewrite integral_cst//; last exact: measurable_ball. +rewrite [X in e%:E * X](_ : _ = mu (ball x t))// muleC. +by rewrite lebesgue_measure_ball// ?ltry// ltW. +Unshelve. all: by end_near. Qed. + +End davg. + +Section lim_sup_davg. +Context {R : realType}. +Local Open Scope ereal_scope. +Implicit Types f g : R -> R. + +Definition lim_sup_davg f x := lime_sup (davg f x) 0. + +Local Notation "f ^*" := (lim_sup_davg f). + +Lemma lim_sup_davg_ge0 f x : 0 <= f^* x. +Proof. by apply: lime_sup_ge0 => y; rewrite /davg iavg_ge0. Qed. + +Lemma lim_sup_davg_le f g x : + measurable_fun setT f -> locally_integrable setT g -> + (f \+ g)%R^* x <= (f^* \+ g^*) x. +Proof. +move=> mf /= [mg _ goo]; apply: le_trans (lime_supD _); last first. + by rewrite ge0_adde_def// inE; exact: lim_sup_davg_ge0. +apply: lime_sup_le => r r0 y y0 ry. +exact: (davgD (measurable_funS _ _ mf) (measurable_funS _ _ mg)). +Qed. + +Lemma continuous_lim_sup_davg (E : set R) f : + measurable_fun setT f -> {in E, continuous f} -> {in E, f^* =1 cst 0}. +Proof. +move=> mg gx x xE. +by have /lim_lime_sup := continuous_cvg_davg mg gx xE. +Qed. + +Lemma lim_sup_davgB (E : set R) f g : + measurable_fun setT f -> {in E, continuous g} -> + locally_integrable [set: R] g -> + {in E, (f \- g)%R^* =1 f^*}. +Proof. +move=> mf cg locg x Ex. +apply/eqP; rewrite eq_le; apply/andP; split. +- rewrite [leRHS](_ : _ = f^* x + (\- g)%R^* x). + by apply: lim_sup_davg_le => //; exact: locally_integrableN. + rewrite (@continuous_lim_sup_davg [set x] (- g)%R) ?adde0//. + + by apply: measurableT_comp => //; case: locg. + + by move=> y; rewrite inE/= => -> /=; exact/continuousN/cg. + + by rewrite inE. +- rewrite [leRHS](_ : _ = ((f \- g)%R^* \+ g^*) x)//. + rewrite {1}(_ : f = f \- g + g)%R; last first. + by apply/funext => y /=; rewrite subrK. + by apply: lim_sup_davg_le => //; apply: measurable_funB => //; case: locg. + rewrite [X in _ + X](@continuous_lim_sup_davg [set x]) ?adde0//. + + by case: locg. + + by move=> y; rewrite inE/= => ->; exact: cg. + + by rewrite inE. +Qed. + +Local Notation mu := (@lebesgue_measure R). + +Lemma lim_sup_davgT_HL_maximal f (x : R) : locally_integrable setT f -> + f^* x <= HL_maximal f x + `|f x|%:E. +Proof. +move=> [mf _ locf]; rewrite /lim_sup_davg lime_sup_lim; apply: lime_le. + (* TODO: should this be a lemma? *) + apply: nondecreasing_at_right_is_cvge; near=> e => y z. + rewrite !in_itv/= => /andP[y0 ye] /andP[z0 ze] yz. + apply: le_ereal_sup => _ /= -[b [yb b0]] <-. + by exists b => //; split => //; exact: le_ball yb. +near=> e. +apply: ub_ereal_sup => _ [b [eb] /= b0] <-. +suff : forall r, davg f x r <= HL_maximal f x + `|f x|%:E by exact. +move=> r. +apply: (@le_trans _ _ ((fine (mu (ball x r)))^-1%:E * + \int[mu]_(y in ball x r) (`| (f y)%:E | + `|(f x)%:E|))). + - rewrite /davg lee_wpmul2l//. + by rewrite lee_fin invr_ge0 fine_ge0. + apply: ge0_le_integral => //. + + exact: measurable_ball. + + do 2 apply: measurableT_comp => //=; apply: measurable_funB => //. + exact: measurableT_comp. + + by move=> *; rewrite adde_ge0. + + apply: emeasurable_funD => //; do 2 apply: measurableT_comp => //. + exact: measurable_funS mf. + by move=> /= y xry; rewrite -EFinD lee_fin// ler_normB. +rewrite [leLHS](_ : _ = (fine (mu (ball x r)))^-1%:E * + (\int[mu]_(y in ball x r) `|(f y)%:E| + + \int[mu]_(y in ball x r) `|(f x)%:E|)); last first. + congr *%E; rewrite ge0_integralD//=; first exact: measurable_ball. + by do 2 apply: measurableT_comp => //; exact: measurable_funS mf. +have [r0|r0] := lerP r 0. + rewrite (ball0 _ _).2// !integral_set0 adde0 mule0 adde_ge0//. + by apply: HL_maximalT_ge0; split => //; exact: openT. +rewrite muleDr//; last by rewrite ge0_adde_def// inE integral_ge0. +rewrite leeD//. + by apply: ereal_sup_ub => /=; exists r => //; rewrite in_itv/= r0. +under eq_integral do rewrite -(mule1 `| _ |). +rewrite ge0_integralZl//; last exact: measurable_ball. +rewrite integral_cst//; last exact: measurable_ball. +rewrite mul1e muleCA !(lebesgue_measure_ball _ (ltW r0)). +rewrite [X in _ * (_ * X)](_ : _ = mu (ball x r))//. +rewrite (lebesgue_measure_ball _ (ltW r0))//. +by rewrite /= -EFinM mulVr ?mulr1// unitfE mulrn_eq0/= gt_eqF. +Unshelve. all: by end_near. Qed. + +End lim_sup_davg. + +Definition lebesgue_pt {R : realType} (f : R -> R) (x : R) := + davg f x r @[r --> (0%R:R)^'+] --> 0%E. + +Local Open Scope ereal_scope. +(* does not require a nonneg function + whereas integral_setU goes (and should maybe be renamed ge0_integral_setU) *) +Lemma integral_setU_EFin d (T : measurableType d) (R : realType) + (mu : {measure set T -> \bar R}) (A B : set T) (f : T -> R) : + measurable A -> measurable B -> + measurable_fun (A `|` B) f -> + [disjoint A & B] -> + \int[mu]_(x in (A `|` B)) (f x)%:E = \int[mu]_(x in A) (f x)%:E + + \int[mu]_(x in B) (f x)%:E. +Proof. +move=> mA mB ABf AB. +rewrite integralE/=. +rewrite integral_setU//; last exact/measurable_funepos/EFin_measurable_fun. +rewrite integral_setU//; last exact/measurable_funeneg/EFin_measurable_fun. +rewrite [X in _ = X + _]integralE/=. +rewrite [X in _ = _ + X]integralE/=. +set ap : \bar R := \int[mu]_(x in A) _; set an : \bar R := \int[mu]_(x in A) _. +set bp : \bar R := \int[mu]_(x in B) _; set bn : \bar R := \int[mu]_(x in B) _. +rewrite oppeD 1?addeACA//. +by rewrite ge0_adde_def// inE integral_ge0. +Qed. +Local Close Scope ereal_scope. + +Section lebesgue_integral_extra. +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. +Proof. +rewrite (eq_integral (cst (f r)))/=; last by move=> x; rewrite inE/= => ->. +by rewrite integral_cst//= lebesgue_measure_set1 mule0. +Qed. + +Lemma ge0_integral_ball_closed (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) -> + \int[mu]_(x in ball 0%R r) f x = + \int[mu]_(x in closed_ball 0%R r) f x. +Proof. +move=> mf f0. +rewrite closed_ball_ball//= sub0r add0r integral_setU//=; last 4 first. + by apply: measurableU => //; exact: measurable_ball. + by move: mf; rewrite closed_ball_ball// sub0r add0r. + by move=> x H; rewrite f0// closed_ball_ball// inE/= sub0r add0r. + apply/disj_setPLR => x [->/=|]; first by apply/eqP; rewrite lt_eqF// gtrN. + by rewrite /ball/= sub0r normrN => /ltr_normlW ?; apply/eqP; rewrite lt_eqF. +rewrite integral_set1 adde0 integral_setU//=. +- by rewrite integral_set1//= ?add0e. +- exact: measurable_ball. +- apply: measurable_funS mf; first exact: measurable_closed_ball. + by move=> x; rewrite closed_ball_ball// sub0r add0r; left. +- by move=> x H; rewrite f0// closed_ball_ball// inE/= sub0r add0r; left. +- apply/disj_setPRL => x/=; rewrite /ball/= sub0r => /ltr_normlW ?. + by apply/eqP; rewrite gt_eqF// ltrNl. +Qed. + +Lemma integral_setD1_EFin (f : R -> R) r (D : set R) : + measurable D -> measurable_fun D f -> D r -> + \int[mu]_(x in D) (f x)%:E = \int[mu]_(x in D `\ r) (f x)%:E. +Proof. +move=> mD mf Dr; rewrite -[in LHS](@setD1K _ r D)// integral_setU_EFin//. +- by rewrite integral_set1// ?add0e. +- exact: measurableD. +- by rewrite setD1K. +- by rewrite disj_set2E; apply/eqP/seteqP; split => // x [? []]. +Qed. + +Lemma integral_itv_bndo_bndc (a : itv_bound R) (r : R) (f : R -> R) : + measurable_fun [set` Interval a (BRight r)] f -> + \int[mu]_(x in [set` Interval a (BLeft r)]) (f x)%:E = + \int[mu]_(x in [set` Interval a (BRight r)]) (f x)%:E. +Proof. +move=> mf; have [ar|ar] := leP a (BLeft r). +- rewrite [RHS](@integral_setD1_EFin _ r) ?setDitv1r//. + by rewrite /= in_itv /= lexx andbT {mf}; case: a ar => -[]. +- by rewrite !set_itv_ge// -leNgt// ltW. +Qed. + +Lemma integral_itv_obnd_cbnd (r : R) (b : itv_bound R) (f : R -> R) : + measurable_fun [set` Interval (BLeft r) b] f -> + \int[mu]_(x in [set` Interval (BRight r) b]) (f x)%:E = + \int[mu]_(x in [set` Interval (BLeft r) b]) (f x)%:E. +Proof. +move=> mf; have [rb|rb] := leP (BRight r) b. +- rewrite [RHS](@integral_setD1_EFin _ r) ?setDitv1l//. + by rewrite /= in_itv /= lexx/= {mf}; case: b rb => -[]. +- by rewrite !set_itv_ge// -leNgt -?ltBRight_leBLeft// ltW. +Qed. + +End lebesgue_integral_extra. + +Section lebesgue_differentiation. +Context {R : realType}. +Local Notation mu := (@lebesgue_measure R). +Local Open Scope ereal_scope. +Implicit Types f : R -> R. + +Local Notation "f ^*" := (lim_sup_davg f). + +Let lebesgue_differentiation_suff (E : set R) f : + (forall a, (0 < a)%R -> mu.-negligible (E `&` [set x | a%:E < f^* x])) -> + {ae mu, forall x : R, E x -> lebesgue_pt f x}. +Proof. +move=> Ef; have {Ef} : mu.-negligible (E `&` [set x | 0 < f^* x]). + suff -> : E `&` [set x | 0 < f^* x] = + E `&` \bigcup_n [set x | n.+1%:R^-1%:E < f^* x]. + rewrite setI_bigcupr; apply: negligible_bigcup => k/=. + by apply: Ef; rewrite invr_gt0. + apply/seteqP; split; last first. + by move=> r [Er] [k ?] /=; split => //; exact: le_lt_trans q. + move=> x /= [Ex] fx0; split => //. + have [fxoo|fxoo] := eqVneq (f^* x) +oo. + by exists 1%N => //=; rewrite fxoo ltry. + near \oo => m; exists m => //=. + rewrite -(@fineK _ (f^* x)) ?gt0_fin_numE ?ltey// lte_fin. + rewrite invf_plt ?posrE//; last by rewrite fine_gt0// ltey fx0. + set r := _^-1; rewrite (@le_lt_trans _ _ `|ceil r|.+1%:R)//. + by rewrite (le_trans _ (abs_ceil_ge _))// ler_norm. + by rewrite ltr_nat ltnS; near: m; exact: nbhs_infty_gt. +apply: negligibleS => z /= /not_implyP[Ez H]; split => //. +rewrite ltNge; apply: contra_notN H. +rewrite le_eqVlt ltNge lime_sup_ge0 /= ?orbF; last by move=> x; exact: iavg_ge0. +move=> /eqP fz0. +suff: lime_inf (davg f z) 0 = 0 by exact: lime_sup_inf_at_right. +apply/eqP; rewrite eq_le -[X in _ <= X <= _]fz0 lime_inf_sup/= fz0. +by apply: lime_inf_ge0 => x; exact: iavg_ge0. +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 + (forall k, mu.-integrable setT (EFin \o f_ k)) -> + forall k, {ae mu, forall x, B k x -> lebesgue_pt (f_ k) x}. +Proof. +move=> B f_ intf_ k; apply: lebesgue_differentiation_suff => e e0. +have mE : measurable (B k) by exact: measurable_ball. +have ex_g_ : exists g_ : (R -> R)^nat, + [/\ (forall n, continuous (g_ n)), + (forall n, mu.-integrable (B k) (EFin \o g_ n)) & + \int[mu]_(z in B k) `|f_ k z - g_ n z|%:E @[n --> \oo] --> 0 ]. + apply: approximation_continuous_integrable => //=. + by rewrite lebesgue_measure_ball//= ltry. + exact: integrableS (intf_ _). +have {ex_g_} ex_gn n : exists gn : R -> R, + [/\ continuous gn, + mu.-integrable (B k) (EFin \o gn) & + \int[mu]_(z in B k) `|f_ k z - gn z|%:E <= n.+1%:R^-1%:E]. + case: ex_g_ => g_ [cg intg] /fine_cvgP[] [m _ fgfin] /cvgrPdist_le. + move=> /(_ n.+1%:R^-1 ltac:(by []))[p _] /(_ _ (leq_addr m p)). + rewrite sub0r normrN -lee_fin => /= fg0. + exists (g_ (p + m)%N); split => //. + rewrite (le_trans _ fg0)// ger0_norm ?fine_ge0 ?integral_ge0// fineK//. + by rewrite fgfin//= leq_addl. +pose g_ n : R -> R := sval (cid (ex_gn n)). +have cg_ n : continuous (g_ n) by rewrite /g_ /sval /=; case: cid => // x []. +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. +have cg_B n : {in B k, continuous (g_B n)}. + by move=> x xBk; 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]. +pose Ee := \bigcap_n (B k `&` (HLf_g_Be n `|` f_g_Be n)). +case/integrableP: (intf_ k) => mf intf. +have mfg n : measurable_fun setT (f_ k \- g_ n)%R. + apply: measurable_funB; first by move/EFin_measurable_fun : mf. + 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. + - 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_funTS. + exact: continuous_measurable_fun. + + move=> /= x Kx; rewrite /g_B /= indicE. + by case: (_ \in _); rewrite ?mulr1 ?mulr0 ?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. + + exact: openT. + + move=> K _ cK; rewrite (le_lt_trans _ intf)//=. + apply: subset_integral => //. + * exact: compact_measurable. + * by do 2 apply: measurableT_comp => //; move/EFin_measurable_fun : mf. +have mEHL i : measurable (HLf_g_Be i). + rewrite /HLf_g_Be -[X in measurable X]setTI. + apply: emeasurable_fun_o_infty => //. + by apply: measurable_HL_maximal; exact: locf_g_B. +have mfge i : measurable (f_g_Be i). + rewrite /f_g_Be -[X in measurable X]setTI. + apply: emeasurable_fun_c_infty => //. + by do 2 apply: measurableT_comp => //; case: (locf_g_B i). +have mEe : measurable Ee. + apply: bigcapT_measurable => i. + by apply: measurableI; [exact: measurable_ball|exact: measurableU]. +have davgfEe : B k `&` [set x | (f_ k)^* x > e%:E] `<=` Ee. + suff: forall n, B k `&` [set x | e%:E < (f_ k)^* x] `<=` + B k `&` (HLf_g_Be n `|` f_g_Be n). + by move=> suf r /= /suf hr n _; exact: hr. + move=> n; rewrite [X in X `<=`_](_ : _ = + B k `&` [set x | e%:E < (f_ k \- g_B n)%R^* x]); last first. + apply/seteqP; split => [x [Ex] /=|x [Ex] /=]. + rewrite (@lim_sup_davgB _ (B k)) ?inE//. + by move/EFin_measurable_fun : mf; exact: measurable_funS. + by rewrite (@lim_sup_davgB _ (B k)) ?inE//; move/EFin_measurable_fun : mf. + move=> r /= [Er] efgnr; split => //. + have {}efgnr := lt_le_trans efgnr (lim_sup_davgT_HL_maximal r (locf_g_B n)). + have [|h] := ltP (e / 2)%:E (HL_maximal (f_ k \- g_B n)%R r); first by left. + right; move: efgnr. + rewrite {1}(splitr e) EFinD -lte_subr_addl// => /ltW/le_trans; apply. + by rewrite lee_subl_addl// leeD. +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. + 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). +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_pdivl_mull ?invr_gt0 ?divr_gt0// -[X in mu X]setTI. + apply: le_trans. + apply: (@le_integral_comp_abse _ _ _ mu _ measurableT + (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. + 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). +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. +near \oo => n. +rewrite (@le_trans _ _ (mu (B k `&` (HLf_g_Be n `|` f_g_Be n))))//. + rewrite le_measure// inE//; apply: measurableI; first exact: measurable_ball. + by apply: measurableU => //; [exact: mEHL|exact: mfge]. +rewrite (@le_trans _ _ ((4 / (e / 2))%:E * n.+1%:R^-1%:E))//. + rewrite (@le_trans _ _ (mu (HLf_g_Be n `|` f_g_Be n)))//. + rewrite le_measure// inE//. + apply: measurableI => //. + by apply: measurableU => //; [exact: mEHL|exact: mfge]. + by apply: measurableU => //; [exact: mEHL|exact: mfge]. + rewrite (le_trans (measureU2 _ _ _))//=; [exact: mEHL|exact: mfge|]. + apply: le_trans; first by apply: leeD; [exact: HL_null|exact: fgn_null]. + rewrite -muleDl// lee_pmul2r// -EFinD lee_fin -{2}(mul1r (_^-1)) -div1r. + by rewrite -mulrDl natr1. +rewrite -lee_pdivl_mull ?divr_gt0// -EFinM lee_fin -(@invrK _ r). +rewrite -invrM ?unitfE ?gt_eqF ?invr_gt0 ?divr_gt0//. +rewrite lef_pV2 ?posrE ?mulr_gt0 ?invr_gt0 ?divr_gt0//. +by rewrite -(@natr1 _ n) -lerBlDr; near: n; exact: nbhs_infty_ger. +Unshelve. all: by end_near. Qed. + +Lemma lebesgue_differentiation f : locally_integrable setT f -> + {ae mu, forall x, lebesgue_pt f x}. +Proof. +move=> locf. +pose B k : set R^o := ball 0%R (k.+1.*2)%:R. +pose fk k := (f \* \1_(B k))%R. +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_ball_closed//. + 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}. + exact: lebesgue_differentiation_bounded. +pose E k : set _ := sval (cid (suf k)). +rewrite /= in E. +have HE k : mu (E k) = 0 /\ ~` [set x | B k x -> lebesgue_pt (fk k) x] `<=` E k. + by rewrite /E /sval; case: cid => // A []. +suff: ~` [set x | lebesgue_pt f x] `<=` + \bigcup_k (~` [set x | B k x -> lebesgue_pt (fk k) x]). + move/(@negligibleS _ _ _ mu); apply => /=. + by apply: negligible_bigcup => k /=; exact: suf. +move=> x /= fx; rewrite -setC_bigcap => h; apply: fx. +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. + 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. + rewrite opprK -lerBrDl -natrB//; last by rewrite -addnn addSnnS ltn_addl. + by rewrite (le_trans (ltW r1))// -addnn addnK// ler1n. + rewrite -opprB ltrNl in xrt. + rewrite ltr0_norm// (lt_le_trans xrt)// lerBlDl (le_trans (ltW r1))//. + rewrite -lerBlDl addrC -lerBrDr (le_trans (ler_norm _))//. + rewrite -normrN in yk1. + rewrite (le_trans (ltW yk1))// -lerBlDr opprK -lerBrDl. + rewrite -natrB//; last by rewrite -addnn addSnnS ltn_addl. + by rewrite -addnn addnK ler1n. +have := h `|ceil x|.+1%N Logic.I. +have Bxx : B `|ceil x|.+1 x. + rewrite /B /ball/= sub0r normrN (le_lt_trans (abs_ceil_ge _))// ltr_nat. + by rewrite -addnn addSnnS ltn_addl. +move=> /(_ Bxx)/fine_cvgP[davg_fk_fin_num davg_fk0]. +have f_fk_ceil : \forall t \near 0^'+, + \int[mu]_(y in ball x t) `|(f y)%:E - (f x)%:E| = + \int[mu]_(y in ball x t) `|fk `|ceil x|.+1 y - fk `|ceil x|.+1 x|%:E. + near=> t. + apply: eq_integral => /= y /[1!inE] xty. + rewrite -(fE x _ t)//; last first. + rewrite /ball/= sub0r normrN (le_lt_trans (abs_ceil_ge _))//. + by rewrite -[in ltRHS]natr1 ltrDl. + rewrite -(fE x _ t)//; last first. + by apply: ballxx; near: t; exact: nbhs_right_gt. + rewrite /ball/= sub0r normrN (le_lt_trans (abs_ceil_ge _))//. + by rewrite -[in ltRHS]natr1 ltrDl. +apply/fine_cvgP; split=> [{davg_fk0}|{davg_fk_fin_num}]. +- move: davg_fk_fin_num => -[M /= M0] davg_fk_fin_num. + apply: filter_app f_fk_ceil; near=> t; move=> Ht. + by rewrite /davg /iavg Ht davg_fk_fin_num//= sub0r normrN gtr0_norm. +- move/cvgrPdist_le in davg_fk0; apply/cvgrPdist_le => e e0. + have [M /= M0 {}davg_fk0] := davg_fk0 _ e0. + apply: filter_app f_fk_ceil; near=> t; move=> Ht. + by rewrite /davg /iavg Ht// davg_fk0//= sub0r normrN gtr0_norm. +Unshelve. all: by end_near. Qed. + +End lebesgue_differentiation. + +Section nicely_shrinking. +Context {R : realType}. +Implicit Types (x : R) (E : (set R)^nat). +Local Notation mu := lebesgue_measure. + +Definition nicely_shrinking x E := + (forall n, measurable (E n)) /\ + exists Cr : R * {posnum R}^nat, [/\ Cr.1 > 0, + (Cr.2 n)%:num @[n --> \oo] --> 0, + (forall n, E n `<=` ball x (Cr.2 n)%:num) & + (forall n, mu (ball x (Cr.2 n)%:num) <= Cr.1%:E * mu (E n))%E]. + +Lemma nicely_shrinking_gt0 x E : nicely_shrinking x E -> + forall n, (0 < mu (E n))%E. +Proof. +move=> [mE [[C r_]]] [/= C_gt0 _ _ + ] n => /(_ n). +rewrite lebesgue_measure_ball// -lee_pdivr_mull//. +apply: lt_le_trans. +by rewrite mule_gt0// lte_fin invr_gt0. +Qed. + +Lemma nicely_shrinking_lty x E : nicely_shrinking x E -> + forall n, (mu (E n) < +oo)%E. +Proof. +move=> [mE [[C r_]]] [/= C_gt0 _ + _] n => /(_ n) Er_. +rewrite (@le_lt_trans _ _ (lebesgue_measure (ball x (r_ n)%:num)))//. + by rewrite le_measure// inE; [exact: mE|exact: measurable_ball]. +by rewrite lebesgue_measure_ball// ltry. +Qed. + +End nicely_shrinking. + +Section nice_lebesgue_differentiation. +Local Open Scope ereal_scope. +Context {R : realType}. +Variable E : R -> (set R)^nat. +Hypothesis hE : forall x, nicely_shrinking x (E x). +Local Notation mu := lebesgue_measure. + +Lemma nice_lebesgue_differentiation (f : R -> R) : + locally_integrable setT f -> + forall x, lebesgue_pt f x -> + (fine (mu (E x n)))^-1%:E * \int[mu]_(y in E x n) (f y)%:E + @[n --> \oo] --> (f x)%:E. +Proof. +move=> locf x fx; apply/(cvge_sub0 _ _).1 => //=; apply/cvg_abse0P. +pose r_ x : {posnum R}^nat := (sval (cid (hE x).2)).2. +pose C := (sval (cid (hE x).2)).1. +have C_gt0 : (0 < C)%R by rewrite /C /sval/=; case: cid => -[? ?] []. +have r_0 y : (r_ y n)%:num @[n --> \oo] --> (0%R : R). + by rewrite /r_ /sval/=; case: cid => -[? ?] []. +have E_r_ n : E x n `<=` ball x (r_ x n)%:num. + by rewrite /r_ /sval/=; case: cid => -[? ?] []. +have muEr_ n : mu (ball x (r_ x n)%:num) <= C%:E * mu (E x n). + by rewrite /C /r_ /sval/=; case: cid => -[? ?] []. +apply: (@squeeze_cvge _ _ _ _ (cst 0) _ + (fun n => C%:E * davg f x (r_ x n)%:num)); last 2 first. + exact: cvg_cst. + move/cvge_at_rightP: fx => /(_ (fun r => (r_ x r)%:num)) fx. + by rewrite -(mule0 C%:E); apply: cvgeM => //;[exact: mule_def_fin | + exact: cvg_cst | apply: fx; split => //; exact: r_0]. +near=> n. +apply/andP; split => //=. +apply: (@le_trans _ _ ((fine (mu (E x n)))^-1%:E * + `| \int[mu]_(y in E x n) ((f y)%:E + (- f x)%:E) |)). + have fxE : (- f x)%:E = + (fine (mu (E x n)))^-1%:E * \int[mu]_(y in E x n) (- f x)%:E. + rewrite integral_cst//=; last exact: (hE _).1. + rewrite muleCA -[X in _ * (_ * X)](@fineK _ (mu (E x n))); last first. + by rewrite ge0_fin_numE// (nicely_shrinking_lty (hE x)). + rewrite -EFinM mulVf ?mulr1// neq_lt fine_gt0 ?orbT//. + by rewrite (nicely_shrinking_gt0 (hE x))//= (nicely_shrinking_lty (hE x)). + rewrite [in leLHS]fxE -muleDr//; last first. + rewrite integral_cst//=; last exact: (hE _).1. + rewrite fin_num_adde_defl// fin_numM// gt0_fin_numE. + by rewrite (nicely_shrinking_lty (hE x)). + by rewrite (nicely_shrinking_gt0 (hE x)). + rewrite abseM gee0_abs; last by rewrite lee_fin// invr_ge0// fine_ge0. + rewrite lee_pmul//; first by rewrite lee_fin// invr_ge0// fine_ge0. + rewrite integralD//=. + - exact: (hE x).1. + - apply/integrableP; split. + apply/EFin_measurable_fun. + by case: locf => + _ _; exact: measurable_funS. + rewrite (@le_lt_trans _ _ + (\int[mu]_(y in closed_ball x (r_ x n)%:num) `|(f y)%:E|))//. + apply: subset_integral => //. + + exact: (hE _).1. + + exact: measurable_closed_ball. + + apply: measurableT_comp => //; apply/EFin_measurable_fun => //. + by case: locf => + _ _; exact: measurable_funS. + + by apply: (subset_trans (E_r_ n)) => //; exact: subset_closed_ball. + by case: locf => _ _; apply => //; exact: closed_ballR_compact. + apply/integrableP; split; first exact: measurable_cst. + rewrite integral_cst //=; last exact: (hE _).1. + by rewrite lte_mul_pinfty// (nicely_shrinking_lty (hE x)). +rewrite muleA lee_pmul//. +- by rewrite lee_fin invr_ge0// fine_ge0. +- rewrite -(@invrK _ C) -EFinM -invfM lee_fin lef_pV2//; last 2 first. + rewrite posrE fine_gt0// (nicely_shrinking_gt0 (hE x))//=. + by rewrite (nicely_shrinking_lty (hE x)). + rewrite posrE mulr_gt0// ?invr_gt0// fine_gt0//. + by rewrite lebesgue_measure_ball// ltry andbT lte_fin mulrn_wgt0. + rewrite lter_pdivrMl // -lee_fin EFinM fineK; last first. + by rewrite lebesgue_measure_ball// ltry andbT lte_fin mulrn_wgt0. + rewrite fineK; last by rewrite ge0_fin_numE// (nicely_shrinking_lty (hE x)). + exact: muEr_. ++ apply: le_trans. + * apply: le_abse_integral => //; first exact: (hE x).1. + apply/EFin_measurable_fun; apply/measurable_funB => //. + by case: locf => + _ _; exact: measurable_funS. + * apply: subset_integral => //; first exact: (hE x).1. + exact: measurable_ball. + * apply/EFin_measurable_fun; apply: measurableT_comp => //. + apply/measurable_funB => //. + by case: locf => + _ _; exact: measurable_funS. +Unshelve. all: by end_near. Qed. + +End nice_lebesgue_differentiation. + +Lemma set_itvxx {R : realDomainType} (x : itv_bound R) : [set` Interval x x] = set0. +Proof. by move: x => [[|] x |[|]]; rewrite !set_itvE. Qed. + +Lemma itv_bndo_setU {R : realDomainType} (a x y : itv_bound R) : + (a <= x)%O -> (x <= y)%O -> + ([set` Interval a y] = [set` Interval a x] `|` [set` Interval x y])%classic. +Proof. +rewrite le_eqVlt => /predU1P[<-{x} ay|]; first by rewrite set_itvxx set0U. +move=> /[swap]. +rewrite le_eqVlt => /predU1P[-> ay|]; first by rewrite set_itvxx setU0. +move: y => [yb y/=|[|]]; last 2 first. + by case: x => [|[|]]. + move=> _ ax; apply/seteqP; split => [z|z] /=. + rewrite !in_itv/= !andbT => -> /=; apply/orP. + by move: x => [[|] x/=|[|]//] in ax *; rewrite leNgt ?(orbN,orNb). + rewrite !in_itv/= !andbT => -[/andP[]|]//. + move: x => [[|] x/=|[|]//] in ax *; move: a => [[|] a/=|[|]//] in ax * => //. + - by apply/le_trans; exact/ltW. + - exact/lt_le_trans. + - by move=> /(le_lt_trans ax) /ltW. + - exact/lt_trans. +move=> xy ax; apply/seteqP; split => [z|z] /=. + rewrite !in_itv /= => /andP[]. + move: a ax => [b t /=|[]//= oox _]. + move=> tx -> zxy /=; rewrite zxy andbT/=; apply/orP. + by case: x xy tx => [[|] x/=|[|]//] xy tx; rewrite leNgt ?(orbN,orNb). + move=> ->; rewrite andbT; apply/orP. + by move: x => [[|] x/=|[|]//] in oox xy *; rewrite leNgt ?(orbN,orNb). +rewrite !in_itv/=. +move: a ax => [b t /= tx| [/= oox|/= oox]]. +- move=> [/andP[-> zx]|]. + move: x => [[|] x|[|]//]/= in xy tx zx *. + case: yb => /= in xy *. + by rewrite (lt_trans zx _). + by rewrite (ltW (lt_le_trans zx _)). + rewrite bnd_simp in xy. + case: yb => /=. + by rewrite (le_lt_trans zx _). + by rewrite (ltW (le_lt_trans zx _)). + move: x => [[|] x|[|]//]/= in xy tx *; rewrite bnd_simp in xy tx. + + move=> /andP[xz ->]; rewrite andbT. + case: b => /=. + by rewrite (le_trans _ xz)// ltW. + by rewrite (lt_le_trans tx). + move=> /andP[xz ->]; rewrite andbT. + case: b tx => /= tx; rewrite bnd_simp in tx. + by rewrite ltW// (le_lt_trans _ xz). + by rewrite (lt_trans tx). +- move: x => [[|] x|[|]//]/= in xy oox *; move=> [|]. + + case: yb => /= in xy *. + by move=> /lt_trans; exact. + rewrite bnd_simp in xy. + by move=> /lt_le_trans => /(_ _ xy)/ltW. + + by move=> /andP[]. + + case: yb => /= in xy *. + by move=> /le_lt_trans; apply. + by move=> /le_trans; apply; exact/ltW. + + by move=> /andP[]. +- by move: x => [[|] x|[|]//]/= in xy oox *. +Qed. + +(* NB: since we only need derive after this point and since this file is very +long I am wondering whether a new file should not be created now *) +Require Import derive. + +Section FTC. +Context {R : realType}. +Notation mu := lebesgue_measure. +Local Open Scope ereal_scope. + +Let FTC0 (f : R -> R) (a : itv_bound R) : mu.-integrable setT (EFin \o f) -> + let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) f t)%R in + forall x, (a < BRight x) -> lebesgue_pt f x -> + h^-1 *: ((F (h + x)%R - F x) : R^o)%R @[h --> (0:R)%R^'] --> f x. +Proof. +move=> intf F x ax fx. +have locf : locally_integrable setT f. + by apply: integrable_locally => //; exact: openT. +apply: cvg_at_right_left_dnbhs. +- apply/cvg_at_rightP => d [d_gt0 d0]. + pose E x n := `[x, x + d n[%classic%R. + have muE y n : mu (E y n) = (d n)%:E. + rewrite /E lebesgue_measure_itv/= lte_fin ltrDl d_gt0. + by rewrite -EFinD addrAC subrr add0r. + have nice_E y : nicely_shrinking y (E y). + split=> [n|]; first exact: measurable_itv. + exists (2, (fun n => PosNum (d_gt0 n))); split => //= [n z|n]. + rewrite /E/= in_itv/= /ball/= ltr_distlC => /andP[yz ->]. + by rewrite (lt_le_trans _ yz)// ltrBlDr ltrDl. + rewrite (lebesgue_measure_ball _ (ltW _))// -/mu muE -EFinM lee_fin. + by rewrite mulr_natl. + have ixdf n : \int[mu]_(t in [set` Interval a (BRight (x + d n))]) (f t)%:E - + \int[mu]_(t in [set` Interval a (BRight x)]) (f t)%:E = + \int[mu]_(y in E x n) (f y)%:E. + rewrite -[in X in X - _]integral_itv_bndo_bndc//=; last first. + by case: locf => + _ _; exact: measurable_funS. + rewrite (@itv_bndo_setU _ _ (BLeft x))//=; last 2 first. + by case: a ax F => [[|] a|[|]]// /ltW. + by rewrite bnd_simp lerDl ltW. + rewrite integral_setU_EFin//=. + - rewrite addeAC -[X in _ - X]integral_itv_bndo_bndc//=; last first. + by case: locf => + _ _; exact: measurable_funS. + rewrite subee ?add0e//. + by apply: integral_fune_fin_num => //; exact: integrableS intf. + - by case: locf => + _ _; exact: measurable_funS. + - apply/disj_setPRL => z/=. + rewrite /E /= !in_itv/= => /andP[xz zxdn]. + move: a ax {F} => [[|] t/=|[_ /=|//]]. + - rewrite lte_fin => tx. + by apply/negP; rewrite negb_and -leNgt xz orbT. + - rewrite lte_fin => tx. + by apply/negP; rewrite negb_and -!leNgt xz orbT. + - by apply/negP; rewrite -leNgt. + rewrite [f in f n @[n --> \oo] --> _](_ : _ = + fun n => (d n)^-1 *: fine (\int[mu]_(t in E x n) (f t)%:E)); last first. + apply/funext => n; congr (_ *: _); rewrite -fineB/=. + by rewrite /= (addrC (d n) x) ixdf. + by apply: integral_fune_fin_num => //; exact: integrableS intf. + by apply: integral_fune_fin_num => //; exact: integrableS intf. + have := nice_lebesgue_differentiation nice_E locf fx. + rewrite {ixdf} -/mu. + rewrite [g in g n @[n --> \oo] --> _ -> _](_ : _ = + fun n => (d n)^-1%:E * \int[mu]_(y in E x n) (f y)%:E); last first. + by apply/funext => n; rewrite muE. + move/fine_cvgP => [_ /=]. + set g := _ \o _ => gf. + set h := (f in f n @[n --> \oo] --> _). + suff : g = h by move=> <-. + apply/funext => n. + rewrite /g /h /= fineM//. + apply: integral_fune_fin_num => //; first exact: (nice_E _).1. + by apply: integrableS intf => //; exact: (nice_E _).1. +- apply/cvg_at_leftP => d [d_gt0 d0]. + have {}Nd_gt0 n : (0 < - d n)%R by rewrite ltrNr oppr0. + pose E x n := `]x + d n, x]%classic%R. + have muE y n : mu (E y n) = (- d n)%:E. + rewrite /E lebesgue_measure_itv/= lte_fin -ltrBrDr. + by rewrite ltrDl Nd_gt0 -EFinD opprD addrA subrr add0r. + have nice_E y : nicely_shrinking y (E y). + split=> [n|]; first exact: measurable_itv. + exists (2, (fun n => PosNum (Nd_gt0 n))); split => //=. + by rewrite -oppr0; exact: cvgN. + move=> n z. + rewrite /E/= in_itv/= /ball/= => /andP[yz zy]. + by rewrite ltr_distlC opprK yz /= (le_lt_trans zy)// ltrDl. + move=> n. + rewrite lebesgue_measure_ball//; last exact: ltW. + by rewrite -/mu muE -EFinM lee_fin mulr_natl. + have ixdf : {near \oo, + (fun n => \int[mu]_(t in [set` Interval a (BRight (x + d n))]) (f t)%:E - + \int[mu]_(t in [set` Interval a (BRight x)]) (f t)%:E) =1 + (fun n => - \int[mu]_(y in E x n) (f y)%:E)}. + case: a ax {F}; last first. + move=> [_|//]. + apply: nearW => n. + rewrite -[in LHS]integral_itv_bndo_bndc//=; last first. + by case: locf => + _ _; exact: measurable_funS. + rewrite -/mu -[LHS]oppeK; congr oppe. + rewrite oppeB; last first. + rewrite fin_num_adde_defl// fin_numN//. + by apply: integral_fune_fin_num => //; exact: integrableS intf. + rewrite addeC. + rewrite (_ : `]-oo, x] = `]-oo, (x + d n)%R] `|` E x n)%classic; last first. + apply/seteqP; rewrite /E/=; split => [y|y] /=. + rewrite !in_itv/= => ->; rewrite andbT ltNge. + by apply/orP; rewrite orbN. + rewrite !in_itv/= => -[|/andP[] //]. + by move=> /le_trans; apply; rewrite -lerBrDl subrr ltW//. + rewrite integral_setU_EFin//=. + - rewrite addeAC. + rewrite -[X in X - _]integral_itv_bndo_bndc//; last first. + by case: locf => + _ _; exact: measurable_funS. + rewrite subee ?add0e//. + by apply: integral_fune_fin_num => //; exact: integrableS intf. + - exact: (nice_E _).1. + - by case: locf => + _ _; exact: measurable_funS. + - apply/disj_setPLR => z/=. + rewrite /E /= !in_itv/= leNgt => xdnz. + by apply/negP; rewrite negb_and xdnz. + move=> b a ax. + move/cvgrPdist_le : d0. + move/(_ (x - a)%R); rewrite subr_gt0 => /(_ ax)[m _ /=] h. + near=> n. + have mn : (m <= n)%N by near: n; exists m. + rewrite -[in X in X - _]integral_itv_bndo_bndc//=; last first. + by case: locf => + _ _; exact: measurable_funS. + rewrite -/mu -[LHS]oppeK; congr oppe. + rewrite oppeB; last first. + rewrite fin_num_adde_defl// fin_numN//. + by apply: integral_fune_fin_num => //; exact: integrableS intf. + rewrite addeC. + rewrite (@itv_bndo_setU _ _ (BRight (x - - d n)%R))//; last 2 first. + case: b in ax * => /=; rewrite bnd_simp. + rewrite lerBrDl addrC -lerBrDl. + by have := h _ mn; rewrite sub0r gtr0_norm. + rewrite lerBrDl -lerBrDr. + by have := h _ mn; rewrite sub0r gtr0_norm. + by rewrite opprK bnd_simp -lerBrDl subrr ltW. + rewrite integral_setU_EFin//=. + - rewrite addeAC -[X in X - _]integral_itv_bndo_bndc//; last first. + by case: locf => + _ _; exact: measurable_funS. + rewrite opprK subee ?add0e//. + by apply: integral_fune_fin_num => //; exact: integrableS intf. + - by case: locf => + _ _; exact: measurable_funS. + - apply/disj_setPLR => z/=. + rewrite /E /= !in_itv/= => /andP[az zxdn]. + by apply/negP; rewrite negb_and -leNgt zxdn. + 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. + 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. + have := nice_lebesgue_differentiation nice_E locf fx. + rewrite {ixdf} -/mu. + move/fine_cvgP => [_ /=]. + (* TODO: use eq_cvg *) + set g := _ \o _ => gf. + set h := (f in f n @[n --> \oo] --> _). + suff : g = h by move=> <-. + apply/funext => n. + rewrite/g /h /= fineM//=; last first. + apply: integral_fune_fin_num => //; first exact: (nice_E _).1. + by apply: integrableS intf => //; exact: (nice_E _).1. + by rewrite muE/= invrN mulNr -mulrN. +Unshelve. all: by end_near. Qed. + +Lemma FTC1 (f : R -> R) (a : itv_bound R) : mu.-integrable setT (EFin \o f) -> + let F x := (\int[mu]_(t in [set` Interval a (BRight x)(*closed*)]) (f t))%R in + forall x, (a < BRight x) -> lebesgue_pt f x -> + derivable (F : R^o -> R^o) x 1 /\ + (F : R -> R^o)^`() x = f x. +Proof. +move=> intf F x ax fx; split. + apply/cvg_ex; exists (f x). + set g := (f in f n @[n --> _] --> _). + have := FTC0 intf ax fx. + set h := (f in f n @[n --> _] --> _ -> _). + suff : g = h by move=> <-. + by apply/funext => y; rewrite /g /h [y%:A](mulr1). +by apply/cvg_lim; [exact: Rhausdorff|exact: FTC0]. +Qed. + +End FTC. + +Section FTC1_cont. +Context {R : realType}. +Notation mu := lebesgue_measure. +Local Open Scope ereal_scope. + +Lemma cont_lebesgue_pt (f : R -> R) x : measurable_fun setT f -> + {for x, continuous f} -> lebesgue_pt f x. +Proof. +move=> mf xf. +rewrite /lebesgue_pt. +have fx0 : davg f x 0 = 0 by rewrite davg0. +rewrite -[X in _ --> X]fx0. +apply: cvg_at_right_filter. +rewrite fx0. +apply: (@continuous_cvg_davg _ [set x]) => //; rewrite ?inE//. +move=> y; rewrite inE/= => ->. +exact: xf. +Qed. + +Lemma FTC1_cont (f : R -> R) (a : itv_bound R) : + mu.-integrable setT (EFin \o f) -> + let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in + forall x, (a < BRight x) -> {for x, continuous f} -> + derivable (F : R^o -> R^o) x 1 /\ + (F : R -> R^o)^`() x = f x. +Proof. +move=> fi F x ax fx. +have lfx : lebesgue_pt f x. + apply: cont_lebesgue_pt => //. + case/integrableP : fi => + _. + by move/EFin_measurable_fun. +have lif : locally_integrable setT f. + apply: integrable_locally => //. + exact: openT. +have /= := @FTC1 R f a fi x. +move=> /(_ ax lfx)/= [dfx f'xE]. +by split; [exact: dfx|rewrite f'xE]. +Qed. + +End FTC1_cont. + +Section density. +Context {R : realType}. +Notation mu := lebesgue_measure. +Local Open Scope ereal_scope. + +Lemma density (A : set R) : measurable A -> + {ae mu, forall x, + mu (A `&` ball x r) * (fine (mu (ball x r)))^-1%:E + @[r --> 0^'+] --> (\1_A x)%:E}. +Proof. +move=> mA. +have loc_indic : locally_integrable [set: R] \1_A. + split => //. + - exact: openT. + - move=> K _ cK. + apply: (@le_lt_trans _ _ (\int[mu]_(x in K) (cst 1 x))). + apply: ge0_le_integral => //=. + + exact: compact_measurable. + + by do 2 apply: measurableT_comp => //. + + move=> y _. + by rewrite indicE; case: (_ \in _) => //=; rewrite ?(normr1,normr0). + rewrite integral_cst//= ?mul1e. + exact: compact_finite_measure. + exact: compact_measurable. +have := @lebesgue_differentiation _ (\1_A) loc_indic. +apply: filter_app; first exact: (ae_filter_ringOfSetsType [the measure _ _ of mu]). +apply: aeW => /= x Ax. +apply/(cvge_sub0 _ _).1 => //. +move: Ax; rewrite /lebesgue_pt /davg /= -/mu => Ax. +have : ((fine (mu (ball x r)))^-1)%:E * + `|\int[mu]_(y in ball x r) (\1_A y - \1_A x)%:E | @[r --> 0^'+] --> 0. + apply: (@squeeze_cvge _ _ _ R (cst 0) _ _ _ _ _ Ax) => //; last exact: cvg_cst. + near=> a. + apply/andP; split. + by rewrite mule_ge0// lee_fin invr_ge0// fine_ge0. + rewrite lee_pmul2l//. + (* TODO: le_integral_comp_abse use nneg *) + apply: le_abse_integral => //; first exact: measurable_ball. + by apply/EFin_measurable_fun; exact: measurable_funB. + rewrite lte_fin invr_gt0// fine_gt0//. + have -> : mu (ball x a) < +oo by rewrite lebesgue_measure_ball// ltry. + suff : 0 < mu (ball x a) by move=> ->. + by rewrite lebesgue_measure_ball// lte_fin mulrn_wgt0. +set f := (f in f r @[r --> 0^'+] --> _ -> _). +rewrite (_ : f = fun r => ((fine (mu (ball x r)))^-1)%:E * + `|mu (A `&` ball x r) - (\1_A x)%:E * mu (ball x r)|); last first. + apply/funext => r; rewrite /f integralB_EFin//=; last 3 first. + - exact: measurable_ball. + - apply/integrableP; split. + exact/EFin_measurable_fun/measurable_indic. + under eq_integral do rewrite /= ger0_norm//=. + rewrite integral_indic//=; last exact: measurable_ball. + rewrite -/mu (@le_lt_trans _ _ (mu (ball x r)))// ?le_measure// ?inE. + + by apply: measurableI => //; exact: measurable_ball. + + exact: measurable_ball. + + have [r0|r0] := ltP r 0%R. + by rewrite ((ball0 _ _).2 (ltW r0))// /mu measure0. + by rewrite lebesgue_measure_ball//= ?ltry. + - apply/integrableP; split; first exact/EFin_measurable_fun/measurable_cst. + rewrite /= integral_cst//=; last exact: measurable_ball. + have [r0|r0] := ltP r 0%R. + by rewrite ((ball0 _ _).2 (ltW r0))// /mu measure0 mule0. + by rewrite lebesgue_measure_ball//= ?ltry. + rewrite integral_indic//=; last exact: measurable_ball. + by rewrite -/mu integral_cst//; exact: measurable_ball. +rewrite indicE. +have [xA H|xA] := boolP (x \in A); last first. + apply: iffRL; apply/propeqP; apply: eq_cvg => r. + rewrite -mulNrn mulr0n adde0 mul0e sube0. + by rewrite gee0_abs// muleC. +have {H} /cvgeN : ((fine (mu (ball x r)))^-1)%:E * + (mu (ball x r) - mu (A `&` ball x r)) @[r --> 0^'+] --> 0. + move: H; apply: cvg_trans; apply: near_eq_cvg. + near=> r. + rewrite mul1e lee0_abs. + rewrite oppeB//; last first. + rewrite fin_num_adde_defl// fin_numN ge0_fin_numE//. + by rewrite lebesgue_measure_ball//ltry. + by rewrite addeC. + rewrite sube_le0 le_measure// ?inE/=. + by apply: measurableI => //; exact: measurable_ball. + exact: measurable_ball. +rewrite oppe0; apply: cvg_trans; apply: near_eq_cvg; near=> r. +rewrite -mulNrn mulr1n muleBr//; last first. + rewrite fin_num_adde_defr// ge0_fin_numE//. + by rewrite lebesgue_measure_ball//= ?ltry. +rewrite (_ : ((fine (mu (ball x r)))^-1)%:E * mu (ball x r) = 1); last first. + rewrite -[X in _ * X](@fineK _ (mu (ball x r)))//; last first. + by rewrite lebesgue_measure_ball//= ?ltry. + by rewrite -EFinM mulVf// lebesgue_measure_ball//= gt_eqF// mulrn_wgt0. +by rewrite oppeB// addeC EFinN muleC. +Unshelve. all: by end_near. Qed. + +End density. diff --git a/theories/realfun.v b/theories/realfun.v index 29b77b0292..48b2bd8a7a 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -241,7 +241,7 @@ have /fine_cvgP[[m _ mfy_] /= _] := h _ (conj py_ y_p). near \oo => n. have mn : (m <= n)%N by near: n; exists m. have {mn} := mfy_ _ mn. -rewrite /y_ /sval; case: cid2 => /= x _. +by rewrite /y_ /sval; case: cid2 => /= x _. Unshelve. all: by end_near. Qed. Lemma cvge_at_leftP (f : R -> \bar R) (p l : R) : From 68d61c3565d7b2bf8d24a00fde98df2971632f18 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 7 Mar 2024 11:15:21 +0900 Subject: [PATCH 2/6] addressing comments Co-authored-by: zstone1 --- CHANGELOG_UNRELEASED.md | 41 ++ _CoqProject | 1 + classical/mathcomp_extra.v | 7 + classical/set_interval.v | 89 +++- theories/Make | 1 + theories/ftc.v | 221 ++++++++++ theories/lebesgue_integral.v | 800 ++++++++++------------------------- theories/normedtype.v | 22 +- theories/numfun.v | 15 + theories/reals.v | 7 + theories/topology.v | 23 +- 11 files changed, 631 insertions(+), 596 deletions(-) create mode 100644 theories/ftc.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 7de7837285..5a189a6e48 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -10,6 +10,44 @@ - in `lebesgue_integral.v` + lemma `ge0_integralZr` - file `function_spaces.v` +- in `mathcomp_extra.v` + + lemma `invf_plt` + +- in `set_interval.v` + + lemmas `setDitv1r`, `setDitv1l` + + lemmas `set_itvxx`, `itv_bndbnd_setU` + +- in `reals.v` + + lemma `abs_ceil_ge` + +- in `topology.v`: + + lemmas `nbhs_infty_ger`, `nbhs0_ltW`, `nbhs0_lt` + +- in `normedtype.v` + + lemma `closed_ball_ball` + +- in `numfun.v` + + lemma `cvg_indic` + +- in `lebesgue_integral.v` + + lemma `locally_integrable_indic` + + definition `davg`, + lemmas `davg0`, `davgD`, `continuous_cvg_davg` + + definition `lim_sup_davg`, + lemmas `lim_sup_davg_ge0`, `lim_sup_davg_le`, + `continuous_lim_sup_davg`, `lim_sup_davgB`, `lim_sup_davgT_HL_maximal` + + definition `lebesgue_pt`, + lemma `continuous_lebesgue_pt` + + lemma `integral_setU_EFin` + + lemmas `integral_set1`, `ge0_integral_closed_ball`, `integral_setD1_EFin`, + `integral_itv_bndo_bndc`, `integral_itv_obnd_cbnd` + + lemma `lebesgue_differentiation` + + lemma `lebesgue_density` + + definition `nicely_shrinking`, + lemmas `nicely_shrinking_gt0`, `nicely_shrinking_lty`, `nice_lebesgue_differentiation` + +- new file `ftc.v`: + - lemmas `FTC1`, `continuous_FTC1` ### Changed - moved from `topology.v` to `function_spaces.v`: `prod_topology`, @@ -73,6 +111,9 @@ + `lte_addl` -> `lteDl` + `lte_addr` -> `lteDr` +- in `lebesgue_integral.v` + + `integral_setU` -> `ge0_integral_setU` + ### Generalized ### Deprecated diff --git a/_CoqProject b/_CoqProject index 347c3af131..a4387ea7b4 100644 --- a/_CoqProject +++ b/_CoqProject @@ -41,6 +41,7 @@ theories/derive.v theories/measure.v theories/numfun.v theories/lebesgue_integral.v +theories/ftc.v theories/hoelder.v theories/probability.v theories/summability.v diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 49ab82ea28..167e5d2bfc 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -985,3 +985,10 @@ Qed. End path_lt. Arguments last_filterP {d T a} P s. + +(* TODO: in MathComp since version 2.3.0 *) +Lemma invf_plt (F : numFieldType) : + {in Num.pos &, forall x y : F, (x^-1 < y)%R = (y^-1 < x)%R}. +Proof. +by move=> x y ? ?; rewrite -[in LHS](@invrK _ y) ltf_pV2// posrE invr_gt0. +Qed. diff --git a/classical/set_interval.v b/classical/set_interval.v index 7d13ca4bb1..e68a327d6a 100644 --- a/classical/set_interval.v +++ b/classical/set_interval.v @@ -121,23 +121,108 @@ Definition set_itvE := (set_itv1, set_itvoo0, set_itvoc0, set_itvco0, set_itvoo, set_itvcc, set_itvoc, set_itvco, set_itv_infty_infty, set_itv_o_infty, set_itv_c_infty, set_itv_infty_o, set_itv_infty_c, set_itv_infty_set0). -Lemma setUitv1 (a : itv_bound T) (x : T) : (a <= BLeft x)%O -> +Lemma set_itvxx a : [set` Interval a a] = set0. +Proof. by move: a => [[|] a |[|]]; rewrite !set_itvE. Qed. + +Lemma setUitv1 a x : (a <= BLeft x)%O -> [set` Interval a (BLeft x)] `|` [set x] = [set` Interval a (BRight x)]. Proof. move=> ax; apply/predeqP => z /=; rewrite itv_splitU1// [in X in _ <-> X]inE. by rewrite (rwP eqP) (rwP orP) orbC. Qed. -Lemma setU1itv (a : itv_bound T) (x : T) : (BRight x <= a)%O -> +Lemma setU1itv a x : (BRight x <= a)%O -> x |` [set` Interval (BRight x) a] = [set` Interval (BLeft x) a]. Proof. move=> ax; apply/predeqP => z /=; rewrite itv_split1U// [in X in _ <-> X]inE. by rewrite (rwP eqP) (rwP orP) orbC. Qed. +Lemma setDitv1r a x : + [set` Interval a (BRight x)] `\ x = [set` Interval a (BLeft x)]. +Proof. +apply/seteqP; split => [z|z] /=; rewrite !in_itv/=. + by move=> [/andP[-> /= zx] /eqP xz]; rewrite lt_neqAle xz. +by rewrite lt_neqAle => /andP[-> /andP[/eqP ? ->]]. +Qed. + +Lemma setDitv1l a x : + [set` Interval (BLeft x) a] `\ x = [set` Interval (BRight x) a]. +Proof. +apply/seteqP; split => [z|z] /=; rewrite !in_itv/=. + move=> [/andP[xz ->]]; rewrite andbT => /eqP. + by rewrite lt_neqAle eq_sym => ->. +move=> /andP[]; rewrite lt_neqAle => /andP[xz zx ->]. +by rewrite andbT; split => //; exact/nesym/eqP. +Qed. + End set_itv_porderType. Arguments neitv {d T} _. +Section set_itv_orderType. +Variables (d : unit) (T : orderType d). +Implicit Types a x y : itv_bound T. +Local Open Scope order_scope. + +Lemma itv_bndbnd_setU a x y : a <= x -> x <= y -> + ([set` Interval a y] = [set` Interval a x] `|` [set` Interval x y])%classic. +Proof. +rewrite le_eqVlt => /predU1P[<-{x} ay|]; first by rewrite set_itvxx set0U. +move=> /[swap]. +rewrite le_eqVlt => /predU1P[-> ay|]; first by rewrite set_itvxx setU0. +move: y => [yb y/=|[|]]; last 2 first. + by case: x => [|[|]]. + move=> _ ax; apply/seteqP; split => [z|z] /=. + rewrite !in_itv/= !andbT => -> /=; apply/orP. + by move: x => [[|] x/=|[|]//] in ax *; rewrite leNgt ?(orbN,orNb). + rewrite !in_itv/= !andbT => -[/andP[]|]//. + move: x => [[|] x/=|[|]//] in ax *; move: a => [[|] a/=|[|]//] in ax * => //. + - by apply/le_trans; exact/ltW. + - exact/lt_le_trans. + - by move=> /(le_lt_trans ax) /ltW. + - exact/lt_trans. +move=> xy ax; apply/seteqP; split => [z|z] /=. + rewrite !in_itv /= => /andP[]. + move: a ax => [b t /=|[]//= oox _]. + move=> tx -> zxy /=; rewrite zxy andbT/=; apply/orP. + by case: x xy tx => [[|] x/=|[|]//] xy tx; rewrite leNgt ?(orbN,orNb). + move=> ->; rewrite andbT; apply/orP. + by move: x => [[|] x/=|[|]//] in oox xy *; rewrite leNgt ?(orbN,orNb). +rewrite !in_itv/=. +move: a ax => [b t /= tx| [/= oox|/= oox]]. +- move=> [/andP[-> zx]|]. + move: x => [[|] x|[|]//]/= in xy tx zx *. + case: yb => /= in xy *. + by rewrite (lt_trans zx _). + by rewrite (ltW (lt_le_trans zx _)). + rewrite bnd_simp in xy. + case: yb => /=. + by rewrite (le_lt_trans zx _). + by rewrite (ltW (le_lt_trans zx _)). + move: x => [[|] x|[|]//]/= in xy tx *; rewrite bnd_simp in xy tx. + + move=> /andP[xz ->]; rewrite andbT. + case: b => /=. + by rewrite (le_trans _ xz)// ltW. + by rewrite (lt_le_trans tx). + move=> /andP[xz ->]; rewrite andbT. + case: b tx => /= tx; rewrite bnd_simp in tx. + by rewrite ltW// (le_lt_trans _ xz). + by rewrite (lt_trans tx). +- move: x => [[|] x|[|]//]/= in xy oox *; move=> [|]. + + case: yb => /= in xy *. + by move=> /lt_trans; exact. + rewrite bnd_simp in xy. + by move=> /lt_le_trans => /(_ _ xy)/ltW. + + by move=> /andP[]. + + case: yb => /= in xy *. + by move=> /le_lt_trans; apply. + by move=> /le_trans; apply; exact/ltW. + + by move=> /andP[]. +- by move: x => [[|] x|[|]//]/= in xy oox *. +Qed. + +End set_itv_orderType. + Lemma set_itv_ge [disp : unit] [T : porderType disp] [b1 b2 : itv_bound T] : ~~ (b1 < b2)%O -> [set` Interval b1 b2] = set0. Proof. by move=> Nb12; rewrite -subset0 => x /=; rewrite itv_ge. Qed. diff --git a/theories/Make b/theories/Make index 57078763bf..3b5510bef9 100644 --- a/theories/Make +++ b/theories/Make @@ -30,6 +30,7 @@ derive.v measure.v numfun.v lebesgue_integral.v +ftc.v hoelder.v probability.v lebesgue_stieltjes_measure.v diff --git a/theories/ftc.v b/theories/ftc.v new file mode 100644 index 0000000000..d5ab2dc5e5 --- /dev/null +++ b/theories/ftc.v @@ -0,0 +1,221 @@ +(* mathcomp analysis (c) 2023 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. +From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +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. + +(**md**************************************************************************) +(* # Fundamental Theorem of Calculus for the Lebesgue Integral *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import numFieldTopology.Exports. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + +Section FTC. +Context {R : realType}. +Notation mu := lebesgue_measure. +Local Open Scope ereal_scope. +Implicit Types (f : R -> R) (a : itv_bound R). + +Let FTC0 f a : + mu.-integrable setT (EFin \o f) -> + let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) f t)%R in + forall x, a < BRight x -> lebesgue_pt f x -> + h^-1 *: (F (h + x) - F x) @[h --> (0:R)%R^'] --> f x. +Proof. +move=> intf F x ax fx. +have locf : locally_integrable setT f. + by apply: integrable_locally => //; exact: openT. +apply: cvg_at_right_left_dnbhs. +- apply/cvg_at_rightP => d [d_gt0 d0]. + pose E x n := `[x, x + d n[%classic%R. + have muE y n : mu (E y n) = (d n)%:E. + rewrite /E lebesgue_measure_itv/= lte_fin ltrDl d_gt0. + by rewrite -EFinD addrAC subrr add0r. + have nice_E y : nicely_shrinking y (E y). + split=> [n|]; first exact: measurable_itv. + exists (2, (fun n => PosNum (d_gt0 n))); split => //= [n z|n]. + rewrite /E/= in_itv/= /ball/= ltr_distlC => /andP[yz ->]. + by rewrite (lt_le_trans _ yz)// ltrBlDr ltrDl. + rewrite (lebesgue_measure_ball _ (ltW _))// -/mu muE -EFinM lee_fin. + by rewrite mulr_natl. + have ixdf n : \int[mu]_(t in [set` Interval a (BRight (x + d n))]) (f t)%:E - + \int[mu]_(t in [set` Interval a (BRight x)]) (f t)%:E = + \int[mu]_(y in E x n) (f y)%:E. + rewrite -[in X in X - _]integral_itv_bndo_bndc//=; last first. + by case: locf => + _ _; exact: measurable_funS. + rewrite (@itv_bndbnd_setU _ _ _ (BLeft x))//=; last 2 first. + by case: a ax F => [[|] a|[|]]// /ltW. + by rewrite bnd_simp lerDl ltW. + rewrite integral_setU_EFin//=. + - rewrite addeAC -[X in _ - X]integral_itv_bndo_bndc//=; last first. + by case: locf => + _ _; exact: measurable_funS. + rewrite subee ?add0e//. + by apply: integral_fune_fin_num => //; exact: integrableS intf. + - by case: locf => + _ _; exact: measurable_funS. + - apply/disj_setPRL => z/=. + rewrite /E /= !in_itv/= => /andP[xz zxdn]. + move: a ax {F} => [[|] t/=|[_ /=|//]]. + - rewrite lte_fin => tx. + by apply/negP; rewrite negb_and -leNgt xz orbT. + - rewrite lte_fin => tx. + by apply/negP; rewrite negb_and -!leNgt xz orbT. + - by apply/negP; rewrite -leNgt. + rewrite [f in f n @[n --> _] --> _](_ : _ = + fun n => (d n)^-1 *: fine (\int[mu]_(t in E x n) (f t)%:E)); last first. + apply/funext => n; congr (_ *: _); rewrite -fineB/=. + by rewrite /= (addrC (d n) x) ixdf. + by apply: integral_fune_fin_num => //; exact: integrableS intf. + by apply: integral_fune_fin_num => //; exact: integrableS intf. + have := nice_lebesgue_differentiation nice_E locf fx. + rewrite {ixdf} -/mu. + rewrite [g in g n @[n --> _] --> _ -> _](_ : _ = + fun n => (d n)^-1%:E * \int[mu]_(y in E x n) (f y)%:E); last first. + by apply/funext => n; rewrite muE. + move/fine_cvgP => [_ /=]. + set g := _ \o _ => gf. + set h := (f in f n @[n --> \oo] --> _). + suff : g = h by move=> <-. + apply/funext => n. + rewrite /g /h /= fineM//. + apply: integral_fune_fin_num => //; first exact: (nice_E _).1. + by apply: integrableS intf => //; exact: (nice_E _).1. +- apply/cvg_at_leftP => d [d_gt0 d0]. + have {}Nd_gt0 n : (0 < - d n)%R by rewrite ltrNr oppr0. + pose E x n := `]x + d n, x]%classic%R. + have muE y n : mu (E y n) = (- d n)%:E. + rewrite /E lebesgue_measure_itv/= lte_fin -ltrBrDr. + by rewrite ltrDl Nd_gt0 -EFinD opprD addrA subrr add0r. + have nice_E y : nicely_shrinking y (E y). + split=> [n|]; first exact: measurable_itv. + exists (2, (fun n => PosNum (Nd_gt0 n))); split => //=. + by rewrite -oppr0; exact: cvgN. + move=> n z. + rewrite /E/= in_itv/= /ball/= => /andP[yz zy]. + by rewrite ltr_distlC opprK yz /= (le_lt_trans zy)// ltrDl. + move=> n. + rewrite lebesgue_measure_ball//; last exact: ltW. + by rewrite -/mu muE -EFinM lee_fin mulr_natl. + have ixdf : {near \oo, + (fun n => \int[mu]_(t in [set` Interval a (BRight (x + d n))]) (f t)%:E - + \int[mu]_(t in [set` Interval a (BRight x)]) (f t)%:E) =1 + (fun n => - \int[mu]_(y in E x n) (f y)%:E)}. + case: a ax {F}; last first. + move=> [_|//]. + apply: nearW => n. + rewrite -[in LHS]integral_itv_bndo_bndc//=; last first. + by case: locf => + _ _; exact: measurable_funS. + rewrite -/mu -[LHS]oppeK; congr oppe. + rewrite oppeB; last first. + rewrite fin_num_adde_defl// fin_numN//. + by apply: integral_fune_fin_num => //; exact: integrableS intf. + rewrite addeC. + rewrite (_ : `]-oo, x] = `]-oo, (x + d n)%R] `|` E x n)%classic; last first. + by rewrite -itv_bndbnd_setU//= bnd_simp ler_wnDr// ltW. + rewrite integral_setU_EFin//=. + - rewrite addeAC. + rewrite -[X in X - _]integral_itv_bndo_bndc//; last first. + by case: locf => + _ _; exact: measurable_funS. + rewrite subee ?add0e//. + by apply: integral_fune_fin_num => //; exact: integrableS intf. + - exact: (nice_E _).1. + - by case: locf => + _ _; exact: measurable_funS. + - apply/disj_setPLR => z/=. + rewrite /E /= !in_itv/= leNgt => xdnz. + by apply/negP; rewrite negb_and xdnz. + move=> b a ax. + move/cvgrPdist_le : d0. + move/(_ (x - a)%R); rewrite subr_gt0 => /(_ ax)[m _ /=] h. + near=> n. + have mn : (m <= n)%N by near: n; exists m. + rewrite -[in X in X - _]integral_itv_bndo_bndc//=; last first. + by case: locf => + _ _; exact: measurable_funS. + rewrite -/mu -[LHS]oppeK; congr oppe. + rewrite oppeB; last first. + rewrite fin_num_adde_defl// fin_numN//. + by apply: integral_fune_fin_num => //; exact: integrableS intf. + rewrite addeC. + rewrite (@itv_bndbnd_setU _ _ _ (BRight (x - - d n)%R))//; last 2 first. + case: b in ax * => /=; rewrite bnd_simp. + rewrite lerBrDl addrC -lerBrDl. + by have := h _ mn; rewrite sub0r gtr0_norm. + rewrite lerBrDl -lerBrDr. + by have := h _ mn; rewrite sub0r gtr0_norm. + by rewrite opprK bnd_simp -lerBrDl subrr ltW. + rewrite integral_setU_EFin//=. + - rewrite addeAC -[X in X - _]integral_itv_bndo_bndc//; last first. + by case: locf => + _ _; exact: measurable_funS. + rewrite opprK subee ?add0e//. + by apply: integral_fune_fin_num => //; exact: integrableS intf. + - by case: locf => + _ _; exact: measurable_funS. + - apply/disj_setPLR => z/=. + rewrite /E /= !in_itv/= => /andP[az zxdn]. + by apply/negP; rewrite negb_and -leNgt zxdn. + 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. + 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. + have := nice_lebesgue_differentiation nice_E locf fx. + rewrite {ixdf} -/mu. + move/fine_cvgP => [_ /=]. + set g := _ \o _ => gf. + rewrite (@eq_cvg _ _ _ _ g)// => n. + rewrite /g /= fineM//=; last first. + apply: integral_fune_fin_num => //; first exact: (nice_E _).1. + by apply: integrableS intf => //; exact: (nice_E _).1. + by rewrite muE/= invrN mulNr -mulrN. +Unshelve. all: by end_near. Qed. + +(* NB: right-closed interval *) +Lemma FTC1 f a : + mu.-integrable setT (EFin \o f) -> + let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in + forall x, a < BRight x -> lebesgue_pt f x -> + derivable F x 1 /\ + F^`() x = f x. +Proof. +move=> intf F x ax fx; split; last first. + by apply/cvg_lim; [exact: Rhausdorff|exact: FTC0]. +apply/cvg_ex; exists (f x). +set g := (f in f n @[n --> _] --> _). +have := FTC0 intf ax fx. +set h := (f in f n @[n --> _] --> _ -> _). +suff : g = h by move=> <-. +apply/funext => y. +rewrite /g /h /=. +by rewrite [X in F (X + _)](mulr1). +Qed. + +Lemma continuous_FTC1 f a : + mu.-integrable setT (EFin \o f) -> + let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in + forall x, a < BRight x -> {for x, continuous f} -> + derivable F x 1 /\ + F^`() x = f x. +Proof. +move=> fi F x ax fx. +have lfx : lebesgue_pt f x. + apply: continuous_lebesgue_pt => // U xU. + case/integrableP : fi => + _. + by move/EFin_measurable_fun; exact: measurable_funS. +have lif : locally_integrable setT f. + by apply: integrable_locally => //; exact: openT. +have /= := @FTC1 f a fi x. +move=> /(_ ax lfx)/= [dfx f'xE]. +by split; [exact: dfx|rewrite f'xE]. +Qed. + +End FTC. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 718e31ad19..b95ab24d72 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -17,6 +17,9 @@ Require Import esum measure lebesgue_measure numfun realfun function_spaces. (* (linearity, non-decreasingness), the monotone convergence theorem, and *) (* Fatou's lemma. Finally, it proves the linearity properties of the *) (* integral, the dominated convergence theorem and Fubini's theorem, etc. *) +(* This file is further completed by related, standard lemmas such as the *) +(* Hardy–Littlewood maximal inequality and Lebesgue's differentiation *) +(* theorem. *) (* *) (* Main notation: *) (* | Coq notation | | Meaning | *) @@ -1189,6 +1192,14 @@ Proof. by rewrite setIC integral_mkcondr. Qed. End domain_change. Arguments integral_mkcond {d T R mu} D f. +Lemma integral_set0 d (T : measurableType d) (R : realType) + (mu : {measure set T -> \bar R}) (f : T -> \bar R) : + (\int[mu]_(x in set0) f x = 0)%E. +Proof. +rewrite integral_mkcond integral0_eq// => x _. +by rewrite /restrict; case: ifPn => //; rewrite in_set0. +Qed. + Section nondecreasing_integral_limit. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType). @@ -2884,7 +2895,7 @@ Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}). -Lemma integral_setU (A B : set T) (mA : measurable A) (mB : measurable B) +Lemma ge0_integral_setU (A B : set T) (mA : measurable A) (mB : measurable B) (f : T -> \bar R) : measurable_fun (A `|` B) f -> (forall x, (A `|` B) x -> 0 <= f x) -> [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. @@ -2913,7 +2924,7 @@ Lemma subset_integral (A B : set T) (mA : measurable A) (mB : measurable B) (f : T -> \bar R) : measurable_fun B f -> (forall x, B x -> 0 <= f x) -> A `<=` B -> \int[mu]_(x in A) f x <= \int[mu]_(x in B) f x. Proof. -move=> mf f0 AB; rewrite -(setDUK AB) integral_setU//; last 4 first. +move=> mf f0 AB; rewrite -(setDUK AB) ge0_integral_setU//; last 4 first. - exact: measurableD. - by rewrite setDUK. - by move=> x; rewrite setDUK//; exact: f0. @@ -2921,12 +2932,6 @@ move=> mf f0 AB; rewrite -(setDUK AB) integral_setU//; last 4 first. by apply: leeDl; apply: integral_ge0 => x [Bx _]; exact: f0. Qed. -Lemma integral_set0 (f : T -> \bar R) : \int[mu]_(x in set0) f x = 0. -Proof. -rewrite integral_mkcond integral0_eq// => x _. -by rewrite /restrict; case: ifPn => //; rewrite in_set0. -Qed. - Lemma ge0_integral_bigsetU (I : eqType) (F : I -> set T) (f : T -> \bar R) (s : seq I) : (forall n, measurable (F n)) -> uniq s -> trivIset [set` s] F -> @@ -2937,7 +2942,7 @@ Lemma ge0_integral_bigsetU (I : eqType) (F : I -> set T) (f : T -> \bar R) Proof. move=> mF; elim: s => [|h t ih] us tF D mf f0. by rewrite /D 2!big_nil integral_set0. -rewrite /D big_cons integral_setU//. +rewrite /D big_cons ge0_integral_setU//. - rewrite big_cons ih//. + by move: us => /= /andP[]. + by apply: sub_trivIset tF => /= i /= it; rewrite inE it orbT. @@ -2968,6 +2973,30 @@ by apply: subset_integral => //; exact: measurableT_comp. Qed. End subset_integral. +#[deprecated(since="mathcomp-analysis 1.0.1", note="use `ge0_integral_setU` instead")] +Notation integral_setU := ge0_integral_setU (only parsing). + +Local Open Scope ereal_scope. +Lemma integral_setU_EFin d (T : measurableType d) (R : realType) + (mu : {measure set T -> \bar R}) (A B : set T) (f : T -> R) : + measurable A -> measurable B -> + measurable_fun (A `|` B) f -> + [disjoint A & B] -> + \int[mu]_(x in (A `|` B)) (f x)%:E = \int[mu]_(x in A) (f x)%:E + + \int[mu]_(x in B) (f x)%:E. +Proof. +move=> mA mB ABf AB. +rewrite integralE/=. +rewrite ge0_integral_setU//; last exact/measurable_funepos/EFin_measurable_fun. +rewrite ge0_integral_setU//; last exact/measurable_funeneg/EFin_measurable_fun. +rewrite [X in _ = X + _]integralE/=. +rewrite [X in _ = _ + X]integralE/=. +set ap : \bar R := \int[mu]_(x in A) _; set an : \bar R := \int[mu]_(x in A) _. +set bp : \bar R := \int[mu]_(x in B) _; set bn : \bar R := \int[mu]_(x in B) _. +rewrite oppeD 1?addeACA//. +by rewrite ge0_adde_def// inE integral_ge0. +Qed. +Local Close Scope ereal_scope. Section Rintegral. Local Open Scope ereal_scope. @@ -3596,7 +3625,7 @@ by rewrite mule0 -eq_le => /eqP. Qed. Lemma ae_eq_integral_abs (D : set T) (mD : measurable D) (f : T -> \bar R) : - measurable_fun D f -> \int[mu]_(x in D) `|f x| = 0 <-> ae_eq D f (cst 0). + measurable_fun D f -> \int[mu]_(x in D) `|f x| = 0 <-> ae_eq D f (cst 0). Proof. move=> mf; split=> [iDf0|Df0]. exists (D `&` [set x | f x != 0]); split; @@ -3660,7 +3689,7 @@ have f_bounded n x : D x -> `|f_ n x| <= n%:R%:E. move=> Dx; rewrite /f_; have [|_] := leP `|f x| n%:R%:E. by rewrite abse_id. by rewrite gee0_abs// lee_fin. -have if_0 n : \int[mu]_(x in D) `|f_ n x| = 0. +have if_0 n : \int[mu]_(x in D) `|f_ n x| = 0. apply: (@ae_eq_integral_abs_bounded _ _ _ n%:R) => //. by apply: measurable_mine => //; exact: measurableT_comp. exact: f_bounded. @@ -5080,7 +5109,7 @@ exists h; split => //; rewrite [eps%:num]splitr; apply: le_lt_trans. rewrite integralD//; first last. - by apply: integrable_abse; under eq_fun do rewrite EFinB; apply: integrableB. - by apply: integrable_abse; under eq_fun do rewrite EFinB; apply: integrableB. -rewrite EFinD lteD// -(setDKU AE) integral_setU => //; first last. +rewrite EFinD lteD// -(setDKU AE) ge0_integral_setU => //; first last. - by rewrite /disj_set setDKI. - rewrite setDKU //; do 2 apply: measurableT_comp => //. exact: measurable_funB. @@ -5807,6 +5836,19 @@ Proof. by move=> lf lg; apply: locally_integrableD => //; exact: locally_integrableN. Qed. +Lemma locally_integrable_indic D (A : set R) : + open D -> measurable A -> locally_integrable D \1_A. +Proof. +move=> oU; split => // K _ cK. +apply: (@le_lt_trans _ _ (\int[mu]_(x in K) cst 1 x)). + apply: ge0_le_integral => //=; first exact: compact_measurable. + - by do 2 apply: measurableT_comp => //. + - move=> y _. + by rewrite indicE; case: (y \in A) => /=; rewrite ?(normr1,normr0). +by rewrite integral_cst//= ?mul1e; [exact: compact_finite_measure| + exact: compact_measurable]. +Qed. + End locally_integrable. Section iavg. @@ -6048,99 +6090,6 @@ Qed. End hardy_littlewood. -(* PR to MahtComp in progress *) -Lemma invf_plt (F : numFieldType) : - {in Num.pos &, forall x y : F, (x^-1 < y)%R = (y^-1 < x)%R}. -Proof. -by move=> x y ? ?; rewrite -[in LHS](@invrK _ y) ltf_pV2// posrE invr_gt0. -Qed. - -(* TODO: move near setUitv1 in set_interval.v *) -Lemma setDitv1r d (R : porderType d) x (r : R) : - ([set` Interval x (BRight r)] `\ r = [set` Interval x (BLeft r)])%classic. -Proof. -apply/seteqP; split => [z|z] /=; rewrite !in_itv/=. - by move=> [/andP[-> /= zr] /eqP rz]; rewrite lt_neqAle rz. -by rewrite lt_neqAle => /andP[-> /andP[/eqP ? ->]]. -Qed. - -Lemma setDitv1l d (R : porderType d) x (r : R) : - ([set` Interval (BLeft r) x] `\ r = [set` Interval (BRight r) x])%classic. -Proof. -apply/seteqP; split => [z|z] /=; rewrite !in_itv/=. - move=> [/andP[rz ->]]; rewrite andbT => /eqP. - by rewrite lt_neqAle eq_sym => ->. -move=> /andP[]; rewrite lt_neqAle => /andP[rz zr ->]. -by rewrite andbT; split => //; exact/nesym/eqP. -Qed. - -Lemma closed_ball_itv {R : realFieldType} (x s : R) (s0 : (0 < s)%R) : - closed_ball x s = `[x - s, x + s]%classic. -Proof. -rewrite (closed_ballE (x:R^o) s0)/= /closed_ball_/=. -by rewrite set_itvE; apply/seteqP; split => t/=; rewrite ler_distlC. -Qed. - -Lemma ball_itv {R : realFieldType} (x s : R) : - ball x s = `]x - s, x + s[%classic. -Proof. -rewrite -(@ball_normE _ R^o) /ball_ set_itvE. -by apply/seteqP; split => t/=; rewrite ltr_distlC. -Qed. - -Lemma closed_ball_ball {R : realFieldType} (x s : R) (s0 : (0 < s)%R) : - closed_ball x s = [set (x - s)%R] `|` ball x s `|` [set (x + s)%R]. -Proof. -rewrite closed_ball_itv// -(@setU1itv _ _ _ (x - s)%R); last first. - by rewrite bnd_simp lerBlDr -addrA lerDl ltW// addr_gt0. -rewrite -(@setUitv1 _ _ _ (x + s)%R); last first. - by rewrite bnd_simp ltrBlDr -addrA ltrDl addr_gt0. -by rewrite ball_itv setUA. -Qed. - -Lemma abs_ceil_ge (R : realType) (x : R) : (`|x| <= `|ceil x|.+1%:R)%R. -Proof. -rewrite -natr1 natr_absz; have [x0|x0] := ltP 0%R x. - by rewrite !gtr0_norm ?ceil_gt0// (le_trans (ceil_ge _))// lerDl. -by rewrite !ler0_norm ?ceil_le0// /ceil opprK; exact/ltW/lt_succ_floor. -Qed. - -Lemma nbhs_infty_ger {R : realType} (r : R) : - \forall n \near \oo, (r <= n%:R)%R. -Proof. -exists (`|ceil r|)%N => // n /=; rewrite -(ler_nat R); apply: le_trans. -by rewrite (le_trans (ceil_ge _))// natr_absz ler_int ler_norm. -Qed. - -Lemma nbhs0_ltW (R : realFieldType) (x : R) : (0 < x)%R -> - \forall r \near nbhs (0%R:R), (r <= x)%R. -Proof. -exists x => // y; rewrite /ball/= sub0r normrN => /ltW. -by apply: le_trans; rewrite ler_norm. -Qed. - -Lemma nbhs0_lt (R : realType) (x : R) : (0 < x)%R -> - \forall r \near nbhs (0%R:R), (r < x)%R. -Proof. -exists x => // z /=; rewrite sub0r normrN. -by apply: le_lt_trans; rewrite ler_norm. -Qed. - -Lemma cvg_indic {R : realFieldType} (x : R^o) k : - x \in (ball 0 k : set R^o) -> - \1_(ball 0 k : set R^o) y @[y --> x] --> (\1_(ball 0 k) x : R). -Proof. -move=> xB; apply/(@cvgrPdist_le _ R^o) => /= e e0; near=> t. -rewrite !indicE xB/= mem_set//=; first by rewrite subrr normr0// ltW. -near: t. -rewrite inE /ball /= sub0r normrN in xB. -exists ((k - `|x|)/2) => /=; first by rewrite divr_gt0// subr_gt0. -rewrite /ball_/= => z /= h; rewrite /ball/= sub0r normrN. -rewrite -(subrK x z) (le_lt_trans (ler_normD _ _))//. -rewrite -ltrBrDr distrC (lt_le_trans h)//. -by rewrite ler_pdivrMr//= ler_pMr// ?subr_gt0// ler1n. -Unshelve. all: by end_near. Qed. - Section davg. Context {R : realType}. Local Notation mu := (@lebesgue_measure R). @@ -6167,38 +6116,35 @@ move=> mf mg; rewrite (le_trans _ (iavgD _ _ _ _)) //. Qed. Let continuous_integralB_fin_num f x : - measurable_fun setT f -> {for x, continuous f} -> + (forall U, nbhs x U -> measurable_fun U f) -> {for x, continuous f} -> \forall t \near 0%R, \int[mu]_(y in ball x t) `|(f y)%:E - (f x)%:E| \is a fin_num. Proof. move=> mf /cvgrPdist_le fx. near (0%R:R)^'+ => e. have e0 : (0 < e)%R by near: e; exact: nbhs_right_gt. -have [r /= r0] := fx _ e0. -move=> {}fx; near=> t. -rewrite ge0_fin_numE ?integral_ge0//. +have [r /= r0] := fx _ e0 => {}fx. +near=> t; rewrite ge0_fin_numE ?integral_ge0//. rewrite (@le_lt_trans _ _ (\int[mu]_(y in ball x r) `|f y - f x|%:E))//. apply: subset_integral => //=. - exact: measurable_ball. - exact: measurable_ball. - do 2 apply: measurableT_comp => //=; apply: measurable_funB => //. - exact: measurable_funS mf. + by apply: mf; exact: nbhsx_ballx. - by apply: le_ball; near: t; exact: nbhs0_ltW. rewrite (@le_lt_trans _ _ (\int[mu]_(y in ball x r) e%:E))//=. apply: ge0_le_integral => //=. - exact: measurable_ball. - do 2 apply: measurableT_comp => //=; apply: measurable_funB => //. - exact: measurable_funS mf. + by apply: mf => /=; exact: nbhsx_ballx. - by rewrite lee_fin ltW. - by move=> y xry; rewrite lee_fin distrC; exact: fx. -rewrite integral_cst// ?mul1e. - rewrite [X in _ * X](_ : _ = mu (ball x r))//. - by rewrite lebesgue_measure_ball// ?ltry// ltW. -exact: measurable_ball. +rewrite integral_cst// ?mul1e /=; last exact: measurable_ball. +by rewrite lebesgue_measure_ball// ?ltry// ltW. Unshelve. all: by end_near. Qed. Let continuous_davg_fin_num f x : - measurable_fun setT f -> {for x, continuous f} -> + (forall U, nbhs x U -> measurable_fun U f) -> {for x, continuous f} -> \forall A \near 0%R, davg f x A \is a fin_num. Proof. move=> mf fx. @@ -6206,23 +6152,22 @@ have [e /= e0 exf] := continuous_integralB_fin_num mf fx. move/cvgrPdist_le in fx. near (0%R:R)^'+ => r. have r0 : (0 < r)%R by near: r; exact: nbhs_right_gt. -have [d /= d0] := fx _ e0. -move=> {}fx; near=> t. -have [t0|t0] := leP t 0%R; first by rewrite davg0. -by rewrite fin_numM// exf//=. +have [d /= d0] := fx _ e0 => {}fx. +near=> t; have [t0|t0] := leP t 0%R; first by rewrite davg0. +by rewrite fin_numM// exf/=. Unshelve. all: by end_near. Qed. -(* TODO: should this be proved without the two Let's above? *) -Lemma continuous_cvg_davg (E : set R) (f : R -> R) : - measurable_fun setT f -> {in E, continuous f} -> - {in E, forall x, davg f x r @[r --> 0%R] --> 0}. +(* NB: should this be proved without the two Let's above? *) +Lemma continuous_cvg_davg (f : R -> R) x : + (forall U, nbhs x U -> measurable_fun U f) -> {for x, continuous f} -> + davg f x r @[r --> 0%R] --> 0. Proof. -move=> mf cf x Ex; apply/fine_cvgP => //; split. - by apply: (@continuous_davg_fin_num) => //; exact: cf. +move=> mf cfx; apply/fine_cvgP; split. + exact: continuous_davg_fin_num. apply/cvgrPdist_le => e e0. -have /cvgrPdist_le /= fx := cf _ Ex. -have [r /= r0] := fx _ e0 => xrf. -have [d /= d0 dfx] := continuous_davg_fin_num mf (cf _ Ex). +have /cvgrPdist_le /= fx := cfx. +have [r /= r0] := fx _ e0 => {}fx. +have [d /= d0 dfx] := continuous_davg_fin_num mf cfx. near=> t. have [t0|t0] := leP t 0%R; first by rewrite /= davg0//= subrr normr0 ltW. rewrite sub0r normrN /= ger0_norm; last first. @@ -6235,13 +6180,12 @@ rewrite (@le_trans _ _ (\int[mu]_(y in ball x t) e%:E))//. apply: ge0_le_integral => //=. - exact: measurable_ball. - do 2 apply: measurableT_comp => //=; apply: measurable_funB => //. - exact: measurable_funS mf. + by apply: mf => /=; exact: nbhsx_ballx. - by move=> y xty; rewrite lee_fin ltW. - - move=> y xty; rewrite lee_fin distrC xrf//. + - move=> y xty; rewrite lee_fin distrC fx//. by apply: (lt_le_trans xty); near: t; exact: nbhs0_ltW. -rewrite integral_cst//; last exact: measurable_ball. -rewrite [X in e%:E * X](_ : _ = mu (ball x t))// muleC. -by rewrite lebesgue_measure_ball// ?ltry// ltW. +rewrite integral_cst//=; last exact: measurable_ball. +by rewrite muleC lebesgue_measure_ball// ?ltry// ltW. Unshelve. all: by end_near. Qed. End davg. @@ -6259,56 +6203,62 @@ Lemma lim_sup_davg_ge0 f x : 0 <= f^* x. Proof. by apply: lime_sup_ge0 => y; rewrite /davg iavg_ge0. Qed. Lemma lim_sup_davg_le f g x : - measurable_fun setT f -> locally_integrable setT g -> + (forall U, nbhs x U -> measurable_fun U f) -> + (forall U, nbhs x U -> measurable_fun U g) -> (f \+ g)%R^* x <= (f^* \+ g^*) x. Proof. -move=> mf /= [mg _ goo]; apply: le_trans (lime_supD _); last first. +move=> mf /= mg; apply: le_trans (lime_supD _); last first. by rewrite ge0_adde_def// inE; exact: lim_sup_davg_ge0. -apply: lime_sup_le => r r0 y y0 ry. -exact: (davgD (measurable_funS _ _ mf) (measurable_funS _ _ mg)). +apply: lime_sup_le => r r0 y; rewrite neq_lt => /orP[y0|y0 ry]. + by rewrite !davg0 ?adde0// ltW. +by apply: davgD; [apply: mf|apply: mg]; exact: nbhsx_ballx. Qed. -Lemma continuous_lim_sup_davg (E : set R) f : - measurable_fun setT f -> {in E, continuous f} -> {in E, f^* =1 cst 0}. -Proof. -move=> mg gx x xE. -by have /lim_lime_sup := continuous_cvg_davg mg gx xE. -Qed. +Lemma continuous_lim_sup_davg f x : + (forall U, nbhs x U -> measurable_fun U f) -> {for x, continuous f} -> + f^* x = 0. +Proof. by move=> mg gx; have /lim_lime_sup := continuous_cvg_davg mg gx. Qed. -Lemma lim_sup_davgB (E : set R) f g : - measurable_fun setT f -> {in E, continuous g} -> +Lemma lim_sup_davgB f g x : + (forall U, nbhs x U -> measurable_fun U f) -> {for x, continuous g} -> locally_integrable [set: R] g -> - {in E, (f \- g)%R^* =1 f^*}. + (f \- g)%R^* x = f^* x. Proof. -move=> mf cg locg x Ex. -apply/eqP; rewrite eq_le; apply/andP; split. +move=> mf cg locg; apply/eqP; rewrite eq_le; apply/andP; split. - rewrite [leRHS](_ : _ = f^* x + (\- g)%R^* x). - by apply: lim_sup_davg_le => //; exact: locally_integrableN. - rewrite (@continuous_lim_sup_davg [set x] (- g)%R) ?adde0//. - + by apply: measurableT_comp => //; case: locg. - + by move=> y; rewrite inE/= => -> /=; exact/continuousN/cg. - + by rewrite inE. + apply: lim_sup_davg_le; [exact: mf|move=> U xU]. + apply/(measurable_comp measurableT) => //. + by case: locg => + _ _; exact: measurable_funS. + rewrite (@continuous_lim_sup_davg (- g)%R); first by rewrite adde0. + - move=> U xU; apply/(measurable_comp measurableT) => //. + by case: locg => + _ _; apply: measurable_funS. + + by move=> y; exact/continuousN/cg. - rewrite [leRHS](_ : _ = ((f \- g)%R^* \+ g^*) x)//. - rewrite {1}(_ : f = f \- g + g)%R; last first. - by apply/funext => y /=; rewrite subrK. - by apply: lim_sup_davg_le => //; apply: measurable_funB => //; case: locg. - rewrite [X in _ + X](@continuous_lim_sup_davg [set x]) ?adde0//. - + by case: locg. - + by move=> y; rewrite inE/= => ->; exact: cg. - + by rewrite inE. + rewrite {1}(_ : f = f \- g + g)%R; last by apply/funext => y; rewrite subrK. + apply: lim_sup_davg_le; [move=> U xU|]. + apply: measurable_funB; [exact: mf|]. + by case: locg => + _ _; exact: measurable_funS. + by move=> U xU; case: locg => + _ _; exact: measurable_funS. + rewrite [X in _ + X](@continuous_lim_sup_davg _ x); [by rewrite adde0| |by[]]. + by move=> U xU; case: locg => + _ _; exact: measurable_funS. Qed. Local Notation mu := (@lebesgue_measure R). +Let is_cvg_ereal_sup_davg f x : + cvg (ereal_sup [set davg f x y | y in ball 0%R e `\ 0%R] @[e --> 0^'+]). +Proof. +apply: nondecreasing_at_right_is_cvge; near=> e => y z. +rewrite !in_itv/= => /andP[y0 ye] /andP[z0 ze] yz. +apply: le_ereal_sup => _ /= -[b [yb b0]] <-. +by exists b => //; split => //; exact: le_ball yb. +Unshelve. all: by end_near. Qed. + Lemma lim_sup_davgT_HL_maximal f (x : R) : locally_integrable setT f -> f^* x <= HL_maximal f x + `|f x|%:E. Proof. move=> [mf _ locf]; rewrite /lim_sup_davg lime_sup_lim; apply: lime_le. - (* TODO: should this be a lemma? *) - apply: nondecreasing_at_right_is_cvge; near=> e => y z. - rewrite !in_itv/= => /andP[y0 ye] /andP[z0 ze] yz. - apply: le_ereal_sup => _ /= -[b [yb b0]] <-. - by exists b => //; split => //; exact: le_ball yb. + exact: is_cvg_ereal_sup_davg. near=> e. apply: ub_ereal_sup => _ [b [eb] /= b0] <-. suff : forall r, davg f x r <= HL_maximal f x + `|f x|%:E by exact. @@ -6350,31 +6300,15 @@ End lim_sup_davg. Definition lebesgue_pt {R : realType} (f : R -> R) (x : R) := davg f x r @[r --> (0%R:R)^'+] --> 0%E. -Local Open Scope ereal_scope. -(* does not require a nonneg function - whereas integral_setU goes (and should maybe be renamed ge0_integral_setU) *) -Lemma integral_setU_EFin d (T : measurableType d) (R : realType) - (mu : {measure set T -> \bar R}) (A B : set T) (f : T -> R) : - measurable A -> measurable B -> - measurable_fun (A `|` B) f -> - [disjoint A & B] -> - \int[mu]_(x in (A `|` B)) (f x)%:E = \int[mu]_(x in A) (f x)%:E + - \int[mu]_(x in B) (f x)%:E. +Lemma continuous_lebesgue_pt {R : realType} (f : R -> R) x : + (forall U, nbhs x U -> measurable_fun U f) -> {for x, continuous f} -> + lebesgue_pt f x. Proof. -move=> mA mB ABf AB. -rewrite integralE/=. -rewrite integral_setU//; last exact/measurable_funepos/EFin_measurable_fun. -rewrite integral_setU//; last exact/measurable_funeneg/EFin_measurable_fun. -rewrite [X in _ = X + _]integralE/=. -rewrite [X in _ = _ + X]integralE/=. -set ap : \bar R := \int[mu]_(x in A) _; set an : \bar R := \int[mu]_(x in A) _. -set bp : \bar R := \int[mu]_(x in B) _; set bn : \bar R := \int[mu]_(x in B) _. -rewrite oppeD 1?addeACA//. -by rewrite ge0_adde_def// inE integral_ge0. +move=> mf xf; rewrite /lebesgue_pt -[X in _ --> X](@davg0 _ f x 0)//. +by apply: cvg_at_right_filter; rewrite davg0//; exact: continuous_cvg_davg. Qed. -Local Close Scope ereal_scope. -Section lebesgue_integral_extra. +Section lebesgue_measure_integral. Context {R : realType}. Local Notation mu := (@lebesgue_measure R). Local Open Scope ereal_scope. @@ -6385,20 +6319,19 @@ rewrite (eq_integral (cst (f r)))/=; last by move=> x; rewrite inE/= => ->. by rewrite integral_cst//= lebesgue_measure_set1 mule0. Qed. -Lemma ge0_integral_ball_closed (r : R) (r0 : (0 < r)%R) (f : R -> \bar R) : +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) -> - \int[mu]_(x in ball 0%R r) f x = - \int[mu]_(x in closed_ball 0%R r) f x. + (forall x, x \in closed_ball 0%R r -> 0 <= f x) -> + \int[mu]_(x in closed_ball 0%R r) f x = \int[mu]_(x in ball 0%R r) f x. Proof. move=> mf f0. -rewrite closed_ball_ball//= sub0r add0r integral_setU//=; last 4 first. +rewrite closed_ball_ball//= sub0r add0r ge0_integral_setU//=; last 4 first. by apply: measurableU => //; exact: measurable_ball. by move: mf; rewrite closed_ball_ball// sub0r add0r. by move=> x H; rewrite f0// closed_ball_ball// inE/= sub0r add0r. apply/disj_setPLR => x [->/=|]; first by apply/eqP; rewrite lt_eqF// gtrN. by rewrite /ball/= sub0r normrN => /ltr_normlW ?; apply/eqP; rewrite lt_eqF. -rewrite integral_set1 adde0 integral_setU//=. +rewrite integral_set1 adde0 ge0_integral_setU//=. - by rewrite integral_set1//= ?add0e. - exact: measurable_ball. - apply: measurable_funS mf; first exact: measurable_closed_ball. @@ -6410,9 +6343,9 @@ Qed. Lemma integral_setD1_EFin (f : R -> R) r (D : set R) : measurable D -> measurable_fun D f -> D r -> - \int[mu]_(x in D) (f x)%:E = \int[mu]_(x in D `\ r) (f x)%:E. + \int[mu]_(x in D `\ r) (f x)%:E = \int[mu]_(x in D) (f x)%:E. Proof. -move=> mD mf Dr; rewrite -[in LHS](@setD1K _ r D)// integral_setU_EFin//. +move=> mD mf Dr; rewrite -[in RHS](@setD1K _ r D)// integral_setU_EFin//. - by rewrite integral_set1// ?add0e. - exact: measurableD. - by rewrite setD1K. @@ -6425,7 +6358,7 @@ Lemma integral_itv_bndo_bndc (a : itv_bound R) (r : R) (f : R -> R) : \int[mu]_(x in [set` Interval a (BRight r)]) (f x)%:E. Proof. move=> mf; have [ar|ar] := leP a (BLeft r). -- rewrite [RHS](@integral_setD1_EFin _ r) ?setDitv1r//. +- rewrite -[RHS](@integral_setD1_EFin _ r) ?setDitv1r//. by rewrite /= in_itv /= lexx andbT {mf}; case: a ar => -[]. - by rewrite !set_itv_ge// -leNgt// ltW. Qed. @@ -6436,12 +6369,12 @@ Lemma integral_itv_obnd_cbnd (r : R) (b : itv_bound R) (f : R -> R) : \int[mu]_(x in [set` Interval (BLeft r) b]) (f x)%:E. Proof. move=> mf; have [rb|rb] := leP (BRight r) b. -- rewrite [RHS](@integral_setD1_EFin _ r) ?setDitv1l//. +- rewrite -[RHS](@integral_setD1_EFin _ r) ?setDitv1l//. by rewrite /= in_itv /= lexx/= {mf}; case: b rb => -[]. - by rewrite !set_itv_ge// -leNgt -?ltBRight_leBLeft// ltW. Qed. -End lebesgue_integral_extra. +End lebesgue_measure_integral. Section lebesgue_differentiation. Context {R : realType}. @@ -6563,9 +6496,12 @@ have davgfEe : B k `&` [set x | (f_ k)^* x > e%:E] `<=` Ee. move=> n; rewrite [X in X `<=`_](_ : _ = B k `&` [set x | e%:E < (f_ k \- g_B n)%R^* x]); last first. apply/seteqP; split => [x [Ex] /=|x [Ex] /=]. - rewrite (@lim_sup_davgB _ (B k)) ?inE//. - by move/EFin_measurable_fun : mf; exact: measurable_funS. - by rewrite (@lim_sup_davgB _ (B k)) ?inE//; move/EFin_measurable_fun : mf. + rewrite lim_sup_davgB//. + by move=> U xU; move/EFin_measurable_fun : mf; exact: measurable_funS. + by apply: cg_B; rewrite inE. + rewrite lim_sup_davgB//. + by move=> U xU; move/EFin_measurable_fun : mf; exact: measurable_funS. + by apply: cg_B; rewrite inE. move=> r /= [Er] efgnr; split => //. have {}efgnr := lt_le_trans efgnr (lim_sup_davgT_HL_maximal r (locf_g_B n)). have [|h] := ltP (e / 2)%:E (HL_maximal (f_ k \- g_B n)%R r); first by left. @@ -6633,7 +6569,7 @@ have mfk k : mu.-integrable setT (EFin \o fk k). 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_ball_closed//. + rewrite setTI -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}. @@ -6694,6 +6630,76 @@ Unshelve. all: by end_near. Qed. End lebesgue_differentiation. +Section density. +Context {R : realType}. +Local Notation mu := lebesgue_measure. +Local Open Scope ereal_scope. + +Lemma lebesgue_density (A : set R) : measurable A -> + {ae mu, forall x, mu (A `&` ball x r) * (fine (mu (ball x r)))^-1%:E + @[r --> 0^'+] --> (\1_A x)%:E}. +Proof. +move=> mA; have := lebesgue_differentiation (locally_integrable_indic openT mA). +apply: filter_app; first exact: (ae_filter_ringOfSetsType mu). +apply: aeW => /= x Ax. +apply/(cvge_sub0 _ _).1 => //. +move: Ax; rewrite /lebesgue_pt /davg /= -/mu => Ax. +have : (fine (mu (ball x r)))^-1%:E * + `|\int[mu]_(y in ball x r) (\1_A y - \1_A x)%:E | @[r --> 0^'+] --> 0. + apply: (@squeeze_cvge _ _ _ R (cst 0) _ _ _ _ _ Ax) => //; [|exact: cvg_cst]. + near=> a. + apply/andP; split; first by rewrite mule_ge0// lee_fin invr_ge0// fine_ge0. + rewrite lee_pmul2l//; last first. + rewrite lte_fin invr_gt0// fine_gt0//. + by rewrite lebesgue_measure_ball// ltry andbT lte_fin mulrn_wgt0. + apply: le_abse_integral => //; first exact: measurable_ball. + by apply/EFin_measurable_fun; exact: measurable_funB. +set f := (f in f r @[r --> 0^'+] --> _ -> _). +rewrite (_ : f = fun r => (fine (mu (ball x r)))^-1%:E * + `|mu (A `&` ball x r) - (\1_A x)%:E * mu (ball x r)|); last first. + apply/funext => r; rewrite /f integralB_EFin//=; last 3 first. + - exact: measurable_ball. + - apply/integrableP; split. + exact/EFin_measurable_fun/measurable_indic. + under eq_integral do rewrite /= ger0_norm//=. + rewrite integral_indic//=; last exact: measurable_ball. + rewrite -/mu (@le_lt_trans _ _ (mu (ball x r)))// ?le_measure// ?inE. + + by apply: measurableI => //; exact: measurable_ball. + + exact: measurable_ball. + + have [r0|r0] := ltP r 0%R. + by rewrite ((ball0 _ _).2 (ltW r0))// /mu measure0. + by rewrite lebesgue_measure_ball//= ?ltry. + - apply/integrableP; split; first exact/EFin_measurable_fun/measurable_cst. + rewrite /= integral_cst//=; last exact: measurable_ball. + have [r0|r0] := ltP r 0%R. + by rewrite ((ball0 _ _).2 (ltW r0))// /mu measure0 mule0. + by rewrite lebesgue_measure_ball//= ?ltry. + rewrite integral_indic//=; last exact: measurable_ball. + by rewrite -/mu integral_cst//; exact: measurable_ball. +rewrite indicE; have [xA xrA0|xA] := boolP (x \in A); last first. + apply: iffRL; apply/propeqP; apply: eq_cvg => r. + by rewrite -mulNrn mulr0n adde0 mul0e sube0 gee0_abs// muleC. +have {xrA0} /cvgeN : (fine (mu (ball x r)))^-1%:E * + (mu (ball x r) - mu (A `&` ball x r)) @[r --> 0^'+] --> 0. + move: xrA0; apply: cvg_trans; apply: near_eq_cvg; near=> r. + rewrite mul1e lee0_abs; last first. + rewrite sube_le0 le_measure// ?inE/=; last exact: measurable_ball. + by apply: measurableI => //; exact: measurable_ball. + rewrite oppeB//; first by rewrite addeC. + rewrite fin_num_adde_defl// fin_numN ge0_fin_numE//. + by rewrite lebesgue_measure_ball// ltry. +rewrite oppe0; apply: cvg_trans; apply: near_eq_cvg; near=> r. +rewrite -mulNrn mulr1n muleBr//; last first. + by rewrite fin_num_adde_defr// ge0_fin_numE// lebesgue_measure_ball//= ?ltry. +rewrite (_ : (fine (mu (ball x r)))^-1%:E * mu (ball x r) = 1); last first. + rewrite -[X in _ * X](@fineK _ (mu (ball x r)))//; last first. + by rewrite lebesgue_measure_ball//= ?ltry. + by rewrite -EFinM mulVf// lebesgue_measure_ball//= gt_eqF// mulrn_wgt0. +by rewrite oppeB// addeC EFinN muleC. +Unshelve. all: by end_near. Qed. + +End density. + Section nicely_shrinking. Context {R : realType}. Implicit Types (x : R) (E : (set R)^nat). @@ -6740,7 +6746,7 @@ Lemma nice_lebesgue_differentiation (f : R -> R) : @[n --> \oo] --> (f x)%:E. Proof. move=> locf x fx; apply/(cvge_sub0 _ _).1 => //=; apply/cvg_abse0P. -pose r_ x : {posnum R}^nat := (sval (cid (hE x).2)).2. +pose r_ x : {posnum R} ^nat := (sval (cid (hE x).2)).2. pose C := (sval (cid (hE x).2)).1. have C_gt0 : (0 < C)%R by rewrite /C /sval/=; case: cid => -[? ?] []. have r_0 y : (r_ y n)%:num @[n --> \oo] --> (0%R : R). @@ -6776,8 +6782,7 @@ apply: (@le_trans _ _ ((fine (mu (E x n)))^-1%:E * rewrite integralD//=. - exact: (hE x).1. - apply/integrableP; split. - apply/EFin_measurable_fun. - by case: locf => + _ _; exact: measurable_funS. + by apply/EFin_measurable_fun; case: locf => + _ _; exact: measurable_funS. rewrite (@le_lt_trans _ _ (\int[mu]_(y in closed_ball x (r_ x n)%:num) `|(f y)%:E|))//. apply: subset_integral => //. @@ -6798,7 +6803,7 @@ rewrite muleA lee_pmul//. rewrite posrE mulr_gt0// ?invr_gt0// fine_gt0//. by rewrite lebesgue_measure_ball// ltry andbT lte_fin mulrn_wgt0. rewrite lter_pdivrMl // -lee_fin EFinM fineK; last first. - by rewrite lebesgue_measure_ball// ltry andbT lte_fin mulrn_wgt0. + by rewrite lebesgue_measure_ball// ltry andbT lte_fin mulrn_wgt0. rewrite fineK; last by rewrite ge0_fin_numE// (nicely_shrinking_lty (hE x)). exact: muEr_. + apply: le_trans. @@ -6813,384 +6818,3 @@ rewrite muleA lee_pmul//. Unshelve. all: by end_near. Qed. End nice_lebesgue_differentiation. - -Lemma set_itvxx {R : realDomainType} (x : itv_bound R) : [set` Interval x x] = set0. -Proof. by move: x => [[|] x |[|]]; rewrite !set_itvE. Qed. - -Lemma itv_bndo_setU {R : realDomainType} (a x y : itv_bound R) : - (a <= x)%O -> (x <= y)%O -> - ([set` Interval a y] = [set` Interval a x] `|` [set` Interval x y])%classic. -Proof. -rewrite le_eqVlt => /predU1P[<-{x} ay|]; first by rewrite set_itvxx set0U. -move=> /[swap]. -rewrite le_eqVlt => /predU1P[-> ay|]; first by rewrite set_itvxx setU0. -move: y => [yb y/=|[|]]; last 2 first. - by case: x => [|[|]]. - move=> _ ax; apply/seteqP; split => [z|z] /=. - rewrite !in_itv/= !andbT => -> /=; apply/orP. - by move: x => [[|] x/=|[|]//] in ax *; rewrite leNgt ?(orbN,orNb). - rewrite !in_itv/= !andbT => -[/andP[]|]//. - move: x => [[|] x/=|[|]//] in ax *; move: a => [[|] a/=|[|]//] in ax * => //. - - by apply/le_trans; exact/ltW. - - exact/lt_le_trans. - - by move=> /(le_lt_trans ax) /ltW. - - exact/lt_trans. -move=> xy ax; apply/seteqP; split => [z|z] /=. - rewrite !in_itv /= => /andP[]. - move: a ax => [b t /=|[]//= oox _]. - move=> tx -> zxy /=; rewrite zxy andbT/=; apply/orP. - by case: x xy tx => [[|] x/=|[|]//] xy tx; rewrite leNgt ?(orbN,orNb). - move=> ->; rewrite andbT; apply/orP. - by move: x => [[|] x/=|[|]//] in oox xy *; rewrite leNgt ?(orbN,orNb). -rewrite !in_itv/=. -move: a ax => [b t /= tx| [/= oox|/= oox]]. -- move=> [/andP[-> zx]|]. - move: x => [[|] x|[|]//]/= in xy tx zx *. - case: yb => /= in xy *. - by rewrite (lt_trans zx _). - by rewrite (ltW (lt_le_trans zx _)). - rewrite bnd_simp in xy. - case: yb => /=. - by rewrite (le_lt_trans zx _). - by rewrite (ltW (le_lt_trans zx _)). - move: x => [[|] x|[|]//]/= in xy tx *; rewrite bnd_simp in xy tx. - + move=> /andP[xz ->]; rewrite andbT. - case: b => /=. - by rewrite (le_trans _ xz)// ltW. - by rewrite (lt_le_trans tx). - move=> /andP[xz ->]; rewrite andbT. - case: b tx => /= tx; rewrite bnd_simp in tx. - by rewrite ltW// (le_lt_trans _ xz). - by rewrite (lt_trans tx). -- move: x => [[|] x|[|]//]/= in xy oox *; move=> [|]. - + case: yb => /= in xy *. - by move=> /lt_trans; exact. - rewrite bnd_simp in xy. - by move=> /lt_le_trans => /(_ _ xy)/ltW. - + by move=> /andP[]. - + case: yb => /= in xy *. - by move=> /le_lt_trans; apply. - by move=> /le_trans; apply; exact/ltW. - + by move=> /andP[]. -- by move: x => [[|] x|[|]//]/= in xy oox *. -Qed. - -(* NB: since we only need derive after this point and since this file is very -long I am wondering whether a new file should not be created now *) -Require Import derive. - -Section FTC. -Context {R : realType}. -Notation mu := lebesgue_measure. -Local Open Scope ereal_scope. - -Let FTC0 (f : R -> R) (a : itv_bound R) : mu.-integrable setT (EFin \o f) -> - let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) f t)%R in - forall x, (a < BRight x) -> lebesgue_pt f x -> - h^-1 *: ((F (h + x)%R - F x) : R^o)%R @[h --> (0:R)%R^'] --> f x. -Proof. -move=> intf F x ax fx. -have locf : locally_integrable setT f. - by apply: integrable_locally => //; exact: openT. -apply: cvg_at_right_left_dnbhs. -- apply/cvg_at_rightP => d [d_gt0 d0]. - pose E x n := `[x, x + d n[%classic%R. - have muE y n : mu (E y n) = (d n)%:E. - rewrite /E lebesgue_measure_itv/= lte_fin ltrDl d_gt0. - by rewrite -EFinD addrAC subrr add0r. - have nice_E y : nicely_shrinking y (E y). - split=> [n|]; first exact: measurable_itv. - exists (2, (fun n => PosNum (d_gt0 n))); split => //= [n z|n]. - rewrite /E/= in_itv/= /ball/= ltr_distlC => /andP[yz ->]. - by rewrite (lt_le_trans _ yz)// ltrBlDr ltrDl. - rewrite (lebesgue_measure_ball _ (ltW _))// -/mu muE -EFinM lee_fin. - by rewrite mulr_natl. - have ixdf n : \int[mu]_(t in [set` Interval a (BRight (x + d n))]) (f t)%:E - - \int[mu]_(t in [set` Interval a (BRight x)]) (f t)%:E = - \int[mu]_(y in E x n) (f y)%:E. - rewrite -[in X in X - _]integral_itv_bndo_bndc//=; last first. - by case: locf => + _ _; exact: measurable_funS. - rewrite (@itv_bndo_setU _ _ (BLeft x))//=; last 2 first. - by case: a ax F => [[|] a|[|]]// /ltW. - by rewrite bnd_simp lerDl ltW. - rewrite integral_setU_EFin//=. - - rewrite addeAC -[X in _ - X]integral_itv_bndo_bndc//=; last first. - by case: locf => + _ _; exact: measurable_funS. - rewrite subee ?add0e//. - by apply: integral_fune_fin_num => //; exact: integrableS intf. - - by case: locf => + _ _; exact: measurable_funS. - - apply/disj_setPRL => z/=. - rewrite /E /= !in_itv/= => /andP[xz zxdn]. - move: a ax {F} => [[|] t/=|[_ /=|//]]. - - rewrite lte_fin => tx. - by apply/negP; rewrite negb_and -leNgt xz orbT. - - rewrite lte_fin => tx. - by apply/negP; rewrite negb_and -!leNgt xz orbT. - - by apply/negP; rewrite -leNgt. - rewrite [f in f n @[n --> \oo] --> _](_ : _ = - fun n => (d n)^-1 *: fine (\int[mu]_(t in E x n) (f t)%:E)); last first. - apply/funext => n; congr (_ *: _); rewrite -fineB/=. - by rewrite /= (addrC (d n) x) ixdf. - by apply: integral_fune_fin_num => //; exact: integrableS intf. - by apply: integral_fune_fin_num => //; exact: integrableS intf. - have := nice_lebesgue_differentiation nice_E locf fx. - rewrite {ixdf} -/mu. - rewrite [g in g n @[n --> \oo] --> _ -> _](_ : _ = - fun n => (d n)^-1%:E * \int[mu]_(y in E x n) (f y)%:E); last first. - by apply/funext => n; rewrite muE. - move/fine_cvgP => [_ /=]. - set g := _ \o _ => gf. - set h := (f in f n @[n --> \oo] --> _). - suff : g = h by move=> <-. - apply/funext => n. - rewrite /g /h /= fineM//. - apply: integral_fune_fin_num => //; first exact: (nice_E _).1. - by apply: integrableS intf => //; exact: (nice_E _).1. -- apply/cvg_at_leftP => d [d_gt0 d0]. - have {}Nd_gt0 n : (0 < - d n)%R by rewrite ltrNr oppr0. - pose E x n := `]x + d n, x]%classic%R. - have muE y n : mu (E y n) = (- d n)%:E. - rewrite /E lebesgue_measure_itv/= lte_fin -ltrBrDr. - by rewrite ltrDl Nd_gt0 -EFinD opprD addrA subrr add0r. - have nice_E y : nicely_shrinking y (E y). - split=> [n|]; first exact: measurable_itv. - exists (2, (fun n => PosNum (Nd_gt0 n))); split => //=. - by rewrite -oppr0; exact: cvgN. - move=> n z. - rewrite /E/= in_itv/= /ball/= => /andP[yz zy]. - by rewrite ltr_distlC opprK yz /= (le_lt_trans zy)// ltrDl. - move=> n. - rewrite lebesgue_measure_ball//; last exact: ltW. - by rewrite -/mu muE -EFinM lee_fin mulr_natl. - have ixdf : {near \oo, - (fun n => \int[mu]_(t in [set` Interval a (BRight (x + d n))]) (f t)%:E - - \int[mu]_(t in [set` Interval a (BRight x)]) (f t)%:E) =1 - (fun n => - \int[mu]_(y in E x n) (f y)%:E)}. - case: a ax {F}; last first. - move=> [_|//]. - apply: nearW => n. - rewrite -[in LHS]integral_itv_bndo_bndc//=; last first. - by case: locf => + _ _; exact: measurable_funS. - rewrite -/mu -[LHS]oppeK; congr oppe. - rewrite oppeB; last first. - rewrite fin_num_adde_defl// fin_numN//. - by apply: integral_fune_fin_num => //; exact: integrableS intf. - rewrite addeC. - rewrite (_ : `]-oo, x] = `]-oo, (x + d n)%R] `|` E x n)%classic; last first. - apply/seteqP; rewrite /E/=; split => [y|y] /=. - rewrite !in_itv/= => ->; rewrite andbT ltNge. - by apply/orP; rewrite orbN. - rewrite !in_itv/= => -[|/andP[] //]. - by move=> /le_trans; apply; rewrite -lerBrDl subrr ltW//. - rewrite integral_setU_EFin//=. - - rewrite addeAC. - rewrite -[X in X - _]integral_itv_bndo_bndc//; last first. - by case: locf => + _ _; exact: measurable_funS. - rewrite subee ?add0e//. - by apply: integral_fune_fin_num => //; exact: integrableS intf. - - exact: (nice_E _).1. - - by case: locf => + _ _; exact: measurable_funS. - - apply/disj_setPLR => z/=. - rewrite /E /= !in_itv/= leNgt => xdnz. - by apply/negP; rewrite negb_and xdnz. - move=> b a ax. - move/cvgrPdist_le : d0. - move/(_ (x - a)%R); rewrite subr_gt0 => /(_ ax)[m _ /=] h. - near=> n. - have mn : (m <= n)%N by near: n; exists m. - rewrite -[in X in X - _]integral_itv_bndo_bndc//=; last first. - by case: locf => + _ _; exact: measurable_funS. - rewrite -/mu -[LHS]oppeK; congr oppe. - rewrite oppeB; last first. - rewrite fin_num_adde_defl// fin_numN//. - by apply: integral_fune_fin_num => //; exact: integrableS intf. - rewrite addeC. - rewrite (@itv_bndo_setU _ _ (BRight (x - - d n)%R))//; last 2 first. - case: b in ax * => /=; rewrite bnd_simp. - rewrite lerBrDl addrC -lerBrDl. - by have := h _ mn; rewrite sub0r gtr0_norm. - rewrite lerBrDl -lerBrDr. - by have := h _ mn; rewrite sub0r gtr0_norm. - by rewrite opprK bnd_simp -lerBrDl subrr ltW. - rewrite integral_setU_EFin//=. - - rewrite addeAC -[X in X - _]integral_itv_bndo_bndc//; last first. - by case: locf => + _ _; exact: measurable_funS. - rewrite opprK subee ?add0e//. - by apply: integral_fune_fin_num => //; exact: integrableS intf. - - by case: locf => + _ _; exact: measurable_funS. - - apply/disj_setPLR => z/=. - rewrite /E /= !in_itv/= => /andP[az zxdn]. - by apply/negP; rewrite negb_and -leNgt zxdn. - 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. - 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. - have := nice_lebesgue_differentiation nice_E locf fx. - rewrite {ixdf} -/mu. - move/fine_cvgP => [_ /=]. - (* TODO: use eq_cvg *) - set g := _ \o _ => gf. - set h := (f in f n @[n --> \oo] --> _). - suff : g = h by move=> <-. - apply/funext => n. - rewrite/g /h /= fineM//=; last first. - apply: integral_fune_fin_num => //; first exact: (nice_E _).1. - by apply: integrableS intf => //; exact: (nice_E _).1. - by rewrite muE/= invrN mulNr -mulrN. -Unshelve. all: by end_near. Qed. - -Lemma FTC1 (f : R -> R) (a : itv_bound R) : mu.-integrable setT (EFin \o f) -> - let F x := (\int[mu]_(t in [set` Interval a (BRight x)(*closed*)]) (f t))%R in - forall x, (a < BRight x) -> lebesgue_pt f x -> - derivable (F : R^o -> R^o) x 1 /\ - (F : R -> R^o)^`() x = f x. -Proof. -move=> intf F x ax fx; split. - apply/cvg_ex; exists (f x). - set g := (f in f n @[n --> _] --> _). - have := FTC0 intf ax fx. - set h := (f in f n @[n --> _] --> _ -> _). - suff : g = h by move=> <-. - by apply/funext => y; rewrite /g /h [y%:A](mulr1). -by apply/cvg_lim; [exact: Rhausdorff|exact: FTC0]. -Qed. - -End FTC. - -Section FTC1_cont. -Context {R : realType}. -Notation mu := lebesgue_measure. -Local Open Scope ereal_scope. - -Lemma cont_lebesgue_pt (f : R -> R) x : measurable_fun setT f -> - {for x, continuous f} -> lebesgue_pt f x. -Proof. -move=> mf xf. -rewrite /lebesgue_pt. -have fx0 : davg f x 0 = 0 by rewrite davg0. -rewrite -[X in _ --> X]fx0. -apply: cvg_at_right_filter. -rewrite fx0. -apply: (@continuous_cvg_davg _ [set x]) => //; rewrite ?inE//. -move=> y; rewrite inE/= => ->. -exact: xf. -Qed. - -Lemma FTC1_cont (f : R -> R) (a : itv_bound R) : - mu.-integrable setT (EFin \o f) -> - let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in - forall x, (a < BRight x) -> {for x, continuous f} -> - derivable (F : R^o -> R^o) x 1 /\ - (F : R -> R^o)^`() x = f x. -Proof. -move=> fi F x ax fx. -have lfx : lebesgue_pt f x. - apply: cont_lebesgue_pt => //. - case/integrableP : fi => + _. - by move/EFin_measurable_fun. -have lif : locally_integrable setT f. - apply: integrable_locally => //. - exact: openT. -have /= := @FTC1 R f a fi x. -move=> /(_ ax lfx)/= [dfx f'xE]. -by split; [exact: dfx|rewrite f'xE]. -Qed. - -End FTC1_cont. - -Section density. -Context {R : realType}. -Notation mu := lebesgue_measure. -Local Open Scope ereal_scope. - -Lemma density (A : set R) : measurable A -> - {ae mu, forall x, - mu (A `&` ball x r) * (fine (mu (ball x r)))^-1%:E - @[r --> 0^'+] --> (\1_A x)%:E}. -Proof. -move=> mA. -have loc_indic : locally_integrable [set: R] \1_A. - split => //. - - exact: openT. - - move=> K _ cK. - apply: (@le_lt_trans _ _ (\int[mu]_(x in K) (cst 1 x))). - apply: ge0_le_integral => //=. - + exact: compact_measurable. - + by do 2 apply: measurableT_comp => //. - + move=> y _. - by rewrite indicE; case: (_ \in _) => //=; rewrite ?(normr1,normr0). - rewrite integral_cst//= ?mul1e. - exact: compact_finite_measure. - exact: compact_measurable. -have := @lebesgue_differentiation _ (\1_A) loc_indic. -apply: filter_app; first exact: (ae_filter_ringOfSetsType [the measure _ _ of mu]). -apply: aeW => /= x Ax. -apply/(cvge_sub0 _ _).1 => //. -move: Ax; rewrite /lebesgue_pt /davg /= -/mu => Ax. -have : ((fine (mu (ball x r)))^-1)%:E * - `|\int[mu]_(y in ball x r) (\1_A y - \1_A x)%:E | @[r --> 0^'+] --> 0. - apply: (@squeeze_cvge _ _ _ R (cst 0) _ _ _ _ _ Ax) => //; last exact: cvg_cst. - near=> a. - apply/andP; split. - by rewrite mule_ge0// lee_fin invr_ge0// fine_ge0. - rewrite lee_pmul2l//. - (* TODO: le_integral_comp_abse use nneg *) - apply: le_abse_integral => //; first exact: measurable_ball. - by apply/EFin_measurable_fun; exact: measurable_funB. - rewrite lte_fin invr_gt0// fine_gt0//. - have -> : mu (ball x a) < +oo by rewrite lebesgue_measure_ball// ltry. - suff : 0 < mu (ball x a) by move=> ->. - by rewrite lebesgue_measure_ball// lte_fin mulrn_wgt0. -set f := (f in f r @[r --> 0^'+] --> _ -> _). -rewrite (_ : f = fun r => ((fine (mu (ball x r)))^-1)%:E * - `|mu (A `&` ball x r) - (\1_A x)%:E * mu (ball x r)|); last first. - apply/funext => r; rewrite /f integralB_EFin//=; last 3 first. - - exact: measurable_ball. - - apply/integrableP; split. - exact/EFin_measurable_fun/measurable_indic. - under eq_integral do rewrite /= ger0_norm//=. - rewrite integral_indic//=; last exact: measurable_ball. - rewrite -/mu (@le_lt_trans _ _ (mu (ball x r)))// ?le_measure// ?inE. - + by apply: measurableI => //; exact: measurable_ball. - + exact: measurable_ball. - + have [r0|r0] := ltP r 0%R. - by rewrite ((ball0 _ _).2 (ltW r0))// /mu measure0. - by rewrite lebesgue_measure_ball//= ?ltry. - - apply/integrableP; split; first exact/EFin_measurable_fun/measurable_cst. - rewrite /= integral_cst//=; last exact: measurable_ball. - have [r0|r0] := ltP r 0%R. - by rewrite ((ball0 _ _).2 (ltW r0))// /mu measure0 mule0. - by rewrite lebesgue_measure_ball//= ?ltry. - rewrite integral_indic//=; last exact: measurable_ball. - by rewrite -/mu integral_cst//; exact: measurable_ball. -rewrite indicE. -have [xA H|xA] := boolP (x \in A); last first. - apply: iffRL; apply/propeqP; apply: eq_cvg => r. - rewrite -mulNrn mulr0n adde0 mul0e sube0. - by rewrite gee0_abs// muleC. -have {H} /cvgeN : ((fine (mu (ball x r)))^-1)%:E * - (mu (ball x r) - mu (A `&` ball x r)) @[r --> 0^'+] --> 0. - move: H; apply: cvg_trans; apply: near_eq_cvg. - near=> r. - rewrite mul1e lee0_abs. - rewrite oppeB//; last first. - rewrite fin_num_adde_defl// fin_numN ge0_fin_numE//. - by rewrite lebesgue_measure_ball//ltry. - by rewrite addeC. - rewrite sube_le0 le_measure// ?inE/=. - by apply: measurableI => //; exact: measurable_ball. - exact: measurable_ball. -rewrite oppe0; apply: cvg_trans; apply: near_eq_cvg; near=> r. -rewrite -mulNrn mulr1n muleBr//; last first. - rewrite fin_num_adde_defr// ge0_fin_numE//. - by rewrite lebesgue_measure_ball//= ?ltry. -rewrite (_ : ((fine (mu (ball x r)))^-1)%:E * mu (ball x r) = 1); last first. - rewrite -[X in _ * X](@fineK _ (mu (ball x r)))//; last first. - by rewrite lebesgue_measure_ball//= ?ltry. - by rewrite -EFinM mulVf// lebesgue_measure_ball//= gt_eqF// mulrn_wgt0. -by rewrite oppeB// addeC EFinN muleC. -Unshelve. all: by end_near. Qed. - -End density. diff --git a/theories/normedtype.v b/theories/normedtype.v index e0f2f841f4..0cfc954612 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -778,6 +778,13 @@ HB.instance Definition _ := End regular_topology. +Lemma ball_itv {R : realFieldType} (x r : R) : + ball x r = `]x - r, x + r[%classic. +Proof. +rewrite -(@ball_normE _ R^o) /ball_ set_itvE. +by apply/seteqP; split => t/=; rewrite ltr_distlC. +Qed. + Module numFieldNormedType. Section realType. @@ -5036,11 +5043,6 @@ move=> r0; apply/seteqP; split => // y; rewrite /ball/=. by move/lt_le_trans => /(_ _ r0); rewrite normr_lt0. Qed. -Lemma ball_itv (x r : R) : (ball x r = `]x - r, x + r[%classic)%R. -Proof. -by apply/seteqP; split => y; rewrite /ball/= in_itv/= ltr_distlC. -Qed. - End ball_realFieldType. Section Closed_Ball. @@ -5115,6 +5117,16 @@ by move=> r0; apply/seteqP; split => y; rewrite closed_ballE// /closed_ball_ /= in_itv/= ler_distlC. Qed. +Lemma closed_ball_ball {R : realFieldType} (x r : R) : (0 < r)%R -> + closed_ball x r = [set (x - r)%R] `|` ball x r `|` [set (x + r)%R]. +Proof. +move=> r0; rewrite closed_ball_itv// -(@setU1itv _ _ _ (x - r)%R); last first. + by rewrite bnd_simp lerBlDr -addrA lerDl ltW// addr_gt0. +rewrite -(@setUitv1 _ _ _ (x + r)%R); last first. + by rewrite bnd_simp ltrBlDr -addrA ltrDl addr_gt0. +by rewrite ball_itv setUA. +Qed. + Lemma closed_ballR_compact (R : realType) (x e : R) : 0 < e -> compact (closed_ball x e). Proof. diff --git a/theories/numfun.v b/theories/numfun.v index 2bce6cd591..667ba1aedb 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -347,6 +347,21 @@ case: ifPn => [|] xA; first by rewrite in_setI xA andbT. by rewrite in_setI (negbTE xA) andbF. Qed. +Lemma cvg_indic {R : realFieldType} (x : R^o) k : + x \in (ball 0 k : set R^o) -> + \1_(ball 0 k : set R^o) y @[y --> x] --> (\1_(ball 0 k) x : R). +Proof. +move=> xB; apply/(@cvgrPdist_le _ R^o) => /= e e0; near=> t. +rewrite !indicE xB/= mem_set//=; first by rewrite subrr normr0// ltW. +near: t. +rewrite inE /ball /= sub0r normrN in xB. +exists ((k - `|x|)/2) => /=; first by rewrite divr_gt0// subr_gt0. +rewrite /ball_/= => z /= h; rewrite /ball/= sub0r normrN. +rewrite -(subrK x z) (le_lt_trans (ler_normD _ _))//. +rewrite -ltrBrDr distrC (lt_le_trans h)//. +by rewrite ler_pdivrMr//= ler_pMr// ?subr_gt0// ler1n. +Unshelve. all: by end_near. Qed. + Section ring. Context (aT : pointedType) (rT : ringType). diff --git a/theories/reals.v b/theories/reals.v index e58b478835..fc47d77dd3 100644 --- a/theories/reals.v +++ b/theories/reals.v @@ -650,6 +650,13 @@ Lemma ceilN x : ceil (- x) = - floor x. Proof. by rewrite /ceil opprK. Qed. Lemma floorN x : floor (- x) = - ceil x. Proof. by rewrite /ceil opprK. Qed. +Lemma abs_ceil_ge x : `|x| <= `|ceil x|.+1%:R. +Proof. +rewrite -natr1 natr_absz; have [x0|x0] := ltP 0%R x. + by rewrite !gtr0_norm ?ceil_gt0// (le_trans (ceil_ge _))// lerDl. +by rewrite !ler0_norm ?ceil_le0// /ceil opprK; exact/ltW/lt_succ_floor. +Qed. + End CeilTheory. (* -------------------------------------------------------------------- *) diff --git a/theories/topology.v b/theories/topology.v index 0350955b54..c838a60da9 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -2266,6 +2266,13 @@ Proof. by exists N.+1. Qed. Lemma nbhs_infty_ge N : \forall n \near \oo, (N <= n)%N. Proof. by exists N. Qed. +Lemma nbhs_infty_ger {R : realType} (r : R) : + \forall n \near \oo, (r <= n%:R)%R. +Proof. +exists (`|ceil r|)%N => // n /=; rewrite -(ler_nat R); apply: le_trans. +by rewrite (le_trans (ceil_ge _))// natr_absz ler_int ler_norm. +Qed. + Lemma cvg_addnl N : addn N @ \oo --> \oo. Proof. by move=> P [n _ Pn]; exists (n - N)%N => // m; rewrite /= leq_subLR => /Pn. @@ -5355,8 +5362,23 @@ HB.instance Definition _ (R : numFieldType) := PseudoMetric.copy R R^o. Module Exports. HB.reexport. End Exports. End numFieldTopology. + Import numFieldTopology.Exports. +Lemma nbhs0_ltW (R : realFieldType) (x : R) : (0 < x)%R -> + \forall r \near nbhs (0%R:R), (r <= x)%R. +Proof. +exists x => // y; rewrite /ball/= sub0r normrN => /ltW. +by apply: le_trans; rewrite ler_norm. +Qed. + +Lemma nbhs0_lt (R : realType) (x : R) : (0 < x)%R -> + \forall r \near nbhs (0%R:R), (r < x)%R. +Proof. +exists x => // z /=; rewrite sub0r normrN. +by apply: le_lt_trans; rewrite ler_norm. +Qed. + Global Instance Proper_dnbhs_regular_numFieldType (R : numFieldType) (x : R^o) : ProperFilter x^'. Proof. @@ -6237,7 +6259,6 @@ rewrite fVA -setIA setIid eqEsubset; split => x [fVx Ax]; split => //. - by have /[!esym VBOB]-[] : (O `&` B) (f x) by split => //; exact: funS. Qed. - Lemma continuous_subspace0 {U} (f : T -> U) : {within set0, continuous f}. Proof. move=> x Q /=. From 5e8a862d9fda186ede61f7afdb8d879afe691ffc Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 16 Mar 2024 19:49:54 +0900 Subject: [PATCH 3/6] addressing comments --- CHANGELOG_UNRELEASED.md | 8 +- theories/ftc.v | 42 +++++----- theories/lebesgue_integral.v | 154 ++++++++++++++++++----------------- theories/normedtype.v | 8 +- theories/realfun.v | 22 ++--- theories/topology.v | 3 +- 6 files changed, 124 insertions(+), 113 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 5a189a6e48..3161d3df02 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -32,7 +32,7 @@ - in `lebesgue_integral.v` + lemma `locally_integrable_indic` + definition `davg`, - lemmas `davg0`, `davgD`, `continuous_cvg_davg` + lemmas `davg0`, `davg_ge0`, `davgD`, `continuous_cvg_davg` + definition `lim_sup_davg`, lemmas `lim_sup_davg_ge0`, `lim_sup_davg_le`, `continuous_lim_sup_davg`, `lim_sup_davgB`, `lim_sup_davgT_HL_maximal` @@ -46,6 +46,9 @@ + definition `nicely_shrinking`, lemmas `nicely_shrinking_gt0`, `nicely_shrinking_lty`, `nice_lebesgue_differentiation` +- in `normedtype.v`: + + lemma `ball_open_nbhs` + - new file `ftc.v`: - lemmas `FTC1`, `continuous_FTC1` @@ -116,6 +119,9 @@ ### Generalized +- in `realfun.v` + + lemma `lime_sup_le` + ### Deprecated ### Removed diff --git a/theories/ftc.v b/theories/ftc.v index d5ab2dc5e5..c47b035716 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -27,11 +27,10 @@ Notation mu := lebesgue_measure. Local Open Scope ereal_scope. Implicit Types (f : R -> R) (a : itv_bound R). -Let FTC0 f a : - mu.-integrable setT (EFin \o f) -> +Let FTC0 f a : mu.-integrable setT (EFin \o f) -> let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) f t)%R in forall x, a < BRight x -> lebesgue_pt f x -> - h^-1 *: (F (h + x) - F x) @[h --> (0:R)%R^'] --> f x. + h^-1 *: (F (h + x) - F x) @[h --> 0%R^'] --> f x. Proof. move=> intf F x ax fx. have locf : locally_integrable setT f. @@ -180,42 +179,39 @@ apply: cvg_at_right_left_dnbhs. Unshelve. all: by end_near. Qed. (* NB: right-closed interval *) -Lemma FTC1 f a : - mu.-integrable setT (EFin \o f) -> +Lemma FTC1 f a : mu.-integrable setT (EFin \o f) -> let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in forall x, a < BRight x -> lebesgue_pt f x -> - derivable F x 1 /\ - F^`() x = f x. + derivable F x 1 /\ F^`() x = f x. Proof. move=> intf F x ax fx; split; last first. by apply/cvg_lim; [exact: Rhausdorff|exact: FTC0]. apply/cvg_ex; exists (f x). -set g := (f in f n @[n --> _] --> _). -have := FTC0 intf ax fx. -set h := (f in f n @[n --> _] --> _ -> _). +have /= := FTC0 intf ax fx. +set g := (f in f n @[n --> _] --> _ -> _). +set h := (f in _ -> f n @[n --> _] --> _). suff : g = h by move=> <-. -apply/funext => y. -rewrite /g /h /=. -by rewrite [X in F (X + _)](mulr1). +by apply/funext => y;rewrite /g /h /= [X in F (X + _)](mulr1). Qed. -Lemma continuous_FTC1 f a : - mu.-integrable setT (EFin \o f) -> +Corollary continuous_FTC1 f a : mu.-integrable setT (EFin \o f) -> let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in forall x, a < BRight x -> {for x, continuous f} -> - derivable F x 1 /\ - F^`() x = f x. + derivable F x 1 /\ F^`() x = f x. Proof. move=> fi F x ax fx. have lfx : lebesgue_pt f x. - apply: continuous_lebesgue_pt => // U xU. - case/integrableP : fi => + _. - by move/EFin_measurable_fun; exact: measurable_funS. + near (0%R:R)^'+ => e. + apply: (@continuous_lebesgue_pt _ _ _ (ball x e)). + - exact: ball_open_nbhs. + - exact: measurable_ball. + - case/integrableP : fi => + _. + by move/EFin_measurable_fun; exact: measurable_funS. + - exact: fx. have lif : locally_integrable setT f. by apply: integrable_locally => //; exact: openT. -have /= := @FTC1 f a fi x. -move=> /(_ ax lfx)/= [dfx f'xE]. +have /= /(_ ax lfx)/= [dfx f'xE] := @FTC1 f a fi x. by split; [exact: dfx|rewrite f'xE]. -Qed. +Unshelve. all: by end_near. Qed. End FTC. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index b95ab24d72..557fc3e2c4 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -6101,6 +6101,8 @@ Definition davg f x (r : R) := iavg (center (f x) \o f) (ball x r). Lemma davg0 f x (r : R) : (r <= 0)%R -> davg f x r = 0. Proof. by move=> r0; rewrite /davg/= (ball0 _ _).2//= iavg0. Qed. +Lemma davg_ge0 f x (r : R) : 0 <= davg f x r. Proof. exact: iavg_ge0. Qed. + Lemma davgD f g (x r : R) : measurable_fun (ball x r) f -> measurable_fun (ball x r) g -> davg (f \+ g)%R x r <= (davg f x \+ davg g x) r. @@ -6115,64 +6117,57 @@ move=> mf mg; rewrite (le_trans _ (iavgD _ _ _ _)) //. - exact: measurable_funB. Qed. -Let continuous_integralB_fin_num f x : - (forall U, nbhs x U -> measurable_fun U f) -> {for x, continuous f} -> +Section continuous_cvg_davg. +Context f (x : R) (U : set R). +Hypotheses (xU : open_nbhs x U) (mU : measurable U) (mUf : measurable_fun U f) + (fx : {for x, continuous f}). + +Let continuous_integralB_fin_num : \forall t \near 0%R, \int[mu]_(y in ball x t) `|(f y)%:E - (f x)%:E| \is a fin_num. Proof. -move=> mf /cvgrPdist_le fx. +move: fx => /cvgrPdist_le /= fx'. near (0%R:R)^'+ => e. have e0 : (0 < e)%R by near: e; exact: nbhs_right_gt. -have [r /= r0] := fx _ e0 => {}fx. +have [r /= r0 {}fx'] := fx' _ e0. +have [d/= d0 dxU] := open_subball xU.1 xU.2. near=> t; rewrite ge0_fin_numE ?integral_ge0//. -rewrite (@le_lt_trans _ _ (\int[mu]_(y in ball x r) `|f y - f x|%:E))//. - apply: subset_integral => //=. - - exact: measurable_ball. - - exact: measurable_ball. - - do 2 apply: measurableT_comp => //=; apply: measurable_funB => //. - by apply: mf; exact: nbhsx_ballx. - - by apply: le_ball; near: t; exact: nbhs0_ltW. -rewrite (@le_lt_trans _ _ (\int[mu]_(y in ball x r) e%:E))//=. - apply: ge0_le_integral => //=. - - exact: measurable_ball. - - do 2 apply: measurableT_comp => //=; apply: measurable_funB => //. - by apply: mf => /=; exact: nbhsx_ballx. - - by rewrite lee_fin ltW. - - by move=> y xry; rewrite lee_fin distrC; exact: fx. -rewrite integral_cst// ?mul1e /=; last exact: measurable_ball. -by rewrite lebesgue_measure_ball// ?ltry// ltW. +have [t0|t0] := leP t 0%R; first by rewrite ((ball0 _ _).2 t0) integral_set0. +have xtU : ball x t `<=` U by apply: dxU => //=. +rewrite (@le_lt_trans _ _ (\int[mu]_(y in ball x t) e%:E))//; last first. + rewrite integral_cst//=; last exact: measurable_ball. + by rewrite (lebesgue_measure_ball _ (ltW t0)) ltry. +apply: ge0_le_integral => //=; first exact: measurable_ball. +- by do 2 apply: measurableT_comp => //=; apply: measurable_funB; + [exact: measurable_funS mUf|exact: measurable_cst]. +- by move=> y _; rewrite lee_fin. +- move=> y xry; rewrite lee_fin distrC fx'//=; apply: (lt_le_trans xry). + by near: t; exact: nbhs0_ltW. Unshelve. all: by end_near. Qed. -Let continuous_davg_fin_num f x : - (forall U, nbhs x U -> measurable_fun U f) -> {for x, continuous f} -> +Let continuous_davg_fin_num : \forall A \near 0%R, davg f x A \is a fin_num. Proof. -move=> mf fx. -have [e /= e0 exf] := continuous_integralB_fin_num mf fx. -move/cvgrPdist_le in fx. +have [e /= e0 exf] := continuous_integralB_fin_num. +move: fx => /cvgrPdist_le fx'. near (0%R:R)^'+ => r. have r0 : (0 < r)%R by near: r; exact: nbhs_right_gt. -have [d /= d0] := fx _ e0 => {}fx. +have [d /= d0 {}fx'] := fx' _ e0. near=> t; have [t0|t0] := leP t 0%R; first by rewrite davg0. by rewrite fin_numM// exf/=. Unshelve. all: by end_near. Qed. -(* NB: should this be proved without the two Let's above? *) -Lemma continuous_cvg_davg (f : R -> R) x : - (forall U, nbhs x U -> measurable_fun U f) -> {for x, continuous f} -> - davg f x r @[r --> 0%R] --> 0. +Lemma continuous_cvg_davg : davg f x r @[r --> 0%R] --> 0. Proof. -move=> mf cfx; apply/fine_cvgP; split. - exact: continuous_davg_fin_num. +apply/fine_cvgP; split; first exact: continuous_davg_fin_num. apply/cvgrPdist_le => e e0. -have /cvgrPdist_le /= fx := cfx. -have [r /= r0] := fx _ e0 => {}fx. -have [d /= d0 dfx] := continuous_davg_fin_num mf cfx. +move: fx => /cvgrPdist_le /= fx'. +have [r /= r0 {}fx'] := fx' _ e0. +have [d /= d0 dfx] := continuous_davg_fin_num. +have [l/= l0 lxU] := open_subball xU.1 xU.2. near=> t. have [t0|t0] := leP t 0%R; first by rewrite /= davg0//= subrr normr0 ltW. -rewrite sub0r normrN /= ger0_norm; last first. - rewrite fine_ge0// mule_ge0//; last exact: integral_ge0. - by rewrite lee_fin invr_ge0// fine_ge0. +rewrite sub0r normrN /= ger0_norm; last by rewrite fine_ge0// davg_ge0. rewrite -lee_fin fineK//; last by rewrite dfx//= sub0r normrN gtr0_norm. rewrite /davg/= /iavg/= lee_pdivr_mull//; last first. by rewrite fine_gt0// lebesgue_measure_ball// ?ltry ?lte_fin ?mulrn_wgt0 ?ltW. @@ -6180,14 +6175,16 @@ rewrite (@le_trans _ _ (\int[mu]_(y in ball x t) e%:E))//. apply: ge0_le_integral => //=. - exact: measurable_ball. - do 2 apply: measurableT_comp => //=; apply: measurable_funB => //. - by apply: mf => /=; exact: nbhsx_ballx. + by apply: measurable_funS mUf => //; apply: lxU => //=. - by move=> y xty; rewrite lee_fin ltW. - - move=> y xty; rewrite lee_fin distrC fx//. - by apply: (lt_le_trans xty); near: t; exact: nbhs0_ltW. + - move=> y xty; rewrite lee_fin distrC fx'//; apply: (lt_le_trans xty). + by near: t; exact: nbhs0_ltW. rewrite integral_cst//=; last exact: measurable_ball. -by rewrite muleC lebesgue_measure_ball// ?ltry// ltW. +by rewrite muleC fineK// (lebesgue_measure_ball _ (ltW t0)). Unshelve. all: by end_near. Qed. +End continuous_cvg_davg. + End davg. Section lim_sup_davg. @@ -6202,45 +6199,51 @@ Local Notation "f ^*" := (lim_sup_davg f). Lemma lim_sup_davg_ge0 f x : 0 <= f^* x. Proof. by apply: lime_sup_ge0 => y; rewrite /davg iavg_ge0. Qed. -Lemma lim_sup_davg_le f g x : - (forall U, nbhs x U -> measurable_fun U f) -> - (forall U, nbhs x U -> measurable_fun U g) -> +Lemma lim_sup_davg_le f g x (U : set R) : open_nbhs x U -> measurable U -> + measurable_fun U f -> measurable_fun U g -> (f \+ g)%R^* x <= (f^* \+ g^*) x. Proof. -move=> mf /= mg; apply: le_trans (lime_supD _); last first. +move=> xU mY mf /= mg; apply: le_trans (lime_supD _); last first. by rewrite ge0_adde_def// inE; exact: lim_sup_davg_ge0. -apply: lime_sup_le => r r0 y; rewrite neq_lt => /orP[y0|y0 ry]. +have [e/= e0 exU] := open_subball xU.1 xU.2. +apply: lime_sup_le; near=> r => y; rewrite neq_lt => /orP[y0|y0 ry]. by rewrite !davg0 ?adde0// ltW. -by apply: davgD; [apply: mf|apply: mg]; exact: nbhsx_ballx. -Qed. +apply: davgD. + apply: measurable_funS mf => //; apply: exU => //=. + by rewrite (lt_le_trans ry)//; near: r; exact: nbhs_right_le. +apply: measurable_funS mg => //; apply: exU => //=. +by rewrite (lt_le_trans ry)//; near: r; exact: nbhs_right_le. +Unshelve. all: by end_near. Qed. -Lemma continuous_lim_sup_davg f x : - (forall U, nbhs x U -> measurable_fun U f) -> {for x, continuous f} -> +Lemma continuous_lim_sup_davg f x (U : set R) : open_nbhs x U -> measurable U -> + measurable_fun U f -> {for x, continuous f} -> f^* x = 0. -Proof. by move=> mg gx; have /lim_lime_sup := continuous_cvg_davg mg gx. Qed. +Proof. +move=> xU mU mUf ctsf. +by have /lim_lime_sup := continuous_cvg_davg xU mU mUf ctsf. +Qed. -Lemma lim_sup_davgB f g x : - (forall U, nbhs x U -> measurable_fun U f) -> {for x, continuous g} -> - locally_integrable [set: R] g -> - (f \- g)%R^* x = f^* x. +Lemma lim_sup_davgB f g x (U : set R) : open_nbhs x U -> measurable U -> + measurable_fun U f -> {for x, continuous g} -> + locally_integrable [set: R] g -> (f \- g)%R^* x = f^* x. Proof. -move=> mf cg locg; apply/eqP; rewrite eq_le; apply/andP; split. +move=> xU mU mUf cg locg; apply/eqP; rewrite eq_le; apply/andP; split. - rewrite [leRHS](_ : _ = f^* x + (\- g)%R^* x). - apply: lim_sup_davg_le; [exact: mf|move=> U xU]. + apply: (lim_sup_davg_le xU) => //. apply/(measurable_comp measurableT) => //. by case: locg => + _ _; exact: measurable_funS. - rewrite (@continuous_lim_sup_davg (- g)%R); first by rewrite adde0. - - move=> U xU; apply/(measurable_comp measurableT) => //. + rewrite (@continuous_lim_sup_davg (- g)%R _ _ xU mU); first by rewrite adde0. + - apply/(measurable_comp measurableT) => //. by case: locg => + _ _; apply: measurable_funS. + by move=> y; exact/continuousN/cg. - rewrite [leRHS](_ : _ = ((f \- g)%R^* \+ g^*) x)//. rewrite {1}(_ : f = f \- g + g)%R; last by apply/funext => y; rewrite subrK. - apply: lim_sup_davg_le; [move=> U xU|]. - apply: measurable_funB; [exact: mf|]. + apply: (lim_sup_davg_le xU mU). + apply: measurable_funB; [exact: mUf|]. by case: locg => + _ _; exact: measurable_funS. - by move=> U xU; case: locg => + _ _; exact: measurable_funS. - rewrite [X in _ + X](@continuous_lim_sup_davg _ x); [by rewrite adde0| |by[]]. - by move=> U xU; case: locg => + _ _; exact: measurable_funS. + by case: locg => + _ _; exact: measurable_funS. + rewrite [X in _ + X](@continuous_lim_sup_davg _ _ _ xU mU); [by rewrite adde0| |by[]]. + by case: locg => + _ _; exact: measurable_funS. Qed. Local Notation mu := (@lebesgue_measure R). @@ -6300,12 +6303,13 @@ End lim_sup_davg. Definition lebesgue_pt {R : realType} (f : R -> R) (x : R) := davg f x r @[r --> (0%R:R)^'+] --> 0%E. -Lemma continuous_lebesgue_pt {R : realType} (f : R -> R) x : - (forall U, nbhs x U -> measurable_fun U f) -> {for x, continuous f} -> - lebesgue_pt f x. +Lemma continuous_lebesgue_pt {R : realType} (f : R -> R) x (U : set R) : + open_nbhs x U -> measurable U -> measurable_fun U f -> + {for x, continuous f} -> lebesgue_pt f x. Proof. -move=> mf xf; rewrite /lebesgue_pt -[X in _ --> X](@davg0 _ f x 0)//. -by apply: cvg_at_right_filter; rewrite davg0//; exact: continuous_cvg_davg. +move=> xU mU mUf xf; rewrite /lebesgue_pt -[X in _ --> X](@davg0 _ f x 0)//. +apply: cvg_at_right_filter; rewrite davg0//. +exact: (continuous_cvg_davg xU mU mUf). Qed. Section lebesgue_measure_integral. @@ -6496,11 +6500,13 @@ have davgfEe : B k `&` [set x | (f_ k)^* x > e%:E] `<=` Ee. move=> n; rewrite [X in X `<=`_](_ : _ = B k `&` [set x | e%:E < (f_ k \- g_B n)%R^* x]); last first. apply/seteqP; split => [x [Ex] /=|x [Ex] /=]. - rewrite lim_sup_davgB//. - by move=> U xU; move/EFin_measurable_fun : mf; exact: measurable_funS. + rewrite (@lim_sup_davgB _ _ _ _ (B k))//. + by split; [exact: ball_open|exact: Ex]. + by move/EFin_measurable_fun : mf; apply: measurable_funS. by apply: cg_B; rewrite inE. - rewrite lim_sup_davgB//. - by move=> U xU; move/EFin_measurable_fun : mf; exact: measurable_funS. + rewrite (@lim_sup_davgB _ _ _ _ (B k))//. + by split; [exact: ball_open|exact: Ex]. + by move/EFin_measurable_fun : mf; apply: measurable_funS. by apply: cg_B; rewrite inE. move=> r /= [Er] efgnr; split => //. have {}efgnr := lt_le_trans efgnr (lim_sup_davgT_HL_maximal r (locf_g_B n)). diff --git a/theories/normedtype.v b/theories/normedtype.v index 0cfc954612..672fb34521 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -5045,8 +5045,6 @@ Qed. End ball_realFieldType. -Section Closed_Ball. - Lemma ball_open (R : numDomainType) (V : normedModType R) (x : V) (r : R) : 0 < r -> open (ball x r). Proof. @@ -5055,6 +5053,12 @@ rewrite /= (le_lt_trans (ler_distD y _ _)) // addrC -ltrBrDr. by near: z; apply: cvgr_dist_lt; rewrite // subr_gt0. Unshelve. all: by end_near. Qed. +Lemma ball_open_nbhs (R : numDomainType) (V : normedModType R) (x : V) (r : R) : + 0 < r -> open_nbhs x (ball x r). +Proof. by move=> e0; split; [exact: ball_open|exact: ballxx]. Qed. + +Section Closed_Ball. + Definition closed_ball_ (R : numDomainType) (V : zmodType) (norm : V -> R) (x : V) (e : R) := [set y | norm (x - y) <= e]. diff --git a/theories/realfun.v b/theories/realfun.v index 48b2bd8a7a..bdbeaab4ad 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -704,11 +704,13 @@ by move=> x y; rewrite !in_itv/= => /andP[x0 xe] /andP[y0 ye] /inf_ball_le. Unshelve. all: by end_near. Qed. Let le_sup_ball f g a : - (forall r, (0 < r)%R -> forall y : R, y != a -> ball a r y -> f y <= g y) -> + (\forall r \near 0^'+, forall y : R, y != a -> ball a r y -> f y <= g y) -> \forall r \near 0^'+, sup_ball f a r <= sup_ball g a r. Proof. -move=> fg; near=> r; apply: ub_ereal_sup => /= _ [s [pas /= /eqP ps]] <-. -apply: (@le_trans _ _ (g s)); first exact: (fg r). +move=> [e/= e0 fg]. +near=> r; apply: ub_ereal_sup => /= _ [s [pas /= /eqP ps]] <-. +rewrite (@le_trans _ _ (g s))//. + by rewrite (fg r)//= sub0r normrN gtr0_norm. by apply: ereal_sup_ub => /=; exists s => //; split => //; exact/eqP. Unshelve. all: by end_near. Qed. @@ -779,7 +781,7 @@ apply: lee_lim => //. Unshelve. all: by end_near. Qed. Lemma lime_sup_le f g a : - (forall r, (0 < r)%R -> forall y, y != a -> ball a r y -> f y <= g y) -> + (\forall r \near 0^'+, forall y, y != a -> ball a r y -> f y <= g y) -> lime_sup f a <= lime_sup g a. Proof. by move=> fg; rewrite !lime_sup_lim; apply: lee_lim => //; exact: le_sup_ball. @@ -788,17 +790,16 @@ Qed. Lemma lime_inf_sup f a : lime_inf f a <= lime_sup f a. Proof. rewrite lime_inf_lim lime_sup_lim; apply: lee_lim => //. -near=> r. -rewrite ereal_sup_le//. +near=> r; rewrite ereal_sup_le//. have ? : exists2 x, ball a r x /\ x <> a & f x = f (a + r / 2)%R. - exists (a + r / 2)%R => //; split. + exists (a + r / 2)%R => //; split. rewrite /ball/= opprD addrA subrr sub0r normrN gtr0_norm ?divr_gt0//. by rewrite ltr_pdivrMr// ltr_pMr// ltr1n. by apply/eqP; rewrite gt_eqF// ltr_pwDr// divr_gt0. -by exists (f (a + r / 2)%R) => //=; rewrite inf_ballE ereal_inf_lb. +by exists (f (a + r / 2)) => //=; rewrite inf_ballE ereal_inf_lb. Unshelve. all: by end_near. Qed. -Local Lemma lim_lime_sup' f a (l : R) : +Local Lemma lim_lime_sup' f a l : f r @[r --> a] --> l%:E -> lime_sup f a <= l%:E. Proof. move=> fpA; apply/lee_addgt0Pr => e e0; rewrite lime_sup_lim. @@ -806,8 +807,7 @@ apply: lime_le => //. move/fine_cvg : (fpA) => /cvgrPdist_le fpA1. move/fcvg_is_fine : (fpA); rewrite near_map => -[d d0] fpA2. have := fpA1 _ e0 => -[q /= q0] H. -near=> x. -apply: ub_ereal_sup => //= _ [y [pry /= yp <-]]. +near=> x; apply: ub_ereal_sup => //= _ [y [pry /= yp <-]]. have ? : f y \is a fin_num. apply: fpA2. rewrite /ball_ /= (lt_le_trans pry)//. diff --git a/theories/topology.v b/theories/topology.v index c838a60da9..691d1089b2 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -42,7 +42,7 @@ Require Import reals signed. (* ## Structure of filter *) (* ``` *) (* filteredType U == interface type for types whose *) -(* elements represent sets of sets on U. *) +(* elements represent sets of sets on U *) (* These sets are intended to be filters *) (* on U but this is not enforced yet. *) (* The HB class is called Filtered. *) @@ -4646,7 +4646,6 @@ Qed. End sup_uniform. - (** PseudoMetric spaces defined using balls *) Definition entourage_ {R : numDomainType} {T T'} (ball : T -> R -> set T') := From 80a1417d96b843ec5f7396bb6294da48da9d9830 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 18 Mar 2024 13:42:22 +0900 Subject: [PATCH 4/6] fix for CI? --- theories/lebesgue_integral.v | 6 +++--- theories/lebesgue_measure.v | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 557fc3e2c4..7d36e851f3 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -5839,12 +5839,12 @@ Qed. Lemma locally_integrable_indic D (A : set R) : open D -> measurable A -> locally_integrable D \1_A. Proof. -move=> oU; split => // K _ cK. +move=> oU mA; split => // K KD_ cK. apply: (@le_lt_trans _ _ (\int[mu]_(x in K) cst 1 x)). apply: ge0_le_integral => //=; first exact: compact_measurable. - by do 2 apply: measurableT_comp => //. - - move=> y _. - by rewrite indicE; case: (y \in A) => /=; rewrite ?(normr1,normr0). + - move=> y Kx; rewrite indicE. + by case: (y \in A) => /=; rewrite ?(normr1,normr0,lexx,lee01). by rewrite integral_cst//= ?mul1e; [exact: compact_finite_measure| exact: compact_measurable]. Qed. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index f729b40989..56d284ee5f 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1875,8 +1875,8 @@ Lemma lebesgue_regularity_outer (D : set R) (eps : R) : measurable D -> mu D < +oo -> (0 < eps)%R -> exists U : set R, [/\ open U , D `<=` U & mu (U `\` D) < eps%:E]. Proof. -move=> mD muDpos epspos. -have /ereal_inf_lt[z [M' covDM sMz zDe]] : mu D < mu D + (eps / 2)%:E. +move=> mD muDoo epspos. +have /ereal_inf_lt[z [/= M' covDM sMz zDe]] : mu D < mu D + (eps / 2)%:E. by rewrite lte_spaddre ?lte_fin ?divr_gt0// ge0_fin_numE. pose e2 n := (eps / 2) / (2 ^ n.+1)%:R. have e2pos n : (0 < e2 n)%R by rewrite ?divr_gt0. @@ -2134,7 +2134,7 @@ Lemma ae_pointwise_almost_uniform measurable A -> mu A < +oo -> {ae mu, (forall x, A x -> f_ ^~ x @\oo --> g x)} -> (0 < eps)%R -> exists B, [/\ measurable B, mu B < eps%:E & - {uniform A `\` B, f_ @\oo --> g}]. + {uniform A `\` B, f_ @ \oo --> g}]. Proof. move=> mf mg mA Afin [C [mC C0 nC] epspos]. have [B [mB Beps Bunif]] : exists B, [/\ d.-measurable B, mu B < eps%:E & From f014fa1b9ca5e35e664a332b543a9b429ef05092 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 18 Mar 2024 15:45:44 +0900 Subject: [PATCH 5/6] CI fix? --- theories/lebesgue_integral.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 7d36e851f3..d5a54c670e 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -6683,7 +6683,7 @@ rewrite (_ : f = fun r => (fine (mu (ball x r)))^-1%:E * rewrite integral_indic//=; last exact: measurable_ball. by rewrite -/mu integral_cst//; exact: measurable_ball. rewrite indicE; have [xA xrA0|xA] := boolP (x \in A); last first. - apply: iffRL; apply/propeqP; apply: eq_cvg => r. + apply: iffRL; apply/propeqP; apply eq_cvg => r. by rewrite -mulNrn mulr0n adde0 mul0e sube0 gee0_abs// muleC. have {xrA0} /cvgeN : (fine (mu (ball x r)))^-1%:E * (mu (ball x r) - mu (A `&` ball x r)) @[r --> 0^'+] --> 0. From a149aa3fcaa2c3a1676833458fddbf1fe9dbfb1b Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 18 Mar 2024 18:56:18 +0900 Subject: [PATCH 6/6] fix CI --- theories/lebesgue_integral.v | 6 +++--- theories/normedtype.v | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index d5a54c670e..bba35b5d78 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -6648,7 +6648,7 @@ Proof. move=> mA; have := lebesgue_differentiation (locally_integrable_indic openT mA). apply: filter_app; first exact: (ae_filter_ringOfSetsType mu). apply: aeW => /= x Ax. -apply/(cvge_sub0 _ _).1 => //. +apply: (cvge_sub0 _ _).1 => //. move: Ax; rewrite /lebesgue_pt /davg /= -/mu => Ax. have : (fine (mu (ball x r)))^-1%:E * `|\int[mu]_(y in ball x r) (\1_A y - \1_A x)%:E | @[r --> 0^'+] --> 0. @@ -6683,7 +6683,7 @@ rewrite (_ : f = fun r => (fine (mu (ball x r)))^-1%:E * rewrite integral_indic//=; last exact: measurable_ball. by rewrite -/mu integral_cst//; exact: measurable_ball. rewrite indicE; have [xA xrA0|xA] := boolP (x \in A); last first. - apply: iffRL; apply/propeqP; apply eq_cvg => r. + apply: iffRL; apply/propeqP; apply: eq_cvg => r. by rewrite -mulNrn mulr0n adde0 mul0e sube0 gee0_abs// muleC. have {xrA0} /cvgeN : (fine (mu (ball x r)))^-1%:E * (mu (ball x r) - mu (A `&` ball x r)) @[r --> 0^'+] --> 0. @@ -6751,7 +6751,7 @@ Lemma nice_lebesgue_differentiation (f : R -> R) : (fine (mu (E x n)))^-1%:E * \int[mu]_(y in E x n) (f y)%:E @[n --> \oo] --> (f x)%:E. Proof. -move=> locf x fx; apply/(cvge_sub0 _ _).1 => //=; apply/cvg_abse0P. +move=> locf x fx; apply: (cvge_sub0 _ _).1 => //=; apply/cvg_abse0P. pose r_ x : {posnum R} ^nat := (sval (cid (hE x).2)).2. pose C := (sval (cid (hE x).2)).1. have C_gt0 : (0 < C)%R by rewrite /C /sval/=; case: cid => -[? ?] []. diff --git a/theories/normedtype.v b/theories/normedtype.v index 672fb34521..1f18d0b777 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -3473,7 +3473,7 @@ Lemma uniform_separatorW {T : uniformType} (A B : set T) : Proof. by case=> E entE AB0; exists (Uniform.class T), E; split => // ?. Qed. Section Urysohn. -Context {T : topologicalType} . +Context {T : topologicalType}. Hypothesis normalT : normal_space T. Section normal_uniform_separators. Context (A : set T).