diff --git a/src/analysis/fourier/add_circle.lean b/src/analysis/fourier/add_circle.lean
index 0a24bd245014b..fa8ed0c38f94b 100644
--- a/src/analysis/fourier/add_circle.lean
+++ b/src/analysis/fourier/add_circle.lean
@@ -28,8 +28,13 @@ This file contains basic results on Fourier series for functions on the additive
   from `add_circle T` to `ℂ`.
 * `fourier_basis` is the Hilbert basis of `Lp ℂ 2 haar_add_circle` given by the images of the
   monomials `fourier n`.
-* `fourier_coeff f n`, for `f : add_circle T → ℂ`, is the `n`-th Fourier coefficient of `f`
-  (defined as an integral over `add_circle T`).
+* `fourier_coeff f n`, for `f : add_circle T → E` (with `E` a complete normed `ℂ`-vector space), is
+  the `n`-th Fourier coefficient of `f`, defined as an integral over `add_circle T`. The lemma
+  `fourier_coeff_eq_interval_integral` expresses this as an integral over `[a, a + T]` for any real
+  `a`.
+* `fourier_coeff_on`, for `f : ℝ → E` and `a < b` reals, is the `n`-th Fourier
+  coefficient of the unique periodic function of period `b - a` which agrees with `f` on `(a, b]`.
+  The lemma `fourier_coeff_on_eq_integral` expresses this as an integral over `[a, b]`.
 
 ## Main statements
 
