HomeHome Metamath Proof Explorer
Theorem List (p. 381 of 409)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Color key:    Metamath Proof Explorer  Metamath Proof Explorer
(1-26620)
  Hilbert Space Explorer  Hilbert Space Explorer
(26621-28143)
  Users' Mathboxes  Users' Mathboxes
(28144-40813)
 

Theorem List for Metamath Proof Explorer - 38001-38100   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremdirkertrigeq 38001* Trigonometric equality for the Dirichlet kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  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 )   &    |-  F  =  ( D `  N )   &    |-  H  =  ( s  e.  RR  |->  ( ( ( 1  /  2
 )  +  sum_ k  e.  ( 1 ... N ) ( cos `  (
 k  x.  s ) ) )  /  pi ) )   =>    |-  ( ph  ->  F  =  H )
 
Theoremdirkeritg 38002* The definite integral of the Dirichlet Kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  D  =  ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( x  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  n )  +  1 )  /  (
 2  x.  pi ) ) ,  ( ( sin `  ( ( n  +  ( 1  /  2 ) )  x.  x ) ) 
 /  ( ( 2  x.  pi )  x.  ( sin `  ( x  /  2 ) ) ) ) ) ) )   &    |-  ( ph  ->  N  e.  NN )   &    |-  F  =  ( D `  N )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <_  B )   &    |-  G  =  ( x  e.  ( A [,] B )  |->  ( ( ( x  /  2 )  +  sum_ k  e.  (
 1 ... N ) ( ( sin `  (
 k  x.  x ) )  /  k ) )  /  pi ) )   =>    |-  ( ph  ->  S. ( A (,) B ) ( F `  x )  _d x  =  ( ( G `  B )  -  ( G `  A ) ) )
 
Theoremdirkercncflem1 38003* If  Y is a multiple of  pi then it belongs to an open inerval  ( A (,) B ) such that for any other point  y in the interval, cos y/2 and sin y/2 are non zero. Such an interval is needed to apply De L'Hopital theorem. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  A  =  ( Y  -  pi )   &    |-  B  =  ( Y  +  pi )   &    |-  ( ph  ->  Y  e.  RR )   &    |-  ( ph  ->  ( Y  mod  ( 2  x.  pi ) )  =  0 )   =>    |-  ( ph  ->  ( Y  e.  ( A (,) B )  /\  A. y  e.  ( ( A (,) B )  \  { Y } ) ( ( sin `  (
 y  /  2 )
 )  =/=  0  /\  ( cos `  ( y  /  2 ) )  =/=  0 ) ) )
 
Theoremdirkercncflem2 38004* Lemma used to proof that the Dirichlet Kernel is continuous at  Y points that are multiples of 
( 2  x.  pi ). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  D  =  ( n  e.  NN  |->  ( y  e.  RR  |->  if ( ( y  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  n )  +  1 )  /  (
 2  x.  pi ) ) ,  ( ( sin `  ( ( n  +  ( 1  /  2 ) )  x.  y ) ) 
 /  ( ( 2  x.  pi )  x.  ( sin `  (
 y  /  2 )
 ) ) ) ) ) )   &    |-  F  =  ( y  e.  ( ( A (,) B ) 
 \  { Y }
 )  |->  ( sin `  (
 ( N  +  (
 1  /  2 )
 )  x.  y ) ) )   &    |-  G  =  ( y  e.  ( ( A (,) B ) 
 \  { Y }
 )  |->  ( ( 2  x.  pi )  x.  ( sin `  (
 y  /  2 )
 ) ) )   &    |-  (
 ( ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  ->  ( sin `  ( y  /  2 ) )  =/=  0 )   &    |-  H  =  ( y  e.  (
 ( A (,) B )  \  { Y }
 )  |->  ( ( N  +  ( 1  / 
 2 ) )  x.  ( cos `  (
 ( N  +  (
 1  /  2 )
 )  x.  y ) ) ) )   &    |-  I  =  ( y  e.  (
 ( A (,) B )  \  { Y }
 )  |->  ( pi  x.  ( cos `  ( y  /  2 ) ) ) )   &    |-  L  =  ( w  e.  ( A (,) B )  |->  ( ( ( N  +  ( 1  /  2
 ) )  x.  ( cos `  ( ( N  +  ( 1  / 
 2 ) )  x.  w ) ) ) 
 /  ( pi  x.  ( cos `  ( w  /  2 ) ) ) ) )   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  Y  e.  ( A (,) B ) )   &    |-  ( ph  ->  ( Y  mod  ( 2  x.  pi ) )  =  0
 )   &    |-  ( ( ph  /\  y  e.  ( ( A (,) B )  \  { Y } ) )  ->  ( cos `  ( y  /  2 ) )  =/=  0 )   =>    |-  ( ph  ->  ( ( D `  N ) `  Y )  e.  ( ( ( D `
  N )  |`  ( ( A (,) B )  \  { Y } ) ) lim CC  Y ) )
 
Theoremdirkercncflem3 38005* The Dirichlet Kernel is continuous at  Y points that are multiples of  ( 2  x.  pi ). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  D  =  ( n  e.  NN  |->  ( y  e.  RR  |->  if ( ( y  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  n )  +  1 )  /  (
 2  x.  pi ) ) ,  ( ( sin `  ( ( n  +  ( 1  /  2 ) )  x.  y ) ) 
 /  ( ( 2  x.  pi )  x.  ( sin `  (
 y  /  2 )
 ) ) ) ) ) )   &    |-  A  =  ( Y  -  pi )   &    |-  B  =  ( Y  +  pi )   &    |-  F  =  ( y  e.  ( A (,) B )  |->  ( ( sin `  (
 ( n  +  (
 1  /  2 )
 )  x.  y ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
 y  /  2 )
 ) ) ) )   &    |-  G  =  ( y  e.  ( A (,) B )  |->  ( ( 2  x.  pi )  x.  ( sin `  (
 y  /  2 )
 ) ) )   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  Y  e.  RR )   &    |-  ( ph  ->  ( Y  mod  ( 2  x.  pi ) )  =  0 )   =>    |-  ( ph  ->  ( ( D `  N ) `  Y )  e.  ( ( D `  N ) lim CC  Y ) )
 
