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 - (∑i∈I. a i * w i x)))⇧2 =
        (l2norm S f)⇧2 + (∑i∈I. (a i)⇧2) -  2 * (∑i∈I. a i * orthonormal_coeff S w f i)"
proof -
  have "S ∈ sets lebesgue"
    using f square_integrable_def by blast
  then have "(λx. ∑i∈I. 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 - (∑i∈I. orthonormal_coeff S w f i * w i x))
       ≤ l2norm S (λx. f x - (∑i∈I. 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 * (∑i∈I. a i * l2product S f(w i)) ≤ (∑i∈I. (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 "(∑i∈I. (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. ∑i∈I ∩ {..n}. (orthonormal_coeff S w f i)⇧2)"
    by (auto simp: incseq_def intro: sum_mono2)
  moreover have "⋀i. (∑i∈I ∩ {..i}. (orthonormal_coeff S w f i)⇧2) ≤ (l2norm S f)⇧2"
    by (simp add: Bessel_inequality assms)
  ultimately obtain L where "(λn. ∑i∈I ∩ {..n}. (orthonormal_coeff S w f i)⇧2) ⇢ L"
    using incseq_convergent by blast
  then have "∀r>0. ∃no. ∀n≥no. ¦(∑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 -(∑i∈I. orthonormal_coeff S w f i * w i x)))⇧2 =
         (l2norm S f)⇧2 - (∑i∈I. (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. (∑i∈I ∩ {..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. (∑i∈I ∩ 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. ∀m≥N. ∀n≥N. 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. ⟦m≥M; n≥M⟧ ⟹ dist (sum ?Ψ {..m}) (sum ?Ψ {..n}) < e⇧2"
      using ‹e > 0› unfolding Cauchy_def by (drule_tac x="e^2" in spec) auto
    have "⟦m≥M; n≥M⟧ ⟹ 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
            ≤ ¦(∑i∈I ∩ {..n}. (orthonormal_coeff S w f i)⇧2) - (∑i∈I ∩ {..m}. (orthonormal_coeff S w f i)⇧2)¦"
      proof (simp add: sum_diff)
        have "(l2norm S (?Θ {Suc m..n}))⇧2
            = (∑i∈I ∩ {Suc m..n}. l2product S (λx. ∑j∈I ∩ {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 "… = (∑i∈I ∩ {Suc m..n}. ∑j∈I ∩ {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 "… ≤ ¦∑i∈I ∩ {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 ≤ ¦∑i∈I ∩ {Suc m..n}. (orthonormal_coeff S w f i)⇧2¦" .
      qed
      also have "… < e⇧2"
        using M [OF ‹n≥M› ‹m≥M›]
        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. (∑i∈I ∩ {..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. (∑i∈I ∩ {..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. (∑i∈I ∩ 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 "integral⇧L (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
  "integral⇧L (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)"
  "integral⇧L (lebesgue_on {-pi..pi}) (λx. cos(m * x) * sin(n * x)) = 0"
  "integral⇧L (lebesgue_on {-pi..pi}) (λx. sin(m * x) * cos(n * x)) = 0"
  "⟦m ≥ 0; n ≥ 0⟧ ⟹ integral⇧L (lebesgue_on {-pi..pi}) (λx. sin (m * x) * sin (n * x)) = (if m = n ∧ n ≠ 0 then pi else 0)"
  "¦integral⇧L (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
  "integral⇧L (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)"
  "integral⇧L (lebesgue_on {-pi..pi}) (λx. cos(m * x) * sin(n * x)) = 0"
  "integral⇧L (lebesgue_on {-pi..pi}) (λx. sin(m * x) * cos(n * x)) = 0"
  "¦integral⇧L (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 "integral⇧L (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 - (∑k≤n. 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 "∃f∈cx_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. (∑k≤n. 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. ∑k≤n1. 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. ∑k≤n2. 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. ∑i∈S. 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. ∑k≤n. 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 ≤ nat⌊n⌋. 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 ≤ nat⌊n⌋. 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. ∑k≤n1. 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. ∑k≤n2. 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)) = (∑k≤n. 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 θ - (∑k≤n. 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 d⇧2 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. d⇧2)"
    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) ≤ d⇧2"
  proof
    show "norm ((if x ≤ a+1 / real (Suc k) then real (Suc k) * d * (a+1 / real (Suc k) - x) else 0)⇧2) ≤ d⇧2"
      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. integral⇧L (lebesgue_on {a..b}) (?f k)) ⇢ integral⇧L (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 ⟹ ¦integral⇧L (lebesgue_on {a..b}) (?f k) - integral⇧L (lebesgue_on {a..b}) ?g¦ < e⇧2"
    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 *: "¦integral⇧L (lebesgue_on {a..b}) (?f (max M N)) - integral⇧L (lebesgue_on {a..b}) ?g¦ < e⇧2"
    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 - (∑k≤n. a k * sin(real k * x) + b k * cos(real k * x))) < e"
proof -
  let ?φ = "λn a b x. ∑k≤n. 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 - (∑k≤n. a k * trigonometric_set k x)) < e"
proof -
  obtain n a b where lee:
    "l2norm {-pi..pi} (λx. f x - (∑k≤n. 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 "(∑k≤n. b k * cos (real k * x)) = (∑i≤n. if i = 0 then b 0 else b i * cos (real i * x))" for x
      by (rule sum.cong) auto
    moreover have "(∑k≤n. a k * sin (real k * x)) = (∑i≤n. (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 "(∑j≤n'. 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 "(∑k≤n. 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 - (∑i≤n. 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. (∑i≤n. orthonormal_coeff {-pi..pi} trigonometric_set f i * trigonometric_set i x)"
  show "∃N. ∀n≥N. ¦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 - (∑k≤N. 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 - (∑k≤N. a k * trigonometric_set k x))"
        proof -
          have "(∑i≤m. (if i ≤ N then a i else 0) * trigonometric_set i x) = (∑i≤N. 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 - (∑i≤m. (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: "integral⇧L (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. ∀n≥no. dist (Fourier_coefficient f n) 0 < e"
    by auto
qed


lemma Riemann_lebesgue_sin:
  assumes "f absolutely_integrable_on {-pi..pi}"
  shows "(λn. integral⇧L (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. ∀n≥no. 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. integral⇧L (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. ∀n≥no. 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 = "integral⇧L (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. ∑k≤2 * n. Fourier_coefficient f k * trigonometric_set k t) ⇢ l
     ⟷ (λn. ∑k≤n. 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 ⟹ ¦(∑k≤2 * 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. ∀n≥no. ¦(∑k≤n. 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 "¦(∑k≤n. 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 "¦(∑k≤2 * (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:
  "(∑k≤n. 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 "(∑k≤n. Fourier_coefficient f k * trigonometric_set k 0) =
          (integral⇧L (lebesgue_on {-pi..pi}) f / 2 +
           (∑k = Suc 0..n div 2. integral⇧L (lebesgue_on {-pi..pi}) (λx. cos(k * x) * f x))) / pi"
proof -
  have "integral⇧L (lebesgue_on {-pi..pi}) f / (sqrt (2 * pi) * sqrt 2 * sqrt pi) = integral⇧L (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 "(∑k≤n. Fourier_coefficient f k * trigonometric_set k 0) =
       integral⇧L (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 "integral⇧L (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  "(∑k≤2*n. Fourier_coefficient f k * trigonometric_set k t) =
          (∑k≤2*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  "(∑k≤2*n. Fourier_coefficient f k * trigonometric_set k t) =
          (∑k≤n. Fourier_coefficient (λx. f(x+t)) (2*k) * trigonometric_set (2*k) 0)"
  (is "?lhs = ?rhs")
proof -
  have "?lhs = (∑k≤n. 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]:
  "integral⇧L (lebesgue_on {-pi..pi}) (Dirichlet_kernel n) = pi"
proof -
  have "integral⇧L (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]:
  "integral⇧L (lebesgue_on {0..pi}) (Dirichlet_kernel n) = pi/2"
proof -
  have "integral⇧L (lebesgue_on {- pi..0}) (Dirichlet_kernel n) +
        integral⇧L (lebesgue_on {0..pi}) (Dirichlet_kernel n) = pi"
    using integral_combine [OF integrable_Dirichlet_kernel] integral_Dirichlet_kernel by simp
  moreover have "integral⇧L (lebesgue_on {- pi..0}) (Dirichlet_kernel n) = integral⇧L (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
   "(∑k≤2*n. Fourier_coefficient f k * trigonometric_set k t) =
            integral⇧L (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. (∑k≤n. 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. (∑k≤n. Fourier_coefficient f k * trigonometric_set k t)) ⇢ f t"
proof -
  let ?Φ = "λn. ∑k≤n. 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. (∑k≤n. Fourier_coefficient f k * trigonometric_set k t) - f t) ⇢ 0"
    if "?Φ ⇢ 0"
  proof (rule Lim_transform_eventually [OF that eventually_sequentiallyI])
    show "(∑k≤n. Fourier_coefficient (λx. f x - f t) k * trigonometric_set k t)
        = (∑k≤n. 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]: "integral⇧L (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 = integral⇧L (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. (∑k≤n. 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. (∑k≤n. 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. (∑k≤n. 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. (∑k≤n. 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 "integral⇧L (lebesgue_on {-a..a}) f = integral⇧L (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 "integral⇧L (lebesgue_on {-a..a}) f = integral⇧L (lebesgue_on {-a..0}) f + integral⇧L (lebesgue_on {0..a}) f"
    by (simp add: True assms integral_combine)
  also have "… = integral⇧L (lebesgue_on {0..a}) (λx. f(-x)) + integral⇧L (lebesgue_on {0..a}) f"
    by (metis (no_types) add.inverse_inverse add.inverse_neutral integral_reflect_real)
  also have "… = integral⇧L (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 "(∑k≤2*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. (∑k≤n. 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. integral⇧L (lebesgue_on {-pi..pi}) (λx. Dirichlet_kernel n x * f x)
            - integral⇧L (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 = integral⇧L (lebesgue_on {-pi..pi}) (λx. sin((n+1/2) * x) * ?f x)" for n
  proof -
    have "?a n = integral⇧L (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 "… = integral⇧L (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. integral⇧L (lebesgue_on {-pi..pi}) (λx. Dirichlet_kernel n x * f x)
            - integral⇧L (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. ∑k≤n. Fourier_coefficient f k * trigonometric_set k t) ⇢ c
     ⟷ (λn. ∑k≤n. 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. ∑k≤n. 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. (∑k≤n. 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. (∑k≤n. 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. n≥N ⟹ ¦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 "¦integral⇧L (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 "integral⇧L (lebesgue_on {0..pi}) (φ n) = integral⇧L (lebesgue_on {0..δ}) (φ n) + integral⇧L (lebesgue_on {δ..pi}) (φ n)"
      by (rule integral_combine) (use ‹0 < δ› ‹δ ≤ pi› in auto)
    moreover have "¦integral⇧L (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 "¦integral⇧L (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. ∀n≥N. ¦integral⇧L (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. ∑k≤2*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. ∑k≤2 * r. Fourier_coefficient f k * trigonometric_set k t) - real n * l
       = (∑r<n. (∑k≤2 * 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. ∑k≤2 * 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. ∑k≤2*r. Fourier_coefficient f k * trigonometric_set k t)) / n) ⇢ l
         ⟷
         ((λn. integral⇧L (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. ∑k≤2*r.  Fourier_coefficient f k * trigonometric_set k t)) / n - l) ⇢ 0"
    by (simp add: LIM_zero_iff)
  also have "… ⟷
        (λn. ((((∑r<n. ∑k≤2*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. ∑k≤2*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. ∀n≥N. ¦(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 "integral⇧L (lebesgue_on {0..ξ}) (Fejer_kernel n) ≤ integral⇧L (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: "integral⇧L (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: "integral⇧L (lebesgue_on {0..ξ}) (λx. Fejer_kernel n x * h x)
                  = integral⇧L (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. ∑k≤2*m. Fourier_coefficient f k * trigonometric_set k x) / n) ⇢ f x"
proof -
  have "(λn. (∑m<n. ∑k≤2*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