@@ -299,8 +304,8 @@ variables {E : Type} [normed_add_comm_group E] [normed_space ℂ E] [complete_sp
 def fourier_coeff (f : add_circle T → E) (n : ℤ) : E :=
 ∫ (t : add_circle T), fourier (-n) t • f t ∂ haar_add_circle
 
-/-- The Fourier coefficients of a function can be computed as an integral
-over `[a, a + T]` for any real `a`. -/
+/-- The Fourier coefficients of a function on `add_circle T` can be computed as an integral
+over `[a, a + T]`, for any real `a`. -/
 lemma fourier_coeff_eq_interval_integral (f : add_circle T → E) (n : ℤ) (a : ℝ) :
   fourier_coeff f n = (1 / T) • ∫ x in a .. a + T, @fourier T (-n) x • f x :=
 begin
@@ -312,6 +317,47 @@ begin
     ←smul_assoc, smul_eq_mul, one_div_mul_cancel hT.out.ne', one_smul],
 end
 
+lemma fourier_coeff.const_smul (f : add_circle T → E) (c : ℂ) (n : ℤ) :
+  fourier_coeff (c • f) n = c • fourier_coeff f n :=
+by simp_rw [fourier_coeff, pi.smul_apply, ←smul_assoc, smul_eq_mul, mul_comm, ←smul_eq_mul,
+  smul_assoc, integral_smul]
+
+lemma fourier_coeff.const_mul (f : add_circle T → ℂ) (c : ℂ) (n : ℤ) :
+  fourier_coeff (λ x, c * f x) n = c * fourier_coeff f n :=
+fourier_coeff.const_smul f c n
+
+omit hT
+
+/-- For a function on `ℝ`, the Fourier coefficients of `f` on `[a, b]` are defined as the
+Fourier coefficients of the unique periodic function agreeing with `f` on `Ioc a b`. -/
+def fourier_coeff_on {a b : ℝ} (hab : a < b) (f : ℝ → E) (n : ℤ) : E :=
+begin
+  haveI := fact.mk (by linarith : 0 < b - a),
+  exact fourier_coeff (add_circle.lift_Ioc (b - a) a f) n
+end
+
+lemma fourier_coeff_on_eq_integral {a b : ℝ} (f : ℝ → E) (n : ℤ) (hab : a < b) :
+  fourier_coeff_on hab f n =
+  (1 / (b - a)) • ∫ x in a ..b, fourier (-n) (x : add_circle (b - a)) • f x :=
+begin
+  rw [fourier_coeff_on, fourier_coeff_eq_interval_integral _ _ a],
+  congr' 1,
+  rw [add_sub, add_sub_cancel'],
+  simp_rw interval_integral.integral_of_le hab.le,
+  refine set_integral_congr measurable_set_Ioc (λ x hx, _),
+  dsimp only,
+  rwa [lift_Ioc_coe_apply],
+  rwa [add_sub, add_sub_cancel'],
+end
+
+lemma fourier_coeff_on.const_smul {a b : ℝ} (f : ℝ → E) (c : ℂ) (n : ℤ) (hab : a < b) :
+  fourier_coeff_on hab (c • f) n = c • fourier_coeff_on hab f n :=
+by apply fourier_coeff.const_smul
+
+lemma fourier_coeff_on.const_mul {a b : ℝ} (f : ℝ → ℂ) (c : ℂ) (n : ℤ) (hab : a < b) :
+  fourier_coeff_on hab (λ x, c * f x) n = c * fourier_coeff_on hab f n :=
+fourier_coeff_on.const_smul _ _ _ _
+
 end fourier_coeff
 
 section fourier_L2
@@ -397,3 +443,72 @@ lemma has_pointwise_sum_fourier_series_of_summable
 end convergence
 
 end scope_hT
+
+
+section deriv
+
+open complex interval_integral
+open_locale interval
+
+variables (T)
+
+lemma has_deriv_at_fourier (n : ℤ) (x : ℝ) : has_deriv_at (λ y:ℝ, fourier n (y : add_circle T))
+  (2 * π * I * n / T * fourier n (x : add_circle T)) x :=
+begin
+  simp_rw [fourier_coe_apply],
+  refine (_ : has_deriv_at (λ y, exp (2 * π * I * n * y / T)) _ _).comp_of_real,
+  rw (λ α β, by ring : ∀ (α β : ℂ), α * exp β = exp β * α),
+  refine (has_deriv_at_exp _).comp x _,
+  convert has_deriv_at_mul_const (2 * ↑π * I * ↑n / T),
+  ext1 y, ring,
+end
+
+lemma has_deriv_at_fourier_neg (n : ℤ) (x : ℝ) :
+  has_deriv_at (λ y:ℝ, fourier (-n) (y : add_circle T))
+  (-2 * π * I * n / T * fourier (-n) (x : add_circle T)) x :=
+by simpa using has_deriv_at_fourier T (-n) x
+
+variables {T}
+
+lemma has_antideriv_at_fourier_neg (hT : fact (0 < T)) {n : ℤ} (hn : n ≠ 0) (x : ℝ) :
+  has_deriv_at (λ (y : ℝ), (T : ℂ) / (-2 * π * I * n) * fourier (-n) (y : add_circle T))
+  (fourier (-n) (x : add_circle T)) x :=
+begin
+  convert (has_deriv_at_fourier_neg T n x).div_const (-2 * π * I * n / T) using 1,
+  { ext1 y, rw div_div_eq_mul_div, ring, },
+  { rw mul_div_cancel_left,
+    simp only [ne.def, div_eq_zero_iff, neg_eq_zero, mul_eq_zero, bit0_eq_zero, one_ne_zero,
+      of_real_eq_zero, false_or, int.cast_eq_zero, not_or_distrib],
+    exact ⟨⟨⟨real.pi_ne_zero, I_ne_zero⟩, hn⟩, hT.out.ne'⟩ },
+end
+
+/-- Express Fourier coefficients of `f` on an interval in terms of those of its derivative. -/
+lemma fourier_coeff_on_of_has_deriv_at {a b : ℝ} (hab : a < b) {f f' : ℝ → ℂ} {n : ℤ}
+  (hn : n ≠ 0) (hf : ∀ x, x ∈ [a, b] → has_deriv_at f (f' x) x)
+  (hf' : interval_integrable f' volume a b) :
+  fourier_coeff_on hab f n =
+  1 / (-2 * π * I * n) * (fourier (-n) (a : add_circle (b - a)) * (f b - f a)
+    - (b - a) * fourier_coeff_on hab f' n) :=
+begin
+  rw ←of_real_sub,
+  have hT : fact (0 < b - a) := ⟨by linarith⟩,
+  simp_rw [fourier_coeff_on_eq_integral, smul_eq_mul, real_smul, of_real_div, of_real_one],
+  conv { for (fourier _ _ * _) [1, 2, 3] { rw mul_comm } },
+  rw integral_mul_deriv_eq_deriv_mul hf (λ x hx, has_antideriv_at_fourier_neg hT hn x) hf'
+    (((map_continuous (fourier (-n))).comp (add_circle.continuous_mk' _)).interval_integrable _ _),
+  dsimp only,
+  have : ∀ (u v w : ℂ), u * ( (b - a : ℝ) / v * w) = (b - a : ℝ) / v * (u * w) := by {intros, ring},
+  conv in (interval_integral _ _ _ _) { congr, funext, rw this, },
+  rw (by ring : ((b - a : ℝ) : ℂ) / ((-2) * π * I * n)
+    = ((b - a : ℝ) : ℂ) * (1 / ((-2) * π * I * n))),
+  have s2 : (b : add_circle (b - a)) = (a : add_circle (b - a)),
+  { simpa using coe_add_period (b - a) a, },
+  rw [s2, integral_const_mul, ←sub_mul, mul_sub, mul_sub],
+  congr' 1,
+  { conv_lhs {rw [mul_comm, mul_div, mul_one]},
+    rw [div_eq_iff (of_real_ne_zero.mpr hT.out.ne')],
+    ring, },
+  { ring, },
+end
+
+end deriv
diff --git a/src/data/real/basic.lean b/src/data/real/basic.lean
index 8117c41595b3b..76aa36a70ac09 100644
--- a/src/data/real/basic.lean
+++ b/src/data/real/basic.lean
@@ -237,6 +237,8 @@ end
 protected theorem zero_lt_one : (0 : ℝ) < 1 :=
 by convert rat_cast_lt.2 zero_lt_one; simp [←of_cauchy_rat_cast, of_cauchy_one, of_cauchy_zero]
 
+protected lemma fact_zero_lt_one : fact ((0 : ℝ) < 1) := ⟨real.zero_lt_one⟩
+
 protected theorem mul_pos {a b : ℝ} : 0 < a → 0 < b → 0 < a * b :=
 begin
   induction a using real.ind_mk with a,
diff --git a/src/geometry/manifold/instances/real.lean b/src/geometry/manifold/instances/real.lean
index 65f01d24a5f95..533dcf5c7af9a 100644
--- a/src/geometry/manifold/instances/real.lean
+++ b/src/geometry/manifold/instances/real.lean
@@ -303,9 +303,7 @@ end
 /-! Register the manifold structure on `Icc 0 1`, and also its zero and one. -/
 section
 
-lemma fact_zero_lt_one : fact ((0 : ℝ) < 1) := ⟨zero_lt_one⟩
-
-local attribute [instance] fact_zero_lt_one
+local attribute [instance] real.fact_zero_lt_one
 
 instance : charted_space (euclidean_half_space 1) (Icc (0 : ℝ) 1) := by apply_instance
 instance : smooth_manifold_with_corners (𝓡∂ 1) (Icc (0 : ℝ) 1) := by apply_instance
diff --git a/src/measure_theory/integral/periodic.lean b/src/measure_theory/integral/periodic.lean
index 9f84cf6475e36..f1f77629745cc 100644
--- a/src/measure_theory/integral/periodic.lean
+++ b/src/measure_theory/integral/periodic.lean
@@ -188,8 +188,7 @@ end
 end add_circle
 
 namespace unit_add_circle
-private lemma fact_zero_lt_one : fact ((0:ℝ) < 1) := ⟨zero_lt_one⟩
-local attribute [instance] fact_zero_lt_one
+local attribute [instance] real.fact_zero_lt_one
 
 noncomputable instance measure_space : measure_space unit_add_circle := add_circle.measure_space 1
 
diff --git a/src/number_theory/well_approximable.lean b/src/number_theory/well_approximable.lean
index 69255ac38e2c6..621d66baf8be1 100644
--- a/src/number_theory/well_approximable.lean
+++ b/src/number_theory/well_approximable.lean
@@ -156,7 +156,7 @@ lemma mem_approx_add_order_of_iff {δ : ℝ} {x : unit_add_circle} {n : ℕ} (hn
   x ∈ approx_add_order_of unit_add_circle n δ ↔
   ∃ m < n, gcd m n = 1 ∧ ‖x - ↑((m : ℝ) / n)‖ < δ :=
 begin
-  haveI : fact ((0 : ℝ) < 1) := ⟨zero_lt_one⟩,
+  haveI := real.fact_zero_lt_one,
   simp only [mem_approx_add_order_of_iff, mem_set_of_eq, ball, exists_prop, dist_eq_norm,
     add_circle.add_order_of_eq_pos_iff hn, mul_one],
   split,
diff --git a/src/number_theory/zeta_values.lean b/src/number_theory/zeta_values.lean
new file mode 100644
index 0000000000000..6484074af7da9
--- /dev/null
+++ b/src/number_theory/zeta_values.lean
@@ -0,0 +1,136 @@
+/-
+Copyright (c) 2022 David Loeffler. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Loeffler
+-/
+
+import number_theory.bernoulli_polynomials
+import analysis.special_functions.integrals
+import measure_theory.integral.interval_integral
+import analysis.fourier.add_circle
+
+/-!
+# Critical values of the Riemann zeta function
+
+In this file we evaluate the Fourier coefficients of Bernoulli polynomials on the interval `[0, 1]`.
+In a future iteration this will be used to evaluate critical values of the Riemann zeta function
+(and other Dirichlet L-functions).
+-/
+
+noncomputable theory
+open_locale nat real interval
+open complex measure_theory set interval_integral
+
+section bernoulli_fun_props
+/-! Simple properties of the Bernoulli polynomial, as a function `ℝ → ℝ`. -/
+
+/-- The function `x ↦ Bₖ(x) : ℝ → ℝ`. -/
+def bernoulli_fun (k : ℕ) (x : ℝ) : ℝ :=
+(polynomial.map (algebra_map ℚ ℝ) (polynomial.bernoulli k)).eval x
+
+lemma bernoulli_fun_eval_zero (k : ℕ) : bernoulli_fun k 0 = bernoulli k :=
+by rw [bernoulli_fun, polynomial.eval_zero_map, polynomial.bernoulli_eval_zero, eq_rat_cast]
+
+lemma bernoulli_fun_endpoints_eq_of_ne_one {k : ℕ} (hk : k ≠ 1) :
+  bernoulli_fun k 1 = bernoulli_fun k 0 :=
+by rw [bernoulli_fun_eval_zero, bernoulli_fun, polynomial.eval_one_map,
+  polynomial.bernoulli_eval_one, bernoulli_eq_bernoulli'_of_ne_one hk, eq_rat_cast]
+
+lemma bernoulli_fun_eval_one (k : ℕ) : bernoulli_fun k 1 = bernoulli_fun k 0 + ite (k = 1) 1 0 :=
+begin
+  rw [bernoulli_fun, bernoulli_fun_eval_zero, polynomial.eval_one_map,
+    polynomial.bernoulli_eval_one],
+  split_ifs,
+  { rw [h, bernoulli_one, bernoulli'_one, eq_rat_cast],
+    push_cast, ring },
+  { rw [bernoulli_eq_bernoulli'_of_ne_one h, add_zero, eq_rat_cast], }
+end
+
+lemma has_deriv_at_bernoulli_fun (k : ℕ) (x : ℝ) :
+  has_deriv_at (bernoulli_fun k) (k * bernoulli_fun (k - 1) x) x :=
+begin
+  convert ((polynomial.bernoulli k).map $ algebra_map ℚ ℝ).has_deriv_at x using 1,
+  simp only [bernoulli_fun, polynomial.derivative_map, polynomial.derivative_bernoulli k,
+    polynomial.map_mul, polynomial.map_nat_cast, polynomial.eval_mul, polynomial.eval_nat_cast],
+end
+
+lemma antideriv_bernoulli_fun (k : ℕ) (x : ℝ) :
+  has_deriv_at (λ x, (bernoulli_fun (k + 1) x) / (k + 1)) (bernoulli_fun k x) x :=
+begin
+  convert (has_deriv_at_bernoulli_fun (k + 1) x).div_const _,
+  field_simp [nat.cast_add_one_ne_zero k],
+  ring,
+end
+
+lemma integral_bernoulli_fun_eq_zero {k : ℕ} (hk : k ≠ 0) :
+  ∫ (x : ℝ) in 0..1, bernoulli_fun k x = 0 :=
+begin
+  rw integral_eq_sub_of_has_deriv_at (λ x hx, antideriv_bernoulli_fun k x)
+    ((polynomial.continuous _).interval_integrable _ _),
+  dsimp only,
+  rw bernoulli_fun_eval_one,
+  split_ifs,
+  { exfalso, exact hk (nat.succ_inj'.mp h), }, { simp },
+end
+
+end bernoulli_fun_props
+
+section bernoulli_fourier_coeffs
+/-! Compute the Fourier coefficients of the Bernoulli functions via integration by parts. -/
+
+local attribute [instance] real.fact_zero_lt_one
+
+/-- The `n`-th Fourier coefficient of the `k`-th Bernoulli function on the interval `[0, 1]`. -/
+def bernoulli_fourier_coeff (k : ℕ) (n : ℤ) : ℂ :=
+fourier_coeff_on zero_lt_one (λ x, bernoulli_fun k x) n
+
+/-- Recurrence relation (in `k`) for the `n`-th Fourier coefficient of `Bₖ`. -/
+lemma bernoulli_fourier_coeff_recurrence (k : ℕ) {n : ℤ} (hn : n ≠ 0) :
+  bernoulli_fourier_coeff k n = 1 / ((-2) * π * I * n) *
+  (ite (k = 1) 1 0 - k * bernoulli_fourier_coeff (k - 1) n) :=
+begin
+  unfold bernoulli_fourier_coeff,
+  rw [fourier_coeff_on_of_has_deriv_at zero_lt_one
+    hn (λ x hx, (has_deriv_at_bernoulli_fun k x).of_real_comp)
+    ((continuous_of_real.comp $ continuous_const.mul
+      $ polynomial.continuous _).interval_integrable _ _)],
+  dsimp only,
+  simp_rw [of_real_one, of_real_zero, sub_zero, one_mul],
+  rw [quotient_add_group.coe_zero, fourier_eval_zero, one_mul,
+    ←of_real_sub, bernoulli_fun_eval_one, add_sub_cancel'],
+  congr' 2,
+  { split_ifs, all_goals { simp only [of_real_one, of_real_zero, one_mul]}, },
+  { simp_rw [of_real_mul, of_real_nat_cast, fourier_coeff_on.const_mul] },
+end
+
+/-- The Fourier coefficients of `B₀(x) = 1`. -/
+lemma bernoulli_zero_fourier_coeff {n : ℤ} (hn : n ≠ 0) : bernoulli_fourier_coeff 0 n = 0 :=
+by simpa using bernoulli_fourier_coeff_recurrence 0 hn
+
+/-- The `0`-th Fourier coefficient of `Bₖ(x)`. -/
+lemma bernoulli_fourier_coeff_zero {k : ℕ} (hk : k ≠ 0) : bernoulli_fourier_coeff k 0 = 0 :=
+by simp_rw [bernoulli_fourier_coeff, fourier_coeff_on_eq_integral, neg_zero, fourier_zero, sub_zero,
+  div_one, one_smul, interval_integral.integral_of_real, integral_bernoulli_fun_eq_zero hk,
+  of_real_zero]
+
+lemma bernoulli_fourier_coeff_eq {k : ℕ} (hk : k ≠ 0) (n : ℤ) :
+  bernoulli_fourier_coeff k n = - k! / (2 * π * I * n) ^ k :=
+begin
+  rcases eq_or_ne n 0 with rfl|hn,
+  { rw [bernoulli_fourier_coeff_zero hk, int.cast_zero, mul_zero,
+    zero_pow' _ hk, div_zero] },
+  refine nat.le_induction _ (λ k hk h'k, _) k (nat.one_le_iff_ne_zero.mpr hk),
+  { rw bernoulli_fourier_coeff_recurrence 1 hn,
+    simp only [nat.cast_one, tsub_self, neg_mul, one_mul, eq_self_iff_true, if_true,
+      nat.factorial_one, pow_one, inv_I, mul_neg],
+    rw [bernoulli_zero_fourier_coeff hn, sub_zero, mul_one, div_neg, neg_div], },
+  { rw [bernoulli_fourier_coeff_recurrence (k + 1) hn, nat.add_sub_cancel k 1],
+    split_ifs,
+    { exfalso, exact (ne_of_gt (nat.lt_succ_iff.mpr hk)) h,},
+    { rw [h'k, nat.factorial_succ, zero_sub, nat.cast_mul, pow_add, pow_one, neg_div,
+        mul_neg, mul_neg, mul_neg, neg_neg, neg_mul, neg_mul, neg_mul, div_neg],
+      field_simp [int.cast_ne_zero.mpr hn, I_ne_zero],
+      ring_nf, } }
+end
+
+end bernoulli_fourier_coeffs
diff --git a/src/topology/instances/add_circle.lean b/src/topology/instances/add_circle.lean
index 7049ede5b7f5e..a67ddcb2eb982 100644
--- a/src/topology/instances/add_circle.lean
+++ b/src/topology/instances/add_circle.lean
@@ -447,8 +447,7 @@ instance : second_countable_topology (add_circle p) := quotient_add_group.second
 
 end add_circle
 
-private lemma fact_zero_lt_one : fact ((0:ℝ) < 1) := ⟨zero_lt_one⟩
-local attribute [instance] fact_zero_lt_one
+local attribute [instance] real.fact_zero_lt_one
 
 /-- The unit circle `ℝ ⧸ ℤ`. -/
 @[derive [compact_space, normal_space, second_countable_topology]]