Theoremdirkercncflem4 38006* The Dirichlet Kernel is continuos at points that are not multiple of 2 π . This is the easier condition, for the proof of the continuity of the Dirichlet kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  D  =  ( n  e.  NN  |->  ( y  e.  RR  |->  if ( ( y  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  n )  +  1 )  /  (
 2  x.  pi ) ) ,  ( ( sin `  ( ( n  +  ( 1  /  2 ) )  x.  y ) ) 
 /  ( ( 2  x.  pi )  x.  ( sin `  (
 y  /  2 )
 ) ) ) ) ) )   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  Y  e.  RR )   &    |-  ( ph  ->  ( Y  mod  ( 2  x.  pi ) )  =/=  0 )   &    |-  A  =  ( |_ `  ( Y 
 /  ( 2  x.  pi ) ) )   &    |-  B  =  ( A  +  1 )   &    |-  C  =  ( A  x.  (
 2  x.  pi ) )   &    |-  E  =  ( B  x.  ( 2  x.  pi ) )   =>    |-  ( ph  ->  ( D `  N )  e.  (
 ( ( topGen `  ran  (,) )  CnP  ( topGen `  ran  (,) ) ) `  Y ) )
 
Theoremdirkercncf 38007* For any natural number  N, the Dirichlet Kernel  ( D `  N
) is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  D  =  ( n  e.  NN  |->  ( y  e.  RR  |->  if ( ( y  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  n )  +  1 )  /  (
 2  x.  pi ) ) ,  ( ( sin `  ( ( n  +  ( 1  /  2 ) )  x.  y ) ) 
 /  ( ( 2  x.  pi )  x.  ( sin `  (
 y  /  2 )
 ) ) ) ) ) )   =>    |-  ( N  e.  NN  ->  ( D `  N )  e.  ( RR -cn-> RR ) )
 
21.30.16  Fourier Series
 
Theoremfourierdlem1 38008 A partition interval is a subset of the partitioned interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR* )   &    |-  ( ph  ->  B  e.  RR* )   &    |-  ( ph  ->  Q : ( 0 ...
 M ) --> ( A [,] B ) )   &    |-  ( ph  ->  I  e.  ( 0..^ M ) )   &    |-  ( ph  ->  X  e.  ( ( Q `  I ) [,] ( Q `  ( I  +  1 ) ) ) )   =>    |-  ( ph  ->  X  e.  ( A [,] B ) )
 
Theoremfourierdlem2 38009* Membership in a 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 ) ) ) } )   =>    |-  ( M  e.  NN  ->  ( Q  e.  ( P `
  M )  <->  ( Q  e.  ( RR  ^m  ( 0
 ... M ) ) 
 /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
  i )  < 
 ( Q `  (
 i  +  1 ) ) ) ) ) )
 
Theoremfourierdlem3 38010* Membership in a partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  P  =  ( m  e.  NN  |->  { p  e.  ( (
 -u pi [,] pi )  ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  -u pi  /\  ( p `
  m )  =  pi )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   =>    |-  ( M  e.  NN  ->  ( Q  e.  ( P `
  M )  <->  ( Q  e.  ( ( -u pi [,] pi )  ^m  (
 0 ... M ) ) 
 /\  ( ( ( Q `  0 )  =  -u pi  /\  ( Q `  M )  =  pi )  /\  A. i  e.  ( 0..^ M ) ( Q `
  i )  < 
 ( Q `  (
 i  +  1 ) ) ) ) ) )
 
Theoremfourierdlem4 38011*  E is a function that maps any point to a periodic corresponding point in  ( A ,  B ]. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  T  =  ( B  -  A )   &    |-  E  =  ( x  e.  RR  |->  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) )   =>    |-  ( ph  ->  E : RR --> ( A (,] B ) )
 
Theoremfourierdlem5 38012*  S is a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  S  =  ( x  e.  ( -u pi [,] pi ) 
 |->  ( sin `  (
 ( X  +  (
 1  /  2 )
 )  x.  x ) ) )   =>    |-  ( X  e.  RR  ->  S : ( -u pi [,] pi ) --> RR )
 
Theoremfourierdlem6 38013  X is in the periodic partition, when the considered interval is centered at  X. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  T  =  ( B  -  A )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  I  e.  ZZ )   &    |-  ( ph  ->  J  e.  ZZ )   &    |-  ( ph  ->  I  <  J )   &    |-  ( ph  ->  ( X  +  ( I  x.  T ) )  e.  ( A [,] B ) )   &    |-  ( ph  ->  ( X  +  ( J  x.  T ) )  e.  ( A [,] B ) )   =>    |-  ( ph  ->  J  =  ( I  +  1 ) )
 
Theoremfourierdlem7 38014* The difference between a point and it's periodic image in the interval, is decreasing. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  T  =  ( B  -  A )   &    |-  E  =  ( x  e.  RR  |->  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  Y  e.  RR )   &    |-  ( ph  ->  X  <_  Y )   =>    |-  ( ph  ->  (
 ( E `  Y )  -  Y )  <_  ( ( E `  X )  -  X ) )
 
Theoremfourierdlem8 38015 A partition interval is a subset of the partitioned interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR* )   &    |-  ( ph  ->  B  e.  RR* )   &    |-  ( ph  ->  Q : ( 0 ...
 M ) --> ( A [,] B ) )   &    |-  ( ph  ->  I  e.  ( 0..^ M ) )   =>    |-  ( ph  ->  ( ( Q `  I ) [,] ( Q `  ( I  +  1 )
 ) )  C_  ( A [,] B ) )
 
Theoremfourierdlem9 38016*  H is a complex 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 ) ) )   =>    |-  ( ph  ->  H : ( -u pi [,] pi ) --> RR )
 
Theoremfourierdlem10 38017 Condition on the bounds of a non empty subinterval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  C  e.  RR )   &    |-  ( ph  ->  D  e.  RR )   &    |-  ( ph  ->  C  <  D )   &    |-  ( ph  ->  ( C (,) D ) 
 C_  ( A (,) B ) )   =>    |-  ( ph  ->  ( A  <_  C  /\  D  <_  B ) )
 
Theoremfourierdlem11 38018* If there is a partition, than the lower bound is strictly less than the upper bound. (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  ->  ( A  e.  RR  /\  B  e.  RR  /\  A  <  B ) )
 
