Home | Metamath
Proof ExplorerTheorem List
(p. 213 of 325)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs

Color key: | Metamath Proof Explorer
(1-22374) |
Hilbert Space Explorer
(22375-23897) |
Users' Mathboxes
(23898-32447) |

Type | Label | Description | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|

Statement | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | chpdifbndlem2 21201* | Lemma for chpdifbnd 21202. (Contributed by Mario Carneiro, 25-May-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ Λ ψ ψ ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | chpdifbnd 21202* | A bound on the difference of nearby ψ values. Theorem 10.5.2 of [Shapiro], p. 427. (Contributed by Mario Carneiro, 25-May-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | logdivbnd 21203* | A bound on a sum of logs, used in pntlemk 21253. This is not as precise as logdivsum 21180 in its asymptotic behavior, but it is valid for all and does not require a limit value. (Contributed by Mario Carneiro, 13-Apr-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | selberg3lem1 21204* | Introduce a log weighting on the summands of ΛΛ, the core of selberg2 21198 (written here as Λψ ). Equation 10.4.21 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Λ ψ Λ ψ Λ ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | selberg3lem2 21205* | Lemma for selberg3 21206. Equation 10.4.21 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Λ ψ Λ ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | selberg3 21206* | Introduce a log weighting on the summands of ΛΛ, the core of selberg2 21198 (written here as Λψ ). Equation 10.6.7 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ Λ ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | selberg4lem1 21207* | Lemma for selberg4 21208. Equation 10.4.20 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Λ ψ Λ Λ ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | selberg4 21208* | The Selberg symmetry formula for products of three primes, instead of two. The sum here can also be written in the symmetric form ΛΛΛ; we eliminate one of the nested sums by using the definition of ψ Λ. This statement can thus equivalently be written ψ ΛΛΛ . Equation 10.4.23 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ Λ Λ ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntrval 21209* | Define the residual of the second Chebyshev function. The goal is to have , or . (Contributed by Mario Carneiro, 8-Apr-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntrf 21210 | Functionality of the residual. Lemma for pnt 21261. (Contributed by Mario Carneiro, 8-Apr-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntrmax 21211* | There is a bound on the residual valid for all . (Contributed by Mario Carneiro, 9-Apr-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntrsumo1 21212* | A bound on a sum over . Equation 10.1.16 of [Shapiro], p. 403. (Contributed by Mario Carneiro, 25-May-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntrsumbnd 21213* | A bound on a sum over . Equation 10.1.16 of [Shapiro], p. 403. (Contributed by Mario Carneiro, 25-May-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntrsumbnd2 21214* | A bound on a sum over . Equation 10.1.16 of [Shapiro], p. 403. (Contributed by Mario Carneiro, 14-Apr-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | selbergr 21215* | Selberg's symmetry formula, using the residual of the second Chebyshev function. Equation 10.6.2 of [Shapiro], p. 428. (Contributed by Mario Carneiro, 16-Apr-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ Λ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | selberg3r 21216* | Selberg's symmetry formula, using the residual of the second Chebyshev function. Equation 10.6.8 of [Shapiro], p. 429. (Contributed by Mario Carneiro, 30-May-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ Λ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | selberg4r 21217* | Selberg's symmetry formula, using the residual of the second Chebyshev function. Equation 10.6.11 of [Shapiro], p. 430. (Contributed by Mario Carneiro, 30-May-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ Λ Λ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | selberg34r 21218* | The sum of selberg3r 21216 and selberg4r 21217. (Contributed by Mario Carneiro, 31-May-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ Λ Λ Λ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntsval 21219* | Define the "Selberg function", whose asymptotic behavior is the content of selberg 21195. (Contributed by Mario Carneiro, 31-May-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Λ ψ Λ ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntsf 21220* | Functionality of the Selberg function. (Contributed by Mario Carneiro, 31-May-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Λ ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | selbergs 21221* | Selberg's symmetry formula, using the definition of the Selberg function. (Contributed by Mario Carneiro, 31-May-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Λ ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | selbergsb 21222* | Selberg's symmetry formula, using the definition of the Selberg function. (Contributed by Mario Carneiro, 31-May-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Λ ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntsval2 21223* | The Selberg function can be expressed using the convolution product of the von Mangoldt function with itself. (Contributed by Mario Carneiro, 31-May-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Λ ψ Λ Λ Λ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntrlog2bndlem1 21224* | The sum of selberg3r 21216 and selberg4r 21217. (Contributed by Mario Carneiro, 31-May-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Λ ψ ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntrlog2bndlem2 21225* | Lemma for pntrlog2bnd 21231. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Λ ψ ψ ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntrlog2bndlem3 21226* | Lemma for pntrlog2bnd 21231. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Λ ψ ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntrlog2bndlem4 21227* | Lemma for pntrlog2bnd 21231. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Λ ψ ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntrlog2bndlem5 21228* | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Λ ψ ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntrlog2bndlem6a 21229* | Lemma for pntrlog2bndlem6 21230. (Contributed by Mario Carneiro, 7-Jun-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Λ ψ ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntrlog2bndlem6 21230* | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Λ ψ ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntrlog2bnd 21231* | A bound on . Equation 10.6.15 of [Shapiro], p. 431. (Contributed by Mario Carneiro, 1-Jun-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntpbnd1a 21232* | Lemma for pntpbnd 21235. (Contributed by Mario Carneiro, 11-Apr-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntpbnd1 21233* | Lemma for pntpbnd 21235. (Contributed by Mario Carneiro, 11-Apr-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntpbnd2 21234* | Lemma for pntpbnd 21235. (Contributed by Mario Carneiro, 11-Apr-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntpbnd 21235* | Lemma for pnt 21261. Establish smallness of at a point. Lemma 10.6.1 in [Shapiro], p. 436. (Contributed by Mario Carneiro, 10-Apr-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntibndlem1 21236 | Lemma for pntibnd 21240. (Contributed by Mario Carneiro, 10-Apr-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntibndlem2a 21237* | Lemma for pntibndlem2 21238. (Contributed by Mario Carneiro, 7-Jun-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntibndlem2 21238* | Lemma for pntibnd 21240. The main work, after eliminating all the quantifiers. (Contributed by Mario Carneiro, 10-Apr-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ ψ ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntibndlem3 21239* | Lemma for pntibnd 21240. Package up pntibndlem2 21238 in quantifiers. (Contributed by Mario Carneiro, 10-Apr-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntibnd 21240* | Lemma for pnt 21261. Establish smallness of on an interval. Lemma 10.6.2 in [Shapiro], p. 436. (Contributed by Mario Carneiro, 10-Apr-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntlemd 21241 |
Lemma for pnt 21261. Closure for the constants used in the
proof. For
comparison with Equation 10.6.27 of [Shapiro], p. 434, is C^*,
is c_{1}, is λ, is c_{2}, and is c_{3}.
(Contributed by Mario Carneiro, 13-Apr-2016.)
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ ; | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntlemc 21242* |
Lemma for pnt 21261. Closure for the constants used in the
proof. For
comparison with Equation 10.6.27 of [Shapiro], p. 434, is α,
is ε,
and is K.
(Contributed by Mario Carneiro,
13-Apr-2016.)
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ ; | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntlema 21243* |
Lemma for pnt 21261. Closure for the constants used in the
proof. The
mammoth expression is a number large enough to satisfy all the
lower bounds needed for . For comparison with Equation 10.6.27 of
[Shapiro], p. 434, is x_{2},
is x_{1}, is the big-O
constant in Equation 10.6.29 of [Shapiro], p. 435, and is the
unnamed lower bound of "for sufficiently large x" in Equation
10.6.34 of
[Shapiro], p. 436. (Contributed by
Mario Carneiro, 13-Apr-2016.)
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ ; ; | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntlemb 21244* | Lemma for pnt 21261. Unpack all the lower bounds contained in , in the form they will be used. For comparison with Equation 10.6.27 of [Shapiro], p. 434, is x. (Contributed by Mario Carneiro, 13-Apr-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ ; ; ; | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntlemg 21245* | Lemma for pnt 21261. Closure for the constants used in the proof. For comparison with Equation 10.6.27 of [Shapiro], p. 434, is j^* and is ĵ. (Contributed by Mario Carneiro, 13-Apr-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ ; ; | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntlemh 21246* | Lemma for pnt 21261. Bounds on the subintervals in the induction. (Contributed by Mario Carneiro, 13-Apr-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ ; ; | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntlemn 21247* | Lemma for pnt 21261. The "naive" base bound, which we will slightly improve. (Contributed by Mario Carneiro, 13-Apr-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ ; ; | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntlemq 21248* | Lemma for pntlemj 21250. (Contributed by Mario Carneiro, 7-Jun-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ ; ; ..^ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntlemr 21249* | Lemma for pntlemj 21250. (Contributed by Mario Carneiro, 7-Jun-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ ; ; ..^ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntlemj 21250* | Lemma for pnt 21261. The induction step. Using pntibnd 21240, we find an interval in which is sufficiently large and has a much smaller value, (instead of our original bound ). (Contributed by Mario Carneiro, 13-Apr-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ ; ; ..^ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntlemi 21251* | Lemma for pnt 21261. Eliminate some assumptions from pntlemj 21250. (Contributed by Mario Carneiro, 13-Apr-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ ; ; ..^ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntlemf 21252* | Lemma for pnt 21261. Add up the pieces in pntlemi 21251 to get an estimate slightly better than the naive lower bound . (Contributed by Mario Carneiro, 13-Apr-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ ; ; ; | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntlemk 21253* | Lemma for pnt 21261. Evaluate the naive part of the estimate. (Contributed by Mario Carneiro, 14-Apr-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ ; ; | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntlemo 21254* | Lemma for pnt 21261. Combine all the estimates to establish a smaller eventual bound on . (Contributed by Mario Carneiro, 14-Apr-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ ; ; | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntleme 21255* | Lemma for pnt 21261. Package up pntlemo 21254 in quantifiers. (Contributed by Mario Carneiro, 14-Apr-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ ; ; | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntlem3 21256* | Lemma for pnt 21261. Equation 10.6.35 in [Shapiro], p. 436. (Contributed by Mario Carneiro, 8-Apr-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntlemp 21257* | Lemma for pnt 21261. Wrapping up more quantifiers. (Contributed by Mario Carneiro, 14-Apr-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ ; | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pntleml 21258* | Lemma for pnt 21261. Equation 10.6.35 in [Shapiro], p. 436. (Contributed by Mario Carneiro, 14-Apr-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ ; ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pnt3 21259 | The Prime Number Theorem, version 3: the second Chebyshev function tends asymptotically to . (Contributed by Mario Carneiro, 1-Jun-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ψ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pnt2 21260 | The Prime Number Theorem, version 2: the first Chebyshev function tends asymptotically to . (Contributed by Mario Carneiro, 1-Jun-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pnt 21261 | The Prime Number Theorem: the number of prime numbers less than tends asymptotically to as goes to infinity. (Contributed by Mario Carneiro, 1-Jun-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

π
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

13.4.13 Ostrowski's theorem | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | abvcxp 21262* | Raising an absolute value to a power less than one yields another absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

AbsVal | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | padicfval 21263* | Value of the p-adic absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | padicval 21264* | Value of the p-adic absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ostth2lem1 21265* | Lemma for ostth2 21284, although it is just a simple statement about exponentials which does not involve any specifics of ostth2 21284. If a power is upper bounded by a linear term, the exponent must be less than one. Or in big-O notation, for any . (Contributed by Mario Carneiro, 10-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | qrngbas 21266 | The base set of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | qdrng 21267 | The rationals form a division ring. (Contributed by Mario Carneiro, 8-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | qrng0 21268 | The zero element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | qrng1 21269 | The unit element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | qrngneg 21270 | The additive inverse in the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s}
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | qrngdiv 21271 | The division operation in the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} /_{r} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | qabvle 21272 | By using induction on , we show a long-range inequality coming from the triangle inequality. (Contributed by Mario Carneiro, 10-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | qabvexp 21273 | Induct the product rule abvmul 15872 to find the absolute value of a power. (Contributed by Mario Carneiro, 10-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ostthlem1 21274* | Lemma for ostth 21286. If two absolute values agree on the positive integers greater than one, then they agree for all rational numbers and thus are equal as functions. (Contributed by Mario Carneiro, 9-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ostthlem2 21275* | Lemma for ostth 21286. Refine ostthlem1 21274 so that it is sufficient to only show equality on the primes. (Contributed by Mario Carneiro, 9-Sep-2014.) (Revised by Mario Carneiro, 20-Jun-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | qabsabv 21276 | The regular absolute value function on the rationals is in fact an absolute value under our definition. (Contributed by Mario Carneiro, 9-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | padicabv 21277* | The p-adic absolute value (with arbitrary base) is an absolute value. (Contributed by Mario Carneiro, 9-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | padicabvf 21278* | The p-adic absolute value is an absolute value. (Contributed by Mario Carneiro, 9-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | padicabvcxp 21279* | All positive powers of the p-adic absolute value are absolute values. (Contributed by Mario Carneiro, 9-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ostth1 21280* | - Lemma for ostth 21286: trivial case. (Not that the proof is trivial, but that we are proving that the function is trivial.) If is equal to on the primes, then by complete induction and the multiplicative property abvmul 15872 of the absolute value, is equal to on all the integers, and ostthlem1 21274 extends this to the other rational numbers. (Contributed by Mario Carneiro, 10-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ostth2lem2 21281* | Lemma for ostth2 21284. (Contributed by Mario Carneiro, 10-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ostth2lem3 21282* | Lemma for ostth2 21284. (Contributed by Mario Carneiro, 10-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ostth2lem4 21283* | Lemma for ostth2 21284. (Contributed by Mario Carneiro, 10-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ostth2 21284* | - Lemma for ostth 21286: regular case. (Contributed by Mario Carneiro, 10-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ostth3 21285* | - Lemma for ostth 21286: p-adic case. (Contributed by Mario Carneiro, 10-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ostth 21286* | Ostrowski's theorem, which classifies all absolute values on . Any such absolute value must either be the trivial absolute value , a constant exponent times the regular absolute value, or a positive exponent times the p-adic absolute value. (Contributed by Mario Carneiro, 10-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

ℂ_{fld}
↾_{s} AbsVal
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

PART 14 GRAPH THEORY
Terms and properties of graphs:
Special kinds of graphs:
For the terms "Path", "Walk", "Trail", "Circuit",
"Cycle" see the remarks below and the definitions in Section I.1 in
[Bollobas] p. 4-5.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

14.1 Undirected graphs -
basics | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

14.1.1 Undirected hypergraphs | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Syntax | cuhg 21287 | Extend class notation with undirected hypergraphs. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

UHGrph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Definition | df-uhgra 21288* | Define the class of all undirected hypergraphs. An undirected hypergraph is a pair of a set and a function into the powerset of this set (the empty set excluded). (Contributed by Alexander van der Vekens, 26-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

UHGrph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | reluhgra 21289 | The class of all undirected hypergraphs is a relation. (Contributed by Alexander van der Vekens, 26-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

UHGrph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uhgrav 21290 | The classes of vertices and edges of an undirected hypergraph are sets. (Contributed by Alexander van der Vekens, 26-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

UHGrph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | isuhgra 21291 | The property of being an undirected hypergraph. (Contributed by Alexander van der Vekens, 26-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

UHGrph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uhgraf 21292 | The edge function of an undirected hypergraph is a function into the power set of the set of vertices. (Contributed by Alexander van der Vekens, 26-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

UHGrph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uhgrafun 21293 | The edge function of an undirected hypergraph is a function. (Contributed by Alexander van der Vekens, 26-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

UHGrph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uhgrass 21294 | An edge is a subset of vertices, analogous to umgrass 21307. (Contributed by Alexander van der Vekens, 26-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

UHGrph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uhgraeq12d 21295 | Equality of hypergraphs. (Contributed by Alexander van der Vekens, 26-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

UHGrph UHGrph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uhgrares 21296 | A subgraph of a hypergraph (formed by removing some edges from the original graph) is a hypergraph, analogous to umgrares 21312. (Contributed by Alexander van der Vekens, 27-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

UHGrph UHGrph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uhgra0 21297 | The empty graph, with vertices but no edges, is a hypergraph, analogous to umgra0 21313. (Contributed by Alexander van der Vekens, 27-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

UHGrph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uhgra0v 21298 | The null graph, with no vertices, is a hypergraph if and only if the edge function is empty. (Contributed by Alexander van der Vekens, 27-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

UHGrph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | uhgraun 21299 | If and are hypergraphs, then is a hypergraph (the vertex set stays the same, but the edges from both graphs are kept, maybe resulting in two edges between two vertices), analogous to umgraun 21316. (Contributed by Alexander van der Vekens, 27-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

UHGrph UHGrph UHGrph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

14.1.2 Undirected multigraphs | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Syntax | cumg 21300 | Extend class notation with undirected multigraphs. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

UMGrph |

< Previous Next > |