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 (intro integral_eq_zero_AE AE_I' [OF null_a]) auto
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})"
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 (intro AE_I' [OF 0]) auto
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