Theoremfourierdlem12 38019* A point of a partition is not an element of any open interval determined by the 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 ) ) ) } )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  ( ph  ->  X  e.  ran  Q )   =>    |-  (
 ( ph  /\  i  e.  ( 0..^ M ) )  ->  -.  X  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
 
Theoremfourierdlem13 38020* Value of  V in terms of value of  Q. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  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 ) )   &    |-  Q  =  ( i  e.  ( 0 ... M )  |->  ( ( V `
  i )  -  X ) )   =>    |-  ( ph  ->  ( ( Q `  I
 )  =  ( ( V `  I )  -  X )  /\  ( V `  I )  =  ( X  +  ( Q `  I ) ) ) )
 
Theoremfourierdlem14 38021* Given the partition  V,  Q is the partition shifted to the left by  X. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  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 ) ) ) }
 )   &    |-  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  ->  M  e.  NN )   &    |-  ( ph  ->  V  e.  ( P `  M ) )   &    |-  Q  =  ( i  e.  ( 0
 ... M )  |->  ( ( V `  i
 )  -  X ) )   =>    |-  ( ph  ->  Q  e.  ( O `  M ) )
 
Theoremfourierdlem15 38022* The range of the partition is between its starting point and its ending point. (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  ->  Q : ( 0 ...
 M ) --> ( A [,] B ) )
 
Theoremfourierdlem16 38023* The coefficients of the fourier series are integrable and reals. (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 ) )   &    |-  ( ph  ->  N  e.  NN0 )   =>    |-  ( ph  ->  (
 ( ( A `  N )  e.  RR  /\  ( x  e.  C  |->  ( F `  x ) )  e.  L^1 )  /\  S. C ( ( F `  x )  x.  ( cos `  ( N  x.  x ) ) )  _d x  e.  RR ) )
 
Theoremfourierdlem17 38024* The defined  L is actually a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  L  =  ( x  e.  ( A (,] B )  |->  if ( x  =  B ,  A ,  x ) )   =>    |-  ( ph  ->  L : ( A (,] B ) --> ( A [,] B ) )
 
Theoremfourierdlem18 38025* The function  S is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  N  e.  RR )   &    |-  S  =  ( s  e.  ( -u pi [,] pi )  |->  ( sin `  ( ( N  +  ( 1  /  2
 ) )  x.  s
 ) ) )   =>    |-  ( ph  ->  S  e.  ( ( -u pi [,] pi ) -cn-> RR ) )
 
Theoremfourierdlem19 38026* If two elements of  D have the same periodic image in  ( A (,] B
) then they are equal. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  ( ph  ->  X  e.  RR )   &    |-  D  =  { y  e.  ( ( A  +  X ) (,] ( B  +  X )
 )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  C }   &    |-  T  =  ( B  -  A )   &    |-  E  =  ( x  e.  RR  |->  ( x  +  (
 ( |_ `  (
 ( B  -  x )  /  T ) )  x.  T ) ) )   &    |-  ( ph  ->  W  e.  D )   &    |-  ( ph  ->  Z  e.  D )   &    |-  ( ph  ->  ( E `  Z )  =  ( E `  W ) )   =>    |-  ( ph  ->  -.  W  <  Z )
 
Theoremfourierdlem20 38027* Every interval in the partition  S is included in an interval of the partition  Q. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <_  B )   &    |-  ( ph  ->  Q : ( 0 ...
 M ) --> RR )   &    |-  ( ph  ->  ( Q `  0 )  <_  A )   &    |-  ( ph  ->  B  <_  ( Q `  M ) )   &    |-  ( ph  ->  J  e.  ( 0..^ N ) )   &    |-  T  =  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )   &    |-  ( ph  ->  S  Isom  <  ,  <  ( ( 0
 ... N ) ,  T ) )   &    |-  I  =  sup ( { k  e.  ( 0..^ M )  |  ( Q `  k )  <_  ( S `
  J ) } ,  RR ,  <  )   =>    |-  ( ph  ->  E. i  e.  (
 0..^ M ) ( ( S `  J ) (,) ( S `  ( J  +  1
 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
 
Theoremfourierdlem21 38028* The coefficients of the fourier series are integrable and reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  C  =  (
 -u pi (,) pi )   &    |-  ( ph  ->  ( F  |`  C )  e.  L^1 )   &    |-  B  =  ( n  e.  NN  |->  ( S. C ( ( F `  x )  x.  ( sin `  ( n  x.  x ) ) )  _d x  /  pi ) )   &    |-  ( ph  ->  N  e.  NN )   =>    |-  ( ph  ->  ( ( ( B `  N )  e.  RR  /\  ( x  e.  C  |->  ( ( F `  x )  x.  ( sin `  ( N  x.  x ) ) ) )  e.  L^1 )  /\  S. C ( ( F `  x )  x.  ( sin `  ( N  x.  x ) ) )  _d x  e.  RR ) )
 
Theoremfourierdlem22 38029* The coefficients of the fourier series are integrable and reals. (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  ->  (
 ( n  e.  NN0  ->  ( A `  n )  e.  RR )  /\  ( n  e.  NN  ->  ( B `  n )  e.  RR )
 ) )
 
Theoremfourierdlem23 38030* If  F is continuous and  X is constant, then  ( F `  ( X  +  s
) ) is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  C_  CC )   &    |-  ( ph  ->  F  e.  ( A -cn-> CC )
 )   &    |-  ( ph  ->  B  C_ 
 CC )   &    |-  ( ph  ->  X  e.  CC )   &    |-  (
 ( ph  /\  s  e.  B )  ->  ( X  +  s )  e.  A )   =>    |-  ( ph  ->  (
 s  e.  B  |->  ( F `  ( X  +  s ) ) )  e.  ( B
 -cn-> CC ) )
 
Theoremfourierdlem24 38031 A sufficient condition for module being nonzero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( A  e.  ( ( -u pi [,] pi ) 
 \  { 0 } )  ->  ( A  mod  ( 2  x.  pi ) )  =/=  0
 )
 
