Home Metamath Proof ExplorerTheorem 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 (1-26406) Hilbert Space Explorer (26407-27929) 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.)
..^                                           ..^                                           ..^

Theoremfourierdlem64 37602* The partition is finer than , when is moved on the same interval where lies. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
..^                                                                ..^              ..^        ..^ ..^

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.)
..^                                           ..^                                           ..^

Theoremfourierdlem66 37604* Value of the function when the argument is not zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Theoremfourierdlem67 37605* is a function (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Theoremfourierdlem68 37606* The derivative of is bounded on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Theoremfourierdlem69 37607* A piecewise continuous function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
..^                             ..^        ..^ lim        ..^ lim

Theoremfourierdlem70 37608* A piecewise continuous function is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
..^        ..^        ..^ lim        ..^ lim        ..^

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.)
..^        ..^ lim        ..^ lim                      ..^

Theoremfourierdlem72 37610* The derivative of is continuous on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
..^                      ..^                                                         ..^

Theoremfourierdlem73 37611* A version of the Riemann Lebesgue lemma: as increases, the integral in goes to zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
..^        ..^        ..^ lim        ..^ lim               ..^

Theoremfourierdlem74 37612* Given a piecewise smooth function , the derived function has a limit at the upper bound of each interval of the partition . (Contributed by Glauco Siliprandi, 11-Dec-2019.)
..^                             lim                             ..^ lim               ..^               ..^        lim               ..^ lim

Theoremfourierdlem75 37613* Given a piecewise smooth function , the derived function has a limit at the lower bound of each interval of the partition . (Contributed by Glauco Siliprandi, 11-Dec-2019.)
..^                      lim                                    ..^ lim               ..^               ..^        lim               ..^ lim

Theoremfourierdlem76 37614* Continuity of and its limits with respect to the partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
..^                      ..^        ..^ lim        ..^ lim                                                                                                   ..^ ..^        ..^ ..^ lim lim

Theoremfourierdlem77 37615* If is bounded, then is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Theoremfourierdlem78 37616* is continuous when restricted on an interval not containing . (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Theoremfourierdlem79 37617* projects every interval of the partition induced by on into a corresponding interval of the partition induced by on . (Contributed by Glauco Siliprandi, 11-Dec-2019.)
..^                                           ..^                                                  ..^        ..^

Theoremfourierdlem80 37618* The derivative of is bounded on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
..^        ..^               ..^        ..^        ..^        ..^               ..^

Theoremfourierdlem81 37619* The integral of a piecewise continuous periodic function is unchanged if the domain is shifted by its period . In this lemma, is assumed to be strictly positive. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
..^                                                  ..^        ..^ lim        ..^ lim

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.)
lim        lim

Theoremfourierdlem83 37621* The fourier partial sum for rewritten as an integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Theoremfourierdlem84 37622* If is piecewise coninuous and is continuous, then is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
..^                      ..^        ..^ lim        ..^ lim               ..^

Theoremfourierdlem85 37623* Limit of the function at the lower bounds of the partition intervals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
..^                      lim                                                                       ..^ lim               ..^               ..^        lim               ..^ lim

Theoremfourierdlem86 37624* Continuity of and its limits with respect to the partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
..^                      ..^        ..^ lim        ..^ lim                                                                                                   ..^        ..^ lim lim

Theoremfourierdlem87 37625* The integral of goes uniformly ( with respect to ) to zero if the measure of the domain of integration goes to zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Theoremfourierdlem88 37626* Given a piecewise continuous function , a continuous function and a continuous function , the function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
..^                      lim        lim                                                                ..^        ..^ lim        ..^ lim               ..^               ..^        lim        lim

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.)
..^                                           ..^        ..^ lim                      ..^                                           ..^              ..^        ..^        lim

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.)
..^                                           ..^                      ..^                                           ..^                            ..^

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.)
..^                                           ..^        ..^ lim                      ..^                                           ..^              ..^        ..^        lim

Theoremfourierdlem92 37630* The integral of a piecewise continuous periodic function is unchanged if the domain is shifted by its period . (Contributed by Glauco Siliprandi, 11-Dec-2019.)
..^                                           ..^               ..^        ..^ lim        ..^ lim

Theoremfourierdlem93 37631* Integral by substitution (the domain is shifted by ) for a piecewise continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
..^                                           ..^        ..^ lim        ..^ lim

Theoremfourierdlem94 37632* For a piecewise smooth function, the left and the right limits exist at any point. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
..^                      ..^        ..^ lim        ..^ lim        lim lim

Theoremfourierdlem95 37633* Algebraic manipulation of integrals, used by other lemmas. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
..^                             ..^        ..^ lim        ..^ lim                                                  ..^        lim        lim        lim        lim

Theoremfourierdlem96 37634* limit for at the lower bound of an interval for the moved partition . (Contributed by Glauco Siliprandi, 11-Dec-2019.)
..^                                    ..^        ..^ lim                      ..^               ..^ ..^ ..^ lim

Theoremfourierdlem97 37635* is continuous on the intervals induced by the moved partition . (Contributed by Glauco Siliprandi, 11-Dec-2019.)
..^                                                  ..^                      ..^

Theoremfourierdlem98 37636* is continuous on the intervals induced by the moved partition . (Contributed by Glauco Siliprandi, 11-Dec-2019.)
..^                                    ..^