diff --git a/src/measure_theory/covering/density_theorem.lean b/src/measure_theory/covering/density_theorem.lean
index cd4078adfa1b8..cd37a11be4cb2 100644
--- a/src/measure_theory/covering/density_theorem.lean
+++ b/src/measure_theory/covering/density_theorem.lean
@@ -134,12 +134,15 @@ end
 
 end
 
-/-- A version of *Lebesgue's density theorem* for a sequence of closed balls whose centres are
+section applications
+variables [sigma_compact_space α] [borel_space α] [is_locally_finite_measure μ]
+  {E : Type*} [normed_add_comm_group E]
+
+/-- A version of *Lebesgue's density theorem* for a sequence of closed balls whose centers are
 not required to be fixed.
 
 See also `besicovitch.ae_tendsto_measure_inter_div`. -/
-lemma ae_tendsto_measure_inter_div
-  [sigma_compact_space α] [borel_space α] [is_locally_finite_measure μ] (S : set α) (K : ℝ) :
+lemma ae_tendsto_measure_inter_div (S : set α) (K : ℝ) :
   ∀ᵐ x ∂μ.restrict S, ∀ {ι : Type*} {l : filter ι} (w : ι → α) (δ : ι → ℝ)
     (δlim : tendsto δ l (𝓝[>] 0))
     (xmem : ∀ᶠ j in l, x ∈ closed_ball (w j) (K * δ j)),
@@ -147,4 +150,27 @@ lemma ae_tendsto_measure_inter_div
 by filter_upwards [(vitali_family μ K).ae_tendsto_measure_inter_div S] with x hx ι l w δ δlim xmem
 using hx.comp (tendsto_closed_ball_filter_at μ _ _ δlim xmem)
 
+/-- A version of *Lebesgue differentiation theorem* for a sequence of closed balls whose
+centers are not required to be fixed. -/
+lemma ae_tendsto_average_norm_sub {f : α → E} (hf : integrable f μ) (K : ℝ) :
+  ∀ᵐ x ∂μ, ∀ {ι : Type*} {l : filter ι} (w : ι → α) (δ : ι → ℝ)
+    (δlim : tendsto δ l (𝓝[>] 0))
+    (xmem : ∀ᶠ j in l, x ∈ closed_ball (w j) (K * δ j)),
+    tendsto (λ j, ⨍ y in closed_ball (w j) (δ j), ∥f y - f x∥ ∂μ) l (𝓝 0) :=
+by filter_upwards [(vitali_family μ K).ae_tendsto_average_norm_sub hf] with x hx ι l w δ δlim xmem
+using hx.comp (tendsto_closed_ball_filter_at μ _ _ δlim xmem)
+
+/-- A version of *Lebesgue differentiation theorem* for a sequence of closed balls whose
+centers are not required to be fixed. -/
+lemma ae_tendsto_average [normed_space ℝ E] [complete_space E]
+  {f : α → E} (hf : integrable f μ) (K : ℝ) :
+  ∀ᵐ x ∂μ, ∀ {ι : Type*} {l : filter ι} (w : ι → α) (δ : ι → ℝ)
+    (δlim : tendsto δ l (𝓝[>] 0))
+    (xmem : ∀ᶠ j in l, x ∈ closed_ball (w j) (K * δ j)),
+    tendsto (λ j, ⨍ y in closed_ball (w j) (δ j), f y ∂μ) l (𝓝 (f x)) :=
+by filter_upwards [(vitali_family μ K).ae_tendsto_average hf] with x hx ι l w δ δlim xmem
+using hx.comp (tendsto_closed_ball_filter_at μ _ _ δlim xmem)
+
+end applications
+
 end is_doubling_measure
diff --git a/src/measure_theory/covering/differentiation.lean b/src/measure_theory/covering/differentiation.lean
index c5671d1179530..1eb18552396a9 100644
--- a/src/measure_theory/covering/differentiation.lean
+++ b/src/measure_theory/covering/differentiation.lean
@@ -8,6 +8,8 @@ import measure_theory.measure.regular
 import measure_theory.function.ae_measurable_order
 import measure_theory.integral.lebesgue
 import measure_theory.decomposition.radon_nikodym
+import measure_theory.integral.average
+import measure_theory.function.locally_integrable
 
 /-!
 # Differentiation of measures
@@ -26,6 +28,13 @@ ratio really makes sense.
 For concrete applications, one needs concrete instances of Vitali families, as provided for instance
 by `besicovitch.vitali_family` (for balls) or by `vitali.vitali_family` (for doubling measures).
 
+Specific applications to Lebesgue density points and the Lebesgue differentiation theorem are also
+derived:
+* `vitali_family.ae_tendsto_measure_inter_div` states that, for almost every point `x ∈ s`,
+  then `μ (s ∩ a) / μ a` tends to `1` as `a` shrinks to `x` along a Vitali family.
+* `vitali_family.ae_tendsto_average_norm_sub` states that, for almost every point `x`, then the
+  average of `y ↦ ∥f y - f x∥` on `a` tends to `0` as `a` shrinks to `x` along a Vitali family.
+
 ## Sketch of proof
 
 Let `v` be a Vitali family for `μ`. Assume for simplicity that `ρ` is absolutely continuous with
@@ -60,6 +69,8 @@ local attribute [instance] emetric.second_countable_of_sigma_compact
 
 variables {α : Type*} [metric_space α] {m0 : measurable_space α}
 {μ : measure α} (v : vitali_family μ)
+{E : Type*} [normed_add_comm_group E]
+
 include v
 
 namespace vitali_family
@@ -706,6 +717,8 @@ begin
   { simp only [Bx, zero_add] }
 end
 
+/-! ### Lebesgue density points -/
+
 /-- Given a measurable set `s`, then `μ (s ∩ a) / μ a` converges when `a` shrinks to a typical
 point `x` along a Vitali family. The limit is `1` for `x ∈ s` and `0` for `x ∉ s`. This shows that
 almost every point of `s` is a Lebesgue density point for `s`. A version for non-measurable sets
@@ -745,6 +758,173 @@ begin
   exact measure_to_measurable_inter_of_sigma_finite ha _,
 end
 
