| Metamath
Proof Explorer Theorem List (p. 276 of 494) | < 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: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | 2sqreunn 27501* | There exists a unique decomposition of a prime of the form 4𝑘 + 1 as a sum of squares of two positive integers. See 2sqnn 27483 for the existence of such a decomposition. (Contributed by AV, 11-Jun-2023.) (Revised by AV, 25-Jun-2023.) |
| ⊢ (𝜑 ↔ (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → (∃!𝑎 ∈ ℕ ∃𝑏 ∈ ℕ 𝜑 ∧ ∃!𝑏 ∈ ℕ ∃𝑎 ∈ ℕ 𝜑)) | ||
| Theorem | 2sqreult 27502* | There exists a unique decomposition of a prime as a sum of squares of two different nonnegative integers. (Contributed by AV, 8-Jun-2023.) (Proposed by GL, 8-Jun-2023.) (Revised by AV, 25-Jun-2023.) |
| ⊢ (𝜑 ↔ (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → (∃!𝑎 ∈ ℕ0 ∃𝑏 ∈ ℕ0 𝜑 ∧ ∃!𝑏 ∈ ℕ0 ∃𝑎 ∈ ℕ0 𝜑)) | ||
| Theorem | 2sqreultb 27503* | There exists a unique decomposition of a prime as a sum of squares of two different nonnegative integers iff 𝑃≡1 (mod 4). (Contributed by AV, 10-Jun-2023.) The prime needs not be odd, as observed by WL. (Revised by AV, 25-Jun-2023.) |
| ⊢ (𝜑 ↔ (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) ⇒ ⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ (∃!𝑎 ∈ ℕ0 ∃𝑏 ∈ ℕ0 𝜑 ∧ ∃!𝑏 ∈ ℕ0 ∃𝑎 ∈ ℕ0 𝜑))) | ||
| Theorem | 2sqreunnlt 27504* | There exists a unique decomposition of a prime of the form 4𝑘 + 1 as a sum of squares of two different positive integers. (Contributed by AV, 4-Jun-2023.) Specialization to different integers, proposed by GL. (Revised by AV, 25-Jun-2023.) |
| ⊢ (𝜑 ↔ (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → (∃!𝑎 ∈ ℕ ∃𝑏 ∈ ℕ 𝜑 ∧ ∃!𝑏 ∈ ℕ ∃𝑎 ∈ ℕ 𝜑)) | ||
| Theorem | 2sqreunnltb 27505* | There exists a unique decomposition of a prime as a sum of squares of two different positive integers iff the prime is of the form 4𝑘 + 1. (Contributed by AV, 11-Jun-2023.) The prime needs not be odd, as observed by WL. (Revised by AV, 25-Jun-2023.) |
| ⊢ (𝜑 ↔ (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) ⇒ ⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ (∃!𝑎 ∈ ℕ ∃𝑏 ∈ ℕ 𝜑 ∧ ∃!𝑏 ∈ ℕ ∃𝑎 ∈ ℕ 𝜑))) | ||
| Theorem | 2sqreuop 27506* | There exists a unique decomposition of a prime of the form 4𝑘 + 1 as a sum of squares of two nonnegative integers. Ordered pair variant of 2sqreu 27500. (Contributed by AV, 2-Jul-2023.) |
| ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑝 ∈ (ℕ0 × ℕ0)((1st ‘𝑝) ≤ (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃)) | ||
| Theorem | 2sqreuopnn 27507* | There exists a unique decomposition of a prime of the form 4𝑘 + 1 as a sum of squares of two positive integers. Ordered pair variant of 2sqreunn 27501. (Contributed by AV, 2-Jul-2023.) |
| ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑝 ∈ (ℕ × ℕ)((1st ‘𝑝) ≤ (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃)) | ||
| Theorem | 2sqreuoplt 27508* | There exists a unique decomposition of a prime as a sum of squares of two different nonnegative integers. Ordered pair variant of 2sqreult 27502. (Contributed by AV, 2-Jul-2023.) |
| ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑝 ∈ (ℕ0 × ℕ0)((1st ‘𝑝) < (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃)) | ||
| Theorem | 2sqreuopltb 27509* | There exists a unique decomposition of a prime as a sum of squares of two different nonnegative integers iff 𝑃≡1 (mod 4). Ordered pair variant of 2sqreultb 27503. (Contributed by AV, 3-Jul-2023.) |
| ⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ ∃!𝑝 ∈ (ℕ0 × ℕ0)((1st ‘𝑝) < (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃))) | ||
| Theorem | 2sqreuopnnlt 27510* | There exists a unique decomposition of a prime of the form 4𝑘 + 1 as a sum of squares of two different positive integers. Ordered pair variant of 2sqreunnlt 27504. (Contributed by AV, 3-Jul-2023.) |
| ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑝 ∈ (ℕ × ℕ)((1st ‘𝑝) < (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃)) | ||
| Theorem | 2sqreuopnnltb 27511* | There exists a unique decomposition of a prime as a sum of squares of two different positive integers iff the prime is of the form 4𝑘 + 1. Ordered pair variant of 2sqreunnltb 27505. (Contributed by AV, 3-Jul-2023.) |
| ⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ ∃!𝑝 ∈ (ℕ × ℕ)((1st ‘𝑝) < (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃))) | ||
| Theorem | 2sqreuopb 27512* | There exists a unique decomposition of a prime as a sum of squares of two different positive integers iff the prime is of the form 4𝑘 + 1. Alternate ordered pair variant of 2sqreunnltb 27505. (Contributed by AV, 3-Jul-2023.) |
| ⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ ∃!𝑝 ∈ (ℕ × ℕ)∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)))) | ||
| Theorem | chebbnd1lem1 27513 | Lemma for chebbnd1 27516: show a lower bound on π(𝑥) at even integers using similar techniques to those used to prove bpos 27337. (Note that the expression 𝐾 is actually equal to 2 · 𝑁, but proving that is not necessary for the proof, and it's too much work.) The key to the proof is bposlem1 27328, which shows that each term in the expansion ((2 · 𝑁)C𝑁) = ∏𝑝 ∈ ℙ (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) is at most 2 · 𝑁, so that the sum really only has nonzero elements up to 2 · 𝑁, and since each term is at most 2 · 𝑁, after taking logs we get the inequality π(2 · 𝑁) · log(2 · 𝑁) ≤ log((2 · 𝑁)C𝑁), and bclbnd 27324 finishes the proof. (Contributed by Mario Carneiro, 22-Sep-2014.) (Revised by Mario Carneiro, 15-Apr-2016.) |
| ⊢ 𝐾 = if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘4) → (log‘((4↑𝑁) / 𝑁)) < ((π‘(2 · 𝑁)) · (log‘(2 · 𝑁)))) | ||
| Theorem | chebbnd1lem2 27514 | Lemma for chebbnd1 27516: Show that log(𝑁) / 𝑁 does not change too much between 𝑁 and 𝑀 = ⌊(𝑁 / 2). (Contributed by Mario Carneiro, 22-Sep-2014.) |
| ⊢ 𝑀 = (⌊‘(𝑁 / 2)) ⇒ ⊢ ((𝑁 ∈ ℝ ∧ 8 ≤ 𝑁) → ((log‘(2 · 𝑀)) / (2 · 𝑀)) < (2 · ((log‘𝑁) / 𝑁))) | ||
| Theorem | chebbnd1lem3 27515 | Lemma for chebbnd1 27516: get a lower bound on π(𝑁) / (𝑁 / log(𝑁)) that is independent of 𝑁. (Contributed by Mario Carneiro, 21-Sep-2014.) |
| ⊢ 𝑀 = (⌊‘(𝑁 / 2)) ⇒ ⊢ ((𝑁 ∈ ℝ ∧ 8 ≤ 𝑁) → (((log‘2) − (1 / (2 · e))) / 2) < ((π‘𝑁) · ((log‘𝑁) / 𝑁))) | ||
| Theorem | chebbnd1 27516 | The Chebyshev bound: The function π(𝑥) is eventually lower bounded by a positive constant times 𝑥 / log(𝑥). Alternatively stated, the function (𝑥 / log(𝑥)) / π(𝑥) is eventually bounded. (Contributed by Mario Carneiro, 22-Sep-2014.) |
| ⊢ (𝑥 ∈ (2[,)+∞) ↦ ((𝑥 / (log‘𝑥)) / (π‘𝑥))) ∈ 𝑂(1) | ||
| Theorem | chtppilimlem1 27517 | Lemma for chtppilim 27519. (Contributed by Mario Carneiro, 22-Sep-2014.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 𝑁 ∈ (2[,)+∞)) & ⊢ (𝜑 → ((𝑁↑𝑐𝐴) / (π‘𝑁)) < (1 − 𝐴)) ⇒ ⊢ (𝜑 → ((𝐴↑2) · ((π‘𝑁) · (log‘𝑁))) < (θ‘𝑁)) | ||
| Theorem | chtppilimlem2 27518* | Lemma for chtppilim 27519. (Contributed by Mario Carneiro, 22-Sep-2014.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 < 1) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (2[,)+∞)(𝑧 ≤ 𝑥 → ((𝐴↑2) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥))) | ||
| Theorem | chtppilim 27519 | The θ function is asymptotic to π(𝑥)log(𝑥), so it is sufficient to prove θ(𝑥) / 𝑥 ⇝𝑟 1 to establish the PNT. (Contributed by Mario Carneiro, 22-Sep-2014.) |
| ⊢ (𝑥 ∈ (2[,)+∞) ↦ ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))) ⇝𝑟 1 | ||
| Theorem | chto1ub 27520 | The θ function is upper bounded by a linear term. Corollary of chtub 27256. (Contributed by Mario Carneiro, 22-Sep-2014.) |
| ⊢ (𝑥 ∈ ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ∈ 𝑂(1) | ||
| Theorem | chebbnd2 27521 | The Chebyshev bound, part 2: The function π(𝑥) is eventually upper bounded by a positive constant times 𝑥 / log(𝑥). Alternatively stated, the function π(𝑥) / (𝑥 / log(𝑥)) is eventually bounded. (Contributed by Mario Carneiro, 22-Sep-2014.) |
| ⊢ (𝑥 ∈ (2[,)+∞) ↦ ((π‘𝑥) / (𝑥 / (log‘𝑥)))) ∈ 𝑂(1) | ||
| Theorem | chto1lb 27522 | The θ function is lower bounded by a linear term. Corollary of chebbnd1 27516. (Contributed by Mario Carneiro, 8-Apr-2016.) |
| ⊢ (𝑥 ∈ (2[,)+∞) ↦ (𝑥 / (θ‘𝑥))) ∈ 𝑂(1) | ||
| Theorem | chpchtlim 27523 | The ψ and θ functions are asymptotic to each other, so is sufficient to prove either θ(𝑥) / 𝑥 ⇝𝑟 1 or ψ(𝑥) / 𝑥 ⇝𝑟 1 to establish the PNT. (Contributed by Mario Carneiro, 8-Apr-2016.) |
| ⊢ (𝑥 ∈ (2[,)+∞) ↦ ((ψ‘𝑥) / (θ‘𝑥))) ⇝𝑟 1 | ||
| Theorem | chpo1ub 27524 | The ψ function is upper bounded by a linear term. (Contributed by Mario Carneiro, 16-Apr-2016.) |
| ⊢ (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∈ 𝑂(1) | ||
| Theorem | chpo1ubb 27525* | The ψ function is upper bounded by a linear term. (Contributed by Mario Carneiro, 31-May-2016.) |
| ⊢ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ ℝ+ (ψ‘𝑥) ≤ (𝑐 · 𝑥) | ||
| Theorem | vmadivsum 27526* | The sum of the von Mangoldt function over 𝑛 is asymptotic to log𝑥 + 𝑂(1). Equation 9.2.13 of [Shapiro], p. 331. (Contributed by Mario Carneiro, 16-Apr-2016.) |
| ⊢ (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) | ||
| Theorem | vmadivsumb 27527* | Give a total bound on the von Mangoldt sum. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ (1[,)+∞)(abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ≤ 𝑐 | ||
| Theorem | rplogsumlem1 27528* | Lemma for rplogsum 27571. (Contributed by Mario Carneiro, 2-May-2016.) |
| ⊢ (𝐴 ∈ ℕ → Σ𝑛 ∈ (2...𝐴)((log‘𝑛) / (𝑛 · (𝑛 − 1))) ≤ 2) | ||
| Theorem | rplogsumlem2 27529* | Lemma for rplogsum 27571. Equation 9.2.14 of [Shapiro], p. 331. (Contributed by Mario Carneiro, 2-May-2016.) |
| ⊢ (𝐴 ∈ ℤ → Σ𝑛 ∈ (1...𝐴)(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) ≤ 2) | ||
| Theorem | dchrisum0lem1a 27530 | Lemma for dchrisum0lem1 27560. (Contributed by Mario Carneiro, 7-Jun-2016.) |
| ⊢ (((𝜑 ∧ 𝑋 ∈ ℝ+) ∧ 𝐷 ∈ (1...(⌊‘𝑋))) → (𝑋 ≤ ((𝑋↑2) / 𝐷) ∧ (⌊‘((𝑋↑2) / 𝐷)) ∈ (ℤ≥‘(⌊‘𝑋)))) | ||
| Theorem | rpvmasumlem 27531* | Lemma for rpvmasum 27570. Calculate the "trivial case" estimate Σ𝑛 ≤ 𝑥( 1 (𝑛)Λ(𝑛) / 𝑛) = log𝑥 + 𝑂(1), where 1 (𝑥) is the principal Dirichlet character. Equation 9.4.7 of [Shapiro], p. 376. (Contributed by Mario Carneiro, 2-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) ∈ 𝑂(1)) | ||
| Theorem | dchrisumlema 27532* | Lemma for dchrisum 27536. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝𝑟 0) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴)) ⇒ ⊢ (𝜑 → ((𝐼 ∈ ℝ+ → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ) ∧ (𝐼 ∈ (𝑀[,)+∞) → 0 ≤ ⦋𝐼 / 𝑛⦌𝐴))) | ||
| Theorem | dchrisumlem1 27533* | Lemma for dchrisum 27536. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝𝑟 0) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴)) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ (𝜑 → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) ⇒ ⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → (abs‘Σ𝑛 ∈ (0..^𝑈)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) | ||
| Theorem | dchrisumlem2 27534* | Lemma for dchrisum 27536. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝𝑟 0) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴)) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ (𝜑 → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) & ⊢ (𝜑 → 𝑈 ∈ ℝ+) & ⊢ (𝜑 → 𝑀 ≤ 𝑈) & ⊢ (𝜑 → 𝑈 ≤ (𝐼 + 1)) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐽 ∈ (ℤ≥‘𝐼)) ⇒ ⊢ (𝜑 → (abs‘((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼))) ≤ ((2 · 𝑅) · ⦋𝑈 / 𝑛⦌𝐴)) | ||
| Theorem | dchrisumlem3 27535* | Lemma for dchrisum 27536. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝𝑟 0) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴)) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ (𝜑 → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) ⇒ ⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵))) | ||
| Theorem | dchrisum 27536* | If 𝑛 ∈ [𝑀, +∞) ↦ 𝐴(𝑛) is a positive decreasing function approaching zero, then the infinite sum Σ𝑛, 𝑋(𝑛)𝐴(𝑛) is convergent, with the partial sum Σ𝑛 ≤ 𝑥, 𝑋(𝑛)𝐴(𝑛) within 𝑂(𝐴(𝑀)) of the limit 𝑇. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝𝑟 0) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴)) ⇒ ⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵))) | ||
| Theorem | dchrmusumlema 27537* | Lemma for dchrmusum 27568 and dchrisumn0 27565. Apply dchrisum 27536 for the function 1 / 𝑦. (Contributed by Mario Carneiro, 4-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) ⇒ ⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦))) | ||
| Theorem | dchrmusum2 27538* | The sum of the Möbius function multiplied by a non-principal Dirichlet character, divided by 𝑛, is bounded, provided that 𝑇 ≠ 0. Lemma 9.4.2 of [Shapiro], p. 380. (Contributed by Mario Carneiro, 4-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑇) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐶 / 𝑦)) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · 𝑇)) ∈ 𝑂(1)) | ||
| Theorem | dchrvmasumlem1 27539* | An alternative expression for a Dirichlet-weighted von Mangoldt sum in terms of the Möbius function. Equation 9.4.11 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 3-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))((𝑋‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) = Σ𝑑 ∈ (1...(⌊‘𝐴))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))((𝑋‘(𝐿‘𝑚)) · ((log‘𝑚) / 𝑚)))) | ||
| Theorem | dchrvmasum2lem 27540* | Give an expression for log𝑥 remarkably similar to Σ𝑛 ≤ 𝑥(𝑋(𝑛)Λ(𝑛) / 𝑛) given in dchrvmasumlem1 27539. Part of Lemma 9.4.3 of [Shapiro], p. 380. (Contributed by Mario Carneiro, 4-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 1 ≤ 𝐴) ⇒ ⊢ (𝜑 → (log‘𝐴) = Σ𝑑 ∈ (1...(⌊‘𝐴))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))((𝑋‘(𝐿‘𝑚)) · ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚)))) | ||
| Theorem | dchrvmasum2if 27541* | Combine the results of dchrvmasumlem1 27539 and dchrvmasum2lem 27540 inside a conditional. (Contributed by Mario Carneiro, 4-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 1 ≤ 𝐴) ⇒ ⊢ (𝜑 → (Σ𝑛 ∈ (1...(⌊‘𝐴))((𝑋‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝜓, (log‘𝐴), 0)) = Σ𝑑 ∈ (1...(⌊‘𝐴))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))((𝑋‘(𝐿‘𝑚)) · ((log‘if(𝜓, (𝐴 / 𝑑), 𝑚)) / 𝑚)))) | ||
| Theorem | dchrvmasumlem2 27542* | Lemma for dchrvmasum 27569. (Contributed by Mario Carneiro, 4-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) → 𝐹 ∈ ℂ) & ⊢ (𝑚 = (𝑥 / 𝑑) → 𝐹 = 𝐾) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → 𝑇 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → (abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚))) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ (𝜑 → ∀𝑚 ∈ (1[,)3)(abs‘(𝐹 − 𝑇)) ≤ 𝑅) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ∈ 𝑂(1)) | ||
| Theorem | dchrvmasumlem3 27543* | Lemma for dchrvmasum 27569. (Contributed by Mario Carneiro, 3-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) → 𝐹 ∈ ℂ) & ⊢ (𝑚 = (𝑥 / 𝑑) → 𝐹 = 𝐾) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → 𝑇 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → (abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚))) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ (𝜑 → ∀𝑚 ∈ (1[,)3)(abs‘(𝐹 − 𝑇)) ≤ 𝑅) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ∈ 𝑂(1)) | ||
| Theorem | dchrvmasumlema 27544* | Lemma for dchrvmasum 27569 and dchrvmasumif 27547. Apply dchrisum 27536 for the function log(𝑦) / 𝑦, which is decreasing above e (or above 3, the nearest integer bound). (Contributed by Mario Carneiro, 5-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · ((log‘𝑎) / 𝑎))) ⇒ ⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑦 ∈ (3[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 · ((log‘𝑦) / 𝑦)))) | ||
| Theorem | dchrvmasumiflem1 27545* | Lemma for dchrvmasumif 27547. (Contributed by Mario Carneiro, 5-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / 𝑦)) & ⊢ 𝐾 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · ((log‘𝑎) / 𝑎))) & ⊢ (𝜑 → 𝐸 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐾) ⇝ 𝑇) & ⊢ (𝜑 → ∀𝑦 ∈ (3[,)+∞)(abs‘((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐸 · ((log‘𝑦) / 𝑦))) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑑)))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, (𝑥 / 𝑑), 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)))) ∈ 𝑂(1)) | ||
| Theorem | dchrvmasumiflem2 27546* | Lemma for dchrvmasum 27569. (Contributed by Mario Carneiro, 5-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / 𝑦)) & ⊢ 𝐾 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · ((log‘𝑎) / 𝑎))) & ⊢ (𝜑 → 𝐸 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐾) ⇝ 𝑇) & ⊢ (𝜑 → ∀𝑦 ∈ (3[,)+∞)(abs‘((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐸 · ((log‘𝑦) / 𝑦))) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑆 = 0, (log‘𝑥), 0))) ∈ 𝑂(1)) | ||
| Theorem | dchrvmasumif 27547* | An asymptotic approximation for the sum of 𝑋(𝑛)Λ(𝑛) / 𝑛 conditional on the value of the infinite sum 𝑆. (We will later show that the case 𝑆 = 0 is impossible, and hence establish dchrvmasum 27569.) (Contributed by Mario Carneiro, 5-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / 𝑦)) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑆 = 0, (log‘𝑥), 0))) ∈ 𝑂(1)) | ||
| Theorem | dchrvmaeq0 27548* | The set 𝑊 is the collection of all non-principal Dirichlet characters such that the sum Σ𝑛 ∈ ℕ, 𝑋(𝑛) / 𝑛 is equal to zero. (Contributed by Mario Carneiro, 5-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / 𝑦)) & ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝑊 ↔ 𝑆 = 0)) | ||
| Theorem | dchrisum0fval 27549* | Value of the function 𝐹, the divisor sum of a Dirichlet character. (Contributed by Mario Carneiro, 5-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝐹 = (𝑏 ∈ ℕ ↦ Σ𝑣 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏} (𝑋‘(𝐿‘𝑣))) ⇒ ⊢ (𝐴 ∈ ℕ → (𝐹‘𝐴) = Σ𝑡 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴} (𝑋‘(𝐿‘𝑡))) | ||
| Theorem | dchrisum0fmul 27550* | The function 𝐹, the divisor sum of a Dirichlet character, is a multiplicative function (but not completely multiplicative). Equation 9.4.27 of [Shapiro], p. 382. (Contributed by Mario Carneiro, 5-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝐹 = (𝑏 ∈ ℕ ↦ Σ𝑣 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏} (𝑋‘(𝐿‘𝑣))) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) ⇒ ⊢ (𝜑 → (𝐹‘(𝐴 · 𝐵)) = ((𝐹‘𝐴) · (𝐹‘𝐵))) | ||
| Theorem | dchrisum0ff 27551* | The function 𝐹 is a real function. (Contributed by Mario Carneiro, 5-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝐹 = (𝑏 ∈ ℕ ↦ Σ𝑣 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏} (𝑋‘(𝐿‘𝑣))) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℝ) ⇒ ⊢ (𝜑 → 𝐹:ℕ⟶ℝ) | ||
| Theorem | dchrisum0flblem1 27552* | Lemma for dchrisum0flb 27554. Base case, prime power. (Contributed by Mario Carneiro, 5-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝐹 = (𝑏 ∈ ℕ ↦ Σ𝑣 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏} (𝑋‘(𝐿‘𝑣))) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℝ) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐴 ∈ ℕ0) ⇒ ⊢ (𝜑 → if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) ≤ (𝐹‘(𝑃↑𝐴))) | ||
| Theorem | dchrisum0flblem2 27553* | Lemma for dchrisum0flb 27554. Induction over relatively prime factors, with the prime power case handled in dchrisum0flblem1 . (Contributed by Mario Carneiro, 5-May-2016.) Replace reference to OLD theorem. (Revised by Wolf Lammen, 8-Sep-2020.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝐹 = (𝑏 ∈ ℕ ↦ Σ𝑣 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏} (𝑋‘(𝐿‘𝑣))) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℝ) & ⊢ (𝜑 → 𝐴 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑃 ∥ 𝐴) & ⊢ (𝜑 → ∀𝑦 ∈ (1..^𝐴)if((√‘𝑦) ∈ ℕ, 1, 0) ≤ (𝐹‘𝑦)) ⇒ ⊢ (𝜑 → if((√‘𝐴) ∈ ℕ, 1, 0) ≤ (𝐹‘𝐴)) | ||
| Theorem | dchrisum0flb 27554* | The divisor sum of a real Dirichlet character, is lower bounded by zero everywhere and one at the squares. Equation 9.4.29 of [Shapiro], p. 382. (Contributed by Mario Carneiro, 5-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝐹 = (𝑏 ∈ ℕ ↦ Σ𝑣 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏} (𝑋‘(𝐿‘𝑣))) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℝ) & ⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → if((√‘𝐴) ∈ ℕ, 1, 0) ≤ (𝐹‘𝐴)) | ||
| Theorem | dchrisum0fno1 27555* | The sum Σ𝑘 ≤ 𝑥, 𝐹(𝑥) / √𝑘 is divergent (i.e. not eventually bounded). Equation 9.4.30 of [Shapiro], p. 383. (Contributed by Mario Carneiro, 5-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝐹 = (𝑏 ∈ ℕ ↦ Σ𝑣 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏} (𝑋‘(𝐿‘𝑣))) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℝ) & ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑘 ∈ (1...(⌊‘𝑥))((𝐹‘𝑘) / (√‘𝑘))) ∈ 𝑂(1)) ⇒ ⊢ ¬ 𝜑 | ||
| Theorem | rpvmasum2 27556* | A partial result along the lines of rpvmasum 27570. The sum of the von Mangoldt function over those integers 𝑛≡𝐴 (mod 𝑁) is asymptotic to (1 − 𝑀)(log𝑥 / ϕ(𝑥)) + 𝑂(1), where 𝑀 is the number of non-principal Dirichlet characters with Σ𝑛 ∈ ℕ, 𝑋(𝑛) / 𝑛 = 0. Our goal is to show this set is empty. Equation 9.4.3 of [Shapiro], p. 375. (Contributed by Mario Carneiro, 5-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} & ⊢ 𝑈 = (Unit‘𝑍) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ 𝑇 = (◡𝐿 “ {𝐴}) & ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑊) → 𝐴 = (1r‘𝑍)) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊))))) ∈ 𝑂(1)) | ||
| Theorem | dchrisum0re 27557* | Suppose 𝑋 is a non-principal Dirichlet character with Σ𝑛 ∈ ℕ, 𝑋(𝑛) / 𝑛 = 0. Then 𝑋 is a real character. Part of Lemma 9.4.4 of [Shapiro], p. 382. (Contributed by Mario Carneiro, 5-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} & ⊢ (𝜑 → 𝑋 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℝ) | ||
| Theorem | dchrisum0lema 27558* | Lemma for dchrisum0 27564. Apply dchrisum 27536 for the function 1 / √𝑦. (Contributed by Mario Carneiro, 10-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} & ⊢ (𝜑 → 𝑋 ∈ 𝑊) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) ⇒ ⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦)))) | ||
| Theorem | dchrisum0lem1b 27559* | Lemma for dchrisum0lem1 27560. (Contributed by Mario Carneiro, 7-Jun-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} & ⊢ (𝜑 → 𝑋 ∈ 𝑊) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦))) ⇒ ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ≤ ((2 · 𝐶) / (√‘𝑥))) | ||
| Theorem | dchrisum0lem1 27560* | Lemma for dchrisum0 27564. (Contributed by Mario Carneiro, 12-May-2016.) (Revised by Mario Carneiro, 7-Jun-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} & ⊢ (𝜑 → 𝑋 ∈ 𝑊) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦))) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1)) | ||
| Theorem | dchrisum0lem2a 27561* | Lemma for dchrisum0 27564. (Contributed by Mario Carneiro, 12-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} & ⊢ (𝜑 → 𝑋 ∈ 𝑊) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦))) & ⊢ 𝐻 = (𝑦 ∈ ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑦))(1 / (√‘𝑑)) − (2 · (√‘𝑦)))) & ⊢ (𝜑 → 𝐻 ⇝𝑟 𝑈) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚)))) ∈ 𝑂(1)) | ||
| Theorem | dchrisum0lem2 27562* | Lemma for dchrisum0 27564. (Contributed by Mario Carneiro, 12-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} & ⊢ (𝜑 → 𝑋 ∈ 𝑊) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦))) & ⊢ 𝐻 = (𝑦 ∈ ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑦))(1 / (√‘𝑑)) − (2 · (√‘𝑦)))) & ⊢ (𝜑 → 𝐻 ⇝𝑟 𝑈) & ⊢ 𝐾 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) & ⊢ (𝜑 → 𝐸 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐾) ⇝ 𝑇) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐸 / 𝑦)) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1)) | ||
| Theorem | dchrisum0lem3 27563* | Lemma for dchrisum0 27564. (Contributed by Mario Carneiro, 12-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} & ⊢ (𝜑 → 𝑋 ∈ 𝑊) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦))) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ 𝑂(1)) | ||
| Theorem | dchrisum0 27564* | The sum Σ𝑛 ∈ ℕ, 𝑋(𝑛) / 𝑛 is nonzero for all non-principal Dirichlet characters (i.e. the assumption 𝑋 ∈ 𝑊 is contradictory). This is the key result that allows to eliminate the conditionals from dchrmusum2 27538 and dchrvmasumif 27547. Lemma 9.4.4 of [Shapiro], p. 382. (Contributed by Mario Carneiro, 12-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} & ⊢ (𝜑 → 𝑋 ∈ 𝑊) ⇒ ⊢ ¬ 𝜑 | ||
| Theorem | dchrisumn0 27565* | The sum Σ𝑛 ∈ ℕ, 𝑋(𝑛) / 𝑛 is nonzero for all non-principal Dirichlet characters (i.e. the assumption 𝑋 ∈ 𝑊 is contradictory). This is the key result that allows to eliminate the conditionals from dchrmusum2 27538 and dchrvmasumif 27547. Lemma 9.4.4 of [Shapiro], p. 382. (Contributed by Mario Carneiro, 12-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑇) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐶 / 𝑦)) ⇒ ⊢ (𝜑 → 𝑇 ≠ 0) | ||
| Theorem | dchrmusumlem 27566* | The sum of the Möbius function multiplied by a non-principal Dirichlet character, divided by 𝑛, is bounded. Equation 9.4.16 of [Shapiro], p. 379. (Contributed by Mario Carneiro, 12-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑇) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐶 / 𝑦)) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑛)) · ((μ‘𝑛) / 𝑛))) ∈ 𝑂(1)) | ||
| Theorem | dchrvmasumlem 27567* | The sum of the Möbius function multiplied by a non-principal Dirichlet character, divided by 𝑛, is bounded. Equation 9.4.16 of [Shapiro], p. 379. (Contributed by Mario Carneiro, 12-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑇) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐶 / 𝑦)) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) ∈ 𝑂(1)) | ||
| Theorem | dchrmusum 27568* | The sum of the Möbius function multiplied by a non-principal Dirichlet character, divided by 𝑛, is bounded. Equation 9.4.16 of [Shapiro], p. 379. (Contributed by Mario Carneiro, 12-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑛)) · ((μ‘𝑛) / 𝑛))) ∈ 𝑂(1)) | ||
| Theorem | dchrvmasum 27569* | The sum of the von Mangoldt function multiplied by a non-principal Dirichlet character, divided by 𝑛, is bounded. Equation 9.4.8 of [Shapiro], p. 376. (Contributed by Mario Carneiro, 12-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) ∈ 𝑂(1)) | ||
| Theorem | rpvmasum 27570* | The sum of the von Mangoldt function over those integers 𝑛≡𝐴 (mod 𝑁) is asymptotic to log𝑥 / ϕ(𝑥) + 𝑂(1). Equation 9.4.3 of [Shapiro], p. 375. (Contributed by Mario Carneiro, 2-May-2016.) (Proof shortened by Mario Carneiro, 26-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑈 = (Unit‘𝑍) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ 𝑇 = (◡𝐿 “ {𝐴}) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) ∈ 𝑂(1)) | ||
| Theorem | rplogsum 27571* | The sum of log𝑝 / 𝑝 over the primes 𝑝≡𝐴 (mod 𝑁) is asymptotic to log𝑥 / ϕ(𝑥) + 𝑂(1). Equation 9.4.3 of [Shapiro], p. 375. (Contributed by Mario Carneiro, 16-Apr-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑈 = (Unit‘𝑍) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ 𝑇 = (◡𝐿 “ {𝐴}) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝)) − (log‘𝑥))) ∈ 𝑂(1)) | ||
| Theorem | dirith2 27572 | Dirichlet's theorem: there are infinitely many primes in any arithmetic progression coprime to 𝑁. Theorem 9.4.1 of [Shapiro], p. 375. (Contributed by Mario Carneiro, 30-Apr-2016.) (Proof shortened by Mario Carneiro, 26-May-2016.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑈 = (Unit‘𝑍) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ 𝑇 = (◡𝐿 “ {𝐴}) ⇒ ⊢ (𝜑 → (ℙ ∩ 𝑇) ≈ ℕ) | ||
| Theorem | dirith 27573* | Dirichlet's theorem: there are infinitely many primes in any arithmetic progression coprime to 𝑁. Theorem 9.4.1 of [Shapiro], p. 375. See https://metamath-blog.blogspot.com/2016/05/dirichlets-theorem.html for an informal exposition. This is Metamath 100 proof #48. (Contributed by Mario Carneiro, 12-May-2016.) |
| ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) → {𝑝 ∈ ℙ ∣ 𝑁 ∥ (𝑝 − 𝐴)} ≈ ℕ) | ||
| Theorem | mudivsum 27574* | Asymptotic formula for Σ𝑛 ≤ 𝑥, μ(𝑛) / 𝑛 = 𝑂(1). Equation 10.2.1 of [Shapiro], p. 405. (Contributed by Mario Carneiro, 14-May-2016.) |
| ⊢ (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ 𝑂(1) | ||
| Theorem | mulogsumlem 27575* | Lemma for mulogsum 27576. (Contributed by Mario Carneiro, 14-May-2016.) |
| ⊢ (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))))) ∈ 𝑂(1) | ||
| Theorem | mulogsum 27576* | Asymptotic formula for Σ𝑛 ≤ 𝑥, (μ(𝑛) / 𝑛)log(𝑥 / 𝑛) = 𝑂(1). Equation 10.2.6 of [Shapiro], p. 406. (Contributed by Mario Carneiro, 14-May-2016.) |
| ⊢ (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) ∈ 𝑂(1) | ||
| Theorem | logdivsum 27577* | Asymptotic analysis of Σ𝑛 ≤ 𝑥, log𝑛 / 𝑛 = (log𝑥)↑2 / 2 + 𝐿 + 𝑂(log𝑥 / 𝑥). (Contributed by Mario Carneiro, 18-May-2016.) |
| ⊢ 𝐹 = (𝑦 ∈ ℝ+ ↦ (Σ𝑖 ∈ (1...(⌊‘𝑦))((log‘𝑖) / 𝑖) − (((log‘𝑦)↑2) / 2))) ⇒ ⊢ (𝐹:ℝ+⟶ℝ ∧ 𝐹 ∈ dom ⇝𝑟 ∧ ((𝐹 ⇝𝑟 𝐿 ∧ 𝐴 ∈ ℝ+ ∧ e ≤ 𝐴) → (abs‘((𝐹‘𝐴) − 𝐿)) ≤ ((log‘𝐴) / 𝐴))) | ||
| Theorem | mulog2sumlem1 27578* | Asymptotic formula for Σ𝑛 ≤ 𝑥, log(𝑥 / 𝑛) / 𝑛 = (1 / 2)log↑2(𝑥) + γ · log𝑥 − 𝐿 + 𝑂(log𝑥 / 𝑥), with explicit constants. Equation 10.2.7 of [Shapiro], p. 407. (Contributed by Mario Carneiro, 18-May-2016.) |
| ⊢ 𝐹 = (𝑦 ∈ ℝ+ ↦ (Σ𝑖 ∈ (1...(⌊‘𝑦))((log‘𝑖) / 𝑖) − (((log‘𝑦)↑2) / 2))) & ⊢ (𝜑 → 𝐹 ⇝𝑟 𝐿) & ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → e ≤ 𝐴) ⇒ ⊢ (𝜑 → (abs‘(Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘(𝐴 / 𝑚)) / 𝑚) − ((((log‘𝐴)↑2) / 2) + ((γ · (log‘𝐴)) − 𝐿)))) ≤ (2 · ((log‘𝐴) / 𝐴))) | ||
| Theorem | mulog2sumlem2 27579* | Lemma for mulog2sum 27581. (Contributed by Mario Carneiro, 19-May-2016.) |
| ⊢ 𝐹 = (𝑦 ∈ ℝ+ ↦ (Σ𝑖 ∈ (1...(⌊‘𝑦))((log‘𝑖) / 𝑖) − (((log‘𝑦)↑2) / 2))) & ⊢ (𝜑 → 𝐹 ⇝𝑟 𝐿) & ⊢ 𝑇 = ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) & ⊢ 𝑅 = (((1 / 2) + (γ + (abs‘𝐿))) + Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚)) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ∈ 𝑂(1)) | ||
| Theorem | mulog2sumlem3 27580* | Lemma for mulog2sum 27581. (Contributed by Mario Carneiro, 13-May-2016.) |
| ⊢ 𝐹 = (𝑦 ∈ ℝ+ ↦ (Σ𝑖 ∈ (1...(⌊‘𝑦))((log‘𝑖) / 𝑖) − (((log‘𝑦)↑2) / 2))) & ⊢ (𝜑 → 𝐹 ⇝𝑟 𝐿) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) − (2 · (log‘𝑥)))) ∈ 𝑂(1)) | ||
| Theorem | mulog2sum 27581* | Asymptotic formula for Σ𝑛 ≤ 𝑥, (μ(𝑛) / 𝑛)log↑2(𝑥 / 𝑛) = 2log𝑥 + 𝑂(1). Equation 10.2.8 of [Shapiro], p. 407. (Contributed by Mario Carneiro, 19-May-2016.) |
| ⊢ (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) − (2 · (log‘𝑥)))) ∈ 𝑂(1) | ||
| Theorem | vmalogdivsum2 27582* | The sum Σ𝑛 ≤ 𝑥, Λ(𝑛)log(𝑥 / 𝑛) / 𝑛 is asymptotic to log↑2(𝑥) / 2 + 𝑂(log𝑥). Exercise 9.1.7 of [Shapiro], p. 336. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1) | ||
| Theorem | vmalogdivsum 27583* | The sum Σ𝑛 ≤ 𝑥, Λ(𝑛)log𝑛 / 𝑛 is asymptotic to log↑2(𝑥) / 2 + 𝑂(log𝑥). Exercise 9.1.7 of [Shapiro], p. 336. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘𝑛)) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1) | ||
| Theorem | 2vmadivsumlem 27584* | Lemma for 2vmadivsum 27585. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘(Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) / 𝑖) − (log‘𝑦))) ≤ 𝐴) ⇒ ⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1)) | ||
| Theorem | 2vmadivsum 27585* | The sum Σ𝑚𝑛 ≤ 𝑥, Λ(𝑚)Λ(𝑛) / 𝑚𝑛 is asymptotic to log↑2(𝑥) / 2 + 𝑂(log𝑥). (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1) | ||
| Theorem | logsqvma 27586* | A formula for log↑2(𝑁) in terms of the primes. Equation 10.4.6 of [Shapiro], p. 418. (Contributed by Mario Carneiro, 13-May-2016.) |
| ⊢ (𝑁 ∈ ℕ → Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (Σ𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑} ((Λ‘𝑢) · (Λ‘(𝑑 / 𝑢))) + ((Λ‘𝑑) · (log‘𝑑))) = ((log‘𝑁)↑2)) | ||
| Theorem | logsqvma2 27587* | The Möbius inverse of logsqvma 27586. Equation 10.4.8 of [Shapiro], p. 418. (Contributed by Mario Carneiro, 13-May-2016.) |
| ⊢ (𝑁 ∈ ℕ → Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ((μ‘𝑑) · ((log‘(𝑁 / 𝑑))↑2)) = (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ((Λ‘𝑑) · (Λ‘(𝑁 / 𝑑))) + ((Λ‘𝑁) · (log‘𝑁)))) | ||
| Theorem | log2sumbnd 27588* | Bound on the difference between Σ𝑛 ≤ 𝐴, log↑2(𝑛) and the equivalent integral. (Contributed by Mario Carneiro, 20-May-2016.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛)↑2) − (𝐴 · (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴))))))) ≤ (((log‘𝐴)↑2) + 2)) | ||
| Theorem | selberglem1 27589* | Lemma for selberg 27592. Estimation of the asymptotic part of selberglem3 27591. (Contributed by Mario Carneiro, 20-May-2016.) |
| ⊢ 𝑇 = ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛) ⇒ ⊢ (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) ∈ 𝑂(1) | ||
| Theorem | selberglem2 27590* | Lemma for selberg 27592. (Contributed by Mario Carneiro, 23-May-2016.) |
| ⊢ 𝑇 = ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛) ⇒ ⊢ (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1) | ||
| Theorem | selberglem3 27591* | Lemma for selberg 27592. Estimation of the left-hand side of logsqvma2 27587. (Contributed by Mario Carneiro, 23-May-2016.) |
| ⊢ (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((μ‘𝑑) · ((log‘(𝑛 / 𝑑))↑2)) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1) | ||
| Theorem | selberg 27592* | Selberg's symmetry formula. The statement has many forms, and this one is equivalent to the statement that Σ𝑛 ≤ 𝑥, Λ(𝑛)log𝑛 + Σ𝑚 · 𝑛 ≤ 𝑥, Λ(𝑚)Λ(𝑛) = 2𝑥log𝑥 + 𝑂(𝑥). Equation 10.4.10 of [Shapiro], p. 419. (Contributed by Mario Carneiro, 23-May-2016.) |
| ⊢ (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1) | ||
| Theorem | selbergb 27593* | Convert eventual boundedness in selberg 27592 to boundedness on [1, +∞). (We have to bound away from zero because the log terms diverge at zero.) (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ (1[,)+∞)(abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ≤ 𝑐 | ||
| Theorem | selberg2lem 27594* | Lemma for selberg2 27595. Equation 10.4.12 of [Shapiro], p. 420. (Contributed by Mario Carneiro, 23-May-2016.) |
| ⊢ (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))) / 𝑥)) ∈ 𝑂(1) | ||
| Theorem | selberg2 27595* | Selberg's symmetry formula, using the second Chebyshev function. Equation 10.4.14 of [Shapiro], p. 420. (Contributed by Mario Carneiro, 23-May-2016.) |
| ⊢ (𝑥 ∈ ℝ+ ↦ (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1) | ||
| Theorem | selberg2b 27596* | Convert eventual boundedness in selberg2 27595 to boundedness on any interval [𝐴, +∞). (We have to bound away from zero because the log terms diverge at zero.) (Contributed by Mario Carneiro, 25-May-2016.) |
| ⊢ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ (1[,)+∞)(abs‘(((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ≤ 𝑐 | ||
| Theorem | chpdifbndlem1 27597* | Lemma for chpdifbnd 27599. (Contributed by Mario Carneiro, 25-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 1 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → ∀𝑧 ∈ (1[,)+∞)(abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) ≤ 𝐵) & ⊢ 𝐶 = ((𝐵 · (𝐴 + 1)) + ((2 · 𝐴) · (log‘𝐴))) & ⊢ (𝜑 → 𝑋 ∈ (1(,)+∞)) & ⊢ (𝜑 → 𝑌 ∈ (𝑋[,](𝐴 · 𝑋))) ⇒ ⊢ (𝜑 → ((ψ‘𝑌) − (ψ‘𝑋)) ≤ ((2 · (𝑌 − 𝑋)) + (𝐶 · (𝑋 / (log‘𝑋))))) | ||
| Theorem | chpdifbndlem2 27598* | Lemma for chpdifbnd 27599. (Contributed by Mario Carneiro, 25-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 1 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → ∀𝑧 ∈ (1[,)+∞)(abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) ≤ 𝐵) & ⊢ 𝐶 = ((𝐵 · (𝐴 + 1)) + ((2 · 𝐴) · (log‘𝐴))) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ (1(,)+∞)∀𝑦 ∈ (𝑥[,](𝐴 · 𝑥))((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦 − 𝑥)) + (𝑐 · (𝑥 / (log‘𝑥))))) | ||
| Theorem | chpdifbnd 27599* | A bound on the difference of nearby ψ values. Theorem 10.5.2 of [Shapiro], p. 427. (Contributed by Mario Carneiro, 25-May-2016.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ (1(,)+∞)∀𝑦 ∈ (𝑥[,](𝐴 · 𝑥))((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦 − 𝑥)) + (𝑐 · (𝑥 / (log‘𝑥))))) | ||
| Theorem | logdivbnd 27600* | A bound on a sum of logs, used in pntlemk 27650. This is not as precise as logdivsum 27577 in its asymptotic behavior, but it is valid for all 𝑁 and does not require a limit value. (Contributed by Mario Carneiro, 13-Apr-2016.) |
| ⊢ (𝑁 ∈ ℕ → Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛) ≤ ((((log‘𝑁) + 1)↑2) / 2)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |