Theory Fourier

section‹The basics of Fourier series›

text‹Ported from HOL Light; thanks to Manuel Eberl for help with the real asymp proof methods›

theory "Fourier"
  imports Periodic Square_Integrable "HOL-Real_Asymp.Real_Asymp" Confine Fourier_Aux2
begin

subsection‹Orthonormal system of L2 functions and their Fourier coefficients›

definition orthonormal_system :: "'a::euclidean_space set  ('b  'a  real)  bool"
  where "orthonormal_system S w  m n. l2product S (w m) (w n) = (if m = n then 1 else 0)"

definition orthonormal_coeff :: "'a::euclidean_space set  (nat  'a  real)  ('a  real)  nat  real"
  where "orthonormal_coeff S w f n = l2product S (w n) f"

lemma orthonormal_system_eq: "orthonormal_system S w  l2product S (w m) (w n) = (if m = n then 1 else 0)"
  by (simp add: orthonormal_system_def)

lemma orthonormal_system_l2norm:
   "orthonormal_system S w  l2norm S (w i) = 1"
  by (simp add: l2norm_def orthonormal_system_def)

lemma orthonormal_partial_sum_diff:
  assumes os: "orthonormal_system S w" and w: "i. (w i) square_integrable S"
    and f: "f square_integrable S" and "finite I"
  shows "(l2norm S (λx. f x - (iI. a i * w i x)))2 =
        (l2norm S f)2 + (iI. (a i)2) -  2 * (iI. a i * orthonormal_coeff S w f i)"
proof -
  have "S  sets lebesgue"
    using f square_integrable_def by blast
  then have "(λx. iI. a i * w i x) square_integrable S"
    by (intro square_integrable_sum square_integrable_lmult w finite I)
  with assms show ?thesis
    apply (simp add: l2norm_pow_2 orthonormal_coeff_def orthonormal_system_def)
    apply (simp add: l2product_rdiff l2product_sym
           l2product_rsum l2product_rmult algebra_simps power2_eq_square if_distrib [of "λx. _ * x"])
    done
qed

lemma orthonormal_optimal_partial_sum:
  assumes "orthonormal_system S w" "i. (w i) square_integrable S"
          "f square_integrable S" "finite I"
  shows "l2norm S (λx. f x - (iI. orthonormal_coeff S w f i * w i x))
        l2norm S (λx. f x - (iI. a i * w i x))"
proof -
  have "2 * (a i * l2product S f(w i))  (a i)2 + (l2product S f(w i))2" for i
    using sum_squares_bound [of "a i" "l2product S f(w i)"]
    by (force simp: algebra_simps)
  then have *: "2 * (iI. a i * l2product S f(w i))  (iI. (a i)2 + (l2product S f(w i))2)"
    by (simp add: sum_distrib_left sum_mono)
  have S: "S  sets lebesgue"
    using assms square_integrable_def by blast
  with assms * show ?thesis
    apply (simp add: l2norm_le square_integrable_sum square_integrable_diff square_integrable_lmult flip: l2norm_pow_2)
    apply (simp add: orthonormal_coeff_def orthonormal_partial_sum_diff)
    apply (simp add: l2product_sym power2_eq_square sum.distrib)
    done
qed

lemma Bessel_inequality:
  assumes "orthonormal_system S w" "i. (w i) square_integrable S"
    "f square_integrable S" "finite I"
  shows "(iI. (orthonormal_coeff S w f i)2)  (l2norm S f)2"
  using orthonormal_partial_sum_diff [OF assms, of "orthonormal_coeff S w f"]
  apply (simp add: algebra_simps flip: power2_eq_square)
  by (metis (lifting) add_diff_cancel_left' diff_ge_0_iff_ge zero_le_power2)

lemma Fourier_series_square_summable:
  assumes os: "orthonormal_system S w" and w: "i. (w i) square_integrable S"
    and f: "f square_integrable S"
  shows "summable (confine (λi. (orthonormal_coeff S w f i) ^ 2) I)"
proof -
  have "incseq (λn. iI  {..n}. (orthonormal_coeff S w f i)2)"
    by (auto simp: incseq_def intro: sum_mono2)
  moreover have "i. (iI  {..i}. (orthonormal_coeff S w f i)2)  (l2norm S f)2"
    by (simp add: Bessel_inequality assms)
  ultimately obtain L where "(λn. iI  {..n}. (orthonormal_coeff S w f i)2)  L"
    using incseq_convergent by blast
  then have "r>0. no. nno. ¦(i{..n}  I. (orthonormal_coeff S w f i)2) - L¦ < r"
    by (simp add: LIMSEQ_iff Int_commute)
  then show ?thesis
    by (auto simp: summable_def sums_confine_le LIMSEQ_iff)
qed

lemma orthonormal_Fourier_partial_sum_diff_squared:
  assumes os: "orthonormal_system S w" and w: "i. (w i) square_integrable S"
    and f: "f square_integrable S" and "finite I"
  shows "(l2norm S (λx. f x -(iI. orthonormal_coeff S w f i * w i x)))2 =
         (l2norm S f)2 - (iI. (orthonormal_coeff S w f i)2)"
  using orthonormal_partial_sum_diff [OF assms, where a = "orthonormal_coeff S w f"]
  by (simp add: power2_eq_square)


lemma Fourier_series_l2_summable:
  assumes os: "orthonormal_system S w" and w: "i. (w i) square_integrable S"
    and f: "f square_integrable S"
  obtains g where "g square_integrable S"
                  "(λn. l2norm S (λx. (iI  {..n}. orthonormal_coeff S w f i * w i x) - g x))
                    0"
proof -
  have S: "S  sets lebesgue"
    using f square_integrable_def by blast
  let  = "λA x. (iI  A. orthonormal_coeff S w f i * w i x)"
  let  = "confine (λi. (orthonormal_coeff S w f i)2) I"
  have si: " A square_integrable S" if "finite A" for A
    by (force intro: square_integrable_lmult w square_integrable_sum S that)
  have "N. mN. nN. l2norm S (λx.  {..m} x -  {..n} x) < e"
    if "e > 0" for e
  proof -
    have "summable "
      by (rule Fourier_series_square_summable [OF os w f])
    then have "Cauchy (λn. sum  {..n})"
      by (simp add: summable_def sums_def_le convergent_eq_Cauchy)
    then obtain M where M: "m n. mM; nM  dist (sum  {..m}) (sum  {..n}) < e2"
      using e > 0 unfolding Cauchy_def by (drule_tac x="e^2" in spec) auto
    have "mM; nM  l2norm S (λx.  {..m} x -  {..n} x) < e" for m n
    proof (induct m n rule: linorder_class.linorder_wlog)
      case (le m n)
      have sum_diff: "sum f(I  {..n}) - sum f(I  {..m}) = sum f(I  {Suc m..n})" for f :: "nat  real"
      proof -
        have "(I  {..n}) =  (I  {..m}  I  {Suc m..n})" "(I  {..m})  (I  {Suc m..n}) = {}"
          using le by auto
        then show ?thesis
          by (simp add: algebra_simps flip: sum.union_disjoint)
      qed
      have "(l2norm S (λx.  {..n} x -  {..m} x))^2
             ¦(iI  {..n}. (orthonormal_coeff S w f i)2) - (iI  {..m}. (orthonormal_coeff S w f i)2)¦"
      proof (simp add: sum_diff)
        have "(l2norm S ( {Suc m..n}))2
            = (iI  {Suc m..n}. l2product S (λx. jI  {Suc m..n}. orthonormal_coeff S w f j * w j x)
                                               (λx. orthonormal_coeff S w f i * w i x))"
          by (simp add: l2norm_pow_2 l2product_rsum si w)
        also have " = (iI  {Suc m..n}. jI  {Suc m..n}.
                            orthonormal_coeff S w f j * orthonormal_coeff S w f i * l2product S (w j) (w i))"
          by (simp add: l2product_lsum l2product_lmult l2product_rmult si w flip: mult.assoc)
        also have "  ¦iI  {Suc m..n}. (orthonormal_coeff S w f i)2¦"
          by (simp add: orthonormal_system_eq [OF os] power2_eq_square if_distrib [of "(*)_"] cong: if_cong)
        finally show "(l2norm S ( {Suc m..n}))2  ¦iI  {Suc m..n}. (orthonormal_coeff S w f i)2¦" .
      qed
      also have " < e2"
        using M [OF nM mM]
        by (simp add: dist_real_def sum_confine_eq_Int Int_commute)
      finally have "(l2norm S (λx.  {..m} x -  {..n} x))^2 < e^2"
        using l2norm_diff [OF si si] by simp
      with e > 0 show ?case
        by (simp add: power2_less_imp_less)
    next
      case (sym a b)
      then show ?case
        by (subst l2norm_diff) (auto simp: si)
    qed
    then show ?thesis
      by blast
  qed
  with that show thesis
    by (blast intro: si [of "{.._}"] l2_complete [of "λn.  {..n}"])
qed

lemma Fourier_series_l2_summable_strong:
  assumes os: "orthonormal_system S w" and w: "i. (w i) square_integrable S"
    and f: "f square_integrable S"
  obtains g where "g square_integrable S"
          "i. i  I  orthonormal_coeff S w (λx. f x - g x) i = 0"
          "(λn. l2norm S (λx. (iI  {..n}. orthonormal_coeff S w f i * w i x) - g x))
            0"
proof -
  have S: "S  sets lebesgue"
    using f square_integrable_def by blast
  obtain g where g: "g square_integrable S"
            and teng: "(λn. l2norm S (λx. (iI  {..n}. orthonormal_coeff S w f i * w i x) - g x))
                        0"
    using Fourier_series_l2_summable [OF assms] .
  show thesis
  proof
    show "orthonormal_coeff S w (λx. f x - g x) i = 0"
      if "i  I" for i
    proof (rule tendsto_unique)
      let  = "λA x. (iI  A. orthonormal_coeff S w f i * w i x)"
      let ?f = "λn. l2product S (w i) (λx. (f x -  {..n} x) + ( {..n} x - g x))"
      show "?f  orthonormal_coeff S w (λx. f x - g x) i"
        by (simp add: orthonormal_coeff_def)
      have 1: "(λn. l2product S (w i) (λx. f x -  {..n} x))  0"
        proof (rule tendsto_eventually)
          have "l2product S (w i) (λx. f x -  {..j} x) = 0"
            if "j  i" for j
            using that i  I
            apply (simp add: l2product_rdiff l2product_rsum l2product_rmult orthonormal_coeff_def w f S)
            apply (simp add: orthonormal_system_eq [OF os] if_distrib [of "(*)_"] cong: if_cong)
            done
          then show "F n in sequentially. l2product S (w i) (λx. f x -  {..n} x) = 0"
            using eventually_at_top_linorder by blast
        qed
        have 2: "(λn. l2product S (w i) (λx.  {..n} x - g x))  0"
        proof (intro Lim_null_comparison [OF _ teng] eventuallyI)
          show "norm (l2product S (w i) (λx.  {..n} x - g x))  l2norm S (λx.  {..n} x - g x)" for n
            using Schwartz_inequality_abs [of "w i" S "(λx.  {..n} x - g x)"]
            by (simp add: S g f w orthonormal_system_l2norm [OF os])
        qed
        show "?f  0"
          using that tendsto_add [OF 1 2]
          by (subst l2product_radd) (simp_all add: l2product_radd w f g S)
      qed auto
  qed (auto simp: g teng)
qed


subsection‹Actual trigonometric orthogonality relations›

lemma integrable_sin_cx:
  "integrable (lebesgue_on {-pi..pi}) (λx. sin(x * c))"
  by (intro continuous_imp_integrable_real continuous_intros)

lemma integrable_cos_cx:
  "integrable (lebesgue_on {-pi..pi}) (λx. cos(x * c))"
  by (intro continuous_imp_integrable_real continuous_intros)

lemma integral_cos_Z' [simp]:
  assumes "n  "
  shows "integralL (lebesgue_on {-pi..pi}) (λx. cos(n * x)) = (if n = 0 then 2 * pi else 0)"
  by (metis assms integral_cos_Z mult_commute_abs)

lemma integral_sin_and_cos:
  fixes m n::int
  shows
  "integralL (lebesgue_on {-pi..pi}) (λx. cos(m * x) * cos(n * x)) = (if ¦m¦ = ¦n¦ then if n = 0 then 2 * pi else pi else 0)"
  "integralL (lebesgue_on {-pi..pi}) (λx. cos(m * x) * sin(n * x)) = 0"
  "integralL (lebesgue_on {-pi..pi}) (λx. sin(m * x) * cos(n * x)) = 0"
  "m  0; n  0  integralL (lebesgue_on {-pi..pi}) (λx. sin (m * x) * sin (n * x)) = (if m = n  n  0 then pi else 0)"
  "¦integralL (lebesgue_on {-pi..pi}) (λx. sin (m * x) * sin (n * x))¦ = (if ¦m¦ = ¦n¦  n  0 then pi else 0)"
  by (simp_all add: abs_if sin_times_sin cos_times_sin sin_times_cos cos_times_cos
                    integrable_sin_cx integrable_cos_cx mult_ac
               flip: distrib_left distrib_right left_diff_distrib right_diff_distrib)

lemma integral_sin_and_cos_Z [simp]:
  fixes m n::real
  assumes "m  " "n  "
  shows
  "integralL (lebesgue_on {-pi..pi}) (λx. cos(m * x) * cos(n * x)) = (if ¦m¦ = ¦n¦ then if n = 0 then 2 * pi else pi else 0)"
  "integralL (lebesgue_on {-pi..pi}) (λx. cos(m * x) * sin(n * x)) = 0"
  "integralL (lebesgue_on {-pi..pi}) (λx. sin(m * x) * cos(n * x)) = 0"
  "¦integralL (lebesgue_on {-pi..pi}) (λx. sin (m * x) * sin (n * x))¦ = (if ¦m¦ = ¦n¦  n  0 then pi else 0)"
  using assms unfolding Ints_def
     apply safe
  unfolding integral_sin_and_cos
     apply auto
  done

lemma integral_sin_and_cos_N [simp]:
  fixes m n::real
  assumes "m  " "n  "
  shows "integralL (lebesgue_on {-pi..pi}) (λx. sin (m * x) * sin (n * x)) = (if m = n  n  0 then pi else 0)"
  using assms unfolding Nats_altdef1 by (auto simp: integral_sin_and_cos)


lemma integrable_sin_and_cos:
  fixes m n::int
  shows "integrable (lebesgue_on {a..b}) (λx. cos(x * m) * cos(x * n))"
        "integrable (lebesgue_on {a..b}) (λx. cos(x * m) * sin(x * n))"
        "integrable (lebesgue_on {a..b}) (λx. sin(x * m) * cos(x * n))"
        "integrable (lebesgue_on {a..b}) (λx. sin(x * m) * sin(x * n))"
  by (intro continuous_imp_integrable_real continuous_intros)+

lemma sqrt_pi_ge1: "sqrt pi  1"
  using pi_gt3 by auto

definition trigonometric_set :: "nat  real  real"
  where "trigonometric_set n 
    if n = 0 then λx. 1 / sqrt(2 * pi)
    else if odd n then λx. sin(real(Suc (n div 2)) * x) / sqrt(pi)
    else (λx. cos((n div 2) * x) / sqrt pi)"

lemma trigonometric_set:
  "trigonometric_set 0 x = 1 / sqrt(2 * pi)"
  "trigonometric_set (Suc (2 * n)) x = sin(real(Suc n) * x) / sqrt(pi)"
  "trigonometric_set (2 * n + 2) x = cos(real(Suc n) * x) / sqrt(pi)"
  "trigonometric_set (Suc (Suc (2 * n))) x = cos(real(Suc n) * x) / sqrt(pi)"
  by (simp_all add: trigonometric_set_def algebra_simps add_divide_distrib)

lemma trigonometric_set_even:
   "trigonometric_set(2*k) = (if k = 0 then (λx. 1 / sqrt(2 * pi)) else (λx. cos(k * x) / sqrt pi))"
  by (induction k) (auto simp: trigonometric_set_def add_divide_distrib split: if_split_asm)

lemma orthonormal_system_trigonometric_set:
    "orthonormal_system {-pi..pi} trigonometric_set"
proof -
  have "l2product {-pi..pi} (trigonometric_set m) (trigonometric_set n) = (if m = n then 1 else 0)" for m n
  proof (induction m rule: odd_even_cases)
    case 0
    show ?case
      by (induction n rule: odd_even_cases) (auto simp: trigonometric_set l2product_def measure_restrict_space)
  next
    case (odd m)
    show ?case
      by (induction n rule: odd_even_cases) (auto simp: trigonometric_set l2product_def double_not_eq_Suc_double)
  next
    case (even m)
    show ?case
      by (induction n rule: odd_even_cases) (auto simp: trigonometric_set l2product_def Suc_double_not_eq_double)
  qed
  then show ?thesis
    unfolding orthonormal_system_def by auto
qed


lemma square_integrable_trigonometric_set:
   "(trigonometric_set i) square_integrable {-pi..pi}"
proof -
  have "continuous_on {-pi..pi} (λx. sin ((1 + real n) * x) / sqrt pi)" for n
    by (intro continuous_intros) auto
  moreover
  have "continuous_on {-pi..pi} (λx. cos (real i * x / 2) / sqrt pi) "
    by (intro continuous_intros) auto
  ultimately show ?thesis
    by (simp add: trigonometric_set_def)
qed

subsection‹Weierstrass for trigonometric polynomials›

lemma Weierstrass_trig_1:
  fixes g :: "real  real"
  assumes contf: "continuous_on UNIV g" and periodic: "x. g(x + 2 * pi) = g x" and 1: "norm z = 1"
  shows "continuous (at z within (sphere 0 1)) (g  Im  Ln)"
proof (cases "Re z < 0")
  let ?f = "complex_of_real  g  (λx. x + pi)  Im  Ln  uminus"
  case True
  have "continuous (at z within (sphere 0 1)) (complex_of_real  g  Im  Ln)"
  proof (rule continuous_transform_within)
    have [simp]: "z  0"
      using True complex_nonneg_Reals_iff by auto
    show "continuous (at z within (sphere 0 1)) ?f"
      by (intro continuous_within_Ln continuous_intros continuous_on_imp_continuous_within [OF contf]) auto
    show "?f x' =  (complex_of_real  g  Im  Ln) x'"
      if "x'  (sphere 0 1)" and "dist x' z < 1" for x'
    proof -
      have "x'  0"
        using that by auto
      with that show ?thesis
        by (auto simp: Ln_minus add.commute periodic)
    qed
  qed (use 1 in auto)
  then have "continuous (at z within (sphere 0 1)) (Re  complex_of_real  g  Im  Ln)"
    unfolding o_def by (rule continuous_Re)
  then show ?thesis
    by (simp add: o_def)
next
  case False
  let ?f = "complex_of_real  g  Im  Ln  uminus"
  have "z  0"
    using 1 by auto
  with False have "z  0"
    by (auto simp: not_less nonpos_Reals_def)
  then have "continuous (at z within (sphere 0 1)) (complex_of_real  g  Im  Ln)"
    by (intro continuous_within_Ln continuous_intros continuous_on_imp_continuous_within [OF contf]) auto
  then have "continuous (at z within (sphere 0 1)) (Re  complex_of_real  g  Im  Ln)"
    unfolding o_def by (rule continuous_Re)
  then show ?thesis
    by (simp add: o_def)
qed

inductive_set cx_poly :: "(complex  real) set" where
    Re: "Re  cx_poly"
  | Im: "Im  cx_poly"
  | const: "(λx. c)  cx_poly"
  | add:   "f  cx_poly; g  cx_poly  (λx. f x + g x)  cx_poly"
  | mult:  "f  cx_poly; g  cx_poly  (λx. f x * g x)  cx_poly"

declare cx_poly.intros [intro]


lemma Weierstrass_trig_polynomial:
  assumes contf: "continuous_on {-pi..pi} f" and fpi: "f(-pi) = f pi" and "0 < e"
  obtains n::nat and a b where
    "x::real. x  {-pi..pi}  ¦f x - (kn. a k * sin (k * x) + b k * cos (k * x))¦ < e"