+/-! ### Lebesgue differentiation theorem -/
+
+lemma ae_tendsto_lintegral_div' {f : α → ℝ≥0∞} (hf : measurable f) (h'f : ∫⁻ y, f y ∂μ ≠ ∞) :
+  ∀ᵐ x ∂μ, tendsto (λ a, (∫⁻ y in a, f y ∂μ) / μ a) (v.filter_at x) (𝓝 (f x)) :=
+begin
+  let ρ := μ.with_density f,
+  haveI : is_finite_measure ρ, from is_finite_measure_with_density h'f,
+  filter_upwards [ae_tendsto_rn_deriv v ρ, rn_deriv_with_density μ hf] with x hx h'x,
+  rw ← h'x,
+  apply hx.congr' _,
+  filter_upwards [v.eventually_filter_at_measurable_set] with a ha,
+  rw ← with_density_apply f ha,
+end
+
+lemma ae_tendsto_lintegral_div {f : α → ℝ≥0∞} (hf : ae_measurable f μ) (h'f : ∫⁻ y, f y ∂μ ≠ ∞) :
+  ∀ᵐ x ∂μ, tendsto (λ a, (∫⁻ y in a, f y ∂μ) / μ a) (v.filter_at x) (𝓝 (f x)) :=
+begin
+  have A : ∫⁻ y, hf.mk f y ∂μ ≠ ∞,
+  { convert h'f using 1,
+    apply lintegral_congr_ae,
+    exact hf.ae_eq_mk.symm },
+  filter_upwards [v.ae_tendsto_lintegral_div' hf.measurable_mk A, hf.ae_eq_mk] with x hx h'x,
+  rw h'x,
+  convert hx,
+  ext1 a,
+  congr' 1,
+  apply lintegral_congr_ae,
+  exact ae_restrict_of_ae (hf.ae_eq_mk)
+end
+
+lemma ae_tendsto_lintegral_nnnorm_sub_div'
+  {f : α → E} (hf : integrable f μ) (h'f : strongly_measurable f) :
+  ∀ᵐ x ∂μ, tendsto (λ a, (∫⁻ y in a, ∥f y - f x∥₊ ∂μ) / μ a) (v.filter_at x) (𝓝 0) :=
+begin
+  /- For every `c`, then `(∫⁻ y in a, ∥f y - c∥₊ ∂μ) / μ a` tends almost everywhere to `∥f x - c∥`.
+  We apply this to a countable set of `c` which is dense in the range of `f`, to deduce the desired
+  convergence.
+  A minor technical inconvenience is that constants are not integrable, so to apply previous lemmas
+  we need to replace `c` with the restriction of `c` to a finite measure set `A n` in the
+  above sketch. -/
+  let A := measure_theory.measure.finite_spanning_sets_in_open μ,
+  rcases h'f.is_separable_range with ⟨t, t_count, ht⟩,
+  have main : ∀ᵐ x ∂μ, ∀ (n : ℕ) (c : E) (hc : c ∈ t),
+    tendsto (λ a, (∫⁻ y in a, ∥f y - (A.set n).indicator (λ y, c) y∥₊ ∂μ) / μ a)
+    (v.filter_at x) (𝓝 (∥f x - (A.set n).indicator (λ y, c) x∥₊)),
+  { simp_rw [ae_all_iff, ae_ball_iff t_count],
+    assume n c hc,
+    apply ae_tendsto_lintegral_div',
+    { refine (h'f.sub _).ennnorm,
+      exact strongly_measurable_const.indicator (is_open.measurable_set (A.set_mem n)) },
+    { apply ne_of_lt,
+      calc ∫⁻ y, ↑∥f y - (A.set n).indicator (λ (y : α), c) y∥₊ ∂μ
+          ≤ ∫⁻ y, (∥f y∥₊ + ∥(A.set n).indicator (λ (y : α), c) y∥₊) ∂μ :
+        begin
+          apply lintegral_mono,
+          assume x,
+          dsimp,
+          rw ← ennreal.coe_add,
+          exact ennreal.coe_le_coe.2 (nnnorm_sub_le _ _),
+        end
+      ... = ∫⁻ y, ∥f y∥₊ ∂μ + ∫⁻ y, ∥(A.set n).indicator (λ (y : α), c) y∥₊ ∂μ :
+        lintegral_add_left h'f.ennnorm _
+      ... < ∞ + ∞ :
+        begin
+          have I : integrable ((A.set n).indicator (λ (y : α), c)) μ,
+            by simp only [integrable_indicator_iff (is_open.measurable_set (A.set_mem n)),
+              integrable_on_const, A.finite n, or_true],
+          exact ennreal.add_lt_add hf.2 I.2,
+        end } },
+  filter_upwards [main, v.ae_eventually_measure_pos] with x hx h'x,
+  have M : ∀ c ∈ t, tendsto (λ a, (∫⁻ y in a, ∥f y - c∥₊ ∂μ) / μ a)
+    (v.filter_at x) (𝓝 (∥f x - c∥₊)),
+  { assume c hc,
+    obtain ⟨n, xn⟩ : ∃ n, x ∈ A.set n, by simpa [← A.spanning] using mem_univ x,
+    specialize hx n c hc,
+    simp only [xn, indicator_of_mem] at hx,
+    apply hx.congr' _,
+    filter_upwards [v.eventually_filter_at_subset_of_nhds (is_open.mem_nhds (A.set_mem n) xn),
+      v.eventually_filter_at_measurable_set]
+      with a ha h'a,
+    congr' 1,
+    apply set_lintegral_congr_fun h'a,
+    apply eventually_of_forall (λ y, _),
+    assume hy,
+    simp only [ha hy, indicator_of_mem] },
+  apply ennreal.tendsto_nhds_zero.2 (λ ε εpos, _),
+  obtain ⟨c, ct, xc⟩ : ∃ c ∈ t, (∥f x - c∥₊ : ℝ≥0∞) < ε / 2,
+  { simp_rw ← edist_eq_coe_nnnorm_sub,
+    have : f x ∈ closure t, from ht (mem_range_self _),
+    exact emetric.mem_closure_iff.1 this (ε / 2) (ennreal.half_pos (ne_of_gt εpos)) },
+  filter_upwards [(tendsto_order.1 (M c ct)).2 (ε / 2) xc, h'x, v.eventually_measure_lt_top x]
+    with a ha h'a h''a,
+  apply ennreal.div_le_of_le_mul,
+  calc ∫⁻ y in a, ∥f y - f x∥₊ ∂μ
+      ≤ ∫⁻ y in a, ∥f y - c∥₊ + ∥f x - c∥₊ ∂μ :
+    begin
+      apply lintegral_mono (λ x, _),
+      simpa only [← edist_eq_coe_nnnorm_sub] using edist_triangle_right _ _ _,
+    end
+  ... = ∫⁻ y in a, ∥f y - c∥₊ ∂μ + ∫⁻ y in a, ∥f x - c∥₊ ∂μ :
+    lintegral_add_right _ measurable_const
+  ... ≤ ε / 2 * μ a + ε / 2 * μ a :
+    begin
+      refine add_le_add _ _,
+      { rw ennreal.div_lt_iff (or.inl (h'a.ne')) (or.inl (h''a.ne)) at ha,
+        exact ha.le },
+      { simp only [lintegral_const, measure.restrict_apply, measurable_set.univ, univ_inter],
+        exact mul_le_mul_right' xc.le _ }
+    end
+  ... = ε * μ a : by rw [← add_mul, ennreal.add_halves]
+end
+
+lemma ae_tendsto_lintegral_nnnorm_sub_div {f : α → E} (hf : integrable f μ) :
+  ∀ᵐ x ∂μ, tendsto (λ a, (∫⁻ y in a, ∥f y - f x∥₊ ∂μ) / μ a) (v.filter_at x) (𝓝 0) :=
+begin
+  have I : integrable (hf.1.mk f) μ, from hf.congr hf.1.ae_eq_mk,
+  filter_upwards [v.ae_tendsto_lintegral_nnnorm_sub_div' I hf.1.strongly_measurable_mk,
+    hf.1.ae_eq_mk] with x hx h'x,
+  apply hx.congr _,
+  assume a,
+  congr' 1,
+  apply lintegral_congr_ae,
+  apply ae_restrict_of_ae,
+  filter_upwards [hf.1.ae_eq_mk] with y hy,
+  rw [hy, h'x]
+end
+
+/-- *Lebesgue differentiation theorem*: for almost every point `x`, the
+average of `∥f y - f x∥` on `a` tends to `0` as `a` shrinks to `x` along a Vitali family.-/
+lemma ae_tendsto_average_norm_sub {f : α → E} (hf : integrable f μ) :
+  ∀ᵐ x ∂μ, tendsto (λ a, ⨍ y in a, ∥f y - f x∥ ∂μ) (v.filter_at x) (𝓝 0) :=
+begin
+  filter_upwards [v.ae_tendsto_lintegral_nnnorm_sub_div hf, v.ae_eventually_measure_pos]
+    with x hx h'x,
+  have := (ennreal.tendsto_to_real ennreal.zero_ne_top).comp hx,
+  simp only [ennreal.zero_to_real] at this,
+  apply tendsto.congr' _ this,
+  filter_upwards [h'x, v.eventually_measure_lt_top x] with a ha h'a,
+  simp only [function.comp_app, ennreal.to_real_div, set_average_eq, div_eq_inv_mul],
+  have A : integrable_on (λ y, (∥f y - f x∥₊ : ℝ)) a μ,
+  { simp_rw [coe_nnnorm],
+    exact (hf.integrable_on.sub (integrable_on_const.2 (or.inr h'a))).norm },
+  rw [lintegral_coe_eq_integral _ A, ennreal.to_real_of_real],
+  { simp_rw [coe_nnnorm],
+    refl },
+  { apply integral_nonneg,
+    assume x,
+    exact nnreal.coe_nonneg _ }
+end
+
+/-- *Lebesgue differentiation theorem*: for almost every point `x`, the
+average of `f` on `a` tends to `f x` as `a` shrinks to `x` along a Vitali family.-/
+lemma ae_tendsto_average [normed_space ℝ E] [complete_space E] {f : α → E} (hf : integrable f μ) :
+  ∀ᵐ x ∂μ, tendsto (λ a, ⨍ y in a, f y ∂μ) (v.filter_at x) (𝓝 (f x)) :=
+begin
+  filter_upwards [v.ae_tendsto_average_norm_sub hf, v.ae_eventually_measure_pos] with x hx h'x,
+  rw tendsto_iff_norm_tendsto_zero,
+  refine squeeze_zero' (eventually_of_forall (λ a, norm_nonneg _)) _ hx,
+  filter_upwards [h'x, v.eventually_measure_lt_top x] with a ha h'a,
+  nth_rewrite 0 [← set_average_const ha.ne' h'a.ne (f x)],
+  simp_rw [set_average_eq'],
+  rw ← integral_sub,
+  { exact norm_integral_le_integral_norm _ },
+  { exact (integrable_inv_smul_measure ha.ne' h'a.ne).2 hf.integrable_on },
+  { exact (integrable_inv_smul_measure ha.ne' h'a.ne).2 (integrable_on_const.2 (or.inr h'a)) }
+end
+
 end
 
 end vitali_family