Home | Metamath
Proof Explorer Theorem List (p. 440 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fprodsubrecnncnvlem 43901* | The sequence π of finite products, where every factor is subtracted an "always smaller" amount, converges to the finite product of the factors. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ π = (π β β β¦ βπ β π΄ (π΅ β (1 / π))) & β’ πΉ = (π₯ β β β¦ βπ β π΄ (π΅ β π₯)) & β’ πΊ = (π β β β¦ (1 / π)) β β’ (π β π β βπ β π΄ π΅) | ||
Theorem | fprodsubrecnncnv 43902* | The sequence π of finite products, where every factor is subtracted an "always smaller" amount, converges to the finite product of the factors. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ (π β π β Fin) & β’ ((π β§ π β π) β π΄ β β) & β’ π = (π β β β¦ βπ β π (π΄ β (1 / π))) β β’ (π β π β βπ β π π΄) | ||
Theorem | fprodaddrecnncnvlem 43903* | The sequence π of finite products, where every factor is added an "always smaller" amount, converges to the finite product of the factors. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ π = (π β β β¦ βπ β π΄ (π΅ + (1 / π))) & β’ πΉ = (π₯ β β β¦ βπ β π΄ (π΅ + π₯)) & β’ πΊ = (π β β β¦ (1 / π)) β β’ (π β π β βπ β π΄ π΅) | ||
Theorem | fprodaddrecnncnv 43904* | The sequence π of finite products, where every factor is added an "always smaller" amount, converges to the finite product of the factors. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ (π β π β Fin) & β’ ((π β§ π β π) β π΄ β β) & β’ π = (π β β β¦ βπ β π (π΄ + (1 / π))) β β’ (π β π β βπ β π π΄) | ||
Theorem | dvsinexp 43905* | The derivative of sin^N . (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ (π β π β β) β β’ (π β (β D (π₯ β β β¦ ((sinβπ₯)βπ))) = (π₯ β β β¦ ((π Β· ((sinβπ₯)β(π β 1))) Β· (cosβπ₯)))) | ||
Theorem | dvcosre 43906 | The real derivative of the cosine. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ (β D (π₯ β β β¦ (cosβπ₯))) = (π₯ β β β¦ -(sinβπ₯)) | ||
Theorem | dvsinax 43907* | Derivative exercise: the derivative with respect to y of sin(Ay), given a constant π΄. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β β β (β D (π¦ β β β¦ (sinβ(π΄ Β· π¦)))) = (π¦ β β β¦ (π΄ Β· (cosβ(π΄ Β· π¦))))) | ||
Theorem | dvsubf 43908 | The subtraction rule for everywhere-differentiable functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:πβΆβ) & β’ (π β πΊ:πβΆβ) & β’ (π β dom (π D πΉ) = π) & β’ (π β dom (π D πΊ) = π) β β’ (π β (π D (πΉ βf β πΊ)) = ((π D πΉ) βf β (π D πΊ))) | ||
Theorem | dvmptconst 43909* | Function-builder for derivative: derivative of a constant. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β {β, β}) & β’ (π β π΄ β ((TopOpenββfld) βΎt π)) & β’ (π β π΅ β β) β β’ (π β (π D (π₯ β π΄ β¦ π΅)) = (π₯ β π΄ β¦ 0)) | ||
Theorem | dvcnre 43910 | From complex differentiation to real differentiation. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((πΉ:ββΆβ β§ β β dom (β D πΉ)) β (β D (πΉ βΎ β)) = ((β D πΉ) βΎ β)) | ||
Theorem | dvmptidg 43911* | Function-builder for derivative: derivative of the identity. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β {β, β}) & β’ (π β π΄ β ((TopOpenββfld) βΎt π)) β β’ (π β (π D (π₯ β π΄ β¦ π₯)) = (π₯ β π΄ β¦ 1)) | ||
Theorem | dvresntr 43912 | Function-builder for derivative: expand the function from an open set to its closure. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β β) & β’ (π β π β π) & β’ (π β πΉ:πβΆβ) & β’ π½ = (πΎ βΎt π) & β’ πΎ = (TopOpenββfld) & β’ (π β ((intβπ½)βπ) = π) β β’ (π β (π D πΉ) = (π D (πΉ βΎ π))) | ||
Theorem | fperdvper 43913* | The derivative of a periodic function is periodic. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ πΊ = (β D πΉ) β β’ ((π β§ π₯ β dom πΊ) β ((π₯ + π) β dom πΊ β§ (πΊβ(π₯ + π)) = (πΊβπ₯))) | ||
Theorem | dvasinbx 43914* | Derivative exercise: the derivative with respect to y of A x sin(By), given two constants π΄ and π΅. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ π΅ β β) β (β D (π¦ β β β¦ (π΄ Β· (sinβ(π΅ Β· π¦))))) = (π¦ β β β¦ ((π΄ Β· π΅) Β· (cosβ(π΅ Β· π¦))))) | ||
Theorem | dvresioo 43915 | Restriction of a derivative to an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ πΉ:π΄βΆβ) β (β D (πΉ βΎ (π΅(,)πΆ))) = ((β D πΉ) βΎ (π΅(,)πΆ))) | ||
Theorem | dvdivf 43916 | The quotient rule for everywhere-differentiable functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:πβΆβ) & β’ (π β πΊ:πβΆ(β β {0})) & β’ (π β dom (π D πΉ) = π) & β’ (π β dom (π D πΊ) = π) β β’ (π β (π D (πΉ βf / πΊ)) = ((((π D πΉ) βf Β· πΊ) βf β ((π D πΊ) βf Β· πΉ)) βf / (πΊ βf Β· πΊ))) | ||
Theorem | dvdivbd 43917* | A sufficient condition for the derivative to be bounded, for the quotient of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β {β, β}) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ (π β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ πΆ)) & β’ ((π β§ π₯ β π) β πΆ β β) & β’ ((π β§ π₯ β π) β π΅ β β) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β β) & β’ ((π β§ π₯ β π) β (absβπΆ) β€ π) & β’ ((π β§ π₯ β π) β (absβπ΅) β€ π ) & β’ ((π β§ π₯ β π) β (absβπ·) β€ π) & β’ ((π β§ π₯ β π) β (absβπ΄) β€ π) & β’ (π β (π D (π₯ β π β¦ π΅)) = (π₯ β π β¦ π·)) & β’ ((π β§ π₯ β π) β π· β β) & β’ (π β πΈ β β+) & β’ (π β βπ₯ β π πΈ β€ (absβπ΅)) & β’ πΉ = (π D (π₯ β π β¦ (π΄ / π΅))) β β’ (π β βπ β β βπ₯ β π (absβ(πΉβπ₯)) β€ π) | ||
Theorem | dvsubcncf 43918 | A sufficient condition for the derivative of a product to be continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:πβΆβ) & β’ (π β πΊ:πβΆβ) & β’ (π β (π D πΉ) β (πβcnββ)) & β’ (π β (π D πΊ) β (πβcnββ)) β β’ (π β (π D (πΉ βf β πΊ)) β (πβcnββ)) | ||
Theorem | dvmulcncf 43919 | A sufficient condition for the derivative of a product to be continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:πβΆβ) & β’ (π β πΊ:πβΆβ) & β’ (π β (π D πΉ) β (πβcnββ)) & β’ (π β (π D πΊ) β (πβcnββ)) β β’ (π β (π D (πΉ βf Β· πΊ)) β (πβcnββ)) | ||
Theorem | dvcosax 43920* | Derivative exercise: the derivative with respect to x of cos(Ax), given a constant π΄. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β β β (β D (π₯ β β β¦ (cosβ(π΄ Β· π₯)))) = (π₯ β β β¦ (π΄ Β· -(sinβ(π΄ Β· π₯))))) | ||
Theorem | dvdivcncf 43921 | A sufficient condition for the derivative of a quotient to be continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:πβΆβ) & β’ (π β πΊ:πβΆ(β β {0})) & β’ (π β (π D πΉ) β (πβcnββ)) & β’ (π β (π D πΊ) β (πβcnββ)) β β’ (π β (π D (πΉ βf / πΊ)) β (πβcnββ)) | ||
Theorem | dvbdfbdioolem1 43922* | Given a function with bounded derivative, on an open interval, here is an absolute bound to the difference of the image of two points in the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ:(π΄(,)π΅)βΆβ) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β πΎ β β) & β’ (π β βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ πΎ) & β’ (π β πΆ β (π΄(,)π΅)) & β’ (π β π· β (πΆ(,)π΅)) β β’ (π β ((absβ((πΉβπ·) β (πΉβπΆ))) β€ (πΎ Β· (π· β πΆ)) β§ (absβ((πΉβπ·) β (πΉβπΆ))) β€ (πΎ Β· (π΅ β π΄)))) | ||
Theorem | dvbdfbdioolem2 43923* | A function on an open interval, with bounded derivative, is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ:(π΄(,)π΅)βΆβ) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β πΎ β β) & β’ (π β βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ πΎ) & β’ π = ((absβ(πΉβ((π΄ + π΅) / 2))) + (πΎ Β· (π΅ β π΄))) β β’ (π β βπ₯ β (π΄(,)π΅)(absβ(πΉβπ₯)) β€ π) | ||
Theorem | dvbdfbdioo 43924* | A function on an open interval, with bounded derivative, is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ:(π΄(,)π΅)βΆβ) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β βπ β β βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π) β β’ (π β βπ β β βπ₯ β (π΄(,)π΅)(absβ(πΉβπ₯)) β€ π) | ||
Theorem | ioodvbdlimc1lem1 43925* | If πΉ has bounded derivative on (π΄(,)π΅) then a sequence of points in its image converges to its lim sup. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 3-Oct-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β βπ¦ β β βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π¦) & β’ (π β π β β€) & β’ (π β π :(β€β₯βπ)βΆ(π΄(,)π΅)) & β’ π = (π β (β€β₯βπ) β¦ (πΉβ(π βπ))) & β’ (π β π β dom β ) & β’ πΎ = inf({π β (β€β₯βπ) β£ βπ β (β€β₯βπ)(absβ((π βπ) β (π βπ))) < (π₯ / (sup(ran (π§ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ§))), β, < ) + 1))}, β, < ) β β’ (π β π β (lim supβπ)) | ||
Theorem | ioodvbdlimc1lem2 43926* | Limit at the lower bound of an open interval, for a function with bounded derivative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 3-Oct-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ:(π΄(,)π΅)βΆβ) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β βπ¦ β β βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π¦) & β’ π = sup(ran (π₯ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ₯))), β, < ) & β’ π = ((ββ(1 / (π΅ β π΄))) + 1) & β’ π = (π β (β€β₯βπ) β¦ (πΉβ(π΄ + (1 / π)))) & β’ π = (π β (β€β₯βπ) β¦ (π΄ + (1 / π))) & β’ π = if(π β€ ((ββ(π / (π₯ / 2))) + 1), ((ββ(π / (π₯ / 2))) + 1), π) & β’ (π β (((((π β§ π₯ β β+) β§ π β (β€β₯βπ)) β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2)) β§ π§ β (π΄(,)π΅)) β§ (absβ(π§ β π΄)) < (1 / π))) β β’ (π β (lim supβπ) β (πΉ limβ π΄)) | ||
Theorem | ioodvbdlimc1 43927* | A real function with bounded derivative, has a limit at the upper bound of an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Proof shortened by AV, 3-Oct-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ:(π΄(,)π΅)βΆβ) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β βπ¦ β β βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π¦) β β’ (π β (πΉ limβ π΄) β β ) | ||
Theorem | ioodvbdlimc2lem 43928* | Limit at the upper bound of an open interval, for a function with bounded derivative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 3-Oct-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ:(π΄(,)π΅)βΆβ) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β βπ¦ β β βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π¦) & β’ π = sup(ran (π₯ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ₯))), β, < ) & β’ π = ((ββ(1 / (π΅ β π΄))) + 1) & β’ π = (π β (β€β₯βπ) β¦ (πΉβ(π΅ β (1 / π)))) & β’ π = (π β (β€β₯βπ) β¦ (π΅ β (1 / π))) & β’ π = if(π β€ ((ββ(π / (π₯ / 2))) + 1), ((ββ(π / (π₯ / 2))) + 1), π) & β’ (π β (((((π β§ π₯ β β+) β§ π β (β€β₯βπ)) β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2)) β§ π§ β (π΄(,)π΅)) β§ (absβ(π§ β π΅)) < (1 / π))) β β’ (π β (lim supβπ) β (πΉ limβ π΅)) | ||
Theorem | ioodvbdlimc2 43929* | A real function with bounded derivative, has a limit at the upper bound of an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Proof shortened by AV, 3-Oct-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ:(π΄(,)π΅)βΆβ) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β βπ¦ β β βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π¦) β β’ (π β (πΉ limβ π΅) β β ) | ||
Theorem | dvdmsscn 43930 | π is a subset of β. This statement is very often used when computing derivatives. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) β β’ (π β π β β) | ||
Theorem | dvmptmulf 43931* | Function-builder for derivative, product rule. A version of dvmptmul 25247 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²π₯π & β’ (π β π β {β, β}) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ (π β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ ((π β§ π₯ β π) β πΆ β β) & β’ ((π β§ π₯ β π) β π· β π) & β’ (π β (π D (π₯ β π β¦ πΆ)) = (π₯ β π β¦ π·)) β β’ (π β (π D (π₯ β π β¦ (π΄ Β· πΆ))) = (π₯ β π β¦ ((π΅ Β· πΆ) + (π· Β· π΄)))) | ||
Theorem | dvnmptdivc 43932* | Function-builder for iterated derivative, division rule for constant divisor. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β π) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π β§ π β (0...π)) β π΅ β β) & β’ ((π β§ π β (0...π)) β ((π Dπ (π₯ β π β¦ π΄))βπ) = (π₯ β π β¦ π΅)) & β’ (π β πΆ β β) & β’ (π β πΆ β 0) & β’ (π β π β β0) β β’ ((π β§ π β (0...π)) β ((π Dπ (π₯ β π β¦ (π΄ / πΆ)))βπ) = (π₯ β π β¦ (π΅ / πΆ))) | ||
Theorem | dvdsn1add 43933 | If πΎ divides π but πΎ does not divide π, then πΎ does not divide (π + π). (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β ((Β¬ πΎ β₯ π β§ πΎ β₯ π) β Β¬ πΎ β₯ (π + π))) | ||
Theorem | dvxpaek 43934* | Derivative of the polynomial (π₯ + π΄)βπΎ. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π΄ β β) & β’ (π β πΎ β β) β β’ (π β (π D (π₯ β π β¦ ((π₯ + π΄)βπΎ))) = (π₯ β π β¦ (πΎ Β· ((π₯ + π΄)β(πΎ β 1))))) | ||
Theorem | dvnmptconst 43935* | The π-th derivative of a constant function. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π΄ β β) & β’ (π β π β β) β β’ (π β ((π Dπ (π₯ β π β¦ π΄))βπ) = (π₯ β π β¦ 0)) | ||
Theorem | dvnxpaek 43936* | The π-th derivative of the polynomial (π₯ + π΄)βπΎ. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π΄ β β) & β’ (π β πΎ β β0) & β’ πΉ = (π₯ β π β¦ ((π₯ + π΄)βπΎ)) β β’ ((π β§ π β β0) β ((π Dπ πΉ)βπ) = (π₯ β π β¦ if(πΎ < π, 0, (((!βπΎ) / (!β(πΎ β π))) Β· ((π₯ + π΄)β(πΎ β π)))))) | ||
Theorem | dvnmul 43937* | Function-builder for the π-th derivative, product rule. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β β) & β’ (π β π β β0) & β’ πΉ = (π₯ β π β¦ π΄) & β’ πΊ = (π₯ β π β¦ π΅) & β’ ((π β§ π β (0...π)) β ((π Dπ πΉ)βπ):πβΆβ) & β’ ((π β§ π β (0...π)) β ((π Dπ πΊ)βπ):πβΆβ) & β’ πΆ = (π β (0...π) β¦ ((π Dπ πΉ)βπ)) & β’ π· = (π β (0...π) β¦ ((π Dπ πΊ)βπ)) β β’ (π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) | ||
Theorem | dvmptfprodlem 43938* | Induction step for dvmptfprod 43939. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²π₯π & β’ β²ππ & β’ β²ππ & β’ β²ππΉ & β’ β²ππΊ & β’ ((π β§ π β πΌ β§ π₯ β π) β π΄ β β) & β’ (π β π· β Fin) & β’ (π β πΈ β V) & β’ (π β Β¬ πΈ β π·) & β’ (π β (π· βͺ {πΈ}) β πΌ) & β’ (π β π β {β, β}) & β’ (((π β§ π₯ β π) β§ π β π·) β πΆ β β) & β’ (π β (π D (π₯ β π β¦ βπ β π· π΄)) = (π₯ β π β¦ Ξ£π β π· (πΆ Β· βπ β (π· β {π})π΄))) & β’ ((π β§ π₯ β π) β πΊ β β) & β’ (π β (π D (π₯ β π β¦ πΉ)) = (π₯ β π β¦ πΊ)) & β’ (π = πΈ β π΄ = πΉ) & β’ (π = πΈ β πΆ = πΊ) β β’ (π β (π D (π₯ β π β¦ βπ β (π· βͺ {πΈ})π΄)) = (π₯ β π β¦ Ξ£π β (π· βͺ {πΈ})(πΆ Β· βπ β ((π· βͺ {πΈ}) β {π})π΄))) | ||
Theorem | dvmptfprod 43939* | Function-builder for derivative, finite product rule. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ β²ππ & β’ π½ = (πΎ βΎt π) & β’ πΎ = (TopOpenββfld) & β’ (π β π β {β, β}) & β’ (π β π β π½) & β’ (π β πΌ β Fin) & β’ ((π β§ π β πΌ β§ π₯ β π) β π΄ β β) & β’ ((π β§ π β πΌ β§ π₯ β π) β π΅ β β) & β’ ((π β§ π β πΌ) β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π = π β π΅ = πΆ) β β’ (π β (π D (π₯ β π β¦ βπ β πΌ π΄)) = (π₯ β π β¦ Ξ£π β πΌ (πΆ Β· βπ β (πΌ β {π})π΄))) | ||
Theorem | dvnprodlem1 43940* | π· is bijective. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ πΆ = (π β π« π β¦ (π β β0 β¦ {π β ((0...π) βm π ) β£ Ξ£π‘ β π (πβπ‘) = π})) & β’ (π β π½ β β0) & β’ π· = (π β ((πΆβ(π βͺ {π}))βπ½) β¦ β¨(π½ β (πβπ)), (π βΎ π )β©) & β’ (π β π β Fin) & β’ (π β π β π) & β’ (π β Β¬ π β π ) & β’ (π β (π βͺ {π}) β π) β β’ (π β π·:((πΆβ(π βͺ {π}))βπ½)β1-1-ontoββͺ π β (0...π½)({π} Γ ((πΆβπ )βπ))) | ||
Theorem | dvnprodlem2 43941* | Induction step for dvnprodlem2 43941. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π β Fin) & β’ ((π β§ π‘ β π) β (π»βπ‘):πβΆβ) & β’ (π β π β β0) & β’ ((π β§ π‘ β π β§ π β (0...π)) β ((π Dπ (π»βπ‘))βπ):πβΆβ) & β’ πΆ = (π β π« π β¦ (π β β0 β¦ {π β ((0...π) βm π ) β£ Ξ£π‘ β π (πβπ‘) = π})) & β’ (π β π β π) & β’ (π β π β (π β π )) & β’ (π β βπ β (0...π)((π Dπ (π₯ β π β¦ βπ‘ β π ((π»βπ‘)βπ₯)))βπ) = (π₯ β π β¦ Ξ£π β ((πΆβπ )βπ)(((!βπ) / βπ‘ β π (!β(πβπ‘))) Β· βπ‘ β π (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))) & β’ (π β π½ β (0...π)) & β’ π· = (π β ((πΆβ(π βͺ {π}))βπ½) β¦ β¨(π½ β (πβπ)), (π βΎ π )β©) β β’ (π β ((π Dπ (π₯ β π β¦ βπ‘ β (π βͺ {π})((π»βπ‘)βπ₯)))βπ½) = (π₯ β π β¦ Ξ£π β ((πΆβ(π βͺ {π}))βπ½)(((!βπ½) / βπ‘ β (π βͺ {π})(!β(πβπ‘))) Β· βπ‘ β (π βͺ {π})(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))) | ||
Theorem | dvnprodlem3 43942* | The multinomial formula for the π-th derivative of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π β Fin) & β’ ((π β§ π‘ β π) β (π»βπ‘):πβΆβ) & β’ (π β π β β0) & β’ ((π β§ π‘ β π β§ π β (0...π)) β ((π Dπ (π»βπ‘))βπ):πβΆβ) & β’ πΉ = (π₯ β π β¦ βπ‘ β π ((π»βπ‘)βπ₯)) & β’ π· = (π β π« π β¦ (π β β0 β¦ {π β ((0...π) βm π ) β£ Ξ£π‘ β π (πβπ‘) = π})) & β’ πΆ = (π β β0 β¦ {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π}) β β’ (π β ((π Dπ πΉ)βπ) = (π₯ β π β¦ Ξ£π β (πΆβπ)(((!βπ) / βπ‘ β π (!β(πβπ‘))) Β· βπ‘ β π (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))) | ||
Theorem | dvnprod 43943* | The multinomial formula for the π-th derivative of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π β Fin) & β’ ((π β§ π‘ β π) β (π»βπ‘):πβΆβ) & β’ (π β π β β0) & β’ ((π β§ π‘ β π β§ π β (0...π)) β ((π Dπ (π»βπ‘))βπ):πβΆβ) & β’ πΉ = (π₯ β π β¦ βπ‘ β π ((π»βπ‘)βπ₯)) & β’ πΆ = (π β β0 β¦ {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π}) β β’ (π β ((π Dπ πΉ)βπ) = (π₯ β π β¦ Ξ£π β (πΆβπ)(((!βπ) / βπ‘ β π (!β(πβπ‘))) Β· βπ‘ β π (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))) | ||
Theorem | itgsin0pilem1 43944* | Calculation of the integral for sine on the (0,Ο) interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ πΆ = (π‘ β (0[,]Ο) β¦ -(cosβπ‘)) β β’ β«(0(,)Ο)(sinβπ₯) dπ₯ = 2 | ||
Theorem | ibliccsinexp 43945* | sin^n on a closed interval is integrable. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ ((π΄ β β β§ π΅ β β β§ π β β0) β (π₯ β (π΄[,]π΅) β¦ ((sinβπ₯)βπ)) β πΏ1) | ||
Theorem | itgsin0pi 43946 | Calculation of the integral for sine on the (0,Ο) interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β«(0(,)Ο)(sinβπ₯) dπ₯ = 2 | ||
Theorem | iblioosinexp 43947* | sin^n on an open integral is integrable. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ ((π΄ β β β§ π΅ β β β§ π β β0) β (π₯ β (π΄(,)π΅) β¦ ((sinβπ₯)βπ)) β πΏ1) | ||
Theorem | itgsinexplem1 43948* | Integration by parts is applied to integrate sin^(N+1). (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ πΉ = (π₯ β β β¦ ((sinβπ₯)βπ)) & β’ πΊ = (π₯ β β β¦ -(cosβπ₯)) & β’ π» = (π₯ β β β¦ ((π Β· ((sinβπ₯)β(π β 1))) Β· (cosβπ₯))) & β’ πΌ = (π₯ β β β¦ (((sinβπ₯)βπ) Β· (sinβπ₯))) & β’ πΏ = (π₯ β β β¦ (((π Β· ((sinβπ₯)β(π β 1))) Β· (cosβπ₯)) Β· -(cosβπ₯))) & β’ π = (π₯ β β β¦ (((cosβπ₯)β2) Β· ((sinβπ₯)β(π β 1)))) & β’ (π β π β β) β β’ (π β β«(0(,)Ο)(((sinβπ₯)βπ) Β· (sinβπ₯)) dπ₯ = (π Β· β«(0(,)Ο)(((cosβπ₯)β2) Β· ((sinβπ₯)β(π β 1))) dπ₯)) | ||
Theorem | itgsinexp 43949* | A recursive formula for the integral of sin^N on the interval (0,Ο) . (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ πΌ = (π β β0 β¦ β«(0(,)Ο)((sinβπ₯)βπ) dπ₯) & β’ (π β π β (β€β₯β2)) β β’ (π β (πΌβπ) = (((π β 1) / π) Β· (πΌβ(π β 2)))) | ||
Theorem | iblconstmpt 43950* | A constant function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β dom vol β§ (volβπ΄) β β β§ π΅ β β) β (π₯ β π΄ β¦ π΅) β πΏ1) | ||
Theorem | itgeq1d 43951* | Equality theorem for an integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ = π΅) β β’ (π β β«π΄πΆ dπ₯ = β«π΅πΆ dπ₯) | ||
Theorem | mbfres2cn 43952 | Measurability of a piecewise function: if πΉ is measurable on subsets π΅ and πΆ of its domain, and these pieces make up all of π΄, then πΉ is measurable on the whole domain. Similar to mbfres2 24931 but here the theorem is extended to complex-valued functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β (πΉ βΎ π΅) β MblFn) & β’ (π β (πΉ βΎ πΆ) β MblFn) & β’ (π β (π΅ βͺ πΆ) = π΄) β β’ (π β πΉ β MblFn) | ||
Theorem | vol0 43953 | The measure of the empty set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (volββ ) = 0 | ||
Theorem | ditgeqiooicc 43954* | A function πΉ on an open interval, has the same directed integral as its extension πΊ on the closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π , if(π₯ = π΅, πΏ, (πΉβπ₯)))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β πΉ:(π΄(,)π΅)βΆβ) β β’ (π β β¨[π΄ β π΅](πΉβπ₯) dπ₯ = β¨[π΄ β π΅](πΊβπ₯) dπ₯) | ||
Theorem | volge0 43955 | The volume of a set is always nonnegative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β dom vol β 0 β€ (volβπ΄)) | ||
Theorem | cnbdibl 43956* | A continuous bounded function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β dom vol) & β’ (π β (volβπ΄) β β) & β’ (π β πΉ β (π΄βcnββ)) & β’ (π β βπ₯ β β βπ¦ β dom πΉ(absβ(πΉβπ¦)) β€ π₯) β β’ (π β πΉ β πΏ1) | ||
Theorem | snmbl 43957 | A singleton is measurable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β β β {π΄} β dom vol) | ||
Theorem | ditgeq3d 43958* | Equality theorem for the directed integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β€ π΅) & β’ ((π β§ π₯ β (π΄(,)π΅)) β π· = πΈ) β β’ (π β β¨[π΄ β π΅]π· dπ₯ = β¨[π΄ β π΅]πΈ dπ₯) | ||
Theorem | iblempty 43959 | The empty function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β β πΏ1 | ||
Theorem | iblsplit 43960* | The union of two integrable functions is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β (vol*β(π΄ β© π΅)) = 0) & β’ (π β π = (π΄ βͺ π΅)) & β’ ((π β§ π₯ β π) β πΆ β β) & β’ (π β (π₯ β π΄ β¦ πΆ) β πΏ1) & β’ (π β (π₯ β π΅ β¦ πΆ) β πΏ1) β β’ (π β (π₯ β π β¦ πΆ) β πΏ1) | ||
Theorem | volsn 43961 | A singleton has 0 Lebesgue measure. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β β β (volβ{π΄}) = 0) | ||
Theorem | itgvol0 43962* | If the domani is negligible, the function is integrable and the integral is 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β (vol*βπ΄) = 0) & β’ ((π β§ π₯ β π΄) β π΅ β β) β β’ (π β ((π₯ β π΄ β¦ π΅) β πΏ1 β§ β«π΄π΅ dπ₯ = 0)) | ||
Theorem | itgcoscmulx 43963* | Exercise: the integral of π₯ β¦ cosππ₯ on an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΅ β€ πΆ) & β’ (π β π΄ β 0) β β’ (π β β«(π΅(,)πΆ)(cosβ(π΄ Β· π₯)) dπ₯ = (((sinβ(π΄ Β· πΆ)) β (sinβ(π΄ Β· π΅))) / π΄)) | ||
Theorem | iblsplitf 43964* | A version of iblsplit 43960 using bound-variable hypotheses instead of distinct variable conditions". (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β²π₯π & β’ (π β (vol*β(π΄ β© π΅)) = 0) & β’ (π β π = (π΄ βͺ π΅)) & β’ ((π β§ π₯ β π) β πΆ β β) & β’ (π β (π₯ β π΄ β¦ πΆ) β πΏ1) & β’ (π β (π₯ β π΅ β¦ πΆ) β πΏ1) β β’ (π β (π₯ β π β¦ πΆ) β πΏ1) | ||
Theorem | ibliooicc 43965* | If a function is integrable on an open interval, it is integrable on the corresponding closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (π₯ β (π΄(,)π΅) β¦ πΆ) β πΏ1) & β’ ((π β§ π₯ β (π΄[,]π΅)) β πΆ β β) β β’ (π β (π₯ β (π΄[,]π΅) β¦ πΆ) β πΏ1) | ||
Theorem | volioc 43966 | The measure of a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ π΅ β β β§ π΄ β€ π΅) β (volβ(π΄(,]π΅)) = (π΅ β π΄)) | ||
Theorem | iblspltprt 43967* | If a function is integrable on any interval of a partition, then it is integrable on the whole interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β²π‘π & β’ (π β π β β€) & β’ (π β π β (β€β₯β(π + 1))) & β’ ((π β§ π β (π...π)) β (πβπ) β β) & β’ ((π β§ π β (π..^π)) β (πβπ) < (πβ(π + 1))) & β’ ((π β§ π‘ β ((πβπ)[,](πβπ))) β π΄ β β) & β’ ((π β§ π β (π..^π)) β (π‘ β ((πβπ)[,](πβ(π + 1))) β¦ π΄) β πΏ1) β β’ (π β (π‘ β ((πβπ)[,](πβπ)) β¦ π΄) β πΏ1) | ||
Theorem | itgsincmulx 43968* | Exercise: the integral of π₯ β¦ sinππ₯ on an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΄ β 0) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΅ β€ πΆ) β β’ (π β β«(π΅(,)πΆ)(sinβ(π΄ Β· π₯)) dπ₯ = (((cosβ(π΄ Β· π΅)) β (cosβ(π΄ Β· πΆ))) / π΄)) | ||
Theorem | itgsubsticclem 43969* | lemma for itgsubsticc 43970. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ = (π’ β (πΎ[,]πΏ) β¦ πΆ) & β’ πΊ = (π’ β β β¦ if(π’ β (πΎ[,]πΏ), (πΉβπ’), if(π’ < πΎ, (πΉβπΎ), (πΉβπΏ)))) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β€ π) & β’ (π β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnβ(πΎ[,]πΏ))) & β’ (π β (π₯ β (π(,)π) β¦ π΅) β (((π(,)π)βcnββ) β© πΏ1)) & β’ (π β πΉ β ((πΎ[,]πΏ)βcnββ)) & β’ (π β πΎ β β) & β’ (π β πΏ β β) & β’ (π β πΎ β€ πΏ) & β’ (π β (β D (π₯ β (π[,]π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) & β’ (π’ = π΄ β πΆ = πΈ) & β’ (π₯ = π β π΄ = πΎ) & β’ (π₯ = π β π΄ = πΏ) β β’ (π β β¨[πΎ β πΏ]πΆ dπ’ = β¨[π β π](πΈ Β· π΅) dπ₯) | ||
Theorem | itgsubsticc 43970* | Integration by u-substitution. The main difference with respect to itgsubst 25335 is that here we consider the range of π΄(π₯) to be in the closed interval (πΎ[,]πΏ). If π΄(π₯) is a continuous, differentiable function from [π, π] to (π, π), whose derivative is continuous and integrable, and πΆ(π’) is a continuous function on (π, π), then the integral of πΆ(π’) from πΎ = π΄(π) to πΏ = π΄(π) is equal to the integral of πΆ(π΄(π₯)) D π΄(π₯) from π to π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β€ π) & β’ (π β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnβ(πΎ[,]πΏ))) & β’ (π β (π’ β (πΎ[,]πΏ) β¦ πΆ) β ((πΎ[,]πΏ)βcnββ)) & β’ (π β (π₯ β (π(,)π) β¦ π΅) β (((π(,)π)βcnββ) β© πΏ1)) & β’ (π β (β D (π₯ β (π[,]π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) & β’ (π’ = π΄ β πΆ = πΈ) & β’ (π₯ = π β π΄ = πΎ) & β’ (π₯ = π β π΄ = πΏ) & β’ (π β πΎ β β) & β’ (π β πΏ β β) β β’ (π β β¨[πΎ β πΏ]πΆ dπ’ = β¨[π β π](πΈ Β· π΅) dπ₯) | ||
Theorem | itgioocnicc 43971* | The integral of a piecewise continuous function πΉ on an open interval is equal to the integral of the continuous function πΊ, in the corresponding closed interval. πΊ is equal to πΉ on the open interval, but it is continuous at the two boundaries, also. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ:dom πΉβΆβ) & β’ (π β (πΉ βΎ (π΄(,)π΅)) β ((π΄(,)π΅)βcnββ)) & β’ (π β (π΄[,]π΅) β dom πΉ) & β’ (π β π β ((πΉ βΎ (π΄(,)π΅)) limβ π΄)) & β’ (π β πΏ β ((πΉ βΎ (π΄(,)π΅)) limβ π΅)) & β’ πΊ = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π , if(π₯ = π΅, πΏ, (πΉβπ₯)))) β β’ (π β (πΊ β πΏ1 β§ β«(π΄[,]π΅)(πΊβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯)) | ||
Theorem | iblcncfioo 43972 | A continuous function πΉ on an open interval (π΄(,)π΅) with a finite right limit π in π΄ and a finite left limit πΏ in π΅ is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β πΏ β (πΉ limβ π΅)) & β’ (π β π β (πΉ limβ π΄)) β β’ (π β πΉ β πΏ1) | ||
Theorem | itgspltprt 43973* | The β« integral splits on a given partition π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β β€) & β’ (π β π β (β€β₯β(π + 1))) & β’ (π β π:(π...π)βΆβ) & β’ ((π β§ π β (π..^π)) β (πβπ) < (πβ(π + 1))) & β’ ((π β§ π‘ β ((πβπ)[,](πβπ))) β π΄ β β) & β’ ((π β§ π β (π..^π)) β (π‘ β ((πβπ)[,](πβ(π + 1))) β¦ π΄) β πΏ1) β β’ (π β β«((πβπ)[,](πβπ))π΄ dπ‘ = Ξ£π β (π..^π)β«((πβπ)[,](πβ(π + 1)))π΄ dπ‘) | ||
Theorem | itgiccshift 43974* | The integral of a function, πΉ stays the same if its closed interval domain is shifted by π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) & β’ (π β π β β+) & β’ πΊ = (π₯ β ((π΄ + π)[,](π΅ + π)) β¦ (πΉβ(π₯ β π))) β β’ (π β β«((π΄ + π)[,](π΅ + π))(πΊβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) | ||
Theorem | itgperiod 43975* | The integral of a periodic function, with period π stays the same if the domain of integration is shifted. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β π β β+) & β’ (π β πΉ:ββΆβ) & β’ ((π β§ π₯ β (π΄[,]π΅)) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ (π β (πΉ βΎ (π΄[,]π΅)) β ((π΄[,]π΅)βcnββ)) β β’ (π β β«((π΄ + π)[,](π΅ + π))(πΉβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) | ||
Theorem | itgsbtaddcnst 43976* | Integral substitution, adding a constant to the function's argument. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β π β β) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) β β’ (π β β¨[(π΄ β π) β (π΅ β π)](πΉβ(π + π )) dπ = β¨[π΄ β π΅](πΉβπ‘) dπ‘) | ||
Theorem | volico 43977 | The measure of left-closed, right-open interval. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ ((π΄ β β β§ π΅ β β) β (volβ(π΄[,)π΅)) = if(π΄ < π΅, (π΅ β π΄), 0)) | ||
Theorem | sublevolico 43978 | The Lebesgue measure of a left-closed, right-open interval is greater than or equal to the difference of the two bounds. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (π΅ β π΄) β€ (volβ(π΄[,)π΅))) | ||
Theorem | dmvolss 43979 | Lebesgue measurable sets are subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ dom vol β π« β | ||
Theorem | ismbl3 43980* | The predicate "π΄ is Lebesgue-measurable". Similar to ismbl2 24813, but here +π is used, and the precondition (vol*βπ₯) β β can be dropped. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π΄ β dom vol β (π΄ β β β§ βπ₯ β π« β((vol*β(π₯ β© π΄)) +π (vol*β(π₯ β π΄))) β€ (vol*βπ₯))) | ||
Theorem | volioof 43981 | The function that assigns the Lebesgue measure to open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (vol β (,)):(β* Γ β*)βΆ(0[,]+β) | ||
Theorem | ovolsplit 43982 | The Lebesgue outer measure function is finitely sub-additive: application to a set split in two parts, using addition for extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β) β β’ (π β (vol*βπ΄) β€ ((vol*β(π΄ β© π΅)) +π (vol*β(π΄ β π΅)))) | ||
Theorem | fvvolioof 43983 | The function value of the Lebesgue measure of an open interval composed with a function. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β πΉ:π΄βΆ(β* Γ β*)) & β’ (π β π β π΄) β β’ (π β (((vol β (,)) β πΉ)βπ) = (volβ((1st β(πΉβπ))(,)(2nd β(πΉβπ))))) | ||
Theorem | volioore 43984 | The measure of an open interval. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ ((π΄ β β β§ π΅ β β) β (volβ(π΄(,)π΅)) = if(π΄ β€ π΅, (π΅ β π΄), 0)) | ||
Theorem | fvvolicof 43985 | The function value of the Lebesgue measure of a left-closed right-open interval composed with a function. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β πΉ:π΄βΆ(β* Γ β*)) & β’ (π β π β π΄) β β’ (π β (((vol β [,)) β πΉ)βπ) = (volβ((1st β(πΉβπ))[,)(2nd β(πΉβπ))))) | ||
Theorem | voliooico 43986 | An open interval and a left-closed, right-open interval with the same real bounds, have the same Lebesgue measure. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (volβ(π΄(,)π΅)) = (volβ(π΄[,)π΅))) | ||
Theorem | ismbl4 43987* | The predicate "π΄ is Lebesgue-measurable". Similar to ismbl 24812, but here +π is used, and the precondition (vol*βπ₯) β β can be dropped. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π΄ β dom vol β (π΄ β β β§ βπ₯ β π« β(vol*βπ₯) = ((vol*β(π₯ β© π΄)) +π (vol*β(π₯ β π΄))))) | ||
Theorem | volioofmpt 43988* | ((vol β (,)) β πΉ) expressed in maps-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ β²π₯πΉ & β’ (π β πΉ:π΄βΆ(β* Γ β*)) β β’ (π β ((vol β (,)) β πΉ) = (π₯ β π΄ β¦ (volβ((1st β(πΉβπ₯))(,)(2nd β(πΉβπ₯)))))) | ||
Theorem | volicoff 43989 | ((vol β [,)) β πΉ) expressed in maps-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β πΉ:π΄βΆ(β Γ β*)) β β’ (π β ((vol β [,)) β πΉ):π΄βΆ(0[,]+β)) | ||
Theorem | voliooicof 43990 | The Lebesgue measure of open intervals is the same as the Lebesgue measure of left-closed right-open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β πΉ:π΄βΆ(β Γ β)) β β’ (π β ((vol β (,)) β πΉ) = ((vol β [,)) β πΉ)) | ||
Theorem | volicofmpt 43991* | ((vol β [,)) β πΉ) expressed in maps-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ β²π₯πΉ & β’ (π β πΉ:π΄βΆ(β Γ β*)) β β’ (π β ((vol β [,)) β πΉ) = (π₯ β π΄ β¦ (volβ((1st β(πΉβπ₯))[,)(2nd β(πΉβπ₯)))))) | ||
Theorem | volicc 43992 | The Lebesgue measure of a closed interval. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ ((π΄ β β β§ π΅ β β β§ π΄ β€ π΅) β (volβ(π΄[,]π΅)) = (π΅ β π΄)) | ||
Theorem | voliccico 43993 | A closed interval and a left-closed, right-open interval with the same real bounds, have the same Lebesgue measure. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (volβ(π΄[,]π΅)) = (volβ(π΄[,)π΅))) | ||
Theorem | mbfdmssre 43994 | The domain of a measurable function is a subset of the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (πΉ β MblFn β dom πΉ β β) | ||
Theorem | stoweidlem1 43995 | Lemma for stoweid 44057. This lemma is used by Lemma 1 in [BrosowskiDeutsh] p. 90; the key step uses Bernoulli's inequality bernneq 14057. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ (π β π β β) & β’ (π β πΎ β β) & β’ (π β π· β β+) & β’ (π β π΄ β β+) & β’ (π β 0 β€ π΄) & β’ (π β π΄ β€ 1) & β’ (π β π· β€ π΄) β β’ (π β ((1 β (π΄βπ))β(πΎβπ)) β€ (1 / ((πΎ Β· π·)βπ))) | ||
Theorem | stoweidlem2 43996* | lemma for stoweid 44057: here we prove that the subalgebra of continuous functions, which contains constant functions, is closed under scaling. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ ((π β§ π β π΄) β π:πβΆβ) & β’ (π β πΈ β β) & β’ (π β πΉ β π΄) β β’ (π β (π‘ β π β¦ (πΈ Β· (πΉβπ‘))) β π΄) | ||
Theorem | stoweidlem3 43997* | Lemma for stoweid 44057: if π΄ is positive and all π terms of a finite product are larger than π΄, then the finite product is larger than π΄βπ. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππΉ & β’ β²ππ & β’ π = seq1( Β· , πΉ) & β’ (π β π β β) & β’ (π β πΉ:(1...π)βΆβ) & β’ ((π β§ π β (1...π)) β π΄ < (πΉβπ)) & β’ (π β π΄ β β+) β β’ (π β (π΄βπ) < (πβπ)) | ||
Theorem | stoweidlem4 43998* | Lemma for stoweid 44057: a class variable replaces a setvar variable, for constant functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) β β’ ((π β§ π΅ β β) β (π‘ β π β¦ π΅) β π΄) | ||
Theorem | stoweidlem5 43999* | There exists a Ξ΄ as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 90: 0 < Ξ΄ < 1 , p >= Ξ΄ on π β π. Here π· is used to represent Ξ΄ in the paper and π to represent π β π in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ π· = if(πΆ β€ (1 / 2), πΆ, (1 / 2)) & β’ (π β π:πβΆβ) & β’ (π β π β π) & β’ (π β πΆ β β+) & β’ (π β βπ‘ β π πΆ β€ (πβπ‘)) β β’ (π β βπ(π β β+ β§ π < 1 β§ βπ‘ β π π β€ (πβπ‘))) | ||
Theorem | stoweidlem6 44000* | Lemma for stoweid 44057: two class variables replace two setvar variables, for multiplication of two functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘ π = πΉ & β’ β²π‘ π = πΊ & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) β β’ ((π β§ πΉ β π΄ β§ πΊ β π΄) β (π‘ β π β¦ ((πΉβπ‘) Β· (πΊβπ‘))) β π΄) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |