diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index bee22e546b..4f3a441204 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -37,6 +37,20 @@
     `measurable_closed_ball`, `lebesgue_measure_closed_ball`,
     `measurable_scale_cball`
 
+- in `classical_sets.v`:
+  + lemmas `trivIsetT_bigcup`, `mem_not_I`
+
+- in `sequences.v`:
+  + lemma `nneseries_tail_cvg`
+
+- in `normedtype.v`:
+  + lemmas `open_subball`, `closed_disjoint_closed_ball`
+
+- in `lebesgue_measure.v`:
+  + lemmas `measure_sigma_sub_additive_tail`, `outer_measure_sigma_subadditive_tail`
+  + definition `vitali_cover`
+  + lemma `vitali_theorem`
+
 ### Changed
 
 ### Renamed
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index 8eaa1ba7cd..1e375d6f28 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -5632,3 +5632,401 @@ by rewrite ritv //= -EFinM lee_fin mulrC.
 Unshelve. all: by end_near. Qed.
 
 End lebesgue_differentiation.
+
+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 ereal_inf_le {R : realType} (A : set (\bar R)) x :
+  A !=set0 -> (forall y, A y -> y <= x)%E ->
+  (ereal_inf A <= x)%E.
+Proof.
+by move=> [x0 Ax0] Ax; rewrite (@le_trans _ _ x0)//;
+  [exact: ereal_inf_lb|exact: Ax].
+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.
+
+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 D f,
+      open D &
+      forall K, K `<=` D -> compact K ->
+        (\int[lebesgue_measure]_(x in K) `|f x|%:E < +oo)%E].
+
+Lemma locally_integrableN {R : realType} (D : set R) (f : R -> R) :
+  locally_integrable D f -> locally_integrable D (\- f)%R.
+Proof.
+move=> [mf oD intf]; split => //; first exact: measurableT_comp.
+by move=> K KD cK; under eq_integral do rewrite normrN; exact: intf.
+Qed.
+
+Lemma locally_integrableD {R : realType} (D : set R) (f g : R -> R) :
+  locally_integrable D f -> locally_integrable D g ->
+  locally_integrable D (f \+ g)%R.
+Proof.
+move=> [mf oD intf] [mg _ intg]; split => //.
+  exact: measurable_funD.
+move=> K KD cK.
+suff : lebesgue_measure.-integrable K ((EFin \o f) \+ (EFin \o g))%E.
+  by move/integrableP => [_].
+apply: integrableD => //=.
+- exact: compact_measurable.
+- apply/integrableP; split => //.
+  + apply/EFin_measurable_fun.
+    apply: measurable_funS mf => //.
+    exact: open_measurable.
+  + by apply: intf.
+- apply/integrableP; split => //.
+  + apply/EFin_measurable_fun.
+    apply: measurable_funS mg => //.
+    exact: open_measurable.
+  + by apply: intg.
+Qed.
+
+Lemma locally_integrableB {R : realType} (D : set R) (f g : R -> R) :
+  locally_integrable D f -> locally_integrable D g ->
+  locally_integrable D (f \- g)%R.
+Proof.
+move=> locf locg.
+apply: locally_integrableD => //.
+exact: locally_integrableN.
+Qed.
+
+Lemma patch_indic T {R : realType} (f : T -> R) (D : set T) :
+  f \_ D = (f \* \1_D)%R.
+Proof.
+apply/funext => x /=; rewrite /patch /= /GRing.Ring.mul /= indicE.
+by case: ifPn => _; rewrite ?(mulr1, mulr0).
+Qed.
+
+Lemma epatch_indic T {R : realType} (f : T -> \bar R) (D : set T) :
+  f \_ D = (f \* (EFin \o \1_D))%E.
+Proof.
+apply/funext => x /=; rewrite /patch /= /GRing.mul /= indicE.
+by case: ifPn => _; rewrite ?(mule1, mule0).
+Qed.
+
+Lemma integral_setI_restrict d (T : measurableType d) (R : realType)
+  (mu : {measure set T -> \bar R}) (E D : set T) (mD : measurable D)
+  (f : T -> \bar R) (mE : measurable E) :
+  (\int[mu]_(x in E `&` D) f x = \int[mu]_(x in E) (f \_ D) x)%E.
+Proof.
+rewrite integral_setI_indic//; apply: eq_integral => x xE.
+by rewrite (epatch_indic f D).
+Qed.
+
+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) (D : set R) :
+  locally_integrable D f -> forall x, 0 <= M (f \_ D)%R x.
+Proof.
+move=> [mf oD locf] 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(* should this lemma use patch?*)/=; last 2 first.
+  exact: open_measurable.
+  exact: measurable_ball.
+congr *%E; apply: eq_integral => /= y yx1.
+rewrite patch_indic/=.
+by rewrite normrM EFinM; congr *%E; rewrite ger0_norm.
+Qed.
+
+Lemma HL_maximalT_ge0 (f : R -> R) :
+  locally_integrable setT f -> forall x, 0 <= M f x.
+Proof.
+by move=> + x => /HL_maximal_ge0 /(_ x); rewrite patch_setT.
+Qed.
+
+Lemma locally_integrable_patch (f : R -> R) (D : set R) : compact D ->
+  locally_integrable D f -> locally_integrable setT (f \_ D).
+Proof.
+move=> cD; move=> [mDf oD intDf]; split => //.
+- apply/(@measurable_restrict _ _ _ _ D setT) => //.
+  exact: compact_measurable.
+- exact: openT.
+- move=> K _ cK.
+  set g := (fun x => `|f x|%:E) \_ D.
+  set fD := fun x => `|(f \_ D) x|%:E.
+  rewrite (@eq_integral _ _ _ mu K g fD)//=; last first.
+    move=> x xK.
+    rewrite /fD /g //=.
+    rewrite epatch_indic//= patch_indic/= normrM /= EFinM; congr *%E.
+    by rewrite ger0_norm.
+  rewrite -integral_setI_restrict//=; last first.
+    exact: compact_measurable.
+    exact: compact_measurable.
+  rewrite (le_lt_trans _ (intDf _ _ cD))//.
+  apply: subset_integral => //=.
+  by apply: measurableI; exact: compact_measurable.
+  exact: compact_measurable.
+  by do 2 apply: measurableT_comp => //=.
+Qed.
+
+Lemma lower_semicontinuous_HL_maximal (f : R -> R) :
+  locally_integrable setT f -> lower_semicontinuous (M 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] <-] 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.
+  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.
+
+Lemma measurable_HL_maximal (f : R -> R) :
+  locally_integrable setT f -> measurable_fun setT (M f).
+Proof.
+move=> lf; apply: lower_semicontinuous_measurable.
+by apply: lower_semicontinuous_HL_maximal.
+Qed.
+
+(* NB: see the PR on hoelder that introduces a notation and a definition for this norm *)
+Let norm1 D f := \int[mu]_(y in D) `|(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 setT 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_regularity_inner_sup//; last 1 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 (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%: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 (scale_ball 1 (B i))))//.
+  have {}DE' := subset_trans KDB DE'.
+  apply: (le_trans (@content_sub_additive _ _ _ [the measure _ _ of mu]
+    K (fun i => scale_ball 3%:R (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_seq.
+    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.
+Qed.
+
+End hardy_littlewood.