Home | Metamath
Proof Explorer Theorem List (p. 441 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | stoweidlem50 44001* | This lemma proves that sets U(t) as defined in Lemma 1 of [BrosowskiDeutsh] p. 90, contain a finite subcover of T \ U. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} & β’ π = {π€ β π½ β£ ββ β π π€ = {π‘ β π β£ 0 < (ββπ‘)}} & β’ π = βͺ π½ & β’ πΆ = (π½ Cn πΎ) & β’ (π β π½ β Comp) & β’ (π β π΄ β πΆ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) & β’ (π β π β π½) & β’ (π β π β π) β β’ (π β βπ’(π’ β Fin β§ π’ β π β§ (π β π) β βͺ π’)) | ||
Theorem | stoweidlem51 44002* | There exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91. Here π· is used to represent π΄ in the paper, because here π΄ is used for the subalgebra of functions. πΈ is used to represent Ξ΅ in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππ & β’ β²π‘π & β’ β²π€π & β’ β²π€π & β’ π = {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} & β’ π = (π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) & β’ π = (seq1(π, π)βπ) & β’ πΉ = (π‘ β π β¦ (π β (1...π) β¦ ((πβπ)βπ‘))) & β’ π = (π‘ β π β¦ (seq1( Β· , (πΉβπ‘))βπ)) & β’ (π β π β β) & β’ (π β π:(1...π)βΆπ) & β’ (π β π:(1...π)βΆπ) & β’ ((π β§ π€ β π) β π€ β π) & β’ (π β π· β βͺ ran π) & β’ (π β π· β π) & β’ (π β π΅ β π) & β’ ((π β§ π β (1...π)) β βπ‘ β (πβπ)((πβπ)βπ‘) < (πΈ / π)) & β’ ((π β§ π β (1...π)) β βπ‘ β π΅ (1 β (πΈ / π)) < ((πβπ)βπ‘)) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π β π΄) β π:πβΆβ) & β’ (π β π β V) & β’ (π β πΈ β β+) & β’ (π β πΈ < (1 / 3)) β β’ (π β βπ₯(π₯ β π΄ β§ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘)))) | ||
Theorem | stoweidlem52 44003* | There exists a neighborhood V as in Lemma 1 of [BrosowskiDeutsh] p. 90. Here Z is used to represent t0 in the paper, and v is used to represent V in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ β²π‘π & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ π = {π‘ β π β£ (πβπ‘) < (π· / 2)} & β’ π = βͺ π½ & β’ πΆ = (π½ Cn πΎ) & β’ (π β π΄ β πΆ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π β β) β (π‘ β π β¦ π) β π΄) & β’ (π β π· β β+) & β’ (π β π· < 1) & β’ (π β π β π½) & β’ (π β π β π) & β’ (π β π β π΄) & β’ (π β βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1)) & β’ (π β (πβπ) = 0) & β’ (π β βπ‘ β (π β π)π· β€ (πβπ‘)) β β’ (π β βπ£ β π½ ((π β π£ β§ π£ β π) β§ βπ β β+ βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π£ (π₯βπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (π₯βπ‘)))) | ||
Theorem | stoweidlem53 44004* | This lemma is used to prove the existence of a function π as in Lemma 1 of [BrosowskiDeutsh] p. 90: π is in the subalgebra, such that 0 β€ π β€ 1, p_(t0) = 0, and 0 < π on π β π. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} & β’ π = {π€ β π½ β£ ββ β π π€ = {π‘ β π β£ 0 < (ββπ‘)}} & β’ π = βͺ π½ & β’ πΆ = (π½ Cn πΎ) & β’ (π β π½ β Comp) & β’ (π β π΄ β πΆ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) & β’ (π β π β π½) & β’ (π β (π β π) β β ) & β’ (π β π β π) β β’ (π β βπ β π΄ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ (πβπ) = 0 β§ βπ‘ β (π β π)0 < (πβπ‘))) | ||
Theorem | stoweidlem54 44005* | There exists a function π₯ as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91. Here π· is used to represent π΄ in the paper, because here π΄ is used for the subalgebra of functions. πΈ is used to represent Ξ΅ in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππ & β’ β²π‘π & β’ β²π¦π & β’ β²π€π & β’ π = βͺ π½ & β’ π = {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} & β’ π = (π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) & β’ πΉ = (π‘ β π β¦ (π β (1...π) β¦ ((π¦βπ)βπ‘))) & β’ π = (π‘ β π β¦ (seq1( Β· , (πΉβπ‘))βπ)) & β’ π = {π€ β π½ β£ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘))} & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π β π΄) β π:πβΆβ) & β’ (π β π β β) & β’ (π β π:(1...π)βΆπ) & β’ (π β π΅ β π) & β’ (π β π· β βͺ ran π) & β’ (π β π· β π) & β’ (π β βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) & β’ (π β π β V) & β’ (π β πΈ β β+) & β’ (π β πΈ < (1 / 3)) β β’ (π β βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘))) | ||
Theorem | stoweidlem55 44006* | This lemma proves the existence of a function p as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_(t0) = 0, and p > 0 on T - U. Here Z is used to represent t0 in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ (π β π½ β Comp) & β’ π = βͺ π½ & β’ πΆ = (π½ Cn πΎ) & β’ (π β π΄ β πΆ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) & β’ (π β π β π½) & β’ (π β π β π) & β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} & β’ π = {π€ β π½ β£ ββ β π π€ = {π‘ β π β£ 0 < (ββπ‘)}} β β’ (π β βπ β π΄ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ (πβπ) = 0 β§ βπ‘ β (π β π)0 < (πβπ‘))) | ||
Theorem | stoweidlem56 44007* | This theorem proves Lemma 1 in [BrosowskiDeutsh] p. 90. Here π is used to represent t0 in the paper, π£ is used to represent π in the paper, and π is used to represent Ξ΅. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ (π β π½ β Comp) & β’ π = βͺ π½ & β’ πΆ = (π½ Cn πΎ) & β’ (π β π΄ β πΆ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π¦ β β) β (π‘ β π β¦ π¦) β π΄) & β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) & β’ (π β π β π½) & β’ (π β π β π) β β’ (π β βπ£ β π½ ((π β π£ β§ π£ β π) β§ βπ β β+ βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π£ (π₯βπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (π₯βπ‘)))) | ||
Theorem | stoweidlem57 44008* | There exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91. In this theorem, it is proven the non-trivial case (the closed set D is nonempty). Here D is used to represent A in the paper, because the variable A is used for the subalgebra of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π· & β’ β²π‘π & β’ β²π‘π & β’ π = {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} & β’ π = {π€ β π½ β£ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘))} & β’ πΎ = (topGenβran (,)) & β’ π = βͺ π½ & β’ πΆ = (π½ Cn πΎ) & β’ π = (π β π΅) & β’ (π β π½ β Comp) & β’ (π β π΄ β πΆ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π β β) β (π‘ β π β¦ π) β π΄) & β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) & β’ (π β π΅ β (Clsdβπ½)) & β’ (π β π· β (Clsdβπ½)) & β’ (π β (π΅ β© π·) = β ) & β’ (π β π· β β ) & β’ (π β πΈ β β+) & β’ (π β πΈ < (1 / 3)) β β’ (π β βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘))) | ||
Theorem | stoweidlem58 44009* | This theorem proves Lemma 2 in [BrosowskiDeutsh] p. 91. Here D is used to represent the set A of Lemma 2, because here the variable A is used for the subalgebra of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π· & β’ β²π‘π & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ π = βͺ π½ & β’ πΆ = (π½ Cn πΎ) & β’ (π β π½ β Comp) & β’ (π β π΄ β πΆ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π β β) β (π‘ β π β¦ π) β π΄) & β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) & β’ (π β π΅ β (Clsdβπ½)) & β’ (π β π· β (Clsdβπ½)) & β’ (π β (π΅ β© π·) = β ) & β’ π = (π β π΅) & β’ (π β πΈ β β+) & β’ (π β πΈ < (1 / 3)) β β’ (π β βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘))) | ||
Theorem | stoweidlem59 44010* | This lemma proves that there exists a function π₯ as in the proof in [BrosowskiDeutsh] p. 91, after Lemma 2: xj is in the subalgebra, 0 <= xj <= 1, xj < Ξ΅ / n on Aj (meaning A in the paper), xj > 1 - \epsilon / n on Bj. Here π· is used to represent A in the paper (because A is used for the subalgebra of functions), πΈ is used to represent Ξ΅. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘πΉ & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ π = βͺ π½ & β’ πΆ = (π½ Cn πΎ) & β’ π· = (π β (0...π) β¦ {π‘ β π β£ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)}) & β’ π΅ = (π β (0...π) β¦ {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)}) & β’ π = {π¦ β π΄ β£ βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1)} & β’ π» = (π β (0...π) β¦ {π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))}) & β’ (π β π½ β Comp) & β’ (π β π΄ β πΆ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π¦ β β) β (π‘ β π β¦ π¦) β π΄) & β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) & β’ (π β πΉ β πΆ) & β’ (π β πΈ β β+) & β’ (π β πΈ < (1 / 3)) & β’ (π β π β β) β β’ (π β βπ₯(π₯:(0...π)βΆπ΄ β§ βπ β (0...π)(βπ‘ β π (0 β€ ((π₯βπ)βπ‘) β§ ((π₯βπ)βπ‘) β€ 1) β§ βπ‘ β (π·βπ)((π₯βπ)βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < ((π₯βπ)βπ‘)))) | ||
Theorem | stoweidlem60 44011* | This lemma proves that there exists a function g as in the proof in [BrosowskiDeutsh] p. 91 (this parte of the proof actually spans through pages 91-92): g is in the subalgebra, and for all π‘ in π, there is a π such that (j-4/3)*Ξ΅ < f(t) <= (j-1/3)*Ξ΅ and (j-4/3)*Ξ΅ < g(t) < (j+1/3)*Ξ΅. Here πΉ is used to represent f in the paper, and πΈ is used to represent Ξ΅. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘πΉ & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ π = βͺ π½ & β’ πΆ = (π½ Cn πΎ) & β’ π· = (π β (0...π) β¦ {π‘ β π β£ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)}) & β’ π΅ = (π β (0...π) β¦ {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)}) & β’ (π β π½ β Comp) & β’ (π β π β β ) & β’ (π β π΄ β πΆ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π¦ β β) β (π‘ β π β¦ π¦) β π΄) & β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) & β’ (π β πΉ β πΆ) & β’ (π β βπ‘ β π 0 β€ (πΉβπ‘)) & β’ (π β πΈ β β+) & β’ (π β πΈ < (1 / 3)) β β’ (π β βπ β π΄ βπ‘ β π βπ β β ((((π β (4 / 3)) Β· πΈ) < (πΉβπ‘) β§ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)) β§ ((πβπ‘) < ((π + (1 / 3)) Β· πΈ) β§ ((π β (4 / 3)) Β· πΈ) < (πβπ‘)))) | ||
Theorem | stoweidlem61 44012* | This lemma proves that there exists a function π as in the proof in [BrosowskiDeutsh] p. 92: π is in the subalgebra, and for all π‘ in π, abs( f(t) - g(t) ) < 2*Ξ΅. Here πΉ is used to represent f in the paper, and πΈ is used to represent Ξ΅. For this lemma there's the further assumption that the function πΉ to be approximated is nonnegative (this assumption is removed in a later theorem). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘πΉ & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ (π β π½ β Comp) & β’ π = βͺ π½ & β’ (π β π β β ) & β’ πΆ = (π½ Cn πΎ) & β’ (π β π΄ β πΆ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) & β’ (π β πΉ β πΆ) & β’ (π β βπ‘ β π 0 β€ (πΉβπ‘)) & β’ (π β πΈ β β+) & β’ (π β πΈ < (1 / 3)) β β’ (π β βπ β π΄ βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < (2 Β· πΈ)) | ||
Theorem | stoweidlem62 44013* | This theorem proves the Stone Weierstrass theorem for the non-trivial case in which T is nonempty. The proof follows [BrosowskiDeutsh] p. 89 (through page 92). (Contributed by Glauco Siliprandi, 20-Apr-2017.) (Revised by AV, 13-Sep-2020.) |
β’ β²π‘πΉ & β’ β²ππ & β’ β²π‘π & β’ π» = (π‘ β π β¦ ((πΉβπ‘) β inf(ran πΉ, β, < ))) & β’ πΎ = (topGenβran (,)) & β’ π = βͺ π½ & β’ (π β π½ β Comp) & β’ πΆ = (π½ Cn πΎ) & β’ (π β π΄ β πΆ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) & β’ (π β πΉ β πΆ) & β’ (π β πΈ β β+) & β’ (π β π β β ) & β’ (π β πΈ < (1 / 3)) β β’ (π β βπ β π΄ βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < πΈ) | ||
Theorem | stoweid 44014* | This theorem proves the Stone-Weierstrass theorem for real-valued functions: let π½ be a compact topology on π, and πΆ be the set of real continuous functions on π. Assume that π΄ is a subalgebra of πΆ (closed under addition and multiplication of functions) containing constant functions and discriminating points (if π and π‘ are distinct points in π, then there exists a function β in π΄ such that h(r) is distinct from h(t) ). Then, for any continuous function πΉ and for any positive real πΈ, there exists a function π in the subalgebra π΄, such that π approximates πΉ up to πΈ (πΈ represents the usual Ξ΅ value). As a classical example, given any a, b reals, the closed interval π = [π, π] could be taken, along with the subalgebra π΄ of real polynomials on π, and then use this theorem to easily prove that real polynomials are dense in the standard metric space of continuous functions on [π, π]. The proof and lemmas are written following [BrosowskiDeutsh] p. 89 (through page 92). Some effort is put in avoiding the use of the axiom of choice. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘πΉ & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ (π β π½ β Comp) & β’ π = βͺ π½ & β’ πΆ = (π½ Cn πΎ) & β’ (π β π΄ β πΆ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β ββ β π΄ (ββπ) β (ββπ‘)) & β’ (π β πΉ β πΆ) & β’ (π β πΈ β β+) β β’ (π β βπ β π΄ βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < πΈ) | ||
Theorem | stowei 44015* | This theorem proves the Stone-Weierstrass theorem for real-valued functions: let π½ be a compact topology on π, and πΆ be the set of real continuous functions on π. Assume that π΄ is a subalgebra of πΆ (closed under addition and multiplication of functions) containing constant functions and discriminating points (if π and π‘ are distinct points in π, then there exists a function β in π΄ such that h(r) is distinct from h(t) ). Then, for any continuous function πΉ and for any positive real πΈ, there exists a function π in the subalgebra π΄, such that π approximates πΉ up to πΈ (πΈ represents the usual Ξ΅ value). As a classical example, given any a, b reals, the closed interval π = [π, π] could be taken, along with the subalgebra π΄ of real polynomials on π, and then use this theorem to easily prove that real polynomials are dense in the standard metric space of continuous functions on [π, π]. The proof and lemmas are written following [BrosowskiDeutsh] p. 89 (through page 92). Some effort is put in avoiding the use of the axiom of choice. The deduction version of this theorem is stoweid 44014: often times it will be better to use stoweid 44014 in other proofs (but this version is probably easier to be read and understood). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ πΎ = (topGenβran (,)) & β’ π½ β Comp & β’ π = βͺ π½ & β’ πΆ = (π½ Cn πΎ) & β’ π΄ β πΆ & β’ ((π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ (π₯ β β β (π‘ β π β¦ π₯) β π΄) & β’ ((π β π β§ π‘ β π β§ π β π‘) β ββ β π΄ (ββπ) β (ββπ‘)) & β’ πΉ β πΆ & β’ πΈ β β+ β β’ βπ β π΄ βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < πΈ | ||
Theorem | wallispilem1 44016* | πΌ is monotone: increasing the exponent, the integral decreases. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ πΌ = (π β β0 β¦ β«(0(,)Ο)((sinβπ₯)βπ) dπ₯) & β’ (π β π β β0) β β’ (π β (πΌβ(π + 1)) β€ (πΌβπ)) | ||
Theorem | wallispilem2 44017* | A first set of properties for the sequence πΌ that will be used in the proof of the Wallis product formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ πΌ = (π β β0 β¦ β«(0(,)Ο)((sinβπ₯)βπ) dπ₯) β β’ ((πΌβ0) = Ο β§ (πΌβ1) = 2 β§ (π β (β€β₯β2) β (πΌβπ) = (((π β 1) / π) Β· (πΌβ(π β 2))))) | ||
Theorem | wallispilem3 44018* | I maps to real values. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ πΌ = (π β β0 β¦ β«(0(,)Ο)((sinβπ₯)βπ) dπ₯) β β’ (π β β0 β (πΌβπ) β β+) | ||
Theorem | wallispilem4 44019* | πΉ maps to explicit expression for the ratio of two consecutive values of πΌ. (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
β’ πΉ = (π β β β¦ (((2 Β· π) / ((2 Β· π) β 1)) Β· ((2 Β· π) / ((2 Β· π) + 1)))) & β’ πΌ = (π β β0 β¦ β«(0(,)Ο)((sinβπ§)βπ) dπ§) & β’ πΊ = (π β β β¦ ((πΌβ(2 Β· π)) / (πΌβ((2 Β· π) + 1)))) & β’ π» = (π β β β¦ ((Ο / 2) Β· (1 / (seq1( Β· , πΉ)βπ)))) β β’ πΊ = π» | ||
Theorem | wallispilem5 44020* | The sequence π» converges to 1. (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
β’ πΉ = (π β β β¦ (((2 Β· π) / ((2 Β· π) β 1)) Β· ((2 Β· π) / ((2 Β· π) + 1)))) & β’ πΌ = (π β β0 β¦ β«(0(,)Ο)((sinβπ₯)βπ) dπ₯) & β’ πΊ = (π β β β¦ ((πΌβ(2 Β· π)) / (πΌβ((2 Β· π) + 1)))) & β’ π» = (π β β β¦ ((Ο / 2) Β· (1 / (seq1( Β· , πΉ)βπ)))) & β’ πΏ = (π β β β¦ (((2 Β· π) + 1) / (2 Β· π))) β β’ π» β 1 | ||
Theorem | wallispi 44021* | Wallis' formula for Ο : Wallis' product converges to Ο / 2 . (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ πΉ = (π β β β¦ (((2 Β· π) / ((2 Β· π) β 1)) Β· ((2 Β· π) / ((2 Β· π) + 1)))) & β’ π = (π β β β¦ (seq1( Β· , πΉ)βπ)) β β’ π β (Ο / 2) | ||
Theorem | wallispi2lem1 44022 | An intermediate step between the first version of the Wallis' formula for Ο and the second version of Wallis' formula. This second version will then be used to prove Stirling's approximation formula for the factorial. (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
β’ (π β β β (seq1( Β· , (π β β β¦ (((2 Β· π) / ((2 Β· π) β 1)) Β· ((2 Β· π) / ((2 Β· π) + 1)))))βπ) = ((1 / ((2 Β· π) + 1)) Β· (seq1( Β· , (π β β β¦ (((2 Β· π)β4) / (((2 Β· π) Β· ((2 Β· π) β 1))β2))))βπ))) | ||
Theorem | wallispi2lem2 44023 | Two expressions are proven to be equal, and this is used to complete the proof of the second version of Wallis' formula for Ο . (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
β’ (π β β β (seq1( Β· , (π β β β¦ (((2 Β· π)β4) / (((2 Β· π) Β· ((2 Β· π) β 1))β2))))βπ) = (((2β(4 Β· π)) Β· ((!βπ)β4)) / ((!β(2 Β· π))β2))) | ||
Theorem | wallispi2 44024 | An alternative version of Wallis' formula for Ο ; this second formula uses factorials and it is later used to prove Stirling's approximation formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π = (π β β β¦ ((((2β(4 Β· π)) Β· ((!βπ)β4)) / ((!β(2 Β· π))β2)) / ((2 Β· π) + 1))) β β’ π β (Ο / 2) | ||
Theorem | stirlinglem1 44025 | A simple limit of fractions is computed. (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
β’ π» = (π β β β¦ ((πβ2) / (π Β· ((2 Β· π) + 1)))) & β’ πΉ = (π β β β¦ (1 β (1 / ((2 Β· π) + 1)))) & β’ πΊ = (π β β β¦ (1 / ((2 Β· π) + 1))) & β’ πΏ = (π β β β¦ (1 / π)) β β’ π» β (1 / 2) | ||
Theorem | stirlinglem2 44026 | π΄ maps to positive reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π΄ = (π β β β¦ ((!βπ) / ((ββ(2 Β· π)) Β· ((π / e)βπ)))) β β’ (π β β β (π΄βπ) β β+) | ||
Theorem | stirlinglem3 44027 | Long but simple algebraic transformations are applied to show that π, the Wallis formula for Ο , can be expressed in terms of π΄, the Stirling's approximation formula for the factorial, up to a constant factor. This will allow (in a later theorem) to determine the right constant factor to be put into the π΄, in order to get the exact Stirling's formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π΄ = (π β β β¦ ((!βπ) / ((ββ(2 Β· π)) Β· ((π / e)βπ)))) & β’ π· = (π β β β¦ (π΄β(2 Β· π))) & β’ πΈ = (π β β β¦ ((ββ(2 Β· π)) Β· ((π / e)βπ))) & β’ π = (π β β β¦ ((((2β(4 Β· π)) Β· ((!βπ)β4)) / ((!β(2 Β· π))β2)) / ((2 Β· π) + 1))) β β’ π = (π β β β¦ ((((π΄βπ)β4) / ((π·βπ)β2)) Β· ((πβ2) / (π Β· ((2 Β· π) + 1))))) | ||
Theorem | stirlinglem4 44028* | Algebraic manipulation of ((π΅ n ) - ( B (π + 1))). It will be used in other theorems to show that π΅ is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π΄ = (π β β β¦ ((!βπ) / ((ββ(2 Β· π)) Β· ((π / e)βπ)))) & β’ π΅ = (π β β β¦ (logβ(π΄βπ))) & β’ π½ = (π β β β¦ ((((1 + (2 Β· π)) / 2) Β· (logβ((π + 1) / π))) β 1)) β β’ (π β β β ((π΅βπ) β (π΅β(π + 1))) = (π½βπ)) | ||
Theorem | stirlinglem5 44029* | If π is between 0 and 1, then a series (without alternating negative and positive terms) is given that converges to log((1+T)/(1-T)). (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π· = (π β β β¦ ((-1β(π β 1)) Β· ((πβπ) / π))) & β’ πΈ = (π β β β¦ ((πβπ) / π)) & β’ πΉ = (π β β β¦ (((-1β(π β 1)) Β· ((πβπ) / π)) + ((πβπ) / π))) & β’ π» = (π β β0 β¦ (2 Β· ((1 / ((2 Β· π) + 1)) Β· (πβ((2 Β· π) + 1))))) & β’ πΊ = (π β β0 β¦ ((2 Β· π) + 1)) & β’ (π β π β β+) & β’ (π β (absβπ) < 1) β β’ (π β seq0( + , π») β (logβ((1 + π) / (1 β π)))) | ||
Theorem | stirlinglem6 44030* | A series that converges to log((π + 1) / π). (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π» = (π β β0 β¦ (2 Β· ((1 / ((2 Β· π) + 1)) Β· ((1 / ((2 Β· π) + 1))β((2 Β· π) + 1))))) β β’ (π β β β seq0( + , π») β (logβ((π + 1) / π))) | ||
Theorem | stirlinglem7 44031* | Algebraic manipulation of the formula for J(n). (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π½ = (π β β β¦ ((((1 + (2 Β· π)) / 2) Β· (logβ((π + 1) / π))) β 1)) & β’ πΎ = (π β β β¦ ((1 / ((2 Β· π) + 1)) Β· ((1 / ((2 Β· π) + 1))β(2 Β· π)))) & β’ π» = (π β β0 β¦ (2 Β· ((1 / ((2 Β· π) + 1)) Β· ((1 / ((2 Β· π) + 1))β((2 Β· π) + 1))))) β β’ (π β β β seq1( + , πΎ) β (π½βπ)) | ||
Theorem | stirlinglem8 44032 | If π΄ converges to πΆ, then πΉ converges to C^2 . (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β²ππ & β’ β²ππ΄ & β’ β²ππ· & β’ π· = (π β β β¦ (π΄β(2 Β· π))) & β’ (π β π΄:ββΆβ+) & β’ πΉ = (π β β β¦ (((π΄βπ)β4) / ((π·βπ)β2))) & β’ πΏ = (π β β β¦ ((π΄βπ)β4)) & β’ π = (π β β β¦ ((π·βπ)β2)) & β’ ((π β§ π β β) β (π·βπ) β β+) & β’ (π β πΆ β β+) & β’ (π β π΄ β πΆ) β β’ (π β πΉ β (πΆβ2)) | ||
Theorem | stirlinglem9 44033* | ((π΅βπ) β (π΅β(π + 1))) is expressed as a limit of a series. This result will be used both to prove that π΅ is decreasing and to prove that π΅ is bounded (below). It will follow that π΅ converges in the reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π΄ = (π β β β¦ ((!βπ) / ((ββ(2 Β· π)) Β· ((π / e)βπ)))) & β’ π΅ = (π β β β¦ (logβ(π΄βπ))) & β’ π½ = (π β β β¦ ((((1 + (2 Β· π)) / 2) Β· (logβ((π + 1) / π))) β 1)) & β’ πΎ = (π β β β¦ ((1 / ((2 Β· π) + 1)) Β· ((1 / ((2 Β· π) + 1))β(2 Β· π)))) β β’ (π β β β seq1( + , πΎ) β ((π΅βπ) β (π΅β(π + 1)))) | ||
Theorem | stirlinglem10 44034* | A bound for any B(N)-B(N + 1) that will allow to find a lower bound for the whole π΅ sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π΄ = (π β β β¦ ((!βπ) / ((ββ(2 Β· π)) Β· ((π / e)βπ)))) & β’ π΅ = (π β β β¦ (logβ(π΄βπ))) & β’ πΎ = (π β β β¦ ((1 / ((2 Β· π) + 1)) Β· ((1 / ((2 Β· π) + 1))β(2 Β· π)))) & β’ πΏ = (π β β β¦ ((1 / (((2 Β· π) + 1)β2))βπ)) β β’ (π β β β ((π΅βπ) β (π΅β(π + 1))) β€ ((1 / 4) Β· (1 / (π Β· (π + 1))))) | ||
Theorem | stirlinglem11 44035* | π΅ is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π΄ = (π β β β¦ ((!βπ) / ((ββ(2 Β· π)) Β· ((π / e)βπ)))) & β’ π΅ = (π β β β¦ (logβ(π΄βπ))) & β’ πΎ = (π β β β¦ ((1 / ((2 Β· π) + 1)) Β· ((1 / ((2 Β· π) + 1))β(2 Β· π)))) β β’ (π β β β (π΅β(π + 1)) < (π΅βπ)) | ||
Theorem | stirlinglem12 44036* | The sequence π΅ is bounded below. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π΄ = (π β β β¦ ((!βπ) / ((ββ(2 Β· π)) Β· ((π / e)βπ)))) & β’ π΅ = (π β β β¦ (logβ(π΄βπ))) & β’ πΉ = (π β β β¦ (1 / (π Β· (π + 1)))) β β’ (π β β β ((π΅β1) β (1 / 4)) β€ (π΅βπ)) | ||
Theorem | stirlinglem13 44037* | π΅ is decreasing and has a lower bound, then it converges. Since π΅ is logπ΄, in another theorem it is proven that π΄ converges as well. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π΄ = (π β β β¦ ((!βπ) / ((ββ(2 Β· π)) Β· ((π / e)βπ)))) & β’ π΅ = (π β β β¦ (logβ(π΄βπ))) β β’ βπ β β π΅ β π | ||
Theorem | stirlinglem14 44038* | The sequence π΄ 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.) |
β’ π΄ = (π β β β¦ ((!βπ) / ((ββ(2 Β· π)) Β· ((π / e)βπ)))) & β’ π΅ = (π β β β¦ (logβ(π΄βπ))) β β’ βπ β β+ π΄ β π | ||
Theorem | stirlinglem15 44039* | The Stirling's formula is proven using a number of local definitions. The main theorem stirling 44040 will use this final lemma, but it will not expose the local definitions. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β²ππ & β’ π = (π β β0 β¦ ((ββ((2 Β· Ο) Β· π)) Β· ((π / e)βπ))) & β’ π΄ = (π β β β¦ ((!βπ) / ((ββ(2 Β· π)) Β· ((π / e)βπ)))) & β’ π· = (π β β β¦ (π΄β(2 Β· π))) & β’ πΈ = (π β β β¦ ((ββ(2 Β· π)) Β· ((π / e)βπ))) & β’ π = (π β β β¦ ((((2β(4 Β· π)) Β· ((!βπ)β4)) / ((!β(2 Β· π))β2)) / ((2 Β· π) + 1))) & β’ πΉ = (π β β β¦ (((π΄βπ)β4) / ((π·βπ)β2))) & β’ π» = (π β β β¦ ((πβ2) / (π Β· ((2 Β· π) + 1)))) & β’ (π β πΆ β β+) & β’ (π β π΄ β πΆ) β β’ (π β (π β β β¦ ((!βπ) / (πβπ))) β 1) | ||
Theorem | stirling 44040 | Stirling's approximation formula for π factorial. The proof follows two major steps: first it is proven that π and π 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.) |
β’ π = (π β β0 β¦ ((ββ((2 Β· Ο) Β· π)) Β· ((π / e)βπ))) β β’ (π β β β¦ ((!βπ) / (πβπ))) β 1 | ||
Theorem | stirlingr 44041 | Stirling's approximation formula for π factorial: here convergence is expressed with respect to the standard topology on the reals. The main theorem stirling 44040 is proven for convergence in the topology of complex numbers. The variable π is used to denote convergence with respect to the standard topology on the reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π = (π β β0 β¦ ((ββ((2 Β· Ο) Β· π)) Β· ((π / e)βπ))) & β’ π = (βπ‘β(topGenβran (,))) β β’ (π β β β¦ ((!βπ) / (πβπ)))π 1 | ||
Theorem | dirkerval 44042* | The Nth Dirichlet Kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π β β β¦ if((π mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β· (sinβ(π / 2))))))) β β’ (π β β β (π·βπ) = (π β β β¦ if((π mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β· (sinβ(π / 2))))))) | ||
Theorem | dirker2re 44043 | The Dirichlet Kernel value is a real if the argument is not a multiple of Ο . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (((π β β β§ π β β) β§ Β¬ (π mod (2 Β· Ο)) = 0) β ((sinβ((π + (1 / 2)) Β· π)) / ((2 Β· Ο) Β· (sinβ(π / 2)))) β β) | ||
Theorem | dirkerdenne0 44044 | The Dirichlet Kernel denominator is never 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π β β β§ Β¬ (π mod (2 Β· Ο)) = 0) β ((2 Β· Ο) Β· (sinβ(π / 2))) β 0) | ||
Theorem | dirkerval2 44045* | The Nth Dirichlet Kernel evaluated at a specific point π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π β β β¦ if((π mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β· (sinβ(π / 2))))))) β β’ ((π β β β§ π β β) β ((π·βπ)βπ) = if((π mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π)) / ((2 Β· Ο) Β· (sinβ(π / 2)))))) | ||
Theorem | dirkerre 44046* | The Dirichlet Kernel at any point evaluates to a real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π β β β¦ if((π mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β· (sinβ(π / 2))))))) β β’ ((π β β β§ π β β) β ((π·βπ)βπ) β β) | ||
Theorem | dirkerper 44047* | the Dirichlet Kernel has period 2Ο. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β· (sinβ(π¦ / 2))))))) & β’ π = (2 Β· Ο) β β’ ((π β β β§ π₯ β β) β ((π·βπ)β(π₯ + π)) = ((π·βπ)βπ₯)) | ||
Theorem | dirkerf 44048* | For any natural number π, the Dirichlet Kernel (π·βπ) is a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β· (sinβ(π¦ / 2))))))) β β’ (π β β β (π·βπ):ββΆβ) | ||
Theorem | dirkertrigeqlem1 44049* | Sum of an even number of alternating cos values. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (πΎ β β β Ξ£π β (1...(2 Β· πΎ))(cosβ(π Β· Ο)) = 0) | ||
Theorem | dirkertrigeqlem2 44050* | Trigonomic equality lemma for the Dirichlet Kernel trigonomic equality. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β (sinβπ΄) β 0) & β’ (π β π β β) β β’ (π β (((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π΄))) / Ο) = ((sinβ((π + (1 / 2)) Β· π΄)) / ((2 Β· Ο) Β· (sinβ(π΄ / 2))))) | ||
Theorem | dirkertrigeqlem3 44051* | Trigonometric equality lemma for the Dirichlet Kernel trigonometric equality. Here we handle the case for an angle that's an odd multiple of Ο. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β β) & β’ (π β πΎ β β€) & β’ π΄ = (((2 Β· πΎ) + 1) Β· Ο) β β’ (π β (((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π΄))) / Ο) = ((sinβ((π + (1 / 2)) Β· π΄)) / ((2 Β· Ο) Β· (sinβ(π΄ / 2))))) | ||
Theorem | dirkertrigeq 44052* | Trigonometric equality for the Dirichlet kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π β β β¦ if((π mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β· (sinβ(π / 2))))))) & β’ (π β π β β) & β’ πΉ = (π·βπ) & β’ π» = (π β β β¦ (((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο)) β β’ (π β πΉ = π») | ||
Theorem | dirkeritg 44053* | The definite integral of the Dirichlet Kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π₯ β β β¦ if((π₯ mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π₯)) / ((2 Β· Ο) Β· (sinβ(π₯ / 2))))))) & β’ (π β π β β) & β’ πΉ = (π·βπ) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ πΊ = (π₯ β (π΄[,]π΅) β¦ (((π₯ / 2) + Ξ£π β (1...π)((sinβ(π Β· π₯)) / π)) / Ο)) β β’ (π β β«(π΄(,)π΅)(πΉβπ₯) dπ₯ = ((πΊβπ΅) β (πΊβπ΄))) | ||
Theorem | dirkercncflem1 44054* | 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 nonzero. Such an interval is needed to apply De L'Hopital theorem. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π΄ = (π β Ο) & β’ π΅ = (π + Ο) & β’ (π β π β β) & β’ (π β (π mod (2 Β· Ο)) = 0) β β’ (π β (π β (π΄(,)π΅) β§ βπ¦ β ((π΄(,)π΅) β {π})((sinβ(π¦ / 2)) β 0 β§ (cosβ(π¦ / 2)) β 0))) | ||
Theorem | dirkercncflem2 44055* | Lemma used to prove that the Dirichlet Kernel is continuous at π points that are multiples of (2 Β· Ο). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β· (sinβ(π¦ / 2))))))) & β’ πΉ = (π¦ β ((π΄(,)π΅) β {π}) β¦ (sinβ((π + (1 / 2)) Β· π¦))) & β’ πΊ = (π¦ β ((π΄(,)π΅) β {π}) β¦ ((2 Β· Ο) Β· (sinβ(π¦ / 2)))) & β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (sinβ(π¦ / 2)) β 0) & β’ π» = (π¦ β ((π΄(,)π΅) β {π}) β¦ ((π + (1 / 2)) Β· (cosβ((π + (1 / 2)) Β· π¦)))) & β’ πΌ = (π¦ β ((π΄(,)π΅) β {π}) β¦ (Ο Β· (cosβ(π¦ / 2)))) & β’ πΏ = (π€ β (π΄(,)π΅) β¦ (((π + (1 / 2)) Β· (cosβ((π + (1 / 2)) Β· π€))) / (Ο Β· (cosβ(π€ / 2))))) & β’ (π β π β β) & β’ (π β π β (π΄(,)π΅)) & β’ (π β (π mod (2 Β· Ο)) = 0) & β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (cosβ(π¦ / 2)) β 0) β β’ (π β ((π·βπ)βπ) β (((π·βπ) βΎ ((π΄(,)π΅) β {π})) limβ π)) | ||
Theorem | dirkercncflem3 44056* | The Dirichlet Kernel is continuous at π points that are multiples of (2 Β· Ο). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β· (sinβ(π¦ / 2))))))) & β’ π΄ = (π β Ο) & β’ π΅ = (π + Ο) & β’ πΉ = (π¦ β (π΄(,)π΅) β¦ ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β· (sinβ(π¦ / 2))))) & β’ πΊ = (π¦ β (π΄(,)π΅) β¦ ((2 Β· Ο) Β· (sinβ(π¦ / 2)))) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β (π mod (2 Β· Ο)) = 0) β β’ (π β ((π·βπ)βπ) β ((π·βπ) limβ π)) | ||
Theorem | dirkercncflem4 44057* | 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.) |
β’ π· = (π β β β¦ (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β· (sinβ(π¦ / 2))))))) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β (π mod (2 Β· Ο)) β 0) & β’ π΄ = (ββ(π / (2 Β· Ο))) & β’ π΅ = (π΄ + 1) & β’ πΆ = (π΄ Β· (2 Β· Ο)) & β’ πΈ = (π΅ Β· (2 Β· Ο)) β β’ (π β (π·βπ) β (((topGenβran (,)) CnP (topGenβran (,)))βπ)) | ||
Theorem | dirkercncf 44058* | For any natural number π, the Dirichlet Kernel (π·βπ) is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β· (sinβ(π¦ / 2))))))) β β’ (π β β β (π·βπ) β (ββcnββ)) | ||
Theorem | fourierdlem1 44059 | A partition interval is a subset of the partitioned interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π:(0...π)βΆ(π΄[,]π΅)) & β’ (π β πΌ β (0..^π)) & β’ (π β π β ((πβπΌ)[,](πβ(πΌ + 1)))) β β’ (π β π β (π΄[,]π΅)) | ||
Theorem | fourierdlem2 44060* | Membership in a partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) β β’ (π β β β (π β (πβπ) β (π β (β βm (0...π)) β§ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) | ||
Theorem | fourierdlem3 44061* | Membership in a partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π β β β¦ {π β ((-Ο[,]Ο) βm (0...π)) β£ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) β β’ (π β β β (π β (πβπ) β (π β ((-Ο[,]Ο) βm (0...π)) β§ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) | ||
Theorem | fourierdlem4 44062* | πΈ is a function that maps any point to a periodic corresponding point in (π΄, π΅]. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ π = (π΅ β π΄) & β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) β β’ (π β πΈ:ββΆ(π΄(,]π΅)) | ||
Theorem | fourierdlem5 44063* | π is a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π₯ β (-Ο[,]Ο) β¦ (sinβ((π + (1 / 2)) Β· π₯))) β β’ (π β β β π:(-Ο[,]Ο)βΆβ) | ||
Theorem | fourierdlem6 44064 | π is in the periodic partition, when the considered interval is centered at π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ π = (π΅ β π΄) & β’ (π β π β β) & β’ (π β πΌ β β€) & β’ (π β π½ β β€) & β’ (π β πΌ < π½) & β’ (π β (π + (πΌ Β· π)) β (π΄[,]π΅)) & β’ (π β (π + (π½ Β· π)) β (π΄[,]π΅)) β β’ (π β π½ = (πΌ + 1)) | ||
Theorem | fourierdlem7 44065* | The difference between the periodic sawtooth function and the identity function is decreasing. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ π = (π΅ β π΄) & β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β€ π) β β’ (π β ((πΈβπ) β π) β€ ((πΈβπ) β π)) | ||
Theorem | fourierdlem8 44066 | A partition interval is a subset of the partitioned interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π:(0...π)βΆ(π΄[,]π΅)) & β’ (π β πΌ β (0..^π)) β β’ (π β ((πβπΌ)[,](πβ(πΌ + 1))) β (π΄[,]π΅)) | ||
Theorem | fourierdlem9 44067* | π» is a complex function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β β) & β’ π» = (π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) β β’ (π β π»:(-Ο[,]Ο)βΆβ) | ||
Theorem | fourierdlem10 44068 | Condition on the bounds of a nonempty subinterval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β πΆ < π·) & β’ (π β (πΆ(,)π·) β (π΄(,)π΅)) β β’ (π β (π΄ β€ πΆ β§ π· β€ π΅)) | ||
Theorem | fourierdlem11 44069* | If there is a partition, than the lower bound is strictly less than the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) β β’ (π β (π΄ β β β§ π΅ β β β§ π΄ < π΅)) | ||
Theorem | fourierdlem12 44070* | A point of a partition is not an element of any open interval determined by the partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ (π β π β ran π) β β’ ((π β§ π β (0..^π)) β Β¬ π β ((πβπ)(,)(πβ(π + 1)))) | ||
Theorem | fourierdlem13 44071* | Value of π in terms of value of π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = (π΄ + π) β§ (πβπ) = (π΅ + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ (π β πΌ β (0...π)) & β’ π = (π β (0...π) β¦ ((πβπ) β π)) β β’ (π β ((πβπΌ) = ((πβπΌ) β π) β§ (πβπΌ) = (π + (πβπΌ)))) | ||
Theorem | fourierdlem14 44072* | Given the partition π, π is the partition shifted to the left by π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = (π΄ + π) β§ (πβπ) = (π΅ + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ π = (π β (0...π) β¦ ((πβπ) β π)) β β’ (π β π β (πβπ)) | ||
Theorem | fourierdlem15 44073* | The range of the partition is between its starting point and its ending point. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) β β’ (π β π:(0...π)βΆ(π΄[,]π΅)) | ||
Theorem | fourierdlem16 44074* | The coefficients of the fourier series are integrable and reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ πΆ = (-Ο(,)Ο) & β’ (π β (πΉ βΎ πΆ) β πΏ1) & β’ π΄ = (π β β0 β¦ (β«πΆ((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο)) & β’ (π β π β β0) β β’ (π β (((π΄βπ) β β β§ (π₯ β πΆ β¦ (πΉβπ₯)) β πΏ1) β§ β«πΆ((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ β β)) | ||
Theorem | fourierdlem17 44075* | The defined πΏ is actually a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ πΏ = (π₯ β (π΄(,]π΅) β¦ if(π₯ = π΅, π΄, π₯)) β β’ (π β πΏ:(π΄(,]π΅)βΆ(π΄[,]π΅)) | ||
Theorem | fourierdlem18 44076* | The function π is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β β) & β’ π = (π β (-Ο[,]Ο) β¦ (sinβ((π + (1 / 2)) Β· π ))) β β’ (π β π β ((-Ο[,]Ο)βcnββ)) | ||
Theorem | fourierdlem19 44077* | If two elements of π· have the same periodic image in (π΄(,]π΅) then they are equal. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β π β β) & β’ π· = {π¦ β ((π΄ + π)(,](π΅ + π)) β£ βπ β β€ (π¦ + (π Β· π)) β πΆ} & β’ π = (π΅ β π΄) & β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) & β’ (π β π β π·) & β’ (π β π β π·) & β’ (π β (πΈβπ) = (πΈβπ)) β β’ (π β Β¬ π < π) | ||
Theorem | fourierdlem20 44078* | Every interval in the partition π is included in an interval of the partition π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β π:(0...π)βΆβ) & β’ (π β (πβ0) β€ π΄) & β’ (π β π΅ β€ (πβπ)) & β’ (π β π½ β (0..^π)) & β’ π = ({π΄, π΅} βͺ (ran π β© (π΄(,)π΅))) & β’ (π β π Isom < , < ((0...π), π)) & β’ πΌ = sup({π β (0..^π) β£ (πβπ) β€ (πβπ½)}, β, < ) β β’ (π β βπ β (0..^π)((πβπ½)(,)(πβ(π½ + 1))) β ((πβπ)(,)(πβ(π + 1)))) | ||
Theorem | fourierdlem21 44079* | The coefficients of the fourier series are integrable and reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ πΆ = (-Ο(,)Ο) & β’ (π β (πΉ βΎ πΆ) β πΏ1) & β’ π΅ = (π β β β¦ (β«πΆ((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο)) & β’ (π β π β β) β β’ (π β (((π΅βπ) β β β§ (π₯ β πΆ β¦ ((πΉβπ₯) Β· (sinβ(π Β· π₯)))) β πΏ1) β§ β«πΆ((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ β β)) | ||
Theorem | fourierdlem22 44080* | The coefficients of the fourier series are integrable and reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ πΆ = (-Ο(,)Ο) & β’ (π β (πΉ βΎ πΆ) β πΏ1) & β’ π΄ = (π β β0 β¦ (β«πΆ((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο)) & β’ π΅ = (π β β β¦ (β«πΆ((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο)) β β’ (π β ((π β β0 β (π΄βπ) β β) β§ (π β β β (π΅βπ) β β))) | ||
Theorem | fourierdlem23 44081* | If πΉ is continuous and π is constant, then (πΉβ(π + π )) is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β πΉ β (π΄βcnββ)) & β’ (π β π΅ β β) & β’ (π β π β β) & β’ ((π β§ π β π΅) β (π + π ) β π΄) β β’ (π β (π β π΅ β¦ (πΉβ(π + π ))) β (π΅βcnββ)) | ||
Theorem | fourierdlem24 44082 | A sufficient condition for module being nonzero. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β ((-Ο[,]Ο) β {0}) β (π΄ mod (2 Β· Ο)) β 0) | ||
Theorem | fourierdlem25 44083* | 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.) |
β’ (π β π β β) & β’ (π β π:(0...π)βΆβ) & β’ (π β πΆ β ((πβ0)[,](πβπ))) & β’ (π β Β¬ πΆ β ran π) & β’ πΌ = sup({π β (0..^π) β£ (πβπ) < πΆ}, β, < ) β β’ (π β βπ β (0..^π)πΆ β ((πβπ)(,)(πβ(π + 1)))) | ||
Theorem | fourierdlem26 44084* | Periodic image of a point π that's in the period that begins with the point π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ π = (π΅ β π΄) & β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) & β’ (π β π β β) & β’ (π β (πΈβπ) = π΅) & β’ (π β π β (π(,](π + π))) β β’ (π β (πΈβπ) = (π΄ + (π β π))) | ||
Theorem | fourierdlem27 44085 | A partition open interval is a subset of the partitioned open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π:(0...π)βΆ(π΄[,]π΅)) & β’ (π β πΌ β (0..^π)) β β’ (π β ((πβπΌ)(,)(πβ(πΌ + 1))) β (π΄(,)π΅)) | ||
Theorem | fourierdlem28 44086* | Derivative of (πΉβ(π + π )). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ π· = (β D (πΉ βΎ ((π + π΄)(,)(π + π΅)))) & β’ (π β π·:((π + π΄)(,)(π + π΅))βΆβ) β β’ (π β (β D (π β (π΄(,)π΅) β¦ (πΉβ(π + π )))) = (π β (π΄(,)π΅) β¦ (π·β(π + π )))) | ||
Theorem | fourierdlem29 44087* | Explicit function value for πΎ applied to π΄. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΎ = (π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) β β’ (π΄ β (-Ο[,]Ο) β (πΎβπ΄) = if(π΄ = 0, 1, (π΄ / (2 Β· (sinβ(π΄ / 2)))))) | ||
Theorem | fourierdlem30 44088* | Sum of three small pieces is less than Ξ΅. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β (π₯ β πΌ β¦ (πΉ Β· -πΊ)) β πΏ1) & β’ ((π β§ π₯ β πΌ) β πΉ β β) & β’ ((π β§ π₯ β πΌ) β πΊ β β) & β’ (π β π΄ β β) & β’ π = (absβπ΄) & β’ (π β πΆ β β) & β’ π = (absβπΆ) & β’ π = (absββ«πΌ(πΉ Β· -πΊ) dπ₯) & β’ (π β πΈ β β+) & β’ (π β π β β) & β’ (π β ((((π + π) + π) / πΈ) + 1) β€ π ) & β’ (π β π΅ β β) & β’ (π β (absβπ΅) β€ 1) & β’ (π β π· β β) & β’ (π β (absβπ·) β€ 1) β β’ (π β (absβ(((π΄ Β· -(π΅ / π )) β (πΆ Β· -(π· / π ))) β β«πΌ(πΉ Β· -(πΊ / π )) dπ₯)) < πΈ) | ||
Theorem | fourierdlem31 44089* | 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.) |
β’ β²ππ & β’ β²ππ & β’ β²ππ & β’ (π β π΄ β Fin) & β’ (π β βπ β π΄ βπ β β βπ β (π(,)+β)π) & β’ π = {π β β β£ βπ β (π(,)+β)π} & β’ π = (π β π΄ β¦ inf(π, β, < )) & β’ π = sup(ran π, β, < ) β β’ (π β βπ β β βπ β (π(,)+β)βπ β π΄ π) | ||
Theorem | fourierdlem32 44090 | Limit of a continuous function on an open subinterval. Lower bound version. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β π β (πΉ limβ π΄)) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β πΆ < π·) & β’ (π β (πΆ(,)π·) β (π΄(,)π΅)) & β’ π = if(πΆ = π΄, π , (πΉβπΆ)) & β’ π½ = ((TopOpenββfld) βΎt (π΄[,)π΅)) β β’ (π β π β ((πΉ βΎ (πΆ(,)π·)) limβ πΆ)) | ||
Theorem | fourierdlem33 44091 | Limit of a continuous function on an open subinterval. Upper bound version. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β πΏ β (πΉ limβ π΅)) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β πΆ < π·) & β’ (π β (πΆ(,)π·) β (π΄(,)π΅)) & β’ π = if(π· = π΅, πΏ, (πΉβπ·)) & β’ π½ = ((TopOpenββfld) βΎt ((π΄(,)π΅) βͺ {π΅})) β β’ (π β π β ((πΉ βΎ (πΆ(,)π·)) limβ π·)) | ||
Theorem | fourierdlem34 44092* | A partition is one to one. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) β β’ (π β π:(0...π)β1-1ββ) | ||
Theorem | fourierdlem35 44093 | There is a single point in (π΄(,]π΅) that's distant from π a multiple integer of π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ π = (π΅ β π΄) & β’ (π β π β β) & β’ (π β πΌ β β€) & β’ (π β π½ β β€) & β’ (π β (π + (πΌ Β· π)) β (π΄(,]π΅)) & β’ (π β (π + (π½ Β· π)) β (π΄(,]π΅)) β β’ (π β πΌ = π½) | ||
Theorem | fourierdlem36 44094* | πΉ is an isomorphism. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β Fin) & β’ (π β π΄ β β) & β’ πΉ = (β©ππ Isom < , < ((0...π), π΄)) & β’ π = ((β―βπ΄) β 1) β β’ (π β πΉ Isom < , < ((0...π), π΄)) | ||
Theorem | fourierdlem37 44095* | πΌ 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.) |
β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ π = (π΅ β π΄) & β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) & β’ πΏ = (π¦ β (π΄(,]π΅) β¦ if(π¦ = π΅, π΄, π¦)) & β’ πΌ = (π₯ β β β¦ sup({π β (0..^π) β£ (πβπ) β€ (πΏβ(πΈβπ₯))}, β, < )) β β’ (π β (πΌ:ββΆ(0..^π) β§ (π₯ β β β sup({π β (0..^π) β£ (πβπ) β€ (πΏβ(πΈβπ₯))}, β, < ) β {π β (0..^π) β£ (πβπ) β€ (πΏβ(πΈβπ₯))}))) | ||
Theorem | fourierdlem38 44096* | The function πΉ is continuous on every interval induced by the partition π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ β (dom πΉβcnββ)) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ π» = (π΄ βͺ ((-Ο[,]Ο) β dom πΉ)) & β’ (π β ran π = π») β β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) | ||
Theorem | fourierdlem39 44097* | Integration by parts of β«(π΄(,)π΅)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) & β’ πΊ = (β D πΉ) & β’ (π β πΊ β ((π΄(,)π΅)βcnββ)) & β’ (π β βπ¦ β β βπ₯ β (π΄(,)π΅)(absβ(πΊβπ₯)) β€ π¦) & β’ (π β π β β+) β β’ (π β β«(π΄(,)π΅)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ = ((((πΉβπ΅) Β· -((cosβ(π Β· π΅)) / π )) β ((πΉβπ΄) Β· -((cosβ(π Β· π΄)) / π ))) β β«(π΄(,)π΅)((πΊβπ₯) Β· -((cosβ(π Β· π₯)) / π )) dπ₯)) | ||
Theorem | fourierdlem40 44098* | π» is a continuous function on any partition interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π΄ β (-Ο[,]Ο)) & β’ (π β π΅ β (-Ο[,]Ο)) & β’ (π β π β β) & β’ (π β Β¬ 0 β (π΄(,)π΅)) & β’ (π β (πΉ βΎ ((π΄ + π)(,)(π΅ + π))) β (((π΄ + π)(,)(π΅ + π))βcnββ)) & β’ (π β π β β) & β’ (π β π β β) & β’ π» = (π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) β β’ (π β (π» βΎ (π΄(,)π΅)) β ((π΄(,)π΅)βcnββ)) | ||
Theorem | fourierdlem41 44099* | 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.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ π = (π΅ β π΄) & β’ ((π β§ π₯ β π· β§ π β β€) β (π₯ + (π Β· π)) β π·) & β’ (π β π β β) & β’ π = (π₯ β β β¦ ((ββ((π΅ β π₯) / π)) Β· π)) & β’ πΈ = (π₯ β β β¦ (π₯ + (πβπ₯))) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ ((π β§ π β (0..^π)) β ((πβπ)(,)(πβ(π + 1))) β π·) β β’ (π β (βπ¦ β β (π¦ < π β§ (π¦(,)π) β π·) β§ βπ¦ β β (π < π¦ β§ (π(,)π¦) β π·))) | ||
Theorem | fourierdlem42 44100* | The set of points in a moved partition are finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 29-Sep-2020.) |
β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΅ < πΆ) & β’ π = (πΆ β π΅) & β’ (π β π΄ β (π΅[,]πΆ)) & β’ (π β π΄ β Fin) & β’ (π β π΅ β π΄) & β’ (π β πΆ β π΄) & β’ π· = (abs β β ) & β’ πΌ = ((π΄ Γ π΄) β I ) & β’ π = ran (π· βΎ πΌ) & β’ πΈ = inf(π , β, < ) & β’ (π β π β β) & β’ (π β π β β) & β’ π½ = (topGenβran (,)) & β’ πΎ = (π½ βΎt (π[,]π)) & β’ π» = {π₯ β (π[,]π) β£ βπ β β€ (π₯ + (π Β· π)) β π΄} & β’ (π β ((π β§ (π β β β§ π β β β§ π < π)) β§ βπ β β€ βπ β β€ ((π + (π Β· π)) β π΄ β§ (π + (π Β· π)) β π΄))) β β’ (π β π» β Fin) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |