HomeHome Metamath Proof Explorer
Theorem List (p. 377 of 394)
< 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-26406)
  Hilbert Space Explorer  Hilbert Space Explorer
(26407-27929)
  Users' Mathboxes  Users' Mathboxes
(27930-39301)
 

Theorem List for Metamath Proof Explorer - 37601-37700   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremfourierdlem63 37601* The upper bound of intervals in the moved partition are mapped to points that are not greater than the corresponding upper bounds in the original partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  T  =  ( B  -  A )   &    |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  (
 0 ... m ) )  |  ( ( ( p `  0 )  =  A  /\  ( p `  m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  ( ph  ->  C  e.  RR )   &    |-  ( ph  ->  D  e.  RR )   &    |-  ( ph  ->  C  <  D )   &    |-  O  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  C  /\  ( p `
  m )  =  D )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  H  =  ( { C ,  D }  u.  { x  e.  ( C [,] D )  |  E. k  e.  ZZ  ( x  +  ( k  x.  T ) )  e.  ran  Q } )   &    |-  N  =  ( ( # `  H )  -  1 )   &    |-  S  =  ( iota f f 
 Isom  <  ,  <  (
 ( 0 ... N ) ,  H )
 )   &    |-  E  =  ( x  e.  RR  |->  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) )   &    |-  ( ph  ->  K  e.  ( 0 ...
 M ) )   &    |-  ( ph  ->  J  e.  (
 0..^ N ) )   &    |-  ( ph  ->  Y  e.  ( ( S `  J ) [,) ( S `  ( J  +  1 ) ) ) )   &    |-  ( ph  ->  ( E `  Y )  <  ( Q `  K ) )   &    |-  X  =  ( ( Q `  K )  -  (
 ( E `  Y )  -  Y ) )   =>    |-  ( ph  ->  ( E `  ( S `  ( J  +  1 )
 ) )  <_  ( Q `  K ) )
 
Theoremfourierdlem64 37602* The partition  V is finer than  Q, when  Q is moved on the same interval where  V lies. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  T  =  ( B  -  A )   &    |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  (
 0 ... m ) )  |  ( ( ( p `  0 )  =  A  /\  ( p `  m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  ( ph  ->  C  e.  RR )   &    |-  ( ph  ->  D  e.  RR )   &    |-  ( ph  ->  C  <  D )   &    |-  H  =  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  ran  Q } )   &    |-  N  =  ( ( # `  H )  -  1 )   &    |-  V  =  ( iota f f 
 Isom  <  ,  <  (
 ( 0 ... N ) ,  H )
 )   &    |-  ( ph  ->  J  e.  ( 0..^ N ) )   &    |-  L  =  sup ( { k  e.  ZZ  |  ( ( Q `  0 )  +  (
 k  x.  T ) )  <_  ( V `  J ) } ,  RR ,  <  )   &    |-  I  =  sup ( { j  e.  ( 0..^ M )  |  ( ( Q `
  j )  +  ( L  x.  T ) )  <_  ( V `
  J ) } ,  RR ,  <  )   =>    |-  ( ph  ->  ( ( I  e.  ( 0..^ M )  /\  L  e.  ZZ )  /\  E. i  e.  ( 0..^ M ) E. l  e.  ZZ  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) 
 C_  ( ( ( Q `  i )  +  ( l  x.  T ) ) (,) ( ( Q `  ( i  +  1
 ) )  +  (
 l  x.  T ) ) ) ) )
 
Theoremfourierdlem65 37603* The distance of two adjacent points in the moved partition is preserved in the original partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  A  /\  ( p `
  m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  T  =  ( B  -  A )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  ( ph  ->  C  e.  RR )   &    |-  ( ph  ->  D  e.  ( C (,) +oo ) )   &    |-  O  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  C  /\  ( p `
  m )  =  D )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  N  =  ( ( # `  ( { C ,  D }  u.  { y  e.  ( C [,] D )  | 
 E. k  e.  ZZ  ( y  +  (
 k  x.  ( B  -  A ) ) )  e.  ran  Q } ) )  -  1 )   &    |-  S  =  (
 iota f f  Isom  <  ,  <  ( ( 0
 ... N ) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A ) ) )  e.  ran  Q } ) ) )   &    |-  E  =  ( x  e.  RR  |->  ( x  +  ( ( |_ `  (
 ( B  -  x )  /  T ) )  x.  T ) ) )   &    |-  L  =  ( y  e.  ( A (,] B )  |->  if ( y  =  B ,  A ,  y ) )   &    |-  Z  =  ( ( S `  j
 )  +  ( B  -  ( E `  ( S `  j ) ) ) )   =>    |-  ( ( ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( E `  ( S `  ( j  +  1 ) ) )  -  ( L `
  ( E `  ( S `  j ) ) ) )  =  ( ( S `  ( j  +  1
 ) )  -  ( S `  j ) ) )
 
Theoremfourierdlem66 37604* Value of the  G function when the argument is not zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  Y  e.  RR )   &    |-  ( ph  ->  W  e.  RR )   &    |-  D  =  ( n  e.  NN  |->  ( s  e.  RR  |->  if ( ( s  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  n )  +  1 )  /  (
 2  x.  pi ) ) ,  ( ( sin `  ( ( n  +  ( 1  /  2 ) )  x.  s ) ) 
 /  ( ( 2  x.  pi )  x.  ( sin `  (
 s  /  2 )
 ) ) ) ) ) )   &    |-  H  =  ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  (
 ( ( F `  ( X  +  s
 ) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) )   &    |-  K  =  ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  1 ,  (
 s  /  ( 2  x.  ( sin `  (
 s  /  2 )
 ) ) ) ) )   &    |-  U  =  ( s  e.  ( -u pi [,] pi )  |->  ( ( H `  s
 )  x.  ( K `
  s ) ) )   &    |-  S  =  ( s  e.  ( -u pi [,] pi )  |->  ( sin `  ( ( n  +  ( 1  /  2 ) )  x.  s ) ) )   &    |-  G  =  ( s  e.  ( -u pi [,] pi )  |->  ( ( U `  s
 )  x.  ( S `
  s ) ) )   &    |-  A  =  ( ( -u pi [,] pi )  \  { 0 } )   =>    |-  ( ( ( ph  /\  n  e.  NN )  /\  s  e.  A )  ->  ( G `  s )  =  ( pi  x.  ( ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  x.  ( ( D `  n ) `  s
 ) ) ) )
 
Theoremfourierdlem67 37605*  G is a function (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  Y  e.  RR )   &    |-  ( ph  ->  W  e.  RR )   &    |-  H  =  ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  (
 ( ( F `  ( X  +  s
 ) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) )   &    |-  K  =  ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  1 ,  (
 s  /  ( 2  x.  ( sin `  (
 s  /  2 )
 ) ) ) ) )   &    |-  U  =  ( s  e.  ( -u pi [,] pi )  |->  ( ( H `  s
 )  x.  ( K `
  s ) ) )   &    |-  ( ph  ->  N  e.  RR )   &    |-  S  =  ( s  e.  ( -u pi [,] pi ) 
 |->  ( sin `  (
 ( N  +  (
 1  /  2 )
 )  x.  s ) ) )   &    |-  G  =  ( s  e.  ( -u pi [,] pi )  |->  ( ( U `  s
 )  x.  ( S `
  s ) ) )   =>    |-  ( ph  ->  G : ( -u pi [,] pi ) --> RR )
 
Theoremfourierdlem68 37606* The derivative of  O is bounded on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  ( ph  ->  ( A [,] B )  C_  ( -u pi [,] pi ) )   &    |-  ( ph  ->  -.  0  e.  ( A [,] B ) )   &    |-  ( ph  ->  ( RR  _D  ( F  |`  ( ( X  +  A ) (,) ( X  +  B )
 ) ) ) : ( ( X  +  A ) (,) ( X  +  B )
 ) --> RR )   &    |-  ( ph  ->  D  e.  RR )   &    |-  ( ( ph  /\  t  e.  ( ( X  +  A ) (,) ( X  +  B )
 ) )  ->  ( abs `  ( F `  t ) )  <_  D )   &    |-  ( ph  ->  E  e.  RR )   &    |-  (
 ( ph  /\  t  e.  ( ( X  +  A ) (,) ( X  +  B )
 ) )  ->  ( abs `  ( ( RR 
 _D  ( F  |`  ( ( X  +  A ) (,) ( X  +  B ) ) ) ) `  t ) )  <_  E )   &    |-  ( ph  ->  C  e.  RR )   &    |-  O  =  ( s  e.  ( A (,) B )  |->  ( ( ( F `  ( X  +  s ) )  -  C )  /  ( 2  x.  ( sin `  ( s  / 
 2 ) ) ) ) )   =>    |-  ( ph  ->  ( dom  ( RR  _D  O )  =  ( A (,) B )  /\  E. b  e.  RR  A. s  e.  dom  ( RR  _D  O ) ( abs `  ( ( RR  _D  O ) `  s
 ) )  <_  b
 ) )
 
Theoremfourierdlem69 37607* A piecewise continuous function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  A  /\  ( p `
  m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  ( ph  ->  F : ( A [,] B ) --> CC )   &    |-  (
 ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i
 ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )   =>    |-  ( ph  ->  F  e.  L^1 )
 
Theoremfourierdlem70 37608* A piecewise continuous function is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A 
 <_  B )   &    |-  ( ph  ->  F : ( A [,] B ) --> RR )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q : ( 0 ...
 M ) --> RR )   &    |-  ( ph  ->  ( Q `  0 )  =  A )   &    |-  ( ph  ->  ( Q `  M )  =  B )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1
 ) ) )   &    |-  (
 ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i
 ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )   &    |-  I  =  ( i  e.  ( 0..^ M )  |->  ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) )   =>    |-  ( ph  ->  E. x  e.  RR  A. s  e.  ( A [,] B ) ( abs `  ( F `  s ) ) 
 <_  x )
 
Theoremfourierdlem71 37609* A periodic piecewise continuous function, possibly undefined on a finite set in each periodic interval, is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  dom  F  C_  RR )   &    |-  ( ph  ->  F : dom  F --> RR )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  T  =  ( B  -  A )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q : ( 0 ...
 M ) --> RR )   &    |-  ( ph  ->  ( Q `  0 )  =  A )   &    |-  ( ph  ->  ( Q `  M )  =  B )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )   &    |-  ( ( (
 ph  /\  x  e.  dom 
 F )  /\  k  e.  ZZ )  ->  ( x  +  ( k  x.  T ) )  e. 
 dom  F )   &    |-  ( ( (
 ph  /\  x  e.  dom 
 F )  /\  k  e.  ZZ )  ->  ( F `  ( x  +  ( k  x.  T ) ) )  =  ( F `  x ) )   &    |-  I  =  ( i  e.  ( 0..^ M )  |->  ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) )   &    |-  E  =  ( x  e.  RR  |->  ( x  +  ( ( |_ `  (
 ( B  -  x )  /  T ) )  x.  T ) ) )   =>    |-  ( ph  ->  E. y  e.  RR  A. x  e. 
 dom  F ( abs `  ( F `  x ) ) 
 <_  y )
 
Theoremfourierdlem72 37610* The derivative of  O is continuous on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  ( ph  ->  X  e.  RR )   &    |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  ( -u pi  +  X )  /\  ( p `  m )  =  ( pi  +  X ) ) 
 /\  A. i  e.  (
 0..^ m ) ( p `  i )  <  ( p `  ( i  +  1
 ) ) ) }
 )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  V  e.  ( P `  M ) )   &    |-  (
 ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( RR  _D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  e.  ( ( ( V `  i
 ) (,) ( V `  ( i  +  1
 ) ) ) -cn-> RR ) )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  ( ph  ->  ( A (,) B ) 
 C_  ( -u pi [,] pi ) )   &    |-  ( ph  ->  -.  0  e.  ( A [,] B ) )   &    |-  ( ph  ->  C  e.  RR )   &    |-  Q  =  ( i  e.  (
 0 ... M )  |->  ( ( V `  i
 )  -  X ) )   &    |-  ( ph  ->  U  e.  ( 0..^ M ) )   &    |-  ( ph  ->  ( A (,) B ) 
 C_  ( ( Q `
  U ) (,) ( Q `  ( U  +  1 )
 ) ) )   &    |-  H  =  ( s  e.  ( A (,) B )  |->  ( ( ( F `  ( X  +  s
 ) )  -  C )  /  s ) )   &    |-  K  =  ( s  e.  ( A (,) B )  |->  ( s  /  ( 2  x.  ( sin `  ( s  / 
 2 ) ) ) ) )   &    |-  O  =  ( s  e.  ( A (,) B )  |->  ( ( H `  s
 )  x.  ( K `
  s ) ) )   =>    |-  ( ph  ->  ( RR  _D  O )  e.  ( ( A (,) B ) -cn-> CC ) )
 
Theoremfourierdlem73 37611* A version of the Riemann Lebesgue lemma: as  r increases, the integral in  S goes to zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  F : ( A [,] B ) --> CC )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q : ( 0 ...
 M ) --> ( A [,] B ) )   &    |-  ( ph  ->  ( Q `  0 )  =  A )   &    |-  ( ph  ->  ( Q `  M )  =  B )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1
 ) ) )   &    |-  (
 ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i
 ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )   &    |-  G  =  ( RR  _D  F )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i
 ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ph  ->  E. y  e.  RR  A. x  e.  dom  G ( abs `  ( G `  x ) )  <_  y )   &    |-  S  =  ( r  e.  RR+  |->  S. ( A (,) B ) ( ( F `  x )  x.  ( sin `  (
 r  x.  x ) ) )  _d x )   &    |-  D  =  ( x  e.  ( ( Q `
  i ) [,] ( Q `  (
 i  +  1 ) ) )  |->  if ( x  =  ( Q `  i ) ,  R ,  if ( x  =  ( Q `  (
 i  +  1 ) ) ,  L ,  ( F `  x ) ) ) )   =>    |-  ( ph  ->  A. e  e.  RR+  E. n  e.  NN  A. r  e.  ( n (,) +oo ) ( abs `  S. ( A (,) B ) ( ( F `  x )  x.  ( sin `  ( r  x.  x ) ) )  _d x )  < 
 e )
 
Theoremfourierdlem74 37612* Given a piecewise smooth function 
F, the derived function 
H has a limit at the upper bound of each interval of the partition  Q. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  X  e.  RR )   &    |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  (
 0 ... m ) )  |  ( ( ( p `  0 )  =  ( -u pi  +  X )  /\  ( p `  m )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ m ) ( p `  i
 )  <  ( p `  ( i  +  1 ) ) ) }
 )   &    |-  ( ph  ->  F : RR --> RR )   &    |-  ( ph  ->  X  e.  ran  V )   &    |-  ( ph  ->  Y  e.  RR )   &    |-  ( ph  ->  W  e.  (
 ( F  |`  ( -oo (,)
 X ) ) lim CC  X ) )   &    |-  H  =  ( s  e.  ( -u pi [,] pi ) 
 |->  if ( s  =  0 ,  0 ,  ( ( ( F `
  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  V  e.  ( P `  M ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1
 ) ) ) ) lim
 CC  ( V `  ( i  +  1
 ) ) ) )   &    |-  Q  =  ( i  e.  ( 0 ... M )  |->  ( ( V `
  i )  -  X ) )   &    |-  O  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  -u pi  /\  ( p `
  m )  =  pi )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  G  =  ( RR  _D  F )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) : ( ( V `  i ) (,) ( V `  ( i  +  1
 ) ) ) --> RR )   &    |-  ( ph  ->  E  e.  (
 ( G  |`  ( -oo (,)
 X ) ) lim CC  X ) )   &    |-  A  =  if ( ( V `
  ( i  +  1 ) )  =  X ,  E ,  ( ( R  -  if ( ( V `  ( i  +  1
 ) )  <  X ,  W ,  Y ) )  /  ( Q `
  ( i  +  1 ) ) ) )   =>    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  A  e.  ( ( H  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) ) lim
 CC  ( Q `  ( i  +  1
 ) ) ) )
 
Theoremfourierdlem75 37613* Given a piecewise smooth function 
F, the derived function 
H has a limit at the lower bound of each interval of the partition  Q. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  X  e.  RR )   &    |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  (
 0 ... m ) )  |  ( ( ( p `  0 )  =  ( -u pi  +  X )  /\  ( p `  m )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ m ) ( p `  i
 )  <  ( p `  ( i  +  1 ) ) ) }
 )   &    |-  ( ph  ->  F : RR --> RR )   &    |-  ( ph  ->  X  e.  ran  V )   &    |-  ( ph  ->  Y  e.  ( ( F  |`  ( X (,) +oo ) ) lim CC  X ) )   &    |-  ( ph  ->  W  e.  RR )   &    |-  H  =  ( s  e.  ( -u pi [,] pi ) 
 |->  if ( s  =  0 ,  0 ,  ( ( ( F `
  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  V  e.  ( P `  M ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1
 ) ) ) ) lim
 CC  ( V `  i ) ) )   &    |-  Q  =  ( i  e.  ( 0 ... M )  |->  ( ( V `
  i )  -  X ) )   &    |-  O  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  -u pi  /\  ( p `
  m )  =  pi )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  G  =  ( RR  _D  F )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) : ( ( V `  i ) (,) ( V `  ( i  +  1
 ) ) ) --> CC )   &    |-  ( ph  ->  E  e.  (
 ( G  |`  ( X (,) +oo ) ) lim CC  X ) )   &    |-  A  =  if ( ( V `
  i )  =  X ,  E ,  ( ( R  -  if ( ( V `  i )  <  X ,  W ,  Y )
 )  /  ( Q `  i ) ) )   =>    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  A  e.  ( ( H  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) ) lim
 CC  ( Q `  i ) ) )
 
Theoremfourierdlem76 37614* Continuity of  O and its limits with respect to the  S partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  ( ph  ->  X  e.  RR )   &    |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  ( -u pi  +  X )  /\  ( p `  m )  =  ( pi  +  X ) ) 
 /\  A. i  e.  (
 0..^ m ) ( p `  i )  <  ( p `  ( i  +  1
 ) ) ) }
 )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  V  e.  ( P `  M ) )   &    |-  (
 ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  e.  ( ( ( V `  i
 ) (,) ( V `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( V `
  i ) (,) ( V `  (
 i  +  1 ) ) ) ) lim CC  ( V `  i ) ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( V `
  i ) (,) ( V `  (
 i  +  1 ) ) ) ) lim CC  ( V `  ( i  +  1 ) ) ) )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  ( ph  ->  ( A [,] B ) 
 C_  ( -u pi [,] pi ) )   &    |-  ( ph  ->  -.  0  e.  ( A [,] B ) )   &    |-  ( ph  ->  C  e.  RR )   &    |-  O  =  ( s  e.  ( A [,] B )  |->  ( ( ( ( F `
  ( X  +  s ) )  -  C )  /  s
 )  x.  ( s 
 /  ( 2  x.  ( sin `  (
 s  /  2 )
 ) ) ) ) )   &    |-  Q  =  ( i  e.  ( 0
 ... M )  |->  ( ( V `  i
 )  -  X ) )   &    |-  T  =  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )   &    |-  N  =  ( ( # `  T )  -  1 )   &    |-  S  =  ( iota f f 
 Isom  <  ,  <  (
 ( 0 ... N ) ,  T )
 )   &    |-  D  =  ( ( ( if ( ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1
 ) ) ,  L ,  ( F `  ( X  +  ( S `  ( j  +  1 ) ) ) ) )  -  C ) 
 /  ( S `  ( j  +  1
 ) ) )  x.  ( ( S `  ( j  +  1
 ) )  /  (
 2  x.  ( sin `  ( ( S `  ( j  +  1
 ) )  /  2
 ) ) ) ) )   &    |-  E  =  ( ( ( if (
 ( S `  j
 )  =  ( Q `
  i ) ,  R ,  ( F `
  ( X  +  ( S `  j ) ) ) )  -  C )  /  ( S `  j ) )  x.  ( ( S `
  j )  /  ( 2  x.  ( sin `  ( ( S `
  j )  / 
 2 ) ) ) ) )   &    |-  ( ch  <->  ( ( (
 ph  /\  j  e.  ( 0..^ N ) ) 
 /\  i  e.  (
 0..^ M ) ) 
 /\  ( ( S `
  j ) (,) ( S `  (
 j  +  1 ) ) )  C_  (
 ( Q `  i
 ) (,) ( Q `  ( i  +  1
 ) ) ) ) )   =>    |-  ( ( ( (
 ph  /\  j  e.  ( 0..^ N ) ) 
 /\  i  e.  (
 0..^ M ) ) 
 /\  ( ( S `
  j ) (,) ( S `  (
 j  +  1 ) ) )  C_  (
 ( Q `  i
 ) (,) ( Q `  ( i  +  1
 ) ) ) ) 
 ->  ( ( D  e.  ( ( O  |`  ( ( S `  j ) (,) ( S `  ( j  +  1
 ) ) ) ) lim
 CC  ( S `  ( j  +  1
 ) ) )  /\  E  e.  ( ( O  |`  ( ( S `
  j ) (,) ( S `  (
 j  +  1 ) ) ) ) lim CC  ( S `  j ) ) )  /\  ( O  |`  ( ( S `
  j ) (,) ( S `  (
 j  +  1 ) ) ) )  e.  ( ( ( S `
  j ) (,) ( S `  (
 j  +  1 ) ) ) -cn-> CC )
 ) )
 
Theoremfourierdlem77 37615* If  H is bounded, then  U is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  Y  e.  RR )   &    |-  ( ph  ->  W  e.  RR )   &    |-  H  =  ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  (
 ( ( F `  ( X  +  s
 ) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) )   &    |-  K  =  ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  1 ,  (
 s  /  ( 2  x.  ( sin `  (
 s  /  2 )
 ) ) ) ) )   &    |-  U  =  ( s  e.  ( -u pi [,] pi )  |->  ( ( H `  s
 )  x.  ( K `
  s ) ) )   &    |-  ( ph  ->  E. a  e.  RR  A. s  e.  ( -u pi [,] pi ) ( abs `  ( H `  s
 ) )  <_  a
 )   =>    |-  ( ph  ->  E. b  e.  RR+  A. s  e.  ( -u pi [,] pi ) ( abs `  ( U `  s ) ) 
 <_  b )
 
Theoremfourierdlem78 37616*  G is continuous when restricted on an interval not containing  0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  ( ph  ->  A  e.  ( -u pi [,] pi ) )   &    |-  ( ph  ->  B  e.  ( -u pi [,] pi ) )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  -.  0  e.  ( A (,) B ) )   &    |-  ( ph  ->  ( F  |`  ( ( A  +  X ) (,) ( B  +  X ) ) )  e.  ( ( ( A  +  X ) (,) ( B  +  X ) ) -cn-> CC )
 )   &    |-  ( ph  ->  Y  e.  RR )   &    |-  ( ph  ->  W  e.  RR )   &    |-  H  =  ( s  e.  ( -u pi [,] pi ) 
 |->  if ( s  =  0 ,  0 ,  ( ( ( F `
  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) )   &    |-  K  =  ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  1 ,  (
 s  /  ( 2  x.  ( sin `  (
 s  /  2 )
 ) ) ) ) )   &    |-  U  =  ( s  e.  ( -u pi [,] pi )  |->  ( ( H `  s
 )  x.  ( K `
  s ) ) )   &    |-  ( ph  ->  N  e.  RR )   &    |-  S  =  ( s  e.  ( -u pi [,] pi ) 
 |->  ( sin `  (
 ( N  +  (
 1  /  2 )
 )  x.  s ) ) )   &    |-  G  =  ( s  e.  ( -u pi [,] pi )  |->  ( ( U `  s
 )  x.  ( S `
  s ) ) )   =>    |-  ( ph  ->  ( G  |`  ( A (,) B ) )  e.  (
 ( A (,) B ) -cn-> RR ) )
 
Theoremfourierdlem79 37617*  E projects every interval of the partition induced by  S on  H into a corresponding interval of the partition induced by  Q on  [ A ,  B ]. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  T  =  ( B  -  A )   &    |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  (
 0 ... m ) )  |  ( ( ( p `  0 )  =  A  /\  ( p `  m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  ( ph  ->  C  e.  RR )   &    |-  ( ph  ->  D  e.  RR )   &    |-  ( ph  ->  C  <  D )   &    |-  O  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  C  /\  ( p `
  m )  =  D )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  H  =  ( { C ,  D }  u.  { x  e.  ( C [,] D )  |  E. k  e.  ZZ  ( x  +  ( k  x.  T ) )  e.  ran  Q } )   &    |-  N  =  ( ( # `  H )  -  1 )   &    |-  S  =  ( iota f f 
 Isom  <  ,  <  (
 ( 0 ... N ) ,  H )
 )   &    |-  E  =  ( x  e.  RR  |->  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) )   &    |-  L  =  ( y  e.  ( A (,] B )  |->  if ( y  =  B ,  A ,  y ) )   &    |-  Z  =  ( ( S `  j
 )  +  if (
 ( ( S `  ( j  +  1
 ) )  -  ( S `  j ) )  <  ( ( Q `
  1 )  -  A ) ,  (
 ( ( S `  ( j  +  1
 ) )  -  ( S `  j ) ) 
 /  2 ) ,  ( ( ( Q `
  1 )  -  A )  /  2
 ) ) )   &    |-  I  =  ( x  e.  RR  |->  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `
  ( E `  x ) ) } ,  RR ,  <  )
 )   =>    |-  ( ( ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( L `  ( E `  ( S `  j ) ) ) (,) ( E `  ( S `  ( j  +  1
 ) ) ) ) 
 C_  ( ( Q `
  ( I `  ( S `  j ) ) ) (,) ( Q `  ( ( I `
  ( S `  j ) )  +  1 ) ) ) )
 
Theoremfourierdlem80 37618* The derivative of  O is bounded on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  ( A [,] B ) 
 C_  ( -u pi [,] pi ) )   &    |-  ( ph  ->  -.  0  e.  ( A [,] B ) )   &    |-  ( ph  ->  C  e.  RR )   &    |-  O  =  ( s  e.  ( A [,] B )  |->  ( ( ( F `  ( X  +  s
 ) )  -  C )  /  ( 2  x.  ( sin `  (
 s  /  2 )
 ) ) ) )   &    |-  I  =  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) )   &    |-  ( ( ph  /\  j  e.  ( 0..^ N ) )  ->  E. w  e.  RR  A. t  e.  I  ( abs `  ( F `  t ) )  <_  w )   &    |-  ( ( ph  /\  j  e.  ( 0..^ N ) )  ->  E. z  e.  RR  A. t  e.  I  ( abs `  ( ( RR  _D  ( F  |`  I ) ) `  t ) )  <_  z )   &    |-  ( ph  ->  S : ( 0 ... N ) --> ( A [,] B ) )   &    |-  ( ( ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  <  ( S `  ( j  +  1
 ) ) )   &    |-  (
 ( ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `  j ) [,] ( S `  (
 j  +  1 ) ) )  C_  ( A [,] B ) )   &    |-  ( ( ( ph  /\  r  e.  ( A [,] B ) ) 
 /\  -.  r  e.  ran 
 S )  ->  E. k  e.  ( 0..^ N ) r  e.  ( ( S `  k ) (,) ( S `  ( k  +  1
 ) ) ) )   &    |-  ( ( ph  /\  j  e.  ( 0..^ N ) )  ->  ( RR  _D  ( F  |`  I ) ) : I --> RR )   &    |-  Y  =  ( s  e.  (
 ( S `  j
 ) (,) ( S `  ( j  +  1
 ) ) )  |->  ( ( ( F `  ( X  +  s
 ) )  -  C )  /  ( 2  x.  ( sin `  (
 s  /  2 )
 ) ) ) )   &    |-  ( ch  <->  ( ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  w  e. 
 RR )  /\  z  e.  RR )  /\  A. t  e.  I  ( abs `  ( F `  t ) )  <_  w )  /\  A. t  e.  I  ( abs `  ( ( RR  _D  ( F  |`  I ) ) `  t ) )  <_  z )
 )   =>    |-  ( ph  ->  E. b  e.  RR  A. s  e. 
 dom  ( RR  _D  O ) ( abs `  ( ( RR  _D  O ) `  s
 ) )  <_  b
 )
 
Theoremfourierdlem81 37619* The integral of a piecewise continuous periodic function  F is unchanged if the domain is shifted by its period  T. In this lemma,  T is assumed to be strictly positive. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  A  /\  ( p `
  m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  T  e.  RR+ )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  (
 ( ph  /\  x  e.  ( A [,] B ) )  ->  ( F `
  ( x  +  T ) )  =  ( F `  x ) )   &    |-  S  =  ( i  e.  ( 0
 ... M )  |->  ( ( Q `  i
 )  +  T ) )   &    |-  ( ph  ->  F : RR --> CC )   &    |-  (
 ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i
 ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )   &    |-  G  =  ( x  e.  ( ( Q `  i ) [,] ( Q `  ( i  +  1
 ) ) )  |->  if ( x  =  ( Q `  i ) ,  R ,  if ( x  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `
  x ) ) ) )   &    |-  H  =  ( x  e.  ( ( S `  i ) [,] ( S `  ( i  +  1
 ) ) )  |->  ( G `  ( x  -  T ) ) )   =>    |-  ( ph  ->  S. ( ( A  +  T ) [,] ( B  +  T )
 ) ( F `  x )  _d x  =  S. ( A [,] B ) ( F `  x )  _d x )
 
Theoremfourierdlem82 37620* Integral by substitution, adding a constant to the function's argument, for a function on an open interval with finite limits ad boundary points. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  G  =  ( x  e.  ( A [,] B )  |->  if ( x  =  A ,  R ,  if ( x  =  B ,  L ,  ( ( F  |`  ( A (,) B ) ) `  x ) ) ) )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  ( ph  ->  F : ( A [,] B ) --> CC )   &    |-  ( ph  ->  ( F  |`  ( A (,) B ) )  e.  ( ( A (,) B ) -cn-> CC ) )   &    |-  ( ph  ->  L  e.  ( F lim CC  B ) )   &    |-  ( ph  ->  R  e.  ( F lim CC  A ) )   &    |-  ( ph  ->  X  e.  RR )   =>    |-  ( ph  ->  S. ( A [,] B ) ( F `  t
 )  _d t  =  S. ( ( A  -  X ) [,] ( B  -  X ) ) ( F `
  ( X  +  t ) )  _d t )
 
Theoremfourierdlem83 37621* The fourier partial sum for  F rewritten as an integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  C  =  (
 -u pi (,) pi )   &    |-  ( ph  ->  ( F  |`  C )  e.  L^1 )   &    |-  A  =  ( n  e.  NN0  |->  ( S. C ( ( F `  x )  x.  ( cos `  ( n  x.  x ) ) )  _d x  /  pi ) )   &    |-  B  =  ( n  e.  NN  |->  ( S. C ( ( F `  x )  x.  ( sin `  ( n  x.  x ) ) )  _d x  /  pi ) )   &    |-  ( ph  ->  X  e.  RR )   &    |-  S  =  ( m  e.  NN  |->  ( ( ( A `
  0 )  / 
 2 )  +  sum_ n  e.  ( 1 ... m ) ( ( ( A `  n )  x.  ( cos `  ( n  x.  X ) ) )  +  ( ( B `  n )  x.  ( sin `  ( n  x.  X ) ) ) ) ) )   &    |-  D  =  ( n  e.  NN  |->  ( s  e. 
 RR  |->  if ( ( s 
 mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  n )  +  1 )  /  ( 2  x.  pi ) ) ,  (
 ( sin `  ( ( n  +  ( 1  /  2 ) )  x.  s ) ) 
 /  ( ( 2  x.  pi )  x.  ( sin `  (
 s  /  2 )
 ) ) ) ) ) )   &    |-  ( ph  ->  N  e.  NN )   =>    |-  ( ph  ->  ( S `  N )  =  S. C ( ( F `  x )  x.  ( ( D `
  N ) `  ( x  -  X ) ) )  _d x )
 
Theoremfourierdlem84 37622* If  F is piecewise coninuous and  D is continuous, then  G is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  F : RR --> RR )   &    |-  ( ph  ->  X  e.  RR )   &    |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  (
 0 ... m ) )  |  ( ( ( p `  0 )  =  ( A  +  X )  /\  ( p `
  m )  =  ( B  +  X ) )  /\  A. i  e.  ( 0..^ m ) ( p `  i
 )  <  ( p `  ( i  +  1 ) ) ) }
 )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  V  e.  ( P `  M ) )   &    |-  (
 ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  e.  ( ( ( V `  i
 ) (,) ( V `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( V `
  i ) (,) ( V `  (
 i  +  1 ) ) ) ) lim CC  ( V `  i ) ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( V `
  i ) (,) ( V `  (
 i  +  1 ) ) ) ) lim CC  ( V `  ( i  +  1 ) ) ) )   &    |-  Q  =  ( i  e.  ( 0
 ... M )  |->  ( ( V `  i
 )  -  X ) )   &    |-  O  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  A  /\  ( p `
  m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  ( ph  ->  D  e.  ( RR -cn-> RR ) )   &    |-  G  =  ( s  e.  ( A [,] B )  |->  ( ( F `  ( X  +  s )
 )  x.  ( D `
  s ) ) )   =>    |-  ( ph  ->  G  e.  L^1 )
 
Theoremfourierdlem85 37623* Limit of the function  G at the lower bounds of the partition intervals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  ( -u pi  +  X )  /\  ( p `  m )  =  ( pi  +  X ) ) 
 /\  A. i  e.  (
 0..^ m ) ( p `  i )  <  ( p `  ( i  +  1
 ) ) ) }
 )   &    |-  ( ph  ->  F : RR --> RR )   &    |-  ( ph  ->  X  e.  ran  V )   &    |-  ( ph  ->  Y  e.  ( ( F  |`  ( X (,) +oo ) ) lim CC  X ) )   &    |-  ( ph  ->  W  e.  RR )   &    |-  H  =  ( s  e.  ( -u pi [,] pi ) 
 |->  if ( s  =  0 ,  0 ,  ( ( ( F `
  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) )   &    |-  K  =  ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  1 ,  (
 s  /  ( 2  x.  ( sin `  (
 s  /  2 )
 ) ) ) ) )   &    |-  U  =  ( s  e.  ( -u pi [,] pi )  |->  ( ( H `  s
 )  x.  ( K `
  s ) ) )   &    |-  ( ph  ->  N  e.  RR )   &    |-  S  =  ( s  e.  ( -u pi [,] pi ) 
 |->  ( sin `  (
 ( N  +  (
 1  /  2 )
 )  x.  s ) ) )   &    |-  G  =  ( s  e.  ( -u pi [,] pi )  |->  ( ( U `  s
 )  x.  ( S `
  s ) ) )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  V  e.  ( P `  M ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1
 ) ) ) ) lim
 CC  ( V `  i ) ) )   &    |-  Q  =  ( i  e.  ( 0 ... M )  |->  ( ( V `
  i )  -  X ) )   &    |-  O  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  -u pi  /\  ( p `
  m )  =  pi )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  I  =  ( RR  _D  F )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( I  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) : ( ( V `  i ) (,) ( V `  ( i  +  1
 ) ) ) --> CC )   &    |-  ( ph  ->  E  e.  (
 ( I  |`  ( X (,) +oo ) ) lim CC  X ) )   &    |-  A  =  ( ( if (
 ( V `  i
 )  =  X ,  E ,  ( ( R  -  if ( ( V `  i )  <  X ,  W ,  Y ) )  /  ( Q `  i ) ) )  x.  ( K `  ( Q `  i ) ) )  x.  ( S `  ( Q `  i ) ) )   =>    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  A  e.  ( ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) ) lim
 CC  ( Q `  i ) ) )
 
Theoremfourierdlem86 37624* Continuity of  O and its limits with respect to the  S partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  ( ph  ->  X  e.  RR )   &    |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  ( -u pi  +  X )  /\  ( p `  m )  =  ( pi  +  X ) ) 
 /\  A. i  e.  (
 0..^ m ) ( p `  i )  <  ( p `  ( i  +  1
 ) ) ) }
 )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  V  e.  ( P `  M ) )   &    |-  (
 ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  e.  ( ( ( V `  i
 ) (,) ( V `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( V `
  i ) (,) ( V `  (
 i  +  1 ) ) ) ) lim CC  ( V `  i ) ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( V `
  i ) (,) ( V `  (
 i  +  1 ) ) ) ) lim CC  ( V `  ( i  +  1 ) ) ) )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  ( ph  ->  ( A [,] B ) 
 C_  ( -u pi [,] pi ) )   &    |-  ( ph  ->  -.  0  e.  ( A [,] B ) )   &    |-  ( ph  ->  C  e.  RR )   &    |-  O  =  ( s  e.  ( A [,] B )  |->  ( ( ( ( F `
  ( X  +  s ) )  -  C )  /  s
 )  x.  ( s 
 /  ( 2  x.  ( sin `  (
 s  /  2 )
 ) ) ) ) )   &    |-  Q  =  ( i  e.  ( 0
 ... M )  |->  ( ( V `  i
 )  -  X ) )   &    |-  T  =  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )   &    |-  N  =  ( ( # `  T )  -  1 )   &    |-  S  =  ( iota f f 
 Isom  <  ,  <  (
 ( 0 ... N ) ,  T )
 )   &    |-  D  =  ( ( ( if ( ( S `  ( j  +  1 ) )  =  ( Q `  ( U  +  1
 ) ) ,  [_ U  /  i ]_ L ,  ( F `  ( X  +  ( S `  ( j  +  1 ) ) ) ) )  -  C ) 
 /  ( S `  ( j  +  1
 ) ) )  x.  ( ( S `  ( j  +  1
 ) )  /  (
 2  x.  ( sin `  ( ( S `  ( j  +  1
 ) )  /  2
 ) ) ) ) )   &    |-  E  =  ( ( ( if (
 ( S `  j
 )  =  ( Q `
  U ) , 
 [_ U  /  i ]_ R ,  ( F `
  ( X  +  ( S `  j ) ) ) )  -  C )  /  ( S `  j ) )  x.  ( ( S `
  j )  /  ( 2  x.  ( sin `  ( ( S `
  j )  / 
 2 ) ) ) ) )   &    |-  U  =  (
 iota_ i  e.  (
 0..^ M ) ( ( S `  j
 ) (,) ( S `  ( j  +  1
 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )   =>    |-  ( ( ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( D  e.  ( ( O  |`  ( ( S `
  j ) (,) ( S `  (
 j  +  1 ) ) ) ) lim CC  ( S `  ( j  +  1 ) ) )  /\  E  e.  ( ( O  |`  ( ( S `  j ) (,) ( S `  ( j  +  1
 ) ) ) ) lim
 CC  ( S `  j ) ) ) 
 /\  ( O  |`  ( ( S `  j ) (,) ( S `  ( j  +  1
 ) ) ) )  e.  ( ( ( S `  j ) (,) ( S `  ( j  +  1
 ) ) ) -cn-> CC ) ) )
 
Theoremfourierdlem87 37625* The integral of  G goes uniformly ( with respect to  n) to zero if the measure of the domain of integration goes to zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  Y  e.  RR )   &    |-  ( ph  ->  W  e.  RR )   &    |-  H  =  ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  (
 ( ( F `  ( X  +  s
 ) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) )   &    |-  K  =  ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  1 ,  (
 s  /  ( 2  x.  ( sin `  (
 s  /  2 )
 ) ) ) ) )   &    |-  U  =  ( s  e.  ( -u pi [,] pi )  |->  ( ( H `  s
 )  x.  ( K `
  s ) ) )   &    |-  S  =  ( s  e.  ( -u pi [,] pi )  |->  ( sin `  ( ( n  +  ( 1  /  2 ) )  x.  s ) ) )   &    |-  G  =  ( s  e.  ( -u pi [,] pi )  |->  ( ( U `  s
 )  x.  ( S `
  s ) ) )   &    |-  ( ph  ->  E. x  e.  RR  A. s  e.  ( -u pi [,] pi ) ( abs `  ( H `  s
 ) )  <_  x )   &    |-  ( ( ph  /\  n  e.  NN )  ->  G  e.  L^1 )   &    |-  D  =  ( ( e  / 
 3 )  /  a
 )   &    |-  ( ch  <->  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  a  e.  RR+  /\  A. n  e. 
 NN  A. s  e.  ( -u pi [,] pi ) ( abs `  ( G `  s ) ) 
 <_  a )  /\  u  e.  dom  vol )  /\  ( u  C_  ( -u pi [,] pi )  /\  ( vol `  u )  <_  D ) )  /\  n  e.  NN )
 )   =>    |-  ( ( ph  /\  e  e.  RR+ )  ->  E. d  e.  RR+  A. u  e.  dom  vol ( ( u  C_  ( -u pi [,] pi )  /\  ( vol `  u )  <_  d )  ->  A. k  e.  NN  ( abs `  S. u ( ( U `  s )  x.  ( sin `  ( ( k  +  ( 1  / 
 2 ) )  x.  s ) ) )  _d s )  < 
 ( e  /  2
 ) ) )
 
Theoremfourierdlem88 37626* Given a piecewise continuous function  F, a continuous function  K and a continuous function  S, the function  G is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  ( -u pi  +  X )  /\  ( p `  m )  =  ( pi  +  X ) ) 
 /\  A. i  e.  (
 0..^ m ) ( p `  i )  <  ( p `  ( i  +  1
 ) ) ) }
 )   &    |-  ( ph  ->  F : RR --> RR )   &    |-  ( ph  ->  X  e.  ran  V )   &    |-  ( ph  ->  Y  e.  ( ( F  |`  ( X (,) +oo ) ) lim CC  X ) )   &    |-  ( ph  ->  W  e.  ( ( F  |`  ( -oo (,) X ) ) lim CC  X ) )   &    |-  H  =  ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  (
 ( ( F `  ( X  +  s
 ) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) )   &    |-  K  =  ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  1 ,  (
 s  /  ( 2  x.  ( sin `  (
 s  /  2 )
 ) ) ) ) )   &    |-  U  =  ( s  e.  ( -u pi [,] pi )  |->  ( ( H `  s
 )  x.  ( K `
  s ) ) )   &    |-  ( ph  ->  N  e.  RR )   &    |-  S  =  ( s  e.  ( -u pi [,] pi ) 
 |->  ( sin `  (
 ( N  +  (
 1  /  2 )
 )  x.  s ) ) )   &    |-  G  =  ( s  e.  ( -u pi [,] pi )  |->  ( ( U `  s
 )  x.  ( S `
  s ) ) )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  V  e.  ( P `  M ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  e.  ( ( ( V `  i
 ) (,) ( V `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( V `
  i ) (,) ( V `  (
 i  +  1 ) ) ) ) lim CC  ( V `  i ) ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( V `
  i ) (,) ( V `  (
 i  +  1 ) ) ) ) lim CC  ( V `  ( i  +  1 ) ) ) )   &    |-  Q  =  ( i  e.  ( 0
 ... M )  |->  ( ( V `  i
 )  -  X ) )   &    |-  O  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  -u pi  /\  ( p `
  m )  =  pi )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  I  =  ( RR  _D  F )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( I  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) : ( ( V `  i ) (,) ( V `  ( i  +  1
 ) ) ) --> RR )   &    |-  ( ph  ->  C  e.  (
 ( I  |`  ( -oo (,)
 X ) ) lim CC  X ) )   &    |-  ( ph  ->  D  e.  (
 ( I  |`  ( X (,) +oo ) ) lim CC  X ) )   =>    |-  ( ph  ->  G  e.  L^1 )
 
Theoremfourierdlem89 37627* Given a piecewise continuous function and changing the interval and the partition, the limit at the lower bound of each interval of the moved partition is still finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  A  /\  ( p `
  m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  T  =  ( B  -  A )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  ( ph  ->  F : RR --> CC )   &    |-  ( ( ph  /\  x  e.  RR )  ->  ( F `  ( x  +  T )
 )  =  ( F `
  x ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i
 ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )   &    |-  ( ph  ->  C  e.  RR )   &    |-  ( ph  ->  D  e.  ( C (,) +oo ) )   &    |-  O  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  C  /\  ( p `
  m )  =  D )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  H  =  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  ran  Q } )   &    |-  N  =  ( ( # `  H )  -  1 )   &    |-  S  =  ( iota f f 
 Isom  <  ,  <  (
 ( 0 ... N ) ,  H )
 )   &    |-  E  =  ( x  e.  RR  |->  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) )   &    |-  Z  =  ( y  e.  ( A (,] B )  |->  if ( y  =  B ,  A ,  y ) )   &    |-  ( ph  ->  J  e.  ( 0..^ N ) )   &    |-  U  =  ( ( S `  ( J  +  1 )
 )  -  ( E `
  ( S `  ( J  +  1
 ) ) ) )   &    |-  I  =  ( x  e.  RR  |->  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( Z `
  ( E `  x ) ) } ,  RR ,  <  )
 )   &    |-  V  =  ( i  e.  ( 0..^ M )  |->  R )   =>    |-  ( ph  ->  if ( ( Z `  ( E `  ( S `
  J ) ) )  =  ( Q `
  ( I `  ( S `  J ) ) ) ,  ( V `  ( I `  ( S `  J ) ) ) ,  ( F `  ( Z `  ( E `  ( S `
  J ) ) ) ) )  e.  ( ( F  |`  ( ( S `  J ) (,) ( S `  ( J  +  1
 ) ) ) ) lim
 CC  ( S `  J ) ) )
 