proof -
  interpret CR: function_ring_on "cx_poly" "sphere 0 1"
  proof
    show "continuous_on (sphere 0 1) f" if "f  cx_poly" for f
      using that by induction (assumption | intro continuous_intros)+
    fix x y::complex
    assume "x  sphere 0 1" and "y  sphere 0 1" and "x  y"
    then consider "Re x  Re y" | "Im x  Im y"
      using complex_eqI by blast
    then show "fcx_poly. f x  f y"
      by (metis cx_poly.Im cx_poly.Re)
  qed (auto simp: cx_poly.intros)
  have "continuous (at z within (sphere 0 1)) (f  Im  Ln)" if "norm z = 1" for z
  proof -
    obtain g where contg: "continuous_on UNIV g" and gf: "x. x  {-pi..pi}  g x = f x"
      and periodic: "x. g(x + 2*pi) = g x"
      using Tietze_periodic_interval [OF contf fpi] by auto
    let ?f = "(g  Im  Ln)"
    show ?thesis
    proof (rule continuous_transform_within)
      show "continuous (at z within (sphere 0 1)) ?f"
        using Weierstrass_trig_1 [OF contg periodic that] by (simp add: sphere_def)
      show "?f x' = (f  Im  Ln) x'"
        if "x'  sphere 0 1" "dist x' z < 1" for x'
      proof -
        have "x'  0"
          using that by auto
        then have "Im (Ln x')  {-pi..pi}"
          using Im_Ln_le_pi [of x'] mpi_less_Im_Ln [of x'] by simp
        then show ?thesis
          using gf by simp
      qed
    qed (use that in auto)
  qed
  then have "continuous_on (sphere 0 1) (f  Im  Ln)"
    using continuous_on_eq_continuous_within mem_sphere_0 by blast
  then obtain g where "g  cx_poly" and g: "x. x  sphere 0 1  ¦(f  Im  Ln) x - g x¦ < e"
    using CR.Stone_Weierstrass_basic [of "f  Im  Ln"] e > 0 by meson
  define trigpoly where
    "trigpoly  λf. n a b. f = (λx. (kn. a k * sin(real k * x) +  b k * cos(real k * x)))"
  have tp_const: "trigpoly(λx. c)" for c
    unfolding trigpoly_def
    by (rule_tac x=0 in exI) auto
  have tp_add: "trigpoly(λx. f x + g x)" if "trigpoly f" "trigpoly g" for f g
  proof -
    obtain n1 a1 b1 where feq: "f = (λx. kn1. a1 k * sin (real k * x) + b1 k * cos (real k * x))"
      using trigpoly f trigpoly_def by blast
    obtain n2 a2 b2 where geq: "g = (λx. kn2. a2 k * sin (real k * x) + b2 k * cos (real k * x))"
      using trigpoly g trigpoly_def by blast
    let ?a = "λn. (if n  n1 then a1 n else 0) + (if n  n2 then a2 n else 0)"
    let ?b = "λn. (if n  n1 then b1 n else 0) + (if n  n2 then b2 n else 0)"
    have eq: "{k. k  max a b  k  a} = {..a}" "{k. k  max a b  k  b} = {..b}" for a b::nat
      by auto
    have "(λx. f x + g x) = (λx. k  max n1 n2. ?a k * sin (real k * x) + ?b k * cos (real k * x))"
      by (simp add: feq geq algebra_simps eq sum.distrib if_distrib [of "λu. _ * u"] cong: if_cong flip: sum.inter_filter)
    then show ?thesis
      unfolding trigpoly_def by meson
  qed
  have tp_sum: "trigpoly(λx. iS. f i x)" if "finite S" "i. i  S  trigpoly(f i)" for f and S :: "nat set"
    using that
    by induction (auto simp: tp_const tp_add)
  have tp_cmul: "trigpoly(λx. c * f x)" if "trigpoly f" for f c
  proof -
    obtain n a b where feq: "f = (λx. kn. a k * sin (real k * x) + b k * cos (real k * x))"
      using trigpoly f trigpoly_def by blast
    have "(λx. c * f x) = (λx. k  n. (c * a k) * sin (real k * x) + (c * b k) * cos (real k * x))"
      by (simp add: feq algebra_simps sum_distrib_left)
    then show ?thesis
      unfolding trigpoly_def by meson
  qed
  have tp_cdiv: "trigpoly(λx. f x / c)" if "trigpoly f" for f c
    using tp_cmul [OF trigpoly f, of "inverse c"]
    by (simp add: divide_inverse_commute)
  have tp_diff: "trigpoly(λx. f x - g x)" if "trigpoly f" "trigpoly g" for f g
    using tp_add [OF trigpoly f tp_cmul [OF trigpoly g, of "-1"]] by auto
  have tp_sin: "trigpoly(λx. sin (n * x))" if "n  " for n
    unfolding trigpoly_def
  proof
    obtain k where "n = real k"
      using Nats_cases n   by blast
    then show "a b. (λx. sin (n * x)) = (λx. i  natn. a i * sin (real i * x) + b i * cos (real i * x))"
      apply (rule_tac x="λi. if i = k then 1 else 0" in exI)
      apply (rule_tac x="λi. 0" in exI)
      apply (simp add: if_distrib [of "λu. u * _"] cong: if_cong)
      done
  qed
  have tp_cos: "trigpoly(λx. cos (n * x))" if "n  " for n
    unfolding trigpoly_def
  proof
    obtain k where "n = real k"
      using Nats_cases n   by blast
    then show "a b. (λx. cos (n * x)) = (λx. i  natn. a i * sin (real i * x) + b i * cos (real i * x))"
      apply (rule_tac x="λi. 0" in exI)
      apply (rule_tac x="λi. if i = k then 1 else 0" in exI)
      apply (simp add: if_distrib [of "λu. u * _"] cong: if_cong)
      done
  qed
  have tp_sincos: "trigpoly(λx. sin(i * x) * sin(j * x))  trigpoly(λx. sin(i * x) * cos(j * x)) 
                   trigpoly(λx. cos(i * x) * sin(j * x))  trigpoly(λx. cos(i * x) * cos(j * x))" (is "?P i j")
    for i j::nat
  proof (rule linorder_wlog [of _ j i])
    show "?P j i" if "i  j" for j i
      using that
      by (simp add: sin_times_sin cos_times_cos sin_times_cos cos_times_sin diff_divide_distrib 
                    tp_add tp_diff tp_cdiv tp_cos tp_sin flip: left_diff_distrib distrib_right)
  qed (simp add: mult_ac)
  have tp_mult: "trigpoly(λx. f x * g x)" if "trigpoly f" "trigpoly g" for f g
  proof -
    obtain n1 a1 b1 where feq: "f = (λx. kn1. a1 k * sin (real k * x) + b1 k * cos (real k * x))"
      using trigpoly f trigpoly_def by blast
    obtain n2 a2 b2 where geq: "g = (λx. kn2. a2 k * sin (real k * x) + b2 k * cos (real k * x))"
      using trigpoly g trigpoly_def by blast
    then show ?thesis
      unfolding feq geq
      by (simp add: algebra_simps sum_product tp_sum tp_add tp_cmul tp_sincos del: mult.commute)
  qed
  have *: "trigpoly(λx.  f(exp(𝗂 * of_real x)))" if "f  cx_poly" for f
    using that
  proof induction
    case Re
    then show ?case
      using tp_cos [of 1] by (auto simp: Re_exp)
  next
    case Im
    then show ?case
      using tp_sin [of 1] by (auto simp: Im_exp)
  qed (auto simp: tp_const tp_add tp_mult)
  obtain n a b where eq: "(g (iexp x)) = (kn. a k * sin (real k * x) + b k * cos (real k * x))" for x
    using * [OF g  cx_poly] trigpoly_def by meson
  show thesis
    proof
    show "¦f θ - (kn. a k * sin (real k * θ) + b k * cos (real k * θ))¦ < e"
      if "θ  {-pi..pi}" for θ
    proof -
      have "f θ - g (iexp θ) = (f  Im  Ln) (iexp θ) - g (iexp θ)"
      proof (cases "θ = -pi")
      case True
        then show ?thesis
          by (simp add: exp_minus fpi)
    next
      case False
      then show ?thesis
        using that by auto
    qed
    then show ?thesis
      using g [of "exp(𝗂 * of_real θ)"] by (simp flip: eq)
    qed
  qed
qed


subsection‹A bit of extra hacking round so that the ends of a function are OK›

lemma integral_tweak_ends:
  fixes a b :: real
  assumes "a < b" "e > 0"
  obtains f where "continuous_on {a..b} f" "f a = d" "f b = 0" "l2norm {a..b} f < e"