Theoremfourierdlem25 38032* If  C is not in the range of the partition, then it is in an open interval induced by the partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q : ( 0 ...
 M ) --> RR )   &    |-  ( ph  ->  C  e.  (
 ( Q `  0
 ) [,] ( Q `  M ) ) )   &    |-  ( ph  ->  -.  C  e.  ran 
 Q )   &    |-  I  =  sup ( { k  e.  (
 0..^ M )  |  ( Q `  k
 )  <  C } ,  RR ,  <  )   =>    |-  ( ph  ->  E. j  e.  (
 0..^ M ) C  e.  ( ( Q `
  j ) (,) ( Q `  (
 j  +  1 ) ) ) )
 
Theoremfourierdlem26 38033* Periodic image of a point  Y that's in the period that begins with the point  X. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  T  =  ( B  -  A )   &    |-  E  =  ( x  e.  RR  |->  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  ( E `  X )  =  B )   &    |-  ( ph  ->  Y  e.  ( X (,] ( X  +  T )
 ) )   =>    |-  ( ph  ->  ( E `  Y )  =  ( A  +  ( Y  -  X ) ) )
 
Theoremfourierdlem27 38034 A partition open interval is a subset of the partitioned open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR* )   &    |-  ( ph  ->  B  e.  RR* )   &    |-  ( ph  ->  Q : ( 0 ...
 M ) --> ( A [,] B ) )   &    |-  ( ph  ->  I  e.  ( 0..^ M ) )   =>    |-  ( ph  ->  ( ( Q `  I ) (,) ( Q `  ( I  +  1 )
 ) )  C_  ( A (,) B ) )
 
Theoremfourierdlem28 38035* Derivative of  ( F `  ( X  +  s
) ). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  D  =  ( RR  _D  ( F  |`  ( ( X  +  A ) (,) ( X  +  B )
 ) ) )   &    |-  ( ph  ->  D : ( ( X  +  A ) (,) ( X  +  B ) ) --> RR )   =>    |-  ( ph  ->  ( RR  _D  ( s  e.  ( A (,) B )  |->  ( F `  ( X  +  s ) ) ) )  =  ( s  e.  ( A (,) B )  |->  ( D `  ( X  +  s ) ) ) )
 
Theoremfourierdlem29 38036* Explicit function value for  K applied to  A. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  K  =  ( s  e.  ( -u pi [,] pi ) 
 |->  if ( s  =  0 ,  1 ,  ( s  /  (
 2  x.  ( sin `  ( s  /  2
 ) ) ) ) ) )   =>    |-  ( A  e.  ( -u pi [,] pi ) 
 ->  ( K `  A )  =  if ( A  =  0 , 
 1 ,  ( A 
 /  ( 2  x.  ( sin `  ( A  /  2 ) ) ) ) ) )
 
Theoremfourierdlem30 38037* Sum of three small pieces is less than ε. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  ( x  e.  I  |->  ( F  x.  -u G ) )  e.  L^1 )   &    |-  (
 ( ph  /\  x  e.  I )  ->  F  e.  CC )   &    |-  ( ( ph  /\  x  e.  I ) 
 ->  G  e.  CC )   &    |-  ( ph  ->  A  e.  CC )   &    |-  X  =  ( abs `  A )   &    |-  ( ph  ->  C  e.  CC )   &    |-  Y  =  ( abs `  C )   &    |-  Z  =  ( abs `  S. I ( F  x.  -u G )  _d x )   &    |-  ( ph  ->  E  e.  RR+ )   &    |-  ( ph  ->  R  e.  RR )   &    |-  ( ph  ->  ( ( ( ( X  +  Y )  +  Z )  /  E )  +  1 )  <_  R )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  ( abs `  B )  <_ 
 1 )   &    |-  ( ph  ->  D  e.  CC )   &    |-  ( ph  ->  ( abs `  D )  <_  1 )   =>    |-  ( ph  ->  ( abs `  ( (
 ( A  x.  -u ( B  /  R ) )  -  ( C  x.  -u ( D  /  R ) ) )  -  S. I ( F  x.  -u ( G  /  R ) )  _d x ) )  <  E )
 
Theoremfourierdlem31 38038* If  A is finite and for any element in  A there is a number  m such that a property holds for all numbers larger than  m, then there is a number  n such that the property holds for all numbers larger than  n and for all elements in  A. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 29-Sep-2020.)
 |-  F/ i ph   &    |-  F/ r ph   &    |-  F/_ i V   &    |-  ( ph  ->  A  e.  Fin )   &    |-  ( ph  ->  A. i  e.  A  E. m  e.  NN  A. r  e.  ( m (,) +oo ) ch )   &    |-  M  =  { m  e.  NN  |  A. r  e.  ( m (,) +oo ) ch }   &    |-  V  =  ( i  e.  A  |-> inf ( M ,  RR ,  <  ) )   &    |-  N  =  sup ( ran  V ,  RR ,  <  )   =>    |-  ( ph  ->  E. n  e.  NN  A. r  e.  ( n (,) +oo ) A. i  e.  A  ch )
 
Theoremfourierdlem31OLD 38039* If  A is finite and for any element in  A there is a number  m such that a property holds for all numbers larger than  m, then there is a number  n such that the property holds for all numbers larger than  n and for all elements in  A. (Contributed by Glauco Siliprandi, 11-Dec-2019.) Obsolete version of fourierdlem31 38038 as of 29-Sep-2020. ( (New usage is discouraged.) (Proof modification is discouraged.)
 |-  F/ i ph   &    |-  F/ r ph   &    |-  F/_ i V   &    |-  ( ph  ->  A  e.  Fin )   &    |-  ( ph  ->  A. i  e.  A  E. m  e.  NN  A. r  e.  ( m (,) +oo ) ch )   &    |-  M  =  { m  e.  NN  |  A. r  e.  ( m (,) +oo ) ch }   &    |-  V  =  ( i  e.  A  |->  sup ( M ,  RR ,  `'  <  ) )   &    |-  N  =  sup ( ran  V ,  RR ,  <  )   =>    |-  ( ph  ->  E. n  e.  NN  A. r  e.  ( n (,) +oo ) A. i  e.  A  ch )
 
Theoremfourierdlem32 38040 Limit of a continuous function on an open subinterval. Lower bound version. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  ( ph  ->  F  e.  (
 ( A (,) B ) -cn-> CC ) )   &    |-  ( ph  ->  R  e.  ( F lim CC  A ) )   &    |-  ( ph  ->  C  e.  RR )   &    |-  ( ph  ->  D  e.  RR )   &    |-  ( ph  ->  C  <  D )   &    |-  ( ph  ->  ( C (,) D )  C_  ( A (,) B ) )   &    |-  Y  =  if ( C  =  A ,  R ,  ( F `
  C ) )   &    |-  J  =  ( ( TopOpen ` fld )t  ( A [,) B ) )   =>    |-  ( ph  ->  Y  e.  ( ( F  |`  ( C (,) D ) ) lim
 CC  C ) )
 
