P. 404 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40301-40400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	stirlinglem11 40301*	B is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )   &    |- B = ( n e. NN |-> ( log ` ( A ` n ) ) )   &    |- K = ( k e. NN |-> ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. k ) ) ) )   =>    |- ( N e. NN -> ( B ` ( N + 1 ) ) < ( B ` N ) )
Theorem	stirlinglem12 40302*	The sequence B is bounded below. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )   &    |- B = ( n e. NN |-> ( log ` ( A ` n ) ) )   &    |- F = ( n e. NN |-> ( 1 / ( n x. ( n + 1 ) ) ) )   =>    |- ( N e. NN -> ( ( B ` 1 ) - ( 1 / 4 ) ) <_ ( B ` N ) )
Theorem	stirlinglem13 40303*	B is decreasing and has a lower bound, then it converges. Since B is log A, in another theorem it is proven that A converges as well. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )   &    |- B = ( n e. NN |-> ( log ` ( A ` n ) ) )   =>    |- E. d e. RR B ~~> d
Theorem	stirlinglem14 40304*	The sequence A converges to a positive real. This proves that the Stirling's formula converges to the factorial, up to a constant. In another theorem, using Wallis' formula for π& , such constant is exactly determined, thus proving the Stirling's formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )   &    |- B = ( n e. NN |-> ( log ` ( A ` n ) ) )   =>    |- E. c e. RR+ A ~~> c
Theorem	stirlinglem15 40305*	The Stirling's formula is proven using a number of local definitions. The main theorem stirling 40306 will use this final lemma, but it will not expose the local definitions. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- F/ n ph   &    |- S = ( n e. NN0 |-> ( ( sqr ` ( ( 2 x. pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) )   &    |- A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )   &    |- D = ( n e. NN |-> ( A ` ( 2 x. n ) ) )   &    |- E = ( n e. NN |-> ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) )   &    |- V = ( n e. NN |-> ( ( ( ( 2 ^ ( 4 x. n ) ) x. ( ( ! ` n ) ^ 4 ) ) / ( ( ! ` ( 2 x. n ) ) ^ 2 ) ) / ( ( 2 x. n ) + 1 ) ) )   &    |- F = ( n e. NN |-> ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) )   &    |- H = ( n e. NN |-> ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) )   &    |- ( ph -> C e. RR+ )   &    |- ( ph -> A ~~> C )   =>    |- ( ph -> ( n e. NN |-> ( ( ! ` n ) / ( S ` n ) ) ) ~~> 1 )
Theorem	stirling 40306	Stirling's approximation formula for n factorial. The proof follows two major steps: first it is proven that S and n factorial are asymptotically equivalent, up to an unknown constant. Then, using Wallis' formula for π it is proven that the unknown constant is the square root of π and then the exact Stirling's formula is established. This is Metamath 100 proof #90. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- S = ( n e. NN0 |-> ( ( sqr ` ( ( 2 x. pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) )   =>    |- ( n e. NN |-> ( ( ! ` n ) / ( S ` n ) ) ) ~~> 1
Theorem	stirlingr 40307	Stirling's approximation formula for n factorial: here convergence is expressed with respect to the standard topology on the reals. The main theorem stirling 40306 is proven for convergence in the topology of complex numbers. The variable R is used to denote convergence with respect to the standard topology on the reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- S = ( n e. NN0 |-> ( ( sqr ` ( ( 2 x. pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) )   &    |- R = ( ~~> t ` ( topGen ` ran (,) ) )   =>    |- ( n e. NN |-> ( ( ! ` n ) / ( S ` n ) ) ) R 1
20.32.15  Dirichlet kernel
Theorem	dirkerval 40308*	The Nth 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 ) ) ) ) ) ) )   =>    |- ( N e. NN -> ( D ` N ) = ( 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 ) ) ) ) ) ) )
Theorem	dirker2re 40309	The Dirchlet Kernel value is a real if the argument is not a multiple of π . (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( ( N e. NN /\ S e. RR ) /\ -. ( S mod ( 2 x. pi ) ) = 0 ) -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. S ) ) / ( ( 2 x. pi ) x. ( sin ` ( S / 2 ) ) ) ) e. RR )
Theorem	dirkerdenne0 40310	The Dirchlet Kernel denominator is never 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( S e. RR /\ -. ( S mod ( 2 x. pi ) ) = 0 ) -> ( ( 2 x. pi ) x. ( sin ` ( S / 2 ) ) ) =/= 0 )
Theorem	dirkerval2 40311*	The Nth Dirichlet Kernel evaluated at a specific point S. (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 ) ) ) ) ) ) )   =>    |- ( ( N e. NN /\ S e. RR ) -> ( ( D ` N ) ` S ) = 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 ) ) ) ) ) )
Theorem	dirkerre 40312*	The Dirichlet Kernel at any point evaluates to a real. (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 ) ) ) ) ) ) )   =>    |- ( ( N e. NN /\ S e. RR ) -> ( ( D ` N ) ` S ) e. RR )
Theorem	dirkerper 40313*	the Dirichlet Kernel has period 2 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 ) ) ) ) ) ) )   &    |- T = ( 2 x. pi )   =>    |- ( ( N e. NN /\ x e. RR ) -> ( ( D ` N ) ` ( x + T ) ) = ( ( D ` N ) ` x ) )
Theorem	dirkerf 40314*	For any natural number N, the Dirichlet Kernel ( D ` N ) is a function. (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 ) : RR --> RR )
Theorem	dirkertrigeqlem1 40315*	Sum of an even number of alternating cos values. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( K e. NN -> sum_ n e. ( 1 ... ( 2 x. K ) ) ( cos ` ( n x. pi ) ) = 0 )
Theorem	dirkertrigeqlem2 40316*	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 ) ) ) ) )
Theorem	dirkertrigeqlem3 40317*	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 ) ) ) ) )
Theorem	dirkertrigeq 40318*	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 )
Theorem	dirkeritg 40319*	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 ) ) )
Theorem	dirkercncflem1 40320*	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 ) ) )
Theorem	dirkercncflem2 40321*	Lemma used to prove 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 ) )
Theorem	dirkercncflem3 40322*	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 ) )
Theorem	dirkercncflem4 40323*	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 ) )
Theorem	dirkercncf 40324*	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 ) )
20.32.16  Fourier Series
Theorem	fourierdlem1 40325	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 ) )
Theorem	fourierdlem2 40326*	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 ) ) ) ) ) )
Theorem	fourierdlem3 40327*	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 ) ) ) ) ) )
Theorem	fourierdlem4 40328*	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 ) )
Theorem	fourierdlem5 40329*	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 )
Theorem	fourierdlem6 40330	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 ) )
Theorem	fourierdlem7 40331*	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 ) )
Theorem	fourierdlem8 40332	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 ) )
Theorem	fourierdlem9 40333*	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 )
Theorem	fourierdlem10 40334	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 ) )
Theorem	fourierdlem11 40335*	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 ) )
Theorem	fourierdlem12 40336*	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 ) ) ) )
Theorem	fourierdlem13 40337*	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 ) ) ) )
Theorem	fourierdlem14 40338*	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 ) )
Theorem	fourierdlem15 40339*	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 ) )
Theorem	fourierdlem16 40340*	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 ) )
Theorem	fourierdlem17 40341*	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 ) )
Theorem	fourierdlem18 40342*	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 ) )
Theorem	fourierdlem19 40343*	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 )
Theorem	fourierdlem20 40344*	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 ) ) ) )
Theorem	fourierdlem21 40345*	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 ) )
Theorem	fourierdlem22 40346*	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 ) ) )
Theorem	fourierdlem23 40347*	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 ) )
Theorem	fourierdlem24 40348	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 )
Theorem	fourierdlem25 40349*	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 ) ) ) )
Theorem	fourierdlem26 40350*	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 ) ) )
Theorem	fourierdlem27 40351	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 ) )
Theorem	fourierdlem28 40352*	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 ) ) ) )
Theorem	fourierdlem29 40353*	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 ) ) ) ) ) )
Theorem	fourierdlem30 40354*	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 )
Theorem	fourierdlem31 40355*	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 )
Theorem	fourierdlem32 40356	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 ) )
Theorem	fourierdlem33 40357	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 ) )
Theorem	fourierdlem34 40358*	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 )
Theorem	fourierdlem35 40359	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 )
Theorem	fourierdlem36 40360*	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 ) )
Theorem	fourierdlem37 40361*	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 ) ) } ) ) )
Theorem	fourierdlem38 40362*	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 ) )
Theorem	fourierdlem39 40363*	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 ) )
Theorem	fourierdlem40 40364*	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 ) )
Theorem	fourierdlem41 40365*	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 ) ) )
Theorem	fourierdlem42 40366*	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 = ( J ↾t ( 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 )
Theorem	fourierdlem43 40367	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
Theorem	fourierdlem44 40368	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 )
Theorem	fourierdlem46 40369*	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 ) ) ) =/= (/) ) )
Theorem	fourierdlem47 40370*	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 )
Theorem	fourierdlem48 40371*	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 ) =/= (/) )
Theorem	fourierdlem49 40372*	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 ) =/= (/) )
Theorem	fourierdlem50 40373*	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 ) ) ) ) )
Theorem	fourierdlem51 40374*	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 )
Theorem	fourierdlem52 40375*	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 ) )
Theorem	fourierdlem53 40376*	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 ) )
Theorem	fourierdlem54 40377*	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 ) ) )
Theorem	fourierdlem55 40378*	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 )
Theorem	fourierdlem56 40379*	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 ) ) )
Theorem	fourierdlem57 40380*	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 ) ) ) )
Theorem	fourierdlem58 40381*	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 ) )
Theorem	fourierdlem59 40382*	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 ) )
Theorem	fourierdlem60 40383*	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 ) )
Theorem	fourierdlem61 40384*	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 ) )
Theorem	fourierdlem62 40385	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 )
Theorem	fourierdlem63 40386*	The upper bound of intervals in the moved partition are mapped to points that are not greater than the corresponding upper bounds in the original partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- T = ( B - A )   &    |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- ( ph -> M e. NN )   &    |- ( ph -> Q e. ( P ` M ) )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> C < D )   &    |- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- H = ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } )   &    |- N = ( ( # ` H ) - 1 )   &    |- S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )   &    |- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )   &    |- ( ph -> K e. ( 0 ... M ) )   &    |- ( ph -> J e. ( 0..^ N ) )   &    |- ( ph -> Y e. ( ( S ` J ) [,) ( S ` ( J + 1 ) ) ) )   &    |- ( ph -> ( E ` Y ) < ( Q ` K ) )   &    |- X = ( ( Q ` K ) - ( ( E ` Y ) - Y ) )   =>    |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) <_ ( Q ` K ) )
Theorem	fourierdlem64 40387*	The partition V is finer than Q, when Q is moved on the same interval where V lies. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- T = ( B - A )   &    |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- ( ph -> M e. NN )   &    |- ( ph -> Q e. ( P ` M ) )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> C < D )   &    |- H = ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } )   &    |- N = ( ( # ` H ) - 1 )   &    |- V = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )   &    |- ( ph -> J e. ( 0..^ N ) )   &    |- L = sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < )   &    |- I = sup ( { j e. ( 0..^ M ) | ( ( Q ` j ) + ( L x. T ) ) <_ ( V ` J ) } , RR , < )   =>    |- ( ph -> ( ( I e. ( 0..^ M ) /\ L e. ZZ ) /\ E. i e. ( 0..^ M ) E. l e. ZZ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) )
Theorem	fourierdlem65 40388*	The distance of two adjacent points in the moved partition is preserved in the original partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- T = ( B - A )   &    |- ( ph -> M e. NN )   &    |- ( ph -> Q e. ( P ` M ) )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. ( C (,) +oo ) )   &    |- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- N = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) - 1 )   &    |- S = ( iota f f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) )   &    |- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )   &    |- L = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) )   &    |- Z = ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) )   =>    |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( L ` ( E ` ( S ` j ) ) ) ) = ( ( S ` ( j + 1 ) ) - ( S ` j ) ) )
Theorem	fourierdlem66 40389*	Value of the G function when the argument is not zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> X e. RR )   &    |- ( ph -> Y e. RR )   &    |- ( ph -> W e. RR )   &    |- D = ( n e. NN |-> ( s e. RR |-> if ( ( s mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) )   &    |- H = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )   &    |- K = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )   &    |- U = ( s e. ( -u pi [,] pi ) |-> ( ( H ` s ) x. ( K ` s ) ) )   &    |- S = ( s e. ( -u pi [,] pi ) |-> ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) )   &    |- G = ( s e. ( -u pi [,] pi ) |-> ( ( U ` s ) x. ( S ` s ) ) )   &    |- A = ( ( -u pi [,] pi ) \ { 0 } )   =>    |- ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( G ` s ) = ( pi x. ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) ) )
Theorem	fourierdlem67 40390*	G is a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> X e. RR )   &    |- ( ph -> Y e. RR )   &    |- ( ph -> W e. RR )   &    |- H = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )   &    |- K = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )   &    |- U = ( s e. ( -u pi [,] pi ) |-> ( ( H ` s ) x. ( K ` s ) ) )   &    |- ( ph -> N e. RR )   &    |- S = ( s e. ( -u pi [,] pi ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) )   &    |- G = ( s e. ( -u pi [,] pi ) |-> ( ( U ` s ) x. ( S ` s ) ) )   =>    |- ( ph -> G : ( -u pi [,] pi ) --> RR )
Theorem	fourierdlem68 40391*	The derivative of O is bounded on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> X e. RR )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A [,] B ) C_ ( -u pi [,] pi ) )   &    |- ( ph -> -. 0 e. ( A [,] B ) )   &    |- ( ph -> ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) : ( ( X + A ) (,) ( X + B ) ) --> RR )   &    |- ( ph -> D e. RR )   &    |- ( ( ph /\ t e. ( ( X + A ) (,) ( X + B ) ) ) -> ( abs ` ( F ` t ) ) <_ D )   &    |- ( ph -> E e. RR )   &    |- ( ( ph /\ t e. ( ( X + A ) (,) ( X + B ) ) ) -> ( abs ` ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` t ) ) <_ E )   &    |- ( ph -> C e. RR )   &    |- O = ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )   =>    |- ( ph -> ( dom ( RR _D O ) = ( A (,) B ) /\ E. b e. RR A. s e. dom ( RR _D O ) ( abs ` ( ( RR _D O ) ` s ) ) <_ b ) )
Theorem	fourierdlem69 40392*	A piecewise continuous function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- ( ph -> M e. NN )   &    |- ( ph -> Q e. ( P ` M ) )   &    |- ( ph -> F : ( A [,] B ) --> CC )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )   =>    |- ( ph -> F e. L^1 )
Theorem	fourierdlem70 40393*	A piecewise continuous function is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> F : ( A [,] B ) --> RR )   &    |- ( ph -> M e. NN )   &    |- ( ph -> Q : ( 0 ... M ) --> RR )   &    |- ( ph -> ( Q ` 0 ) = A )   &    |- ( ph -> ( Q ` M ) = B )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )   &    |- I = ( i e. ( 0..^ M ) |-> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )   =>    |- ( ph -> E. x e. RR A. s e. ( A [,] B ) ( abs ` ( F ` s ) ) <_ x )
Theorem	fourierdlem71 40394*	A periodic piecewise continuous function, possibly undefined on a finite set in each periodic interval, is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> dom F C_ RR )   &    |- ( ph -> F : dom F --> RR )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- T = ( B - A )   &    |- ( ph -> M e. NN )   &    |- ( ph -> Q : ( 0 ... M ) --> RR )   &    |- ( ph -> ( Q ` 0 ) = A )   &    |- ( ph -> ( Q ` M ) = B )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )   &    |- ( ( ( ph /\ x e. dom F ) /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. dom F )   &    |- ( ( ( ph /\ x e. dom F ) /\ k e. ZZ ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) )   &    |- I = ( i e. ( 0..^ M ) |-> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )   &    |- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )   =>    |- ( ph -> E. y e. RR A. x e. dom F ( abs ` ( F ` x ) ) <_ y )
Theorem	fourierdlem72 40395*	The derivative of O is continuous on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> X e. RR )   &    |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( -u pi + X ) /\ ( p ` m ) = ( pi + X ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- ( ph -> M e. NN )   &    |- ( ph -> V e. ( P ` M ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> RR ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A (,) B ) C_ ( -u pi [,] pi ) )   &    |- ( ph -> -. 0 e. ( A [,] B ) )   &    |- ( ph -> C e. RR )   &    |- Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )   &    |- ( ph -> U e. ( 0..^ M ) )   &    |- ( ph -> ( A (,) B ) C_ ( ( Q ` U ) (,) ( Q ` ( U + 1 ) ) ) )   &    |- H = ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / s ) )   &    |- K = ( s e. ( A (,) B ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )   &    |- O = ( s e. ( A (,) B ) |-> ( ( H ` s ) x. ( K ` s ) ) )   =>    |- ( ph -> ( RR _D O ) e. ( ( A (,) B ) -cn-> CC ) )
Theorem	fourierdlem73 40396*	A version of the Riemann Lebesgue lemma: as r increases, the integral in S goes to zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> F : ( A [,] B ) --> CC )   &    |- ( ph -> M e. NN )   &    |- ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )   &    |- ( ph -> ( Q ` 0 ) = A )   &    |- ( ph -> ( Q ` M ) = B )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )   &    |- G = ( RR _D F )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )   &    |- ( ph -> E. y e. RR A. x e. dom G ( abs ` ( G ` x ) ) <_ y )   &    |- S = ( r e. RR+ |-> S. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x )   &    |- D = ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) )   =>    |- ( ph -> A. e e. RR+ E. n e. NN A. r e. ( n (,) +oo ) ( abs ` S. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( r x. x ) ) ) _d x ) < e )
Theorem	fourierdlem74 40397*	Given a piecewise smooth function F, the derived function H has a limit at the upper bound of each interval of the partition Q. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> X e. RR )   &    |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( -u pi + X ) /\ ( p ` m ) = ( pi + X ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- ( ph -> F : RR --> RR )   &    |- ( ph -> X e. ran V )   &    |- ( ph -> Y e. RR )   &    |- ( ph -> W e. ( ( F |` ( -oo (,) X ) ) lim CC X ) )   &    |- H = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> V e. ( P ` M ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` ( i + 1 ) ) ) )   &    |- Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )   &    |- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = -u pi /\ ( p ` m ) = pi ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- G = ( RR _D F )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( G |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR )   &    |- ( ph -> E e. ( ( G |` ( -oo (,) X ) ) lim CC X ) )   &    |- A = if ( ( V ` ( i + 1 ) ) = X , E , ( ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) / ( Q ` ( i + 1 ) ) ) )   =>    |- ( ( ph /\ i e. ( 0..^ M ) ) -> A e. ( ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
Theorem	fourierdlem75 40398*	Given a piecewise smooth function F, the derived function H has a limit at the lower bound of each interval of the partition Q. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> X e. RR )   &    |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( -u pi + X ) /\ ( p ` m ) = ( pi + X ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- ( ph -> F : RR --> RR )   &    |- ( ph -> X e. ran V )   &    |- ( ph -> Y e. ( ( F |` ( X (,) +oo ) ) lim CC X ) )   &    |- ( ph -> W e. RR )   &    |- H = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> V e. ( P ` M ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` i ) ) )   &    |- Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )   &    |- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = -u pi /\ ( p ` m ) = pi ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- G = ( RR _D F )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( G |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> CC )   &    |- ( ph -> E e. ( ( G |` ( X (,) +oo ) ) lim CC X ) )   &    |- A = if ( ( V ` i ) = X , E , ( ( R - if ( ( V ` i ) < X , W , Y ) ) / ( Q ` i ) ) )   =>    |- ( ( ph /\ i e. ( 0..^ M ) ) -> A e. ( ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
Theorem	fourierdlem76 40399*	Continuity of O and its limits with respect to the S partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> X e. RR )   &    |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( -u pi + X ) /\ ( p ` m ) = ( pi + X ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )   &    |- ( ph -> M e. NN )   &    |- ( ph -> V e. ( P ` M ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` i ) ) )   &    |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` ( i + 1 ) ) ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A [,] B ) C_ ( -u pi [,] pi ) )   &    |- ( ph -> -. 0 e. ( A [,] B ) )   &    |- ( ph -> C e. RR )   &    |- O = ( s e. ( A [,] B ) |-> ( ( ( ( F ` ( X + s ) ) - C ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )   &    |- Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )   &    |- T = ( { A , B } u. ( ran Q i^i ( A (,) B ) ) )   &    |- N = ( ( # ` T ) - 1 )   &    |- S = ( iota f f Isom < , < ( ( 0 ... N ) , T ) )   &    |- D = ( ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) ) x. ( ( S ` ( j + 1 ) ) / ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) ) )   &    |- E = ( ( ( if ( ( S ` j ) = ( Q ` i ) , R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) )   &    |- ( ch <-> ( ( ( ph /\ j e. ( 0..^ N ) ) /\ i e. ( 0..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )   =>    |- ( ( ( ( ph /\ j e. ( 0..^ N ) ) /\ i e. ( 0..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( D e. ( ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) lim CC ( S ` ( j + 1 ) ) ) /\ E e. ( ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) lim CC ( S ` j ) ) ) /\ ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) ) )
Theorem	fourierdlem77 40400*	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 )