P. 377 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37601-37700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fourierdlem63 37601*	The upper bound of intervals in the moved partition are mapped to points that are not greater than the corresponding upper bounds in the original partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- T = ( B - A )   &    |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- ( ph -> M e. NN )   &    |- ( ph -> Q e. ( P ` M ) )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> C < D )   &    |- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- H = ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } )   &    |- N = ( ( # ` H ) - 1 )   &    |- S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )   &    |- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )   &    |- ( ph -> K e. ( 0 ... M ) )   &    |- ( ph -> J e. ( 0..^ N ) )   &    |- ( ph -> Y e. ( ( S ` J ) [,) ( S ` ( J + 1 ) ) ) )   &    |- ( ph -> ( E ` Y ) < ( Q ` K ) )   &    |- X = ( ( Q ` K ) - ( ( E ` Y ) - Y ) )   =>    |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) <_ ( Q ` K ) )
Theorem	fourierdlem64 37602*	The partition V is finer than Q, when Q is moved on the same interval where V lies. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- T = ( B - A )   &    |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- ( ph -> M e. NN )   &    |- ( ph -> Q e. ( P ` M ) )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> C < D )   &    |- H = ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } )   &    |- N = ( ( # ` H ) - 1 )   &    |- V = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )   &    |- ( ph -> J e. ( 0..^ N ) )   &    |- L = sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < )   &    |- I = sup ( { j e. ( 0..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } , RR , < )   =>    |- ( ph -> ( ( I e. ( 0..^ M ) /\ L e. ZZ ) /\ E. i e. ( 0..^ M ) E. l e. ZZ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) )
Theorem	fourierdlem65 37603*	The distance of two adjacent points in the moved partition is preserved in the original partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- T = ( B - A )   &    |- ( ph -> M e. NN )   &    |- ( ph -> Q e. ( P ` M ) )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. ( C (,) +oo ) )   &    |- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- N = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) - 1 )   &    |- S = ( iota f f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) )   &    |- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )   &    |- L = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) )   &    |- Z = ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) )   =>    |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( L ` ( E ` ( S ` j ) ) ) ) = ( ( S ` ( j + 1 ) ) - ( S ` j ) ) )
Theorem	fourierdlem66 37604*	Value of the G function when the argument is not zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> X e. RR )   &    |- ( ph -> Y e. RR )   &    |- ( ph -> W e. RR )   &    |- D = ( n e. NN |-> ( s e. RR |-> if ( ( s mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) )   &    |- H = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )   &    |- K = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )   &    |- U = ( s e. ( -u pi [,] pi ) |-> ( ( H ` s ) x. ( K ` s ) ) )   &    |- S = ( s e. ( -u pi [,] pi ) |-> ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) )   &    |- G = ( s e. ( -u pi [,] pi ) |-> ( ( U ` s ) x. ( S ` s ) ) )   &    |- A = ( ( -u pi [,] pi ) \ { 0 } )   =>    |- ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( G ` s ) = ( pi x. ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) ) )
Theorem	fourierdlem67 37605*	G is a function (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> X e. RR )   &    |- ( ph -> Y e. RR )   &    |- ( ph -> W e. RR )   &    |- H = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )   &    |- K = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )   &    |- U = ( s e. ( -u pi [,] pi ) |-> ( ( H ` s ) x. ( K ` s ) ) )   &    |- ( ph -> N e. RR )   &    |- S = ( s e. ( -u pi [,] pi ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) )   &    |- G = ( s e. ( -u pi [,] pi ) |-> ( ( U ` s ) x. ( S ` s ) ) )   =>    |- ( ph -> G : ( -u pi [,] pi ) --> RR )
Theorem	fourierdlem68 37606*	The derivative of O is bounded on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> X e. RR )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A [,] B ) C_ ( -u pi [,] pi ) )   &    |- ( ph -> -. 0 e. ( A [,] B ) )   &    |- ( ph -> ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) : ( ( X + A ) (,) ( X + B ) ) --> RR )   &    |- ( ph -> D e. RR )   &    |- ( ( ph /\ t e. ( ( X + A ) (,) ( X + B ) ) ) -> ( abs ` ( F ` t ) ) <_ D )   &    |- ( ph -> E e. RR )   &    |- ( ( ph /\ t e. ( ( X + A ) (,) ( X + B ) ) ) -> ( abs ` ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` t ) ) <_ E )   &    |- ( ph -> C e. RR )   &    |- O = ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )   =>    |- ( ph -> ( dom ( RR _D O ) = ( A (,) B ) /\ E. b e. RR A. s e. dom ( RR _D O ) ( abs ` ( ( RR _D O ) ` s ) ) <_ b ) )
Theorem	fourierdlem69 37607*	A piecewise continuous function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- ( ph -> M e. NN )   &    |- ( ph -> Q e. ( P ` M ) )   &    |- ( ph -> F : ( A [,] B ) --> CC )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )   =>    |- ( ph -> F e. L^1 )
Theorem	fourierdlem70 37608*	A piecewise continuous function is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> F : ( A [,] B ) --> RR )   &    |- ( ph -> M e. NN )   &    |- ( ph -> Q : ( 0 ... M ) --> RR )   &    |- ( ph -> ( Q ` 0 ) = A )   &    |- ( ph -> ( Q ` M ) = B )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )   &    |- I = ( i e. ( 0..^ M ) |-> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )   =>    |- ( ph -> E. x e. RR A. s e. ( A [,] B ) ( abs ` ( F ` s ) ) <_ x )
Theorem	fourierdlem71 37609*	A periodic piecewise continuous function, possibly undefined on a finite set in each periodic interval, is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> dom F C_ RR )   &    |- ( ph -> F : dom F --> RR )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- T = ( B - A )   &    |- ( ph -> M e. NN )   &    |- ( ph -> Q : ( 0 ... M ) --> RR )   &    |- ( ph -> ( Q ` 0 ) = A )   &    |- ( ph -> ( Q ` M ) = B )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )   &    |- ( ( ( ph /\ x e. dom F ) /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. dom F )   &    |- ( ( ( ph /\ x e. dom F ) /\ k e. ZZ ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) )   &    |- I = ( i e. ( 0..^ M ) |-> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )   &    |- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )   =>    |- ( ph -> E. y e. RR A. x e. dom F ( abs ` ( F ` x ) ) <_ y )
Theorem	fourierdlem72 37610*	The derivative of O is continuous on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> X e. RR )   &    |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( -u pi + X ) /\ ( p ` m ) = ( pi + X ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- ( ph -> M e. NN )   &    |- ( ph -> V e. ( P ` M ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> RR ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A (,) B ) C_ ( -u pi [,] pi ) )   &    |- ( ph -> -. 0 e. ( A [,] B ) )   &    |- ( ph -> C e. RR )   &    |- Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )   &    |- ( ph -> U e. ( 0..^ M ) )   &    |- ( ph -> ( A (,) B ) C_ ( ( Q ` U ) (,) ( Q ` ( U + 1 ) ) ) )   &    |- H = ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / s ) )   &    |- K = ( s e. ( A (,) B ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )   &    |- O = ( s e. ( A (,) B ) |-> ( ( H ` s ) x. ( K ` s ) ) )   =>    |- ( ph -> ( RR _D O ) e. ( ( A (,) B ) -cn-> CC ) )
Theorem	fourierdlem73 37611*	A version of the Riemann Lebesgue lemma: as r increases, the integral in S goes to zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> F : ( A [,] B ) --> CC )   &    |- ( ph -> M e. NN )   &    |- ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )   &    |- ( ph -> ( Q ` 0 ) = A )   &    |- ( ph -> ( Q ` M ) = B )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )   &    |- G = ( RR _D F )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )   &    |- ( ph -> E. y e. RR A. x e. dom G ( abs ` ( G ` x ) ) <_ y )   &    |- S = ( r e. RR+ |-> S. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x )   &    |- D = ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) )   =>    |- ( ph -> A. e e. RR+ E. n e. NN A. r e. ( n (,) +oo ) ( abs ` S. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < e )
Theorem	fourierdlem74 37612*	Given a piecewise smooth function F, the derived function H has a limit at the upper bound of each interval of the partition Q. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> X e. RR )   &    |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( -u pi + X ) /\ ( p ` m ) = ( pi + X ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- ( ph -> F : RR --> RR )   &    |- ( ph -> X e. ran V )   &    |- ( ph -> Y e. RR )   &    |- ( ph -> W e. ( ( F |` ( -oo (,) X ) ) lim CC X ) )   &    |- H = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> V e. ( P ` M ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` ( i + 1 ) ) ) )   &    |- Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )   &    |- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = -u pi /\ ( p ` m ) = pi ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- G = ( RR _D F )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( G |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR )   &    |- ( ph -> E e. ( ( G |` ( -oo (,) X ) ) lim CC X ) )   &    |- A = if ( ( V ` ( i + 1 ) ) = X , E , ( ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) / ( Q ` ( i + 1 ) ) ) )   =>    |- ( ( ph /\ i e. ( 0..^ M ) ) -> A e. ( ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
Theorem	fourierdlem75 37613*	Given a piecewise smooth function F, the derived function H has a limit at the lower bound of each interval of the partition Q. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> X e. RR )   &    |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( -u pi + X ) /\ ( p ` m ) = ( pi + X ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- ( ph -> F : RR --> RR )   &    |- ( ph -> X e. ran V )   &    |- ( ph -> Y e. ( ( F |` ( X (,) +oo ) ) lim CC X ) )   &    |- ( ph -> W e. RR )   &    |- H = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> V e. ( P ` M ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` i ) ) )   &    |- Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )   &    |- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = -u pi /\ ( p ` m ) = pi ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- G = ( RR _D F )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( G |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> CC )   &    |- ( ph -> E e. ( ( G |` ( X (,) +oo ) ) lim CC X ) )   &    |- A = if ( ( V ` i ) = X , E , ( ( R - if ( ( V ` i ) < X , W , Y ) ) / ( Q ` i ) ) )   =>    |- ( ( ph /\ i e. ( 0..^ M ) ) -> A e. ( ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
Theorem	fourierdlem76 37614*	Continuity of O and its limits with respect to the S partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> X e. RR )   &    |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( -u pi + X ) /\ ( p ` m ) = ( pi + X ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- ( ph -> M e. NN )   &    |- ( ph -> V e. ( P ` M ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` i ) ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` ( i + 1 ) ) ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A [,] B ) C_ ( -u pi [,] pi ) )   &    |- ( ph -> -. 0 e. ( A [,] B ) )   &    |- ( ph -> C e. RR )   &    |- O = ( s e. ( A [,] B ) |-> ( ( ( ( F ` ( X + s ) ) - C ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )   &    |- Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )   &    |- T = ( { A , B } u. ( ran Q i^i ( A (,) B ) ) )   &    |- N = ( ( # ` T ) - 1 )   &    |- S = ( iota f f Isom < , < ( ( 0 ... N ) , T ) )   &    |- D = ( ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) ) x. ( ( S ` ( j + 1 ) ) / ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) ) )   &    |- E = ( ( ( if ( ( S ` j ) = ( Q ` i ) , R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) )   &    |- ( ch <-> ( ( ( ph /\ j e. ( 0..^ N ) ) /\ i e. ( 0..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )   =>    |- ( ( ( ( ph /\ j e. ( 0..^ N ) ) /\ i e. ( 0..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( D e. ( ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) lim CC ( S ` ( j + 1 ) ) ) /\ E e. ( ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) lim CC ( S ` j ) ) ) /\ ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) ) )
Theorem	fourierdlem77 37615*	If H is bounded, then U is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> X e. RR )   &    |- ( ph -> Y e. RR )   &    |- ( ph -> W e. RR )   &    |- H = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )   &    |- K = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )   &    |- U = ( s e. ( -u pi [,] pi ) |-> ( ( H ` s ) x. ( K ` s ) ) )   &    |- ( ph -> E. a e. RR A. s e. ( -u pi [,] pi ) ( abs ` ( H ` s ) ) <_ a )   =>    |- ( ph -> E. b e. RR+ A. s e. ( -u pi [,] pi ) ( abs ` ( U ` s ) ) <_ b )
Theorem	fourierdlem78 37616*	G is continuous when restricted on an interval not containing 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> A e. ( -u pi [,] pi ) )   &    |- ( ph -> B e. ( -u pi [,] pi ) )   &    |- ( ph -> X e. RR )   &    |- ( ph -> -. 0 e. ( A (,) B ) )   &    |- ( ph -> ( F |` ( ( A + X ) (,) ( B + X ) ) ) e. ( ( ( A + X ) (,) ( B + X ) ) -cn-> CC ) )   &    |- ( ph -> Y e. RR )   &    |- ( ph -> W e. RR )   &    |- H = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )   &    |- K = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )   &    |- U = ( s e. ( -u pi [,] pi ) |-> ( ( H ` s ) x. ( K ` s ) ) )   &    |- ( ph -> N e. RR )   &    |- S = ( s e. ( -u pi [,] pi ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) )   &    |- G = ( s e. ( -u pi [,] pi ) |-> ( ( U ` s ) x. ( S ` s ) ) )   =>    |- ( ph -> ( G |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> RR ) )
Theorem	fourierdlem79 37617*	E projects every interval of the partition induced by S on H into a corresponding interval of the partition induced by Q on [ A , B ]. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- T = ( B - A )   &    |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- ( ph -> M e. NN )   &    |- ( ph -> Q e. ( P ` M ) )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> C < D )   &    |- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- H = ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } )   &    |- N = ( ( # ` H ) - 1 )   &    |- S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )   &    |- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )   &    |- L = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) )   &    |- Z = ( ( S ` j ) + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) )   &    |- I = ( x e. RR |-> sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } , RR , < ) )   =>    |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( L ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` j ) ) ) (,) ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) )
Theorem	fourierdlem80 37618*	The derivative of O is bounded on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> X e. RR )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( A [,] B ) C_ ( -u pi [,] pi ) )   &    |- ( ph -> -. 0 e. ( A [,] B ) )   &    |- ( ph -> C e. RR )   &    |- O = ( s e. ( A [,] B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )   &    |- I = ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) )   &    |- ( ( ph /\ j e. ( 0..^ N ) ) -> E. w e. RR A. t e. I ( abs ` ( F ` t ) ) <_ w )   &    |- ( ( ph /\ j e. ( 0..^ N ) ) -> E. z e. RR A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z )   &    |- ( ph -> S : ( 0 ... N ) --> ( A [,] B ) )   &    |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( S ` j ) < ( S ` ( j + 1 ) ) )   &    |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( S ` j ) [,] ( S ` ( j + 1 ) ) ) C_ ( A [,] B ) )   &    |- ( ( ( ph /\ r e. ( A [,] B ) ) /\ -. r e. ran S ) -> E. k e. ( 0..^ N ) r e. ( ( S ` k ) (,) ( S ` ( k + 1 ) ) ) )   &    |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( RR _D ( F |` I ) ) : I --> RR )   &    |- Y = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )   &    |- ( ch <-> ( ( ( ( ( ph /\ j e. ( 0..^ N ) ) /\ w e. RR ) /\ z e. RR ) /\ A. t e. I ( abs ` ( F ` t ) ) <_ w ) /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) )   =>    |- ( ph -> E. b e. RR A. s e. dom ( RR _D O ) ( abs ` ( ( RR _D O ) ` s ) ) <_ b )
Theorem	fourierdlem81 37619*	The integral of a piecewise continuous periodic function F is unchanged if the domain is shifted by its period T. In this lemma, T is assumed to be strictly positive. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- ( ph -> M e. NN )   &    |- ( ph -> T e. RR+ )   &    |- ( ph -> Q e. ( P ` M ) )   &    |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` ( x + T ) ) = ( F ` x ) )   &    |- S = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) + T ) )   &    |- ( ph -> F : RR --> CC )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )   &    |- G = ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) )   &    |- H = ( x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) |-> ( G ` ( x - T ) ) )   =>    |- ( ph -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
Theorem	fourierdlem82 37620*	Integral by substitution, adding a constant to the function's argument, for a function on an open interval with finite limits ad boundary points. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> F : ( A [,] B ) --> CC )   &    |- ( ph -> ( F |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC ) )   &    |- ( ph -> L e. ( F lim CC B ) )   &    |- ( ph -> R e. ( F lim CC A ) )   &    |- ( ph -> X e. RR )   =>    |- ( ph -> S. ( A [,] B ) ( F ` t ) _d t = S. ( ( A - X ) [,] ( B - X ) ) ( F ` ( X + t ) ) _d t )
Theorem	fourierdlem83 37621*	The fourier partial sum for F rewritten as an integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : RR --> RR )   &    |- C = ( -u pi (,) pi )   &    |- ( ph -> ( F |` C ) e. L^1 )   &    |- A = ( n e. NN0 |-> ( S. C ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / pi ) )   &    |- B = ( n e. NN |-> ( S. C ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / pi ) )   &    |- ( ph -> X e. RR )   &    |- S = ( m e. NN |-> ( ( ( A ` 0 ) / 2 ) + sum_ n e. ( 1 ... m ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) )   &    |- D = ( n e. NN |-> ( s e. RR |-> if ( ( s mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) )   &    |- ( ph -> N e. NN )   =>    |- ( ph -> ( S ` N ) = S. C ( ( F ` x ) x. ( ( D ` N ) ` ( x - X ) ) ) _d x )
Theorem	fourierdlem84 37622*	If F is piecewise coninuous and D is continuous, then G is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> F : RR --> RR )   &    |- ( ph -> X e. RR )   &    |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A + X ) /\ ( p ` m ) = ( B + X ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- ( ph -> M e. NN )   &    |- ( ph -> V e. ( P ` M ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` i ) ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` ( i + 1 ) ) ) )   &    |- Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )   &    |- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- ( ph -> D e. ( RR -cn-> RR ) )   &    |- G = ( s e. ( A [,] B ) |-> ( ( F ` ( X + s ) ) x. ( D ` s ) ) )   =>    |- ( ph -> G e. L^1 )
Theorem	fourierdlem85 37623*	Limit of the function G at the lower bounds of the partition intervals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( -u pi + X ) /\ ( p ` m ) = ( pi + X ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- ( ph -> F : RR --> RR )   &    |- ( ph -> X e. ran V )   &    |- ( ph -> Y e. ( ( F |` ( X (,) +oo ) ) lim CC X ) )   &    |- ( ph -> W e. RR )   &    |- H = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )   &    |- K = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )   &    |- U = ( s e. ( -u pi [,] pi ) |-> ( ( H ` s ) x. ( K ` s ) ) )   &    |- ( ph -> N e. RR )   &    |- S = ( s e. ( -u pi [,] pi ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) )   &    |- G = ( s e. ( -u pi [,] pi ) |-> ( ( U ` s ) x. ( S ` s ) ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> V e. ( P ` M ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` i ) ) )   &    |- Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )   &    |- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = -u pi /\ ( p ` m ) = pi ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- I = ( RR _D F )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( I |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> CC )   &    |- ( ph -> E e. ( ( I |` ( X (,) +oo ) ) lim CC X ) )   &    |- A = ( ( if ( ( V ` i ) = X , E , ( ( R - if ( ( V ` i ) < X , W , Y ) ) / ( Q ` i ) ) ) x. ( K ` ( Q ` i ) ) ) x. ( S ` ( Q ` i ) ) )   =>    |- ( ( ph /\ i e. ( 0..^ M ) ) -> A e. ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
Theorem	fourierdlem86 37624*	Continuity of O and its limits with respect to the S partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> X e. RR )   &    |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( -u pi + X ) /\ ( p ` m ) = ( pi + X ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- ( ph -> M e. NN )   &    |- ( ph -> V e. ( P ` M ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` i ) ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` ( i + 1 ) ) ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A [,] B ) C_ ( -u pi [,] pi ) )   &    |- ( ph -> -. 0 e. ( A [,] B ) )   &    |- ( ph -> C e. RR )   &    |- O = ( s e. ( A [,] B ) |-> ( ( ( ( F ` ( X + s ) ) - C ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )   &    |- Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )   &    |- T = ( { A , B } u. ( ran Q i^i ( A (,) B ) ) )   &    |- N = ( ( # ` T ) - 1 )   &    |- S = ( iota f f Isom < , < ( ( 0 ... N ) , T ) )   &    |- D = ( ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( U + 1 ) ) , [_ U / i ]_ L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) ) x. ( ( S ` ( j + 1 ) ) / ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) ) )   &    |- E = ( ( ( if ( ( S ` j ) = ( Q ` U ) , [_ U / i ]_ R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) )   &    |- U = ( iota_ i e. ( 0..^ M ) ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )   =>    |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( D e. ( ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) lim CC ( S ` ( j + 1 ) ) ) /\ E e. ( ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) lim CC ( S ` j ) ) ) /\ ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) ) )
Theorem	fourierdlem87 37625*	The integral of G goes uniformly ( with respect to n) to zero if the measure of the domain of integration goes to zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> X e. RR )   &    |- ( ph -> Y e. RR )   &    |- ( ph -> W e. RR )   &    |- H = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )   &    |- K = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )   &    |- U = ( s e. ( -u pi [,] pi ) |-> ( ( H ` s ) x. ( K ` s ) ) )   &    |- S = ( s e. ( -u pi [,] pi ) |-> ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) )   &    |- G = ( s e. ( -u pi [,] pi ) |-> ( ( U ` s ) x. ( S ` s ) ) )   &    |- ( ph -> E. x e. RR A. s e. ( -u pi [,] pi ) ( abs ` ( H ` s ) ) <_ x )   &    |- ( ( ph /\ n e. NN ) -> G e. L^1 )   &    |- D = ( ( e / 3 ) / a )   &    |- ( ch <-> ( ( ( ( ( ph /\ e e. RR+ ) /\ a e. RR+ /\ A. n e. NN A. s e. ( -u pi [,] pi ) ( abs ` ( G ` s ) ) <_ a ) /\ u e. dom vol ) /\ ( u C_ ( -u pi [,] pi ) /\ ( vol ` u ) <_ D ) ) /\ n e. NN ) )   =>    |- ( ( ph /\ e e. RR+ ) -> E. d e. RR+ A. u e. dom vol ( ( u C_ ( -u pi [,] pi ) /\ ( vol ` u ) <_ d ) -> A. k e. NN ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) )
Theorem	fourierdlem88 37626*	Given a piecewise continuous function F, a continuous function K and a continuous function S, the function G is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( -u pi + X ) /\ ( p ` m ) = ( pi + X ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- ( ph -> F : RR --> RR )   &    |- ( ph -> X e. ran V )   &    |- ( ph -> Y e. ( ( F |` ( X (,) +oo ) ) lim CC X ) )   &    |- ( ph -> W e. ( ( F |` ( -oo (,) X ) ) lim CC X ) )   &    |- H = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )   &    |- K = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )   &    |- U = ( s e. ( -u pi [,] pi ) |-> ( ( H ` s ) x. ( K ` s ) ) )   &    |- ( ph -> N e. RR )   &    |- S = ( s e. ( -u pi [,] pi ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) )   &    |- G = ( s e. ( -u pi [,] pi ) |-> ( ( U ` s ) x. ( S ` s ) ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> V e. ( P ` M ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` i ) ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` ( i + 1 ) ) ) )   &    |- Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )   &    |- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = -u pi /\ ( p ` m ) = pi ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- I = ( RR _D F )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( I |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR )   &    |- ( ph -> C e. ( ( I |` ( -oo (,) X ) ) lim CC X ) )   &    |- ( ph -> D e. ( ( I |` ( X (,) +oo ) ) lim CC X ) )   =>    |- ( ph -> G e. L^1 )
Theorem	fourierdlem89 37627*	Given a piecewise continuous function and changing the interval and the partition, the limit at the lower bound of each interval of the moved partition is still finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- T = ( B - A )   &    |- ( ph -> M e. NN )   &    |- ( ph -> Q e. ( P ` M ) )   &    |- ( ph -> F : RR --> CC )   &    |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. ( C (,) +oo ) )   &    |- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- H = ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } )   &    |- N = ( ( # ` H ) - 1 )   &    |- S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )   &    |- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )   &    |- Z = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) )   &    |- ( ph -> J e. ( 0..^ N ) )   &    |- U = ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) )   &    |- I = ( x e. RR |-> sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( Z ` ( E ` x ) ) } , RR , < ) )   &    |- V = ( i e. ( 0..^ M ) |-> R )   =>    |- ( ph -> if ( ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) , ( V ` ( I ` ( S ` J ) ) ) , ( F ` ( Z ` ( E ` ( S ` J ) ) ) ) ) e. ( ( F |` ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) lim CC ( S ` J ) ) )
Theorem	fourierdlem90 37628*	Given a piecewise continuous function, it is still continuous with respect to an open interval of the moved partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- T = ( B - A )   &    |- ( ph -> M e. NN )   &    |- ( ph -> Q e. ( P ` M ) )   &    |- ( ph -> F : RR --> CC )   &    |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. ( C (,) +oo ) )   &    |- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- H = ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } )   &    |- N = ( ( # ` H ) - 1 )   &    |- S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )   &    |- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )   &    |- L = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) )   &    |- ( ph -> J e. ( 0..^ N ) )   &    |- U = ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) )   &    |- G = ( F |` ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) )   &    |- R = ( y e. ( ( ( L ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) |-> ( G ` ( y - U ) ) )   &    |- I = ( x e. RR |-> sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } , RR , < ) )   =>    |- ( ph -> ( F |` ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) e. ( ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) -cn-> CC ) )
Theorem	fourierdlem91 37629*	Given a piecewise continuous function and changing the interval and the partition, the limit at the upper bound of each interval of the moved partition is still finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- T = ( B - A )   &    |- ( ph -> M e. NN )   &    |- ( ph -> Q e. ( P ` M ) )   &    |- ( ph -> F : RR --> CC )   &    |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. ( C (,) +oo ) )   &    |- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- H = ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } )   &    |- N = ( ( # ` H ) - 1 )   &    |- S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )   &    |- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )   &    |- Z = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) )   &    |- ( ph -> J e. ( 0..^ N ) )   &    |- U = ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) )   &    |- I = ( x e. RR |-> sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( Z ` ( E ` x ) ) } , RR , < ) )   &    |- W = ( i e. ( 0..^ M ) |-> L )   =>    |- ( ph -> if ( ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) , ( W ` ( I ` ( S ` J ) ) ) , ( F ` ( E ` ( S ` ( J + 1 ) ) ) ) ) e. ( ( F |` ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) lim CC ( S ` ( J + 1 ) ) ) )
Theorem	fourierdlem92 37630*	The integral of a piecewise continuous periodic function F is unchanged if the domain is shifted by its period T. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- ( ph -> M e. NN )   &    |- ( ph -> T e. RR )   &    |- ( ph -> Q e. ( P ` M ) )   &    |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` ( x + T ) ) = ( F ` x ) )   &    |- S = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) + T ) )   &    |- H = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A + T ) /\ ( p ` m ) = ( B + T ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- ( ph -> F : RR --> CC )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )   =>    |- ( ph -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
Theorem	fourierdlem93 37631*	Integral by substitution (the domain is shifted by X) for a piecewise continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = -u pi /\ ( p ` m ) = pi ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- H = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> Q e. ( P ` M ) )   &    |- ( ph -> X e. RR )   &    |- ( ph -> F : ( -u pi [,] pi ) --> CC )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )   =>    |- ( ph -> S. ( -u pi [,] pi ) ( F ` t ) _d t = S. ( ( -u pi - X ) [,] ( pi - X ) ) ( F ` ( X + s ) ) _d s )
Theorem	fourierdlem94 37632*	For a piecewise smooth function, the left and the right limits exist at any point. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : RR --> RR )   &    |- T = ( 2 x. pi )   &    |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )   &    |- ( ph -> X e. RR )   &    |- P = ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = -u pi /\ ( p ` n ) = pi ) /\ A. i e. ( 0..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- ( ph -> M e. NN )   &    |- ( ph -> Q e. ( P ` M ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) =/= (/) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) =/= (/) )   =>    |- ( ph -> ( ( ( F |` ( -oo (,) X ) ) lim CC X ) =/= (/) /\ ( ( F |` ( X (,) +oo ) ) lim CC X ) =/= (/) ) )
Theorem	fourierdlem95 37633*	Algebraic manipulation of integrals, used by other lemmas. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> X e. RR )   &    |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( -u pi + X ) /\ ( p ` m ) = ( pi + X ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- ( ph -> M e. NN )   &    |- ( ph -> V e. ( P ` M ) )   &    |- ( ph -> X e. ran V )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` i ) ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` ( i + 1 ) ) ) )   &    |- H = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )   &    |- K = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )   &    |- U = ( s e. ( -u pi [,] pi ) |-> ( ( H ` s ) x. ( K ` s ) ) )   &    |- S = ( s e. ( -u pi [,] pi ) |-> ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) )   &    |- G = ( s e. ( -u pi [,] pi ) |-> ( ( U ` s ) x. ( S ` s ) ) )   &    |- I = ( RR _D F )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( I |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR )   &    |- ( ph -> B e. ( ( I |` ( -oo (,) X ) ) lim CC X ) )   &    |- ( ph -> C e. ( ( I |` ( X (,) +oo ) ) lim CC X ) )   &    |- ( ph -> Y e. ( ( F |` ( X (,) +oo ) ) lim CC X ) )   &    |- ( ph -> W e. ( ( F |` ( -oo (,) X ) ) lim CC X ) )   &    |- ( ph -> A e. dom vol )   &    |- ( ph -> A C_ ( ( -u pi [,] pi ) \ { 0 } ) )   &    |- E = ( n e. NN |-> ( S. A ( G ` s ) _d s / pi ) )   &    |- D = ( n e. NN |-> ( s e. RR |-> if ( ( s mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) )   &    |- ( ph -> O e. RR )   &    |- ( ( ph /\ s e. A ) -> if ( 0 < s , Y , W ) = O )   &    |- ( ( ph /\ n e. NN ) -> S. A ( ( D ` n ) ` s ) _d s = ( 1 / 2 ) )   =>    |- ( ( ph /\ n e. NN ) -> ( ( E ` n ) + ( O / 2 ) ) = S. A ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s )
Theorem	fourierdlem96 37634*	limit for F at the lower bound of an interval for the moved partition V. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : RR --> RR )   &    |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- T = ( B - A )   &    |- ( ph -> M e. NN )   &    |- ( ph -> Q e. ( P ` M ) )   &    |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. ( C (,) +oo ) )   &    |- ( ph -> J e. ( 0..^ ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) )   &    |- V = ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) )   =>    |- ( ph -> if ( ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` J ) ) ) = ( Q ` ( ( y e. RR |-> sup ( { j e. ( 0..^ M ) | ( Q ` j ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) ) } , RR , < ) ) ` ( V ` J ) ) ) , ( ( i e. ( 0..^ M ) |-> R ) ` ( ( y e. RR |-> sup ( { j e. ( 0..^ M ) | ( Q ` j ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) ) } , RR , < ) ) ` ( V ` J ) ) ) , ( F ` ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` J ) ) ) ) ) e. ( ( F |` ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) lim CC ( V ` J ) ) )
Theorem	fourierdlem97 37635*	F is continuous on the intervals induced by the moved partition V. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : RR --> RR )   &    |- G = ( RR _D F )   &    |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A e. RR )   &    |- T = ( B - A )   &    |- ( ph -> M e. NN )   &    |- ( ph -> Q e. ( P ` M ) )   &    |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. ( C (,) +oo ) )   &    |- ( ph -> J e. ( 0..^ ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) )   &    |- V = ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) )   &    |- H = ( s e. RR |-> if ( s e. dom G , ( G ` s ) , 0 ) )   =>    |- ( ph -> ( G |` ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) e. ( ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) -cn-> CC ) )
Theorem	fourierdlem98 37636*	F is continuous on the intervals induced by the moved partition V. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : RR --> RR )   &    |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- T = ( B - A )   &    |- ( ph -> M e. NN )   &    |- ( ph -> Q e. ( P ` M ) )   &    |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 )