Theoremfourierdlem33 38041 Limit of a continuous function on an open subinterval. Upper bound version. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  ( ph  ->  F  e.  (
 ( A (,) B ) -cn-> CC ) )   &    |-  ( ph  ->  L  e.  ( F lim CC  B ) )   &    |-  ( ph  ->  C  e.  RR )   &    |-  ( ph  ->  D  e.  RR )   &    |-  ( ph  ->  C  <  D )   &    |-  ( ph  ->  ( C (,) D )  C_  ( A (,) B ) )   &    |-  Y  =  if ( D  =  B ,  L ,  ( F `
  D ) )   &    |-  J  =  ( ( TopOpen ` fld )t  ( ( A (,) B )  u.  { B }
 ) )   =>    |-  ( ph  ->  Y  e.  ( ( F  |`  ( C (,) D ) ) lim
 CC  D ) )
 
Theoremfourierdlem34 38042* A partition is one to one. (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  ->  Q : ( 0 ...
 M ) -1-1-> RR )
 
Theoremfourierdlem35 38043 There is a single point in  ( A (,] B
) that's distant from 
X a multiple integer of  T. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  T  =  ( B  -  A )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  I  e.  ZZ )   &    |-  ( ph  ->  J  e.  ZZ )   &    |-  ( ph  ->  ( X  +  ( I  x.  T ) )  e.  ( A (,] B ) )   &    |-  ( ph  ->  ( X  +  ( J  x.  T ) )  e.  ( A (,] B ) )   =>    |-  ( ph  ->  I  =  J )
 
Theoremfourierdlem36 38044*  F is an isomorphism. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  Fin )   &    |-  ( ph  ->  A  C_ 
 RR )   &    |-  F  =  (
 iota f f  Isom  <  ,  <  ( ( 0
 ... N ) ,  A ) )   &    |-  N  =  ( ( # `  A )  -  1 )   =>    |-  ( ph  ->  F 
 Isom  <  ,  <  (
 ( 0 ... N ) ,  A )
 )
 
Theoremfourierdlem37 38045*  I is a function that maps any real point to the point that in the partition that immediately precedes the corresponding periodic point in the interval. (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 ) )   &    |-  T  =  ( B  -  A )   &    |-  E  =  ( x  e.  RR  |->  ( x  +  ( ( |_ `  (
 ( B  -  x )  /  T ) )  x.  T ) ) )   &    |-  L  =  ( y  e.  ( A (,] B )  |->  if ( y  =  B ,  A ,  y ) )   &    |-  I  =  ( x  e.  RR  |->  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `
  ( E `  x ) ) } ,  RR ,  <  )
 )   =>    |-  ( ph  ->  ( I : RR --> ( 0..^ M )  /\  ( x  e.  RR  ->  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `
  ( E `  x ) ) } ,  RR ,  <  )  e.  { i  e.  (
 0..^ M )  |  ( Q `  i
 )  <_  ( L `  ( E `  x ) ) } )
 ) )
 
Theoremfourierdlem38 38046* The function  F is continuous on every interval induced by the partition  Q. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F  e.  ( dom  F -cn-> CC ) )   &    |-  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 ) )   &    |-  H  =  ( A  u.  ( (
 -u pi [,] pi )  \  dom  F ) )   &    |-  ( ph  ->  ran 
 Q  =  H )   =>    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i
 ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )
 
Theoremfourierdlem39 38047* Integration by parts of  S. ( A (,) B ) ( ( F `  x
)  x.  ( sin `  ( R  x.  x
) ) )  _d x (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A 
 <_  B )   &    |-  ( ph  ->  F  e.  ( ( A [,] B ) -cn-> CC ) )   &    |-  G  =  ( RR  _D  F )   &    |-  ( ph  ->  G  e.  ( ( A (,) B ) -cn-> CC ) )   &    |-  ( ph  ->  E. y  e.  RR  A. x  e.  ( A (,) B ) ( abs `  ( G `  x ) )  <_  y )   &    |-  ( ph  ->  R  e.  RR+ )   =>    |-  ( ph  ->  S. ( A (,) B ) ( ( F `  x )  x.  ( sin `  ( R  x.  x ) ) )  _d x  =  ( ( ( ( F `
  B )  x.  -u ( ( cos `  ( R  x.  B ) ) 
 /  R ) )  -  ( ( F `
  A )  x.  -u ( ( cos `  ( R  x.  A ) ) 
 /  R ) ) )  -  S. ( A (,) B ) ( ( G `  x )  x.  -u ( ( cos `  ( R  x.  x ) )  /  R ) )  _d x ) )
 
