maximal inequality modulo boundedness

theories/lebesgue_integral.v

@@ -5344,3 +5344,376 @@ Qed.
 
 End sfinite_fubini.
 Arguments sfinite_Fubini {d d' X Y R} m1 m2 f.
+
+(* PR in progress *)
+Lemma eseries_cond {R : numFieldType} (f : nat -> \bar R) P N :
+  (\sum_(N <= i <oo | P i) f i = \sum_(i <oo | P i && (N <= i)%N) f i)%E.
+Proof. by congr (lim _); apply: eq_fun => n /=; apply: big_nat_widenl. Qed.
+
+Lemma eseries_mkcondr {R : numFieldType} (f : nat -> \bar R) P Q :
+  (\sum_(i <oo | P i && Q i) f i = \sum_(i <oo | P i) if Q i then f i else 0)%E.
+Proof. by congr (lim _); apply/funext => n; rewrite big_mkcondr. Qed.
+
+Lemma lee_addgt0Pr {R : realType} (x y : \bar R) :
+  reflect (forall e, (0 < e)%R -> (x <= y + e%:E)%E) (x <= y)%E.
+Proof.
+apply/(iffP idP) => [|].
+- move: x y => [x| |] [y| |]//.
+  + rewrite lee_fin => xy e e0.
+    rewrite -EFinD lee_fin.
+    by rewrite ler_paddr// ltW.
+  + by move=> _ e e0; rewrite leNye.
+- move: x y => [x| |] [y| |]// xy.
+  + rewrite lee_fin; apply/ler_addgt0Pr => e e0.
+    by rewrite -lee_fin EFinD xy.
+  + by rewrite leey.
+  + by move: xy => /(_ 1 lte01).
+  + by move: xy => /(_ 1 lte01).
+  + by move: xy => /(_ 1 lte01).
+  + by rewrite leNye.
+Qed.
+(* /PR in progress *)
+
+Section outer_measureU.
+Context d (T : semiRingOfSetsType d) (R : realType).
+Variable mu : {outer_measure set T -> \bar R}.
+Local Open Scope ereal_scope.
+
+Lemma outer_measure_subadditive (F : nat -> set T) n :
+  mu (\big[setU/set0]_(i < n) F i) <= \sum_(i < n) mu (F i).
+Proof.
+set F' := fun k => if (k < n)%N then F k else set0.
+rewrite -(big_mkord xpredT F) big_nat (eq_bigr F')//; last first.
+  by move=> k /= kn; rewrite /F' kn.
+rewrite -big_nat big_mkord.
+have := outer_measure_sigma_subadditive mu F'.
+rewrite (bigcup_splitn n) (_ : bigcup _ _ = set0) ?setU0; last first.
+  by rewrite bigcup0 // => k _; rewrite /F' /= ltnNge leq_addr.
+move/le_trans; apply.
+rewrite (nneseries_split n)// [X in _ + X](_ : _ = 0) ?adde0//; last first.
+  rewrite eseries_cond/= eseries_mkcond eseries0//.
+  by move=> k _; case: ifPn => //; rewrite /F' leqNgt => /negbTE ->.
+by apply: lee_sum => i _; rewrite /F' ltn_ord.
+Qed.
+
+Lemma outer_measureU2 A B : mu (A `|` B) <= mu A + mu B.
+Proof.
+have := outer_measure_subadditive (bigcup2 A B) 2.
+by rewrite !big_ord_recl/= !big_ord0 setU0 adde0.
+Qed.
+
+End outer_measureU.
+
+Lemma ereal_sup_le {R : realType} (A : set (\bar R)) x :
+  A !=set0 -> (forall y, A y -> x <= y)%E ->
+  (x <= ereal_sup A)%E.
+Proof.
+by move=> [x0 Ax0] Ax; rewrite (@le_trans _ _ x0)//;
+  [exact: Ax|exact: ereal_sup_ub].
+Qed.
+
+Lemma trivIset_nth (I : eqType) d (T : measurableType d) h (t : seq I)
+  (F : I -> set T) : uniq (h :: t) ->
+  trivIset [set` h :: t] F <->
+    trivIset (`I_(size (h :: t))) (fun i => F (nth h (in_tuple (h :: t)) i)).
+Proof.
+move=> uht; split=> /trivIsetP htF; apply/trivIsetP => i j Di Dj ij.
+  apply: htF => //=.
+  by apply/(nthP h); exists i.
+  by apply/(nthP h); exists j.
+  apply: contra ij => /eqP.
+  by move/uniqP => /(_ uht); rewrite !inE Di Dj => /(_ _ _)/eqP; exact.
+move/(nthP h) : Di => -[i' i'ht i'i].
+move/(nthP h) : Dj => -[j' j'ht j'j].
+rewrite -i'i -j'j; apply: htF => //.
+by apply: contra ij; rewrite -i'i -j'j => /eqP ->.
+Qed.
+
+Lemma ge0_integral_bigsetU_seq d (T : measurableType d) (R : realType)
+    (mu : {measure set T -> \bar R}) (I : eqType) (F : I -> set T)
+    (f : T -> \bar R) (E : seq I) : uniq E ->
+  (forall n, measurable (F n)) ->
+  let D := \big[setU/set0]_(i <- E) F i in
+  measurable_fun D f ->
+  (forall x, D x -> (0 <= f x))%E ->
+  trivIset [set` E] F ->
+  (\int[mu]_(x in D) f x = \sum_(i <- E) \int[mu]_(x in F i) f x)%E.
+Proof.
+move: E => [uE mF D mf f0 tF|h t uE mF].
+  by rewrite /D !big_nil integral_set0.
+rewrite !(big_nth h) !big_mkord => D mf f0 tF.
+rewrite -(@ge0_integral_bigsetU _ _ _ _ (fun i => F (nth h (in_tuple (h :: t)) i)))//.
+exact/trivIset_nth.
+Qed.
+
+Lemma lebesgue_measure_inner_regular {R : realType} (A : set R) :
+  measurable A ->
+  let mu := @lebesgue_measure R in
+  (mu A < +oo)%E ->
+  mu A = ereal_sup [set mu K | K in [set K | compact K /\ K `<=` A]].
+Proof.
+move=> mA mu muA; apply/eqP; rewrite eq_le; apply/andP; split; last first.
+  apply: ub_ereal_sup => /= x [B /= [cB BA <-{x}]].
+  exact: le_outer_measure.
+apply/lee_addgt0Pr => e e0.
+have [B [cB BA /= ABe]] := lebesgue_regularity_inner mA muA e0.
+rewrite -{1}(setDKU BA).
+rewrite (@le_trans _ _ (mu B + mu (A `\` B))%E)//.
+  by rewrite setUC outer_measureU2.
+rewrite lee_add//; last by rewrite ltW.
+by apply: ereal_sup_ub => /=; exists B.
+Qed.
+
+Section lower_semicontinuous.
+Local Open Scope ereal_scope.
+
+Definition lower_semicontinuous (X : topologicalType) (R : realType)
+    (u : X -> \bar R) :=
+  forall x (a : R), (a%:E < u x)%E ->
+    exists2 V, nbhs x V & forall y, V y -> (a%:E < u y)%E.
+
+Lemma lower_semicontinuousP {X : topologicalType} {R : realType}
+    (f : X -> \bar R) :
+  lower_semicontinuous f <-> forall a : R, 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.
+
+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.
+rewrite preimage_itv_o_infty.
+by move/lower_semicontinuousP : scif; apply.
+Qed.
+
+End lower_semicontinuous.
+
+Definition locally_integrable {R : realType} (D : set R) (f : R -> R) :=
+  [/\ measurable_fun setT f,
+      open D &
+      forall K, K `<=` D -> compact K ->
+        (\int[lebesgue_measure]_(x in K) `|f x|%:E < +oo)%E].
+
+Section hardy_littlewood.
+Context {R : realType}.
+Notation mu := (@lebesgue_measure R).
+Local Open Scope ereal_scope.
+
+Definition HL_max (f : R -> R) (x : R^o) (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 : R -> R) (x : R^o) 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 : R -> R) (x : R^o) : \bar R :=
+  ereal_sup [set HL_max f x r | r in `]0, +oo[%classic%R].
+
+Notation M := HL_maximal.
+
+Lemma HL_maximal_ge0 (f : R -> R) :
+  locally_integrable setT f -> forall x, 0 <= M f x.
+Proof.
+move=> [mf _ locf] x.
+apply: ereal_sup_le => //=; last first.
+  by move=> y [r]; rewrite in_itv/= andbT => r0 <-{y}; exact: HL_max_ge0.
+have /locf : compact (closed_ball x 1) by exact: closed_ballR_compact.
+move/(_ (@subsetT _ _)) => koo.
+pose k' := \int[mu]_(x in ball x 1) `|f x|%:E.
+have k'oo : k' < +oo.
+  rewrite (le_lt_trans _ koo)//; apply: subset_integral => //.
+  - exact: measurable_ball.
+  - exact: measurable_closed_ball.
+  - apply/measurableT_comp => //.
+    by apply/measurableT_comp => //; exact: measurable_funTS.
+  - exact: (@subset_closed_ball _ [normedModType R of R^o]).
+exists ((fine (mu (ball x 1)))^-1%:E * k') => /=.
+by exists 1%R => //; rewrite in_itv/= ltr01.
+Qed.
+
+Lemma lower_semicontinuous_HL_maximal (f : R -> R) :
+  locally_integrable setT f -> lower_semicontinuous (M f).
+Proof.
+move=> 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_maximal_ge0 _ _)).
+rewrite openE /= => x /= /ereal_sup_gt[_ [r r0] <-] axrk.
+rewrite /= in_itv /= andbT in r0.
+rewrite /HL_max in axrk; set k := integral _ _ _ in axrk.
+apply: nbhs_singleton; apply: nbhs_interior; rewrite nbhsE /=.
+have k_lty : k < +oo.
+  case: locf => mf _ locf.
+  rewrite (le_lt_trans _ (locf (closed_ball x r) _ _))//.
+    apply: subset_integral => //.
+    - exact: measurable_ball.
+    - by apply: measurable_closed_ball; exact/ltW.
+    - apply: measurable_funTS; apply/measurableT_comp => //=.
+      exact: measurableT_comp.
+    - exact: (@subset_closed_ball _ [normedModType R of R^o]).
+  exact: closed_ballR_compact.
+have k_fin_num : k \is a fin_num by rewrite ge0_fin_numE//= integral_ge0.
+have k_gt0 : 0 < k.
+  rewrite lt_neqAle integral_ge0// andbT; apply/negP => /eqP k0.
+  by move: axrk; rewrite -k0 mule0 ltNge lee_fin a0.
+move: a0; rewrite le_eqVlt => /predU1P[a0|a0].
+  move: axrk; rewrite -{a}a0 => xrk.
+  near (at_right (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) <= M 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//.
+  by rewrite lee_fin pmulrn_rge0// 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: axrk; 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 by rewrite ltW.
+  rewrite -!EFinM !lte_fin -invf_div ltf_pinv//; last first.
+    by rewrite posrE pmulrn_lgt0.
+  rewrite /= -[in X in X -> _]mulr_natl -ltr_pdivl_mull//.
+  by rewrite -[in X in X -> _]subr_gt0.
+near (at_right (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.
+
+(* NB: see the PR on hoelder that introduces a notation and a definition for this norm *)
+Let norm1 f := \int[mu]_y `|(f y)%:E|.
+
+Lemma maximal_inequality (f : R -> R) c :
+  locally_integrable setT f -> (0 < c)%R ->
+  mu [set x | M f x > c%:E] <= (3%:R / c)%:E * norm1 f.
+Proof.
+move=> /= locf c0.
+have r_proof x : M 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_measure_inner_regular//; last 2 first.
+  - rewrite -[X in measurable X]setTI; apply: emeasurable_fun_o_infty => //.
+    apply: lower_semicontinuous_measurable.
+    exact: lower_semicontinuous_HL_maximal.
+  - admit.
+apply: ub_ereal_sup => /= x /= [K [cK Kcmf <-{x}]].
+pose r_ x :=
+  if pselect (M 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 < M 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 => (r, PosNum (r_pos r))).
+have {}Kcmf : K `<=` cover [set i | M 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 < M 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] (scale_ball 1 \o B).
+  apply: (subset_trans Kcover) => /= x [r Dr] rx.
+  by exists r => //=; rewrite scale_ball1.
+have [E [ED tEB DE]] := @vitali_lemma_finite_cover _ _ B 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'] (scale_ball 1 \o B).
+  by apply: sub_trivIset tEB => x/=; rewrite mem_undup.
+have {DE}DE' : cover [set` D] (scale_ball 1 \o B) `<=`
+               cover [set` E'] (scale_ball 3 \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 (scale_ball 1 (B i))))//.
+  have {}DE' := subset_trans KDB DE'.
+  apply: (le_trans (@content_sub_additive _ _ _ mu
+    K (fun i => scale_ball 3 (B (nth 0%R E' i))) (size E') _ _ _)) => //.
+  - by move=> k ?; exact: measurable_ball.
+  - by apply: closed_measurable; apply: compact_closed => //; exact: Rhausdorff.
+  - apply: (subset_trans DE'); rewrite /cover bigcup_set.
+    by rewrite (big_nth 0%R)//= big_mkord.
+  - rewrite /= ge0_sume_distrr//= (big_nth 0%R) big_mkord; apply: lee_sum => i _.
+    by rewrite !lebesgue_measure_ball ?mulr_ge0 ?ler0n// mul1r -mulrnAr EFinM.
+rewrite !EFinM -muleA lee_wpmul2l//=.
+apply: (@le_trans _ _ (\sum_(i <- E') c^-1%:E *
+    \int[mu]_(y in scale_ball 1 (B i)) `|(f y)|%:E)).
+  rewrite big_seq [in leRHS]big_seq; apply: lee_sum => r /E'D /Dsub /[!inE] rD.
+  rewrite -lee_pdivr_mull ?invr_gt0// invrK !scale_ball1 /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_seq//= ; last 2 first.
+  - by move=> n; rewrite scale_ball1; exact: measurable_ball.
+  - apply: measurableT_comp => //; apply: measurable_funTS.
+    by apply: measurableT_comp => //; case: locf.
+apply: subset_integral => //.
+- by apply: bigsetU_measurable => ? ?; exact: measurable_ball.
+- apply: measurableT_comp => //.
+  by apply: measurableT_comp => //; case: locf.
+Admitted.
+
+End hardy_littlewood.