proof -
  have cont: "continuous_on {a..b}
          (λx. if x  a+1 / real(Suc n)
               then ((Suc n) * d) * ((a+1 / (Suc n)) - x) else 0)" for n
  proof (cases "a+1/(Suc n)  b")
    case True
    have *: "1 / (1 + real n) > 0"
      by auto
    have abeq: "{a..b} = {a..a+1/(Suc n)}  {a+1/(Suc n)..b}"
      using a < b True
      apply auto
      using "*" by linarith
    show ?thesis
      unfolding abeq
    proof (rule continuous_on_cases)
      show "continuous_on {a..a+1 / real (Suc n)} (λx. real (Suc n) * d * (a+1 / real (Suc n) - x))"
        by (intro continuous_intros)
    qed auto
  next
    case False
    show ?thesis
    proof (rule continuous_on_eq [where f = "λx. ((Suc n) * d) * ((a+1/(Suc n)) - x)"])
      show " continuous_on {a..b} (λx. (Suc n) * d * (a+1 / real (Suc n) - x))"
        by (intro continuous_intros)
    qed (use False in auto)
  qed
  let ?f = "λk x. (if x  a+1 / (Suc k) then (Suc k) * d * (a+1 / (Suc k) - x) else 0)2"
  let ?g = "λx. if x = a then d2 else 0"
  have bmg: "?g  borel_measurable (lebesgue_on {a..b})"
    apply (rule measurable_restrict_space1)
    using borel_measurable_if_I [of _ "{a}", OF borel_measurable_const] by auto
  have bmf: "?f k  borel_measurable (lebesgue_on {a..b})" for k
  proof -
    have bm: "(λx. (Suc k) * d * (a+1 / real (Suc k) - x))
               borel_measurable (lebesgue_on {..a+1 / (Suc k)})"
      by (intro measurable) (auto simp: measurable_completion measurable_restrict_space1)
    show ?thesis
      apply (intro borel_measurable_power measurable_restrict_space1)
      using borel_measurable_if_I [of _ "{.. a+1 / (Suc k)}", OF bm]  apply auto
      done
  qed
  have int_d2: "integrable (lebesgue_on {a..b}) (λx. d2)"
    by (intro continuous_imp_integrable_real continuous_intros)
  have "(λk. ?f k x)  ?g x"
    if x: "x  {a..b}" for x
  proof (cases "x = a")
    case False
    then have "x > a"
      using x by auto
    with x obtain N where "N > 0" and N: "1 / real N < x-a"
      using real_arch_invD [of "x-a"]
      by (force simp: inverse_eq_divide)
    then have "x > a+1 / (1 + real k)"
      if "k  N" for k
    proof -
      have "a+1 / (1 + real k) < a+1 / real N"
        using that 0 < N by (simp add: field_simps)
      also have " < x"
        using N by linarith
      finally show ?thesis .
    qed
    then show ?thesis
      apply (intro tendsto_eventually eventually_sequentiallyI [where c=N])
      by (fastforce simp: False)
  qed auto
  then have tends: "AE x in (lebesgue_on {a..b}). (λk. ?f k x)  ?g x"
    by force
  have le_d2: "k. AE x in (lebesgue_on {a..b}). norm (?f k x)  d2"
  proof
    show "norm ((if x  a+1 / real (Suc k) then real (Suc k) * d * (a+1 / real (Suc k) - x) else 0)2)  d2"
      if "x  space (lebesgue_on {a..b})" for k x
      using that
      apply (simp add: abs_mult divide_simps flip: abs_le_square_iff)
      apply (auto simp: abs_if zero_less_mult_iff mult_left_le)
      done
  qed
  have integ: "integrable (lebesgue_on {a..b}) ?g"
    using integrable_dominated_convergence [OF bmg bmf int_d2 tends le_d2] by auto
  have int: "(λk. integralL (lebesgue_on {a..b}) (?f k))  integralL (lebesgue_on {a..b}) ?g"
    using integral_dominated_convergence [OF bmg bmf int_d2 tends le_d2] by auto
  then obtain N where N: "k. k  N  ¦integralL (lebesgue_on {a..b}) (?f k) - integralL (lebesgue_on {a..b}) ?g¦ < e2"
    apply (simp add: lim_sequentially dist_real_def)
    apply (drule_tac x="e^2" in spec)
    using e > 0
    by auto
  obtain M where "M > 0" and M: "1 / real M < b-a"
    using real_arch_invD [of "b-a"]
    by (metis a < b diff_gt_0_iff_gt inverse_eq_divide neq0_conv)
  have *: "¦integralL (lebesgue_on {a..b}) (?f (max M N)) - integralL (lebesgue_on {a..b}) ?g¦ < e2"
    using N by force
  let  = "λx. if x  a+1/(Suc (max M N)) then ((Suc (max M N)) * d) * ((a+1/(Suc (max M N))) - x) else 0"
  show ?thesis
  proof
    show "continuous_on {a..b} "
      by (rule cont)
    have "1 / (1 + real (max M N))  1 / (real M)"
      by (simp add: 0 < M frac_le)
    then have "¬ (b  a+1 / (1 + real (max M N)))"
      using M a < b M > 0 max.cobounded1 [of M N]
      by linarith
    then show " b = 0"
      by simp
    have null_a: "{a}  null_sets (lebesgue_on {a..b})"
      using a < b by (simp add: null_sets_restrict_space)
    have "LINT x|lebesgue_on {a..b}. ?g x = 0"
      by (force intro: integral_eq_zero_AE AE_I' [OF null_a])
    then have "l2norm {a..b}  < sqrt (e^2)"
      unfolding l2norm_def l2product_def power2_eq_square [symmetric]
      apply (intro real_sqrt_less_mono)
      using "*" by linarith
    then show "l2norm {a..b}  < e"
      using e > 0 by auto
  qed auto
qed


lemma square_integrable_approximate_continuous_ends:
  assumes f: "f square_integrable {a..b}" and "a < b" "0 < e"
  obtains g where "continuous_on {a..b} g" "g b = g a" "g square_integrable {a..b}" "l2norm {a..b} (λx. f x - g x) < e"
proof -
  obtain g where contg: "continuous_on UNIV g" and "g square_integrable {a..b}"
    and lg: "l2norm {a..b} (λx. f x - g x) < e/2"
    using f e > 0 square_integrable_approximate_continuous
    by (metis (full_types) box_real(2) half_gt_zero_iff lmeasurable_cbox)
  obtain h where conth: "continuous_on {a..b} h" and "h a = g b - g a" "h b = 0"
    and lh: "l2norm {a..b} h < e/2"
    using integral_tweak_ends e > 0
    by (metis a < b zero_less_divide_iff zero_less_numeral)
  have "h square_integrable {a..b}"
    using continuous_on {a..b} h continuous_imp_square_integrable by blast
  show thesis
  proof
    show "continuous_on {a..b} (λx. g x + h x)"
      by (blast intro: continuous_on_subset [OF contg] conth continuous_intros)
    then show "(λx. g x + h x) square_integrable {a..b}"
      using continuous_imp_square_integrable by blast
    show "g b + h b = g a + h a"
      by (simp add: h a = g b - g a h b = 0)
    have "l2norm {a..b} (λx. (f x - g x) + - h x) < e"
    proof (rule le_less_trans [OF l2norm_triangle [of "λx. f x - g x" "{a..b}" "λx. - (h x)"]])
      show "(λx. f x - g x) square_integrable {a..b}"
        using g square_integrable {a..b} f square_integrable_diff by blast
      show "(λx. - h x) square_integrable {a..b}"
        by (simp add: h square_integrable {a..b})
      show "l2norm {a..b} (λx. f x - g x) + l2norm {a..b} (λx. - h x) < e"
        using h square_integrable {a..b} l2norm_neg lg lh by auto
    qed
    then show "l2norm {a..b} (λx. f x - (g x + h x)) < e"
      by (simp add: field_simps)
  qed
qed


subsection‹Hence the main approximation result›

lemma Weierstrass_l2_trig_polynomial:
  assumes f: "f square_integrable {-pi..pi}" and "0 < e"
  obtains n a b where
   "l2norm {-pi..pi} (λx. f x - (kn. a k * sin(real k * x) + b k * cos(real k * x))) < e"
proof -
  let  = "λn a b x. kn. a k * sin(real k * x) + b k * cos(real k * x)"
  obtain g where contg: "continuous_on {-pi..pi} g" and geq: "g(-pi) = g pi"
           and g: "g square_integrable {-pi..pi}" and norm_fg: "l2norm {-pi..pi} (λx. f x - g x) < e/2"
    using e > 0 by (auto intro: square_integrable_approximate_continuous_ends [OF f, of "e/2"])
  then obtain n a b where g_phi_less: "x. x  {-pi..pi}  ¦g x - ( n a b x)¦ < e/6"
    using e > 0 Weierstrass_trig_polynomial [OF contg geq, of "e/6"]
    by (meson zero_less_divide_iff zero_less_numeral)
  show thesis
  proof
    have si: "( n u v) square_integrable {-pi..pi}" for n::nat and u v
    proof (intro square_integrable_sum continuous_imp_square_integrable)
      show "continuous_on {-pi..pi} (λx. u k * sin (real k * x) + v k * cos (real k * x))"
        if "k  {..n}" for k
        using that by (intro continuous_intros)
    qed auto
    have "l2norm {-pi..pi} (λx. f x - ( n a b x)) =  l2norm {-pi..pi} (λx. (f x - g x) + (g x - ( n a b x)))"
      by simp
    also have "  l2norm {-pi..pi} (λx. f x - g x) + l2norm {-pi..pi} (λx. g x - ( n a b x))"
    proof (rule l2norm_triangle)
      show "(λx. f x - g x) square_integrable {-pi..pi}"
        using f g square_integrable_diff by blast
      show "(λx. g x - ( n a b x)) square_integrable {-pi..pi}"
        using g si square_integrable_diff by blast
    qed
    also have " < e"
    proof -
      have g_phi: "(λx. g x - ( n a b x)) square_integrable {-pi..pi}"
        using g si square_integrable_diff by blast
      have "l2norm {-pi..pi} (λx. g x - ( n a b x))  e/2"
        unfolding l2norm_def l2product_def power2_eq_square [symmetric]
      proof (rule real_le_lsqrt)
        have "LINT x|lebesgue_on {-pi..pi}. (g x - ( n a b x))2
             LINT x|lebesgue_on {-pi..pi}. (e / 6) ^ 2"
        proof (rule integral_mono)
          show "integrable (lebesgue_on {-pi..pi}) (λx. (g x - ( n a b x))2)"
            using g_phi square_integrable_def by auto
          show "integrable (lebesgue_on {-pi..pi}) (λx. (e / 6)2)"
            by (intro continuous_intros continuous_imp_integrable_real)
          show "(g x - ( n a b x))2  (e / 6)2" if "x  space (lebesgue_on {-pi..pi})" for x
            using e > 0 g_phi_less that
            apply (simp add: abs_le_square_iff [symmetric])
            using less_eq_real_def by blast
        qed
        also have "  (e / 2)2"
          using e > 0 pi_less_4 by (auto simp: power2_eq_square measure_restrict_space)
        finally show "LINT x|lebesgue_on {-pi..pi}. (g x - ( n a b x))2  (e / 2)2" .
      qed (use e > 0 in auto)
      with norm_fg show ?thesis
        by auto
    qed
    finally show "l2norm {-pi..pi} (λx. f x - ( n a b x)) < e" .
  qed
qed


proposition Weierstrass_l2_trigonometric_set:
  assumes f: "f square_integrable {-pi..pi}" and "0 < e"
  obtains n a where "l2norm {-pi..pi} (λx. f x - (kn. a k * trigonometric_set k x)) < e"
proof -
  obtain n a b where lee:
    "l2norm {-pi..pi} (λx. f x - (kn. a k * sin(real k * x) + b k * cos(real k * x))) < e"
    using Weierstrass_l2_trig_polynomial [OF assms] .
  let ?a = "λk. if k = 0 then sqrt(2 * pi) * b 0
                else if even k then sqrt pi * b(k div 2)
                else if k  2 * n then sqrt pi * a((Suc k) div 2)
                else 0"
  show thesis
  proof
    have [simp]: "Suc (i * 2)  n * 2  i<n" "{..n}  {..<n} = {..<n}" for i n
      by auto
    have "(kn. b k * cos (real k * x)) = (in. if i = 0 then b 0 else b i * cos (real i * x))" for x
      by (rule sum.cong) auto
    moreover have "(kn. a k * sin (real k * x)) = (in. (if Suc (2 * i)  2 * n then sqrt pi * a (Suc i) * sin ((1 + real i) * x) else 0) / sqrt pi)"
                   (is "?lhs = ?rhs") for x
    proof (cases "n=0")
      case False
      then obtain n' where n': "n = Suc n'"
        using not0_implies_Suc by blast
      have "?lhs = (k = Suc 0..n. a k * sin (real k * x))"
        by (simp add: atMost_atLeast0 sum_shift_lb_Suc0_0)
      also have " = (i<n. a (Suc i) * sin (x + x * real i))"
      proof (subst sum.reindex_bij_betw [symmetric])
        show "bij_betw Suc {..n'} {Suc 0..n}"
          by (simp add: atMost_atLeast0 n')
        show "(jn'. a (Suc j) * sin (real (Suc j) * x)) = (i<n. a (Suc i) * sin (x + x * real i))"
        unfolding n' lessThan_Suc_atMost by (simp add: algebra_simps)
      qed
      also have " = ?rhs"
        by (simp add: field_simps if_distrib [of "λx. x/_"] sum.inter_restrict [where B = "{..<n}", simplified, symmetric] cong: if_cong)
      finally
      show ?thesis .
    qed auto
    ultimately
    have "(kn. a k * sin(real k * x) + b k * cos(real k * x)) = (k  Suc(2*n). ?a k * trigonometric_set k x)" for x
      unfolding sum.in_pairs_0 trigonometric_set_def
      by (simp add: sum.distrib if_distrib [of "λx. x*_"] cong: if_cong)
    with lee show "l2norm {-pi..pi} (λx. f x - (k  Suc(2*n). ?a k * trigonometric_set k x)) < e"
      by auto
  qed
qed

subsection‹Convergence wrt the L2 norm of trigonometric Fourier series›

definition Fourier_coefficient
  where "Fourier_coefficient  orthonormal_coeff {-pi..pi} trigonometric_set"

lemma Fourier_series_l2:
  assumes "f square_integrable {-pi..pi}"
  shows "(λn. l2norm {-pi..pi} (λx. f x - (in. Fourier_coefficient f i * trigonometric_set i x)))
          0"
proof (clarsimp simp add: lim_sequentially dist_real_def Fourier_coefficient_def)
  let ?h = "λn x. (in. orthonormal_coeff {-pi..pi} trigonometric_set f i * trigonometric_set i x)"
  show "N. nN. ¦l2norm {-pi..pi} (λx. f x - ?h n x)¦ < e"
    if "0 < e" for e
  proof -
    obtain N a where lte: "l2norm {-pi..pi} (λx. f x - (kN. a k * trigonometric_set k x)) < e"
      using Weierstrass_l2_trigonometric_set by (meson 0 < e assms)
    show ?thesis
    proof (intro exI allI impI)
      show "¦l2norm {-pi..pi} (λx. f x - ?h m x)¦ < e"
        if "N  m" for m
      proof -
        have "¦l2norm {-pi..pi} (λx. f x - ?h m x)¦ = l2norm {-pi..pi} (λx. f x - ?h m x)"
        proof (rule abs_of_nonneg)
          show "0  l2norm {-pi..pi} (λx. f x -  ?h m x)"
            apply (intro l2norm_pos_le square_integrable_diff square_integrable_sum square_integrable_lmult
                square_integrable_trigonometric_set assms, auto)
            done
        qed
        also have "  l2norm {-pi..pi} (λx. f x - (kN. a k * trigonometric_set k x))"
        proof -
          have "(im. (if i  N then a i else 0) * trigonometric_set i x) = (iN. a i * trigonometric_set i x)" for x
            using sum.inter_restrict [where A = "{..m}" and B = "{..N}", symmetric] that
            by (force simp: if_distrib [of "λx. x * _"] min_absorb2 cong: if_cong)
          moreover
          have "l2norm {-pi..pi} (λx. f x - ?h m x)
                 l2norm {-pi..pi} (λx. f x - (im. (if i  N then a i else 0) * trigonometric_set i x))"
            using orthonormal_optimal_partial_sum
              [OF orthonormal_system_trigonometric_set square_integrable_trigonometric_set assms]
            by simp
          ultimately show ?thesis
            by simp
        qed
        also have " < e"
          by (rule lte)
        finally show ?thesis .
      qed
    qed
  qed
qed



subsection‹Fourier coefficients go to 0 (weak form of Riemann-Lebesgue)›

lemma trigonometric_set_mul_absolutely_integrable:
  assumes "f absolutely_integrable_on {-pi..pi}"
  shows "(λx. trigonometric_set n x * f x) absolutely_integrable_on {-pi..pi}"
proof (rule absolutely_integrable_bounded_measurable_product_real)
  show "trigonometric_set n  borel_measurable (lebesgue_on {-pi..pi})"
    using square_integrable_def square_integrable_trigonometric_set by blast
  show "bounded (trigonometric_set n ` {-pi..pi})"
    unfolding bounded_iff using pi_gt3 sqrt_pi_ge1
    by (rule_tac x=1 in exI)
      (auto simp: trigonometric_set_def dist_real_def
        intro: order_trans [OF abs_sin_le_one] order_trans [OF abs_cos_le_one])
qed (auto simp: assms)


lemma trigonometric_set_mul_integrable:
   "f absolutely_integrable_on {-pi..pi}  integrable (lebesgue_on {-pi..pi}) (λx. trigonometric_set n x * f x)"
  using trigonometric_set_mul_absolutely_integrable
  by (simp add: integrable_restrict_space set_integrable_def)

lemma trigonometric_set_integrable [simp]: "integrable (lebesgue_on {-pi..pi}) (trigonometric_set n)"
  using trigonometric_set_mul_integrable [where f = id]
  by simp (metis absolutely_integrable_imp_integrable fmeasurableD interval_cbox lmeasurable_cbox square_integrable_imp_absolutely_integrable square_integrable_trigonometric_set)

lemma absolutely_integrable_sin_product:
  assumes "f absolutely_integrable_on {-pi..pi}"
  shows "(λx. sin(k * x) * f x) absolutely_integrable_on {-pi..pi}"
proof (rule absolutely_integrable_bounded_measurable_product_real)
  show "(λx. sin (k * x))  borel_measurable (lebesgue_on {-pi..pi})"
    by (metis borel_measurable_integrable integrable_sin_cx mult_commute_abs)
  show "bounded ((λx. sin (k * x)) ` {-pi..pi})"
    by (metis (mono_tags, lifting) abs_sin_le_one bounded_iff imageE real_norm_def)
qed (auto simp: assms)

lemma absolutely_integrable_cos_product:
  assumes "f absolutely_integrable_on {-pi..pi}"
  shows "(λx. cos(k * x) * f x) absolutely_integrable_on {-pi..pi}"
proof (rule absolutely_integrable_bounded_measurable_product_real)
  show "(λx. cos (k * x))  borel_measurable (lebesgue_on {-pi..pi})"
    by (metis borel_measurable_integrable integrable_cos_cx mult_commute_abs)
  show "bounded ((λx. cos (k * x)) ` {-pi..pi})"
    by (metis (mono_tags, lifting) abs_cos_le_one bounded_iff imageE real_norm_def)
qed (auto simp: assms)

lemma
  assumes "f absolutely_integrable_on {-pi..pi}"
  shows Fourier_products_integrable_cos: "integrable (lebesgue_on {-pi..pi}) (λx. cos(k * x) * f x)"
  and   Fourier_products_integrable_sin: "integrable (lebesgue_on {-pi..pi}) (λx. sin(k * x) * f x)"
  using absolutely_integrable_cos_product absolutely_integrable_sin_product assms
  by (auto simp: integrable_restrict_space set_integrable_def)


lemma Riemann_lebesgue_square_integrable:
  assumes "orthonormal_system S w" "i. w i square_integrable S" "f square_integrable S"
  shows "orthonormal_coeff S w f  0"
  using Fourier_series_square_summable [OF assms, of UNIV] summable_LIMSEQ_zero by force

proposition Riemann_lebesgue:
  assumes "f absolutely_integrable_on {-pi..pi}"
  shows "Fourier_coefficient f  0"
  unfolding lim_sequentially
proof (intro allI impI)
  fix e::real
  assume "e > 0"
  then obtain g where "continuous_on UNIV g" and gabs: "g absolutely_integrable_on {-pi..pi}"
                and fg_e2: "integralL (lebesgue_on {-pi..pi}) (λx. ¦f x - g x¦) < e/2"
    using absolutely_integrable_approximate_continuous [OF assms, of "e/2"]
    by (metis (full_types) box_real(2) half_gt_zero_iff lmeasurable_cbox)
  have "g square_integrable {-pi..pi}"
    using continuous_on UNIV g continuous_imp_square_integrable continuous_on_subset by blast
  then have "orthonormal_coeff {-pi..pi} trigonometric_set g  0"
    using Riemann_lebesgue_square_integrable orthonormal_system_trigonometric_set square_integrable_trigonometric_set by blast
  with e > 0 obtain N where N: "n. n  N  ¦orthonormal_coeff {-pi..pi} trigonometric_set g n¦ < e/2"
    unfolding lim_sequentially by (metis half_gt_zero_iff norm_conv_dist real_norm_def)
  have "¦Fourier_coefficient f n¦ < e"
    if "n  N" for n
  proof -
    have "¦LINT x|lebesgue_on {-pi..pi}. trigonometric_set n x * g x¦ < e/2"
      using N [OF n  N] by (auto simp: orthonormal_coeff_def l2product_def)

    have "integrable (lebesgue_on {-pi..pi}) (λx. trigonometric_set n x * g x)"
      using gabs trigonometric_set_mul_integrable by blast
    moreover have "integrable (lebesgue_on {-pi..pi}) (λx. trigonometric_set n x * f x)"
      using assms trigonometric_set_mul_integrable by blast
    ultimately have "¦(LINT x|lebesgue_on {-pi..pi}. trigonometric_set n x * g x) -
                        (LINT x|lebesgue_on {-pi..pi}. trigonometric_set n x * f x)¦
                     = ¦(LINT x|lebesgue_on {-pi..pi}. trigonometric_set n x * (g x - f x))¦"
      by (simp add:  algebra_simps flip: Bochner_Integration.integral_diff)
    also have "  LINT x|lebesgue_on {-pi..pi}. ¦f x - g x¦"
    proof (rule integral_abs_bound_integral)
      show "integrable (lebesgue_on {-pi..pi}) (λx. trigonometric_set n x * (g x - f x))"
        by (simp add: gabs assms trigonometric_set_mul_integrable)
      have "(λx. f x - g x) absolutely_integrable_on {-pi..pi}"
        using gabs assms by blast
      then show "integrable (lebesgue_on {-pi..pi}) (λx. ¦f x - g x¦)"
        by (simp add: absolutely_integrable_imp_integrable)
      fix x
      assume "x  space (lebesgue_on {-pi..pi})"
      then have "-pi  x" "x  pi"
        by auto
      have "¦trigonometric_set n x¦  1"
        using pi_ge_two
        apply (simp add: trigonometric_set_def)
        using sqrt_pi_ge1 abs_sin_le_one order_trans abs_cos_le_one by metis
      then show "¦trigonometric_set n x * (g x - f x)¦  ¦f x - g x¦"
        using abs_ge_zero mult_right_mono by (fastforce simp add: abs_mult abs_minus_commute)
    qed
    finally have "¦(LINT x|lebesgue_on {-pi..pi}. trigonometric_set n x * g x) -
           (LINT x|lebesgue_on {-pi..pi}. trigonometric_set n x * f x)¦
           LINT x|lebesgue_on {-pi..pi}. ¦f x - g x¦" .
    then show ?thesis
      using N [OF n  N] fg_e2
      unfolding Fourier_coefficient_def orthonormal_coeff_def l2product_def
      by linarith
  qed
  then show "no. nno. dist (Fourier_coefficient f n) 0 < e"
    by auto
qed


lemma Riemann_lebesgue_sin:
  assumes "f absolutely_integrable_on {-pi..pi}"
  shows "(λn. integralL (lebesgue_on {-pi..pi}) (λx. sin(real n * x) * f x))  0"
  unfolding lim_sequentially
proof (intro allI impI)
  fix e::real
  assume "e > 0"
  then obtain N where N: "n. n  N  ¦Fourier_coefficient f n¦ < e/4"
    using Riemann_lebesgue [OF assms]
    unfolding lim_sequentially
    by (metis norm_conv_dist real_norm_def zero_less_divide_iff zero_less_numeral)
  have "¦LINT x|lebesgue_on {-pi..pi}. sin (real n * x) * f x¦ < e" if "n > N" for n
    using that
  proof (induction n)
    case (Suc n)
    have "¦Fourier_coefficient f(Suc (2 * n))¦ < e/4"
      using N Suc.prems by auto
    then have "¦LINT x|lebesgue_on {-pi..pi}. sin ((1 + real n) * x) * f x¦ < sqrt pi * e / 4"
      by (simp add: Fourier_coefficient_def orthonormal_coeff_def
          trigonometric_set_def l2product_def field_simps)
    also have "  e"
      using 0 < e pi_less_4 real_sqrt_less_mono by (fastforce simp add: field_simps)
    finally show ?case
      by simp
  qed auto
  then show "no. nno. dist (LINT x|lebesgue_on {-pi..pi}. sin (real n * x) * f x) 0 < e"
    by (metis (full_types) le_neq_implies_less less_add_same_cancel2 less_trans norm_conv_dist real_norm_def zero_less_one)
qed

lemma Riemann_lebesgue_cos:
  assumes "f absolutely_integrable_on {-pi..pi}"
  shows "(λn. integralL (lebesgue_on {-pi..pi}) (λx. cos(real n * x) * f x))  0"
  unfolding lim_sequentially
proof (intro allI impI)
  fix e::real
  assume "e > 0"
  then obtain N where N: "n. n  N  ¦Fourier_coefficient f n¦ < e/4"
    using Riemann_lebesgue [OF assms]
    unfolding lim_sequentially
    by (metis norm_conv_dist real_norm_def zero_less_divide_iff zero_less_numeral)
  have "¦LINT x|lebesgue_on {-pi..pi}. cos (real n * x) * f x¦ < e" if "n > N" for n
    using that
  proof (induction n)
    case (Suc n)
    have eq: "(x * 2 + x * (real n * 2)) / 2 = x + x * (real n)" for x
      by simp
    have "¦Fourier_coefficient f(2*n + 2)¦ < e/4"
      using N Suc.prems by auto
    then have "¦LINT x|lebesgue_on {-pi..pi}. f x * cos (x + x * (real n))¦ < sqrt pi * e / 4"
      by (simp add: Fourier_coefficient_def orthonormal_coeff_def
          trigonometric_set_def l2product_def field_simps eq)
    also have "  e"
      using 0 < e pi_less_4 real_sqrt_less_mono by (fastforce simp add: field_simps)
    finally show ?case
      by (simp add: field_simps)
  qed auto
  then show "no. nno. dist (LINT x|lebesgue_on {-pi..pi}. cos (real n * x) * f x) 0 < e"
    by (metis (full_types) le_neq_implies_less less_add_same_cancel2 less_trans norm_conv_dist real_norm_def zero_less_one)
qed


lemma Riemann_lebesgue_sin_half:
  assumes "f absolutely_integrable_on {-pi..pi}"
  shows "(λn. LINT x|lebesgue_on {-pi..pi}. sin ((real n + 1/2) * x) * f x)  0"
proof (simp add: algebra_simps sin_add)
  let ?INT = "integralL (lebesgue_on {-pi..pi})"
  let ?f = "(λn. ?INT (λx. sin(n * x) * cos(1/2 * x) * f x) +
                 ?INT (λx. cos(n * x) * sin(1/2 * x) * f x))"
  show "(λn. ?INT (λx. f x * (cos (x * real n) * sin (x/2)) + f x * (sin (x * real n) * cos (x/2))))  0"
  proof (rule Lim_transform_eventually)
    have sin: "(λx. sin (1/2 * x) * f x) absolutely_integrable_on {-pi..pi}"
      by (intro absolutely_integrable_sin_product assms)
    have cos: "(λx. cos (1/2 * x) * f x) absolutely_integrable_on {-pi..pi}"
      by (intro absolutely_integrable_cos_product assms)
    show "F n in sequentially. ?f n = ?INT (λx. f x * (cos (x * real n) * sin (x/2)) + f x * (sin (x * real n) * cos (x/2)))"
      unfolding mult.assoc
      apply (rule eventuallyI)
      apply (subst Bochner_Integration.integral_add [symmetric])
        apply (safe intro!: cos absolutely_integrable_sin_product sin absolutely_integrable_cos_product absolutely_integrable_imp_integrable)
        apply (auto simp: algebra_simps)
      done
    have "?f  0 + 0"
      unfolding mult.assoc
      by (intro tendsto_add Riemann_lebesgue_sin Riemann_lebesgue_cos sin cos)
    then show "?f  (0::real)" by simp
  qed
qed


lemma Fourier_sum_limit_pair:
  assumes "f absolutely_integrable_on {-pi..pi}"
  shows "(λn. k2 * n. Fourier_coefficient f k * trigonometric_set k t)  l
      (λn. kn. Fourier_coefficient f k * trigonometric_set k t)  l"
        (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  show ?rhs
    unfolding lim_sequentially dist_real_def
  proof (intro allI impI)
    fix e::real
    assume "e > 0"
    then obtain N1 where N1: "n. n  N1  ¦Fourier_coefficient f n¦ < e/2"
      using Riemann_lebesgue [OF assms] unfolding lim_sequentially
      by (metis norm_conv_dist real_norm_def zero_less_divide_iff zero_less_numeral)
    obtain N2 where N2: "n. n  N2  ¦(k2 * n. Fourier_coefficient f k * trigonometric_set k t) - l¦ < e/2"
      using L unfolding lim_sequentially dist_real_def
      by (meson 0 < e half_gt_zero_iff)
    show "no. nno. ¦(kn. Fourier_coefficient f k * trigonometric_set k t) - l¦ < e"
    proof (intro exI allI impI)
      fix n
      assume n: "N1 + 2*N2 + 1  n"
      then have "n  N1" "n  N2" "n div 2  N2"
        by linarith+
      consider "n = 2 * (n div 2)" | "n = Suc(2 * (n div 2))"
        by linarith
      then show "¦(kn. Fourier_coefficient f k * trigonometric_set k t) - l¦ < e"
      proof cases
        case 1
        show ?thesis
          apply (subst 1)
          using N2 [OF n div 2  N2] by linarith
      next
        case 2
        have "¦(k2 * (n div 2). Fourier_coefficient f k * trigonometric_set k t) - l¦ < e/2"
          using N2 [OF n div 2  N2] by linarith
        moreover have "¦Fourier_coefficient f(Suc (2 * (n div 2))) * trigonometric_set (Suc (2 * (n div 2))) t¦ < (e/2) * 1"
        proof -
          have "¦trigonometric_set (Suc (2 * (n div 2))) t¦  1"
            apply (simp add: trigonometric_set)
            using abs_sin_le_one sqrt_pi_ge1 by (blast intro: order_trans)
          moreover have "¦Fourier_coefficient f(Suc (2 * (n div 2)))¦ < e/2"
            using N1 N1  n by auto
          ultimately show ?thesis
            unfolding abs_mult
            by (meson abs_ge_zero le_less_trans mult_left_mono mult_less_cancel_right_pos zero_less_one)
        qed
        ultimately show ?thesis
          apply (subst 2)
          unfolding sum.atMost_Suc by linarith
      qed
    qed
  qed
next
  assume ?rhs then show ?lhs
    unfolding lim_sequentially
    by (auto simp: elim!: imp_forward ex_forward)
qed


subsection‹Express Fourier sum in terms of the special expansion at the origin›

lemma Fourier_sum_0:
  "(k  n. Fourier_coefficient f k * trigonometric_set k 0) =
     (k  n div 2. Fourier_coefficient f(2*k) * trigonometric_set (2*k) 0)"
  (is "?lhs = ?rhs")
proof -
  have "?lhs = (k = 2 * 0.. Suc (2 * (n div 2)). Fourier_coefficient f k * trigonometric_set k 0)"
  proof (rule sum.mono_neutral_left)
    show "i{2 * 0..Suc (2 * (n div 2))} - {..n}. Fourier_coefficient f i * trigonometric_set i 0 = 0"
    proof clarsimp
      fix i
      assume "i  Suc (2 * (n div 2))" "¬ i  n"
			then have "i = Suc n" "even n"
			  by presburger+
			moreover
			assume "trigonometric_set i 0  0"
			ultimately
			show "Fourier_coefficient f i = 0"
				by (simp add: trigonometric_set_def)
		qed
	qed auto
  also have " = ?rhs"
 	  unfolding sum.in_pairs by (simp add: trigonometric_set atMost_atLeast0)
  finally show ?thesis .
qed


lemma Fourier_sum_0_explicit:
  "(kn. Fourier_coefficient f k * trigonometric_set k 0)
    = (Fourier_coefficient f 0 / sqrt 2 + (k = 1..n div 2. Fourier_coefficient f(2*k))) / sqrt pi"
  (is "?lhs = ?rhs")
proof -
  have "(k=0..n. Fourier_coefficient f k * trigonometric_set k 0)
        = Fourier_coefficient f 0 * trigonometric_set 0 0 + (k = 1..n. Fourier_coefficient f k * trigonometric_set k 0)"
    by (simp add: Fourier_sum_0 sum.atLeast_Suc_atMost)
  also have " = ?rhs"
  proof -
    have "Fourier_coefficient f 0 * trigonometric_set 0 0 = Fourier_coefficient f 0 / (sqrt 2 * sqrt pi)"
      by (simp add: real_sqrt_mult trigonometric_set(1))
    moreover have "(k = Suc 0..n. Fourier_coefficient f k * trigonometric_set k 0) = (k = Suc 0..n div 2. Fourier_coefficient f(2*k)) / sqrt pi"
    proof (induction n)
      case (Suc n)
      show ?case
        by (simp add: Suc) (auto simp: trigonometric_set_def field_simps)
    qed auto
    ultimately show ?thesis
      by (simp add: add_divide_distrib)
  qed
  finally show ?thesis
    by (simp add: atMost_atLeast0)
qed

lemma Fourier_sum_0_integrals:
  assumes "f absolutely_integrable_on {-pi..pi}"
  shows "(kn. Fourier_coefficient f k * trigonometric_set k 0) =
          (integralL (lebesgue_on {-pi..pi}) f / 2 +
           (k = Suc 0..n div 2. integralL (lebesgue_on {-pi..pi}) (λx. cos(k * x) * f x))) / pi"
proof -
  have "integralL (lebesgue_on {-pi..pi}) f / (sqrt (2 * pi) * sqrt 2 * sqrt pi) = integralL (lebesgue_on {-pi..pi}) f / (2 * pi)"
    by (simp add: algebra_simps real_sqrt_mult)
  moreover have "(k = Suc 0..n div 2. LINT x|lebesgue_on {-pi..pi}. trigonometric_set (2*k) x * f x) / sqrt pi
               = (k = Suc 0..n div 2. LINT x|lebesgue_on {-pi..pi}. cos (k * x) * f x) / pi"
    by (simp add: trigonometric_set_def sum_divide_distrib)
  ultimately show ?thesis
    unfolding Fourier_sum_0_explicit
    by (simp add: Fourier_coefficient_def orthonormal_coeff_def l2product_def trigonometric_set add_divide_distrib)
qed


lemma Fourier_sum_0_integral:
  assumes "f absolutely_integrable_on {-pi..pi}"
  shows "(kn. Fourier_coefficient f k * trigonometric_set k 0) =
       integralL (lebesgue_on {-pi..pi}) (λx. (1/2 + (k = Suc 0..n div 2. cos(k * x))) * f x) / pi"
proof -
  note * = Fourier_products_integrable_cos [OF assms]
  have "integrable (lebesgue_on {-pi..pi}) (λx. n = Suc 0..n div 2. f x * cos (x * real n))"
    using * by (force simp: mult_ac)
  moreover have "integralL (lebesgue_on {-pi..pi}) f / 2 + (k = Suc 0..n div 2. LINT x|lebesgue_on {-pi..pi}. f x * cos (x * real k))
               = (LINT x|lebesgue_on {-pi..pi}. f x / 2) + (LINT x|lebesgue_on {-pi..pi}. (n = Suc 0..n div 2. f x * cos (x * real n)))"
  proof (subst Bochner_Integration.integral_sum)
    show "integrable (lebesgue_on {-pi..pi}) (λx. f x * cos (x * real i))"
      if "i  {Suc 0..n div 2}" for i
      using that * [of i] by (auto simp: Bochner_Integration.integral_sum mult_ac)
  qed auto
  ultimately show ?thesis
    using Fourier_products_integrable_cos [OF assms] absolutely_integrable_imp_integrable [OF assms]
    by (simp add: Fourier_sum_0_integrals sum_distrib_left assms algebra_simps)
qed


subsection‹How Fourier coefficients behave under addition etc›

lemma Fourier_coefficient_add:
  assumes "f absolutely_integrable_on {-pi..pi}" "g absolutely_integrable_on {-pi..pi}"
  shows "Fourier_coefficient (λx. f x + g x) i =
                Fourier_coefficient f i + Fourier_coefficient g i"
  using assms trigonometric_set_mul_integrable
  by (simp add: Fourier_coefficient_def orthonormal_coeff_def l2product_def distrib_left)

lemma Fourier_coefficient_minus:
  assumes "f absolutely_integrable_on {-pi..pi}"
  shows "Fourier_coefficient (λx. - f x) i = - Fourier_coefficient f i"
  using assms trigonometric_set_mul_integrable
  by (simp add: Fourier_coefficient_def orthonormal_coeff_def l2product_def)

lemma Fourier_coefficient_diff:
  assumes f: "f absolutely_integrable_on {-pi..pi}" and g: "g absolutely_integrable_on {-pi..pi}"
  shows "Fourier_coefficient (λx. f x - g x) i = Fourier_coefficient f i - Fourier_coefficient g i"
proof -
  have mg: "(λx. - g x) absolutely_integrable_on {-pi..pi}"
    using g by (simp add: absolutely_integrable_measurable_real)
  show ?thesis
    using Fourier_coefficient_add [OF f mg] Fourier_coefficient_minus [OF g] by simp
qed

lemma Fourier_coefficient_const:
   "Fourier_coefficient (λx. c) i = (if i = 0 then c * sqrt(2 * pi) else 0)"
  by (auto simp: Fourier_coefficient_def orthonormal_coeff_def l2product_def trigonometric_set_def divide_simps measure_restrict_space)

lemma Fourier_offset_term:
  fixes f :: "real  real"
  assumes f: "f absolutely_integrable_on {-pi..pi}" and periodic: "x. f(x + 2*pi) = f x"
  shows  "Fourier_coefficient (λx. f(x+t)) (2 * n + 2) * trigonometric_set (2 * n + 2) 0
        = Fourier_coefficient f(2 * n+1) * trigonometric_set (2 * n+1) t
        + Fourier_coefficient f(2 * n + 2) * trigonometric_set (2 * n + 2) t"
proof -
  have eq: "(2 + 2 * real n) * x / 2 = (1 + real n) * x" for x
    by (simp add: divide_simps)
  have 1: "integrable (lebesgue_on {-pi..pi}) (λx. f x * (cos (x + x * n) * cos (t + t * n)))"
    using Fourier_products_integrable_cos [of f "Suc n"] f
    by (simp add: algebra_simps) (simp add: mult.assoc [symmetric])
  have 2: "integrable (lebesgue_on {-pi..pi}) (λx. f x * (sin (x + x * n) * sin (t + t * n)))"
    using Fourier_products_integrable_sin [of f "Suc n"] f
    by (simp add: algebra_simps) (simp add: mult.assoc [symmetric])
  have "has_bochner_integral (lebesgue_on {-pi..pi}) (λx. cos (real (Suc n) * (x + t - t)) * f(x + t))
                 (LINT x|lebesgue_on {-pi..pi}. cos (real (Suc n) * (x - t)) * f x)"
  proof (rule has_integral_periodic_offset)
    have "(λx. cos (real (Suc n) * (x - t)) * f x) absolutely_integrable_on {-pi..pi}"
    proof (rule absolutely_integrable_bounded_measurable_product_real)
      show "(λx. cos (real (Suc n) * (x - t)))  borel_measurable (lebesgue_on {-pi..pi})"
        by (intro continuous_imp_measurable_on_sets_lebesgue continuous_intros) auto
      show "bounded ((λx. cos (real (Suc n) * (x - t))) ` {-pi..pi})"
        by (rule boundedI [where B=1]) auto
    qed (use f in auto)
    then show "has_bochner_integral (lebesgue_on {-pi..pi}) (λx. cos ((Suc n) * (x - t)) * f x) (LINT x|lebesgue_on {-pi..pi}. cos (real (Suc n) * (x - t)) * f x)"
      by (simp add: has_bochner_integral_integrable integrable_restrict_space set_integrable_def)
  next
    fix x
    show "cos (real (Suc n) * (x + (pi - - pi) - t)) * f(x + (pi - - pi)) = cos (real (Suc n) * (x - t)) * f x"
      using periodic cos.plus_of_nat [of "(Suc n) * (x - t)" "Suc n"] by (simp add: algebra_simps)
  qed
  then have "has_bochner_integral (lebesgue_on {-pi..pi}) (λx. cos (real (Suc n) * x) * f(x + t))
                 (LINT x|lebesgue_on {-pi..pi}. cos (real (Suc n) * (x - t)) * f x)"
    by simp
  then have "LINT x|lebesgue_on {-pi..pi}. cos ((Suc n) * x) * f(x+t)
           = LINT x|lebesgue_on {-pi..pi}. cos ((Suc n) * (x - t)) * f x"
    using has_bochner_integral_integral_eq by blast
  also have " = LINT x|lebesgue_on {-pi..pi}. cos ((Suc n) * x - ((Suc n) * t)) * f x"
    by (simp add: algebra_simps)
  also have " = cos ((Suc n) * t) * (LINT x|lebesgue_on {-pi..pi}. cos ((Suc n) * x) * f x)
                 + sin ((Suc n) * t) * (LINT x|lebesgue_on {-pi..pi}. sin ((Suc n) * x) * f x)"
    by (simp add: cos_diff algebra_simps 1 2 flip: integral_mult_left_zero integral_mult_right_zero)
  finally have "LINT x|lebesgue_on {-pi..pi}. cos ((Suc n) * x) * f(x+t)
        = cos ((Suc n) * t) * (LINT x|lebesgue_on {-pi..pi}. cos ((Suc n) * x) * f x)
        + sin ((Suc n) * t) * (LINT x|lebesgue_on {-pi..pi}. sin ((Suc n) * x) * f x)" .
  then show ?thesis
    unfolding Fourier_coefficient_def orthonormal_coeff_def trigonometric_set_def
    by (simp add: eq) (simp add: divide_simps algebra_simps l2product_def)
qed


lemma Fourier_sum_offset:
  fixes f :: "real  real"
  assumes f: "f absolutely_integrable_on {-pi..pi}" and periodic: "x. f(x + 2*pi) = f x"
  shows  "(k2*n. Fourier_coefficient f k * trigonometric_set k t) =
          (k2*n. Fourier_coefficient (λx. f(x+t)) k * trigonometric_set k 0)" (is "?lhs = ?rhs")
proof -
  have "?lhs = Fourier_coefficient f 0 * trigonometric_set 0 t + (k = Suc 0..2*n. Fourier_coefficient f k * trigonometric_set k t)"
    by (simp add: atMost_atLeast0 sum.atLeast_Suc_atMost)
  moreover have "(k = Suc 0..2*n. Fourier_coefficient f k * trigonometric_set k t) =
                 (k = Suc 0..2*n. Fourier_coefficient (λx. f(x+t)) k * trigonometric_set k 0)"
  proof (cases n)
    case (Suc n')
    have "(k = Suc 0..2 * n. Fourier_coefficient f k * trigonometric_set k t)
        = (k = Suc 0.. Suc (Suc (2 * n')). Fourier_coefficient f k * trigonometric_set k t)"
      by (simp add: Suc)
    also have " = (k  Suc (2 * n'). Fourier_coefficient f(Suc k) * trigonometric_set (Suc k) t)"
      unfolding atMost_atLeast0 using sum.shift_bounds_cl_Suc_ivl by blast
    also have " = (k  Suc (2 * n'). Fourier_coefficient (λx. f(x+t)) (Suc k) * trigonometric_set (Suc k) 0)"
      unfolding sum.in_pairs_0
    proof (rule sum.cong [OF refl])
      show "Fourier_coefficient f(Suc (2 * k)) * trigonometric_set (Suc (2 * k)) t + Fourier_coefficient f(Suc (Suc (2 * k))) * trigonometric_set (Suc (Suc (2 * k))) t = Fourier_coefficient (λx. f(x + t)) (Suc (2 * k)) * trigonometric_set (Suc (2 * k)) 0 + Fourier_coefficient (λx. f(x + t)) (Suc (Suc (2 * k))) * trigonometric_set (Suc (Suc (2 * k))) 0"
        if "k  {..n'}" for k
        using that Fourier_offset_term [OF assms, of t ] by (auto simp: trigonometric_set_def)
    qed
    also have " = (k = Suc 0..Suc (Suc (2 * n')). Fourier_coefficient (λx. f(x+t)) k * trigonometric_set k 0)"
      by (simp only: atMost_atLeast0 sum.shift_bounds_cl_Suc_ivl)
    also have " = (k = Suc 0..2*n. Fourier_coefficient (λx. f(x+t)) k * trigonometric_set k 0)"
      by (simp add: Suc)
    finally show ?thesis .
  qed auto
  moreover have "?rhs
           = Fourier_coefficient (λx. f(x+t)) 0 * trigonometric_set 0 0 + (k = Suc 0..2*n. Fourier_coefficient (λx. f(x+t)) k * trigonometric_set k 0)"
    by (simp add: atMost_atLeast0 sum.atLeast_Suc_atMost)
  moreover have "Fourier_coefficient f 0 * trigonometric_set 0 t
               = Fourier_coefficient (λx. f(x+t)) 0 * trigonometric_set 0 0"
    by (simp add: Fourier_coefficient_def orthonormal_coeff_def trigonometric_set_def l2product_def integral_periodic_offset periodic)
  ultimately show ?thesis
    by simp
qed


lemma Fourier_sum_offset_unpaired:
  fixes f :: "real  real"
  assumes f: "f absolutely_integrable_on {-pi..pi}" and periodic: "x. f(x + 2*pi) = f x"
  shows  "(k2*n. Fourier_coefficient f k * trigonometric_set k t) =
          (kn. Fourier_coefficient (λx. f(x+t)) (2*k) * trigonometric_set (2*k) 0)"
  (is "?lhs = ?rhs")
proof -
  have "?lhs = (kn. Fourier_coefficient (λx. f(x+t)) (2*k) *  trigonometric_set (2*k) 0 +
                   Fourier_coefficient (λx. f(x+t)) (Suc (2*k)) * trigonometric_set (Suc (2*k)) 0)"
    apply (simp add: assms Fourier_sum_offset)
    apply (subst sum.in_pairs_0 [symmetric])
    by (simp add: trigonometric_set)
  also have " = ?rhs"
    by (auto simp: trigonometric_set)
  finally show ?thesis .
qed

subsection‹Express partial sums using Dirichlet kernel›

definition Dirichlet_kernel
  where "Dirichlet_kernel 
           λn x. if x = 0 then real n + 1/2
                          else sin((real n + 1/2) * x) / (2 * sin(x/2))"

lemma Dirichlet_kernel_0 [simp]:
   "¦x¦ < 2 * pi  Dirichlet_kernel 0 x = 1/2"
  by (auto simp: Dirichlet_kernel_def sin_zero_iff)

lemma Dirichlet_kernel_minus [simp]: "Dirichlet_kernel n (-x) = Dirichlet_kernel n x"
  by (auto simp: Dirichlet_kernel_def)


lemma Dirichlet_kernel_continuous_strong:
   "continuous_on {-(2 * pi)<..<2 * pi} (Dirichlet_kernel n)"
proof -
  have "isCont (Dirichlet_kernel n) z" if "-(2 * pi) < z" "z < 2 * pi" for z
  proof (cases "z=0")
    case True
    have *: "(λx. sin ((n + 1/2) * x) / (2 * sin (x/2))) 0  real n + 1/2"
      by real_asymp
    show ?thesis
      unfolding Dirichlet_kernel_def continuous_at True
      apply (rule Lim_transform_eventually [where f = "λx. sin((n + 1/2) * x) / (2 * sin(x/2))"])
       apply (auto simp: * eventually_at_filter)
      done
  next
    case False
    have "continuous (at z) (λx. sin((real n + 1/2) * x) / (2 * sin(x/2)))"
      using that False by (intro continuous_intros) (auto simp: sin_zero_iff)
    moreover have "F x in nhds z. x  0"
      using False t1_space_nhds by blast
    ultimately show ?thesis
      using False
      by (force simp: Dirichlet_kernel_def continuous_at eventually_at_filter elim: Lim_transform_eventually)
  qed
  then show ?thesis
    by (simp add: continuous_on_eq_continuous_at)
qed

lemma Dirichlet_kernel_continuous: "continuous_on {-pi..pi} (Dirichlet_kernel n)"
  apply (rule continuous_on_subset [OF Dirichlet_kernel_continuous_strong], clarsimp)
  using pi_gt_zero by linarith


lemma absolutely_integrable_mult_Dirichlet_kernel:
  assumes "f absolutely_integrable_on {-pi..pi}"
  shows "(λx. Dirichlet_kernel n x * f x) absolutely_integrable_on {-pi..pi}"
proof (rule absolutely_integrable_bounded_measurable_product_real)
  show "Dirichlet_kernel n  borel_measurable (lebesgue_on {-pi..pi})"
    by (simp add: Dirichlet_kernel_continuous continuous_imp_measurable_on_sets_lebesgue)
  have "compact (Dirichlet_kernel n ` {-pi..pi})"
    by (auto simp: compact_continuous_image [OF Dirichlet_kernel_continuous])
  then show "bounded (Dirichlet_kernel n ` {-pi..pi})"
    using compact_imp_bounded by blast
qed (use assms in auto)


lemma cosine_sum_lemma:
   "(1/2 + (k = Suc 0..n. cos(real k * x))) * sin(x/2) =  sin((real n + 1/2) * x) / 2"
proof -
  consider "n=0" | "n  1" by linarith
  then show ?thesis
  proof cases
    case 2
    then have "(k = Suc 0..n. (sin (real k * x + x/2) * 2 - sin (real k * x - x/2) * 2) / 2)
        = sin (real n * x + x/2) - sin (x/2)"
    proof (induction n)
      case (Suc n)
      show ?case
      proof (cases "n=0")
        case False
        with Suc show ?thesis
          by (simp add: divide_simps algebra_simps)
      qed auto
    qed auto
    then show ?thesis
      by (simp add: distrib_right sum_distrib_right cos_times_sin)
  qed auto
qed


lemma Dirichlet_kernel_cosine_sum:
  assumes "¦x¦ < 2 * pi"
  shows "Dirichlet_kernel n x = 1/2 + (k = Suc 0..n. cos(real k * x))"
proof -
  have "sin ((real n + 1/2) * x) / (2 * sin (x/2)) = 1/2 + (k = Suc 0..n. cos (real k * x))"
    if "x  0"
  proof -
    have "sin(x/2)  0"
      using assms that by (auto simp: sin_zero_iff)
    then show ?thesis
     using cosine_sum_lemma [of x n] by (simp add: divide_simps)
  qed
  then show ?thesis
    by (auto simp: Dirichlet_kernel_def)
qed

lemma integrable_Dirichlet_kernel: "integrable (lebesgue_on {-pi..pi}) (Dirichlet_kernel n)"
  using Dirichlet_kernel_continuous continuous_imp_integrable_real by blast

lemma integral_Dirichlet_kernel [simp]:
  "integralL (lebesgue_on {-pi..pi}) (Dirichlet_kernel n) = pi"
proof -
  have "integralL (lebesgue_on {-pi..pi}) (Dirichlet_kernel n) = LINT x|lebesgue_on {-pi..pi}. 1/2 + (k = Suc 0..n. cos (k * x))"
    using pi_ge_two
    by (force intro: Bochner_Integration.integral_cong [OF refl Dirichlet_kernel_cosine_sum])
  also have " = (LINT x|lebesgue_on {-pi..pi}. 1/2) + (LINT x|lebesgue_on {-pi..pi}. (k = Suc 0..n. cos (k * x)))"
  proof (rule Bochner_Integration.integral_add)
    show "integrable (lebesgue_on {-pi..pi}) (λx. k = Suc 0..n. cos (real k * x))"
      by (rule Bochner_Integration.integrable_sum) (metis integrable_cos_cx mult_commute_abs)
  qed auto
  also have " = pi"
  proof -
    have "i. Suc 0  i; i  n
          integrable (lebesgue_on {-pi..pi}) (λx. cos (real i * x))"
      by (metis integrable_cos_cx mult_commute_abs)
    then have "LINT x|lebesgue_on {-pi..pi}. (k = Suc 0..n. cos (real k * x)) = 0"
      by (simp add: Bochner_Integration.integral_sum)
    then show ?thesis
      by (auto simp: measure_restrict_space)
  qed
  finally show ?thesis .
qed

lemma integral_Dirichlet_kernel_half [simp]:
  "integralL (lebesgue_on {0..pi}) (Dirichlet_kernel n) = pi/2"
proof -
  have "integralL (lebesgue_on {- pi..0}) (Dirichlet_kernel n) +
        integralL (lebesgue_on {0..pi}) (Dirichlet_kernel n) = pi"
    using integral_combine [OF integrable_Dirichlet_kernel] integral_Dirichlet_kernel by simp
  moreover have "integralL (lebesgue_on {- pi..0}) (Dirichlet_kernel n) = integralL (lebesgue_on {0..pi}) (Dirichlet_kernel n)"
    using integral_reflect_real [of pi 0 "Dirichlet_kernel n"] by simp
  ultimately show ?thesis
    by simp
qed


lemma Fourier_sum_offset_Dirichlet_kernel:
  assumes f: "f absolutely_integrable_on {-pi..pi}" and periodic: "x. f(x + 2*pi) = f x"
  shows
   "(k2*n. Fourier_coefficient f k * trigonometric_set k t) =
            integralL (lebesgue_on {-pi..pi}) (λx. Dirichlet_kernel n x * f(x+t)) / pi"
  (is "?lhs = ?rhs")
proof -
  have ft: "(λx. f(x+t)) absolutely_integrable_on {-pi..pi}"
    using absolutely_integrable_periodic_offset [OF f, of t] periodic by simp
  have "?lhs = (k=0..n. Fourier_coefficient (λx. f(x+t)) (2*k) * trigonometric_set (2*k) 0)"
    using Fourier_sum_offset_unpaired assms atMost_atLeast0 by auto
  also have " = Fourier_coefficient (λx. f(x+t)) 0 / sqrt (2 * pi)
                 + (k = Suc 0..n. Fourier_coefficient (λx. f(x+t)) (2*k) / sqrt pi)"
    by (simp add: sum.atLeast_Suc_atMost trigonometric_set_def)
  also have " = (LINT x|lebesgue_on {-pi..pi}. f(x+t)) / (2 * pi) +
                   (k = Suc 0..n. (LINT x|lebesgue_on {-pi..pi}. cos (real k * x) * f(x+t)) / pi)"
    by (simp add: Fourier_coefficient_def orthonormal_coeff_def trigonometric_set_def l2product_def)
  also have " = LINT x|lebesgue_on {-pi..pi}.
                     f(x+t) / (2 * pi) + (k = Suc 0..n. (cos (real k * x) * f(x+t)) / pi)"
    using Fourier_products_integrable_cos [OF ft] absolutely_integrable_imp_integrable [OF ft] by simp
  also have " = (LINT x|lebesgue_on {-pi..pi}.
                     f(x+t) / 2 + (k = Suc 0..n. cos (real k * x) * f(x+t))) / pi"
    by (simp add: divide_simps sum_distrib_right mult.assoc)
  also have " = ?rhs"
  proof -
    have "LINT x|lebesgue_on {-pi..pi}. f(x + t) / 2 + (k = Suc 0..n. cos (real k * x) * f(x + t))
        = LINT x|lebesgue_on {-pi..pi}. Dirichlet_kernel n x * f(x + t)"
    proof -
      have eq: "f(x+t) / 2 + (k = Suc 0..n. cos (real k * x) * f(x + t))
              = Dirichlet_kernel n x * f(x + t)" if "- pi  x" "x  pi" for x
      proof (cases "x = 0")
        case False
        then have "sin (x/2)  0"
          using that by (auto simp: sin_zero_iff)
        then have "f(x + t) * (1/2 + (k = Suc 0..n. cos(real k * x))) = f(x + t) * sin((real n + 1/2) * x) / 2 / sin(x/2)"
          using cosine_sum_lemma [of x n] by (simp add: divide_simps)
        then show ?thesis
          by (simp add: Dirichlet_kernel_def False field_simps sum_distrib_left)
      qed (simp add: Dirichlet_kernel_def algebra_simps)
      show ?thesis
        by (rule Bochner_Integration.integral_cong [OF refl]) (simp add: eq)
    qed
    then show ?thesis by simp
  qed
  finally show ?thesis .
qed


lemma Fourier_sum_limit_Dirichlet_kernel:
  assumes f: "f absolutely_integrable_on {-pi..pi}" and periodic: "x. f(x + 2*pi) = f x"
  shows "((λn. (kn. Fourier_coefficient f k * trigonometric_set k t))  l)
      (λn. LINT x|lebesgue_on {-pi..pi}. Dirichlet_kernel n x * f(x + t))  pi * l"
    (is "?lhs = ?rhs")
proof -
  have "?lhs  (λn. (LINT x|lebesgue_on {-pi..pi}. Dirichlet_kernel n x * f(x + t)) / pi)  l"
    by (simp add: Fourier_sum_limit_pair [OF f, symmetric] Fourier_sum_offset_Dirichlet_kernel assms)
  also have "  (λk. (LINT x|lebesgue_on {-pi..pi}. Dirichlet_kernel k x * f(x + t)) * inverse pi)
                     pi * l * inverse pi"
    by (auto simp: divide_simps)
  also have "  ?rhs"
    using tendsto_mult_right_iff [of "inverse pi", symmetric] by auto
  finally show ?thesis .
qed

subsection‹A directly deduced sufficient condition for convergence at a point›

lemma simple_Fourier_convergence_periodic:
  assumes f: "f absolutely_integrable_on {-pi..pi}"
    and ft: "(λx. (f(x+t) - f t) / sin(x/2)) absolutely_integrable_on {-pi..pi}"
    and periodic: "x. f(x + 2*pi) = f x"
  shows "(λn. (kn. Fourier_coefficient f k * trigonometric_set k t))  f t"
proof -
  let  = "λn. kn. Fourier_coefficient (λx. f x - f t) k * trigonometric_set k t"
  let  = "λn. LINT x|lebesgue_on {-pi..pi}. Dirichlet_kernel n x * (f(x + t) - f t)"
  have fft: "(λx. f x - f t) absolutely_integrable_on {-pi..pi}"
    by (simp add: f absolutely_integrable_measurable_real)
  have fxt: "(λx. f(x + t)) absolutely_integrable_on {-pi..pi}"
    using absolutely_integrable_periodic_offset assms by auto
  have *: "  0    0"
    by (simp add: Fourier_sum_limit_Dirichlet_kernel fft periodic)
  moreover have "(λn. (kn. Fourier_coefficient f k * trigonometric_set k t) - f t)  0"
    if "  0"
  proof (rule Lim_transform_eventually [OF that eventually_sequentiallyI])
    show "(kn. Fourier_coefficient (λx. f x - f t) k * trigonometric_set k t)
        = (kn. Fourier_coefficient f k * trigonometric_set k t) - f t"
      if "Suc 0  n" for n
    proof -
      have "(k = Suc 0..n. Fourier_coefficient (λx. f x - f t) k * trigonometric_set k t)
          = (k = Suc 0..n. Fourier_coefficient f k * trigonometric_set k t)"
      proof (rule sum.cong [OF refl])
        fix k
        assume k: "k  {Suc 0..n}"
        then have [simp]: "integralL (lebesgue_on {-pi..pi}) (trigonometric_set k) = 0"
          by (auto simp: trigonometric_set_def)
        show "Fourier_coefficient (λx. f x - f t) k * trigonometric_set k t = Fourier_coefficient f k * trigonometric_set k t"
          using k unfolding Fourier_coefficient_def orthonormal_coeff_def l2product_def
          by (simp add: right_diff_distrib f absolutely_integrable_measurable_real trigonometric_set_mul_integrable)
      qed
      moreover have "Fourier_coefficient (λx. f x - f t) 0 * trigonometric_set 0 t =
                     Fourier_coefficient f 0 * trigonometric_set 0 t - f t"
        using f unfolding Fourier_coefficient_def orthonormal_coeff_def l2product_def
        by (auto simp: divide_simps trigonometric_set absolutely_integrable_imp_integrable measure_restrict_space)
      ultimately show ?thesis
        by (simp add: sum.atLeast_Suc_atMost atMost_atLeast0)
    qed
  qed
  moreover
  have "  0"
  proof -
    have eq: "n.  n = integralL (lebesgue_on {-pi..pi}) (λx. sin((n + 1/2) * x) * ((f(x+t) - f t) / sin(x/2) / 2))"
      unfolding Dirichlet_kernel_def
      by (rule Bochner_Integration.integral_cong [OF refl]) (auto simp: divide_simps sin_zero_iff)
    show ?thesis
      unfolding eq
      by (intro ft set_integrable_divide Riemann_lebesgue_sin_half)
  qed
  ultimately show ?thesis
    by (simp add: LIM_zero_cancel)
qed


subsection‹A more natural sufficient Hoelder condition at a point›

lemma bounded_inverse_sin_half:
  assumes "d > 0"
  obtains B where "B>0" "x. x  ({-pi..pi} - {-d<..<d})  ¦inverse (sin (x/2))¦  B"
proof -
  have "bounded ((λx. inverse (sin (x/2))) ` ({-pi..pi} - {- d<..<d}))"
  proof (intro compact_imp_bounded compact_continuous_image)
    have "x  {-pi..pi}; x  0  sin (x/2)  0" for x
      using 0 < d by (auto simp: sin_zero_iff)
    then show "continuous_on ({-pi..pi} - {-d<..<d}) (λx. inverse (sin (x/2)))"
      using 0 < d by (intro continuous_intros) auto
    show "compact ({-pi..pi} - {-d<..<d})"
      by (simp add: compact_diff)
  qed
  then show thesis
    using that by (auto simp: bounded_pos)
qed

proposition Hoelder_Fourier_convergence_periodic:
  assumes f: "f absolutely_integrable_on {-pi..pi}" and "d > 0" "a > 0"
    and ft: "x. ¦x-t¦ < d  ¦f x - f t¦  M * ¦x-t¦ powr a"
    and periodic: "x. f(x + 2*pi) = f x"
  shows "(λn. (kn. Fourier_coefficient f k * trigonometric_set k t))  f t"
proof (rule simple_Fourier_convergence_periodic [OF f])
  have half: "((λx. sin(x/2)) has_real_derivative 1/2) (at 0)"
    by (rule derivative_eq_intros refl | force)+
  then obtain e0::real where "e0 > 0" and e0: "x. x  0; ¦x¦ < e0  ¦sin (x/2) / x - 1/2¦ < 1/4"
    apply (simp add: DERIV_def Lim_at dist_real_def)
    apply (drule_tac x="1/4" in spec, auto)
    done
  obtain e where "e > 0" and e: "x. ¦x¦ < e  ¦(f(x+t) - f t) / sin (x/2)¦  4 * (¦M¦ * ¦x¦ powr (a-1))"
  proof
    show "min d e0 > 0"
      using d > 0 e0 > 0 by auto
  next
    fix x
    assume x: "¦x¦ < min d e0"
    show "¦(f(x + t) - f t) / sin (x/2)¦  4 * (¦M¦ * ¦x¦ powr (a - 1))"
    proof (cases "sin(x/2) = 0  x=0")
      case False
      have eq: "¦(f(x + t) - f t) / sin (x/2)¦ = ¦inverse (sin (x/2) / x)¦ * (¦f(x + t) - f t¦ / ¦x¦)"
        by simp
      show ?thesis
        unfolding eq
      proof (rule mult_mono)
        have "¦sin (x/2) / x - 1/2¦ < 1/4"
          using e0 [of x] x False by force
        then have "1/4  ¦sin (x/2) / x¦"
          by (simp add: abs_if field_simps split: if_split_asm)
        then show "¦inverse (sin (x/2) / x)¦  4"
          using False by (simp add: field_simps)
        have "¦f(x + t) - f t¦ / ¦x¦  M * ¦x + t - t¦ powr (a - 1)"
          using ft [of "x+t"] x by (auto simp: divide_simps algebra_simps Transcendental.powr_mult_base)
        also have "  ¦M¦ * ¦x¦ powr (a - 1)"
          by (simp add: mult_mono)
        finally show "¦f(x + t) - f t¦ / ¦x¦  ¦M¦ * ¦x¦ powr (a - 1)" .
      qed auto
    qed auto
  qed
  obtain B where "B>0" and B: "x. x  ({-pi..pi} - {- e<..<e})  ¦inverse (sin (x/2))¦  B"
    using bounded_inverse_sin_half [OF e > 0] by metis
  let ?g = "λx. max (B * ¦f(x + t) - f t¦) ((4 * ¦M¦) * ¦x¦ powr (a - 1))"
  show "(λx. (f(x + t) - f t) / sin (x/2)) absolutely_integrable_on {-pi..pi}"
  proof (rule measurable_bounded_by_integrable_imp_absolutely_integrable)
    have fxt: "(λx. f(x + t)) absolutely_integrable_on {-pi..pi}"
      using absolutely_integrable_periodic_offset assms by auto
    show "(λx. (f(x + t) - f t) / sin (x/2))  borel_measurable (lebesgue_on {-pi..pi})"
    proof (intro measurable)
      show "(λx. f(x + t))  borel_measurable (lebesgue_on {-pi..pi})"
        using absolutely_integrable_on_def fxt integrable_imp_measurable by blast
      show "(λx. sin (x/2))  borel_measurable (lebesgue_on {-pi..pi})"
        by (intro continuous_imp_measurable_on_sets_lebesgue continuous_intros) auto
    qed auto
    have "(λx. f(x + t) - f t) absolutely_integrable_on {-pi..pi}"
      by (intro set_integral_diff fxt) (simp add: set_integrable_def)
    moreover
    have "(λx. ¦x¦ powr (a - 1)) absolutely_integrable_on {-pi..pi}"
    proof -
      have "((λx. x powr (a - 1)) has_integral
       inverse a * pi powr a - inverse a * 0 powr a)
       {0..pi}"
      proof (rule fundamental_theorem_of_calculus_interior)
        show "continuous_on {0..pi} (λx. inverse a * x powr a)"
          using a > 0
          by (intro continuous_on_powr' continuous_intros) auto
        show "((λb. inverse a * b powr a) has_vector_derivative x powr (a - 1)) (at x)"
          if "x  {0<..<pi}" for x
          using that a > 0
          apply (simp flip: has_real_derivative_iff_has_vector_derivative)
          apply (rule derivative_eq_intros | simp)+
          done
      qed auto
      then have int: "(λx. x powr (a - 1)) integrable_on {0..pi}"
        by blast
      show ?thesis
      proof (rule nonnegative_absolutely_integrable_1)
        show "(λx. ¦x¦ powr (a - 1)) integrable_on {-pi..pi}"
        proof (rule Henstock_Kurzweil_Integration.integrable_combine)
          show "(λx. ¦x¦ powr (a - 1)) integrable_on {0..pi}"
            using int integrable_eq by fastforce
          then show "(λx. ¦x¦ powr (a - 1)) integrable_on {- pi..0}"
            using Henstock_Kurzweil_Integration.integrable_reflect_real by fastforce
        qed auto
      qed auto
    qed
    ultimately show "?g integrable_on {-pi..pi}"
      apply (intro set_lebesgue_integral_eq_integral absolutely_integrable_max_1 absolutely_integrable_bounded_measurable_product_real set_integrable_abs measurable)
              apply (auto simp: image_constant_conv)
      done
    show "norm ((f(x + t) - f t) / sin (x/2))  ?g x" if "x  {-pi..pi}" for x
    proof (cases "¦x¦ < e")
      case True
      then show ?thesis
        using e [OF True] by (simp add: max_def)
    next
      case False
      then have "¦inverse (sin (x/2))¦  B"
        using B that by force
      then have "¦inverse (sin (x/2))¦ * ¦f(x + t) - f t¦  B * ¦f(x + t) - f t¦"
        by (simp add: mult_right_mono)
      then have "¦f(x + t) - f t¦ / ¦sin (x/2)¦  B * ¦f(x + t) - f t¦"
        by (simp add: divide_simps split: if_split_asm)
      then show ?thesis
        by auto
    qed
  qed auto
qed (auto simp: periodic)


text‹In particular, a Lipschitz condition at the point›
corollary Lipschitz_Fourier_convergence_periodic:
  assumes f: "f absolutely_integrable_on {-pi..pi}" and "d > 0"
    and ft: "x. ¦x-t¦ < d  ¦f x - f t¦  M * ¦x-t¦"
    and periodic: "x. f(x + 2*pi) = f x"
  shows "(λn. (kn. Fourier_coefficient f k * trigonometric_set k t))  f t"
  using Hoelder_Fourier_convergence_periodic [OF f d > 0, of 1] assms
  by (fastforce simp add:)

text‹In particular, if left and right derivatives both exist›
proposition bi_differentiable_Fourier_convergence_periodic:
  assumes f: "f absolutely_integrable_on {-pi..pi}"
    and f_lt: "f differentiable at_left t"
    and f_gt: "f differentiable at_right t"
    and periodic: "x. f(x + 2*pi) = f x"
  shows "(λn. (kn. Fourier_coefficient f k * trigonometric_set k t))  f t"
proof -
  obtain D_lt where D_lt: "e. e > 0  d>0. x<t. 0 < dist x t  dist x t < d  dist ((f x - f t) / (x - t)) D_lt < e"
    using f_lt unfolding has_field_derivative_iff real_differentiable_def Lim_within
    by (meson lessThan_iff)
  then obtain d_lt where "d_lt > 0"
    and d_lt: "x. x < t; 0 < ¦x - t¦; ¦x - t¦ < d_lt  ¦(f x - f t) / (x - t) - D_lt¦ < 1"
    unfolding dist_real_def by (metis dist_commute dist_real_def zero_less_one)
  obtain D_gt where D_gt: "e. e > 0  d>0. x>t. 0 < dist x t  dist x t < d  dist ((f x - f t) / (x - t)) D_gt < e"
    using f_gt unfolding has_field_derivative_iff real_differentiable_def Lim_within
    by (meson greaterThan_iff)
  then obtain d_gt where "d_gt > 0"
    and d_gt: "x. x > t; 0 < ¦x - t¦; ¦x - t¦ < d_gt  ¦(f x - f t) / (x - t) - D_gt¦ < 1"
    unfolding dist_real_def by (metis dist_commute dist_real_def zero_less_one)
  show ?thesis
  proof (rule Lipschitz_Fourier_convergence_periodic [OF f])
    fix x
    assume "¦x - t¦ < min d_lt d_gt"
    then have *: "¦x - t¦ < d_lt" "¦x - t¦ < d_gt"
      by auto
    consider "x<t" | "x=t" | "x>t"
      by linarith
    then show "¦f x - f t¦  (¦D_lt¦ + ¦D_gt¦ + 1)  * ¦x - t¦"
    proof cases
      case 1
      then have "¦(f x - f t) / (x - t) - D_lt¦ < 1"
        using d_lt [OF 1] * by auto
      then have "¦(f x - f t) / (x - t)¦ - ¦D_lt¦ < 1"
        by linarith
      then have "¦f x - f t¦  (¦D_lt¦ + 1) * ¦x - t¦"
        by (simp add: comm_semiring_class.distrib divide_simps split: if_split_asm)
      also have "  (¦D_lt¦ + ¦D_gt¦ + 1) * ¦x - t¦"
        by (simp add: mult_right_mono)
      finally show ?thesis .
    next
      case 3
      then have "¦(f x - f t) / (x - t) - D_gt¦ < 1"
        using d_gt [OF 3] * by auto
      then have "¦(f x - f t) / (x - t)¦ - ¦D_gt¦ < 1"
        by linarith
      then have "¦f x - f t¦  (¦D_gt¦ + 1) * ¦x - t¦"
        by (simp add: comm_semiring_class.distrib divide_simps split: if_split_asm)
      also have "  (¦D_lt¦ + ¦D_gt¦ + 1) * ¦x - t¦"
        by (simp add: mult_right_mono)
      finally show ?thesis .
    qed auto
  qed (auto simp: 0 < d_gt 0 < d_lt periodic)
qed


text‹And in particular at points where the function is differentiable›
lemma differentiable_Fourier_convergence_periodic:
  assumes f: "f absolutely_integrable_on {-pi..pi}"
    and fdif: "f differentiable (at t)"
    and periodic: "x. f(x + 2*pi) = f x"
  shows "(λn. (kn. Fourier_coefficient f k * trigonometric_set k t))  f t"
  by (rule bi_differentiable_Fourier_convergence_periodic) (auto simp: differentiable_at_withinI assms)

text‹Use reflection to halve the region of integration›
lemma absolutely_integrable_mult_Dirichlet_kernel_reflected:
  assumes f: "f absolutely_integrable_on {-pi..pi}"
    and periodic: "x. f(x + 2*pi) = f x"
  shows "(λx. Dirichlet_kernel n x * f(t+x)) absolutely_integrable_on {-pi..pi}"
        "(λx. Dirichlet_kernel n x * f(t-x)) absolutely_integrable_on {-pi..pi}"
        "(λx. Dirichlet_kernel n x * c) absolutely_integrable_on {-pi..pi}"
proof -
  show "(λx. Dirichlet_kernel n x * f(t+x)) absolutely_integrable_on {-pi..pi}"
    apply (rule absolutely_integrable_mult_Dirichlet_kernel)
    using absolutely_integrable_periodic_offset [OF f, of t] periodic
    apply simp
    done
  then show "(λx. Dirichlet_kernel n x * f(t-x)) absolutely_integrable_on {-pi..pi}"
    by (subst absolutely_integrable_reflect_real [symmetric]) simp
  show "(λx. Dirichlet_kernel n x * c) absolutely_integrable_on {-pi..pi}"
    by (simp add: absolutely_integrable_measurable_real borel_measurable_integrable integrable_Dirichlet_kernel)
qed


lemma absolutely_integrable_mult_Dirichlet_kernel_reflected_part:
  assumes f: "f absolutely_integrable_on {-pi..pi}"
    and periodic: "x. f(x + 2*pi) = f x" and "d  pi"
  shows "(λx. Dirichlet_kernel n x * f(t+x)) absolutely_integrable_on {0..d}"
        "(λx. Dirichlet_kernel n x * f(t-x)) absolutely_integrable_on {0..d}"
        "(λx. Dirichlet_kernel n x * c) absolutely_integrable_on {0..d}"
  using absolutely_integrable_mult_Dirichlet_kernel_reflected [OF f periodic, of n] d  pi
  by (force intro: absolutely_integrable_on_subinterval)+

lemma absolutely_integrable_mult_Dirichlet_kernel_reflected_part2:
  assumes f: "f absolutely_integrable_on {-pi..pi}"
    and periodic: "x. f(x + 2*pi) = f x" and "d  pi"
  shows "(λx. Dirichlet_kernel n x * (f(t+x) + f(t-x))) absolutely_integrable_on {0..d}"
        "(λx. Dirichlet_kernel n x * ((f(t+x) + f(t-x)) - c)) absolutely_integrable_on {0..d}"
  using absolutely_integrable_mult_Dirichlet_kernel_reflected_part assms
  by (simp_all add: distrib_left right_diff_distrib)

lemma integral_reflect_and_add:
  fixes f :: "real  'b::euclidean_space"
  assumes "integrable (lebesgue_on {-a..a}) f"
  shows "integralL (lebesgue_on {-a..a}) f = integralL (lebesgue_on {0..a})  (λx. f x + f(-x))"
proof (cases "a  0")
  case True
  have f: "integrable (lebesgue_on {0..a}) f" "integrable (lebesgue_on {-a..0}) f"
    using integrable_subinterval assms by fastforce+
  then have fm: "integrable (lebesgue_on {0..a}) (λx. f(-x))"
    using integrable_reflect_real by fastforce
  have "integralL (lebesgue_on {-a..a}) f = integralL (lebesgue_on {-a..0}) f + integralL (lebesgue_on {0..a}) f"
    by (simp add: True assms integral_combine)
  also have " = integralL (lebesgue_on {0..a}) (λx. f(-x)) + integralL (lebesgue_on {0..a}) f"
    by (metis (no_types) add.inverse_inverse add.inverse_neutral integral_reflect_real)
  also have " = integralL (lebesgue_on {0..a}) (λx. f x + f(-x))"
    by (simp add: fm f)
  finally show ?thesis .
qed (use assms in auto)

lemma Fourier_sum_offset_Dirichlet_kernel_half:
  assumes f: "f absolutely_integrable_on {-pi..pi}"
    and periodic: "x. f(x + 2*pi) = f x"
  shows "(k2*n. Fourier_coefficient f k * trigonometric_set k t) - l
       = (LINT x|lebesgue_on {0..pi}. Dirichlet_kernel n x * (f(t+x) + f(t-x) - 2*l)) / pi"
proof -
  have fxt: "(λx. f(x + t)) absolutely_integrable_on {-pi..pi}"
    using absolutely_integrable_periodic_offset assms by auto
  have int: "integrable (lebesgue_on {0..pi}) (Dirichlet_kernel n)"
    using not_integrable_integral_eq by fastforce
  have "LINT x|lebesgue_on {-pi..pi}. Dirichlet_kernel n x * f(x + t)
      = LINT x|lebesgue_on {0..pi}. Dirichlet_kernel n x * f(x + t) + Dirichlet_kernel n (- x) * f(- x + t)"
    by (simp add: integral_reflect_and_add absolutely_integrable_imp_integrable absolutely_integrable_mult_Dirichlet_kernel fxt)
  also have " = (LINT x|lebesgue_on {0..pi}. Dirichlet_kernel n x * (f(t+x) + f(t-x) - 2*l)) + pi * l"
    using absolutely_integrable_mult_Dirichlet_kernel_reflected_part [OF f periodic order_refl, of n t]
    apply (simp add: algebra_simps absolutely_integrable_imp_integrable int)
    done
  finally show ?thesis
    by (simp add: Fourier_sum_offset_Dirichlet_kernel assms divide_simps)
qed

lemma Fourier_sum_limit_Dirichlet_kernel_half:
  assumes f: "f absolutely_integrable_on {-pi..pi}"
    and periodic: "x. f(x + 2*pi) = f x"
  shows "(λn. (kn. Fourier_coefficient f k * trigonometric_set k t))  l
      (λn. (LINT x|lebesgue_on {0..pi}. Dirichlet_kernel n x * (f(t+x) + f(t-x) - 2*l)))  0"
  apply (simp flip: Fourier_sum_limit_pair [OF f])
  apply (simp add: Lim_null [where l=l] Fourier_sum_offset_Dirichlet_kernel_half assms)
  done


subsection‹Localization principle: convergence only depends on values "nearby"›

proposition Riemann_localization_integral:
  assumes f: "f absolutely_integrable_on {-pi..pi}" and g: "g absolutely_integrable_on {-pi..pi}"
    and "d > 0" and d: "x. ¦x¦ < d  f x = g x"
  shows "(λn. integralL (lebesgue_on {-pi..pi}) (λx. Dirichlet_kernel n x * f x)
            - integralL (lebesgue_on {-pi..pi}) (λx. Dirichlet_kernel n x * g x))
          0"  (is "?a  0")
proof -
  let ?f = "λx. (if ¦x¦ < d then 0 else f x - g x) / sin(x/2) / 2"
  have eq: "?a n = integralL (lebesgue_on {-pi..pi}) (λx. sin((n+1/2) * x) * ?f x)" for n
  proof -
    have "?a n = integralL (lebesgue_on {-pi..pi}) (λx. Dirichlet_kernel n x * (if ¦x¦ < d then 0 else f x - g x))"
      apply (simp add: absolutely_integrable_imp_integrable absolutely_integrable_mult_Dirichlet_kernel f g flip: Bochner_Integration.integral_diff)
      apply (auto simp: d algebra_simps intro: Bochner_Integration.integral_cong)
      done
    also have " = integralL (lebesgue_on {-pi..pi}) (λx. sin((n+1/2) * x) * ?f x)"
      using d > 0 by (auto simp: Dirichlet_kernel_def intro: Bochner_Integration.integral_cong)
    finally show ?thesis .
  qed
  show ?thesis
    unfolding eq
  proof (rule Riemann_lebesgue_sin_half)
    obtain B where "B>0" and B: "x. x  ({-pi..pi} - {-d<..<d})  ¦inverse (sin (x/2))¦  B"
      using bounded_inverse_sin_half [OF d > 0] by metis
    have "(λx. (if ¦x¦ < d then 0 else f x - g x) / sin (x/2)) absolutely_integrable_on {-pi..pi}"
    proof (rule measurable_bounded_by_integrable_imp_absolutely_integrable)
      show "(λx. (if ¦x¦ < d then 0 else f x - g x) / sin (x/2))  borel_measurable (lebesgue_on {-pi..pi})"
      proof (intro measurable)
        show "f  borel_measurable (lebesgue_on {-pi..pi})" "g  borel_measurable (lebesgue_on {-pi..pi})"
          using absolutely_integrable_on_def f g integrable_imp_measurable by blast+
        show "(λx. x)  borel_measurable (lebesgue_on {-pi..pi})"
             "(λx. sin (x/2))  borel_measurable (lebesgue_on {-pi..pi})"
          by (intro continuous_intros continuous_imp_measurable_on_sets_lebesgue | force)+
      qed auto
      have "(λx. B * ¦f x - g x¦) absolutely_integrable_on {-pi..pi}"
        using B > 0 by (simp add: f g set_integrable_abs)
      then show "(λx. B * ¦f x - g x¦) integrable_on {-pi..pi}"
        using absolutely_integrable_on_def by blast
    next
      fix x
      assume x: "x  {-pi..pi}"
      then have [simp]: "sin (x/2) = 0  x=0"
        using 0 < d by (force simp: sin_zero_iff)
      show "norm ((if ¦x¦ < d then 0 else f x - g x) / sin (x/2))  B * ¦f x - g x¦"
      proof (cases "¦x¦ < d")
        case False
        then have "1  B * ¦sin (x/2)¦"
          using B > 0 B [of x] x d > 0
          by (auto simp: abs_less_iff divide_simps split: if_split_asm)
        then have "1 * ¦f x - g x¦  B * ¦sin (x/2)¦ * ¦f x - g x¦"
          by (metis (full_types) abs_ge_zero mult.commute mult_left_mono)
        then show ?thesis
          using False by (auto simp: divide_simps algebra_simps)
      qed (simp add: d)
    qed auto
    then show "(λx. (if ¦x¦ < d then 0 else f x - g x) / sin (x/2) / 2) absolutely_integrable_on {-pi..pi}"
      using set_integrable_divide by blast
  qed
qed

lemma Riemann_localization_integral_range:
  assumes f: "f absolutely_integrable_on {-pi..pi}"
    and "0 < d" "d  pi"
  shows "(λn. integralL (lebesgue_on {-pi..pi}) (λx. Dirichlet_kernel n x * f x)
            - integralL (lebesgue_on {-d..d}) (λx. Dirichlet_kernel n x * f x))
              0"
proof -
  have *: "(λn. (LINT x|lebesgue_on {-pi..pi}. Dirichlet_kernel n x * f x)
              - (LINT x|lebesgue_on {-pi..pi}. Dirichlet_kernel n x * (if x  {-d..d} then f x else 0)))
            0"
  proof (rule Riemann_localization_integral [OF f _ 0 < d])
    have "f absolutely_integrable_on {-d..d}"
      using f absolutely_integrable_on_subinterval d  pi by fastforce
    moreover have "(λx. if - pi  x  x  pi then if x  {-d..d} then f x else 0  else 0)
                 = (λx. if x  {-d..d} then f x else 0)"
      using d  pi by force
    ultimately
    show "(λx. if x  {-d..d} then f x else 0) absolutely_integrable_on {-pi..pi}"
      apply (subst absolutely_integrable_restrict_UNIV [symmetric])
      apply (simp flip: absolutely_integrable_restrict_UNIV [of "{-d..d}" f])
      done
  qed auto
  then show ?thesis
    using integral_restrict [of "{-d..d}" "{-pi..pi}" "λx. Dirichlet_kernel _ x * f x"] assms
    by (simp add: if_distrib cong: if_cong)
qed

lemma Riemann_localization:
  assumes f: "f absolutely_integrable_on {-pi..pi}" and g: "g absolutely_integrable_on {-pi..pi}"
    and perf: "x. f(x + 2*pi) = f x"
    and perg: "x. g(x + 2*pi) = g x"
    and "d > 0" and d: "x. ¦x-t¦ < d  f x = g x"
  shows "(λn. kn. Fourier_coefficient f k * trigonometric_set k t)  c
      (λn. kn. Fourier_coefficient g k * trigonometric_set k t)  c"
proof -
  have "(λn. LINT x|lebesgue_on {-pi..pi}. Dirichlet_kernel n x * f(x + t))  pi * c
     (λn. LINT x|lebesgue_on {-pi..pi}. Dirichlet_kernel n x * g (x + t))  pi * c"
  proof (intro Lim_transform_eq Riemann_localization_integral)
    show "(λx. f(x + t)) absolutely_integrable_on {-pi..pi}" "(λx. g (x + t)) absolutely_integrable_on {-pi..pi}"
      using assms by (auto intro: absolutely_integrable_periodic_offset)
  qed (use assms in auto)
  then show ?thesis
    by (simp add: Fourier_sum_limit_Dirichlet_kernel assms)
qed

subsection‹Localize the earlier integral›

lemma Riemann_localization_integral_range_half:
  assumes f: "f absolutely_integrable_on {-pi..pi}"
    and "0 < d" "d  pi"
  shows "(λn. (LINT x|lebesgue_on {0..pi}. Dirichlet_kernel n x * (f x + f(-x)))
            - (LINT x|lebesgue_on {0..d}. Dirichlet_kernel n x * (f x + f(-x))))  0"
