diff --git a/theories/charge.v b/theories/charge.v
index 1fd90eb7bc..6e077a7a17 100644
--- a/theories/charge.v
+++ b/theories/charge.v
@@ -585,7 +585,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 09ce1738c1..43f0babf2e 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.
+Require Import esum measure lebesgue_measure numfun realfun.
 
 (******************************************************************************)
 (*                            Lebesgue Integral                               *)
@@ -1708,7 +1708,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}].
@@ -1751,7 +1751,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}].
@@ -2863,8 +2863,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 :=
@@ -4919,7 +4921,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),
@@ -5954,3 +5956,1428 @@ rewrite -ge0_integral_bigsetU//=.
 Qed.
 
 End hardy_littlewood.
+
+Lemma nbhs_pinfty_ge_nat {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 abs_ceil (R : realType) (x : R) : (`|x| <= `|ceil x|.+1%:R)%R.
+Proof.
+have [x0|x0] := leP 0%R x.
+  rewrite ger0_norm// -natr1 (@le_trans _ _ ((ceil x)%:~R + 1)%R)//; last first.
+    by rewrite ler_add2r natr_absz ler_int ler_norm.
+  by rewrite (le_trans (ceil_ge _))// ler_addl//.
+rewrite /ceil.
+rewrite abszN.
+rewrite -(normrN x).
+rewrite -natr1.
+apply/ltW.
+rewrite (lt_le_trans (lt_succ_floor _))//.
+rewrite natr_absz.
+rewrite ler_add2r.
+rewrite ler_int.
+rewrite (le_trans _ (ler_norm _))//.
+by rewrite (gtr0_norm)// ltr_oppr oppr0.
+Qed.
+
+(* TODO: move *)
+Lemma near_nbhs_ge0 (R : realType) (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 near_nbhs_gt0 (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.
+
+Section lebesgue_point.
+Context {R : realType}.
+Local Notation mu := (@lebesgue_measure R).
+Local Open Scope ereal_scope.
+
+Definition favg (f : R -> R) (x r : R) := iavg (center (f x) \o f) (ball x r).
+
+Lemma favgD (f g : R -> R) (a x : R) :
+  measurable_fun (ball a x) f -> measurable_fun (ball a x) g ->
+  favg (f \+ g)%R a x <= (favg f a \+ favg g a) x.
+Proof.
+move=> mf mg.
+rewrite /favg/=.
+apply: (le_trans _ (iavgD _ _ _ _)) => //.
+- rewrite le_eqVlt; apply/orP; left; apply/eqP => /=.
+  congr iavg.
+  apply/funext => r /=.
+  by rewrite opprD addrACA.
+- exact: measurable_ball.
+- have [x0|x0] := leP x 0%R.
+    by rewrite (ball0 _ _).2// measure0.
+  by rewrite (lebesgue_measure_ball _ (ltW x0)) ltry.
+- exact: measurable_funB.
+- exact: measurable_funB.
+Qed.
+
+Lemma favg0 (f : R -> R) (x r : R) : (r <= 0)%R -> favg f x r = 0.
+Proof. by move=> r0; rewrite /favg/= (ball0 _ _).2//= iavg0. Qed.
+
+Definition lebesgue_pt (f : R -> R) (x : R) :=
+  favg f x r @[r --> (0%R:R)^'+]--> 0.
+
+End lebesgue_point.
+
+Section continuous_favg_fin_num.
+
+Local Open Scope ereal_scope.
+Let continuous_integralB_fin_num (R : realType) (g : R -> R) x :
+  measurable_fun setT g -> {for x, continuous g} ->
+  \forall t \near 0%R:R,
+    \int[lebesgue_measure]_(y in ball x t) `|(g y)%:E - (g x)%:E| \is a fin_num.
+Proof.
+move=> mg /(@cvgrPdist_le _ [pseudoMetricNormedZmodType R of R^o]) gx.
+near (0%R:R)^'+ => d.
+have d0 : (0 < d)%R by near: d; exact: nbhs_right_gt.
+have := gx _ d0 => -[z /= z0] {}gx.
+near=> t.
+rewrite ge0_fin_numE ?integral_ge0//.
+rewrite (@le_lt_trans _ _ (\int[lebesgue_measure]_(y in ball x z) `|g y - g x|%:E))//.
+  apply: subset_integral => //=.
+  - exact: measurable_ball.
+  - exact: measurable_ball.
+  - do 2 apply: measurableT_comp => //=; apply: measurable_funB => //.
+    exact: measurable_funS mg.
+  - by apply: le_ball; near: t; exact: near_nbhs_ge0.
+rewrite (@le_lt_trans _ _ (\int[lebesgue_measure]_(y in ball x z) d%:E))//=.
+  apply: ge0_le_integral => //=.
+  - exact: measurable_ball.
+  - do 2 apply: measurableT_comp => //=; apply: measurable_funB => //.
+    exact: measurable_funS mg.
+  - by rewrite lee_fin ltW.
+  - by move=> y xzy;rewrite lee_fin distrC; exact: gx.
+rewrite integral_cst// ?mul1e.
+  rewrite [X in _ * X](_ : _ = lebesgue_measure (ball x z)) //.
+  by rewrite lebesgue_measure_ball// ?ltry// ltW.
+exact: measurable_ball.
+Unshelve. all: by end_near.
+Qed.
+
+(* NB: see lebesgue_differentiation_continuous for duplicate
+ f -> `|f - g| *)
+Lemma continuous_favg_fin_num {R : realType} (g : R -> R) x :
+  measurable_fun setT g -> {for x, continuous g} ->
+  \forall F \near (0%R:R), favg g x F \is a fin_num.
+Proof.
+move=> mg gx.
+have [y /= y0 H] := continuous_integralB_fin_num mg gx.
+move/(@cvgrPdist_le _ [pseudoMetricNormedZmodType R of R^o]) in gx.
+near (0%R:R)^'+ => d.
+have d0 : (0 < d)%R by near: d; exact: nbhs_right_gt.
+have := gx _ d0 => -[x1 /= x10] {}gx.
+near=> t.
+have [t0|t0] := leP t 0%R; first by rewrite favg0.
+rewrite fin_numM// H//= sub0r normrN gtr0_norm//.
+by near: t; exact: near_nbhs_gt0.
+Unshelve. all: by end_near.
+Qed.
+Local Close Scope ereal_scope.
+
+End continuous_favg_fin_num.
+
+Global Instance ProperFilterR (R : realType) (p : R) :
+  ProperFilter [set P | exists2 i : R, [set e | (0 < e)%R] i & ball_ [eta normr] p i `<=` P].
+Proof.
+apply: Build_ProperFilter => //.
+move=> P /= [r r0 prP]; exists p; apply: prP.
+exact: ball_norm_center.
+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.
+
+Lemma locally_integrable_patch (R : realType) (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 _ _ _ [the measure _ _ of lebesgue_measure] 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.
+
+Section lim_favg.
+Context {R : realType}.
+Local Open Scope ereal_scope.
+Implicit Types f g : R -> R.
+
+Definition lim_favg f x := lime_sup (favg f x) (0%R:R).
+
+Local Notation "f ^*" := (lim_favg f).
+
+Lemma lim_favg_ge0 f x : 0 <= f^* x.
+Proof. by apply: lime_sup_ge0 => y; rewrite /favg iavg_ge0. Qed.
+
+Lemma lim_favg_le f g : measurable_fun setT f -> locally_integrable setT g ->
+  forall x, (f \+ g)%R^* x <= (f^* \+ g^*) x.
+Proof.
+move=> mf /= [mg _ goo] x; rewrite /lim_favg /=.
+apply: le_trans (lime_supD _); last first.
+  by rewrite ge0_adde_def// inE; exact: lim_favg_ge0.
+apply: lime_sup_le => r r0 y y0 ry.
+by apply: favgD => //;
+  [exact: measurable_funS mf|exact: measurable_funS mg].
+Qed.
+
+Lemma continuous_lim_favg (E : set R) g :
+  measurable_fun setT g -> {in E, continuous g} -> {in E, g^* =1 cst 0}.
+Proof.
+move=> mg gx.
+rewrite /lim_favg.
+suff: {in E, forall x, favg g x r @[r --> (0%R:R)] --> 0}.
+  by move=> h x /h/lim_lime_sup.
+move=> x Ex.
+apply/(@fine_cvgP R) => //.
+have {}gx : {for x, continuous g} by exact: gx.
+move/(@cvgrPdist_le _ [pseudoMetricNormedZmodType R of R^o]) : (gx) => gx'.
+split.
+  exact: (@continuous_favg_fin_num).
+apply/(@cvgrPdist_le _ [pseudoMetricNormedZmodType R of R^o]).
+move=> e e0.
+have := gx' _ e0 => -[x2 x20] gx''.
+have [x0 hx0 H] := continuous_favg_fin_num mg gx.
+near=> t.
+have [t0|t0] := leP t 0%R.
+  by rewrite /= favg0//= subrr normr0 ltW.
+have tx0 : (t < x0)%R by near: t; exact: near_nbhs_gt0.
+have tx2 : (t <= x2)%R by near: t; exact: near_nbhs_ge0.
+rewrite sub0r normrN /= ger0_norm; last first.
+  rewrite fine_ge0// mule_ge0//.
+    by rewrite lee_fin invr_ge0// fine_ge0.
+  exact: integral_ge0.
+rewrite -lee_fin fineK//; last by rewrite H//= sub0r normrN gtr0_norm.
+rewrite /favg/= /iavg/= lee_pdivr_mull//; last first.
+  rewrite fine_gt0// lebesgue_measure_ball// ?ltry ?lte_fin ?mulrn_wgt0//.
+  exact: ltW.
+rewrite (@le_trans _ _ (\int[lebesgue_measure]_(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 mg.
+  - move=> x1 xtx1.
+    by rewrite lee_fin ltW.
+  - move=> x1 xtx1.
+    rewrite lee_fin distrC.
+    apply: gx''.
+    exact: (lt_le_trans xtx1).
+rewrite integral_cst//.
+  rewrite [X in e%:E * X](_ : _ = lebesgue_measure (ball x t)) //.
+  rewrite muleC.
+  by rewrite lebesgue_measure_ball// ?ltry// ltW.
+exact: measurable_ball.
+Unshelve. all: by end_near. Qed.
+
+Lemma lim_favgB (E : set R) (f g : R -> R) (cg : {in E, continuous g}) :
+  measurable_fun setT f ->
+  locally_integrable [set: R] g ->
+  {in E, (f \- g)%R^* =1 f^*}.
+Proof.
+move=> mf locg x Ex.
+apply/eqP; rewrite eq_le; apply/andP; split.
+- rewrite [leRHS](_ : _ = f^* x + (\- g)%R^* x).
+    by apply: lim_favg_le => //; exact: locally_integrableN.
+  rewrite (@continuous_lim_favg [set x] (- g)%R) ?adde0//.
+  + by apply: measurableT_comp => //; case: locg.
+  + move=> y; rewrite inE/= => -> /=.
+    apply/(@continuousN _ [normedModType R of R^o]).
+    exact: 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.
+    apply: lim_favg_le => //.
+    by apply: measurable_funB => //; case: locg.
+  rewrite [X in _ + X](@continuous_lim_favg [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_favgT_HL_maximal f (x : R) : locally_integrable setT f ->
+  f^* x <= HL_maximal f x + `|f x|%:E.
+Proof.
+move=> [mf _ locf]; rewrite /lim_favg; apply: lime_le.
+  apply: nondecreasing_at_right_is_cvge => y t0 z yz.
+  apply: le_ereal_sup => _ /= -[b [yb b0]] <-.
+  exists b => //; split => //.
+  exact: le_ball yb.
+near=> a.
+apply: ub_ereal_sup => _ [b [r'b] /= b0] <-.
+suff : forall r, favg 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 /favg 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.
+    + apply: emeasurable_funD => //; do 2 apply: measurableT_comp => //.
+      exact: measurable_funS mf.
+  move=> /= x0 xrx0.
+  by rewrite -EFinD lee_fin// ler_norm_sub.
+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 lee_add//.
+  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.
+
+Lemma lim_favg_HL_maximal f (D : set R) (x : R) :
+  compact D -> locally_integrable D f ->
+  (f \_ D) ^* x <= HL_maximal (f \_ D) x + `|(f \_ D) x|%:E.
+Proof.
+move=> cD.
+by move/locally_integrable_patch => /(_ cD)/lim_favgT_HL_maximal; exact.
+Qed.
+
+End lim_favg.
+
+(* NB: on the model of invr_lt1? *)
+Lemma invr_plt (R : numFieldType) :
+  {in Num.pos &, forall x y : R, (x^-1 < y)%R = (y^-1 < x)%R}.
+Proof.
+move=> x y x0 y0.
+by rewrite -[in LHS](@invrK _ y) ltf_pinv// posrE invr_gt0.
+Qed.
+
+(* TODO: move *)
+Lemma interval_setD1r 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 interval_setD1l 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.
+
+(*Reserved Notation "a `| A" (at level 52, left associativity).
+Notation "A `| a" := (A `|` [set a]) : classical_set_scope.*)
+
+Lemma interval_setU1r d (R : porderType d) x (r : R) :
+  (x <= BLeft r)%O ->
+  ([set` Interval x (BLeft r)] `|` [set r] = [set` Interval x (BRight r)])%classic.
+Proof.
+move=> xr; rewrite -[RHS](@setDKU _ [set r]) ?interval_setD1r//.
+rewrite sub1set inE/= in_itv/= lexx andbT.
+by case: x xr => // -[].
+Qed.
+
+Lemma interval_setU1l d (R : porderType d) x (r : R) :
+  (BRight r <= x)%O ->
+  (r |` [set` Interval (BRight r) x] = [set` Interval (BLeft r) x])%classic.
+Proof.
+move=> rx; rewrite -[RHS](@setDUK _ [set r]) ?interval_setD1l//.
+rewrite sub1set inE/= in_itv/= lexx/=.
+by case: x rx => // -[].
+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 _ [normedModType R of R^o])//= /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 _ [normedModType R of R^o]) /ball_ set_itvE.
+by apply/seteqP; split => t/=; rewrite ltr_distlC.
+Qed.
+
+Lemma closed_ball_punct {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// -(@interval_setU1l _ _ _ (x - s)%R); last first.
+  by rewrite bnd_simp ler_subl_addr -addrA ler_addl ltW// addr_gt0.
+rewrite -(@interval_setU1r _ _ _ (x + s)%R); last first.
+  by rewrite bnd_simp ltr_subl_addr -addrA ltr_addl addr_gt0.
+by rewrite ball_itv setUA.
+Qed.
+
+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 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 := \int[mu]_(x in A) _.
+set an := \int[mu]_(x in A) _.
+set bp := \int[mu]_(x in B) _.
+set bn := \int[mu]_(x in B) _.
+rewrite oppeD; last first.
+  by rewrite ge0_adde_def// inE integral_ge0.
+by rewrite addeACA.
+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 first.
+  by move=> x; rewrite inE/= => ->.
+by rewrite integral_cst//= lebesgue_measure_set1 mule0.
+Qed.
+
+Lemma integral_setD1_EFin (f : R -> R) y (D : set R) :
+  measurable D -> measurable_fun D f -> D y ->
+  \int[mu]_(x in D) (f x)%:E = \int[mu]_(x in D `\ y) (f x)%:E.
+Proof.
+move=> mD mf Dy.
+rewrite -[in LHS](@setD1K _ y D)//.
+rewrite integral_setU_EFin//.
+rewrite integral_set1// ?add0e//.
+apply: measurableD => //.
+by rewrite setD1K.
+by rewrite disj_set2E; apply/eqP/seteqP; split => // x [? []].
+Qed.
+
+Lemma integral_itv_bndo_bndc (a : itv_bound R) (b : R) (f : R -> R) :
+  measurable_fun setT f ->
+   \int[lebesgue_measure]_(x in [set` Interval a (BLeft b)]) (f x)%:E =
+   \int[lebesgue_measure]_(x in [set` Interval a (BRight b)]) (f x)%:E.
+Proof.
+move=> mf.
+have [ab|ab] := leP a (BLeft b).
+- rewrite [RHS](@integral_setD1_EFin _ b)//.
+  + by rewrite interval_setD1r.
+  + exact: measurable_funS mf.
+  + rewrite /= in_itv /= lexx andbT.
+    by case: a ab => -[].
+- rewrite (_ : [set` _] = set0); last first.
+    apply/seteqP; split => // x/=.
+    rewrite in_itv/=.
+    case: a ab => // -[]//= t; rewrite bnd_simp => bt.
+      by move=> /andP[] /le_lt_trans /[apply]; rewrite ltNge (ltW bt).
+    by move=> /andP[] /lt_trans /[apply]; rewrite ltNge bt.
+  rewrite (_ : [set` _] = set0)//.
+  apply/seteqP; split => // x/=.
+  rewrite in_itv/=.
+  case: a ab => // -[]//= t; rewrite bnd_simp => bt.
+    by move=> /andP[] /le_trans /[apply]; rewrite leNgt bt.
+  by move=> /andP[] /lt_le_trans /[apply]; rewrite ltNge bt.
+Qed.
+
+Lemma integral_itv_obnd_cbnd (a : R) (b : itv_bound R) (f : R -> R) :
+  measurable_fun setT f ->
+   \int[lebesgue_measure]_(x in [set` Interval (BRight a) b]) (f x)%:E =
+   \int[lebesgue_measure]_(x in [set` Interval (BLeft a) b]) (f x)%:E.
+Proof.
+move=> mf.
+have [ab|ab] := leP (BRight a) b.
+- rewrite [RHS](@integral_setD1_EFin _ a)//.
+  + by rewrite interval_setD1l.
+  + exact: measurable_funS mf.
+  + rewrite /= in_itv /= lexx/=.
+    by case: b ab => -[].
+- rewrite (_ : [set` _] = set0); last first.
+    apply/seteqP; split => // x/=; rewrite in_itv/= => /andP[ax].
+    case: b ab => // -[]//= t; rewrite bnd_simp => ta.
+      by move=> /(lt_trans ax); rewrite ltNge ta.
+    by move=> /(lt_le_trans ax); rewrite ltNge (ltW ta).
+  rewrite (_ : [set` _] = set0)//.
+  apply/seteqP; split => // x/=; rewrite in_itv/= => /andP[ax].
+  case: b ab => // -[]//= t; rewrite bnd_simp => ta.
+    by move=> /(le_lt_trans ax); rewrite ltNge ta.
+  by move=> /(le_trans ax); rewrite leNgt ta.
+Qed.
+
+Lemma ge0_integral_ball_closed (s : R) (s0 : (0 < s)%R) (f : R -> \bar R) :
+  measurable_fun (closed_ball 0%R s : set R^o) f ->
+  (forall x, x \in (closed_ball 0%R s : set R^o) -> 0 <= f x) ->
+  \int[mu]_(x in ball 0%R s : set R^o) f x =
+  \int[mu]_(x in closed_ball 0%R s : set R^o) f x.
+Proof.
+move=> mf f0.
+rewrite closed_ball_punct//= sub0r add0r integral_setU//=; last 4 first.
+  by apply: measurableU => //; exact: measurable_ball.
+  by move: mf; rewrite closed_ball_punct// sub0r add0r.
+  by move=> x H; rewrite f0// closed_ball_punct// inE/= sub0r add0r.
+  apply/disj_setPLR => x [->/=|].
+    by apply/eqP; rewrite lt_eqF// gtr_opp.
+  rewrite /ball/= sub0r normrN.
+  by move/ltr_normlW => ?; apply/eqP; rewrite lt_eqF.
+rewrite integral_set1 adde0.
+rewrite integral_setU//=; last 4 first.
+  exact: measurable_ball.
+  apply: measurable_funS mf.
+    exact: measurable_closed_ball.
+  by move=> x; rewrite closed_ball_punct// sub0r add0r; left.
+  by move=> x H; rewrite f0// closed_ball_punct// inE/= sub0r add0r; left.
+  apply/disj_setPRL => x/=.
+  rewrite /ball/= sub0r.
+  move/ltr_normlW => ?.
+  apply/eqP.
+  by rewrite gt_eqF// ltr_oppl.
+by rewrite integral_set1//= ?add0e.
+Qed.
+
+End lebesgue_integral_extra.
+
+(* TODO: move *)
+Lemma cvg_indic {R : realFieldType} (x : R^o) k :
+  x \in (ball 0%R k : set R^o) ->
+  \1_(ball 0%R k : set R^o) y @[y --> x:R] --> (\1_(ball 0%R k) x : R).
+Proof.
+move=> xB.
+apply/(@cvgrPdist_le _ [pseudoMetricNormedZmodType R of R^o]) => e e0.
+near=> t.
+rewrite !indicE xB/= mem_set//=.
+  by rewrite subrr normr0// ltW.
+near: t.
+rewrite inE /ball /= sub0r normrN in xB.
+exists ((k - `|x|)/2)%R => /=; first by rewrite divr_gt0// subr_gt0.
+rewrite /ball_/= => z /= h.
+rewrite /ball/= sub0r normrN.
+rewrite -(subrK x z) (le_lt_trans (ler_norm_add _ _))//.
+rewrite -ltr_subr_addr distrC (lt_le_trans h)//.
+by rewrite ler_pdivr_mulr//= ler_pmulr// ?subr_gt0// ler1n.
+Unshelve. all: by end_near. Qed.
+
+Section lebesgue_differentiation_lemmas.
+Context {R : realType}.
+Local Notation mu := (@lebesgue_measure R).
+Local Open Scope ereal_scope.
+
+Local Notation "f ^*" := (lim_favg f).
+
+Lemma lebesgue_differentiation_suff (E : set R) (f : R -> R) :
+  (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=> suf.
+have neglif : mu.-negligible (E `&` [set x | 0 < f^* x]).
+  have -> : E `&` [set x | 0 < f^* x] =
+            E `&` \bigcup_n [set x | n.+1%:R^-1%:E < f^* x].
+    apply/seteqP; split.
+      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 invr_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 _))// ler_norm.
+      rewrite ltr_nat ltnS.
+      by near: m; exact: nbhs_infty_gt.
+    move=> r [Er] [k ?] /=; split => //.
+    exact: le_lt_trans q.
+  rewrite setI_bigcupr.
+  apply: negligible_bigcup => k/=.
+  by apply: suf; rewrite invr_gt0.
+apply: negligibleS neglif => z /= /not_implyP[Ez H]; split => //.
+rewrite ltNge; apply: contra_notN H.
+rewrite le_eqVlt ltNge lime_sup_ge0 /= ?orbF; last first.
+  by move=> x; exact: iavg_ge0.
+move=> /eqP lime_supfz0.
+suff lime_inffz0 : lime_inf (favg f z) 0 = 0 by exact: lime_inf_sup_lim.
+apply/eqP; rewrite eq_le.
+  rewrite -[X in _ <= X <= _]lime_supfz0 lime_inf_sup/= lime_supfz0.
+by apply: lime_inf_ge0 => x; exact: iavg_ge0.
+Unshelve. all: by end_near. Qed.
+
+End lebesgue_differentiation_lemmas.
+
+Section lebesgue_differentiation.
+Context {R : realType}.
+Local Notation mu := (@lebesgue_measure R).
+Local Open Scope ereal_scope.
+
+Local Notation "f ^*" := (lim_favg f).
+
+Lemma lebesgue_differentiation_bounded (f : R -> R) :
+  let B k := (ball 0 k.+1.*2%:R : set R^o)%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 => a a0.
+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)) &
+      (fun n => \int[mu]_(z in B k) `|f_ k z - g_ n z|%:E) --> 0 ].
+  apply: approximation_continuous_integrable => //=.
+    by rewrite lebesgue_measure_ball//= ltry.
+  exact: integrableS (intf_ _).
+have 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].
+  move/(@cvgrPdist_le _ [pseudoMetricNormedZmodType R of R^o]).
+  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_Ba n : set _ := [set x | `| (f_ k \- g_B n)%R x |%:E >= (a / 2)%:E].
+pose HL_f_g_Ba n : set _ := [set x | HL_maximal (f_ k \- g_B n)%R x > (a / 2)%:E].
+pose Ea := \bigcap_n (B k `&` (HL_f_g_Ba n `|` f_g_Ba 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.
+  - by apply: measurable_funM => //; exact: continuous_measurable_fun.
+  - exact: openT.
+  - move=> K _ cK.
+    rewrite (@le_lt_trans _ _ (\int[mu]_(x in K) `|g_ n x|%:E))//.
+      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; case: (_ \in _).
+          by rewrite mulr1.
+        by rewrite mulr0 normr0.
+    have : {within K, continuous (g_ n)} by apply: continuous_subspaceT.
+    by move/(continuous_compact_integrable cK) => /integrableP[_ /=].
+have locfg' 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 (HL_f_g_Ba i).
+  rewrite /HL_f_g_Ba -[X in measurable X]setTI.
+  apply: emeasurable_fun_o_infty => //.
+  by apply: measurable_HL_maximal; exact: locfg'.
+have mfga i : measurable (f_g_Ba i).
+  rewrite /f_g_Ba -[X in measurable X]setTI.
+  apply: emeasurable_fun_c_infty => //.
+  by do 2 apply: measurableT_comp => //; case: (locfg' i).
+have ? : measurable Ea.
+  apply: bigcapT_measurable => i.
+  by apply: measurableI; [exact: measurable_ball|exact: measurableU].
+have f_star_Ea : B k `&` [set x | (f_ k)^* x > a%:E] `<=` Ea.
+  suff: forall n, B k `&` [set x | a%:E < (f_ k)^* x] `<=`
+                  B k `&` (HL_f_g_Ba n `|` f_g_Ba n).
+    by move=> suf r /= /suf hr n _; exact: hr.
+  move=> n; rewrite [X in X `<=`_](_ : _ = B k `&`
+      [set x | a%:E < (f_ k \- g_B n)%R^* x]); last first.
+    apply/seteqP; split => [x [Ex] /=|x [Ex] /=].
+      rewrite (@lim_favgB _ (B k)) ?inE//.
+      by move/EFin_measurable_fun : mf; exact: measurable_funS.
+    rewrite (@lim_favgB _ (B k)) ?inE//.
+    by move/EFin_measurable_fun : mf.
+  move=> r /= [Er] afgnr; split => //.
+  have afgnr' := lt_le_trans afgnr (lim_favgT_HL_maximal r (locfg' n)).
+  have [|h] := ltP (a / 2)%:E (HL_maximal (f_ k \- g_B n)%R r); first by left.
+  right.
+  move: afgnr'.
+  rewrite {1}(splitr a) EFinD -lte_subr_addl// => /ltW/le_trans; apply.
+  by rewrite lee_subl_addl// lee_add.
+suff: mu Ea = 0 by exists Ea.
+have HL_null n : mu (HL_f_g_Ba n) <= (3%:R / (a / 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 _ _ _ [the measure _ _ of mu] setT h)//=; last first.
+    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).
+  by rewrite -integral_setI_indic//= setTI; exact: ifg_ub.
+have fgn_null n : mu [set x | `|(f_ k \- g_B n) x|%:E >= (a / 2)%:E] <=
+                     (a / 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 _ _ _ [the measure _ _ of mu] _ measurableT
+        (EFin \o (f_ k \- g_B n)%R) (a / 2) id) => //=.
+      by apply: measurableT_comp => //; case: (locfg' n).
+    by rewrite divr_gt0.
+  set h := (fun x => `|(f_ k \- g_ n) x|%:E * (\1_(B k) x)%:E).
+  rewrite (@eq_integral _ _ _ [the measure _ _ of mu] setT h)//=; last first.
+    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).
+  by rewrite -integral_setI_indic//= setTI; exact: ifg_ub.
+apply/eqP; rewrite eq_le measure_ge0 andbT.
+apply/lee_addgt0Pr => e e0; rewrite add0e.
+have incl n : Ea `<=` B k `&` (HL_f_g_Ba n `|` f_g_Ba n).
+  by move=> r; apply.
+near \oo => n.
+rewrite (@le_trans _ _ (mu (B k `&` (HL_f_g_Ba n `|` f_g_Ba n))))//.
+  rewrite le_measure// inE//.
+  apply: measurableI; first exact: measurable_ball.
+  by apply: measurableU => //; [exact: mEHL|exact: mfga].
+rewrite (@le_trans _ _ ((4 / (a / 2))%:E * n.+1%:R^-1%:E))//.
+  rewrite (@le_trans _ _ (mu (HL_f_g_Ba n `|` f_g_Ba n)))//.
+    rewrite le_measure// inE//.
+      apply: measurableI => //.
+      by apply: measurableU => //; [exact: mEHL|exact: mfga].
+    by apply: measurableU => //; [exact: mEHL|exact: mfga].
+  rewrite (le_trans (measureU2 _ _ _))//=.
+  - exact: mEHL.
+  - exact: mfga.
+  - apply: le_trans.
+      by apply: lee_add; [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 _ e).
+rewrite -invrM ?unitfE ?gt_eqF ?invr_gt0 ?divr_gt0//.
+rewrite lef_pinv ?posrE ?mulr_gt0 ?invr_gt0 ?divr_gt0//.
+rewrite -(natr1 _ n) -ler_subl_addr.
+by near: n; exact: nbhs_pinfty_ge_nat.
+Unshelve. all: by end_near. Qed.
+
+Lemma lebesgue_differentiation (f : R -> R) : 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 _ _ _ [the measure _ _ of 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 : set R^o) 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)// -ler_subr_addr.
+    rewrite (le_trans (ler_norm _))// (le_trans (ltW yk1))// -ler_subl_addr.
+    rewrite opprK -ler_subr_addl.
+    rewrite -natrB//; last by rewrite -addnn addSnnS ltn_addl.
+    by rewrite (le_trans (ltW r1))// -addnn addnK// ler1n.
+  rewrite -opprB ltr_oppl in xrt.
+  rewrite ltr0_norm// (lt_le_trans xrt)// ler_subl_addl (le_trans (ltW r1))//.
+  rewrite -ler_subl_addl addrC -ler_subr_addr (le_trans (ler_norm _))//.
+  rewrite -normrN in yk1.
+  rewrite (le_trans (ltW yk1))// -ler_subl_addr opprK -ler_subr_addl.
+  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 _))// ltr_nat.
+  by rewrite -addnn addSnnS ltn_addl.
+move/(_ Bxx)/fine_cvgP => -[favg_fk_fin_num favg_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 _))//.
+    by rewrite -[in ltRHS]natr1 ltr_addl.
+  rewrite -(fE x _ t)//; last first.
+    by apply: ballxx; near: t; exact: nbhs_right_gt.
+  rewrite /ball/= sub0r normrN (le_lt_trans (abs_ceil _))//.
+  by rewrite -[in ltRHS]natr1 ltr_addl.
+apply/fine_cvgP; split=> [{favg_fk0}|{favg_fk_fin_num}].
+- move: favg_fk_fin_num => -[M /= M0] favg_fk_fin_num.
+  apply: filter_app f_fk_ceil; near=> t; move=> Ht.
+  by rewrite /favg /iavg Ht favg_fk_fin_num//= sub0r normrN gtr0_norm.
+- move/(@cvgrPdist_le _ [pseudoMetricNormedZmodType R of R^o]) in favg_fk0.
+  apply/(@cvgrPdist_le _ [pseudoMetricNormedZmodType R of R^o]) => e e0.
+  have [M /= M0 {}favg_fk0] := favg_fk0 _ e0.
+  apply: filter_app f_fk_ceil; near=> t; move=> Ht.
+  by rewrite /favg /iavg Ht// favg_fk0//= sub0r normrN gtr0_norm.
+Unshelve. all: by end_near. Qed.
+
+End lebesgue_differentiation.
+
+Section regular_cvg.
+Context {R : realType}.
+Implicit Types (x : R) (E : (set R)^nat).
+
+Definition regular_cvg x E :=
+  (forall n, measurable (E n)) /\
+  exists Cr : R * {posnum R}^nat, [/\ Cr.1 > 0,
+    (Cr.2 n)%:num @[n --> \oo] --> (0:R)%R,
+    (forall n, E n `<=` ball x (Cr.2 n)%:num) &
+    (forall n, (lebesgue_measure (ball x (Cr.2 n)%:num) <=
+               Cr.1%:E * lebesgue_measure (E n)))%E].
+
+Lemma regular_cvg_gt0 x E : regular_cvg x E ->
+  forall n, (0 < lebesgue_measure (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 regular_cvg_lty x E : regular_cvg x E ->
+  forall n, (lebesgue_measure (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)))//.
+  rewrite le_measure// inE.
+  exact: mE.
+  exact: measurable_ball.
+by rewrite lebesgue_measure_ball// ltry.
+Qed.
+
+End regular_cvg.
+
+Section regular_lebesgue_differentiation.
+Context {R : realType}.
+Let mu := @lebesgue_measure R.
+Variable E : R -> (set R)^nat.
+Hypothesis hE : forall x, regular_cvg x (E x).
+Local Open Scope ereal_scope.
+
+Lemma regular_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 => //=; 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 * favg 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// (regular_cvg_lty (hE x)).
+    rewrite -EFinM mulVf ?mulr1// neq_lt fine_gt0 ?orbT//.
+    by rewrite (regular_cvg_gt0 (hE x))//= (regular_cvg_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 (regular_cvg_lty (hE x)).
+    by rewrite (regular_cvg_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]_(x0 in closed_ball x (r_ x n)%:num) `|(f x0)%:E|))//.
+      apply: subset_integral => //.
+      + exact: (hE _).1.
+      + exact: measurable_closed_ball.
+      + apply: measurableT_comp => //; apply/EFin_measurable_fun => //.
+        by case: locf => + _ _; exact: measurable_funS.
+      + 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// (regular_cvg_lty (hE x)).
+rewrite muleA lee_pmul//.
+- by rewrite lee_fin invr_ge0// fine_ge0.
+- rewrite -(@invrK _ C) -EFinM -invfM lee_fin lef_pinv//; last 2 first.
+    rewrite posrE fine_gt0// (regular_cvg_gt0 (hE x))//=.
+    by rewrite (regular_cvg_lty (hE x)).
+    rewrite posrE mulr_gt0// ?invr_gt0// fine_gt0//.
+    by rewrite /mu lebesgue_measure_ball// ltry andbT lte_fin mulrn_wgt0.
+  rewrite lter_pdivr_mull // -lee_fin EFinM fineK; last first.
+      by rewrite /mu lebesgue_measure_ball// ltry andbT lte_fin mulrn_wgt0.
+  rewrite fineK; last by rewrite ge0_fin_numE// (regular_cvg_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 regular_lebesgue_differentiation.
+
+Require Import derive.
+
+Section FTC.
+Context {R : realType}.
+Let mu := @lebesgue_measure R.
+Local Open Scope ereal_scope.
+
+Let FTC0 (f : R -> R) : mu.-integrable setT (EFin \o f) ->
+  let F x := (\int[mu]_(t in `]-oo, x]) f t)%R in
+  forall 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 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 /mu lebesgue_measure_itv/= lte_fin ltr_addl d_gt0.
+    by rewrite -EFinD addrAC subrr add0r.
+  have reg_cvg_E y : regular_cvg 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)// ltr_subl_addr ltr_addl.
+    rewrite (lebesgue_measure_ball _ (ltW _))// -/mu muE -EFinM lee_fin.
+    by rewrite mulr_natl.
+  have K n : \int[mu]_(t in `]-oo, (x + d n)%R]) (f t)%:E -
+             \int[mu]_(t in `]-oo, x]) (f t)%:E =
+             \int[mu]_(y in E x n) (f y)%:E.
+    rewrite -[in LHS]integral_itv_bndo_bndc//=; last first.
+      by case: locf.
+    rewrite (_ : `]-oo, (x + d n)%R[ = `]-oo, x[ `|` E x n)%classic; last first.
+      apply/seteqP; split => [y|y] /=.
+        rewrite /E/= !in_itv/= => ->; rewrite andbT leNgt.
+        by apply/orP; rewrite orbN.
+      rewrite /E/= !in_itv/= => -[K1(*TODO: rename*)|/andP[_ ->//]].
+      by rewrite (lt_le_trans K1)// ler_addl ltW.
+    rewrite integral_setU_EFin//=.
+    - rewrite addeAC.
+      rewrite -[X in _ - X]integral_itv_bndo_bndc//=; last first.
+        by case: locf.
+      rewrite subee ?add0e//.
+      by apply: integral_fune_fin_num => //; exact: integrableS intf.
+    - exact: (reg_cvg_E _).1.
+    - by case: locf => + _ _; exact: measurable_funS.
+    - apply/disj_setPRL => z/=.
+      rewrite /E /= !in_itv/= => /andP[].
+      by rewrite leNgt => /negP.
+  rewrite [f in f n @[n --> \oo] --> _](_ : _ =
+      fun n => (d n)^-1 *:
+               ((fine (\int[mu]_(t in E x n) (f t)%:E)) : R^o)); last first.
+    apply/funext => n; congr (_ *: _).
+    rewrite -fineB; last 2 first.
+      by apply: integral_fune_fin_num => //; exact: integrableS intf.
+      by apply: integral_fune_fin_num => //; exact: integrableS intf.
+    by rewrite addrC K.
+  have := regular_lebesgue_differentiation reg_cvg_E locf fx.
+  rewrite {K} -/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 _ => Hg.
+  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 => //.
+    exact: (reg_cvg_E _).1.
+  by apply: integrableS intf => //; exact: (reg_cvg_E _).1.
+- apply/cvg_at_leftP => d [d_gt0 d0].
+  have {}d_gt0 : forall n, (0 < - d n)%R by move=> n; rewrite ltr_oppr oppr0.
+  pose E x n := `]x + d n, x]%classic%R.
+  have muE y n : mu (E y n) = (- d n)%:E.
+    rewrite /E /mu lebesgue_measure_itv/= lte_fin -ltr_subr_addr.
+    by rewrite ltr_addl d_gt0 -EFinD opprD addrA subrr add0r.
+  have reg_cvg_E y : regular_cvg y (E y).
+    split=> [n|]; first exact: measurable_itv.
+    exists (2, (fun n => PosNum (d_gt0 n))); split => //=.
+      rewrite -oppr0.
+      exact: (@cvgN _ [pseudoMetricNormedZmodType R of R^o]).
+    move=> n z.
+      rewrite /E/= in_itv/= /ball/= => /andP[yz zy].
+      by rewrite ltr_distlC opprK yz /= (le_lt_trans zy)// ltr_addl.
+    move=> n.
+    rewrite lebesgue_measure_ball//; last exact: ltW.
+    by rewrite -/mu muE -EFinM lee_fin mulr_natl.
+  have K n : \int[mu]_(t in `]-oo, (x + d n)%R]) (f t)%:E -
+             \int[mu]_(t in `]-oo, x]) (f t)%:E =
+             - \int[mu]_(y in E x n) (f y)%:E.
+    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[] //].
+      move=> /le_trans; apply; rewrite -ler_subr_addl subrr ltW//.
+      by rewrite -oppr0 -ltr_oppr.
+    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: (reg_cvg_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.
+  rewrite [f in f n @[n --> \oo] --> _](_ : _ =
+      fun n => ((d n)^-1) *
+               - fine (\int[mu]_(y in E x n) (f y)%:E))%R; last first.
+    apply/funext => n.
+    rewrite -fineB; last 2 first.
+      by apply: integral_fune_fin_num => //; exact: integrableS intf.
+      by apply: integral_fune_fin_num => //; exact: integrableS intf.
+    by rewrite addrC K// fineN.
+  rewrite {K}.
+  have := regular_lebesgue_differentiation reg_cvg_E locf fx.
+  rewrite -/mu.
+  move/fine_cvgP => [_ /=].
+  (* TODO: use eq_cvg *)
+  set g := _ \o _ => Hg.
+  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: (reg_cvg_E _).1.
+    by apply: integrableS intf => //; exact: (reg_cvg_E _).1.
+  by rewrite muE/= invrN mulNr -mulrN.
+Qed.
+
+Lemma FTC1 (f : R -> R) : mu.-integrable setT (EFin \o f) ->
+  let F x := (\int[mu]_(t in `]-oo, x]) (f t))%R in
+  forall 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 fx; split.
+  apply/cvg_ex; exists (f x).
+  set g := (f in f n @[n --> _] --> _).
+  have := FTC0 intf 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 FTC'.
+Context {R : realType}.
+Let mu := @lebesgue_measure R.
+Local Open Scope ereal_scope.
+
+Let FTC0 (f : R -> R) (a : R) : locally_integrable setT f ->
+  let F x := (\int[mu]_(t in `[a, x]) f t)%R in
+  forall x, (a < x)%R -> lebesgue_pt f x ->
+    h^-1 *: ((F (h + x)%R - F x) : R^o)%R @[h --> (0:R)%R^'] --> f x.
+Proof.
+move=> locf F x ax fx; case: (locf) => mf _ intf.
+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 /mu lebesgue_measure_itv/= lte_fin ltr_addl d_gt0.
+    by rewrite -EFinD addrAC subrr add0r.
+  have reg_cvg_E y : regular_cvg 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)// ltr_subl_addr ltr_addl.
+    rewrite (lebesgue_measure_ball _ (ltW _))// -/mu muE -EFinM lee_fin.
+    by rewrite mulr_natl.
+  have K n : \int[mu]_(t in `[a, (x + d n)%R]) (f t)%:E -
+             \int[mu]_(t in `[a, x]) (f t)%:E =
+             \int[mu]_(y in E x n) (f y)%:E.
+    rewrite -[in LHS]integral_itv_bndo_bndc//= -/mu.
+    rewrite (_ : `[a, (x + d n)%R[ = `[a, x[ `|` E x n)%classic; last first.
+      apply/seteqP; split => [y|y] /=.
+        rewrite /E/= !in_itv/= => /andP[->/= yxdn].
+        by have [|/=] := ltP y x; [left|right].
+      rewrite /E/= !in_itv/= => -[/andP[ay yx]|/andP[xy yxd]].
+        by rewrite ay/= (lt_trans yx)// ltr_addl.
+      by rewrite yxd andbT (le_trans (ltW ax)).
+    rewrite integral_setU_EFin//=.
+    - rewrite addeAC.
+      rewrite -[X in _ - X]integral_itv_bndo_bndc//.
+      rewrite subee ?add0e// integral_itv_bndo_bndc//.
+      apply: integral_fune_fin_num => //=.
+      apply/integrableP; split.
+        by apply/EFin_measurable_fun; exact: measurable_funS mf.
+      apply: intf => //.
+      exact: segment_compact.
+    - exact: (reg_cvg_E _).1.
+    - exact: measurable_funS mf.
+    - apply/disj_setPRL => z/=.
+      rewrite /E /= !in_itv/= => /andP[xz zxd].
+      by apply/negP; rewrite negb_and -leNgt xz orbT.
+  rewrite [f in f n @[n --> \oo] --> _](_ : _ =
+      fun n => (d n)^-1 *:
+               ((fine (\int[mu]_(t in E x n) (f t)%:E)) : R^o)); last first.
+    apply/funext => n; congr (_ *: _).
+    rewrite -fineB/=; last 2 first.
+      apply: integral_fune_fin_num => //=.
+      apply/integrableP; split.
+        by apply/EFin_measurable_fun; exact: measurable_funS mf.
+      by apply: intf => //; exact: segment_compact.
+      apply: integral_fune_fin_num => //=.
+      apply/integrableP; split.
+        by apply/EFin_measurable_fun; exact: measurable_funS mf.
+      by apply: intf => //; exact: segment_compact.
+    by rewrite addrC K.
+  have := regular_lebesgue_differentiation reg_cvg_E locf fx.
+  rewrite {K} -/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 _ => Hg.
+  set h := (f in f n @[n --> \oo] --> _).
+  suff : g = h by move=> <-.
+  apply/funext => n.
+  rewrite /g /h /= fineM//.
+  rewrite /E integral_itv_bndo_bndc//.
+  apply: integral_fune_fin_num => //=.
+  apply/integrableP; split.
+    by apply/EFin_measurable_fun; exact: measurable_funS mf.
+  by apply: intf => //; exact: segment_compact.
+- apply/cvg_at_leftP => d [d_gt0 d0].
+  have {}d_gt0 : forall n, (0 < - d n)%R by move=> n; rewrite ltr_oppr oppr0.
+  pose E x n := `]x + d n, x]%classic%R.
+  have muE y n : mu (E y n) = (- d n)%:E.
+    rewrite /E /mu lebesgue_measure_itv/= lte_fin -ltr_subr_addr.
+    by rewrite ltr_addl d_gt0 -EFinD opprD addrA subrr add0r.
+  have reg_cvg_E y : regular_cvg y (E y).
+    split=> [n|]; first exact: measurable_itv.
+    exists (2, (fun n => PosNum (d_gt0 n))); split => //=.
+      rewrite -oppr0.
+      exact: (@cvgN _ [pseudoMetricNormedZmodType R of R^o]).
+    move=> n z.
+      rewrite /E/= in_itv/= /ball/= => /andP[yz zy].
+      by rewrite ltr_distlC opprK yz /= (le_lt_trans zy)// ltr_addl.
+    move=> n.
+    rewrite lebesgue_measure_ball//; last exact: ltW.
+    by rewrite -/mu muE -EFinM lee_fin mulr_natl.
+  have K : {near \oo, (fun n => \int[mu]_(t in `[a, (x + d n)%R]) (f t)%:E -
+             \int[mu]_(t in `[a, x]) (f t)%:E) =1
+            (fun n => - \int[mu]_(y in E x n) (f y)%:E)}.
+    move/(@cvgrPdist_le _ [pseudoMetricNormedZmodType R of R^o]) : d0.
+    move/(_ (x - a)%R); rewrite subr_gt0 => /(_ ax)[m _ /=] h.
+    near=> n.
+    have mn : (m <= n)%N by near: n; exists m.
+    rewrite (_ : `[a, x] = `[a, (x + d n)%R] `|` E x n)%classic; last first.
+      apply/seteqP; split => [y|y] /=.
+        rewrite /E/= !in_itv/= => /andP[ay yx].
+        rewrite ay/= yx andbT.
+        by have [|] := leP y (x + d n)%R; [left|right].
+      rewrite /E/= !in_itv/= => -[/andP[ay yxd]|/andP[xdy yx]].
+        rewrite ay/= (le_trans yxd)// -ler_subr_addl subrr ltW//.
+        by rewrite -oppr0 -ltr_oppr.
+      rewrite yx andbT.
+      have := h _ mn; rewrite sub0r gtr0_norm//.
+      rewrite ler_subr_addl ler_subl_addr => /le_trans; apply.
+      exact: ltW.
+    rewrite integral_setU_EFin//=.
+    - rewrite oppeD//; last first.
+        rewrite fin_num_adde_defr//.
+        apply: integral_fune_fin_num => //=.
+        apply/integrableP; split.
+          by apply/EFin_measurable_fun; exact: measurable_funS mf.
+        by apply: intf => //; exact: segment_compact.
+      rewrite addeA subee; last first.
+        apply: integral_fune_fin_num => //=.
+        apply/integrableP; split.
+          by apply/EFin_measurable_fun; exact: measurable_funS mf.
+        by apply: intf => //; exact: segment_compact.
+      by rewrite add0e.
+    - exact: (reg_cvg_E _).1.
+    - exact: measurable_funS mf.
+    - apply/disj_setPRL => z/=.
+      rewrite /E /= !in_itv/= => /andP[xdz zx].
+      by apply/negP; rewrite negb_and -!ltNge xdz orbT.
+  apply: (@cvg_trans _ (((d n)^-1 * - (fine (\int[mu]_(y in E x n) (f y)%:E)))%R @[n --> \oo])).
+    apply: near_eq_cvg.
+    near=> n.
+    rewrite -fineB; last 2 first.
+      apply: integral_fune_fin_num => //=.
+      apply/integrableP; split.
+        by apply/EFin_measurable_fun; exact: measurable_funS mf.
+      by apply: intf => //; exact: segment_compact.
+      rewrite /=.
+    apply: integral_fune_fin_num => //=.
+    apply/integrableP; split.
+      by apply/EFin_measurable_fun; exact: measurable_funS mf.
+    by apply: intf => //; exact: segment_compact.
+  rewrite addrC/=.
+  transitivity ((d n)^-1 * fine
+    (\int[lebesgue_measure]_(x0 in `[a, (x + d n)%R]) (f x0)%:E -
+     \int[lebesgue_measure]_(x0 in `[a, x]) (f x0)%:E))%R => //.
+  congr *%R.
+  rewrite -fineN.
+  congr fine.
+  apply/esym.
+  by near: n.
+rewrite {K}.
+have := regular_lebesgue_differentiation reg_cvg_E locf fx.
+rewrite -/mu.
+move/fine_cvgP => [_ /=].
+(* TODO: use eq_cvg *)
+set g := _ \o _ => Hg.
+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: (reg_cvg_E _).1.
+  rewrite /=.
+  rewrite /E.
+  apply/integrableP; split.
+    by apply/EFin_measurable_fun; exact: measurable_funS mf.
+  rewrite integral_itv_obnd_cbnd//=; last first.
+    by apply/measurableT_comp => //.
+   by apply: intf => //; exact: segment_compact.
+by rewrite muE/= invrN mulNr -mulrN.
+Unshelve. all: by end_near. Qed.
+
+Lemma FTC1_2 (f : R -> R) (a : R) : locally_integrable setT f ->
+  let F x := (\int[mu]_(t in `[a, x]) (f t))%R in
+  forall x, (a < x)%R -> lebesgue_pt f x ->
+  derivable (F : R^o -> R^o) x 1 /\
+  (F : R -> R^o)^`() x = f x.
+Proof.
+move=> locf F x ax fx; split.
+  apply/cvg_ex; exists (f x).
+  set g := (f in f n @[n --> _] --> _).
+  have := FTC0 locf 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 FTC_example.
+Context {R : realType}.
+Let mu := @lebesgue_measure R.
+
+Definition staircase (r : R) : R := if r <= 0 then 0 else 1.
+
+Lemma integrable_staircase : mu.-integrable setT (EFin \o staircase).
+Proof.
+apply/integrableP; split.
+Abort.
+
+End FTC_example.
+
+Section density.
+Context {R : realType}.
+Let mu := @lebesgue_measure R.
+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 => //.
+move: Ax; rewrite /lebesgue_pt /favg /= -/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 /mu lebesgue_measure_ball// ltry.
+  suff : 0 < mu (ball x a) by move=> ->.
+  by rewrite /mu 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 /mu 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 /mu 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 /mu 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 /mu 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 /mu lebesgue_measure_ball//= ?ltry.
+  by rewrite -EFinM mulVf// /mu 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 e60aacb08a..b82097e6fa 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -6428,7 +6428,7 @@ Qed.
 End center_radius_realFieldType.
 
 Section vitali_lemma_finite.
-Context {R : realType} {I : eqType}.
+Context {R : realType} {I : choiceType}.
 Variable (B : I -> set R).
 Hypothesis is_ballB : forall i, is_ball (B i).
 Hypothesis B_set0 : forall i, B i !=set0.
diff --git a/theories/realfun.v b/theories/realfun.v
index f47a784a48..7ba1d39ca6 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -47,6 +47,9 @@ Notation "'increasing_fun' f" := ({mono f : n m / (n <= m)%O >-> (n <= m)%O})
 Notation "'decreasing_fun' f" := ({mono f : n m / (n <= m)%O >-> (n >= m)%O})
   (at level 10).
 
+Lemma nbhs_dnbhs_neq {R : realFieldType} (p : R) : \forall x \near nbhs p^', x != p.
+Proof. exact: withinT. Qed.
+
 Section fun_cvg.
 
 Section fun_cvg_realFieldType.
@@ -221,7 +224,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.
 
 End cvge_fun_cvg_seq.