HomeHome Metamath Proof Explorer
Theorem List (p. 380 of 402)
< 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-26569)
  Hilbert Space Explorer  Hilbert Space Explorer
(26570-28092)
  Users' Mathboxes  Users' Mathboxes
(28093-40161)
 

Theorem List for Metamath Proof Explorer - 37901-38000   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremdirkertrigeqlem2 37901* Trigonomic equality lemma for the Dirichlet Kernel trigonomic equality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  ( sin `  A )  =/=  0 )   &    |-  ( ph  ->  N  e.  NN )   =>    |-  ( ph  ->  ( ( ( 1  / 
 2 )  +  sum_ n  e.  ( 1 ...
 N ) ( cos `  ( n  x.  A ) ) )  /  pi )  =  (
 ( sin `  ( ( N  +  ( 1  /  2 ) )  x.  A ) ) 
 /  ( ( 2  x.  pi )  x.  ( sin `  ( A  /  2 ) ) ) ) )
 
Theoremdirkertrigeqlem3 37902* Trigonometric equality lemma for the Dirichlet Kernel trigonometric equality. Here we handle the case for an angle that's an odd multiple of  pi. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  K  e.  ZZ )   &    |-  A  =  ( ( ( 2  x.  K )  +  1 )  x.  pi )   =>    |-  ( ph  ->  ( (
 ( 1  /  2
 )  +  sum_ n  e.  ( 1 ... N ) ( cos `  ( n  x.  A ) ) )  /  pi )  =  ( ( sin `  ( ( N  +  ( 1  /  2
 ) )  x.  A ) )  /  (
 ( 2  x.  pi )  x.  ( sin `  ( A  /  2 ) ) ) ) )
 
Theoremdirkertrigeq 37903* 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 37904* 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 37905* 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 37906* 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 37907* 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 37908* 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 37909* 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 37910 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 37911* 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 37912* 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 37913*  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 37914*  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 37915  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 37916* 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 37917 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 37918*  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 37919 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 37920* 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 37921* 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 37922* 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 37923* 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 37924* 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 37925* 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 37926* 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 37927* 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 37928* 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 37929* 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 37930* 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 37931* 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 37932* 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 37933 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 37934* 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 37935* 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 37936 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 37937* 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 37938* 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 37939* 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 37940* 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 37941* 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 37940 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 37942 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 37943 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 37944* 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 37945 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 37946*  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 37947*  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 37948* 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 37949* 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 37950*  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 37951* 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 37952* 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 37953* The set of points in a moved partition are finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.) Obsolete version of fourierdlem42 37952 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 37954  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 37955 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 37956* 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 37957* 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 37958* 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 37959* 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 37960* 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 37961*  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 37962* 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 37963* 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 37964* 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 37965*  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 37966* 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 37967* 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 37968* 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 37969* 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 37970* 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 37971* 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 37972 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 37973* 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 37974* 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 37975* 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 37976* 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 37977*  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 37978* 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 37979* 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 37980* 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 37981* 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 37982* 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 37983* 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 37984* 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