proof -
  have *: "(λx. Dirichlet_kernel n x * f x) absolutely_integrable_on {-d..d}" for n
    by (metis (full_types) absolutely_integrable_mult_Dirichlet_kernel absolutely_integrable_on_subinterval
              d  pi atLeastatMost_subset_iff f neg_le_iff_le)
  show ?thesis
    using absolutely_integrable_mult_Dirichlet_kernel [OF f]
    using Riemann_localization_integral_range [OF assms]
    apply (simp add: "*" absolutely_integrable_imp_integrable integral_reflect_and_add)
    apply (simp add: algebra_simps)
    done
qed


lemma Fourier_sum_limit_Dirichlet_kernel_part:
  assumes f: "f absolutely_integrable_on {-pi..pi}"
    and periodic: "x. f(x + 2*pi) = f x"
    and d: "0 < d" "d  pi"
  shows "(λn. kn. Fourier_coefficient f k * trigonometric_set k t)  l
      (λn. (LINT x|lebesgue_on {0..d}. Dirichlet_kernel n x * ((f(t+x) + f(t-x)) - 2*l)))  0"
proof -
  have "(λx. f(t+x)) absolutely_integrable_on {-pi..pi}"
    using absolutely_integrable_periodic_offset [OF f, of t] periodic by simp
  then have int: "(λx. f(t+x) - l) absolutely_integrable_on {-pi..pi}"
    by auto
  have "(λn. LINT x|lebesgue_on {0..pi}. Dirichlet_kernel n x * (f(t+x) + f(t-x) - 2*l))  0
     (λn. LINT x|lebesgue_on {0..d}. Dirichlet_kernel n x * (f(t+x) + f(t-x) - 2*l))  0"
    by (rule Lim_transform_eq) (use Riemann_localization_integral_range_half [OF int d] in auto)
  then show ?thesis
    by (simp add: Fourier_sum_limit_Dirichlet_kernel_half assms)
