Home | Metamath
Proof Explorer Theorem List (p. 381 of 409) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-26620) |
Hilbert Space Explorer
(26621-28143) |
Users' Mathboxes
(28144-40813) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dirkertrigeq 38001* | Trigonometric equality for the Dirichlet kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | dirkeritg 38002* | The definite integral of the Dirichlet Kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | dirkercncflem1 38003* | If is a multiple of then it belongs to an open inerval such that for any other point 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.) |
Theorem | dirkercncflem2 38004* | Lemma used to proof that the Dirichlet Kernel is continuous at points that are multiples of . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
lim | ||
Theorem | dirkercncflem3 38005* | The Dirichlet Kernel is continuous at points that are multiples of . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
lim | ||
Theorem | dirkercncflem4 38006* | The Dirichlet Kernel is continuos at points that are not multiple of 2 π . This is the easier condition, for the proof of the continuity of the Dirichlet kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | dirkercncf 38007* | For any natural number , the Dirichlet Kernel is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem1 38008 | A partition interval is a subset of the partitioned interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ | ||
Theorem | fourierdlem2 38009* | Membership in a partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ ..^ | ||
Theorem | fourierdlem3 38010* | Membership in a partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ ..^ | ||
Theorem | fourierdlem4 38011* | is a function that maps any point to a periodic corresponding point in . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem5 38012* | is a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem6 38013 | is in the periodic partition, when the considered interval is centered at . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem7 38014* | The difference between a point and it's periodic image in the interval, is decreasing. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem8 38015 | A partition interval is a subset of the partitioned interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ | ||
Theorem | fourierdlem9 38016* | is a complex function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem10 38017 | Condition on the bounds of a non empty subinterval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem11 38018* | If there is a partition, than the lower bound is strictly less than the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ | ||
Theorem | fourierdlem12 38019* | A point of a partition is not an element of any open interval determined by the partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ ..^ | ||
Theorem | fourierdlem13 38020* | Value of in terms of value of . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ | ||
Theorem | fourierdlem14 38021* | Given the partition , is the partition shifted to the left by . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ ..^ | ||
Theorem | fourierdlem15 38022* | The range of the partition is between its starting point and its ending point. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ | ||
Theorem | fourierdlem16 38023* | The coefficients of the fourier series are integrable and reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem17 38024* | The defined is actually a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem18 38025* | The function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem19 38026* | If two elements of have the same periodic image in then they are equal. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem20 38027* | Every interval in the partition is included in an interval of the partition . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ ..^ ..^ | ||
Theorem | fourierdlem21 38028* | The coefficients of the fourier series are integrable and reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem22 38029* | The coefficients of the fourier series are integrable and reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem23 38030* | If is continuous and is constant, then is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem24 38031 | A sufficient condition for module being nonzero. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem25 38032* | If 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.) |
..^ ..^ | ||
Theorem | fourierdlem26 38033* | Periodic image of a point that's in the period that begins with the point . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem27 38034 | A partition open interval is a subset of the partitioned open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ | ||
Theorem | fourierdlem28 38035* | Derivative of . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem29 38036* | Explicit function value for applied to . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem30 38037* | Sum of three small pieces is less than ε. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem31 38038* | If is finite and for any element in there is a number such that a property holds for all numbers larger than , then there is a number such that the property holds for all numbers larger than and for all elements in . (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 29-Sep-2020.) |
inf | ||
Theorem | fourierdlem31OLD 38039* | If is finite and for any element in there is a number such that a property holds for all numbers larger than , then there is a number such that the property holds for all numbers larger than and for all elements in . (Contributed by Glauco Siliprandi, 11-Dec-2019.) Obsolete version of fourierdlem31 38038 as of 29-Sep-2020. ( (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | fourierdlem32 38040 | Limit of a continuous function on an open subinterval. Lower bound version. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
lim ℂ_{fld} ↾_{t} lim | ||
Theorem | fourierdlem33 38041 | Limit of a continuous function on an open subinterval. Upper bound version. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
lim ℂ_{fld} ↾_{t} lim | ||
Theorem | fourierdlem34 38042* | A partition is one to one. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ | ||
Theorem | fourierdlem35 38043 | There is a single point in that's distant from a multiple integer of . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem36 38044* | is an isomorphism. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem37 38045* | 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.) |
..^ ..^ ..^ ..^ ..^ | ||
Theorem | fourierdlem38 38046* | The function is continuous on every interval induced by the partition . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ ..^ | ||
Theorem | fourierdlem39 38047* | Integration by parts of (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem40 38048* | is a continuous function on any partition interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem41 38049* | Lemma used to prove that every real is a limit point for the domain of the derivative of the periodic function to be approximated. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ ..^ | ||
Theorem | fourierdlem42 38050* | The set of points in a moved partition are finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 29-Sep-2020.) |
inf ↾_{t} | ||
Theorem | fourierdlem42OLD 38051* | The set of points in a moved partition are finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.) Obsolete version of fourierdlem42 38050 as of 29-Sep-2020. ( (New usage is discouraged.) (Proof modification is discouraged.) |
↾_{t} | ||
Theorem | fourierdlem43 38052 | is a real function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem44 38053 | A condition for having non zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem46 38054* | The function has a limit at the bounds of every interval induced by the partition . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
lim lim ..^ lim lim | ||
Theorem | fourierdlem47 38055* | For large enough, the final expression is less than the given positive . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem48 38056* | The given periodic function has a right limit at every point in the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ ..^ ..^ lim ..^ lim | ||
Theorem | fourierdlem49 38057* | The given periodic function has a left limit at every point in the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ ..^ ..^ lim lim | ||
Theorem | fourierdlem50 38058* | Continuity of and its limits with respect to the partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ ..^ ..^ ..^ ..^ ..^ | ||
Theorem | fourierdlem51 38059* | is in the periodic partition, when the considered interval is centered at . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem52 38060* | d16:d17,d18:jca |- ( ph -> ( ( S 0 ) ) ) . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem53 38061* | The limit of at is the limit of at . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
lim lim | ||
Theorem | fourierdlem54 38062* | Given a partition and an arbitrary interval , a partition on is built such that it preserves any periodic function piecewise continuous on will be piecewise continuous on , with the same limits. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ ..^ | ||
Theorem | fourierdlem55 38063* | is a real function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem56 38064* | Derivative of the function on an interval non containing ' 0 '. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem57 38065* | The derivative of . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem58 38066* | The derivative of is continuous on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem59 38067* | The derivative of is continuous on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem60 38068* | Given a differentiable function , with finite limit of the derivative at the derived function has a limit at . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
lim lim lim | ||
Theorem | fourierdlem61 38069* | Given a differentiable function , with finite limit of the derivative at the derived function has a limit at . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
lim lim lim | ||
Theorem | fourierdlem62 38070 | The function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem63 38071* | The upper bound of intervals in the moved partition are mapped to points that are not greater than the corresponding upper bounds in the original partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ ..^ ..^ | ||
Theorem | fourierdlem64 38072* | The partition is finer than , when is moved on the same interval where lies. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ ..^ ..^ ..^ ..^ | ||
Theorem | fourierdlem65 38073* | The distance of two adjacent points in the moved partition is preserved in the original partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ ..^ ..^ | ||
Theorem | fourierdlem66 38074* | Value of the function when the argument is not zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem67 38075* | is a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem68 38076* | The derivative of is bounded on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | fourierdlem69 38077* | A piecewise continuous function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ ..^ ..^ lim ..^ lim | ||
Theorem | fourierdlem70 38078* | A piecewise continuous function is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ ..^ ..^ lim ..^ lim ..^ | ||
Theorem | fourierdlem71 38079* | A periodic piecewise continuous function, possibly undefined on a finite set in each periodic interval, is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ ..^ lim ..^ lim ..^ | ||
Theorem | fourierdlem72 38080* | The derivative of is continuous on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ ..^ ..^ | ||
Theorem | fourierdlem73 38081* | A version of the Riemann Lebesgue lemma: as increases, the integral in goes to zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
..^ ..^ ..^ lim ..^ lim ..^ | ||
Theorem | fourierdlem74 38082* | 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 | ||
Theorem | fourierdlem75 38083* | 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.) |