(* ========================================================================= *)
(* L_p spaces, square integrable functions and basics of Fourier series. *)
(* ========================================================================= *)
needs "Multivariate/realanalysis.ml";;
(* ------------------------------------------------------------------------- *)
(* Somewhat general lemmas, but perhaps not enough to be installed. *)
(* ------------------------------------------------------------------------- *)
let REAL_MAX_RPOW = prove
(`!x y z. &0 <= x /\ &0 <= y /\ &0 <= z
==> max (x rpow z) (y rpow z) = (max x y) rpow z`,
MATCH_MP_TAC
REAL_WLOG_LE THEN CONJ_TAC THENL
[MESON_TAC[REAL_ARITH `max x y:real = max y x`]; ALL_TAC] THEN
SIMP_TAC[
RPOW_LE2; REAL_ARITH `max x y:real = if x <= y then y else x`]);;
let REAL_MIN_RPOW = prove
(`!x y z. &0 <= x /\ &0 <= y /\ &0 <= z
==> min (x rpow z) (y rpow z) = (min x y) rpow z`,
MATCH_MP_TAC
REAL_WLOG_LE THEN CONJ_TAC THENL
[MESON_TAC[REAL_ARITH `min x y:real = min y x`]; ALL_TAC] THEN
SIMP_TAC[
RPOW_LE2; REAL_ARITH `min x y:real = if x <= y then x else y`]);;
let LIM_RPOW_NULL = prove
(`!net p x:A->real.
((lift o x) --> vec 0) net /\ &0 < p
==> ((\i. lift(x(i) rpow p)) --> vec 0) net`,
(* ------------------------------------------------------------------------- *)
(* L_p spaces with respect to a set s. *)
(* ------------------------------------------------------------------------- *)
let LSPACE_NEG = prove
(`!s p f:real^M->real^N. f
IN lspace s p ==> (\x. --(f x))
IN lspace s p`,
REWRITE_TAC[VECTOR_ARITH `--x:real^N = --(&1) % x`;
LSPACE_CMUL]);;
let LSPACE_ADD = prove
(`!s p f g:real^M->real^N.
&0 <= p /\ f
IN lspace s p /\ g
IN lspace s p
==> (\x. f(x) + g(x))
IN lspace s p`,
let LSPACE_SUB = prove
(`!s p f g:real^M->real^N.
&0 <= p /\ f
IN lspace s p /\ g
IN lspace s p
==> (\x. f(x) - g(x))
IN lspace s p`,
let LSPACE_VSUM = prove
(`!s p f:A->real^M->real^N t.
&0 < p /\
FINITE t /\ (!i. i
IN t ==> (f i)
IN lspace s p)
==> (\x. vsum t (\i. f i x))
IN lspace s p`,
let LSPACE_MAX = prove
(`!s p k f:real^M->real^N g:real^M->real^N.
f
IN lspace s p /\ g
IN lspace s p /\ &0 < p
==> ((\x. lambda i. max (f x$i) (g x$i)):real^M->real^N)
IN lspace s p`,
let LSPACE_MIN = prove
(`!s p k f:real^M->real^N g:real^M->real^N.
f
IN lspace s p /\ g
IN lspace s p /\ &0 < p
==> ((\x. lambda i. min (f x$i) (g x$i)):real^M->real^N)
IN lspace s p`,
let LSPACE_MONO = prove
(`!f:real^M->real^N s p q.
f
IN lspace s q /\ measurable s /\ &0 < p /\ p <= q
==> f
IN lspace s p`,
let LSPACE_INCLUSION = prove
(`!s p q. measurable s /\ &0 < p /\ p <= q
==> (lspace s q :(real^M->real^N)->bool)
SUBSET (lspace s p)`,
REWRITE_TAC[
SUBSET] THEN REPEAT STRIP_TAC THEN
MATCH_MP_TAC
LSPACE_MONO THEN EXISTS_TAC `q:real` THEN
ASM_REWRITE_TAC[]);;
(* ------------------------------------------------------------------------- *)
(* The corresponding seminorm; Hoelder and Minkowski inequalities. *)
(* ------------------------------------------------------------------------- *)
let LNORM_NEG = prove
(`!s p f:real^M->real^N. lnorm s p (\x. --(f x)) = lnorm s p f`,
let LNORM_MUL = prove
(`!s p f c. f
IN lspace s p /\ ~(p = &0)
==> lnorm s p (\x. c % f x) = abs(c) * lnorm s p f`,
let LNORM_EQ_0 = prove
(`!s p f. ~(p = &0) /\ f
IN lspace s p
==> (lnorm s p f = &0 <=>
negligible {x | x
IN s /\ ~(f x = vec 0)})`,
let LNORM_RPOW = prove
(`!s p f:real^M->real^N.
f
IN lspace s p /\ ~(p = &0)
==> (lnorm s p f) rpow p =
drop(integral s (\x. lift(norm(f x) rpow p)))`,
let INTEGRAL_LNORM_RPOW = prove
(`!s p f:real^M->real^N.
f
IN lspace s p /\ ~(p = &0)
==> integral s (\x. lift(norm(f x) rpow p)) =
lift((lnorm s p f) rpow p)`,
let HOELDER_INEQUALITY = prove
(`!s p q f:real^M->real^N g:real^M->real^N.
&0 < p /\ &0 < q /\ inv(p) + inv(q) = &1 /\
f
IN lspace s p /\ g
IN lspace s q
==> drop(integral s (\x. lift(norm(f x) * norm(g x))))
<= lnorm s p f * lnorm s q g`,
let HOELDER_INEQUALITY_FULL = prove
(`!s p q f:real^M->real^N g:real^M->real^N.
&0 < p /\ &0 < q /\ inv(p) + inv(q) = &1 /\
f
IN lspace s p /\ g
IN lspace s q
==> (\x. lift(norm(f x) * norm(g x)))
integrable_on s /\
drop(integral s (\x. lift(norm(f x) * norm(g x))))
<= lnorm s p f * lnorm s q g`,
let LNORM_TRIANGLE = prove
(`!s p f:real^M->real^N g:real^M->real^N.
f
IN lspace s p /\ g
IN lspace s p /\ &1 <= p
==> lnorm s p (\x. f x + g x) <= lnorm s p f + lnorm s p g`,
let VSUM_LNORM = prove
(`!s p f:A->real^M->real^N t.
&1 <= p /\
FINITE t /\ (!i. i
IN t ==> (f i)
IN lspace s p)
==> lnorm s p (\x. vsum t (\i. f i x)) <= sum t (\i. lnorm s p (f i))`,
REWRITE_TAC[
IMP_CONJ;
RIGHT_FORALL_IMP_THM] THEN
REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN
MATCH_MP_TAC
FINITE_INDUCT_STRONG THEN
ASM_SIMP_TAC[
SUM_CLAUSES;
VSUM_CLAUSES;
LNORM_0;
REAL_LE_REFL;
REAL_ARITH `&1 <= p ==> ~(p = &0)`] THEN
MAP_EVERY X_GEN_TAC [`i:A`; `u:A->bool`] THEN
REWRITE_TAC[
IN_INSERT] THEN
DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
ASM_SIMP_TAC[] THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
MATCH_MP_TAC(REAL_ARITH `a <= x + y ==> y <= z ==> a <= x + z`) THEN
W(MP_TAC o PART_MATCH (lhand o rand)
LNORM_TRIANGLE o lhand o snd) THEN
ASM_SIMP_TAC[ETA_AX;
LSPACE_VSUM; REAL_ARITH `&1 <= p ==> &0 < p`]);;
(* ------------------------------------------------------------------------- *)
(* The main lemma for Riesz-Fischer, as in Royden's book. *)
(* ------------------------------------------------------------------------- *)
let LSPACE_SUMMABLE_UNIV = prove
(`!f:num->real^M->real^N p s.
&1 <= p /\
(!i. f i
IN lspace s p) /\
real_summable (:num) (\i. lnorm s p (f i))
==> ?g. g
IN lspace s p /\
!e. &0 < e ==> eventually
(\n. lnorm s p (\x. vsum (0..n) (\i. f i x) -
g(x)) < e)
sequentially`,
let LSPACE_SUMMABLE = prove
(`!f:num->real^M->real^N p s t.
&1 <= p /\
(!i. i
IN t ==> f i
IN lspace s p) /\
real_summable t (\i. lnorm s p (f i))
==> ?g. g
IN lspace s p /\
((\n. lnorm s p (\x. vsum (t
INTER (0..n)) (\i. f i x) - g x))
---> &0) sequentially`,
REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM
REAL_SUMMABLE_RESTRICT] THEN
REWRITE_TAC[] THEN STRIP_TAC THEN
MP_TAC(ISPECL
[`(\n:num x. if n
IN t then f n x else vec 0):num->real^M->real^N`;
`p:real`; `s:real^M->bool`]
LSPACE_SUMMABLE_UNIV) THEN
ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
[CONJ_TAC THENL
[X_GEN_TAC `i:num` THEN ASM_CASES_TAC `(i:num)
IN t` THEN
ASM_SIMP_TAC[
LSPACE_0; ETA_AX; REAL_ARITH `&1 <= p ==> ~(p = &0)`];
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
real_summable]) THEN
REWRITE_TAC[
real_summable] THEN MATCH_MP_TAC
MONO_EXISTS THEN
GEN_TAC THEN MATCH_MP_TAC EQ_IMP THEN
AP_THM_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
REWRITE_TAC[
FUN_EQ_THM] THEN GEN_TAC THEN COND_CASES_TAC THEN
ASM_SIMP_TAC[ETA_AX;
LNORM_0; REAL_ARITH `&1 <= p ==> ~(p = &0)`]];
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `g:real^M->real^N` THEN
ASM_CASES_TAC `(g:real^M->real^N)
IN lspace s p` THEN
ASM_REWRITE_TAC[
tendsto_real] THEN
MATCH_MP_TAC
MONO_FORALL THEN GEN_TAC THEN
MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[] THEN
MATCH_MP_TAC(REWRITE_RULE[
IMP_CONJ]
EVENTUALLY_MONO) THEN
X_GEN_TAC `n:num` THEN REWRITE_TAC[
REAL_SUB_RZERO] THEN
MATCH_MP_TAC(REAL_ARITH `&0 <= x /\ x = y ==> x < e ==> abs y < e`) THEN
CONJ_TAC THENL
[MATCH_MP_TAC
LNORM_POS_LE THEN MATCH_MP_TAC
LSPACE_SUB THEN
ASM_SIMP_TAC[REAL_ARITH `&1 <= p ==> &0 <= p`] THEN
MATCH_MP_TAC
LSPACE_VSUM THEN
ASM_SIMP_TAC[
FINITE_NUMSEG; REAL_ARITH `&1 <= p ==> &0 < p`] THEN
X_GEN_TAC `i:num` THEN ASM_CASES_TAC `(i:num)
IN t` THEN
ASM_SIMP_TAC[ETA_AX;
LSPACE_0; REAL_ARITH `&1 <= p ==> ~(p = &0)`];
AP_TERM_TAC THEN REWRITE_TAC[
FUN_EQ_THM] THEN
X_GEN_TAC `x:real^M` THEN REWRITE_TAC[GSYM
VSUM_RESTRICT_SET] THEN
REWRITE_TAC[SET_RULE `s
INTER t = {x | x
IN t /\ x
IN s}`]]]);;
(* ------------------------------------------------------------------------- *)
(* Completeness (Riesz-Fischer). *)
(* ------------------------------------------------------------------------- *)
let RIESZ_FISCHER = prove
(`!f:num->real^M->real^N p s.
&1 <= p /\ (!n. (f n)
IN lspace s p) /\
(!e. &0 < e
==> ?N. !m n. m >= N /\ n >= N
==> lnorm s p (\x. f m x - f n x) < e)
==> ?g. g
IN lspace s p /\
!e. &0 < e
==> ?N. !n. n >= N
==> lnorm s p (\x. f n x - g x) < e`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN
`?k:num->num.
(!n. k n < k (SUC n)) /\
(!n. lnorm s p ((\x. f (k(SUC n)) x - f (k n) x):real^M->real^N)
< inv(&2 pow n))`
STRIP_ASSUME_TAC THENL
[FIRST_X_ASSUM(MP_TAC o GEN `n:num` o SPEC `inv(&2 pow n)`) THEN
REWRITE_TAC[
REAL_LT_INV_EQ;
REAL_LT_POW2;
SKOLEM_THM] THEN
DISCH_THEN(X_CHOOSE_TAC `N:num->num`) THEN
MP_TAC(prove_recursive_functions_exist num_RECURSION
`k 0 = N 0 /\
!n. k(SUC n) =
MAX (k n + 1) (
MAX (N n) (N(SUC n)))`) THEN
MATCH_MP_TAC
MONO_EXISTS THEN REPEAT STRIP_TAC THEN
ASM_REWRITE_TAC[ARITH_RULE `n <
MAX (n + 1) m`] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
CONJ_TAC THENL [ARITH_TAC; SPEC_TAC(`n:num`,`n:num`)] THEN
INDUCT_TAC THEN ASM_REWRITE_TAC[] THEN ARITH_TAC;
ALL_TAC] THEN
MP_TAC(ISPECL
[`\n x. f (k(SUC n)) x - (f:num->real^M->real^N) (k n) x`;
`p:real`; `s:real^M->bool`]
LSPACE_SUMMABLE_UNIV) THEN
ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
[ASM_SIMP_TAC[
LSPACE_SUB; ETA_AX; REAL_ARITH `&1 <= p ==> &0 <= p`] THEN
MATCH_MP_TAC
REAL_SUMMABLE_COMPARISON THEN
EXISTS_TAC `\n. inv(&2) pow n` THEN CONJ_TAC THENL
[MATCH_MP_TAC
REAL_SUMMABLE_GP THEN CONV_TAC REAL_RAT_REDUCE_CONV;
EXISTS_TAC `0` THEN X_GEN_TAC `n:num` THEN DISCH_THEN(K ALL_TAC) THEN
REWRITE_TAC[GSYM
REAL_INV_POW] THEN
MATCH_MP_TAC(REAL_ARITH `&0 <= x /\ x < y ==> abs x <= y`) THEN
ASM_SIMP_TAC[
LNORM_POS_LE;
LSPACE_SUB; ETA_AX;
REAL_ARITH `&1 <= p ==> &0 <= p`]];
DISCH_THEN(X_CHOOSE_THEN `g:real^M->real^N` MP_TAC) THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "*")) THEN
EXISTS_TAC `\x. (g:real^M->real^N) x + f (k 0:num) x` THEN
ASM_SIMP_TAC[
LSPACE_ADD; ETA_AX; REAL_ARITH `&1 <= p ==> &0 <= p`] THEN
X_GEN_TAC `e:real` THEN DISCH_TAC THEN
REMOVE_THEN "*" (MP_TAC o SPEC `e / &2`) THEN
ASM_REWRITE_TAC[
REAL_HALF;
EVENTUALLY_SEQUENTIALLY] THEN
REWRITE_TAC[
ADD1;
VSUM_DIFFS_ALT;
LE_0] THEN
DISCH_THEN(X_CHOOSE_THEN `N1:num` (LABEL_TAC "+")) THEN
FIRST_X_ASSUM(MP_TAC o SPEC `e / &2`) THEN
ASM_REWRITE_TAC[
REAL_HALF;
GE] THEN
DISCH_THEN(X_CHOOSE_TAC `N2:num`) THEN
EXISTS_TAC `
MAX N1 N2` THEN X_GEN_TAC `n:num` THEN
REWRITE_TAC[ARITH_RULE `
MAX N1 N2 <= n <=> N1 <= n /\ N2 <= n`] THEN
STRIP_TAC THEN REMOVE_THEN "+" (MP_TAC o SPEC `n:num`) THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`k(n + 1):num`; `n:num`]) THEN
ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
[MATCH_MP_TAC
LE_TRANS THEN EXISTS_TAC `n + 1` THEN
CONJ_TAC THENL [ASM_ARITH_TAC; SPEC_TAC(`n + 1`,`m:num`)] THEN
INDUCT_TAC THEN REWRITE_TAC[
LE_0] THEN
MATCH_MP_TAC(ARITH_RULE
`m <= k m /\ k m < k(SUC m) ==> SUC m <= k(SUC m)`) THEN
ASM_REWRITE_TAC[];
REPEAT DISCH_TAC THEN
ONCE_REWRITE_TAC[VECTOR_ARITH
`f n x - (g x + f (k 0) x):real^N =
(f (k (n + 1)) x - f (k 0) x - g x) +
--(f (k (n + 1)) x - f n x)`] THEN
W(MP_TAC o PART_MATCH (lhand o rand)
LNORM_TRIANGLE o lhand o snd) THEN
ASM_SIMP_TAC[
LSPACE_SUB;
LSPACE_NEG; ETA_AX;
REAL_ARITH `&1 <= p ==> &0 <= p`] THEN
MATCH_MP_TAC(REAL_ARITH
`x < e / &2 /\ y < e / &2 ==> z <= x + y ==> z < e`) THEN
ASM_SIMP_TAC[
LNORM_NEG;
LSPACE_SUB; ETA_AX;
REAL_ARITH `&1 <= p ==> &0 <= p`]]]);;
(* ------------------------------------------------------------------------- *)
(* A sort of dominated convergence theorem for L_p spaces. *)
(* ------------------------------------------------------------------------- *)
let LSPACE_DOMINATED_CONVERGENCE = prove
(`!f:num->real^M->real^N g h:real^M->real^N s p k.
&0 < p /\
(!n. (f n)
IN lspace s p) /\ h
IN lspace s p /\
(!n x. x
IN s ==> norm(f n x) <= norm(h x)) /\
negligible k /\
(!x. x
IN s
DIFF k ==> ((\n. f n x) --> g(x)) sequentially)
==> g
IN lspace s p /\
((\n. lnorm s p (\x. f n x - g x)) ---> &0) sequentially`,
(* ------------------------------------------------------------------------- *)
(* Approximation of functions in L_p by bounded ones and continuous ones. *)
(* ------------------------------------------------------------------------- *)
let LSPACE_APPROXIMATE_CONTINUOUS = prove
(`!f:real^M->real^N s p e.
&1 <= p /\ measurable s /\ f
IN lspace s p /\ &0 < e
==> ?g. g
continuous_on (:real^M) /\
g
IN lspace s p /\
lnorm s p (\x. f x - g x) < e`,
REPEAT STRIP_TAC THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP (REAL_ARITH `&1 <= p ==> &0 < p`)) THEN
MP_TAC(ISPECL [`f:real^M->real^N`; `s:real^M->bool`; `p:real`; `e / &2`]
LSPACE_APPROXIMATE_BOUNDED) THEN
ASM_REWRITE_TAC[
REAL_HALF] THEN
DISCH_THEN(X_CHOOSE_THEN `h:real^M->real^N` STRIP_ASSUME_TAC) THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
BOUNDED_POS]) THEN
REWRITE_TAC[
FORALL_IN_IMAGE] THEN
DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN
SUBGOAL_THEN
`?k g. negligible k /\
(!n. g n
continuous_on (:real^M)) /\
(!n x. x
IN s ==> norm(g n x:real^N) <= norm(B % vec 1:real^N)) /\
(!x. x
IN (s
DIFF k) ==> ((\n. g n x) --> h x) sequentially)`
STRIP_ASSUME_TAC THENL
[SUBGOAL_THEN `(h:real^M->real^N)
measurable_on s` MP_TAC THENL
[RULE_ASSUM_TAC(REWRITE_RULE[lspace;
IN_ELIM_THM]) THEN ASM_REWRITE_TAC[];
ALL_TAC] THEN
REWRITE_TAC[
measurable_on] THEN MATCH_MP_TAC
MONO_EXISTS THEN
X_GEN_TAC `k:real^M->bool` THEN
DISCH_THEN(X_CHOOSE_THEN `g:num->real^M->real^N` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `(\n x. lambda i. max (--B) (min B (((g n x):real^N)$i))):
num->real^M->real^N` THEN
ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL
[X_GEN_TAC `n:num` THEN
FIRST_X_ASSUM(MP_TAC o SPEC `n:num`) THEN
MP_TAC(ISPECL [`(:real^M)`; `(lambda i. B):real^N`]
CONTINUOUS_ON_CONST) THEN
REWRITE_TAC[IMP_IMP] THEN
DISCH_THEN(MP_TAC o MATCH_MP
CONTINUOUS_ON_MIN) THEN
MP_TAC(ISPECL [`(:real^M)`; `(lambda i. --B):real^N`]
CONTINUOUS_ON_CONST) THEN
REWRITE_TAC[IMP_IMP] THEN
DISCH_THEN(MP_TAC o MATCH_MP
CONTINUOUS_ON_MAX) THEN
MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_TERM_TAC THEN
SIMP_TAC[
FUN_EQ_THM;
CART_EQ;
LAMBDA_BETA];
REPEAT STRIP_TAC THEN MATCH_MP_TAC
NORM_LE_COMPONENTWISE THEN
SIMP_TAC[
LAMBDA_BETA;
VEC_COMPONENT;
VECTOR_MUL_COMPONENT] THEN
REAL_ARITH_TAC;
X_GEN_TAC `x:real^M` THEN REWRITE_TAC[
IN_DIFF] THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `x:real^M`) THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[
LIM_SEQUENTIALLY] THEN
MATCH_MP_TAC
MONO_FORALL THEN X_GEN_TAC `ee:real` THEN
MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `N:num` THEN
MATCH_MP_TAC
MONO_FORALL THEN X_GEN_TAC `n:num` THEN
MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[] THEN
MATCH_MP_TAC(NORM_ARITH
`norm(c - a:real^N) <= norm(b - a)
==> dist(b,a) < ee ==> dist(c,a) < ee`) THEN
MATCH_MP_TAC
NORM_LE_COMPONENTWISE THEN
SIMP_TAC[
LAMBDA_BETA;
VECTOR_SUB_COMPONENT] THEN
X_GEN_TAC `k:num` THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `x:real^M`) THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(MP_TAC o MATCH_MP
NORM_BOUND_COMPONENT_LE) THEN
DISCH_THEN(MP_TAC o SPEC `k:num`) THEN ASM_REWRITE_TAC[] THEN
REAL_ARITH_TAC];
ALL_TAC] THEN
SUBGOAL_THEN `!n. ((g:num->real^M->real^N) n)
IN lspace s p` ASSUME_TAC THENL
[X_GEN_TAC `n:num` THEN
MATCH_MP_TAC
LSPACE_BOUNDED_MEASURABLE THEN
EXISTS_TAC `(\x. B % vec 1):real^M->real^N` THEN
ASM_SIMP_TAC[
LSPACE_CONST] THEN
ONCE_REWRITE_TAC[GSYM
MEASURABLE_ON_UNIV] THEN
MATCH_MP_TAC(REWRITE_RULE[
lebesgue_measurable; indicator]
MEASURABLE_ON_RESTRICT) THEN
ASM_SIMP_TAC[
CONTINUOUS_IMP_MEASURABLE_ON; ETA_AX] THEN
MATCH_MP_TAC
INTEGRABLE_IMP_MEASURABLE THEN
ASM_REWRITE_TAC[GSYM
MEASURABLE_INTEGRABLE];
ALL_TAC] THEN
MP_TAC(ISPECL
[`g:num->real^M->real^N`; `h:real^M->real^N`;
`(\x. B % vec 1):real^M->real^N`;
`s:real^M->bool`; `p:real`; `k:real^M->bool`]
LSPACE_DOMINATED_CONVERGENCE) THEN
ASM_SIMP_TAC[
LSPACE_CONST] THEN
REWRITE_TAC[
REALLIM_SEQUENTIALLY;
REAL_SUB_RZERO] THEN
DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN ASM_REWRITE_TAC[
REAL_HALF] THEN
DISCH_THEN(X_CHOOSE_THEN `n:num` (MP_TAC o SPEC `n:num`)) THEN
REWRITE_TAC[
LE_REFL] THEN DISCH_TAC THEN
EXISTS_TAC `(g:num->real^M->real^N) n` THEN
ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN
`(\x. f x - (g:num->real^M->real^N) n x) =
(\x. (f x - h x) + --(g n x - h x))`
SUBST1_TAC THENL [SIMP_TAC[
FUN_EQ_THM] THEN VECTOR_ARITH_TAC; ALL_TAC] THEN
W(MP_TAC o PART_MATCH (lhand o rand)
LNORM_TRIANGLE o lhand o snd) THEN
ASM_SIMP_TAC[
LSPACE_SUB; ETA_AX;
REAL_LT_IMP_LE;
LSPACE_NEG] THEN
MATCH_MP_TAC(REAL_ARITH
`y < e / &2 /\ z < e / &2 ==> x <= y + z ==> x < e`) THEN
ASM_SIMP_TAC[
LNORM_NEG; REAL_ARITH `abs x < e ==> x < e`]);;
(* ------------------------------------------------------------------------- *)
(* Square-integrable real->real functions. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("square_integrable_on",(12,"right"));;
(* ------------------------------------------------------------------------- *)
(* The norm and inner product in L2. *)
(* ------------------------------------------------------------------------- *)
let L2PRODUCT_SYM = prove
(`!s f g. l2product s f g = l2product s g f`,
REWRITE_TAC[l2product; REAL_MUL_SYM]);;
(* ------------------------------------------------------------------------- *)
(* Orthonormal system of L2 functions and their Fourier coefficients. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Actual trigonometric orthogonality relations. *)
(* ------------------------------------------------------------------------- *)
let REAL_INTEGRABLE_ON_INTERVAL_TAC =
MATCH_MP_TAC REAL_INTEGRABLE_CONTINUOUS THEN
MATCH_MP_TAC REAL_DIFFERENTIABLE_ON_IMP_REAL_CONTINUOUS_ON THEN
REWRITE_TAC[REAL_DIFFERENTIABLE_ON_DIFFERENTIABLE] THEN
GEN_TAC THEN DISCH_TAC THEN REAL_DIFFERENTIABLE_TAC;;
let ODD_EVEN_INDUCT_LEMMA = prove
(`(!n:num. P 0) /\ (!n. P(2 * n + 1)) /\ (!n. P(2 * n + 2)) ==> !n. P n`,
REWRITE_TAC[
FORALL_SIMP] THEN STRIP_TAC THEN
MATCH_MP_TAC
num_INDUCTION THEN ASM_REWRITE_TAC[] THEN
X_GEN_TAC `n:num` THEN DISCH_THEN(K ALL_TAC) THEN
MP_TAC(ISPEC `n:num`
EVEN_OR_ODD) THEN
REWRITE_TAC[
EVEN_EXISTS;
ODD_EXISTS] THEN STRIP_TAC THEN
ASM_REWRITE_TAC[ARITH_RULE
`SUC(2 * n) = 2 * n + 1 /\ SUC(2 * n + 1) = 2 * n + 2`]);;
(* ------------------------------------------------------------------------- *)
(* Weierstrass for trigonometric polynomials. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* A bit of extra hacking round so that the ends of a function are OK. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Hence the main approximation result. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Convergence w.r.t. L2 norm of trigonometric Fourier series. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Fourier coefficients go to 0 (weak form of Riemann-Lebesgue). *)
(* ------------------------------------------------------------------------- *)
let ABSOLUTELY_INTEGRABLE_SIN_PRODUCT,ABSOLUTELY_INTEGRABLE_COS_PRODUCT =
(CONJ_PAIR o prove)
(`(!f k. f absolutely_real_integrable_on real_interval[--pi,pi]
==> (\x. sin(k * x) * f x) absolutely_real_integrable_on
real_interval[--pi,pi]) /\
(!f k. f absolutely_real_integrable_on real_interval[--pi,pi]
==> (\x. cos(k * x) * f x) absolutely_real_integrable_on
real_interval[--pi,pi])`,
REPEAT STRIP_TAC THEN
MATCH_MP_TAC ABSOLUTELY_REAL_INTEGRABLE_BOUNDED_MEASURABLE_PRODUCT THEN
(ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
[MATCH_MP_TAC REAL_MEASURABLE_ON_MEASURABLE_SUBSET THEN
EXISTS_TAC `(:real)` THEN
REWRITE_TAC[REAL_MEASURABLE_REAL_INTERVAL; SUBSET_UNIV] THEN
MATCH_MP_TAC CONTINUOUS_IMP_REAL_MEASURABLE_ON THEN
MATCH_MP_TAC REAL_DIFFERENTIABLE_ON_IMP_REAL_CONTINUOUS_ON THEN
REWRITE_TAC[ETA_AX; IN_UNIV; REAL_DIFFERENTIABLE_ON_DIFFERENTIABLE] THEN
SPEC_TAC(`n:num`,`n:num`) THEN MATCH_MP_TAC ODD_EVEN_INDUCT_LEMMA THEN
REWRITE_TAC[trigonometric_set; real_div] THEN
REPEAT STRIP_TAC THEN REAL_DIFFERENTIABLE_TAC;
REWRITE_TAC[real_bounded; FORALL_IN_IMAGE] THEN EXISTS_TAC `&1` THEN
SPEC_TAC(`n:num`,`n:num`) THEN MATCH_MP_TAC ODD_EVEN_INDUCT_LEMMA THEN
REWRITE_TAC[trigonometric_set; COS_BOUND; SIN_BOUND]]));;
let FOURIER_SUM_LIMIT_PAIR = prove
(`!f n t l.
f
absolutely_real_integrable_on real_interval [--pi,pi]
==> (((\n. sum(0..2*n) (\k.
fourier_coefficient f k *
trigonometric_set k t)) ---> l)
sequentially <=>
((\n. sum(0..n) (\k.
fourier_coefficient f k *
trigonometric_set k t)) ---> l)
sequentially)`,
REPEAT STRIP_TAC THEN REWRITE_TAC[
REALLIM_SEQUENTIALLY] THEN
EQ_TAC THEN DISCH_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THENL
[FIRST_ASSUM(MP_TAC o MATCH_MP
RIEMANN_LEBESGUE) THEN
REWRITE_TAC[
REALLIM_SEQUENTIALLY;
REAL_SUB_RZERO] THEN
DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN ASM_REWRITE_TAC[
REAL_HALF] THEN
DISCH_THEN(X_CHOOSE_THEN `N1:num` (LABEL_TAC "1")) THEN
SUBGOAL_THEN `&0 < e / &2` (fun th -> FIRST_ASSUM(MP_TAC o C MATCH_MP th))
THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `N2:num` (LABEL_TAC "2")) THEN
EXISTS_TAC `N1 + 2 * N2 + 1` THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN
DISJ_CASES_THEN SUBST1_TAC
(ARITH_RULE `n = 2 * n DIV 2 \/ n = SUC(2 * n DIV 2)`) THEN
REWRITE_TAC[
SUM_CLAUSES_NUMSEG;
LE_0] THENL
[MATCH_MP_TAC(REAL_ARITH `abs x < e / &2 ==> abs x < e`) THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
MATCH_MP_TAC(REAL_ARITH
`abs(x - l) < e / &2 /\ abs y < e / &2 ==> abs((x + y) - l) < e`) THEN
CONJ_TAC THENL
[FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; ALL_TAC] THEN
MATCH_MP_TAC(REAL_ARITH
`abs(x * y) <= abs(x) * &1 /\ abs(x) < e ==> abs(x * y) < e`) THEN
CONJ_TAC THENL
[REWRITE_TAC[
REAL_ABS_MUL] THEN MATCH_MP_TAC
REAL_LE_LMUL THEN
REWRITE_TAC[
REAL_ABS_POS] THEN
SPEC_TAC(`SUC(2 * n DIV 2)`,`r:num`) THEN
MATCH_MP_TAC
ODD_EVEN_INDUCT_LEMMA THEN
REWRITE_TAC[
ADD1;
trigonometric_set;
REAL_ABS_DIV] THEN
SIMP_TAC[
REAL_LE_LDIV_EQ; REAL_ARITH `&0 < x ==> &0 < abs x`;
SQRT_POS_LT; REAL_ARITH `&0 < &2 * x <=> &0 < x`;
PI_POS] THEN
REPEAT STRIP_TAC THEN MATCH_MP_TAC
REAL_LE_TRANS THEN
EXISTS_TAC `&1` THEN REWRITE_TAC[
COS_BOUND;
SIN_BOUND] THEN
MATCH_MP_TAC(REAL_ARITH `&1 <= x ==> &1 <= &1 * abs x`) THEN
SUBST1_TAC(GSYM
SQRT_1) THEN MATCH_MP_TAC
SQRT_MONO_LE THEN
MP_TAC
PI_APPROX_32 THEN REAL_ARITH_TAC;
FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC]];
FIRST_X_ASSUM(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC
MONO_EXISTS THEN GEN_TAC THEN DISCH_TAC THEN
REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC]);;
(* ------------------------------------------------------------------------- *)
(* Express Fourier sum in terms of the special expansion at the origin. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* How Fourier coefficients behave under addition etc. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Shifting the origin for integration of periodic functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Express partial sums using Dirichlet kernel. *)
(* ------------------------------------------------------------------------- *)
let DIRICHLET_KERNEL_0 = prove
(`!x. abs(x) < &2 * pi ==>
dirichlet_kernel 0 x = &1 / &2`,
REPEAT STRIP_TAC THEN REWRITE_TAC[
dirichlet_kernel] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_ADD_LID] THEN
REWRITE_TAC[
real_div; REAL_MUL_LID; REAL_MUL_SYM;
REAL_MUL_RID] THEN
MATCH_MP_TAC(REAL_FIELD `~(x = &0) ==> inv(&2 * x) * x = inv(&2)`) THEN
DISCH_TAC THEN SUBGOAL_THEN `~(x * inv(&2) = &0)` MP_TAC THENL
[ASM_REAL_ARITH_TAC; REWRITE_TAC[] THEN MATCH_MP_TAC
SIN_EQ_0_PI] THEN
ASM_REAL_ARITH_TAC);;
let COSINE_SUM_LEMMA = prove
(`!n x. (&1 / &2 + sum(1..n) (\k. cos(&k * x))) * sin(x / &2) =
sin((&n + &1 / &2) * x) / &2`,
REPEAT STRIP_TAC THEN DISJ_CASES_TAC(ARITH_RULE `n = 0 \/ 1 <= n`) THENL
[ASM_REWRITE_TAC[REAL_ADD_LID;
SUM_CLAUSES_NUMSEG; ARITH] THEN
REWRITE_TAC[
real_div; REAL_MUL_LID;
REAL_ADD_RID; REAL_MUL_SYM];
REPEAT STRIP_TAC THEN REWRITE_TAC[
REAL_ADD_RDISTRIB; GSYM
SUM_RMUL] THEN
REWRITE_TAC[
REAL_MUL_COS_SIN;
real_div;
REAL_SUB_RDISTRIB] THEN
SUBGOAL_THEN
`!k x. &k * x + x * inv(&2) = (&(k + 1) * x - x * inv(&2))`
(fun th -> REWRITE_TAC[th;
SUM_DIFFS_ALT])
THENL [REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN REAL_ARITH_TAC; ALL_TAC] THEN
ASM_REWRITE_TAC[GSYM REAL_OF_NUM_ADD; GSYM
real_div] THEN
REWRITE_TAC[REAL_ARITH `&1 * x - x / &2 = x / &2`] THEN
REWRITE_TAC[REAL_ARITH `(&n + &1) * x - x / &2 = (&n + &1 / &2) * x`] THEN
REWRITE_TAC[
REAL_ADD_RDISTRIB] THEN REAL_ARITH_TAC]);;
(* ------------------------------------------------------------------------- *)
(* A directly deduced sufficient condition for convergence at a point. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* A more natural sufficient Hoelder condition at a point. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* In particular, a Lipschitz condition at the point. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* In particular, if left and right derivatives both exist. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* And in particular at points where the function is differentiable. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Use reflection to halve the region of integration. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Localization principle: convergence only depends on values "nearby". *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Localize the earlier integral. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Make a harmless simplifying tweak to the Dirichlet kernel. *)
(* ------------------------------------------------------------------------- *)
let FOURIER_SUM_LIMIT_SINE_PART = prove
(`!f t l d.
f
absolutely_real_integrable_on real_interval[--pi,pi] /\
(!x. f (x + &2 * pi) = f x) /\ &0 < d /\ d <= pi
==> (((\n. sum (0..n)
(\k.
fourier_coefficient f k *
trigonometric_set k t))
---> l) sequentially <=>
((\n.
real_integral (
real_interval[&0,d])
(\x. sin((&n + &1 / &2) * x) *
((f(t + x) + f(t - x)) - &2 * l) / x))
---> &0) sequentially)`,
let lemma0 = prove
(`!x. abs(sin(x) - x) <= abs(x) pow 3`,
GEN_TAC THEN MP_TAC(ISPECL [`0`; `Cx x`] TAYLOR_CSIN) THEN
REWRITE_TAC[VSUM_CLAUSES_NUMSEG; GSYM CX_SIN] THEN
CONV_TAC NUM_REDUCE_CONV THEN
REWRITE_TAC[complex_pow; COMPLEX_POW_1; COMPLEX_DIV_1; IM_CX] THEN
REWRITE_TAC[GSYM CX_MUL; GSYM CX_SUB; COMPLEX_NORM_CX; REAL_ABS_0] THEN
REWRITE_TAC[REAL_EXP_0; REAL_MUL_LID] THEN REAL_ARITH_TAC) in
let lemma1 = prove
(`!x. ~(x = &0) ==> abs(sin(x) / x - &1) <= x pow 2`,
REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN
MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN EXISTS_TAC `abs x` THEN
REWRITE_TAC[GSYM REAL_ABS_MUL; GSYM(CONJUNCT2 real_pow)] THEN
ASM_REWRITE_TAC[GSYM REAL_ABS_NZ; ARITH] THEN
ASM_SIMP_TAC[REAL_SUB_LDISTRIB; REAL_DIV_LMUL; REAL_MUL_RID] THEN
REWRITE_TAC[lemma0]) in
let lemma2 = prove
(`!x. abs(x) <= &1 / &2 ==> abs(x) / &2 <= abs(sin x)`,
REPEAT STRIP_TAC THEN MP_TAC(SPEC `x:real` lemma0) THEN
MATCH_MP_TAC(REAL_ARITH
`&4 * x3 <= abs x ==> abs(s - x) <= x3 ==> abs(x) / &2 <= abs s`) THEN
REWRITE_TAC[REAL_ARITH
`&4 * x pow 3 <= x <=> x * x pow 2 <= x * (&1 / &2) pow 2`] THEN
MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS] THEN
ASM_REAL_ARITH_TAC) in
let lemma3 = prove
(`!x. ~(x = &0) /\ abs x <= &1 / &2
==> abs(inv(sin x) - inv x) <= &2 * abs x`,
REPEAT STRIP_TAC THEN
MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN EXISTS_TAC `abs(sin x)` THEN
REWRITE_TAC[GSYM REAL_ABS_MUL] THEN ASM_CASES_TAC `sin x = &0` THENL
[MP_TAC(SPEC `x:real` SIN_EQ_0_PI) THEN
MP_TAC PI_APPROX_32 THEN ASM_REAL_ARITH_TAC;
ASM_SIMP_TAC[GSYM REAL_ABS_NZ; REAL_SUB_LDISTRIB; REAL_MUL_RINV] THEN
REWRITE_TAC[REAL_ARITH `abs(&1 - s * inv x) = abs(s / x - &1)`] THEN
MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `(x:real) pow 2` THEN
ASM_SIMP_TAC[lemma1] THEN ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN
REWRITE_TAC[REAL_POW_2; REAL_MUL_ASSOC] THEN
MATCH_MP_TAC REAL_LE_RMUL THEN
MP_TAC(ISPEC `x:real` lemma2) THEN ASM_REAL_ARITH_TAC]) in
REPEAT STRIP_TAC THEN
MP_TAC(ISPECL [`f:real->real`; `t:real`; `l:real`; `d:real`]
FOURIER_SUM_LIMIT_DIRICHLET_KERNEL_PART) THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
MATCH_MP_TAC REALLIM_TRANSFORM_EQ THEN REWRITE_TAC[] THEN
MATCH_MP_TAC REALLIM_TRANSFORM_EVENTUALLY THEN
MP_TAC(ISPECL [`f:real->real`; `--pi`; `pi`; `t:real`]
ABSOLUTELY_REAL_INTEGRABLE_PERIODIC_OFFSET) THEN
ASM_REWRITE_TAC[REAL_ARITH `pi - --pi = &2 * pi`] THEN
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [REAL_ADD_SYM] THEN
DISCH_THEN(fun th -> ASSUME_TAC th THEN MP_TAC th) THEN
GEN_REWRITE_TAC LAND_CONV [absolutely_real_integrable_on] THEN
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
[GSYM REAL_INTEGRABLE_REFLECT] THEN
REWRITE_TAC[GSYM absolutely_real_integrable_on; GSYM real_sub] THEN
REWRITE_TAC[REAL_NEG_NEG] THEN DISCH_TAC THEN EXISTS_TAC
`\n. real_integral (real_interval[&0,d])
(\x. sin((&n + &1 / &2) * x) *
(inv(&2 * sin(x / &2)) - inv x) *
((f(t + x) + f(t - x)) - &2 * l))` THEN
REWRITE_TAC[EVENTUALLY_SEQUENTIALLY] THEN CONJ_TAC THENL
[EXISTS_TAC `1` THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN
REWRITE_TAC[REAL_INTEGRAL_DIRICHLET_KERNEL_MUL_EXPAND] THEN
REWRITE_TAC[REAL_ARITH
`a * (inv y - inv x) * b:real = a / y * b - a / x * b`] THEN
REWRITE_TAC[REAL_ARITH `sin(y) * (a - b) / x = sin(y) / x * (a - b)`] THEN
MATCH_MP_TAC REAL_INTEGRAL_SUB THEN CONJ_TAC THENL
[REWRITE_TAC[GSYM REAL_INTEGRABLE_DIRICHLET_KERNEL_MUL_EXPAND] THEN
MATCH_MP_TAC ABSOLUTELY_REAL_INTEGRABLE_IMP_INTEGRABLE THEN
MATCH_MP_TAC ABSOLUTELY_REAL_INTEGRABLE_ON_SUBINTERVAL THEN
EXISTS_TAC `real_interval[--pi,pi]` THEN CONJ_TAC THENL
[ALL_TAC; REWRITE_TAC[SUBSET_REAL_INTERVAL] THEN ASM_REAL_ARITH_TAC] THEN
MATCH_MP_TAC ABSOLUTELY_REAL_INTEGRABLE_MUL_DIRICHLET_KERNEL THEN
ASM_SIMP_TAC[ABSOLUTELY_REAL_INTEGRABLE_ADD;
ABSOLUTELY_REAL_INTEGRABLE_SUB;
ABSOLUTELY_REAL_INTEGRABLE_CONST];
MATCH_MP_TAC(REWRITE_RULE[IMP_IMP] REAL_INTEGRABLE_SPIKE) THEN
EXISTS_TAC `\x. dirichlet_kernel n x * (&2 * sin(x / &2)) / x *
((f(t + x) + f(t - x)) - &2 * l)` THEN
EXISTS_TAC `{&0}` THEN REWRITE_TAC[REAL_NEGLIGIBLE_SING] THEN
CONJ_TAC THENL
[X_GEN_TAC `x:real` THEN
REWRITE_TAC[IN_DIFF; IN_SING; IN_REAL_INTERVAL; REAL_MUL_ASSOC] THEN
STRIP_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
ASM_REWRITE_TAC[dirichlet_kernel] THEN
MATCH_MP_TAC(REAL_FIELD
`~(x = &0) /\ ~(y = &0) ==> a / x = a / (&2 * y) * (&2 * y) / x`) THEN
MP_TAC(ISPEC `x / &2` SIN_EQ_0_PI) THEN ASM_REAL_ARITH_TAC;
MATCH_MP_TAC ABSOLUTELY_REAL_INTEGRABLE_IMP_INTEGRABLE THEN
MATCH_MP_TAC ABSOLUTELY_REAL_INTEGRABLE_ON_SUBINTERVAL THEN
EXISTS_TAC `real_interval[--pi,pi]` THEN CONJ_TAC THENL
[ALL_TAC;
REWRITE_TAC[SUBSET_REAL_INTERVAL] THEN ASM_REAL_ARITH_TAC] THEN
MATCH_MP_TAC ABSOLUTELY_REAL_INTEGRABLE_MUL_DIRICHLET_KERNEL THEN
MATCH_MP_TAC ABSOLUTELY_REAL_INTEGRABLE_BOUNDED_MEASURABLE_PRODUCT THEN
ASM_SIMP_TAC[ABSOLUTELY_REAL_INTEGRABLE_ADD;
ABSOLUTELY_REAL_INTEGRABLE_SUB;
ABSOLUTELY_REAL_INTEGRABLE_CONST] THEN
CONJ_TAC THENL
[MATCH_MP_TAC REAL_MEASURABLE_ON_DIV THEN
REWRITE_TAC[REAL_NEGLIGIBLE_SING; SING_GSPEC] THEN
CONJ_TAC THEN MATCH_MP_TAC
REAL_CONTINUOUS_IMP_REAL_MEASURABLE_ON_CLOSED_SUBSET THEN
REWRITE_TAC[REAL_CLOSED_UNIV; REAL_CLOSED_REAL_INTERVAL] THEN
REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
REPEAT STRIP_TAC THEN
MATCH_MP_TAC REAL_CONTINUOUS_ATREAL_WITHINREAL THEN
MATCH_MP_TAC REAL_DIFFERENTIABLE_IMP_CONTINUOUS_ATREAL THEN
REAL_DIFFERENTIABLE_TAC;
ALL_TAC]]] THEN
SUBGOAL_THEN `real_bounded (IMAGE (\x. &1 + (x / &2) pow 2)
(real_interval[--pi,pi]))`
MP_TAC THENL
[MATCH_MP_TAC REAL_COMPACT_IMP_BOUNDED THEN
MATCH_MP_TAC REAL_COMPACT_CONTINUOUS_IMAGE THEN
REWRITE_TAC[REAL_COMPACT_INTERVAL] THEN
REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
REPEAT STRIP_TAC THEN
MATCH_MP_TAC REAL_CONTINUOUS_ATREAL_WITHINREAL THEN
MATCH_MP_TAC REAL_DIFFERENTIABLE_IMP_CONTINUOUS_ATREAL THEN
REAL_DIFFERENTIABLE_TAC;
REWRITE_TAC[REAL_BOUNDED_POS; FORALL_IN_IMAGE] THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `B:real` THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "*")) THEN
ASM_REWRITE_TAC[] THEN X_GEN_TAC `x:real` THEN DISCH_TAC THEN
ASM_CASES_TAC `x = &0` THENL
[ASM_REWRITE_TAC[real_div; REAL_INV_0; REAL_MUL_RID] THEN
ASM_REAL_ARITH_TAC;
REMOVE_THEN "*" (MP_TAC o SPEC `x:real`) THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC(REAL_ARITH
`abs(z - &1) <= y ==> abs(&1 + y) <= B ==> abs(z) <= B`) THEN
ASM_SIMP_TAC[REAL_FIELD
`~(x = &0) ==> (&2 * y) / x = y / (x / &2)`] THEN
MATCH_MP_TAC lemma1 THEN ASM_REAL_ARITH_TAC]];
SUBGOAL_THEN `real_interval[&0,d] SUBSET real_interval[--pi,pi]`
MP_TAC THENL
[REWRITE_TAC[SUBSET_REAL_INTERVAL] THEN ASM_REAL_ARITH_TAC;
DISCH_THEN(fun th -> REWRITE_TAC
[GSYM(MATCH_MP REAL_INTEGRAL_RESTRICT th)])] THEN
REWRITE_TAC[MESON[REAL_MUL_LZERO; REAL_MUL_RZERO]
`(if p x then a x * b x * c x else &0) =
a x * (if p x then b x else &0) * c x`] THEN
MATCH_MP_TAC RIEMANN_LEBESGUE_SIN_HALF THEN
MATCH_MP_TAC ABSOLUTELY_REAL_INTEGRABLE_BOUNDED_MEASURABLE_PRODUCT THEN
ASM_SIMP_TAC[ABSOLUTELY_REAL_INTEGRABLE_ADD;
ABSOLUTELY_REAL_INTEGRABLE_SUB;
ABSOLUTELY_REAL_INTEGRABLE_CONST] THEN
CONJ_TAC THENL
[MATCH_MP_TAC REAL_MEASURABLE_ON_CASES THEN
REWRITE_TAC[REAL_MEASURABLE_ON_0; SET_RULE `{x | x IN s} = s`;
REAL_LEBESGUE_MEASURABLE_INTERVAL] THEN
MATCH_MP_TAC REAL_MEASURABLE_ON_SUB THEN CONJ_TAC THEN
GEN_REWRITE_TAC (LAND_CONV) [GSYM ETA_AX] THEN REWRITE_TAC[] THEN
ONCE_REWRITE_TAC[REAL_ARITH `inv x = &1 / x`] THEN
MATCH_MP_TAC REAL_MEASURABLE_ON_DIV THEN
SIMP_TAC[REAL_CONTINUOUS_IMP_REAL_MEASURABLE_ON_CLOSED_SUBSET;
REAL_CLOSED_REAL_INTERVAL; REAL_CONTINUOUS_ON_CONST;
REAL_CONTINUOUS_ON_ID; SING_GSPEC; REAL_NEGLIGIBLE_SING;
REAL_CLOSED_UNIV] THEN
CONJ_TAC THENL
[MATCH_MP_TAC CONTINUOUS_IMP_REAL_MEASURABLE_ON THEN
REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
REPEAT STRIP_TAC THEN
MATCH_MP_TAC REAL_CONTINUOUS_ATREAL_WITHINREAL THEN
MATCH_MP_TAC REAL_DIFFERENTIABLE_IMP_CONTINUOUS_ATREAL THEN
REAL_DIFFERENTIABLE_TAC;
REWRITE_TAC[REAL_ARITH `&2 * x = &0 <=> x = &0`] THEN
REWRITE_TAC[REAL_SIN_X2_ZEROS] THEN
MATCH_MP_TAC REAL_NEGLIGIBLE_COUNTABLE THEN
MATCH_MP_TAC COUNTABLE_IMAGE THEN REWRITE_TAC[COUNTABLE_INTEGER]];
ALL_TAC] THEN
SUBGOAL_THEN
`real_bounded(IMAGE (\x. inv (&2 * sin (x / &2)) - inv x)
(real_interval[--pi,-- &1] UNION
real_interval[&1,pi]))`
MP_TAC THENL
[MATCH_MP_TAC REAL_COMPACT_IMP_BOUNDED THEN
MATCH_MP_TAC REAL_COMPACT_CONTINUOUS_IMAGE THEN
SIMP_TAC[REAL_COMPACT_INTERVAL; REAL_COMPACT_UNION] THEN
REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
REPEAT STRIP_TAC THEN
MATCH_MP_TAC REAL_CONTINUOUS_ATREAL_WITHINREAL THEN
MATCH_MP_TAC REAL_DIFFERENTIABLE_IMP_CONTINUOUS_ATREAL THEN
REAL_DIFFERENTIABLE_TAC THEN MP_TAC(ISPEC `x / &2` SIN_EQ_0_PI) THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [IN_UNION]) THEN
REWRITE_TAC[IN_REAL_INTERVAL] THEN REAL_ARITH_TAC;
ALL_TAC] THEN
REWRITE_TAC[REAL_BOUNDED_POS; FORALL_IN_IMAGE] THEN
REWRITE_TAC[IN_REAL_INTERVAL; IN_UNION] THEN
DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `max B (&2)` THEN CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC] THEN
X_GEN_TAC `x:real` THEN STRIP_TAC THEN
COND_CASES_TAC THENL [ALL_TAC; ASM_REAL_ARITH_TAC] THEN
ASM_CASES_TAC `abs(x) <= &1` THENL
[ALL_TAC;
MATCH_MP_TAC(REAL_ARITH `x <= B ==> x <= max B C`) THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REAL_ARITH_TAC] THEN
ASM_CASES_TAC `x = &0` THENL
[ASM_REWRITE_TAC[real_div; REAL_MUL_LZERO; REAL_INV_0; SIN_0] THEN
ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
REWRITE_TAC[REAL_INV_MUL] THEN
MATCH_MP_TAC(REAL_ARITH
`abs(is - &2 * ix) <= &1 ==> abs(inv(&2) * is - ix) <= max B (&2)`) THEN
REWRITE_TAC[GSYM real_div] THEN
GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o RAND_CONV)
[GSYM REAL_INV_DIV] THEN
MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 * abs(x / &2)` THEN
CONJ_TAC THENL [MATCH_MP_TAC lemma3; ASM_REAL_ARITH_TAC] THEN
ASM_REAL_ARITH_TAC]);;
(* ------------------------------------------------------------------------- *)
(* Dini's test. *)
(* ------------------------------------------------------------------------- *)
let FOURIER_DINI_TEST = prove
(`!f t l d.
f
absolutely_real_integrable_on real_interval[--pi,pi] /\
(!x. f (x + &2 * pi) = f x) /\
&0 < d /\
(\x. abs((f(t + x) + f(t - x)) - &2 * l) / x)
real_integrable_on real_interval[&0,d]
==> ((\n. sum (0..n)
(\k.
fourier_coefficient f k *
trigonometric_set k t))
---> l) sequentially`,
REPEAT STRIP_TAC THEN
MP_TAC(ISPECL [`f:real->real`; `t:real`; `l:real`; `pi`]
FOURIER_SUM_LIMIT_SINE_PART) THEN
ASM_REWRITE_TAC[
PI_POS;
REAL_LE_REFL] THEN DISCH_THEN SUBST1_TAC THEN
REWRITE_TAC[
REALLIM_SEQUENTIALLY] THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
FIRST_ASSUM(MP_TAC o MATCH_MP
REAL_INDEFINITE_INTEGRAL_CONTINUOUS_RIGHT) THEN
REWRITE_TAC[
real_continuous_on] THEN DISCH_THEN(MP_TAC o SPEC `&0`) THEN
ASM_SIMP_TAC[
IN_REAL_INTERVAL;
REAL_LE_REFL;
REAL_LT_IMP_LE] THEN
SIMP_TAC[
REAL_INTEGRAL_NULL;
REAL_LE_REFL] THEN
DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN ASM_REWRITE_TAC[
REAL_HALF] THEN
DISCH_THEN(X_CHOOSE_THEN `k:real` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
ABBREV_TAC `dd = min d (min (k / &2) pi)` THEN
DISCH_THEN(MP_TAC o SPEC `dd:real`) THEN
REWRITE_TAC[
REAL_SUB_RZERO] THEN ANTS_TAC THENL
[MP_TAC
PI_POS THEN ASM_REAL_ARITH_TAC; ALL_TAC] THEN
SUBGOAL_THEN `&0 < dd /\ dd <= d /\ dd <= pi /\ dd < k`
STRIP_ASSUME_TAC THENL
[MP_TAC
PI_POS THEN ASM_REAL_ARITH_TAC; ALL_TAC] THEN
MP_TAC(ISPECL [`f:real->real`; `--pi`; `pi`; `t:real`]
ABSOLUTELY_REAL_INTEGRABLE_PERIODIC_OFFSET) THEN
ASM_REWRITE_TAC[REAL_ARITH `pi - --pi = &2 * pi`] THEN
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [REAL_ADD_SYM] THEN
DISCH_THEN(fun th -> ASSUME_TAC th THEN MP_TAC th) THEN
GEN_REWRITE_TAC LAND_CONV [
absolutely_real_integrable_on] THEN
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
[GSYM
REAL_INTEGRABLE_REFLECT] THEN
REWRITE_TAC[GSYM
absolutely_real_integrable_on; GSYM
real_sub] THEN
REWRITE_TAC[
REAL_NEG_NEG] THEN DISCH_TAC THEN
SUBGOAL_THEN
`(\x. ((f(t + x) + f(t - x)) - &2 * l) / x)
absolutely_real_integrable_on
real_interval[&0,dd]`
ASSUME_TAC THENL
[REWRITE_TAC[
ABSOLUTELY_REAL_INTEGRABLE_REAL_MEASURABLE] THEN CONJ_TAC THENL
[MATCH_MP_TAC
REAL_MEASURABLE_ON_DIV THEN
SIMP_TAC[
REAL_CONTINUOUS_IMP_REAL_MEASURABLE_ON_CLOSED_SUBSET;
REAL_CLOSED_REAL_INTERVAL;
REAL_CONTINUOUS_ON_CONST;
REAL_CONTINUOUS_ON_ID;
SING_GSPEC;
REAL_NEGLIGIBLE_SING;
REAL_CLOSED_UNIV] THEN
MATCH_MP_TAC
INTEGRABLE_IMP_REAL_MEASURABLE THEN
MATCH_MP_TAC
REAL_INTEGRABLE_SUBINTERVAL THEN
MAP_EVERY EXISTS_TAC [`--pi`; `pi`] THEN
ASM_SIMP_TAC[
ABSOLUTELY_REAL_INTEGRABLE_IMP_INTEGRABLE;
REAL_INTEGRABLE_ADD;
REAL_INTEGRABLE_SUB;
REAL_INTEGRABLE_CONST] THEN
REWRITE_TAC[
SUBSET_REAL_INTERVAL] THEN ASM_REAL_ARITH_TAC;
MATCH_MP_TAC
REAL_INTEGRABLE_SUBINTERVAL THEN
MAP_EVERY EXISTS_TAC [`&0:real`; `d:real`] THEN CONJ_TAC THENL
[FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (ONCE_REWRITE_RULE
[TAUT `p ==> q ==> r <=> q ==> p ==> r`]
REAL_INTEGRABLE_SPIKE)) THEN
EXISTS_TAC `{}:real->bool` THEN REWRITE_TAC[
REAL_NEGLIGIBLE_EMPTY] THEN
SIMP_TAC[
REAL_ABS_DIV;
IN_REAL_INTERVAL;
IN_DIFF] THEN
SIMP_TAC[
real_abs];
REWRITE_TAC[
SUBSET_REAL_INTERVAL] THEN ASM_REAL_ARITH_TAC]];
ALL_TAC] THEN
SUBGOAL_THEN
`(\x. ((f(t + x) + f(t - x)) - &2 * l) / x)
absolutely_real_integrable_on
real_interval[dd,pi]`
ASSUME_TAC THENL
[REWRITE_TAC[ONCE_REWRITE_RULE[REAL_MUL_SYM]
real_div] THEN
MATCH_MP_TAC
ABSOLUTELY_REAL_INTEGRABLE_BOUNDED_MEASURABLE_PRODUCT THEN
REPEAT CONJ_TAC THENL
[GEN_REWRITE_TAC LAND_CONV [GSYM ETA_AX] THEN REWRITE_TAC[] THEN
ONCE_REWRITE_TAC[REAL_ARITH `inv x = &1 / x`] THEN
MATCH_MP_TAC
REAL_MEASURABLE_ON_DIV THEN
SIMP_TAC[
REAL_CONTINUOUS_IMP_REAL_MEASURABLE_ON_CLOSED_SUBSET;
REAL_CLOSED_REAL_INTERVAL;
REAL_CONTINUOUS_ON_CONST;
REAL_CONTINUOUS_ON_ID;
SING_GSPEC;
REAL_NEGLIGIBLE_SING;
REAL_CLOSED_UNIV];
REWRITE_TAC[
real_bounded;
FORALL_IN_IMAGE] THEN
EXISTS_TAC `inv dd:real` THEN X_GEN_TAC `x:real` THEN
REWRITE_TAC[
IN_REAL_INTERVAL;
REAL_ABS_INV] THEN STRIP_TAC THEN
MATCH_MP_TAC
REAL_LE_INV2 THEN ASM_REAL_ARITH_TAC;
MATCH_MP_TAC
ABSOLUTELY_REAL_INTEGRABLE_ON_SUBINTERVAL THEN
EXISTS_TAC `
real_interval[--pi,pi]` THEN
ASM_SIMP_TAC[
ABSOLUTELY_REAL_INTEGRABLE_ADD;
ABSOLUTELY_REAL_INTEGRABLE_SUB;
ABSOLUTELY_REAL_INTEGRABLE_CONST] THEN
REWRITE_TAC[
SUBSET_REAL_INTERVAL] THEN ASM_REAL_ARITH_TAC];
ALL_TAC] THEN
SUBGOAL_THEN
`(!n. (\x. sin((&n + &1 / &2) * x) *
((f(t + x) + f(t - x)) - &2 * l) / x)
absolutely_real_integrable_on
real_interval[&0,dd]) /\
(!n. (\x. sin((&n + &1 / &2) * x) *
((f(t + x) + f(t - x)) - &2 * l) / x)
absolutely_real_integrable_on
real_interval[dd,pi])`
STRIP_ASSUME_TAC THENL
[REPEAT STRIP_TAC THEN
MATCH_MP_TAC
ABSOLUTELY_REAL_INTEGRABLE_BOUNDED_MEASURABLE_PRODUCT THEN
ASM_REWRITE_TAC[] THEN
(CONJ_TAC THENL
[MATCH_MP_TAC
REAL_CONTINUOUS_IMP_REAL_MEASURABLE_ON_CLOSED_SUBSET THEN
REWRITE_TAC[
REAL_CLOSED_UNIV;
REAL_CLOSED_REAL_INTERVAL] THEN
REWRITE_TAC[
REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
REPEAT STRIP_TAC THEN
MATCH_MP_TAC
REAL_CONTINUOUS_ATREAL_WITHINREAL THEN
MATCH_MP_TAC
REAL_DIFFERENTIABLE_IMP_CONTINUOUS_ATREAL THEN
REAL_DIFFERENTIABLE_TAC;
REWRITE_TAC[
real_bounded;
FORALL_IN_IMAGE] THEN
EXISTS_TAC `&1` THEN REWRITE_TAC[
SIN_BOUND]]);
ALL_TAC] THEN
REPEAT STRIP_TAC THEN
MP_TAC(ISPEC `\x. if abs x < dd then &0
else ((f:real->real)(t + x) - l) / x`
RIEMANN_LEBESGUE_SIN_HALF) THEN
SIMP_TAC[
REAL_INTEGRAL_REFLECT_AND_ADD;
ABSOLUTELY_REAL_INTEGRABLE_IMP_INTEGRABLE;
FOURIER_PRODUCTS_INTEGRABLE_STRONG] THEN
ANTS_TAC THENL
[ONCE_REWRITE_TAC[GSYM
ABSOLUTELY_REAL_INTEGRABLE_RESTRICT_UNIV] THEN
REWRITE_TAC[MESON[] `(if P x then if Q x then &0 else a x else &0) =
(if P x /\ ~Q x then a x else &0)`] THEN
REWRITE_TAC[ONCE_REWRITE_RULE[REAL_MUL_SYM]
real_div] THEN
REWRITE_TAC[MESON[
REAL_MUL_RZERO;
REAL_MUL_LZERO]
`(if P x /\ Q x then a x * b x else &0) =
(if Q x then a x else &0) * (if P x then b x else &0)`] THEN
MATCH_MP_TAC
ABSOLUTELY_REAL_INTEGRABLE_BOUNDED_MEASURABLE_PRODUCT THEN
ASM_SIMP_TAC[
ABSOLUTELY_REAL_INTEGRABLE_RESTRICT_UNIV;
ABSOLUTELY_REAL_INTEGRABLE_SUB;
ABSOLUTELY_REAL_INTEGRABLE_CONST] THEN
CONJ_TAC THENL
[MATCH_MP_TAC
REAL_MEASURABLE_ON_CASES THEN
REWRITE_TAC[
REAL_MEASURABLE_ON_0] THEN CONJ_TAC THENL
[REWRITE_TAC[SET_RULE `{x | ~P x} =
UNIV DIFF {x | P x}`] THEN
REWRITE_TAC[
REAL_LEBESGUE_MEASURABLE_COMPL] THEN
REWRITE_TAC[REAL_ARITH `abs x < d <=> --d < x /\ x < d`] THEN
REWRITE_TAC[GSYM
real_interval;
REAL_LEBESGUE_MEASURABLE_INTERVAL];
GEN_REWRITE_TAC LAND_CONV [GSYM ETA_AX] THEN REWRITE_TAC[] THEN
ONCE_REWRITE_TAC[REAL_ARITH `inv x = &1 / x`] THEN
MATCH_MP_TAC
REAL_MEASURABLE_ON_DIV THEN
SIMP_TAC[
REAL_CONTINUOUS_IMP_REAL_MEASURABLE_ON_CLOSED_SUBSET;
REAL_CLOSED_REAL_INTERVAL;
REAL_CONTINUOUS_ON_CONST;
REAL_CONTINUOUS_ON_ID;
SING_GSPEC;
REAL_NEGLIGIBLE_SING;
REAL_CLOSED_UNIV]];
REWRITE_TAC[
real_bounded;
FORALL_IN_IMAGE;
IN_UNIV] THEN
EXISTS_TAC `inv dd:real` THEN X_GEN_TAC `x:real` THEN
REWRITE_TAC[
REAL_NOT_LT] THEN COND_CASES_TAC THEN
ASM_SIMP_TAC[
REAL_LE_INV_EQ;
REAL_LT_IMP_LE;
REAL_ABS_NUM;
REAL_ABS_INV] THEN
MATCH_MP_TAC
REAL_LE_INV2 THEN ASM_REAL_ARITH_TAC];
ALL_TAC] THEN
REWRITE_TAC[
REAL_ABS_NEG;
REAL_MUL_RNEG;
SIN_NEG;
REAL_MUL_LNEG] THEN
REWRITE_TAC[GSYM
real_sub; GSYM
REAL_SUB_LDISTRIB] THEN
REWRITE_TAC[
real_div;
REAL_INV_NEG;
REAL_MUL_RNEG;
REAL_NEG_NEG] THEN
REWRITE_TAC[REAL_ARITH
`(if p then &0 else a) - (if p then &0 else --b) =
(if p then &0 else a + b)`] THEN
REWRITE_TAC[GSYM
REAL_ADD_RDISTRIB] THEN REWRITE_TAC[GSYM
real_div] THEN
REWRITE_TAC[MESON[
REAL_MUL_RZERO]
`s * (if p then &0 else y) = (if ~p then s * y else &0)`] THEN
ONCE_REWRITE_TAC[GSYM
REAL_INTEGRAL_RESTRICT_UNIV] THEN
REWRITE_TAC[MESON[]
`(if p then if q then x else &0 else &0) =
(if p /\ q then x else &0)`] THEN
REWRITE_TAC[
IN_REAL_INTERVAL] THEN
ASM_SIMP_TAC[REAL_ARITH
`&0 < dd /\ dd <= pi
==> ((&0 <= x /\ x <= pi) /\ ~(abs x < dd) <=>
dd <= x /\ x <= pi)`] THEN
REWRITE_TAC[GSYM
IN_REAL_INTERVAL;
REAL_INTEGRAL_RESTRICT_UNIV] THEN
REWRITE_TAC[REAL_ARITH `(x - l) + (y - l) = (x + y) - &2 * l`] THEN
REWRITE_TAC[
REALLIM_SEQUENTIALLY] THEN
DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN ASM_REWRITE_TAC[
REAL_HALF] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `N:num` THEN DISCH_TAC THEN
X_GEN_TAC `n:num` THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `n:num`) THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(REAL_ARITH
`
real_integral(
real_interval[&0,dd]) f +
real_integral(
real_interval[dd,pi]) f =
real_integral(
real_interval[&0,pi]) f /\
abs(
real_integral(
real_interval[&0,dd]) f) < e / &2
==> abs(
real_integral(
real_interval[dd,pi]) f - &0) < e / &2
==> abs(
real_integral(
real_interval[&0,pi]) f) < e`) THEN
CONJ_TAC THENL
[MATCH_MP_TAC
REAL_INTEGRAL_COMBINE THEN
REPEAT(CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC]) THEN
MATCH_MP_TAC
REAL_INTEGRABLE_COMBINE THEN EXISTS_TAC `dd:real` THEN
ASM_SIMP_TAC[
ABSOLUTELY_REAL_INTEGRABLE_IMP_INTEGRABLE;
REAL_LT_IMP_LE];
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
`abs x < e / &2 ==> abs y <= x ==> abs y < e / &2`)) THEN
MATCH_MP_TAC
REAL_INTEGRAL_ABS_BOUND_INTEGRAL THEN
ASM_SIMP_TAC[
ABSOLUTELY_REAL_INTEGRABLE_IMP_INTEGRABLE] THEN
CONJ_TAC THENL
[MATCH_MP_TAC
REAL_INTEGRABLE_SUBINTERVAL THEN
MAP_EVERY EXISTS_TAC [`&0`; `d:real`] THEN
ASM_REWRITE_TAC[
SUBSET_REAL_INTERVAL] THEN ASM_REAL_ARITH_TAC;
X_GEN_TAC `x:real` THEN REWRITE_TAC[
IN_REAL_INTERVAL] THEN
SIMP_TAC[
REAL_ABS_MUL;
REAL_ABS_DIV; REAL_ARITH
`&0 <= x ==> abs x = x`] THEN
REPEAT STRIP_TAC THEN REWRITE_TAC[
real_div; REAL_MUL_ASSOC] THEN
MATCH_MP_TAC
REAL_LE_RMUL THEN ASM_REWRITE_TAC[
REAL_LE_INV_EQ] THEN
ONCE_REWRITE_TAC[REAL_ARITH `x * y <= y <=> x * y <= &1 * y`] THEN
MATCH_MP_TAC
REAL_LE_RMUL THEN
REWRITE_TAC[
REAL_ABS_POS;
SIN_BOUND]]]);;
(* ------------------------------------------------------------------------- *)
(* Convergence for functions of bounded variation. *)
(* ------------------------------------------------------------------------- *)
let REAL_INTEGRAL_SIN_OVER_X_BOUND = prove
(`!a b c.
&0 <= a /\ &0 < c
==> (\x. sin(c * x) / x)
real_integrable_on real_interval[a,b] /\
abs(
real_integral (
real_interval[a,b]) (\x. sin(c * x) / x)) <= &4`,
let lemma0 = prove
(`!a b. (\x. sin x) real_integrable_on (real_interval[a,b]) /\
abs(real_integral (real_interval[a,b]) (\x. sin x)) <= &2`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `a <= b` THENL
[MP_TAC(ISPECL [`\x. --(cos x)`; `\x. sin x`; `a:real`; `b:real`]
REAL_FUNDAMENTAL_THEOREM_OF_CALCULUS) THEN
REWRITE_TAC[] THEN ANTS_TAC THENL
[ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN REAL_DIFF_TAC THEN
REAL_ARITH_TAC;
REWRITE_TAC[HAS_REAL_INTEGRAL_INTEGRABLE_INTEGRAL] THEN STRIP_TAC THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(REAL_ARITH
`abs x <= &1 /\ abs y <= &1 ==> abs(--y - --x) <= &2`) THEN
REWRITE_TAC[COS_BOUND]];
RULE_ASSUM_TAC(REWRITE_RULE[REAL_NOT_LE]) THEN
ASM_SIMP_TAC[REAL_INTEGRABLE_ON_NULL; REAL_INTEGRAL_NULL; REAL_LT_IMP_LE;
REAL_ABS_NUM; REAL_POS]]) in
let lemma1 = prove
(`!a b. &0 < a
==> (\x. sin x / x) real_integrable_on real_interval[a,b] /\
abs(real_integral (real_interval[a,b])
(\x. sin x / x)) <= &4 / a`,
REPEAT GEN_TAC THEN DISCH_TAC THEN ASM_CASES_TAC `a <= b` THENL
[MP_TAC(ISPECL [`\x. sin x`; `\x:real. --(inv x)`; `a:real`; `b:real`]
REAL_SECOND_MEAN_VALUE_THEOREM_FULL) THEN
ASM_REWRITE_TAC[REAL_INTERVAL_EQ_EMPTY; REAL_NOT_LT; lemma0] THEN
ANTS_TAC THENL
[REWRITE_TAC[REAL_LE_NEG2; IN_REAL_INTERVAL] THEN REPEAT STRIP_TAC THEN
MATCH_MP_TAC REAL_LE_INV2 THEN ASM_REAL_ARITH_TAC;
DISCH_THEN(X_CHOOSE_THEN `c:real`
(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
DISCH_THEN(MP_TAC o MATCH_MP HAS_REAL_INTEGRAL_NEG) THEN
REWRITE_TAC[REAL_ARITH `--(--(inv y) * x):real = x / y`] THEN
REWRITE_TAC[HAS_REAL_INTEGRAL_INTEGRABLE_INTEGRAL] THEN STRIP_TAC THEN
ASM_REWRITE_TAC[REAL_NEG_ADD; REAL_MUL_LNEG; REAL_NEG_NEG] THEN
MATCH_MP_TAC(REAL_ARITH
`inv b <= inv a /\ abs x <= inv a * &2 /\ abs y <= inv b * &2
==> abs(x + y) <= &4 / a`) THEN
ASM_SIMP_TAC[REAL_LE_INV2; REAL_ABS_MUL] THEN CONJ_TAC THEN
MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[REAL_ABS_POS; lemma0] THEN
ASM_REWRITE_TAC[real_abs; REAL_LE_REFL; REAL_LE_INV_EQ] THEN
ASM_REAL_ARITH_TAC];
RULE_ASSUM_TAC(REWRITE_RULE[REAL_NOT_LE]) THEN
ASM_SIMP_TAC[REAL_INTEGRABLE_ON_NULL; REAL_INTEGRAL_NULL; REAL_LT_IMP_LE;
REAL_ABS_NUM; REAL_POS] THEN
MATCH_MP_TAC REAL_LE_DIV THEN ASM_REAL_ARITH_TAC]) in
let lemma2 = prove
(`!x. &0 <= x ==> sin(x) <= x`,
REPEAT STRIP_TAC THEN ASM_CASES_TAC `x <= &1` THENL
[ALL_TAC; ASM_MESON_TAC[SIN_BOUNDS; REAL_LE_TOTAL; REAL_LE_TRANS]] THEN
MP_TAC(ISPECL [`1`; `Cx x`] TAYLOR_CSIN) THEN
CONV_TAC(TOP_DEPTH_CONV num_CONV) THEN
REWRITE_TAC[VSUM_CLAUSES_NUMSEG; GSYM CX_SIN] THEN
CONV_TAC NUM_REDUCE_CONV THEN
REWRITE_TAC[GSYM CX_POW; GSYM CX_MUL; GSYM CX_DIV; GSYM CX_NEG;
GSYM CX_ADD; GSYM CX_SUB] THEN
REWRITE_TAC[COMPLEX_NORM_CX; IM_CX; REAL_ABS_0; REAL_EXP_0] THEN
SIMP_TAC[REAL_POW_1; REAL_DIV_1; real_pow;
REAL_MUL_LNEG; REAL_MUL_LID] THEN
MATCH_MP_TAC(REAL_ARITH
`e <= t ==> abs(sin x - (x + --t)) <= e ==> sin x <= x`) THEN
ASM_REWRITE_TAC[real_abs; REAL_ARITH
`x pow 5 / &24 <= x pow 3 / &6 <=>
x pow 3 * x pow 2 <= x pow 3 * &2 pow 2`] THEN
MATCH_MP_TAC REAL_LE_LMUL THEN ASM_SIMP_TAC[REAL_POW_LE] THEN
REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS] THEN ASM_REAL_ARITH_TAC) in
let lemma3 = prove
(`!x. &0 <= x /\ x <= &2 ==> abs(sin x / x) <= &1`,
GEN_TAC THEN STRIP_TAC THEN ASM_CASES_TAC `x = &0` THENL
[ASM_SIMP_TAC[real_div; REAL_MUL_RZERO; REAL_INV_0;
REAL_ABS_NUM; REAL_POS];
ASM_SIMP_TAC[REAL_ABS_DIV; REAL_LE_LDIV_EQ; REAL_MUL_LID;
REAL_ARITH `&0 <= x /\ ~(x = &0) ==> &0 < abs x`] THEN
MATCH_MP_TAC(REAL_ARITH `s <= x /\ &0 <= s ==> abs s <= abs x`) THEN
ASM_SIMP_TAC[lemma2] THEN MATCH_MP_TAC SIN_POS_PI_LE THEN
MP_TAC PI_APPROX_32 THEN ASM_REAL_ARITH_TAC]) in
let lemma4 = prove
(`!a b. &0 <= a /\ b <= &2
==> (\x. sin x / x) real_integrable_on real_interval[a,b] /\
abs(real_integral (real_interval[a,b])
(\x. sin x / x)) <= &2`,
REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_CASES_TAC `a <= b` THENL
[MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
[MATCH_MP_TAC REAL_MEASURABLE_BOUNDED_BY_INTEGRABLE_IMP_INTEGRABLE THEN
EXISTS_TAC `(\x. &1):real->real` THEN
REWRITE_TAC[REAL_INTEGRABLE_CONST] THEN CONJ_TAC THENL
[MATCH_MP_TAC REAL_MEASURABLE_ON_DIV THEN REPEAT CONJ_TAC THENL
[MATCH_MP_TAC INTEGRABLE_IMP_REAL_MEASURABLE THEN
GEN_REWRITE_TAC LAND_CONV [GSYM ETA_AX] THEN REWRITE_TAC[lemma0];
MATCH_MP_TAC CONTINUOUS_IMP_REAL_MEASURABLE_ON THEN
REWRITE_TAC[REAL_CONTINUOUS_ON_ID];
REWRITE_TAC[SING_GSPEC; REAL_NEGLIGIBLE_SING]];
REWRITE_TAC[IN_REAL_INTERVAL] THEN REPEAT STRIP_TAC THEN
MATCH_MP_TAC lemma3 THEN ASM_REAL_ARITH_TAC];
DISCH_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
EXISTS_TAC `real_integral (real_interval [a,b]) (\x. &1)` THEN
CONJ_TAC THENL
[MATCH_MP_TAC REAL_INTEGRAL_ABS_BOUND_INTEGRAL THEN
ASM_REWRITE_TAC[REAL_INTEGRABLE_CONST] THEN
REWRITE_TAC[IN_REAL_INTERVAL] THEN REPEAT STRIP_TAC THEN
MATCH_MP_TAC lemma3 THEN ASM_REAL_ARITH_TAC;
ASM_SIMP_TAC[REAL_INTEGRAL_CONST] THEN ASM_REAL_ARITH_TAC]];
RULE_ASSUM_TAC(REWRITE_RULE[REAL_NOT_LE]) THEN
ASM_SIMP_TAC[REAL_INTEGRABLE_ON_NULL; REAL_INTEGRAL_NULL; REAL_LT_IMP_LE;
REAL_ABS_NUM; REAL_POS]]) in
let lemma5 = prove
(`!a b. &0 <= a
==> (\x. sin x / x) real_integrable_on real_interval[a,b] /\
abs(real_integral (real_interval[a,b]) (\x. sin x / x)) <= &4`,
REPEAT GEN_TAC THEN DISCH_TAC THEN
ASM_CASES_TAC `b <= &2` THENL
[ASM_MESON_TAC[lemma4; REAL_ARITH `x <= &2 ==> x <= &4`]; ALL_TAC] THEN
ASM_CASES_TAC `&2 <= a` THENL
[MP_TAC(SPECL [`a:real`; `b:real`] lemma1) THEN
ANTS_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
MATCH_MP_TAC MONO_AND THEN REWRITE_TAC[] THEN
MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] REAL_LE_TRANS) THEN
ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_ARITH `&2 <= a ==> &0 < a`] THEN
ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
RULE_ASSUM_TAC(REWRITE_RULE[REAL_NOT_LE]) THEN
MP_TAC(ISPECL [`\x. sin x / x`; `a:real`; `b:real`; `&2`]
REAL_INTEGRABLE_COMBINE) THEN
ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN ANTS_TAC THENL
[CONJ_TAC THENL
[ASM_MESON_TAC[lemma4; REAL_LE_REFL];
ASM_MESON_TAC[lemma1; REAL_ARITH `&0 < &2`]];
DISCH_TAC] THEN
MP_TAC(ISPECL [`\x. sin x / x`; `a:real`; `b:real`; `&2`]
REAL_INTEGRAL_COMBINE) THEN
ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
MATCH_MP_TAC(REAL_ARITH
`abs(x) <= &2 /\ abs(y) <= &2 ==> abs(x + y) <= &4`) THEN
CONJ_TAC THENL
[ASM_MESON_TAC[lemma4; REAL_LE_REFL];
GEN_REWRITE_TAC RAND_CONV [REAL_ARITH `&2 = &4 / &2`] THEN
ASM_MESON_TAC[lemma1; REAL_ARITH `&0 < &2`]]) in
REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_CASES_TAC `a <= b` THENL
[MP_TAC(ISPECL [`c * a:real`; `c * b:real`] lemma5) THEN
ASM_SIMP_TAC[REAL_LE_MUL; REAL_LT_IMP_LE] THEN
DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
GEN_REWRITE_TAC LAND_CONV [HAS_REAL_INTEGRAL_INTEGRAL] THEN
DISCH_THEN(MP_TAC o SPEC `c:real` o MATCH_MP (REWRITE_RULE[IMP_CONJ]
HAS_REAL_INTEGRAL_STRETCH)) THEN
ASM_SIMP_TAC[REAL_LT_IMP_NZ; REAL_ADD_RID; REAL_SUB_RZERO] THEN
DISCH_THEN(MP_TAC o SPEC `c:real` o MATCH_MP HAS_REAL_INTEGRAL_LMUL) THEN
ASM_SIMP_TAC[IMAGE_STRETCH_REAL_INTERVAL; REAL_LE_INV_EQ; REAL_LT_IMP_LE;
REAL_FIELD `&0 < c ==> inv c * c * a = a`; REAL_INV_MUL; real_div;
REAL_FIELD `&0 < c ==> c * s * inv c * inv x = s * inv x`;
REAL_FIELD `&0 < c ==> c * inv c * i = i /\ abs c = c`] THEN
REWRITE_TAC[GSYM real_div; REAL_INTERVAL_EQ_EMPTY] THEN
ASM_SIMP_TAC[GSYM REAL_NOT_LE; REAL_LE_LMUL_EQ] THEN
REWRITE_TAC[HAS_REAL_INTEGRAL_INTEGRABLE_INTEGRAL] THEN
STRIP_TAC THEN ASM_REWRITE_TAC[];
RULE_ASSUM_TAC(REWRITE_RULE[REAL_NOT_LE]) THEN
ASM_SIMP_TAC[REAL_INTEGRABLE_ON_NULL; REAL_INTEGRAL_NULL; REAL_LT_IMP_LE;
REAL_ABS_NUM; REAL_POS]]);;
let FOURIER_JORDAN_BOUNDED_VARIATION = prove
(`!f x d.
f
absolutely_real_integrable_on real_interval[--pi,pi] /\
(!x. f(x + &2 * pi) = f x) /\
&0 < d /\
f
has_bounded_real_variation_on real_interval[x - d,x + d]
==> ((\n. sum (0..n)
(\k.
fourier_coefficient f k *
trigonometric_set k x))
---> ((reallim (atreal x within {l | l <= x}) f +
reallim (atreal x within {r | r >= x}) f) / &2))
sequentially`,
let lemma = prove
(`!f l d. &0 < d
==> ((f ---> l) (atreal (&0) within real_interval[&0,d]) <=>
(f ---> l) (atreal (&0) within {x | &0 <= x}))`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC REALLIM_TRANSFORM_WITHINREAL_SET THEN
REWRITE_TAC[EVENTUALLY_ATREAL] THEN EXISTS_TAC `d:real` THEN
ASM_REWRITE_TAC[IN_ELIM_THM; IN_REAL_INTERVAL] THEN REAL_ARITH_TAC) in
MAP_EVERY X_GEN_TAC [`f:real->real`; `t:real`; `d0:real`] THEN
STRIP_TAC THEN
ABBREV_TAC `s = (reallim (atreal t within {l | l <= t}) f +
reallim (atreal t within {r | r >= t}) f) / &2` THEN
MP_TAC(SPECL [`f:real->real`; `t:real`; `s:real`; `min d0 pi`]
FOURIER_SUM_LIMIT_SINE_PART) THEN
ASM_REWRITE_TAC[REAL_LT_MIN; PI_POS; REAL_ARITH `min d0 pi <= pi`] THEN
DISCH_THEN SUBST1_TAC THEN
ABBREV_TAC `h = \u. ((f:real->real)(t + u) + f(t - u)) - &2 * s` THEN
FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [FUN_EQ_THM]) THEN
SIMP_TAC[] THEN DISCH_THEN(K ALL_TAC) THEN ABBREV_TAC `d = min d0 pi` THEN
SUBGOAL_THEN `&0 < d` ASSUME_TAC THENL
[MP_TAC PI_POS THEN ASM_REAL_ARITH_TAC; ALL_TAC] THEN
SUBGOAL_THEN
`h has_bounded_real_variation_on real_interval[&0,d]`
ASSUME_TAC THENL
[FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I
[HAS_BOUNDED_REAL_VARIATION_DARBOUX]) THEN
EXPAND_TAC "h" THEN REWRITE_TAC[HAS_BOUNDED_REAL_VARIATION_DARBOUX] THEN
REWRITE_TAC[LEFT_IMP_EXISTS_THM; IN_REAL_INTERVAL] THEN
MAP_EVERY X_GEN_TAC [`f1:real->real`; `f2:real->real`] THEN STRIP_TAC THEN
EXISTS_TAC `\x. ((f1:real->real)(t + x) - f2(t - x)) - s` THEN
EXISTS_TAC `\x. ((f2:real->real)(t + x) - f1(t - x)) + s` THEN
ASM_REWRITE_TAC[REAL_ARITH `x - s <= y - s <=> x <= y`; REAL_LE_RADD] THEN
REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL [ALL_TAC; REAL_ARITH_TAC] THEN
REPEAT STRIP_TAC THEN MATCH_MP_TAC(REAL_ARITH
`a <= a' /\ b' <= b ==> a - b <= a' - b'`) THEN
CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN `(h ---> &0) (atreal(&0) within {x | &0 <= x})`
ASSUME_TAC THENL
[EXPAND_TAC "h" THEN EXPAND_TAC "s" THEN
REWRITE_TAC[REAL_ARITH
`(f' + f) - &2 * (l + l') / &2 = (f - l) + (f' - l')`] THEN
MATCH_MP_TAC REALLIM_NULL_ADD THEN CONJ_TAC THENL
[SUBGOAL_THEN
`?l. (f ---> l) (atreal t within {l | l <= t})` MP_TAC
THENL
[MP_TAC(ISPECL [`f:real->real`; `t - d0:real`; `t + d0:real`; `t:real`]
HAS_BOUNDED_REAL_VARIATION_LEFT_LIMIT) THEN
ASM_REWRITE_TAC[IN_REAL_INTERVAL] THEN
ANTS_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `l:real` THEN
REWRITE_TAC[REALLIM_WITHINREAL] THEN
MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `e:real` THEN
ASM_CASES_TAC `&0 < e` THEN
ASM_REWRITE_TAC[IN_REAL_INTERVAL; IN_ELIM_THM] THEN
DISCH_THEN(X_CHOOSE_THEN `d1:real` (fun th ->
EXISTS_TAC `min d0 d1` THEN
CONJUNCTS_THEN2 ASSUME_TAC MP_TAC th)) THEN
ASM_REWRITE_TAC[REAL_LT_MIN] THEN
MATCH_MP_TAC MONO_FORALL THEN ASM_REAL_ARITH_TAC;
DISCH_THEN(MP_TAC o SELECT_RULE) THEN
REWRITE_TAC[GSYM reallim] THEN
REWRITE_TAC[REALLIM_WITHINREAL] THEN
MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `e:real` THEN
ASM_CASES_TAC `&0 < e` THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `d1:real` THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN(fun th ->
X_GEN_TAC `x:real` THEN MP_TAC(SPEC `t - x:real` th)) THEN
MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[REAL_SUB_RZERO] THEN
REAL_ARITH_TAC];
SUBGOAL_THEN
`?l. (f ---> l) (atreal t within {r | r >= t})` MP_TAC
THENL
[MP_TAC(ISPECL [`f:real->real`; `t - d0:real`; `t + d0:real`; `t:real`]
HAS_BOUNDED_REAL_VARIATION_RIGHT_LIMIT) THEN
ASM_REWRITE_TAC[IN_REAL_INTERVAL] THEN
ANTS_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `l:real` THEN
REWRITE_TAC[REALLIM_WITHINREAL] THEN
MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `e:real` THEN
ASM_CASES_TAC `&0 < e` THEN
ASM_REWRITE_TAC[IN_REAL_INTERVAL; IN_ELIM_THM] THEN
DISCH_THEN(X_CHOOSE_THEN `d1:real` (fun th ->
EXISTS_TAC `min d0 d1` THEN
CONJUNCTS_THEN2 ASSUME_TAC MP_TAC th)) THEN
ASM_REWRITE_TAC[REAL_LT_MIN] THEN
MATCH_MP_TAC MONO_FORALL THEN ASM_REAL_ARITH_TAC;
DISCH_THEN(MP_TAC o SELECT_RULE) THEN
REWRITE_TAC[GSYM reallim] THEN
REWRITE_TAC[REALLIM_WITHINREAL] THEN
MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `e:real` THEN
ASM_CASES_TAC `&0 < e` THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `d1:real` THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN(fun th ->
X_GEN_TAC `x:real` THEN MP_TAC(SPEC `t + x:real` th)) THEN
MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[REAL_SUB_RZERO] THEN
REAL_ARITH_TAC]];
ALL_TAC] THEN
REWRITE_TAC[REALLIM_SEQUENTIALLY] THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
SUBGOAL_THEN
`?k. &0 < k /\ k < d /\
!n. (\x. sin ((&n + &1 / &2) * x) * h x / x)
real_integrable_on real_interval[&0,k] /\
abs(real_integral (real_interval[&0,k])
(\x. sin ((&n + &1 / &2) * x) * h x / x))
<= e / &2`
STRIP_ASSUME_TAC THENL
[SUBGOAL_THEN
`?h1 h2.
(!x y. x IN real_interval[&0,d] /\ y IN real_interval[&0,d] /\ x <= y
==> h1 x <= h1 y) /\
(!x y. x IN real_interval[&0,d] /\ y IN real_interval[&0,d] /\ x <= y
==> h2 x <= h2 y) /\
(h1 ---> &0) (atreal (&0) within {x | &0 <= x}) /\
(h2 ---> &0) (atreal (&0) within {x | &0 <= x}) /\
(!x. h x = h1 x - h2 x)`
STRIP_ASSUME_TAC THENL
[MP_TAC(ISPECL [`h:real->real`; `&0`; `d:real`]
HAS_BOUNDED_REAL_VARIATION_DARBOUX) THEN
ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`h1:real->real`; `h2:real->real`] THEN
STRIP_TAC THEN
MP_TAC(ISPECL [`h1:real->real`; `&0`; `d:real`; `&0`]
INCREASING_RIGHT_LIMIT) THEN
ASM_REWRITE_TAC[ENDS_IN_REAL_INTERVAL; REAL_INTERVAL_EQ_EMPTY] THEN
ASM_SIMP_TAC[REAL_NOT_LT; REAL_LT_IMP_LE] THEN
DISCH_THEN(X_CHOOSE_TAC `l:real`) THEN
MP_TAC(ISPECL [`h2:real->real`; `&0`; `d:real`; `&0`]
INCREASING_RIGHT_LIMIT) THEN
ASM_REWRITE_TAC[ENDS_IN_REAL_INTERVAL; REAL_INTERVAL_EQ_EMPTY] THEN
ASM_SIMP_TAC[REAL_NOT_LT; REAL_LT_IMP_LE] THEN
DISCH_THEN(X_CHOOSE_TAC `l':real`) THEN
SUBGOAL_THEN `l':real = l` SUBST_ALL_TAC THENL
[CONV_TAC SYM_CONV THEN ONCE_REWRITE_TAC[GSYM REAL_SUB_0] THEN
MATCH_MP_TAC(ISPEC `atreal (&0) within {x | &0 <= x}`
REALLIM_UNIQUE) THEN
EXISTS_TAC `h:real->real` THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
[W(MP_TAC o PART_MATCH (lhs o rand) TRIVIAL_LIMIT_WITHIN_REALINTERVAL o
rand o snd) THEN
REWRITE_TAC[is_realinterval; IN_ELIM_THM] THEN
ANTS_TAC THENL [REAL_ARITH_TAC; DISCH_THEN SUBST1_TAC] THEN
REWRITE_TAC[EXTENSION; NOT_FORALL_THM; IN_ELIM_THM; IN_SING] THEN
EXISTS_TAC `&1` THEN REAL_ARITH_TAC;
GEN_REWRITE_TAC (RATOR_CONV o LAND_CONV) [GSYM ETA_AX] THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REALLIM_SUB THEN
MAP_EVERY UNDISCH_TAC
[`(h1 ---> l) (atreal(&0) within real_interval[&0,d])`;
`(h2 ---> l') (atreal(&0) within real_interval[&0,d])`] THEN
ASM_SIMP_TAC[lemma]];
EXISTS_TAC `\x. (h1:real->real)(x) - l` THEN
EXISTS_TAC `\x. (h2:real->real)(x) - l` THEN
ASM_REWRITE_TAC[REAL_ARITH `x - l <= y - l <=> x <= y`] THEN
ASM_REWRITE_TAC[GSYM REALLIM_NULL] THEN
MAP_EVERY UNDISCH_TAC
[`(h1 ---> l) (atreal(&0) within real_interval[&0,d])`;
`(h2 ---> l) (atreal(&0) within real_interval[&0,d])`] THEN
ASM_SIMP_TAC[lemma] THEN REPEAT DISCH_TAC THEN REAL_ARITH_TAC];
ALL_TAC] THEN
SUBGOAL_THEN
`?k. &0 < k /\ k < d /\ abs(h1 k) < e / &16 /\ abs(h2 k) < e / &16`
MP_TAC THENL
[UNDISCH_TAC `(h2 ---> &0) (atreal (&0) within {x | &0 <= x})` THEN
UNDISCH_TAC `(h1 ---> &0) (atreal (&0) within {x | &0 <= x})` THEN
REWRITE_TAC[REALLIM_WITHINREAL; IN_ELIM_THM; REAL_SUB_RZERO] THEN
DISCH_THEN(MP_TAC o SPEC `e / &16`) THEN ANTS_TAC THENL
[ASM_REAL_ARITH_TAC;
DISCH_THEN(X_CHOOSE_THEN `k1:real` STRIP_ASSUME_TAC)] THEN
DISCH_THEN(MP_TAC o SPEC `e / &16`) THEN ANTS_TAC THENL
[ASM_REAL_ARITH_TAC;
DISCH_THEN(X_CHOOSE_THEN `k2:real` STRIP_ASSUME_TAC)] THEN
EXISTS_TAC `min d (min k1 k2) / &2` THEN
REPLICATE_TAC 2 (CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC]) THEN
CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `k:real` THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN X_GEN_TAC `n:num` THEN
MP_TAC(ISPECL [`\x. sin((&n + &1 / &2) * x) / x`; `h1:real->real`;
`&0`; `k:real`; `&0`; `(h1:real->real) k`]
REAL_SECOND_MEAN_VALUE_THEOREM_GEN_FULL) THEN
ASM_SIMP_TAC[REAL_INTERVAL_EQ_EMPTY; REAL_NOT_LT; REAL_LT_IMP_LE] THEN
ASM_SIMP_TAC[REAL_INTEGRAL_SIN_OVER_X_BOUND; REAL_LE_REFL; REAL_ADD_LID;
REAL_ARITH `&0 < &n + &1 / &2`; REAL_MUL_LZERO] THEN
ANTS_TAC THENL
[CONJ_TAC THENL
[X_GEN_TAC `x:real` THEN REWRITE_TAC[IN_REAL_INTERVAL] THEN
REPEAT STRIP_TAC THENL
[REWRITE_TAC[GSYM REAL_NOT_LT] THEN DISCH_TAC THEN
UNDISCH_TAC `(h1 ---> &0) (atreal (&0) within {x | &0 <= x})` THEN
REWRITE_TAC[REALLIM_WITHINREAL; IN_ELIM_THM; REAL_SUB_RZERO] THEN
DISCH_THEN(MP_TAC o SPEC `--((h1:real->real) x)`) THEN
REWRITE_TAC[NOT_IMP] THEN CONJ_TAC THENL
[ASM_REAL_ARITH_TAC; ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `dd:real` MP_TAC) THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC
(MP_TAC o SPEC `min d (min x dd) / &2`)) THEN
REWRITE_TAC[NOT_IMP] THEN CONJ_TAC THENL
[ASM_REAL_ARITH_TAC; ALL_TAC] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
`h < &0 ==> h' <= h ==> ~(abs h' < --h)`));
ALL_TAC] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN
REWRITE_TAC[IN_REAL_INTERVAL] THEN ASM_REAL_ARITH_TAC;
REWRITE_TAC[IN_REAL_INTERVAL] THEN REPEAT STRIP_TAC THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN
REWRITE_TAC[IN_REAL_INTERVAL] THEN ASM_REAL_ARITH_TAC];
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
[REAL_ARITH `h * s / x:real = s * h / x`] THEN
REWRITE_TAC[HAS_REAL_INTEGRAL_INTEGRABLE_INTEGRAL] THEN
DISCH_THEN(X_CHOOSE_THEN `c1:real` STRIP_ASSUME_TAC)] THEN
MP_TAC(ISPECL [`\x. sin((&n + &1 / &2) * x) / x`; `h2:real->real`;
`&0`; `k:real`; `&0`; `(h2:real->real) k`]
REAL_SECOND_MEAN_VALUE_THEOREM_GEN_FULL) THEN
ASM_SIMP_TAC[REAL_INTERVAL_EQ_EMPTY; REAL_NOT_LT; REAL_LT_IMP_LE] THEN
ASM_SIMP_TAC[REAL_INTEGRAL_SIN_OVER_X_BOUND; REAL_LE_REFL; REAL_ADD_LID;
REAL_ARITH `&0 < &n + &1 / &2`; REAL_MUL_LZERO] THEN
ANTS_TAC THENL
[CONJ_TAC THENL
[X_GEN_TAC `x:real` THEN REWRITE_TAC[IN_REAL_INTERVAL] THEN
REPEAT STRIP_TAC THENL
[REWRITE_TAC[GSYM REAL_NOT_LT] THEN DISCH_TAC THEN
UNDISCH_TAC `(h2 ---> &0) (atreal (&0) within {x | &0 <= x})` THEN
REWRITE_TAC[REALLIM_WITHINREAL; IN_ELIM_THM; REAL_SUB_RZERO] THEN
DISCH_THEN(MP_TAC o SPEC `--((h2:real->real) x)`) THEN
REWRITE_TAC[NOT_IMP] THEN CONJ_TAC THENL
[ASM_REAL_ARITH_TAC; ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `dd:real` MP_TAC) THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC
(MP_TAC o SPEC `min d (min x dd) / &2`)) THEN
REWRITE_TAC[NOT_IMP] THEN CONJ_TAC THENL
[ASM_REAL_ARITH_TAC; ALL_TAC] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
`h < &0 ==> h' <= h ==> ~(abs h' < --h)`));
ALL_TAC] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN
REWRITE_TAC[IN_REAL_INTERVAL] THEN ASM_REAL_ARITH_TAC;
REWRITE_TAC[IN_REAL_INTERVAL] THEN REPEAT STRIP_TAC THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN
REWRITE_TAC[IN_REAL_INTERVAL] THEN ASM_REAL_ARITH_TAC];
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
[REAL_ARITH `h * s / x:real = s * h / x`] THEN
REWRITE_TAC[HAS_REAL_INTEGRAL_INTEGRABLE_INTEGRAL] THEN
DISCH_THEN(X_CHOOSE_THEN `c2:real` STRIP_ASSUME_TAC)] THEN
REWRITE_TAC[REAL_ARITH
`s * (h - h') / x:real = s * h / x - s * h' / x`] THEN
ASM_SIMP_TAC[REAL_INTEGRABLE_SUB; REAL_INTEGRAL_SUB] THEN
MATCH_MP_TAC(REAL_ARITH
`abs(x) <= e / &16 * &4 /\ abs(y) <= e / &16 * &4
==> abs(x - y) <= e / &2`) THEN
REWRITE_TAC[REAL_ABS_MUL] THEN CONJ_TAC THEN
MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[REAL_ABS_POS] THEN
RULE_ASSUM_TAC(REWRITE_RULE[IN_REAL_INTERVAL]) THEN
ASM_SIMP_TAC[REAL_INTEGRAL_SIN_OVER_X_BOUND; REAL_LT_IMP_LE;
REAL_ARITH `&0 < &n + &1 / &2`];
ALL_TAC] THEN
MP_TAC(ISPECL [`f:real->real`; `--pi`; `pi`; `t:real`]
ABSOLUTELY_REAL_INTEGRABLE_PERIODIC_OFFSET) THEN
ASM_REWRITE_TAC[REAL_ARITH `pi - --pi = &2 * pi`] THEN
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [REAL_ADD_SYM] THEN
DISCH_THEN(fun th -> ASSUME_TAC th THEN MP_TAC th) THEN
GEN_REWRITE_TAC LAND_CONV [absolutely_real_integrable_on] THEN
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
[GSYM REAL_INTEGRABLE_REFLECT] THEN
REWRITE_TAC[GSYM absolutely_real_integrable_on; GSYM real_sub] THEN
REWRITE_TAC[REAL_NEG_NEG] THEN DISCH_TAC THEN
SUBGOAL_THEN
`(\x. h x / x) absolutely_real_integrable_on real_interval[k,d]`
ASSUME_TAC THENL
[REWRITE_TAC[ONCE_REWRITE_RULE[REAL_MUL_SYM] real_div] THEN
MATCH_MP_TAC ABSOLUTELY_REAL_INTEGRABLE_BOUNDED_MEASURABLE_PRODUCT THEN
REPEAT CONJ_TAC THENL
[GEN_REWRITE_TAC LAND_CONV [GSYM ETA_AX] THEN
MATCH_MP_TAC REAL_CONTINUOUS_IMP_REAL_MEASURABLE_ON_CLOSED_SUBSET THEN
REWRITE_TAC[REAL_CLOSED_REAL_INTERVAL] THEN
REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_CONTINUOUS_INV_WITHINREAL THEN
REWRITE_TAC[REAL_CONTINUOUS_WITHIN_ID] THEN
RULE_ASSUM_TAC(REWRITE_RULE[IN_REAL_INTERVAL]) THEN ASM_REAL_ARITH_TAC;
REWRITE_TAC[real_bounded; FORALL_IN_IMAGE; IN_REAL_INTERVAL] THEN
EXISTS_TAC `inv k:real` THEN REPEAT STRIP_TAC THEN
REWRITE_TAC[REAL_ABS_INV] THEN MATCH_MP_TAC REAL_LE_INV2 THEN
ASM_REAL_ARITH_TAC;
EXPAND_TAC "h" THEN MATCH_MP_TAC ABSOLUTELY_REAL_INTEGRABLE_SUB THEN
REWRITE_TAC[ABSOLUTELY_REAL_INTEGRABLE_CONST] THEN
MATCH_MP_TAC ABSOLUTELY_REAL_INTEGRABLE_ON_SUBINTERVAL THEN
EXISTS_TAC `real_interval[--pi,pi]` THEN
ASM_SIMP_TAC[ABSOLUTELY_REAL_INTEGRABLE_ADD] THEN
REWRITE_TAC[SUBSET_REAL_INTERVAL] THEN ASM_REAL_ARITH_TAC];
ALL_TAC] THEN
SUBGOAL_THEN
`!n. (\x. sin((&n + &1 / &2) * x) * h x / x) absolutely_real_integrable_on
real_interval[k,d]`
ASSUME_TAC THENL
[GEN_TAC THEN
MATCH_MP_TAC ABSOLUTELY_REAL_INTEGRABLE_BOUNDED_MEASURABLE_PRODUCT THEN
ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
[MATCH_MP_TAC REAL_CONTINUOUS_IMP_REAL_MEASURABLE_ON_CLOSED_SUBSET THEN
REWRITE_TAC[REAL_CLOSED_UNIV; REAL_CLOSED_REAL_INTERVAL] THEN
REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
REPEAT STRIP_TAC THEN
MATCH_MP_TAC REAL_CONTINUOUS_ATREAL_WITHINREAL THEN
MATCH_MP_TAC REAL_DIFFERENTIABLE_IMP_CONTINUOUS_ATREAL THEN
REAL_DIFFERENTIABLE_TAC;
REWRITE_TAC[real_bounded; FORALL_IN_IMAGE] THEN
EXISTS_TAC `&1` THEN REWRITE_TAC[SIN_BOUND]];
ALL_TAC] THEN
MP_TAC(ISPEC `\x. if k <= x /\ x <= d then h x / x else &0`
RIEMANN_LEBESGUE_SIN_HALF) THEN
REWRITE_TAC[absolutely_real_integrable_on] THEN
REWRITE_TAC[MESON[REAL_ABS_NUM]
`abs(if p then x else &0) = if p then abs x else &0`] THEN
ONCE_REWRITE_TAC[GSYM REAL_INTEGRAL_RESTRICT_UNIV; GSYM
REAL_INTEGRABLE_RESTRICT_UNIV] THEN
REWRITE_TAC[MESON[REAL_MUL_RZERO]
`(if P then s * (if Q then a else &0) else &0) =
(if P /\ Q then s * a else &0)`] THEN
REWRITE_TAC[IN_REAL_INTERVAL] THEN
REWRITE_TAC[MESON[] `(if P then if Q then x else &0 else &0) =
(if P /\ Q then x else &0)`] THEN
SUBGOAL_THEN `!x. (--pi <= x /\ x <= pi) /\ k <= x /\ x <= d <=>
k <= x /\ x <= d`
(fun th -> REWRITE_TAC[th])
THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
REWRITE_TAC[GSYM IN_REAL_INTERVAL; REAL_INTEGRAL_RESTRICT_UNIV;
REAL_INTEGRABLE_RESTRICT_UNIV] THEN
ASM_REWRITE_TAC[GSYM absolutely_real_integrable_on] THEN
REWRITE_TAC[REALLIM_SEQUENTIALLY] THEN
DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN ASM_REWRITE_TAC[REAL_HALF] THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `N:num` THEN
MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `n:num` THEN
MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[] THEN
FIRST_X_ASSUM(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC o SPEC `n:num`) THEN
MATCH_MP_TAC(REAL_ARITH
`x + y = z ==> abs(x) <= e / &2 ==> abs(y) < e / &2 ==> abs(z) < e`) THEN
REWRITE_TAC[REAL_SUB_RZERO] THEN MATCH_MP_TAC REAL_INTEGRAL_COMBINE THEN
REPEAT(CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC]) THEN
MATCH_MP_TAC REAL_INTEGRABLE_COMBINE THEN EXISTS_TAC `k:real` THEN
ASM_SIMP_TAC[ABSOLUTELY_REAL_INTEGRABLE_IMP_INTEGRABLE] THEN
ASM_REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Cesaro summability of Fourier series using Fejer kernel. *)
(* ------------------------------------------------------------------------- *)