qed

subsection‹Make a harmless simplifying tweak to the Dirichlet kernel›

lemma inte_Dirichlet_kernel_mul_expand:
  assumes f: "f  borel_measurable (lebesgue_on S)" and S: "S  sets lebesgue"
  shows "(LINT x|lebesgue_on S. Dirichlet_kernel n x * f x
        = LINT x|lebesgue_on S. sin((n+1/2) * x) * f x / (2 * sin(x/2)))
        (integrable (lebesgue_on S) (λx. Dirichlet_kernel n x * f x)
       integrable (lebesgue_on S) (λx. sin((n+1/2) * x) * f x / (2 * sin(x/2))))"
proof (cases "0  S")
  case True
  have *: "{x. x = 0  x  S}  sets (lebesgue_on S)"
    using True  by (simp add: S sets_restrict_space_iff cong: conj_cong)
  have bm1: "(λx. Dirichlet_kernel n x * f x)  borel_measurable (lebesgue_on S)"
    unfolding Dirichlet_kernel_def
    by (force intro: * assms measurable continuous_imp_measurable_on_sets_lebesgue continuous_intros)
  have bm2: "(λx. sin ((n + 1/2) * x) * f x / (2 * sin (x/2)))  borel_measurable (lebesgue_on S)"
    by (intro assms measurable continuous_imp_measurable_on_sets_lebesgue continuous_intros) auto
  have 0: "{0}  null_sets (lebesgue_on S)"
    using True by (simp add: S null_sets_restrict_space)
  show ?thesis
    apply (intro conjI integral_cong_AE integrable_cong_AE bm1 bm2 AE_I' [OF 0])
    unfolding Dirichlet_kernel_def  by auto
next
  case False
  then show ?thesis
    unfolding Dirichlet_kernel_def by (auto intro!: Bochner_Integration.integral_cong Bochner_Integration.integrable_cong)
qed

lemma
  assumes f: "f  borel_measurable (lebesgue_on S)" and S: "S  sets lebesgue"
  shows integral_Dirichlet_kernel_mul_expand:
        "(LINT x|lebesgue_on S. Dirichlet_kernel n x * f x)
       = (LINT x|lebesgue_on S. sin((n+1/2) * x) * f x / (2 * sin(x/2)))" (is "?th1")
  and integrable_Dirichlet_kernel_mul_expand:
       "integrable (lebesgue_on S) (λx. Dirichlet_kernel n x * f x)
     integrable (lebesgue_on S) (λx. sin((n+1/2) * x) * f x / (2 * sin(x/2)))" (is "?th2")
  using inte_Dirichlet_kernel_mul_expand [OF assms] by auto


proposition Fourier_sum_limit_sine_part:
  assumes f: "f absolutely_integrable_on {-pi..pi}"
    and periodic: "x. f(x + 2*pi) = f x"
    and d: "0 < d" "d  pi"
  shows "(λn. (kn. Fourier_coefficient f k * trigonometric_set k t))  l
      (λn. LINT x|lebesgue_on {0..d}. sin((n + 1/2) * x) * ((f(t+x) + f(t-x) - 2*l) / x))  0"
    (is "?lhs    0")
proof -
  have ftx: "(λx. f(t+x)) absolutely_integrable_on {-pi..pi}"
    using absolutely_integrable_periodic_offset assms by auto
  then have ftmx: "(λx. f(t-x)) absolutely_integrable_on {-pi..pi}"
    by (simp flip: absolutely_integrable_reflect_real [where f= "(λx. f(t+x))"])
  have fbm: "(λx. f(t+x) + f(t-x) - 2*l) absolutely_integrable_on {-pi..pi}"
    by (force intro: ftmx ftx)
  let  = "λn. LINT x|lebesgue_on {0..d}. Dirichlet_kernel n x * ((f(t+x) + f(t-x)) - 2*l)"
  have "?lhs    0"
    by (intro Fourier_sum_limit_Dirichlet_kernel_part assms)
  moreover have "  0    0"
  proof (rule Lim_transform_eq [OF Lim_transform_eventually])
    let ?f = "λn. LINT x|lebesgue_on {0..d}. sin((real n + 1/2) * x) * (1 / (2 * sin(x/2)) - 1/x) * (f(t+x) + f(t-x) - 2*l)"
    have "?f n = (LINT x|lebesgue_on {-pi..pi}.
            sin ((n + 1/2) * x) * ((if x  {0..d} then 1 / (2 * sin (x/2)) - 1/x else 0) * (f(t+x) + f(t-x) - 2*l)))" for n
      using d by (simp add: integral_restrict if_distrib [of "λu. _ * (u * _)"] mult.assoc flip: atLeastAtMost_iff cong: if_cong)
    moreover have "  0"
    proof (intro Riemann_lebesgue_sin_half absolutely_integrable_bounded_measurable_product_real)
      have "(λx. 1 / (2 * sin(x/2)) - 1/x)  borel_measurable (lebesgue_on {0..d})"
        by (intro measurable continuous_imp_measurable_on_sets_lebesgue continuous_intros) auto
      then show "(λx. if x  {0..d} then 1 / (2 * sin(x/2)) - 1/x else 0)  borel_measurable (lebesgue_on {-pi..pi})"
        using d by (simp add: borel_measurable_if_lebesgue_on flip: atLeastAtMost_iff)

      let ?g = "λx::real. 1 / (2 * sin(x/2)) - 1/x"
      have limg: "(?g  ?g a) (at a within {0..d})"   ―‹thanks to Manuel Eberl›
        if a: "0  a" "a  d" for a
      proof -
        have "(?g  0) (at_right 0)" and "(?g  ?g d) (at_left d)"
          using d sin_gt_zero[of "d/2"] by (real_asymp simp: field_simps)+
        moreover have "(?g  ?g a) (at a)" if "a > 0"
          using a that d sin_gt_zero[of "a/2"] that by (real_asymp simp: field_simps)
        ultimately show ?thesis using that d
          by (cases "a = 0  a = d") (auto simp: at_within_Icc_at at_within_Icc_at_right at_within_Icc_at_left)
      qed
      have "((λx. if x  {0..d} then 1 / (2 * sin(x/2)) - 1/x else 0) ` {-pi..pi}) = ((λx. 1 / (2 * sin(x/2)) - 1/x) ` {0..d})"
        using d  by (auto intro: image_eqI [where x=0])
      moreover have "bounded "
        by (intro compact_imp_bounded compact_continuous_image) (auto simp: continuous_on limg)
      ultimately show "bounded ((λx. if x  {0..d} then 1 / (2 * sin(x/2)) - 1/x else 0) ` {-pi..pi})"
        by simp
    qed (auto simp: fbm)
    ultimately show "?f  (0::real)"
      by simp
    show "F n in sequentially. ?f n =  n -  n"
    proof (rule eventually_sequentiallyI [where c = "Suc 0"])
      fix n
      assume "n  Suc 0"
      have "integrable (lebesgue_on {0..d}) (λx. sin ((real n + 1/2) * x) * (f(t+x) + f(t-x) - 2*l) / (2 * sin(x/2)))"
        using d
        apply (subst integrable_Dirichlet_kernel_mul_expand [symmetric])
          apply (intro assms absolutely_integrable_imp_borel_measurable absolutely_integrable_on_subinterval [OF fbm]
                       absolutely_integrable_imp_integrable absolutely_integrable_mult_Dirichlet_kernel_reflected_part2 | force)+
        done
      moreover have "integrable (lebesgue_on {0..d}) (λx. sin ((real n + 1/2) * x) * (f(t+x) + f(t-x) - 2*l) / x)"
      proof (rule integrable_cong_AE_imp)
        let ?g = "λx. Dirichlet_kernel n x * (2 * sin(x/2) / x * (f(t+x) + f(t-x) - 2*l))"
        have *: "¦2 * sin (x/2) / x¦  1" for x::real
          using abs_sin_x_le_abs_x [of "x/2"]
          by (simp add: divide_simps mult.commute abs_mult)
        have "bounded ((λx. 1 + (x/2)2) ` {-pi..pi})"
          by (intro compact_imp_bounded compact_continuous_image continuous_intros) auto
        then have bo: "bounded ((λx. 2 * sin (x/2) / x) ` {-pi..pi})"
          using * unfolding bounded_real by blast
        show "integrable (lebesgue_on {0..d}) ?g"
          using d
          apply (intro absolutely_integrable_imp_integrable
              absolutely_integrable_on_subinterval [OF absolutely_integrable_mult_Dirichlet_kernel]
              absolutely_integrable_bounded_measurable_product_real bo fbm
              measurable continuous_imp_measurable_on_sets_lebesgue continuous_intros, auto)
          done
        show "(λx. sin ((n + 1/2) * x) * (f(t+x) + f(t-x) - 2*l) / x)  borel_measurable (lebesgue_on {0..d})"
          using d
          apply (intro measurable absolutely_integrable_imp_borel_measurable
                       absolutely_integrable_on_subinterval [OF ftx] absolutely_integrable_on_subinterval [OF ftmx]
                       absolutely_integrable_continuous_real continuous_intros, auto)
          done
        have "Dirichlet_kernel n x * (2 * sin(x/2)) / x = sin ((real n + 1/2) * x) / x"
          if "0 < x" "x  d" for x
          using that d by (simp add: Dirichlet_kernel_def divide_simps sin_zero_pi_iff)
        then show "AE x in lebesgue_on {0..d}. ?g x = sin ((real n + 1/2) * x) * (f(t+x) + f(t-x) - 2*l) / x"
          using d by (force intro: AE_I' [where N="{0}"])
      qed
      ultimately have "?f n = (LINT x|lebesgue_on {0..d}. sin ((n + 1/2) * x) * (f(t+x) + f(t-x) - 2*l) / (2 * sin(x/2)))
                 - (LINT x|lebesgue_on {0..d}. sin ((n + 1/2) * x) * (f(t+x) + f(t-x) - 2*l) / x)"
        by (simp add: right_diff_distrib [of _ _ "1/_"] left_diff_distrib)
      also have " =  n -  n"
        using d
        by (simp add: measurable_restrict_mono [OF absolutely_integrable_imp_borel_measurable [OF fbm]]
                      integral_Dirichlet_kernel_mul_expand)
      finally show "?f n =  n -  n" .
    qed
  qed
  ultimately show ?thesis
    by simp
qed


subsection‹Dini's test for the convergence of a Fourier series›

proposition Fourier_Dini_test:
  assumes f: "f absolutely_integrable_on {-pi..pi}"
    and periodic: "x. f(x + 2*pi) = f x"
    and int0d: "integrable (lebesgue_on {0..d}) (λx. ¦f(t+x) + f(t-x) - 2*l¦ / x)"
    and "0 < d"
  shows "(λn. (kn. Fourier_coefficient f k * trigonometric_set k t))  l"
proof -
  define φ where "φ  λn x. sin((n + 1/2) * x) * ((f(t+x) + f(t-x) - 2*l) / x)"
  have "(λn. LINT x|lebesgue_on {0..pi}. φ n x)  0"
    unfolding lim_sequentially dist_real_def
  proof (intro allI impI)
    fix e :: real
    assume "e > 0"
    define θ where "θ  λx. LINT x|lebesgue_on {0..x}. ¦f(t+x) + f(t-x) - 2*l¦ / x"
    have [simp]: "θ 0 = 0"
      by (simp add: θ_def integral_eq_zero_null_sets)
    have cont: "continuous_on {0..d} θ"
      unfolding θ_def using indefinite_integral_continuous_real int0d by blast
    with d > 0
    have "e>0. da>0. x'{0..d}. ¦x' - 0¦ < da  ¦θ x' - θ 0¦ < e"
      by (force simp: continuous_on_real_range dest: bspec [where x=0])
    with e > 0
    obtain k where "k > 0" and k: "x'. 0  x'; x' < k; x'  d  ¦θ x'¦ < e/2"
      by (drule_tac x="e/2" in spec) auto
    define δ where "δ  min d (min (k/2) pi)"
    have e2: "¦θ δ¦ < e/2" and "δ > 0" "δ  pi"
      unfolding δ_def using k k > 0 d > 0 by auto
    have ftx: "(λx. f(t+x)) absolutely_integrable_on {-pi..pi}"
      using absolutely_integrable_periodic_offset assms by auto
    then have ftmx: "(λx. f(t-x)) absolutely_integrable_on {-pi..pi}"
      by (simp flip: absolutely_integrable_reflect_real [where f= "(λx. f(t+x))"])
    have 1: "φ n absolutely_integrable_on {0..δ}" for n::nat
      unfolding φ_def
    proof (rule absolutely_integrable_bounded_measurable_product_real)
      show "(λx. sin ((real n + 1/2) * x))  borel_measurable (lebesgue_on {0..δ})"
        by (intro continuous_imp_measurable_on_sets_lebesgue continuous_intros) auto
      show "bounded ((λx. sin ((real n + 1/2) * x)) ` {0..δ})"
        by (simp add: bounded_iff) (use abs_sin_le_one in blast)
      have "(λx. (f(t+x) + f(t-x) - 2*l) / x)  borel_measurable (lebesgue_on {0..δ})"
        using d > 0 unfolding δ_def
        by (intro measurable absolutely_integrable_imp_borel_measurable
            absolutely_integrable_on_subinterval [OF ftx] absolutely_integrable_on_subinterval [OF ftmx]
            absolutely_integrable_continuous_real continuous_intros, auto)
      moreover have "integrable (lebesgue_on {0..δ}) (norm  (λx. (f(t+x) + f(t-x) - 2*l) / x))"
      proof (rule integrable_subinterval [of 0 d])
        show "integrable (lebesgue_on {0..d}) (norm  (λx. (f(t+x) + f(t-x) - 2*l) / x))"
          using int0d by (subst Bochner_Integration.integrable_cong) (auto simp: o_def)
        show "{0..δ}  {0..d}"
          using d > 0 by (auto simp: δ_def)
      qed
      ultimately show "(λx. (f(t+x) + f(t-x) - 2*l) / x) absolutely_integrable_on {0..δ}"
        by (auto simp: absolutely_integrable_measurable)
    qed auto
    have 2: "φ n absolutely_integrable_on {δ..pi}" for n::nat
      unfolding φ_def
    proof (rule absolutely_integrable_bounded_measurable_product_real)
      show "(λx. sin ((n + 1/2) * x))  borel_measurable (lebesgue_on {δ..pi})"
        by (intro continuous_imp_measurable_on_sets_lebesgue continuous_intros) auto
      show "bounded ((λx. sin ((n + 1/2) * x)) ` {δ..pi})"
        by (simp add: bounded_iff) (use abs_sin_le_one in blast)
    have "(λx. inverse x * (f(t+x) + f(t-x) - 2*l)) absolutely_integrable_on {δ..pi}"
    proof (rule absolutely_integrable_bounded_measurable_product_real)
      have "(λx. 1/x)  borel_measurable (lebesgue_on {δ..pi})"
        by (auto simp: measurable_completion measurable_restrict_space1)
      then show "inverse  borel_measurable (lebesgue_on {δ..pi})"
        by (metis (no_types, lifting) inverse_eq_divide measurable_lebesgue_cong)
      have "x{δ..pi}. inverse ¦x¦  inverse δ"
        using 0 < δ by auto
      then show "bounded (inverse ` {δ..pi})"
        by (auto simp: bounded_iff)
      show "(λx. f(t+x) + f(t-x) - 2*l) absolutely_integrable_on {δ..pi}"
      proof (rule absolutely_integrable_on_subinterval)
        show "(λx. (f(t+x) + f(t-x) - 2*l)) absolutely_integrable_on {-pi..pi}"
          by (fast intro: ftx ftmx absolutely_integrable_on_const)
        show "{δ..pi}  {-pi..pi}"
          using 0 < δ by auto
      qed
    qed auto
    then show "(λx. (f(t+x) + f(t-x) - 2*l) / x) absolutely_integrable_on {δ..pi}"
      by (metis (no_types, lifting) divide_inverse mult.commute set_integrable_cong)
  qed auto
  have "(λx. f(t+x) - l) absolutely_integrable_on {-pi..pi}"
    using ftx by auto
  moreover have "bounded ((λx. 0) ` {x. ¦x¦ < δ})"
    using bounded_def by blast
  moreover have "bounded (inverse ` {x. ¬ ¦x¦ < δ})"
    using δ > 0 by (auto simp: divide_simps intro: boundedI [where B = "1/δ"])
  ultimately have "(λx. (if ¦x¦ < δ then 0 else inverse x) * (if x  {-pi..pi} then f(t+x) - l else 0)) absolutely_integrable_on UNIV"
    apply (intro absolutely_integrable_bounded_measurable_product_real measurable set_integral_diff)
          apply (auto simp: lebesgue_on_UNIV_eq measurable_completion simp flip: absolutely_integrable_restrict_UNIV [where S = "{-pi..pi}"])
    done
  moreover have "(if x  {-pi..pi} then if ¦x¦ < δ then 0 else (f(t+x) - l) / x else 0)
               = (if ¦x¦ < δ then 0 else inverse x) * (if x  {-pi..pi} then f(t+x) - l else 0)"  for x
    by (auto simp: divide_simps)
  ultimately have *: "(λx. if ¦x¦ < δ then 0 else (f(t+x) - l) / x) absolutely_integrable_on {-pi..pi}"
    by (simp add: flip: absolutely_integrable_restrict_UNIV [where S = "{-pi..pi}"])
  have "(λn. LINT x|lebesgue_on {0..pi}. sin ((n + 1/2) * x) * (if ¦x¦ < δ then 0 else (f(t+x) - l) / x)
                                       + sin ((n + 1/2) * -x) * (if ¦x¦ < δ then 0 else (f(t-x) - l) / -x))
         0"
    using Riemann_lebesgue_sin_half [OF *] *
    by (simp add: integral_reflect_and_add absolutely_integrable_imp_integrable absolutely_integrable_sin_product cong: if_cong)
  moreover have "sin ((n + 1/2) * x) * (if ¦x¦ < δ then 0 else (f(t+x) - l) / x)
               + sin ((n + 1/2) * -x) * (if ¦x¦ < δ then 0 else (f(t-x) - l) / -x)
           = (if ¬ ¦x¦ < δ then φ n x else 0)" for x n
    by simp (auto simp: divide_simps algebra_simps φ_def)
  ultimately have "(λn. LINT x|lebesgue_on {0..pi}. (if ¬ ¦x¦ < δ then φ n x else 0))  0"
    by simp
  moreover have "(if 0  x  x  pi then if ¬ ¦x¦ < δ then φ n x else 0 else 0)
               = (if δ  x  x  pi then φ n x else 0)" for x n
    using δ > 0 by auto
  ultimately have : "(λn. LINT x|lebesgue_on {δ..pi}. φ n x)  0"
    by (simp flip: Lebesgue_Measure.integral_restrict_UNIV)
  then obtain N::nat where N: "n. nN  ¦LINT x|lebesgue_on {δ..pi}. φ n x¦ < e/2"
    unfolding lim_sequentially dist_real_def
    by (metis (full_types) 0 < e diff_zero half_gt_zero_iff)
  have "¦integralL (lebesgue_on {0..pi}) (φ n)¦ < e" if "n  N" for n::nat
  proof -
    have int: "integrable (lebesgue_on {0..pi}) (φ (real n))"
      by (intro integrable_combine [of concl: 0 pi] absolutely_integrable_imp_integrable) (use  δ > 0  δ  pi 1 2 in auto)
    then have "integralL (lebesgue_on {0..pi}) (φ n) = integralL (lebesgue_on {0..δ}) (φ n) + integralL (lebesgue_on {δ..pi}) (φ n)"
      by (rule integral_combine) (use 0 < δ δ  pi in auto)
    moreover have "¦integralL (lebesgue_on {0..δ}) (φ n)¦  LINT x|lebesgue_on {0..δ}. ¦f(t + x) + f(t - x) - 2 * l¦ / x"
    proof (rule integral_abs_bound_integral)
      show "integrable (lebesgue_on {0..δ}) (φ (real n))"
        by (meson integrable_subinterval δ  pi int atLeastatMost_subset_iff order_refl)
      have "{0..δ}  {0..d}"
        by (auto simp: δ_def)
      then show "integrable (lebesgue_on {0..δ}) (λx. ¦f(t + x) + f(t - x) - 2 * l¦ / x)"
        by (rule integrable_subinterval [OF int0d])
      show "¦φ (real n) x¦  ¦f(t + x) + f(t - x) - 2 * l¦ / x"
        if "x  space (lebesgue_on {0..δ})" for x
        using that
        apply (auto simp: φ_def divide_simps abs_mult)
        by (simp add: mult.commute mult_left_le)
    qed
    ultimately have "¦integralL (lebesgue_on {0..pi}) (φ n)¦ < e/2 + e/2"
      using N [OF that] e2 unfolding θ_def by linarith
    then show ?thesis
      by simp
  qed
  then show "N. nN. ¦integralL (lebesgue_on {0..pi}) (φ (real n)) - 0¦ < e"
    by force