Theoremfourierdlem40 38048*  H is a continuous function on any partition interval. (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 ) ) )   =>    |-  ( ph  ->  ( H  |`  ( A (,) B ) )  e.  (
 ( A (,) B ) -cn-> CC ) )
 
Theoremfourierdlem41 38049* Lemma used to prove that every real is a limit point for the domain of the derivative of the periodic function to be approximated. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  T  =  ( B  -  A )   &    |-  ( ( ph  /\  x  e.  D  /\  k  e. 
 ZZ )  ->  ( x  +  ( k  x.  T ) )  e.  D )   &    |-  ( ph  ->  X  e.  RR )   &    |-  Z  =  ( x  e.  RR  |->  ( ( |_ `  (
 ( B  -  x )  /  T ) )  x.  T ) )   &    |-  E  =  ( x  e.  RR  |->  ( x  +  ( Z `  x ) ) )   &    |-  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  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) 
 C_  D )   =>    |-  ( ph  ->  ( E. y  e.  RR  ( y  <  X  /\  ( y (,) X )  C_  D )  /\  E. y  e.  RR  ( X  <  y  /\  ( X (,) y )  C_  D ) ) )
 
Theoremfourierdlem42 38050* The set of points in a moved partition are finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 29-Sep-2020.)
 |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  C  e.  RR )   &    |-  ( ph  ->  B  <  C )   &    |-  T  =  ( C  -  B )   &    |-  ( ph  ->  A  C_  ( B [,] C ) )   &    |-  ( ph  ->  A  e.  Fin )   &    |-  ( ph  ->  B  e.  A )   &    |-  ( ph  ->  C  e.  A )   &    |-  D  =  ( abs  o.  -  )   &    |-  I  =  ( ( A  X.  A )  \  _I  )   &    |-  R  =  ran  ( D  |`  I )   &    |-  E  = inf ( R ,  RR ,  <  )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  Y  e.  RR )   &    |-  J  =  (
 topGen `  ran  (,) )   &    |-  K  =  ( Jt  ( X [,] Y ) )   &    |-  H  =  { x  e.  ( X [,] Y )  |  E. k  e.  ZZ  ( x  +  ( k  x.  T ) )  e.  A }   &    |-  ( ps  <->  ( ( ph  /\  ( a  e.  RR  /\  b  e.  RR  /\  a  <  b ) ) 
 /\  E. j  e.  ZZ  E. k  e.  ZZ  (
 ( a  +  (
 j  x.  T ) )  e.  A  /\  ( b  +  (
 k  x.  T ) )  e.  A ) ) )   =>    |-  ( ph  ->  H  e.  Fin )
 
Theoremfourierdlem42OLD 38051* The set of points in a moved partition are finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.) Obsolete version of fourierdlem42 38050 as of 29-Sep-2020. ( (New usage is discouraged.) (Proof modification is discouraged.)
 |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  C  e.  RR )   &    |-  ( ph  ->  B  <  C )   &    |-  T  =  ( C  -  B )   &    |-  ( ph  ->  A  C_  ( B [,] C ) )   &    |-  ( ph  ->  A  e.  Fin )   &    |-  ( ph  ->  B  e.  A )   &    |-  ( ph  ->  C  e.  A )   &    |-  D  =  ( abs  o.  -  )   &    |-  I  =  ( ( A  X.  A )  \  _I  )   &    |-  R  =  ran  ( D  |`  I )   &    |-  E  =  sup ( R ,  RR ,  `'  <  )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  Y  e.  RR )   &    |-  J  =  ( topGen `  ran  (,) )   &    |-  K  =  ( Jt  ( X [,] Y ) )   &    |-  H  =  { x  e.  ( X [,] Y )  |  E. k  e.  ZZ  ( x  +  ( k  x.  T ) )  e.  A }   &    |-  ( ps  <->  ( ( ph  /\  ( a  e.  RR  /\  b  e.  RR  /\  a  <  b ) ) 
 /\  E. j  e.  ZZ  E. k  e.  ZZ  (
 ( a  +  (
 j  x.  T ) )  e.  A  /\  ( b  +  (
 k  x.  T ) )  e.  A ) ) )   =>    |-  ( ph  ->  H  e.  Fin )
 
Theoremfourierdlem43 38052  K is a real function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  K  =  ( s  e.  ( -u pi [,] pi ) 
 |->  if ( s  =  0 ,  1 ,  ( s  /  (
 2  x.  ( sin `  ( s  /  2
 ) ) ) ) ) )   =>    |-  K : ( -u pi [,] pi ) --> RR
 
Theoremfourierdlem44 38053 A condition for having  ( sin `  ( A  /  2 ) ) non zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  (
 ( A  e.  ( -u pi [,] pi ) 
 /\  A  =/=  0
 )  ->  ( sin `  ( A  /  2
 ) )  =/=  0
 )
 
Theoremfourierdlem46 38054* The function  F has a limit at the bounds of every interval induced by the partition  Q. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F  e.  ( dom  F -cn-> CC ) )   &    |-  (
 ( ph  /\  x  e.  ( ( -u pi [,) pi )  \  dom  F ) )  ->  (
 ( F  |`  ( x (,) +oo ) ) lim CC  x )  =/=  (/) )   &    |-  (
 ( ph  /\  x  e.  ( ( -u pi (,] pi )  \  dom  F ) )  ->  (
 ( F  |`  ( -oo (,) x ) ) lim CC  x )  =/=  (/) )   &    |-  ( ph  ->  Q  Isom  <  ,  <  ( ( 0
 ... M ) ,  H ) )   &    |-  ( ph  ->  Q : ( 0 ... M ) --> H )   &    |-  ( ph  ->  I  e.  ( 0..^ M ) )   &    |-  ( ph  ->  ( Q `  I )  <  ( Q `  ( I  +  1
 ) ) )   &    |-  ( ph  ->  ( ( Q `
  I ) (,) ( Q `  ( I  +  1 )
 ) )  C_  ( -u pi (,) pi ) )   &    |-  ( ph  ->  C  e.  RR )   &    |-  H  =  ( { -u pi ,  pi ,  C }  u.  ( ( -u pi [,] pi )  \  dom  F ) )   &    |-  ( ph  ->  ran 
 Q  =  H )   =>    |-  ( ph  ->  ( (
 ( F  |`  ( ( Q `  I ) (,) ( Q `  ( I  +  1
 ) ) ) ) lim
 CC  ( Q `  I ) )  =/=  (/)  /\  ( ( F  |`  ( ( Q `  I ) (,) ( Q `  ( I  +  1 ) ) ) ) lim CC  ( Q `
  ( I  +  1 ) ) )  =/=  (/) ) )
 
Theoremfourierdlem47 38055* For  r large enough, the final expression is less than the given positive  E. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  ( x  e.  I  |->  F )  e.  L^1 )   &    |-  (
 ( ph  /\  r  e. 
 RR )  ->  ( x  e.  I  |->  ( F  x.  -u G ) )  e.  L^1 )   &    |-  ( ( ph  /\  x  e.  I ) 
 ->  F  e.  CC )   &    |-  (
 ( ( ph  /\  x  e.  I )  /\  r  e.  CC )  ->  G  e.  CC )   &    |-  ( ( (
 ph  /\  x  e.  I )  /\  r  e. 
 RR )  ->  ( abs `  G )  <_ 
 1 )   &    |-  ( ph  ->  A  e.  CC )   &    |-  X  =  ( abs `  A )   &    |-  ( ph  ->  C  e.  CC )   &    |-  Y  =  ( abs `  C )   &    |-  Z  =  S. I ( abs `  F )  _d x   &    |-  ( ph  ->  E  e.  RR+ )   &    |-  ( ( ph  /\  r  e.  CC )  ->  B  e.  CC )   &    |-  ( ( ph  /\  r  e.  RR )  ->  ( abs `  B )  <_  1 )   &    |-  (
 ( ph  /\  r  e. 
 CC )  ->  D  e.  CC )   &    |-  ( ( ph  /\  r  e.  RR )  ->  ( abs `  D )  <_  1 )   &    |-  M  =  ( ( |_ `  (
 ( ( ( X  +  Y )  +  Z )  /  E )  +  1 ) )  +  1 )   =>    |-  ( ph  ->  E. m  e.  NN  A. r  e.  ( m (,) +oo ) ( abs `  ( ( ( A  x.  -u ( B  /  r ) )  -  ( C  x.  -u ( D  /  r ) ) )  -  S. I
 ( F  x.  -u ( G  /  r ) )  _d x ) )  <  E )
 
Theoremfourierdlem48 38056* The given periodic function  F has a right limit at every point in the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  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 : D --> RR )   &    |-  ( ( ph  /\  x  e.  D  /\  k  e.  ZZ )  ->  ( x  +  (
 k  x.  T ) )  e.  D )   &    |-  ( ( ph  /\  x  e.  D  /\  k  e. 
 ZZ )  ->  ( F `  ( x  +  ( k  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  ->  X  e.  RR )   &    |-  Z  =  ( x  e.  RR  |->  ( ( |_ `  (
 ( B  -  x )  /  T ) )  x.  T ) )   &    |-  E  =  ( x  e.  RR  |->  ( x  +  ( Z `  x ) ) )   &    |-  ( ch  <->  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  y  e.  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) ) )  /\  k  e. 
 ZZ )  /\  y  =  ( X  +  (
 k  x.  T ) ) ) )   =>    |-  ( ph  ->  ( ( F  |`  ( X (,) +oo ) ) lim CC  X )  =/=  (/) )
 
Theoremfourierdlem49 38057* The given periodic function  F has a left limit at every point in the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  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  ->  D  C_  RR )   &    |-  ( ph  ->  F : D --> RR )   &    |-  (
 ( ph  /\  x  e.  D  /\  k  e. 
 ZZ )  ->  ( x  +  ( k  x.  T ) )  e.  D )   &    |-  ( ( ph  /\  x  e.  D  /\  k  e.  ZZ )  ->  ( F `  ( x  +  ( k  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  ->  X  e.  RR )   &    |-  Z  =  ( x  e.  RR  |->  ( ( |_ `  (
 ( B  -  x )  /  T ) )  x.  T ) )   &    |-  E  =  ( x  e.  RR  |->  ( x  +  ( Z `  x ) ) )   =>    |-  ( ph  ->  (
 ( F  |`  ( -oo (,)
 X ) ) lim CC  X )  =/=  (/) )
 
Theoremfourierdlem50 38058* Continuity of  O and its limits with respect to the  S partition. (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  ->  M  e.  NN )   &    |-  ( ph  ->  V  e.  ( P `  M ) )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  ( ph  ->  ( A [,] B )  C_  ( -u pi [,] pi ) )   &    |-  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 )
 )   &    |-  ( ph  ->  J  e.  ( 0..^ N ) )   &    |-  U  =  (
 iota_ i  e.  (
 0..^ M ) ( ( S `  J ) (,) ( S `  ( J  +  1
 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )   &    |-  ( ch  <->  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  J ) (,) ( S `  ( J  +  1
 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  /\  k  e.  ( 0..^ M ) )  /\  ( ( S `  J ) (,) ( S `  ( J  +  1
 ) ) )  C_  ( ( Q `  k ) (,) ( Q `  ( k  +  1 ) ) ) ) )   =>    |-  ( ph  ->  ( U  e.  ( 0..^ M )  /\  ( ( S `  J ) (,) ( S `  ( J  +  1
 ) ) )  C_  ( ( Q `  U ) (,) ( Q `  ( U  +  1 ) ) ) ) )
 
Theoremfourierdlem51 38059*  X is in the periodic partition, when the considered interval is centered at  X. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <  0 )   &    |-  ( ph  ->  0  <  B )   &    |-  T  =  ( B  -  A )   &    |-  ( ph  ->  C  e.  Fin )   &    |-  ( ph  ->  C  C_  ( A [,] B ) )   &    |-  ( ph  ->  B  e.  C )   &    |-  E  =  ( x  e.  RR  |->  ( x  +  (
 ( |_ `  (
 ( B  -  x )  /  T ) )  x.  T ) ) )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  ( E `  X )  e.  C )   &    |-  D  =  ( {
 ( A  +  X ) ,  ( B  +  X ) }  u.  { y  e.  ( ( A  +  X ) [,] ( B  +  X ) )  | 
 E. k  e.  ZZ  ( y  +  (
 k  x.  T ) )  e.  C }
 )   &    |-  F  =  ( iota
 f f  Isom  <  ,  <  ( ( 0
 ... ( ( # `  D )  -  1
 ) ) ,  D ) )   &    |-  H  =  {
 y  e.  ( ( A  +  X ) (,] ( B  +  X ) )  | 
 E. k  e.  ZZ  ( y  +  (
 k  x.  T ) )  e.  C }   =>    |-  ( ph  ->  X  e.  ran  F )
 
Theoremfourierdlem52 38060* d16:d17,d18:jca |- ( ph -> ( ( S  0 )  <_  A  /\  A  <_  ( S 0 ) ) ) . (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  T  e.  Fin )   &    |-  N  =  ( ( # `  T )  -  1 )   &    |-  S  =  (
 iota f f  Isom  <  ,  <  ( ( 0
 ... N ) ,  T ) )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  T 
 C_  ( A [,] B ) )   &    |-  ( ph  ->  A  e.  T )   &    |-  ( ph  ->  B  e.  T )   =>    |-  ( ph  ->  (
 ( S : ( 0 ... N ) --> ( A [,] B )  /\  ( S `  0 )  =  A )  /\  ( S `  N )  =  B ) )
 
Theoremfourierdlem53 38061* The limit of  F ( s ) at  ( X  +  D ) is the limit of  F ( X  +  s ) at  D. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  A  C_  RR )   &    |-  G  =  ( s  e.  A  |->  ( F `
  ( X  +  s ) ) )   &    |-  ( ( ph  /\  s  e.  A )  ->  ( X  +  s )  e.  B )   &    |-  ( ph  ->  B 
 C_  RR )   &    |-  ( ( ph  /\  s  e.  A ) 
 ->  s  =/=  D )   &    |-  ( ph  ->  C  e.  ( ( F  |`  B ) lim
 CC  ( X  +  D ) ) )   &    |-  ( ph  ->  D  e.  CC )   =>    |-  ( ph  ->  C  e.  ( G lim CC  D ) )
 
