From e418417a57a41615e2cb7533b896b77936f732d3 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 22 Jun 2023 22:08:45 +0900 Subject: [PATCH] maximal inequality --- CHANGELOG_UNRELEASED.md | 24 +++ theories/charge.v | 40 +++-- theories/ereal.v | 16 +- theories/lebesgue_integral.v | 321 ++++++++++++++++++++++++++++++++--- theories/lebesgue_measure.v | 14 +- theories/normedtype.v | 26 +++ theories/numfun.v | 7 + 7 files changed, 398 insertions(+), 50 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 782b9aac7..e1259f514 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -29,6 +29,27 @@ `nondecreasing_cvge`, `nondecreasing_is_cvge`, `nondecreasing_at_right_cvge`, `nondecreasing_at_right_is_cvge`, `nonincreasing_at_right_cvge`, `nonincreasing_at_right_is_cvge` +- in `ereal.v`: + + lemmas `ereal_sup_le`, `ereal_inf_le` + +- in `normedtype.v`: + + definition `lower_semicontinuous` + + lemma `lower_semicontinuousP` + +- in `numfun.v`: + + lemma `patch_indic` + +- in `lebesgue_measure.v` + + lemma `lower_semicontinuous_measurable` + +- in `lebesgue_integral.v`: + + definition `locally_integrable` + + lemmas `integrable_locally`, `locally_integrableN`, `locally_integrableD`, + `locally_integrableB` + + definitions `HL_max`, `HL_maximal` + + lemmas `HL_max_ge0`, `HL_maximal_ge0`, `HL_maximalT_ge0`, + `lower_semicontinuous_HL_maximal`, `measurable_HL_maximal`, + `maximal_inequality` ### Changed @@ -39,6 +60,9 @@ ### Generalized +- in `lebesgue_integral.v` + + `ge0_integral_bigsetU` generalized from `nat` to `eqType` + ### Deprecated ### Removed diff --git a/theories/charge.v b/theories/charge.v index f1cebbc9f..1fd90eb7b 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -1136,17 +1136,19 @@ Let E m j := is_max_approxRN mu nu m j. Let int_F_nu m A (mA : measurable A) : \int[mu]_(x in A) F m x <= nu A. Proof. -rewrite [leLHS](_ : _ = \sum_(j < m.+1) \int[mu]_(x in (A `&` E m j)) F m x); - last first. +rewrite [leLHS](_ : _ = + \sum_(j < m.+1) \int[mu]_(x in (A `&` E m j)) F m x); last first. rewrite -[in LHS](setIT A) -(bigsetU_is_max_approxRN mu nu m) big_distrr/=. - rewrite (@ge0_integral_bigsetU _ _ _ _ (fun n => A `&` E m n))//. + rewrite -(@big_mkord _ _ _ m.+1 xpredT (fun i => A `&` is_max_approxRN mu nu m i)). + rewrite ge0_integral_bigsetU ?big_mkord//. - by move=> n; apply: measurableI => //; exact: measurable_is_max_approxRN. - - by apply: measurable_funTS => //; exact: measurable_max_approxRN_seq. - - by move=> ? ?; exact: max_approxRN_seq_ge0. + - exact: iota_uniq. - apply: trivIset_setIl; apply: (@sub_trivIset _ _ _ setT (E m)) => //. exact: trivIset_is_max_approxRN. -rewrite [leLHS](_ : _ = \sum_(j < m.+1) (\int[mu]_(x in (A `&` (E m j))) g j x)); - last first. + - by apply: measurable_funTS => //; exact: measurable_max_approxRN_seq. + - by move=> ? ?; exact: max_approxRN_seq_ge0. +rewrite [leLHS](_ : _ = + \sum_(j < m.+1) (\int[mu]_(x in (A `&` (E m j))) g j x)); last first. apply: eq_bigr => i _; apply:eq_integral => x; rewrite inE => -[?] [] Fmgi h. by apply/eqP; rewrite eq_le; rewrite /F Fmgi lexx. rewrite [leRHS](_ : _ = \sum_(j < m.+1) (nu (A `&` E m j))); last first. @@ -1582,16 +1584,15 @@ End radon_nikodym. Notation "'d nu '/d mu" := (Radon_Nikodym mu nu) : charge_scope. Section radon_nikodym_lemmas. +Context d (T : measurableType d) (R : realType). -Lemma dominates_cscale d (T : measurableType d) (R : realType) - (mu : {sigma_finite_measure set T -> \bar R}) - (nu : {charge set T -> \bar R}) - (c : R) : nu `<< mu -> cscale c nu `<< mu. +Lemma dominates_cscale (mu : {sigma_finite_measure set T -> \bar R}) + (nu : {charge set T -> \bar R}) (c : R) : + nu `<< mu -> cscale c nu `<< mu. Proof. by move=> numu E mE /numu; rewrite /cscale => ->//; rewrite mule0. Qed. -Lemma Radon_Nikodym_cscale d (T : measurableType d) (R : realType) - (mu : {sigma_finite_measure set T -> \bar R}) - (nu : {charge set T -> \bar R}) (c : R) : +Lemma Radon_Nikodym_cscale (mu : {sigma_finite_measure set T -> \bar R}) + (nu : {charge set T -> \bar R}) (c : R) : nu `<< mu -> ae_eq mu [set: T] ('d [the charge _ _ of cscale c nu] '/d mu) (fun x => c%:E * 'd nu '/d mu x). @@ -1606,17 +1607,14 @@ move=> numu; apply: integral_ae_eq => [//| | |E mE]. by rewrite -Radon_Nikodym_integral. Qed. -Lemma dominates_caddl d (T : measurableType d) - (R : realType) (mu : {sigma_finite_measure set T -> \bar R}) - (nu0 nu1 : {charge set T -> \bar R}) : - nu0 `<< mu -> nu1 `<< mu -> - cadd nu0 nu1 `<< mu. +Lemma dominates_caddl (mu : {sigma_finite_measure set T -> \bar R}) + (nu0 nu1 : {charge set T -> \bar R}) : + nu0 `<< mu -> nu1 `<< mu -> cadd nu0 nu1 `<< mu. Proof. by move=> nu0mu nu1mu A mA A0; rewrite /cadd nu0mu// nu1mu// adde0. Qed. -Lemma Radon_Nikodym_cadd d (T : measurableType d) (R : realType) - (mu : {sigma_finite_measure set T -> \bar R}) +Lemma Radon_Nikodym_cadd (mu : {sigma_finite_measure set T -> \bar R}) (nu0 nu1 : {charge set T -> \bar R}) : nu0 `<< mu -> nu1 `<< mu -> ae_eq mu [set: T] ('d [the charge _ _ of cadd nu0 nu1] '/d mu) diff --git a/theories/ereal.v b/theories/ereal.v index a249452e7..ec5b8b10d 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -506,6 +506,12 @@ case: xgetP => /=; first by move=> _ -> -[] /ubP geS _; apply geS. by case: (ereal_supremums_neq0 S) => /= x0 Sx0; move/(_ x0). Qed. +Lemma ereal_sup_le S x : S !=set0 -> + (forall y, S y -> x <= y) -> x <= ereal_sup S. +Proof. +by case=> y Sy Sx; rewrite (@le_trans _ _ y)//; [exact:Sx|exact:ereal_sup_ub]. +Qed. + Lemma ereal_sup_ninfty S : ereal_sup S = -oo <-> S `<=` [set -oo]. Proof. split. @@ -518,14 +524,20 @@ Proof. by move=> x Sx; rewrite /ereal_inf lee_oppl; apply ereal_sup_ub; exists x. Qed. +Lemma ereal_inf_le S x : S !=set0 -> (forall y, S y -> y <= x) -> + ereal_inf S <= x. +Proof. +by case=> y Sy Sx; rewrite (@le_trans _ _ y)//; [exact:ereal_inf_lb|exact:Sx]. +Qed. + Lemma ereal_inf_pinfty S : ereal_inf S = +oo <-> S `<=` [set +oo]. Proof. rewrite eqe_oppLRP oppe_subset image_set1; exact: ereal_sup_ninfty. Qed. Lemma le_ereal_sup : {homo @ereal_sup R : A B / A `<=` B >-> A <= B}. -Proof. by move=> A B AB; apply ub_ereal_sup => x Ax; apply/ereal_sup_ub/AB. Qed. +Proof. by move=> A B AB; apply: ub_ereal_sup => x Ax; apply/ereal_sup_ub/AB. Qed. Lemma le_ereal_inf : {homo @ereal_inf R : A B / A `<=` B >-> B <= A}. -Proof. by move=> A B AB; apply lb_ereal_inf => x Bx; exact/ereal_inf_lb/AB. Qed. +Proof. by move=> A B AB; apply: lb_ereal_inf => x Bx; exact/ereal_inf_lb/AB. Qed. Lemma hasNub_ereal_sup (A : set (\bar R)) : ~ has_ubound A -> A !=set0 -> ereal_sup A = +oo%E. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 2fd860001..e454fbe4b 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -45,6 +45,11 @@ Require Import esum measure lebesgue_measure numfun. (* m1 \x^ m2 == product measure over T1 * T2, m2 is a measure *) (* measure over T1, and m1 is a sigma finite *) (* measure over T2 *) +(* locally_integrable D f == the real number-valued function f is locally *) +(* integrable on D *) +(* HL_maximal == the Hardy–Littlewood maximal operator *) +(* input: real number-valued function *) +(* output: extended real number-valued function *) (* *) (******************************************************************************) @@ -2804,28 +2809,30 @@ rewrite integral_mkcond integral0_eq// => x _. by rewrite /restrict; case: ifPn => //; rewrite in_set0. Qed. -Lemma ge0_integral_bigsetU (F : (set T)^nat) (f : T -> \bar R) n : - (forall n, measurable (F n)) -> - let D := \big[setU/set0]_(i < n) F i in +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 -> + let D := \big[setU/set0]_(i <- s) F i in measurable_fun D f -> (forall x, D x -> 0 <= f x) -> - trivIset `I_n F -> - \int[mu]_(x in D) f x = \sum_(i < n) \int[mu]_(x in F i) f x. -Proof. -move=> mF. -elim: n => [|n ih] D mf f0 tF; first by rewrite /D 2!big_ord0 integral_set0. -rewrite /D big_ord_recr/= integral_setU//; last 4 first. - - exact: bigsetU_measurable. - - by move: mf; rewrite /D big_ord_recr. - - by move: f0; rewrite /D big_ord_recr. - - apply/eqP; move: (trivIset_bigsetUI tF (ltnSn n) (leqnn n)). - rewrite [in X in X -> _](eq_bigl xpredT)// => i. - by rewrite (leq_trans (ltn_ord i)). -rewrite ih ?big_ord_recr//. -- apply: measurable_funS mf => //; first exact: bigsetU_measurable. - by rewrite /D big_ord_recr /=; apply: subsetUl. -- by move=> t Dt; apply: f0; rewrite /D big_ord_recr/=; left. -- by apply: sub_trivIset tF => x; exact: leq_trans. + \int[mu]_(x in D) f x = \sum_(i <- s) \int[mu]_(x in F i) f x. +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 big_cons ih//. + + by move: us => /= /andP[]. + + by apply: sub_trivIset tF => /= i /= it; rewrite inE it orbT. + + apply: measurable_funS mf => //; first exact: bigsetU_measurable. + by rewrite /D big_cons; exact: subsetUr. + + by move=> x UFx; apply: f0; rewrite /D big_cons; right. +- exact: bigsetU_measurable. +- by move: mf; rewrite /D big_cons. +- by move: f0; rewrite /D big_cons. +- apply/eqP; rewrite big_distrr/= big_seq big1// => i it. + move/trivIsetP : tF; apply => //=; rewrite ?mem_head//. + + by rewrite inE it orbT. + + by apply/eqP => hi; move: us => /=; rewrite hi it. Qed. Lemma le_integral_abse (D : set T) (mD : measurable D) (g : T -> \bar R) a : @@ -3139,11 +3146,13 @@ rewrite monotone_convergence//; last 3 first. transitivity (lim (fun N => \int[mu]_(x in \big[setU/set0]_(i < N) F i) f x)). congr (lim _); rewrite funeqE => n. by rewrite /f_ [in RHS]integral_mkcond big_mkord. -congr (lim _); rewrite funeqE => /= n; rewrite ge0_integral_bigsetU ?big_mkord//. +congr (lim _); rewrite funeqE => /= n. +rewrite -(big_mkord xpredT) ge0_integral_bigsetU ?big_mkord//. +- exact: iota_uniq. +- exact: sub_trivIset tF. - case: fi => + _; apply: measurable_funS => //; first exact: bigcup_measurable. exact: bigsetU_bigcup. - by move=> y Dy; apply: f0; exact: bigsetU_bigcup Dy. -- exact: sub_trivIset tF. Qed. Lemma integrableS (E D : set T) (f : T -> \bar R) : @@ -3318,14 +3327,14 @@ suff: \int[mu]_(x in D) ((g1 \+ g2)^\+ x) + \int[mu]_(x in D) (g1^\- x) + \int[mu]_(x in D) (g1^\- x) + \int[mu]_(x in D) (g2^\- x) \is a fin_num. rewrite ge0_fin_numE//. by rewrite lte_add_pinfty// ; exact: integral_funeneg_lt_pinfty. - by apply: adde_ge0; exact: integral_ge0. + by rewrite adde_ge0// integral_ge0. rewrite -sube_eq; last 2 first. - rewrite ge0_fin_numE. apply: lte_add_pinfty; last exact: integral_funeneg_lt_pinfty. apply: lte_add_pinfty; last exact: integral_funeneg_lt_pinfty. exact: integral_funepos_lt_pinfty (integrableD _ _ _). rewrite adde_ge0//; last exact: integral_ge0. - by apply: adde_ge0; exact: integral_ge0. + by rewrite adde_ge0// integral_ge0. - by rewrite fin_num_adde_defr. rewrite -(addeA (\int[mu]_(x in D) (g1 \+ g2)^\+ x)). rewrite (addeC (\int[mu]_(x in D) (g1 \+ g2)^\+ x)). @@ -5651,3 +5660,267 @@ by rewrite ritv //= -EFinM lee_fin mulrC. Unshelve. all: by end_near. Qed. End lebesgue_differentiation_continuous. + +Section locally_integrable. +Context {R : realType}. +Implicit Types (D : set R) (f g : R -> R). +Local Open Scope ereal_scope. + +Definition locally_integrable D f := [/\ + measurable_fun D f, open D & + forall K, K `<=` D -> compact K -> + \int[lebesgue_measure]_(x in K) `|f x|%:E < +oo]. + +Lemma integrable_locally D f : let mu := @lebesgue_measure R in open D -> + mu.-integrable D (EFin \o f) -> locally_integrable D f. +Proof. +move=> mu oD /integrableP[mf foo]; split => //; first exact/EFin_measurable_fun. +- move=> K KD cK; rewrite (le_lt_trans _ foo)// subset_integral//. + + exact: compact_measurable. + + exact: open_measurable. + + apply/EFin_measurable_fun; apply: measurableT_comp => //. + exact/EFin_measurable_fun. +Qed. + +Lemma locally_integrableN D f : + locally_integrable D f -> locally_integrable D (\- f)%R. +Proof. +move=> [mf oD foo]; split => //; first exact: measurableT_comp. +by move=> K KD cK; under eq_integral do rewrite normrN; exact: foo. +Qed. + +Lemma locally_integrableD D f g : + locally_integrable D f -> locally_integrable D g -> + locally_integrable D (f \+ g)%R. +Proof. +move=> [mf oD foo] [mg _ goo]; split => //; first exact: measurable_funD. +move=> K KD cK. +suff : lebesgue_measure.-integrable K ((EFin \o f) \+ (EFin \o g)). + by move/integrableP => [_]. +apply: integrableD => //=; first exact: compact_measurable. +- apply/integrableP; split; last exact: foo. + apply/EFin_measurable_fun; apply: measurable_funS mf => //. + exact: open_measurable. +- apply/integrableP; split; last exact: goo. + apply/EFin_measurable_fun; apply: measurable_funS mg => //. + exact: open_measurable. +Qed. + +Lemma locally_integrableB D f g : + locally_integrable D f -> locally_integrable D g -> + locally_integrable D (f \- g)%R. +Proof. +by move=> lf lg; apply: locally_integrableD => //; exact: locally_integrableN. +Qed. + +End locally_integrable. + +Section hardy_littlewood. +Context {R : realType}. +Notation mu := (@lebesgue_measure R). +Implicit Types f : R -> R. +Local Open Scope ereal_scope. + +Definition HL_max f (x r : R) : \bar R := + (fine (mu (ball x r)))^-1%:E * \int[mu]_(y in ball x r) `| (f y)%:E|. + +Lemma HL_max_ge0 f (x r : R) : 0 <= HL_max f x r. +Proof. +rewrite /HL_max mule_ge0//; last exact: integral_ge0. +by rewrite lee_fin invr_ge0// fine_ge0. +Qed. + +Definition HL_maximal f (x : R) : \bar R := + ereal_sup [set HL_max f x r | r in `]0, +oo[%classic%R]. + +Notation HL := HL_maximal. + +Lemma HL_maximal_ge0 f (D : set R) : + locally_integrable D f -> forall x, 0 <= HL (f \_ D) x. +Proof. +move=> Df x; apply: ereal_sup_le => //=; last first. + by move=> y [r]; rewrite in_itv/= andbT => r0 <-{y}; exact: HL_max_ge0. +pose k := \int[mu]_(x in D `&` ball x 1) `|f x|%:E. +exists ((fine (mu (ball x 1)))^-1%:E * k) => /=; exists 1%R => //. + by rewrite in_itv/= ltr01. +rewrite /HL_max /k setIC integral_setI_indic/=. +- congr *%E; apply: eq_integral => /= y yx1. + by rewrite patch_indic/= normrM EFinM; congr *%E; rewrite ger0_norm. +- by apply: open_measurable; case: Df. +- exact: measurable_ball. +Qed. + +Lemma HL_maximalT_ge0 f : locally_integrable setT f -> forall x, 0 <= HL f x. +Proof. by move=> + x => /HL_maximal_ge0 /(_ x); rewrite patch_setT. Qed. + +Lemma lower_semicontinuous_HL_maximal f : + locally_integrable setT f -> lower_semicontinuous (HL f). +Proof. +move=> [mf ? locf]; apply/lower_semicontinuousP => a. +have [a0|a0] := lerP 0 a; last first. + rewrite [X in open X](_ : _ = setT); first exact: openT. + apply/seteqP; split => // x _ /=. + by rewrite (lt_le_trans _ (HL_maximalT_ge0 _ _)). +rewrite openE /= => x /= /ereal_sup_gt[_ [r r0] <-] afxr. +rewrite /= in_itv /= andbT in r0. +rewrite /HL_max in afxr; set k := integral _ _ _ in afxr. +apply: nbhs_singleton; apply: nbhs_interior; rewrite nbhsE /=. +have k_lty : k < +oo. + rewrite (le_lt_trans _ (locf (closed_ball x r) _ (closed_ballR_compact _)))//. + apply: subset_integral => //; first exact: measurable_ball. + - by apply: measurable_closed_ball; exact/ltW. + - apply: measurable_funTS; apply/measurableT_comp => //=. + exact: measurableT_comp. + - exact: subset_closed_ball. +have k_fin_num : k \is a fin_num by rewrite ge0_fin_numE//= integral_ge0. +have k_gt0 : 0 < k. + rewrite lt0e integral_ge0// andbT; apply/negP => /eqP k0. + by move: afxr; rewrite k0 mule0 lte_fin ltNge a0. +move: a0; rewrite le_eqVlt => /predU1P[a0|a0]. + move: afxr; rewrite -{a}a0 => xrk. + near (0%R : R)^'+ => d. + have d0 : (0 < d)%R by near: d; exact: nbhs_right_gt. + have xrdk : 0 < (fine (mu (ball x (r + d))))^-1%:E * k. + rewrite mule_gt0// lte_fin invr_gt0// fine_gt0//. + rewrite lebesgue_measure_ball; last by rewrite addr_ge0// ltW. + by rewrite ltry andbT lte_fin pmulrn_lgt0// addr_gt0. + exists (ball x d). + by split; [exact: (@ball_open _ [normedModType R of R^o])|exact: ballxx]. + move=> y; rewrite /ball/= => xyd. + have ? : ball x r `<=` ball y (r + d). + move=> /= z; rewrite /ball/= => xzr; rewrite -(subrK x y) -(addrA (y - x)%R). + by rewrite (le_lt_trans (ler_norm_add _ _))// addrC ltr_add// distrC. + have ? : k <= \int[mu]_(y in ball y (r + d)) `|(f y)%:E|. + apply: subset_integral =>//; [exact:measurable_ball|exact:measurable_ball|]. + apply: measurable_funTS; apply: measurableT_comp => //=. + by apply/measurableT_comp => //=; case: locf. + have : HL_max f y (r + d) <= HL f y. + apply: ereal_sup_ub => /=; exists (r + d)%R => //. + by rewrite in_itv/= andbT addr_gt0. + apply/lt_le_trans/(lt_le_trans xrdk). + rewrite lebesgue_measure_ball; last by rewrite addr_ge0// ltW. + rewrite /HL_max lebesgue_measure_ball; last by rewrite addr_ge0// ltW. + rewrite lee_wpmul2l// lee_fin invr_ge0// fine_ge0// lee_fin pmulrn_rge0//. + by rewrite addr_gt0. +have ? : fine k / a \is Num.pos by rewrite posrE divr_gt0// fine_gt0 // k_gt0. +have kar : (0 < 2^-1 * (fine k / a) - r)%R. + move: afxr; rewrite -{1}(fineK k_fin_num) -lte_pdivr_mulr; last first. + by rewrite fine_gt0// k_gt0/= ltey_eq k_fin_num. + rewrite lebesgue_measure_ball//; last exact: ltW. + rewrite -!EFinM !lte_fin -invf_div ltf_pinv ?posrE ?pmulrn_lgt0//. + rewrite /= -[in X in X -> _]mulr_natl -ltr_pdivl_mull//. + by rewrite -[in X in X -> _]subr_gt0. +near (0%R : R)^'+ => d. +have axrdk : a%:E < (fine (mu (ball x (r + d))))^-1%:E * k. + rewrite lebesgue_measure_ball//; last by rewrite addr_ge0// ltW. + rewrite -(fineK k_fin_num) -lte_pdivr_mulr; last first. + by rewrite fine_gt0// k_gt0 k_lty. + rewrite -!EFinM !lte_fin -invf_div ltf_pinv//; last first. + by rewrite posrE fine_gt0// ltry andbT lte_fin pmulrn_lgt0// addr_gt0. + rewrite -mulr_natl -ltr_pdivl_mull// -ltr_subr_addl. + by near: d; exact: nbhs_right_lt. +exists (ball x d). + by split; [exact: (@ball_open _ [normedModType R of R^o])|exact: ballxx]. +move=> y; rewrite /ball/= => xyd. +have ? : ball x r `<=` ball y (r + d). + move=> /= z; rewrite /ball/= => xzr; rewrite -(subrK x y) -(addrA (y - x)%R). + by rewrite (le_lt_trans (ler_norm_add _ _))// addrC ltr_add// distrC. +have ? : k <= \int[mu]_(z in ball y (r + d)) `|(f z)%:E|. + apply: subset_integral => //; [exact: measurable_ball|exact: measurable_ball|]. + apply: measurable_funTS; apply: measurableT_comp => //=. + by apply/measurableT_comp => //=; case: locf. +have afxrdi : a%:E < (fine (mu (ball x (r + d))))^-1%:E * + \int[mu]_(z in ball y (r + d)) `|(f z)%:E|. + by rewrite (lt_le_trans axrdk)// lee_wpmul2l// lee_fin invr_ge0// fine_ge0. +have /lt_le_trans : a%:E < HL_max f y (r + d). + rewrite (lt_le_trans afxrdi)// /HL_max. + rewrite lebesgue_measure_ball; last by rewrite addr_ge0// ltW. + rewrite lebesgue_measure_ball; last by rewrite addr_ge0// ltW. + rewrite lee_wpmul2l// lee_fin invr_ge0// fine_ge0//= lee_fin pmulrn_rge0//. + by rewrite addr_gt0. +apply; apply: ereal_sup_ub => /=. +by exists (r + d)%R => //; rewrite in_itv/= andbT addr_gt0. +Unshelve. all: by end_near. Qed. + +Lemma measurable_HL_maximal f : + locally_integrable setT f -> measurable_fun setT (HL f). +Proof. +move=> lf; apply: lower_semicontinuous_measurable. +exact: lower_semicontinuous_HL_maximal. +Qed. + +Let norm1 D f := \int[mu]_(y in D) `|(f y)%:E|. + +Lemma maximal_inequality f c : + locally_integrable setT f -> (0 < c)%R -> + mu [set x | HL f x > c%:E] <= (3%:R / c)%:E * norm1 setT f. +Proof. +move=> /= locf c0. +have r_proof x : HL f x > c%:E -> {r | (0 < r)%R & + \int[mu]_(y in ball x r) `|(f y)%:E| > c%:E * mu (ball x r)}. + move=> /ereal_sup_gt/cid2[y /= /cid2[r]]. + rewrite in_itv/= andbT => rg0 <-{y} Hc; exists r => //. + rewrite -(@fineK _ (mu (ball x r))) ?ge0_fin_numE//; last first. + by rewrite lebesgue_measure_ball ?ltry// ltW. + rewrite -lte_pdivl_mulr// 1?muleC// fine_gt0//. + by rewrite lebesgue_measure_ball 1?ltW// ltry lte_fin mulrn_wgt0. +rewrite lebesgue_regularity_inner_sup//; last first. + rewrite -[X in measurable X]setTI; apply: emeasurable_fun_o_infty => //. + exact: measurable_HL_maximal. +apply: ub_ereal_sup => /= x /= [K [cK Kcmf <-{x}]]. +pose r_ x := + if pselect (HL f x > c%:E) is left H then s2val (r_proof _ H) else 1%R. +have r_pos (x : R) : (0 < r_ x)%R. + by rewrite /r_; case: pselect => //= cMfx; case: (r_proof _ cMfx). +have cMfx_int x : c%:E < HL f x -> + \int[mu]_(y in ball x (r_ x)) `|(f y)|%:E > c%:E * mu (ball x (r_ x)). + move=> cMfx; rewrite /r_; case: pselect => //= => {}cMfx. + by case: (r_proof _ cMfx). +set B := fun r => ball r (r_ r). +have {}Kcmf : K `<=` cover [set i | HL f i > c%:E] (fun i => ball i (r_ i)). + by move=> r /Kcmf /= cMfr; exists r => //; exact: ballxx. +have {Kcmf}[D Dsub Kcover] : finite_subset_cover [set i | c%:E < HL f i] + (fun i => ball i (r_ i)) K. + move: cK; rewrite compact_cover => /(_ _ _ _ _ Kcmf); apply. + by move=> /= x cMfx; exact/(@ball_open _ [normedModType R of R^o])/r_pos. +have KDB : K `<=` cover [set` D] B. + by apply: (subset_trans Kcover) => /= x [r Dr] rx; exists r. +have is_ballB i : is_ball (B i) by exact: is_ball_ball. +have Bset0 i : B i !=set0 by exists i; exact: ballxx. +have [E [ED tEB DE]] := @vitali_lemma_finite_cover _ _ B is_ballB Bset0 D. +pose E' := undup E. +have {ED}E'D : {subset E' <= D} by move=> x; rewrite mem_undup => /ED. +have {tEB}tE'B : trivIset [set` E'] B. + by apply: sub_trivIset tEB => x/=; rewrite mem_undup. +have {DE}DE' : cover [set` D] B `<=` + cover [set` E'] (scale_ball 3%:R \o B). + by move=> x /DE [r/= rE] Brx; exists r => //=; rewrite mem_undup. +have uniqE' : uniq E' by exact: undup_uniq. +rewrite (@le_trans _ _ (3%:R%:E * \sum_(i <- E') mu (B i)))//. + have {}DE' := subset_trans KDB DE'. + apply: (le_trans (@content_sub_additive _ _ _ [the measure _ _ of mu] + K (fun i => 3%:R *` B (nth 0%R E' i)) (size E') _ _ _)) => //. + - by move=> k ?; rewrite scale_ballE//; exact: measurable_ball. + - by apply: closed_measurable; apply: compact_closed => //; exact: Rhausdorff. + - apply: (subset_trans DE'); rewrite /cover bigcup_seq. + by rewrite (big_nth 0%R)//= big_mkord. + - rewrite /= ge0_sume_distrr//= (big_nth 0%R) big_mkord; apply: lee_sum => i _. + rewrite scale_ballE// !lebesgue_measure_ball ?mulr_ge0 ?(ltW (r_pos _))//. + by rewrite -mulrnAr EFinM. +rewrite !EFinM -muleA lee_wpmul2l//=. +apply: (@le_trans _ _ + (\sum_(i <- E') c^-1%:E * \int[mu]_(y in B i) `|(f y)|%:E)). + rewrite big_seq [in leRHS]big_seq; apply: lee_sum => r /E'D /Dsub /[!inE] rD. + by rewrite -lee_pdivr_mull ?invr_gt0// invrK /B/=; exact/ltW/cMfx_int. +rewrite -ge0_sume_distrr//; last by move=> x _; rewrite integral_ge0. +rewrite lee_wpmul2l//; first by rewrite lee_fin invr_ge0 ltW. +rewrite -ge0_integral_bigsetU//=. +- apply: subset_integral => //. + + by apply: bigsetU_measurable => ? ?; exact: measurable_ball. + + by apply: measurableT_comp => //; apply: measurableT_comp => //; case: locf. +- by move=> n; exact: measurable_ball. +- apply: measurableT_comp => //; apply: measurable_funTS. + by apply: measurableT_comp => //; case: locf. +Qed. + +End hardy_littlewood. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 594b396d6..40ae266c4 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1386,9 +1386,9 @@ Proof. by move/is_intervalP => ->; exact: measurable_itv. Qed. Section coutinuous_measurable. Variable R : realType. -Lemma open_measurable (U : set R) : open U -> measurable U. +Lemma open_measurable (A : set R) : open A -> measurable A. Proof. -move=> /open_bigcup_rat ->; rewrite bigcup_mkcond; apply: bigcupT_measurable_rat. +move=>/open_bigcup_rat ->; rewrite bigcup_mkcond; apply: bigcupT_measurable_rat. move=> q; case: ifPn => // qfab; apply: is_interval_measurable => //. exact: is_interval_bigcup_ointsub. Qed. @@ -1400,7 +1400,7 @@ move=> mD /open_subspaceP [V [oV] VD]; rewrite setIC -VD. by apply: measurableI => //; exact: open_measurable. Qed. -Lemma closed_measurable (U : set R) : closed U -> measurable U. +Lemma closed_measurable (A : set R) : closed A -> measurable A. Proof. by move/closed_openC/open_measurable/measurableC; rewrite setCK. Qed. Lemma compact_measurable (A : set R) : compact A -> measurable A. @@ -1431,6 +1431,14 @@ Qed. End coutinuous_measurable. +Lemma lower_semicontinuous_measurable {R : realType} (f : R -> \bar R) : + lower_semicontinuous f -> measurable_fun setT f. +Proof. +move=> scif; apply: (measurability (ErealGenOInfty.measurableE R)). +move=> /= _ [_ [a ->]] <-; apply: measurableI => //; apply: open_measurable. +by rewrite preimage_itv_o_infty; move/lower_semicontinuousP : scif; exact. +Qed. + Section standard_measurable_fun. Variable R : realType. Implicit Types D : set R. diff --git a/theories/normedtype.v b/theories/normedtype.v index 951ead23e..03a2b544a 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -19,6 +19,11 @@ Require Import ereal reals signed topology prodnormedzmodule. (* balls; the carrier type must have a *) (* normed Zmodule over a numDomainType. *) (* *) +(* lower_semicontinuous f == the extented real-valued function f is *) +(* lower-semicontinuous. The type of f is *) +(* X -> \bar R with X : topologicalType and *) +(* R : realType *) +(* *) (* * Normed modules : *) (* normedModType K == interface type for a normed module *) (* structure over the numDomainType K. *) @@ -351,6 +356,27 @@ rewrite -natr1 natr_absz -abszE gez0_abs ?ceil_ge0// 1?ler_oppr ?oppr0//. by rewrite ltr_spaddr. Qed. +Section lower_semicontinuous. +Context {X : topologicalType} {R : realType}. +Implicit Types f : X -> \bar R. +Local Open Scope ereal_scope. + +Definition lower_semicontinuous f := forall x a, a%:E < f x -> + exists2 V, nbhs x V & forall y, V y -> a%:E < f y. + +Lemma lower_semicontinuousP f : + lower_semicontinuous f <-> forall a, open [set x | f x > a%:E]. +Proof. +split=> [sci a|openf x a afx]. + rewrite openE /= => x /= /sci[A + Aaf]; rewrite nbhsE /= => -[B xB BA]. + apply: nbhs_singleton; apply: nbhs_interior. + by rewrite nbhsE /=; exists B => // y /BA /=; exact: Aaf. +exists [set x | a%:E < f x] => //. +by rewrite nbhsE/=; exists [set x | a%:E < f x]. +Qed. + +End lower_semicontinuous. + (** neighborhoods *) Section Nbhs'. diff --git a/theories/numfun.v b/theories/numfun.v index 4e8db0cab..17d7654c3 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -308,6 +308,13 @@ Qed. End indic_lemmas. +Lemma patch_indic T {R : numFieldType} (f : T -> R) (D : set T) : + f \_ D = (f \* \1_D)%R. +Proof. +apply/funext => x /=; rewrite /patch /= indicE. +by case: ifPn => _; rewrite ?(mulr1, mulr0). +Qed. + Lemma xsection_indic (R : ringType) T1 T2 (A : set (T1 * T2)) x : xsection A x = (fun y => (\1_A (x, y) : R)) @^-1` [set 1]. Proof.