qed
  then show ?thesis
    unfolding φ_def using Fourier_sum_limit_sine_part assms pi_gt_zero by blast
qed


subsection‹Cesaro summability of Fourier series using Fejér kernel›

definition Fejer_kernel :: "nat  real  real"
  where
  "Fejer_kernel  λn x. if n = 0 then 0 else (r<n. Dirichlet_kernel r x) / n"

lemma Fejer_kernel:
     "Fejer_kernel n x =
        (if n = 0 then 0
         else if x = 0 then n/2
         else sin(n / 2 * x) ^ 2 / (2 * n * sin(x/2) ^ 2))"
proof (cases "x=0  sin(x/2) = 0")
  case True
  have "(r<n. (1 + real r * 2)) = real n * real n"
    by (induction n) (auto simp: algebra_simps)
  with True show ?thesis
    by (auto simp: Fejer_kernel_def Dirichlet_kernel_def field_simps simp flip: sum_divide_distrib)
next
  case False
  have "sin (x/2) * (r<n. sin ((real r * 2 + 1) * x / 2)) =
        sin (real n * x / 2) * sin (real n * x / 2)"
  proof (induction n)
  next
    case (Suc n)
    then show ?case
      apply (simp add: field_simps sin_times_sin)
      apply (simp add: add_divide_distrib)
      done
  qed auto
  then show ?thesis
    using False
    unfolding Fejer_kernel_def Dirichlet_kernel_def
    by (simp add: divide_simps power2_eq_square mult.commute flip: sum_divide_distrib)