Theoremfourierdlem90 37628* Given a piecewise continuous function, it is still continuous with respect to an open interval of the moved partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  A  /\  ( p `
  m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  T  =  ( B  -  A )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  ( ph  ->  F : RR --> CC )   &    |-  ( ( ph  /\  x  e.  RR )  ->  ( F `  ( x  +  T )
 )  =  ( F `
  x ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i
 ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ph  ->  C  e.  RR )   &    |-  ( ph  ->  D  e.  ( C (,) +oo ) )   &    |-  O  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  C  /\  ( p `
  m )  =  D )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  H  =  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  ran  Q } )   &    |-  N  =  ( ( # `  H )  -  1 )   &    |-  S  =  ( iota f f 
 Isom  <  ,  <  (
 ( 0 ... N ) ,  H )
 )   &    |-  E  =  ( x  e.  RR  |->  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) )   &    |-  L  =  ( y  e.  ( A (,] B )  |->  if ( y  =  B ,  A ,  y ) )   &    |-  ( ph  ->  J  e.  ( 0..^ N ) )   &    |-  U  =  ( ( S `  ( J  +  1 )
 )  -  ( E `
  ( S `  ( J  +  1
 ) ) ) )   &    |-  G  =  ( F  |`  ( ( L `  ( E `  ( S `
  J ) ) ) (,) ( E `
  ( S `  ( J  +  1
 ) ) ) ) )   &    |-  R  =  ( y  e.  ( ( ( L `  ( E `  ( S `  J ) ) )  +  U ) (,) ( ( E `  ( S `  ( J  +  1 ) ) )  +  U ) )  |->  ( G `  ( y  -  U ) ) )   &    |-  I  =  ( x  e.  RR  |->  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `
  ( E `  x ) ) } ,  RR ,  <  )
 )   =>    |-  ( ph  ->  ( F  |`  ( ( S `
  J ) (,) ( S `  ( J  +  1 )
 ) ) )  e.  ( ( ( S `
  J ) (,) ( S `  ( J  +  1 )
 ) ) -cn-> CC )
 )
 
Theoremfourierdlem91 37629* Given a piecewise continuous function and changing the interval and the partition, the limit at the upper bound of each interval of the moved partition is still finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  A  /\  ( p `
  m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  T  =  ( B  -  A )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  ( ph  ->  F : RR --> CC )   &    |-  ( ( ph  /\  x  e.  RR )  ->  ( F `  ( x  +  T )
 )  =  ( F `
  x ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i
 ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )   &    |-  ( ph  ->  C  e.  RR )   &    |-  ( ph  ->  D  e.  ( C (,) +oo ) )   &    |-  O  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  C  /\  ( p `
  m )  =  D )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  H  =  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  ran  Q } )   &    |-  N  =  ( ( # `  H )  -  1 )   &    |-  S  =  ( iota f f 
 Isom  <  ,  <  (
 ( 0 ... N ) ,  H )
 )   &    |-  E  =  ( x  e.  RR  |->  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) )   &    |-  Z  =  ( y  e.  ( A (,] B )  |->  if ( y  =  B ,  A ,  y ) )   &    |-  ( ph  ->  J  e.  ( 0..^ N ) )   &    |-  U  =  ( ( S `  ( J  +  1 )
 )  -  ( E `
  ( S `  ( J  +  1
 ) ) ) )   &    |-  I  =  ( x  e.  RR  |->  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( Z `
  ( E `  x ) ) } ,  RR ,  <  )
 )   &    |-  W  =  ( i  e.  ( 0..^ M )  |->  L )   =>    |-  ( ph  ->  if ( ( E `  ( S `  ( J  +  1 ) ) )  =  ( Q `
  ( ( I `
  ( S `  J ) )  +  1 ) ) ,  ( W `  ( I `  ( S `  J ) ) ) ,  ( F `  ( E `  ( S `
  ( J  +  1 ) ) ) ) )  e.  (
 ( F  |`  ( ( S `  J ) (,) ( S `  ( J  +  1
 ) ) ) ) lim
 CC  ( S `  ( J  +  1
 ) ) ) )
 
Theoremfourierdlem92 37630* The integral of a piecewise continuous periodic function  F is unchanged if the domain is shifted by its period  T. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  A  /\  ( p `
  m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  T  e.  RR )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  (
 ( ph  /\  x  e.  ( A [,] B ) )  ->  ( F `
  ( x  +  T ) )  =  ( F `  x ) )   &    |-  S  =  ( i  e.  ( 0
 ... M )  |->  ( ( Q `  i
 )  +  T ) )   &    |-  H  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  ( A  +  T )  /\  ( p `  m )  =  ( B  +  T )
 )  /\  A. i  e.  ( 0..^ m ) ( p `  i
 )  <  ( p `  ( i  +  1 ) ) ) }
 )   &    |-  ( ph  ->  F : RR --> CC )   &    |-  (
 ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i
 ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )   =>    |-  ( ph  ->  S. ( ( A  +  T ) [,] ( B  +  T )
 ) ( F `  x )  _d x  =  S. ( A [,] B ) ( F `  x )  _d x )
 
Theoremfourierdlem93 37631* Integral by substitution (the domain is shifted by  X) for a piecewise continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  -u pi  /\  ( p `
  m )  =  pi )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  H  =  ( i  e.  (
 0 ... M )  |->  ( ( Q `  i
 )  -  X ) )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  F : ( -u pi [,] pi ) --> CC )   &    |-  (
 ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i
 ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )   =>    |-  ( ph  ->  S. ( -u pi [,] pi ) ( F `  t )  _d t  =  S. ( ( -u pi  -  X ) [,] ( pi  -  X ) ) ( F `
  ( X  +  s ) )  _d s )
 
Theoremfourierdlem94 37632* For a piecewise smooth function, the left and the right limits exist at any point. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  T  =  ( 2  x.  pi )   &    |-  ( ( ph  /\  x  e.  RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x ) )   &    |-  ( ph  ->  X  e.  RR )   &    |-  P  =  ( n  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... n ) )  |  ( ( ( p `
  0 )  =  -u pi  /\  ( p `
  n )  =  pi )  /\  A. i  e.  ( 0..^ n ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( RR  _D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( RR 
 _D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `
  i ) )  =/=  (/) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( RR 
 _D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `
  ( i  +  1 ) ) )  =/=  (/) )   =>    |-  ( ph  ->  (
 ( ( F  |`  ( -oo (,)
 X ) ) lim CC  X )  =/=  (/)  /\  (
 ( F  |`  ( X (,) +oo ) ) lim CC  X )  =/=  (/) ) )
 
Theoremfourierdlem95 37633* Algebraic manipulation of integrals, used by other lemmas. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  ( ph  ->  X  e.  RR )   &    |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  ( -u pi  +  X )  /\  ( p `  m )  =  ( pi  +  X ) ) 
 /\  A. i  e.  (
 0..^ m ) ( p `  i )  <  ( p `  ( i  +  1
 ) ) ) }
 )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  V  e.  ( P `  M ) )   &    |-  ( ph  ->  X  e.  ran  V )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1
 ) ) ) )  e.  ( ( ( V `  i ) (,) ( V `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( V `
  i ) (,) ( V `  (
 i  +  1 ) ) ) ) lim CC  ( V `  i ) ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( V `
  i ) (,) ( V `  (
 i  +  1 ) ) ) ) lim CC  ( V `  ( i  +  1 ) ) ) )   &    |-  H  =  ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  (
 ( ( F `  ( X  +  s
 ) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) )   &    |-  K  =  ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  1 ,  (
 s  /  ( 2  x.  ( sin `  (
 s  /  2 )
 ) ) ) ) )   &    |-  U  =  ( s  e.  ( -u pi [,] pi )  |->  ( ( H `  s
 )  x.  ( K `
  s ) ) )   &    |-  S  =  ( s  e.  ( -u pi [,] pi )  |->  ( sin `  ( ( n  +  ( 1  /  2 ) )  x.  s ) ) )   &    |-  G  =  ( s  e.  ( -u pi [,] pi )  |->  ( ( U `  s
 )  x.  ( S `
  s ) ) )   &    |-  I  =  ( RR  _D  F )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( I  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) : ( ( V `  i ) (,) ( V `  ( i  +  1
 ) ) ) --> RR )   &    |-  ( ph  ->  B  e.  (
 ( I  |`  ( -oo (,)
 X ) ) lim CC  X ) )   &    |-  ( ph  ->  C  e.  (
 ( I  |`  ( X (,) +oo ) ) lim CC  X ) )   &    |-  ( ph  ->  Y  e.  (
 ( F  |`  ( X (,) +oo ) ) lim CC  X ) )   &    |-  ( ph  ->  W  e.  (
 ( F  |`  ( -oo (,)
 X ) ) lim CC  X ) )   &    |-  ( ph  ->  A  e.  dom  vol )   &    |-  ( ph  ->  A 
 C_  ( ( -u pi [,] pi )  \  { 0 } )
 )   &    |-  E  =  ( n  e.  NN  |->  ( S. A ( G `  s )  _d s  /  pi ) )   &    |-  D  =  ( n  e.  NN  |->  ( s  e.  RR  |->  if ( ( s  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  n )  +  1 )  /  (
 2  x.  pi ) ) ,  ( ( sin `  ( ( n  +  ( 1  /  2 ) )  x.  s ) ) 
 /  ( ( 2  x.  pi )  x.  ( sin `  (
 s  /  2 )
 ) ) ) ) ) )   &    |-  ( ph  ->  O  e.  RR )   &    |-  (
 ( ph  /\  s  e.  A )  ->  if ( 0  <  s ,  Y ,  W )  =  O )   &    |-  (
 ( ph  /\  n  e. 
 NN )  ->  S. A ( ( D `
  n ) `  s )  _d s  =  ( 1  /  2
 ) )   =>    |-  ( ( ph  /\  n  e.  NN )  ->  (
 ( E `  n )  +  ( O  /  2 ) )  =  S. A ( ( F `  ( X  +  s ) )  x.  ( ( D `
  n ) `  s ) )  _d s )
 
Theoremfourierdlem96 37634* limit for  F at the lower bound of an interval for the moved partition  V. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  A  /\  ( p `
  m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  T  =  ( B  -  A )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  (
 ( ph  /\  x  e. 
 RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )   &    |-  ( ph  ->  C  e.  RR )   &    |-  ( ph  ->  D  e.  ( C (,) +oo ) )   &    |-  ( ph  ->  J  e.  (
 0..^ ( ( # `  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  ran  Q } ) )  -  1 ) ) )   &    |-  V  =  ( iota g g  Isom  <  ,  <  ( ( 0 ... ( ( # `  ( { C ,  D }  u.  { y  e.  ( C [,] D )  | 
 E. k  e.  ZZ  ( y  +  (
 k  x.  T ) )  e.  ran  Q } ) )  -  1 ) ) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. h  e.  ZZ  ( y  +  ( h  x.  T ) )  e.  ran  Q } ) ) )   =>    |-  ( ph  ->  if (
 ( ( u  e.  ( A (,] B )  |->  if ( u  =  B ,  A ,  u ) ) `  ( ( v  e. 
 RR  |->  ( v  +  ( ( |_ `  (
 ( B  -  v
 )  /  T )
 )  x.  T ) ) ) `  ( V `  J ) ) )  =  ( Q `
  ( ( y  e.  RR  |->  sup ( { j  e.  (
 0..^ M )  |  ( Q `  j
 )  <_  ( ( u  e.  ( A (,] B )  |->  if ( u  =  B ,  A ,  u )
 ) `  ( (
 v  e.  RR  |->  ( v  +  ( ( |_ `  ( ( B  -  v ) 
 /  T ) )  x.  T ) ) ) `  y ) ) } ,  RR ,  <  ) ) `  ( V `  J ) ) ) ,  (
 ( i  e.  (
 0..^ M )  |->  R ) `  ( ( y  e.  RR  |->  sup ( { j  e.  ( 0..^ M )  |  ( Q `  j )  <_  ( ( u  e.  ( A (,] B )  |->  if ( u  =  B ,  A ,  u ) ) `  ( ( v  e.  RR  |->  ( v  +  ( ( |_ `  ( ( B  -  v ) 
 /  T ) )  x.  T ) ) ) `  y ) ) } ,  RR ,  <  ) ) `  ( V `  J ) ) ) ,  ( F `  ( ( u  e.  ( A (,] B )  |->  if ( u  =  B ,  A ,  u ) ) `  ( ( v  e. 
 RR  |->  ( v  +  ( ( |_ `  (
 ( B  -  v
 )  /  T )
 )  x.  T ) ) ) `  ( V `  J ) ) ) ) )  e.  ( ( F  |`  ( ( V `  J ) (,) ( V `  ( J  +  1
 ) ) ) ) lim
 CC  ( V `  J ) ) )
 
Theoremfourierdlem97 37635*  F is continuous on the intervals induced by the moved partition  V. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  G  =  ( RR  _D  F )   &    |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  A  /\  ( p `
  m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  e.  RR )   &    |-  T  =  ( B  -  A )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  (
 ( ph  /\  x  e. 
 RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ph  ->  C  e.  RR )   &    |-  ( ph  ->  D  e.  ( C (,) +oo ) )   &    |-  ( ph  ->  J  e.  (
 0..^ ( ( # `  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  ran  Q } ) )  -  1 ) ) )   &    |-  V  =  ( iota g g  Isom  <  ,  <  ( ( 0 ... ( ( # `  ( { C ,  D }  u.  { y  e.  ( C [,] D )  | 
 E. k  e.  ZZ  ( y  +  (
 k  x.  T ) )  e.  ran  Q } ) )  -  1 ) ) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. h  e.  ZZ  ( y  +  ( h  x.  T ) )  e.  ran  Q } ) ) )   &    |-  H  =  ( s  e.  RR  |->  if ( s  e. 
 dom  G ,  ( G `
  s ) ,  0 ) )   =>    |-  ( ph  ->  ( G  |`  ( ( V `  J ) (,) ( V `  ( J  +  1 )
 ) ) )  e.  ( ( ( V `
  J ) (,) ( V `  ( J  +  1 )
 ) ) -cn-> CC )
 )
 
Theoremfourierdlem98 37636*  F is continuous on the intervals induced by the moved partition  V. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  A  /\  ( p `
  m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  T  =  ( B  -  A )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  (
 ( ph  /\  x  e. 
 RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1
 )