Theoremfourierdlem54 38062* Given a partition  Q and an arbitrary interval  [ C ,  D ], a partition  S on  [ C ,  D ] is built such that it preserves any periodic function piecewise continuous on  Q will be piecewise continuous on  S, with the same limits. (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 )
 )   =>    |-  ( ph  ->  (
 ( N  e.  NN  /\  S  e.  ( O `
  N ) ) 
 /\  S  Isom  <  ,  <  ( ( 0
 ... N ) ,  H ) ) )
 
Theoremfourierdlem55 38063*  U is a real 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  ->  U : ( -u pi [,] pi ) --> RR )
 
Theoremfourierdlem56 38064* Derivative of the  K function on an interval non containing ' 0 '. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  K  =  ( s  e.  ( -u pi [,] pi ) 
 |->  if ( s  =  0 ,  1 ,  ( s  /  (
 2  x.  ( sin `  ( s  /  2
 ) ) ) ) ) )   &    |-  ( ph  ->  ( A (,) B ) 
 C_  ( ( -u pi [,] pi )  \  { 0 } )
 )   &    |-  ( ( ph  /\  s  e.  ( A (,) B ) )  ->  s  =/=  0 )   =>    |-  ( ph  ->  ( RR  _D  ( s  e.  ( A (,) B )  |->  ( K `  s ) ) )  =  ( s  e.  ( A (,) B )  |->  ( ( ( ( sin `  (
 s  /  2 )
 )  -  ( ( ( cos `  (
 s  /  2 )
 )  /  2 )  x.  s ) )  /  ( ( sin `  (
 s  /  2 )
 ) ^ 2 ) )  /  2 ) ) )
 