qed

lemma Fejer_kernel_0 [simp]: "Fejer_kernel 0 x = 0"  "Fejer_kernel n 0 = n/2"
  by (auto simp: Fejer_kernel)

lemma Fejer_kernel_continuous_strong:
  "continuous_on {-(2 * pi)<..<2 * pi} (Fejer_kernel n)"
proof (cases "n=0")
  case False
  then show ?thesis
  by (simp add: Fejer_kernel_def continuous_intros Dirichlet_kernel_continuous_strong)
qed (simp add: Fejer_kernel_def)

lemma Fejer_kernel_continuous:
  "continuous_on {-pi..pi} (Fejer_kernel n)"
  apply (rule continuous_on_subset [OF Fejer_kernel_continuous_strong])
  apply (simp add: subset_iff)
  using pi_gt_zero apply linarith
  done


lemma absolutely_integrable_mult_Fejer_kernel:
  assumes "f absolutely_integrable_on {-pi..pi}"
  shows "(λx. Fejer_kernel n x * f x) absolutely_integrable_on {-pi..pi}"
proof (rule absolutely_integrable_bounded_measurable_product_real)
  show "Fejer_kernel n  borel_measurable (lebesgue_on {-pi..pi})"
    by (simp add: Fejer_kernel_continuous continuous_imp_measurable_on_sets_lebesgue)
  show "bounded (Fejer_kernel n ` {-pi..pi})"
    using Fejer_kernel_continuous compact_continuous_image compact_imp_bounded by blast
qed (use assms in auto)


lemma absolutely_integrable_mult_Fejer_kernel_reflected1:
  assumes f: "f absolutely_integrable_on {-pi..pi}"
    and periodic: "x. f(x + 2*pi) = f x"
  shows "(λx. Fejer_kernel n x * f(t + x)) absolutely_integrable_on {-pi..pi}"
  using assms
  by (force intro: absolutely_integrable_mult_Fejer_kernel absolutely_integrable_periodic_offset)

lemma absolutely_integrable_mult_Fejer_kernel_reflected2:
  assumes f: "f absolutely_integrable_on {-pi..pi}"
    and periodic: "x. f(x + 2*pi) = f x"
  shows "(λx. Fejer_kernel n x * f(t - x)) absolutely_integrable_on {-pi..pi}"
proof -
  have "(λx. f(t - x)) absolutely_integrable_on {-pi..pi}"
    using assms
    apply (subst absolutely_integrable_reflect_real [symmetric])
    apply (simp add: absolutely_integrable_periodic_offset)
    done
  then show ?thesis
    by (rule absolutely_integrable_mult_Fejer_kernel)
qed

lemma absolutely_integrable_mult_Fejer_kernel_reflected3:
  shows "(λx. Fejer_kernel n x * c) absolutely_integrable_on {-pi..pi}"
  using absolutely_integrable_on_const absolutely_integrable_mult_Fejer_kernel by blast


lemma absolutely_integrable_mult_Fejer_kernel_reflected_part1:
  assumes f: "f absolutely_integrable_on {-pi..pi}"
    and periodic: "x. f(x + 2*pi) = f x" and "d  pi"
  shows "(λx. Fejer_kernel n x * f(t + x)) absolutely_integrable_on {0..d}"
  by (rule absolutely_integrable_on_subinterval [OF absolutely_integrable_mult_Fejer_kernel_reflected1]) (auto simp: assms)

