Metamath Proof Explorer

Theorem fourierdlem115

Description: Fourier serier convergence, for piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem115.f 
|- ( ph -> F : RR --> RR )
fourierdlem115.t 
|- T = ( 2 x. _pi )
fourierdlem115.per 
|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
fourierdlem115.g 
|- G = ( ( RR _D F ) |` ( -u _pi (,) _pi ) )
fourierdlem115.dmdv 
|- ( ph -> ( ( -u _pi (,) _pi ) \ dom G ) e. Fin )
fourierdlem115.dvcn 
|- ( ph -> G e. ( dom G -cn-> CC ) )
fourierdlem115.rlim 
|- ( ( ph /\ x e. ( ( -u _pi [,) _pi ) \ dom G ) ) -> ( ( G |` ( x (,) +oo ) ) limCC x ) =/= (/) )
fourierdlem115.llim 
|- ( ( ph /\ x e. ( ( -u _pi (,] _pi ) \ dom G ) ) -> ( ( G |` ( -oo (,) x ) ) limCC x ) =/= (/) )
fourierdlem115.x 
|- ( ph -> X e. RR )
fourierdlem115.l 
|- ( ph -> L e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
fourierdlem115.r 
|- ( ph -> R e. ( ( F |` ( X (,) +oo ) ) limCC X ) )
fourierdlem115.a 
|- A = ( n e. NN0 |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) )
fourierdlem115.b 
|- B = ( n e. NN |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) )
fourierdlem115.s 
|- S = ( k e. NN |-> ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) )
Assertion fourierdlem115 
|- ( ph -> ( seq 1 ( + , S ) ~~> ( ( ( L + R ) / 2 ) - ( ( A ` 0 ) / 2 ) ) /\ ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( ( L + R ) / 2 ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem115.f 
 |-  ( ph -> F : RR --> RR )
2 fourierdlem115.t 
 |-  T = ( 2 x. _pi )
3 fourierdlem115.per 
 |-  ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
4 fourierdlem115.g 
 |-  G = ( ( RR _D F ) |` ( -u _pi (,) _pi ) )
5 fourierdlem115.dmdv 
 |-  ( ph -> ( ( -u _pi (,) _pi ) \ dom G ) e. Fin )
6 fourierdlem115.dvcn 
 |-  ( ph -> G e. ( dom G -cn-> CC ) )
7 fourierdlem115.rlim 
 |-  ( ( ph /\ x e. ( ( -u _pi [,) _pi ) \ dom G ) ) -> ( ( G |` ( x (,) +oo ) ) limCC x ) =/= (/) )
8 fourierdlem115.llim 
 |-  ( ( ph /\ x e. ( ( -u _pi (,] _pi ) \ dom G ) ) -> ( ( G |` ( -oo (,) x ) ) limCC x ) =/= (/) )
9 fourierdlem115.x 
 |-  ( ph -> X e. RR )
10 fourierdlem115.l 
 |-  ( ph -> L e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
11 fourierdlem115.r 
 |-  ( ph -> R e. ( ( F |` ( X (,) +oo ) ) limCC X ) )
12 fourierdlem115.a 
 |-  A = ( n e. NN0 |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) )
13 fourierdlem115.b 
 |-  B = ( n e. NN |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) )
14 fourierdlem115.s 
 |-  S = ( k e. NN |-> ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) )
15 oveq1 
 |-  ( n = k -> ( n x. x ) = ( k x. x ) )
16 15 fveq2d 
 |-  ( n = k -> ( cos ` ( n x. x ) ) = ( cos ` ( k x. x ) ) )
17 16 oveq2d 
 |-  ( n = k -> ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) = ( ( F ` x ) x. ( cos ` ( k x. x ) ) ) )
18 17 adantr 
 |-  ( ( n = k /\ x e. ( -u _pi (,) _pi ) ) -> ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) = ( ( F ` x ) x. ( cos ` ( k x. x ) ) ) )
19 18 itgeq2dv 
 |-  ( n = k -> S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x = S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( k x. x ) ) ) _d x )
20 19 oveq1d 
 |-  ( n = k -> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) = ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( k x. x ) ) ) _d x / _pi ) )
21 20 cbvmptv 
 |-  ( n e. NN0 |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) ) = ( k e. NN0 |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( k x. x ) ) ) _d x / _pi ) )
22 12 21 eqtri 
 |-  A = ( k e. NN0 |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( k x. x ) ) ) _d x / _pi ) )
23 15 fveq2d 
 |-  ( n = k -> ( sin ` ( n x. x ) ) = ( sin ` ( k x. x ) ) )
24 23 oveq2d 
 |-  ( n = k -> ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) = ( ( F ` x ) x. ( sin ` ( k x. x ) ) ) )
25 24 adantr 
 |-  ( ( n = k /\ x e. ( -u _pi (,) _pi ) ) -> ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) = ( ( F ` x ) x. ( sin ` ( k x. x ) ) ) )
26 25 itgeq2dv 
 |-  ( n = k -> S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x = S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( k x. x ) ) ) _d x )
27 26 oveq1d 
 |-  ( n = k -> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) = ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( k x. x ) ) ) _d x / _pi ) )
28 27 cbvmptv 
 |-  ( n e. NN |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) ) = ( k e. NN |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( k x. x ) ) ) _d x / _pi ) )
29 13 28 eqtri 
 |-  B = ( k e. NN |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( k x. x ) ) ) _d x / _pi ) )
30 eqid 
 |-  ( k e. NN |-> { w e. ( RR ^m ( 0 ... k ) ) | ( ( ( w ` 0 ) = -u _pi /\ ( w ` k ) = _pi ) /\ A. z e. ( 0 ..^ k ) ( w ` z ) < ( w ` ( z + 1 ) ) ) } ) = ( k e. NN |-> { w e. ( RR ^m ( 0 ... k ) ) | ( ( ( w ` 0 ) = -u _pi /\ ( w ` k ) = _pi ) /\ A. z e. ( 0 ..^ k ) ( w ` z ) < ( w ` ( z + 1 ) ) ) } )
31 id 
 |-  ( y = x -> y = x )
32 oveq2 
 |-  ( y = x -> ( _pi - y ) = ( _pi - x ) )
33 32 oveq1d 
 |-  ( y = x -> ( ( _pi - y ) / T ) = ( ( _pi - x ) / T ) )
34 33 fveq2d 
 |-  ( y = x -> ( |_ ` ( ( _pi - y ) / T ) ) = ( |_ ` ( ( _pi - x ) / T ) ) )
35 34 oveq1d 
 |-  ( y = x -> ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) = ( ( |_ ` ( ( _pi - x ) / T ) ) x. T ) )
36 31 35 oveq12d 
 |-  ( y = x -> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) = ( x + ( ( |_ ` ( ( _pi - x ) / T ) ) x. T ) ) )
37 36 cbvmptv 
 |-  ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) = ( x e. RR |-> ( x + ( ( |_ ` ( ( _pi - x ) / T ) ) x. T ) ) )
38 eqid 
 |-  ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) = ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) )
39 eqid 
 |-  ( ( # ` ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) - 1 ) = ( ( # ` ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) - 1 )
40 isoeq1 
 |-  ( g = f -> ( g Isom < , < ( ( 0 ... ( ( # ` ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) - 1 ) ) , ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) <-> f Isom < , < ( ( 0 ... ( ( # ` ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) - 1 ) ) , ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) ) )
41 40 cbviotavw 
 |-  ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) - 1 ) ) , ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) ) = ( iota f f Isom < , < ( ( 0 ... ( ( # ` ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) - 1 ) ) , ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) )
42 1 2 3 4 5 6 7 8 9 10 11 22 29 14 30 37 38 39 41 fourierdlem114 
 |-  ( ph -> ( seq 1 ( + , S ) ~~> ( ( ( L + R ) / 2 ) - ( ( A ` 0 ) / 2 ) ) /\ ( ( ( A ` 0 ) / 2 ) + sum_ k e. NN ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) ) = ( ( L + R ) / 2 ) ) )
43 42 simpld 
 |-  ( ph -> seq 1 ( + , S ) ~~> ( ( ( L + R ) / 2 ) - ( ( A ` 0 ) / 2 ) ) )
44 nfcv 
 |-  F/_ k ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) )
45 nfmpt1 
 |-  F/_ n ( n e. NN0 |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) )
46 12 45 nfcxfr 
 |-  F/_ n A
47 nfcv 
 |-  F/_ n k
48 46 47 nffv 
 |-  F/_ n ( A ` k )
49 nfcv 
 |-  F/_ n x.
50 nfcv 
 |-  F/_ n ( cos ` ( k x. X ) )
51 48 49 50 nfov 
 |-  F/_ n ( ( A ` k ) x. ( cos ` ( k x. X ) ) )
52 nfcv 
 |-  F/_ n +
53 nfmpt1 
 |-  F/_ n ( n e. NN |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) )
54 13 53 nfcxfr 
 |-  F/_ n B
55 54 47 nffv 
 |-  F/_ n ( B ` k )
56 nfcv 
 |-  F/_ n ( sin ` ( k x. X ) )
57 55 49 56 nfov 
 |-  F/_ n ( ( B ` k ) x. ( sin ` ( k x. X ) ) )
58 51 52 57 nfov 
 |-  F/_ n ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) )
59 fveq2 
 |-  ( n = k -> ( A ` n ) = ( A ` k ) )
60 oveq1 
 |-  ( n = k -> ( n x. X ) = ( k x. X ) )
61 60 fveq2d 
 |-  ( n = k -> ( cos ` ( n x. X ) ) = ( cos ` ( k x. X ) ) )
62 59 61 oveq12d 
 |-  ( n = k -> ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) = ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) )
63 fveq2 
 |-  ( n = k -> ( B ` n ) = ( B ` k ) )
64 60 fveq2d 
 |-  ( n = k -> ( sin ` ( n x. X ) ) = ( sin ` ( k x. X ) ) )
65 63 64 oveq12d 
 |-  ( n = k -> ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) = ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) )
66 62 65 oveq12d 
 |-  ( n = k -> ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) = ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) )
67 44 58 66 cbvsumi 
 |-  sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) = sum_ k e. NN ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) )
68 67 oveq2i 
 |-  ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( ( ( A ` 0 ) / 2 ) + sum_ k e. NN ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) )
69 42 simprd 
 |-  ( ph -> ( ( ( A ` 0 ) / 2 ) + sum_ k e. NN ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) ) = ( ( L + R ) / 2 ) )
70 68 69 syl5eq 
 |-  ( ph -> ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( ( L + R ) / 2 ) )
71 43 70 jca 
 |-  ( ph -> ( seq 1 ( + , S ) ~~> ( ( ( L + R ) / 2 ) - ( ( A ` 0 ) / 2 ) ) /\ ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( ( L + R ) / 2 ) ) )