Theoremfourierdlem57 38065* The derivative of  O. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  ( RR  _D  ( F  |`  ( ( X  +  A ) (,) ( X  +  B )
 ) ) ) : ( ( X  +  A ) (,) ( X  +  B )
 ) --> 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 )
 ) ) ) )   =>    |-  ( ( ph  ->  ( ( RR  _D  O ) : ( A (,) B ) --> RR  /\  ( RR 
 _D  O )  =  ( s  e.  ( A (,) B )  |->  ( ( ( ( ( RR  _D  ( F  |`  ( ( X  +  A ) (,) ( X  +  B )
 ) ) ) `  ( X  +  s
 ) )  x.  (
 2  x.  ( sin `  ( s  /  2
 ) ) ) )  -  ( ( cos `  ( s  /  2
 ) )  x.  (
 ( F `  ( X  +  s )
 )  -  C ) ) )  /  (
 ( 2  x.  ( sin `  ( s  / 
 2 ) ) ) ^ 2 ) ) ) ) )  /\  ( RR  _D  (
 s  e.  ( A (,) B )  |->  ( 2  x.  ( sin `  ( s  /  2
 ) ) ) ) )  =  ( s  e.  ( A (,) B )  |->  ( cos `  (
 s  /  2 )
 ) ) )
 
Theoremfourierdlem58 38066* The derivative of  K is continuous on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  K  =  ( s  e.  A  |->  ( s  /  (
 2  x.  ( sin `  ( s  /  2
 ) ) ) ) )   &    |-  ( ph  ->  A 
 C_  ( -u pi [,] pi ) )   &    |-  ( ph  ->  -.  0  e.  A )   &    |-  ( ph  ->  A  e.  ( topGen `  ran  (,) ) )   =>    |-  ( ph  ->  ( RR  _D  K )  e.  ( A -cn-> RR )
 )
 
Theoremfourierdlem59 38067* The derivative of  H is continuous 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  ->  -.  0  e.  ( A (,) B ) )   &    |-  ( ph  ->  ( RR  _D  ( F  |`  ( ( X  +  A ) (,) ( X  +  B ) ) ) )  e.  ( ( ( X  +  A ) (,) ( X  +  B ) ) -cn-> RR ) )   &    |-  ( ph  ->  C  e.  RR )   &    |-  H  =  ( s  e.  ( A (,) B )  |->  ( ( ( F `  ( X  +  s
 ) )  -  C )  /  s ) )   =>    |-  ( ph  ->  ( RR  _D  H )  e.  (
 ( A (,) B ) -cn-> RR ) )
 
Theoremfourierdlem60 38068* Given a differentiable function  F, with finite limit of the derivative at  A the derived function  H has a limit at  0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  ( ph  ->  F : ( A (,) B ) --> RR )   &    |-  ( ph  ->  Y  e.  ( F lim CC  B ) )   &    |-  G  =  ( RR  _D  F )   &    |-  ( ph  ->  dom  G  =  ( A (,) B ) )   &    |-  ( ph  ->  E  e.  ( G lim CC  B ) )   &    |-  H  =  ( s  e.  (
 ( A  -  B ) (,) 0 )  |->  ( ( ( F `  ( B  +  s
 ) )  -  Y )  /  s ) )   &    |-  N  =  ( s  e.  ( ( A  -  B ) (,) 0
 )  |->  ( ( F `
  ( B  +  s ) )  -  Y ) )   &    |-  D  =  ( s  e.  (
 ( A  -  B ) (,) 0 )  |->  s )   =>    |-  ( ph  ->  E  e.  ( H lim CC  0
 ) )
 
Theoremfourierdlem61 38069* Given a differentiable function  F, with finite limit of the derivative at  A the derived function  H has a limit at  0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  ( ph  ->  F : ( A (,) B ) --> RR )   &    |-  ( ph  ->  Y  e.  ( F lim CC  A ) )   &    |-  G  =  ( RR  _D  F )   &    |-  ( ph  ->  dom  G  =  ( A (,) B ) )   &    |-  ( ph  ->  E  e.  ( G lim CC  A ) )   &    |-  H  =  ( s  e.  (
 0 (,) ( B  -  A ) )  |->  ( ( ( F `  ( A  +  s
 ) )  -  Y )  /  s ) )   &    |-  N  =  ( s  e.  ( 0 (,) ( B  -  A ) ) 
 |->  ( ( F `  ( A  +  s
 ) )  -  Y ) )   &    |-  D  =  ( s  e.  ( 0 (,) ( B  -  A ) )  |->  s )   =>    |-  ( ph  ->  E  e.  ( H lim CC  0
 ) )
 
Theoremfourierdlem62 38070 The function  K is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  K  =  ( y  e.  ( -u pi [,] pi ) 
 |->  if ( y  =  0 ,  1 ,  ( y  /  (
 2  x.  ( sin `  ( y  /  2
 ) ) ) ) ) )   =>    |-  K  e.  ( (
 -u pi [,] pi ) -cn-> RR )
 
Theoremfourierdlem63 38071* 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 ) )
 
Theoremfourierdlem64 38072* 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 ) ) ) ) )
 
Theoremfourierdlem65 38073* 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 ) ) )
 
Theoremfourierdlem66 38074* 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
 ) ) ) )
 
Theoremfourierdlem67 38075*  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 )
 
Theoremfourierdlem68 38076* 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
 ) )
 
Theoremfourierdlem69 38077* 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 )
 
Theoremfourierdlem70 38078* 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 )
 
Theoremfourierdlem71 38079* 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 )
 
Theoremfourierdlem72 38080* 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 ) )
 
Theoremfourierdlem73 38081* 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 )
 
Theoremfourierdlem74 38082* 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
 ) ) ) )
 
Theoremfourierdlem75 38083* 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 )   &    |-