lemma absolutely_integrable_mult_Fejer_kernel_reflected_part2:
  assumes f: "f absolutely_integrable_on {-pi..pi}"
    and periodic: "x. f(x + 2*pi) = f x" and "d  pi"
  shows "(λx. Fejer_kernel n x * f(t - x)) absolutely_integrable_on {0..d}"
  by (rule absolutely_integrable_on_subinterval [OF absolutely_integrable_mult_Fejer_kernel_reflected2]) (auto simp: assms)

lemma absolutely_integrable_mult_Fejer_kernel_reflected_part3:
  assumes "d  pi"
  shows "(λx. Fejer_kernel n x * c) absolutely_integrable_on {0..d}"
  by (rule absolutely_integrable_on_subinterval [OF absolutely_integrable_mult_Fejer_kernel_reflected2]) (auto simp: assms)

lemma absolutely_integrable_mult_Fejer_kernel_reflected_part4:
  assumes f: "f absolutely_integrable_on {-pi..pi}"
    and periodic: "x. f(x + 2*pi) = f x" and "d  pi"
  shows "(λx. Fejer_kernel n x * (f(t + x) + f(t - x))) absolutely_integrable_on {0..d}"
  unfolding distrib_left
  by (intro set_integral_add absolutely_integrable_mult_Fejer_kernel_reflected_part1 absolutely_integrable_mult_Fejer_kernel_reflected_part2 assms)

lemma absolutely_integrable_mult_Fejer_kernel_reflected_part5:
  assumes f: "f absolutely_integrable_on {-pi..pi}"
    and periodic: "x. f(x + 2*pi) = f x" and "d  pi"
  shows "(λx. Fejer_kernel n x * ((f(t + x) + f(t - x)) - c)) absolutely_integrable_on {0..d}"
  unfolding distrib_left right_diff_distrib
  by (intro set_integral_add set_integral_diff absolutely_integrable_on_const
      absolutely_integrable_mult_Fejer_kernel_reflected_part1 absolutely_integrable_mult_Fejer_kernel_reflected_part2 assms, auto)


lemma Fourier_sum_offset_Fejer_kernel_half:
  fixes n::nat
  assumes f: "f absolutely_integrable_on {-pi..pi}"
    and periodic: "x. f(x + 2*pi) = f x" and "n > 0"
  shows "(r<n. k2*r. Fourier_coefficient f k * trigonometric_set k t) / n - l
       = (LINT x|lebesgue_on {0..pi}. Fejer_kernel n x * (f(t + x) + f(t - x) - 2 * l)) / pi"
proof -
  have "(r<n. k2 * r. Fourier_coefficient f k * trigonometric_set k t) - real n * l
       = (r<n. (k2 * r. Fourier_coefficient f k * trigonometric_set k t) - l)"
    by (simp add: sum_subtractf)
  also have " = (r<n.
                      (LINT x|lebesgue_on {0..pi}. Dirichlet_kernel r x * (f(t + x) + f(t - x) - 2 * l)) / pi)"
    by (simp add: Fourier_sum_offset_Dirichlet_kernel_half assms)
  also have " = real n * ((LINT x|lebesgue_on {0..pi}. Fejer_kernel n x * (f(t + x) + f(t - x) - 2 * l)) / pi)"
  proof -
    have "integrable (lebesgue_on {0..pi}) (λx. Dirichlet_kernel i x * (f(t + x) + f(t - x) - 2 * l))" for i
      using absolutely_integrable_mult_Dirichlet_kernel_reflected_part2(2) f periodic
      by (force simp: intro!: absolutely_integrable_imp_integrable)
    then show ?thesis
      using n > 0
      apply (simp add: Fejer_kernel_def flip: sum_divide_distrib)
      apply (simp add: sum_distrib_right flip: Bochner_Integration.integral_sum [symmetric])
      done
  qed
  finally have "(r<n. k2 * r. Fourier_coefficient f k * trigonometric_set k t) - real n * l = real n * ((LINT x|lebesgue_on {0..pi}. Fejer_kernel n x * (f(t + x) + f(t - x) - 2 * l)) / pi)" .
  with n > 0 show ?thesis
    by (auto simp: mult.commute divide_simps)
qed


lemma Fourier_sum_limit_Fejer_kernel_half:
  fixes n::nat
  assumes f: "f absolutely_integrable_on {-pi..pi}"
    and periodic: "x. f(x + 2*pi) = f x"
  shows "(λn. ((r<n. k2*r. Fourier_coefficient f k * trigonometric_set k t)) / n)  l
         
         ((λn. integralL (lebesgue_on {0..pi}) (λx. Fejer_kernel n x * ((f(t + x) + f(t - x)) - 2*l)))   0)"
        (is "?lhs = ?rhs")
proof -
  have "?lhs 
        (λn. ((r<n. k2*r.  Fourier_coefficient f k * trigonometric_set k t)) / n - l)  0"
    by (simp add: LIM_zero_iff)
  also have " 
        (λn. ((((r<n. k2*r.  Fourier_coefficient f k * trigonometric_set k t)) / n) - l) * pi)  0"
    using tendsto_mult_right_iff [OF pi_neq_zero] by simp
  also have "  ?rhs"
    apply (intro Lim_transform_eq [OF Lim_transform_eventually [of "λn. 0"]] eventually_sequentiallyI [of 1])
    apply (simp_all add: Fourier_sum_offset_Fejer_kernel_half assms)
    done
  finally show ?thesis .
qed


lemma has_integral_Fejer_kernel:
  "has_bochner_integral (lebesgue_on {-pi..pi}) (Fejer_kernel n) (if n = 0 then 0 else pi)"
proof -
  have "has_bochner_integral (lebesgue_on {-pi..pi}) (λx. (r<n. Dirichlet_kernel r x) / real n) ((r<n. pi) / n)"
    by (simp add: has_bochner_integral_iff integrable_Dirichlet_kernel has_bochner_integral_divide has_bochner_integral_sum)
  then show ?thesis
    by (auto simp: Fejer_kernel_def)
qed

lemma has_integral_Fejer_kernel_half:
  "has_bochner_integral (lebesgue_on {0..pi}) (Fejer_kernel n) (if n = 0 then 0 else pi/2)"
proof -
  have "has_bochner_integral (lebesgue_on {0..pi}) (λx. (r<n. Dirichlet_kernel r x) / real n) ((r<n. pi/2) / n)"
    apply (intro has_bochner_integral_sum has_bochner_integral_divide)
    using not_integrable_integral_eq by (force simp: has_bochner_integral_iff)
  then show ?thesis
    by (auto simp: Fejer_kernel_def)
qed

lemma Fejer_kernel_pos_le [simp]: "Fejer_kernel n x  0"
  by (simp add: Fejer_kernel)


theorem Fourier_Fejer_Cesaro_summable:
  assumes f: "f absolutely_integrable_on {-pi..pi}"
    and periodic: "x. f(x + 2*pi) = f x"
    and fl: "(f  l) (at t within atMost t)"
    and fr: "(f  r) (at t within atLeast t)"
  shows "(λn. (m<n. k2*m. Fourier_coefficient f k * trigonometric_set k t) / n)  (l+r) / 2"
proof -
  define h where "h  λu. (f(t+u) + f(t-u)) - (l+r)"
  have "(λn. LINT u|lebesgue_on {0..pi}. Fejer_kernel n u * h u)  0"
  proof -
    have h0: "(h  0) (at 0 within atLeast 0)"
    proof -
      have l0: "((λu. f(t-u) - l)  0) (at 0 within {0..})"
        using fl
        unfolding Lim_within
        apply (elim all_forward imp_forward ex_forward conj_forward asm_rl, clarify)
        apply (drule_tac x="t-x" in bspec)
         apply (auto simp: dist_norm)
        done
      have r0: "((λu. f(t + u) - r)  0) (at 0 within {0..})"
        using fr
        unfolding Lim_within
        apply (elim all_forward imp_forward ex_forward conj_forward asm_rl, clarify)
        apply (drule_tac x="t+x" in bspec)
         apply (auto simp: dist_norm)
        done
      show ?thesis
        using tendsto_add [OF l0 r0] by (simp add: h_def algebra_simps)
    qed
    show ?thesis
      unfolding lim_sequentially dist_real_def diff_0_right
    proof clarify
      fix e::real
      assume "e > 0"
      then obtain x' where "0 < x'" "x. 0 < x; x < x'  ¦h x¦ < e / (2 * pi)"
        using h0 unfolding Lim_within dist_real_def
        by (auto simp: dest: spec [where x="e/2/pi"])
      then obtain ξ where "0 < ξ" "ξ < pi" and ξ: "x. 0 < x  x  ξ  ¦h x¦ < e/2/pi"
        apply (intro that [where ξ="min x' pi/2"], auto)
        using m2pi_less_pi by linarith
      have ftx: "(λx. f(t+x)) absolutely_integrable_on {-pi..pi}"
        using absolutely_integrable_periodic_offset assms by auto
      then have ftmx: "(λx. f(t-x)) absolutely_integrable_on {-pi..pi}"
        by (simp flip: absolutely_integrable_reflect_real [where f= "(λx. f(t+x))"])
      have h_aint: "h absolutely_integrable_on {-pi..pi}"
        unfolding h_def
        by (intro absolutely_integrable_on_const set_integral_diff set_integral_add, auto simp: ftx ftmx)
      have "(λn. LINT x|lebesgue_on {ξ..pi}. Fejer_kernel n x * h x)  0"
      proof (rule Lim_null_comparison)
        define φ where "φ  λn. (LINT x|lebesgue_on {ξ..pi}. ¦h x¦ / (2 * sin(x/2) ^ 2)) / n"
        show "F n in sequentially. norm (LINT x|lebesgue_on {ξ..pi}. Fejer_kernel n x * h x)  φ n"
        proof (rule eventually_sequentiallyI)
          fix n::nat assume "n  1"
          have hint: "(λx. h x / (2 * sin(x/2) ^ 2)) absolutely_integrable_on {ξ..pi}"
            unfolding divide_inverse mult.commute [of "h _"]
          proof (rule absolutely_integrable_bounded_measurable_product_real)
            have cont: "continuous_on {ξ..pi} (λx. inverse (2 * (sin (x * inverse 2))2))"
              using 0 < ξ by (intro continuous_intros) (auto simp: sin_zero_pi_iff)
            show "(λx. inverse (2 * (sin (x * inverse 2))2))  borel_measurable (lebesgue_on {ξ..pi})"
              using 0 < ξ
              by (intro cont continuous_imp_measurable_on_sets_lebesgue) auto
            show "bounded ((λx. inverse (2 * (sin (x * inverse 2))2)) ` {ξ..pi})"
              using cont by (simp add: compact_continuous_image compact_imp_bounded)
            show "h absolutely_integrable_on {ξ..pi}"
              using 0 < ξ ξ < pi by (auto intro: absolutely_integrable_on_subinterval [OF h_aint])
          qed auto
          then have *: "integrable (lebesgue_on {ξ..pi}) (λx. ¦h x¦ / (2 * (sin (x/2))2))"
            by (simp add: absolutely_integrable_measurable o_def)
          define ψ where
              "ψ  λx. (if n = 0 then 0 else if x = 0 then n/2
                         else (sin (real n / 2 * x))2 / (2 * real n * (sin (x/2))2)) * h x"
          have "¦LINT x|lebesgue_on {ξ..pi}. ψ x¦
               (LINT x|lebesgue_on {ξ..pi}. ¦h x¦ / (2 * (sin (x/2))2) / n)"
          proof (rule integral_abs_bound_integral)
            show **: "integrable (lebesgue_on {ξ..pi}) (λx. ¦h x¦ / (2 * (sin (x/2))2) / n)"
              using Bochner_Integration.integrable_mult_left [OF *, of "1/n"]
              by (simp add: field_simps)
            show : "¦ψ x¦  ¦h x¦ / (2 * (sin (x/2))2) / real n"
              if "x  space (lebesgue_on {ξ..pi})" for x
              using that 0 < ξ
              apply (simp add: ψ_def divide_simps mult_less_0_iff abs_mult)
              apply (auto simp: square_le_1 mult_left_le_one_le)
              done
            show "integrable (lebesgue_on {ξ..pi}) ψ"
            proof (rule measurable_bounded_by_integrable_imp_lebesgue_integrable [OF _ **])
              let ?g = "λx. ¦h x¦ / (2 * sin(x/2) ^ 2) / n"
              have ***: "integrable (lebesgue_on {ξ..pi}) (λx. (sin (n/2 * x))2 * (inverse (2 * (sin (x/2))2) * h x))"
              proof (rule absolutely_integrable_imp_integrable [OF absolutely_integrable_bounded_measurable_product_real])
                show "(λx. (sin (real n / 2 * x))2)  borel_measurable (lebesgue_on {ξ..pi})"
                  by (intro continuous_imp_measurable_on_sets_lebesgue continuous_intros) auto
                show "bounded ((λx. (sin (real n / 2 * x))2) ` {ξ..pi})"
                  by (force simp: square_le_1 intro: boundedI [where B=1])
                show "(λx. inverse (2 * (sin (x/2))2) * h x) absolutely_integrable_on {ξ..pi}"
                  using hint by (simp add: divide_simps)
              qed auto
              show "ψ  borel_measurable (lebesgue_on {ξ..pi})"
                apply (rule borel_measurable_integrable)
                apply (rule Bochner_Integration.integrable_cong [where f = "λx. sin(n / 2 * x) ^ 2 / (2 * n * sin(x/2) ^ 2) * h x", OF refl, THEN iffD1])
                using 0 < ξ **
                 apply (force simp: ψ_def divide_simps algebra_simps mult_less_0_iff abs_mult)
                using Bochner_Integration.integrable_mult_left [OF ***, of "1/n"]
                by (simp add: field_simps)
              show "norm (ψ x)  ?g x" if "x  {ξ..pi}" for x
                using that  by (simp add: ψ_def)
            qed auto
          qed
          then show "norm (LINT x|lebesgue_on {ξ..pi}. Fejer_kernel n x * h x)  φ n"
            by (simp add: Fejer_kernel φ_def ψ_def flip: Bochner_Integration.integral_divide [OF *])
        qed
        show "φ  0"
          unfolding φ_def divide_inverse
          by (simp add: tendsto_mult_right_zero lim_inverse_n)
      qed
      then obtain N where N: "n. n  N  ¦LINT x|lebesgue_on {ξ..pi}. Fejer_kernel n x * h x¦ < e/2"
        unfolding lim_sequentially by (metis half_gt_zero_iff norm_conv_dist real_norm_def e > 0)
      show "N. nN. ¦(LINT u|lebesgue_on {0..pi}. Fejer_kernel n u * h u)¦ < e"
      proof (intro exI allI impI)
        fix n :: nat
        assume n: "n  max 1 N"
        with N have 1: "¦LINT x|lebesgue_on {ξ..pi}. Fejer_kernel n x * h x¦ < e/2"
          by simp
        have "integralL (lebesgue_on {0..ξ}) (Fejer_kernel n)  integralL (lebesgue_on {0..pi}) (Fejer_kernel n)"
         using ξ < pi has_bochner_integral_iff has_integral_Fejer_kernel_half
         by (force intro!: integral_mono_lebesgue_on_AE)
        also have "  pi"
          using has_integral_Fejer_kernel_half by (simp add: has_bochner_integral_iff)
        finally have int_le_pi: "integralL (lebesgue_on {0..ξ}) (Fejer_kernel n)  pi" .
        have 2: "¦LINT x|lebesgue_on {0..ξ}. Fejer_kernel n x * h x¦  (LINT x|lebesgue_on {0..ξ}. Fejer_kernel n x * e/2/pi)"
        proof -
          have eq: "integralL (lebesgue_on {0..ξ}) (λx. Fejer_kernel n x * h x)
                  = integralL (lebesgue_on {0..ξ}) (λx. Fejer_kernel n x * (if x = 0 then 0 else h x))"
          proof (rule integral_cong_AE)
            have : "{u. u  0  P u}  {0..ξ} = {0}  Collect P  {0..ξ}"
              "{u. u  0  P u}  {0..ξ} = (Collect P  {0..ξ}) - {0}" for P
              using 0 < ξ by auto
            have *: "- {0}  A  {0..ξ} = A  {0..ξ} - {0}" for A
              by auto
            show "(λx. Fejer_kernel n x * h x)  borel_measurable (lebesgue_on {0..ξ})"
              using ξ < pi
              by (intro absolutely_integrable_imp_borel_measurable h_aint
                  absolutely_integrable_on_subinterval [OF absolutely_integrable_mult_Fejer_kernel], auto)
            then show "(λx. Fejer_kernel n x * (if x = 0 then 0 else h x))  borel_measurable (lebesgue_on {0..ξ})"
              apply (simp add: in_borel_measurable Ball_def vimage_def Collect_conj_eq Collect_imp_eq * flip: Collect_neg_eq)
              apply (elim all_forward imp_forward asm_rl)
              using 0 < ξ
              apply (auto simp:  sets.insert_in_sets sets_restrict_space_iff cong: conj_cong)
              done
            have 0: "{0}  null_sets (lebesgue_on {0..ξ})"
              using 0 < ξ by (simp add: null_sets_restrict_space)
            then show "AE x in lebesgue_on {0..ξ}. Fejer_kernel n x * h x = Fejer_kernel n x * (if x = 0 then 0 else h x)"
              by (auto intro: AE_I' [OF 0])
          qed
          show ?thesis
            unfolding eq
          proof (rule integral_abs_bound_integral)
            have "(λx. if x = 0 then 0 else h x) absolutely_integrable_on {- pi..pi}"
            proof (rule absolutely_integrable_spike [OF h_aint])
              show "negligible {0}"
                by auto
            qed auto
            with 0 < ξ ξ < pi show "integrable (lebesgue_on {0..ξ}) (λx. Fejer_kernel n x * (if x = 0 then 0 else h x))"
              by (intro absolutely_integrable_imp_integrable h_aint absolutely_integrable_on_subinterval [OF absolutely_integrable_mult_Fejer_kernel]) auto
            show "integrable (lebesgue_on {0..ξ}) (λx. Fejer_kernel n x * e / 2 / pi)"
              by (simp add: absolutely_integrable_imp_integrable ξ < pi absolutely_integrable_mult_Fejer_kernel_reflected_part3 less_eq_real_def)
            show "¦Fejer_kernel n x * (if x = 0 then 0 else h x)¦  Fejer_kernel n x * e / 2 / pi"
              if "x  space (lebesgue_on {0..ξ})" for x
              using that ξ [of x] e > 0
              by (auto simp: abs_mult eq simp flip: times_divide_eq_right intro: mult_left_mono)
          qed
        qed
        have 3: "  e/2"
          using int_le_pi 0 < e
          by (simp add: divide_simps mult.commute [of e])

        have "integrable (lebesgue_on {0..pi}) (λx. Fejer_kernel n x * h x)"
          unfolding h_def
          by (simp add: absolutely_integrable_imp_integrable absolutely_integrable_mult_Fejer_kernel_reflected_part5 assms)
        then have "LINT x|lebesgue_on {0..pi}. Fejer_kernel n x * h x
                 = (LINT x|lebesgue_on {0..ξ}. Fejer_kernel n x * h x) + (LINT x|lebesgue_on {ξ..pi}. Fejer_kernel n x * h x)"
          by (rule integral_combine) (use  0 < ξ ξ < pi in auto)
        then show "¦LINT u|lebesgue_on {0..pi}. Fejer_kernel n u * h u¦ < e"
          using 1 2 3 by linarith
      qed
    qed
  qed
  then show ?thesis
    unfolding h_def by (simp add: Fourier_sum_limit_Fejer_kernel_half assms add_divide_distrib)
qed

corollary Fourier_Fejer_Cesaro_summable_simple:
  assumes f: "continuous_on UNIV f"
    and periodic: "x. f(x + 2*pi) = f x"
  shows "(λn. (m<n. k2*m. Fourier_coefficient f k * trigonometric_set k x) / n)  f x"
proof -
  have "(λn. (m<n. k2*m. Fourier_coefficient f k * trigonometric_set k x) / n)  (f x + f x) / 2"
  proof (rule Fourier_Fejer_Cesaro_summable)
    show "f absolutely_integrable_on {- pi..pi}"
      using absolutely_integrable_continuous_real continuous_on_subset f by blast
    show "(f  f x) (at x within {..x})"  "(f  f x) (at x within {x..})"
      using Lim_at_imp_Lim_at_within continuous_on_def f by blast+
  qed (auto simp: periodic Lim_at_imp_Lim_at_within continuous_on_def f)
  then show ?thesis
    by simp
qed

end