Home | Metamath
Proof Explorer Theorem List (p. 246 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | o1cxp 24501* | An eventually bounded function taken to a nonnegative power is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 0 ≤ (ℜ‘𝐶)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵↑𝑐𝐶)) ∈ 𝑂(1)) | ||
Theorem | cxp2limlem 24502* | A linear factor grows slower than any exponential with base greater than 1. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 1 < 𝐴) → (𝑛 ∈ ℝ+ ↦ (𝑛 / (𝐴↑𝑐𝑛))) ⇝𝑟 0) | ||
Theorem | cxp2lim 24503* | Any power grows slower than any exponential with base greater than 1. (Contributed by Mario Carneiro, 18-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → (𝑛 ∈ ℝ+ ↦ ((𝑛↑𝑐𝐴) / (𝐵↑𝑐𝑛))) ⇝𝑟 0) | ||
Theorem | cxploglim 24504* | The logarithm grows slower than any positive power. (Contributed by Mario Carneiro, 18-Sep-2014.) |
⊢ (𝐴 ∈ ℝ+ → (𝑛 ∈ ℝ+ ↦ ((log‘𝑛) / (𝑛↑𝑐𝐴))) ⇝𝑟 0) | ||
Theorem | cxploglim2 24505* | Every power of the logarithm grows slower than any positive power. (Contributed by Mario Carneiro, 20-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+) → (𝑛 ∈ ℝ+ ↦ (((log‘𝑛)↑𝑐𝐴) / (𝑛↑𝑐𝐵))) ⇝𝑟 0) | ||
Theorem | divsqrtsumlem 24506* | Lemma for divsqrsum 24508 and divsqrtsum2 24509. (Contributed by Mario Carneiro, 18-May-2016.) |
⊢ 𝐹 = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑛)) − (2 · (√‘𝑥)))) ⇒ ⊢ (𝐹:ℝ+⟶ℝ ∧ 𝐹 ∈ dom ⇝𝑟 ∧ ((𝐹 ⇝𝑟 𝐿 ∧ 𝐴 ∈ ℝ+) → (abs‘((𝐹‘𝐴) − 𝐿)) ≤ (1 / (√‘𝐴)))) | ||
Theorem | divsqrsumf 24507* | The function 𝐹 used in divsqrsum 24508 is a real function. (Contributed by Mario Carneiro, 12-May-2016.) |
⊢ 𝐹 = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑛)) − (2 · (√‘𝑥)))) ⇒ ⊢ 𝐹:ℝ+⟶ℝ | ||
Theorem | divsqrsum 24508* | The sum Σ𝑛 ≤ 𝑥(1 / √𝑛) is asymptotic to 2√𝑥 + 𝐿 with a finite limit 𝐿. (In fact, this limit is ζ(1 / 2) ≈ -1.46....) (Contributed by Mario Carneiro, 9-May-2016.) |
⊢ 𝐹 = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑛)) − (2 · (√‘𝑥)))) ⇒ ⊢ 𝐹 ∈ dom ⇝𝑟 | ||
Theorem | divsqrtsum2 24509* | A bound on the distance of the sum Σ𝑛 ≤ 𝑥(1 / √𝑛) from its asymptotic value 2√𝑥 + 𝐿. (Contributed by Mario Carneiro, 18-May-2016.) |
⊢ 𝐹 = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑛)) − (2 · (√‘𝑥)))) & ⊢ (𝜑 → 𝐹 ⇝𝑟 𝐿) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ ℝ+) → (abs‘((𝐹‘𝐴) − 𝐿)) ≤ (1 / (√‘𝐴))) | ||
Theorem | divsqrtsumo1 24510* | The sum Σ𝑛 ≤ 𝑥(1 / √𝑛) has the asymptotic expansion 2√𝑥 + 𝐿 + 𝑂(1 / √𝑥), for some 𝐿. (Contributed by Mario Carneiro, 10-May-2016.) |
⊢ 𝐹 = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑛)) − (2 · (√‘𝑥)))) & ⊢ (𝜑 → 𝐹 ⇝𝑟 𝐿) ⇒ ⊢ (𝜑 → (𝑦 ∈ ℝ+ ↦ (((𝐹‘𝑦) − 𝐿) · (√‘𝑦))) ∈ 𝑂(1)) | ||
Theorem | cvxcl 24511* | Closure of a 0-1 linear combination in a convex set. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → (𝑥[,]𝑦) ⊆ 𝐷) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) ∈ 𝐷) | ||
Theorem | scvxcvx 24512* | A strictly convex function is convex. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝐷⟶ℝ) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ≤ ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))) | ||
Theorem | jensenlem1 24513* | Lemma for jensen 24515. (Contributed by Mario Carneiro, 4-Jun-2016.) |
⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝐷⟶ℝ) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝑇:𝐴⟶(0[,)+∞)) & ⊢ (𝜑 → 𝑋:𝐴⟶𝐷) & ⊢ (𝜑 → 0 < (ℂfld Σg 𝑇)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑡 ∈ (0[,]1))) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))) & ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐵) & ⊢ (𝜑 → (𝐵 ∪ {𝑧}) ⊆ 𝐴) & ⊢ 𝑆 = (ℂfld Σg (𝑇 ↾ 𝐵)) & ⊢ 𝐿 = (ℂfld Σg (𝑇 ↾ (𝐵 ∪ {𝑧}))) ⇒ ⊢ (𝜑 → 𝐿 = (𝑆 + (𝑇‘𝑧))) | ||
Theorem | jensenlem2 24514* | Lemma for jensen 24515. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝐷⟶ℝ) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝑇:𝐴⟶(0[,)+∞)) & ⊢ (𝜑 → 𝑋:𝐴⟶𝐷) & ⊢ (𝜑 → 0 < (ℂfld Σg 𝑇)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑡 ∈ (0[,]1))) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))) & ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐵) & ⊢ (𝜑 → (𝐵 ∪ {𝑧}) ⊆ 𝐴) & ⊢ 𝑆 = (ℂfld Σg (𝑇 ↾ 𝐵)) & ⊢ 𝐿 = (ℂfld Σg (𝑇 ↾ (𝐵 ∪ {𝑧}))) & ⊢ (𝜑 → 𝑆 ∈ ℝ+) & ⊢ (𝜑 → ((ℂfld Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆) ∈ 𝐷) & ⊢ (𝜑 → (𝐹‘((ℂfld Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) ≤ ((ℂfld Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) ⇒ ⊢ (𝜑 → (((ℂfld Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝐵 ∪ {𝑧}))) / 𝐿) ∈ 𝐷 ∧ (𝐹‘((ℂfld Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝐵 ∪ {𝑧}))) / 𝐿)) ≤ ((ℂfld Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝐵 ∪ {𝑧}))) / 𝐿))) | ||
Theorem | jensen 24515* | Jensen's inequality, a finite extension of the definition of convexity (the last hypothesis). (Contributed by Mario Carneiro, 21-Jun-2015.) (Proof shortened by AV, 27-Jul-2019.) |
⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝐷⟶ℝ) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝑇:𝐴⟶(0[,)+∞)) & ⊢ (𝜑 → 𝑋:𝐴⟶𝐷) & ⊢ (𝜑 → 0 < (ℂfld Σg 𝑇)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑡 ∈ (0[,]1))) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))) ⇒ ⊢ (𝜑 → (((ℂfld Σg (𝑇 ∘𝑓 · 𝑋)) / (ℂfld Σg 𝑇)) ∈ 𝐷 ∧ (𝐹‘((ℂfld Σg (𝑇 ∘𝑓 · 𝑋)) / (ℂfld Σg 𝑇))) ≤ ((ℂfld Σg (𝑇 ∘𝑓 · (𝐹 ∘ 𝑋))) / (ℂfld Σg 𝑇)))) | ||
Theorem | amgmlem 24516 | Lemma for amgm 24517. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ 𝑀 = (mulGrp‘ℂfld) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ+) ⇒ ⊢ (𝜑 → ((𝑀 Σg 𝐹)↑𝑐(1 / (#‘𝐴))) ≤ ((ℂfld Σg 𝐹) / (#‘𝐴))) | ||
Theorem | amgm 24517 | Inequality of arithmetic and geometric means. Here (𝑀 Σg 𝐹) calculates the group sum within the multiplicative monoid of the complex numbers (or in other words, it multiplies the elements 𝐹(𝑥), 𝑥 ∈ 𝐴 together), and (ℂfld Σg 𝐹) calculates the group sum in the additive group (i.e. the sum of the elements). This is Metamath 100 proof #38. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ 𝑀 = (mulGrp‘ℂfld) ⇒ ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) → ((𝑀 Σg 𝐹)↑𝑐(1 / (#‘𝐴))) ≤ ((ℂfld Σg 𝐹) / (#‘𝐴))) | ||
Syntax | cem 24518 | The Euler-Mascheroni constant. (The label abbreviates Euler-Mascheroni.) |
class γ | ||
Definition | df-em 24519 | Define the Euler-Mascheroni constant, γ = 0.577... . This is the limit of the series Σ𝑘 ∈ (1...𝑚)(1 / 𝑘) − (log‘𝑚), with a proof that the limit exists in emcl 24529. (Contributed by Mario Carneiro, 11-Jul-2014.) |
⊢ γ = Σ𝑘 ∈ ℕ ((1 / 𝑘) − (log‘(1 + (1 / 𝑘)))) | ||
Theorem | logdifbnd 24520 | Bound on the difference of logs. (Contributed by Mario Carneiro, 23-May-2016.) |
⊢ (𝐴 ∈ ℝ+ → ((log‘(𝐴 + 1)) − (log‘𝐴)) ≤ (1 / 𝐴)) | ||
Theorem | logdiflbnd 24521 | Lower bound on the difference of logs. (Contributed by Mario Carneiro, 3-Jul-2017.) |
⊢ (𝐴 ∈ ℝ+ → (1 / (𝐴 + 1)) ≤ ((log‘(𝐴 + 1)) − (log‘𝐴))) | ||
Theorem | emcllem1 24522* | Lemma for emcl 24529. The series 𝐹 and 𝐺 are sequences of real numbers that approach γ from above and below, respectively. (Contributed by Mario Carneiro, 11-Jul-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛))) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1)))) ⇒ ⊢ (𝐹:ℕ⟶ℝ ∧ 𝐺:ℕ⟶ℝ) | ||
Theorem | emcllem2 24523* | Lemma for emcl 24529. 𝐹 is increasing, and 𝐺 is decreasing. (Contributed by Mario Carneiro, 11-Jul-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛))) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1)))) ⇒ ⊢ (𝑁 ∈ ℕ → ((𝐹‘(𝑁 + 1)) ≤ (𝐹‘𝑁) ∧ (𝐺‘𝑁) ≤ (𝐺‘(𝑁 + 1)))) | ||
Theorem | emcllem3 24524* | Lemma for emcl 24529. The function 𝐻 is the difference between 𝐹 and 𝐺. (Contributed by Mario Carneiro, 11-Jul-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛))) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1)))) & ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (log‘(1 + (1 / 𝑛)))) ⇒ ⊢ (𝑁 ∈ ℕ → (𝐻‘𝑁) = ((𝐹‘𝑁) − (𝐺‘𝑁))) | ||
Theorem | emcllem4 24525* | Lemma for emcl 24529. The difference between series 𝐹 and 𝐺 tends to zero. (Contributed by Mario Carneiro, 11-Jul-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛))) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1)))) & ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (log‘(1 + (1 / 𝑛)))) ⇒ ⊢ 𝐻 ⇝ 0 | ||
Theorem | emcllem5 24526* | Lemma for emcl 24529. The partial sums of the series 𝑇, which is used in the definition df-em 24519, is in fact the same as 𝐺. (Contributed by Mario Carneiro, 11-Jul-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛))) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1)))) & ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (log‘(1 + (1 / 𝑛)))) & ⊢ 𝑇 = (𝑛 ∈ ℕ ↦ ((1 / 𝑛) − (log‘(1 + (1 / 𝑛))))) ⇒ ⊢ 𝐺 = seq1( + , 𝑇) | ||
Theorem | emcllem6 24527* | Lemma for emcl 24529. By the previous lemmas, 𝐹 and 𝐺 must approach a common limit, which is γ by definition. (Contributed by Mario Carneiro, 11-Jul-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛))) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1)))) & ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (log‘(1 + (1 / 𝑛)))) & ⊢ 𝑇 = (𝑛 ∈ ℕ ↦ ((1 / 𝑛) − (log‘(1 + (1 / 𝑛))))) ⇒ ⊢ (𝐹 ⇝ γ ∧ 𝐺 ⇝ γ) | ||
Theorem | emcllem7 24528* | Lemma for emcl 24529 and harmonicbnd 24530. Derive bounds on γ as 𝐹(1) and 𝐺(1). (Contributed by Mario Carneiro, 11-Jul-2014.) (Revised by Mario Carneiro, 9-Apr-2016.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛))) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1)))) & ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (log‘(1 + (1 / 𝑛)))) & ⊢ 𝑇 = (𝑛 ∈ ℕ ↦ ((1 / 𝑛) − (log‘(1 + (1 / 𝑛))))) ⇒ ⊢ (γ ∈ ((1 − (log‘2))[,]1) ∧ 𝐹:ℕ⟶(γ[,]1) ∧ 𝐺:ℕ⟶((1 − (log‘2))[,]γ)) | ||
Theorem | emcl 24529 | Closure and bounds for the Euler-Mascheroni constant. (Contributed by Mario Carneiro, 11-Jul-2014.) |
⊢ γ ∈ ((1 − (log‘2))[,]1) | ||
Theorem | harmonicbnd 24530* | A bound on the harmonic series, as compared to the natural logarithm. (Contributed by Mario Carneiro, 9-Apr-2016.) |
⊢ (𝑁 ∈ ℕ → (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘𝑁)) ∈ (γ[,]1)) | ||
Theorem | harmonicbnd2 24531* | A bound on the harmonic series, as compared to the natural logarithm. (Contributed by Mario Carneiro, 13-Apr-2016.) |
⊢ (𝑁 ∈ ℕ → (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘(𝑁 + 1))) ∈ ((1 − (log‘2))[,]γ)) | ||
Theorem | emre 24532 | The Euler-Mascheroni constant is a real number. (Contributed by Mario Carneiro, 11-Jul-2014.) |
⊢ γ ∈ ℝ | ||
Theorem | emgt0 24533 | The Euler-Mascheroni constant is positive. (Contributed by Mario Carneiro, 11-Jul-2014.) |
⊢ 0 < γ | ||
Theorem | harmonicbnd3 24534* | A bound on the harmonic series, as compared to the natural logarithm. (Contributed by Mario Carneiro, 13-Apr-2016.) |
⊢ (𝑁 ∈ ℕ0 → (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘(𝑁 + 1))) ∈ (0[,]γ)) | ||
Theorem | harmoniclbnd 24535* | A bound on the harmonic series, as compared to the natural logarithm. (Contributed by Mario Carneiro, 13-Apr-2016.) |
⊢ (𝐴 ∈ ℝ+ → (log‘𝐴) ≤ Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚)) | ||
Theorem | harmonicubnd 24536* | A bound on the harmonic series, as compared to the natural logarithm. (Contributed by Mario Carneiro, 13-Apr-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) ≤ ((log‘𝐴) + 1)) | ||
Theorem | harmonicbnd4 24537* | The asymptotic behavior of Σ𝑚 ≤ 𝐴, 1 / 𝑚 = log𝐴 + γ + 𝑂(1 / 𝐴). (Contributed by Mario Carneiro, 14-May-2016.) |
⊢ (𝐴 ∈ ℝ+ → (abs‘(Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − ((log‘𝐴) + γ))) ≤ (1 / 𝐴)) | ||
Theorem | fsumharmonic 24538* | Bound a finite sum based on the harmonic series, where the "strong" bound 𝐶 only applies asymptotically, and there is a "weak" bound 𝑅 for the remaining values. (Contributed by Mario Carneiro, 18-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → (𝑇 ∈ ℝ ∧ 1 ≤ 𝑇)) & ⊢ (𝜑 → (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅)) & ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 0 ≤ 𝐶) & ⊢ (((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ 𝑇 ≤ (𝐴 / 𝑛)) → (abs‘𝐵) ≤ (𝐶 · 𝑛)) & ⊢ (((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ (𝐴 / 𝑛) < 𝑇) → (abs‘𝐵) ≤ 𝑅) ⇒ ⊢ (𝜑 → (abs‘Σ𝑛 ∈ (1...(⌊‘𝐴))(𝐵 / 𝑛)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝐴))𝐶 + (𝑅 · ((log‘𝑇) + 1)))) | ||
Syntax | czeta 24539 | The Riemann zeta function. |
class ζ | ||
Definition | df-zeta 24540* | Define the Riemann zeta function. This definition uses a series expansion of the alternating zeta function ~? zetaalt that is convergent everywhere except 1, but going from the alternating zeta function to the regular zeta function requires dividing by 1 − 2↑(1 − 𝑠), which has zeroes other than 1. To extract the correct value of the zeta function at these points, we extend the divided alternating zeta function by continuity. (Contributed by Mario Carneiro, 18-Jul-2014.) |
⊢ ζ = (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))) | ||
Theorem | zetacvg 24541* | The zeta series is convergent. (Contributed by Mario Carneiro, 18-Jul-2014.) |
⊢ (𝜑 → 𝑆 ∈ ℂ) & ⊢ (𝜑 → 1 < (ℜ‘𝑆)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (𝑘↑𝑐-𝑆)) ⇒ ⊢ (𝜑 → seq1( + , 𝐹) ∈ dom ⇝ ) | ||
Syntax | clgam 24542 | Logarithm of the Gamma function. |
class log Γ | ||
Syntax | cgam 24543 | The Gamma function. |
class Γ | ||
Syntax | cigam 24544 | The inverse Gamma function. |
class 1/Γ | ||
Definition | df-lgam 24545* | Define the log-Gamma function. We can work with this form of the gamma function a bit easier than the equivalent expression for the gamma function itself, and moreover this function is not actually equal to log(Γ(𝑥)) because the branch cuts are placed differently (we do have exp(log Γ(𝑥)) = Γ(𝑥), though). This definition is attributed to Euler, and unlike the usual integral definition is defined on the entire complex plane except the nonpositive integers ℤ ∖ ℕ, where the function has simple poles. (Contributed by Mario Carneiro, 12-Jul-2014.) |
⊢ log Γ = (𝑧 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ↦ (Σ𝑚 ∈ ℕ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) − (log‘𝑧))) | ||
Definition | df-gam 24546 | Define the Gamma function. See df-lgam 24545 for more information about the reason for this definition in terms of the log-gamma function. (Contributed by Mario Carneiro, 12-Jul-2014.) |
⊢ Γ = (exp ∘ log Γ) | ||
Definition | df-igam 24547 | Define the inverse Gamma function, which is defined everywhere, unlike the Gamma function itself. (Contributed by Mario Carneiro, 16-Jul-2017.) |
⊢ 1/Γ = (𝑥 ∈ ℂ ↦ if(𝑥 ∈ (ℤ ∖ ℕ), 0, (1 / (Γ‘𝑥)))) | ||
Theorem | eldmgm 24548 | Elementhood in the set of non-nonpositive integers. (Contributed by Mario Carneiro, 12-Jul-2014.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ↔ (𝐴 ∈ ℂ ∧ ¬ -𝐴 ∈ ℕ0)) | ||
Theorem | dmgmaddn0 24549 | If 𝐴 is not a nonpositive integer, then 𝐴 + 𝑁 is nonzero for any nonnegative integer 𝑁. (Contributed by Mario Carneiro, 12-Jul-2014.) |
⊢ ((𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ∧ 𝑁 ∈ ℕ0) → (𝐴 + 𝑁) ≠ 0) | ||
Theorem | dmlogdmgm 24550 | If 𝐴 is in the continuous domain of the logarithm, then it is in the domain of the Gamma function. (Contributed by Mario Carneiro, 8-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (-∞(,]0)) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) | ||
Theorem | rpdmgm 24551 | A positive real number is in the domain of the Gamma function. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) | ||
Theorem | dmgmn0 24552 | If 𝐴 is not a nonpositive integer, then 𝐴 is nonzero. (Contributed by Mario Carneiro, 3-Jul-2017.) |
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) ⇒ ⊢ (𝜑 → 𝐴 ≠ 0) | ||
Theorem | dmgmaddnn0 24553 | If 𝐴 is not a nonpositive integer and 𝑁 is a nonnegative integer, then 𝐴 + 𝑁 is also not a nonpositive integer. (Contributed by Mario Carneiro, 6-Jul-2017.) |
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴 + 𝑁) ∈ (ℂ ∖ (ℤ ∖ ℕ))) | ||
Theorem | dmgmdivn0 24554 | Lemma for lgamf 24568. (Contributed by Mario Carneiro, 3-Jul-2017.) |
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) & ⊢ (𝜑 → 𝑀 ∈ ℕ) ⇒ ⊢ (𝜑 → ((𝐴 / 𝑀) + 1) ≠ 0) | ||
Theorem | lgamgulmlem1 24555* | Lemma for lgamgulm 24561. (Contributed by Mario Carneiro, 3-Jul-2017.) |
⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))} ⇒ ⊢ (𝜑 → 𝑈 ⊆ (ℂ ∖ (ℤ ∖ ℕ))) | ||
Theorem | lgamgulmlem2 24556* | Lemma for lgamgulm 24561. (Contributed by Mario Carneiro, 3-Jul-2017.) |
⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))} & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → (2 · 𝑅) ≤ 𝑁) ⇒ ⊢ (𝜑 → (abs‘((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1)))) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))) | ||
Theorem | lgamgulmlem3 24557* | Lemma for lgamgulm 24561. (Contributed by Mario Carneiro, 3-Jul-2017.) |
⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))} & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → (2 · 𝑅) ≤ 𝑁) ⇒ ⊢ (𝜑 → (abs‘((𝐴 · (log‘((𝑁 + 1) / 𝑁))) − (log‘((𝐴 / 𝑁) + 1)))) ≤ (𝑅 · ((2 · (𝑅 + 1)) / (𝑁↑2)))) | ||
Theorem | lgamgulmlem4 24558* | Lemma for lgamgulm 24561. (Contributed by Mario Carneiro, 3-Jul-2017.) |
⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))} & ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))) & ⊢ 𝑇 = (𝑚 ∈ ℕ ↦ if((2 · 𝑅) ≤ 𝑚, (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))), ((𝑅 · (log‘((𝑚 + 1) / 𝑚))) + ((log‘((𝑅 + 1) · 𝑚)) + π)))) ⇒ ⊢ (𝜑 → seq1( + , 𝑇) ∈ dom ⇝ ) | ||
Theorem | lgamgulmlem5 24559* | Lemma for lgamgulm 24561. (Contributed by Mario Carneiro, 3-Jul-2017.) |
⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))} & ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))) & ⊢ 𝑇 = (𝑚 ∈ ℕ ↦ if((2 · 𝑅) ≤ 𝑚, (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))), ((𝑅 · (log‘((𝑚 + 1) / 𝑚))) + ((log‘((𝑅 + 1) · 𝑚)) + π)))) ⇒ ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝐺‘𝑛)‘𝑦)) ≤ (𝑇‘𝑛)) | ||
Theorem | lgamgulmlem6 24560* | The series 𝐺 is uniformly convergent on the compact region 𝑈, which describes a circle of radius 𝑅 with holes of size 1 / 𝑅 around the poles of the gamma function. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))} & ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))) & ⊢ 𝑇 = (𝑚 ∈ ℕ ↦ if((2 · 𝑅) ≤ 𝑚, (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))), ((𝑅 · (log‘((𝑚 + 1) / 𝑚))) + ((log‘((𝑅 + 1) · 𝑚)) + π)))) ⇒ ⊢ (𝜑 → (seq1( ∘𝑓 + , 𝐺) ∈ dom (⇝𝑢‘𝑈) ∧ (seq1( ∘𝑓 + , 𝐺)(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ 𝑂) → ∃𝑟 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘𝑂) ≤ 𝑟))) | ||
Theorem | lgamgulm 24561* | The series 𝐺 is uniformly convergent on the compact region 𝑈, which describes a circle of radius 𝑅 with holes of size 1 / 𝑅 around the poles of the gamma function. (Contributed by Mario Carneiro, 3-Jul-2017.) |
⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))} & ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))) ⇒ ⊢ (𝜑 → seq1( ∘𝑓 + , 𝐺) ∈ dom (⇝𝑢‘𝑈)) | ||
Theorem | lgamgulm2 24562* | Rewrite the limit of the sequence 𝐺 in terms of the log-Gamma function. (Contributed by Mario Carneiro, 6-Jul-2017.) |
⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))} & ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))) ⇒ ⊢ (𝜑 → (∀𝑧 ∈ 𝑈 (log Γ‘𝑧) ∈ ℂ ∧ seq1( ∘𝑓 + , 𝐺)(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧))))) | ||
Theorem | lgambdd 24563* | The log-Gamma function is bounded on the region 𝑈. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))} & ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))) ⇒ ⊢ (𝜑 → ∃𝑟 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘(log Γ‘𝑧)) ≤ 𝑟) | ||
Theorem | lgamucov 24564* | The 𝑈 regions used in the proof of lgamgulm 24561 have interiors which cover the entire domain of the Gamma function. (Contributed by Mario Carneiro, 6-Jul-2017.) |
⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))} & ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) & ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝜑 → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈)) | ||
Theorem | lgamucov2 24565* | The 𝑈 regions used in the proof of lgamgulm 24561 have interiors which cover the entire domain of the Gamma function. (Contributed by Mario Carneiro, 8-Jul-2017.) |
⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))} & ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) ⇒ ⊢ (𝜑 → ∃𝑟 ∈ ℕ 𝐴 ∈ 𝑈) | ||
Theorem | lgamcvglem 24566* | Lemma for lgamf 24568 and lgamcvg 24580. (Contributed by Mario Carneiro, 8-Jul-2017.) |
⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))} & ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) & ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1)))) ⇒ ⊢ (𝜑 → ((log Γ‘𝐴) ∈ ℂ ∧ seq1( + , 𝐺) ⇝ ((log Γ‘𝐴) + (log‘𝐴)))) | ||
Theorem | lgamcl 24567 | The log-Gamma function is a complex function defined on the whole complex plane except for the negative integers. (Contributed by Mario Carneiro, 8-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (log Γ‘𝐴) ∈ ℂ) | ||
Theorem | lgamf 24568 | The log-Gamma function is a complex function defined on the whole complex plane except for the negative integers. (Contributed by Mario Carneiro, 6-Jul-2017.) |
⊢ log Γ:(ℂ ∖ (ℤ ∖ ℕ))⟶ℂ | ||
Theorem | gamf 24569 | The Gamma function is a complex function defined on the whole complex plane except for the negative integers. (Contributed by Mario Carneiro, 6-Jul-2017.) |
⊢ Γ:(ℂ ∖ (ℤ ∖ ℕ))⟶ℂ | ||
Theorem | gamcl 24570 | The exponential of the log-Gamma function is the Gamma function (by definition). (Contributed by Mario Carneiro, 8-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (Γ‘𝐴) ∈ ℂ) | ||
Theorem | eflgam 24571 | The exponential of the log-Gamma function is the Gamma function (by definition). (Contributed by Mario Carneiro, 8-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (exp‘(log Γ‘𝐴)) = (Γ‘𝐴)) | ||
Theorem | gamne0 24572 | The Gamma function is never zero. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (Γ‘𝐴) ≠ 0) | ||
Theorem | igamval 24573 | Value of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.) |
⊢ (𝐴 ∈ ℂ → (1/Γ‘𝐴) = if(𝐴 ∈ (ℤ ∖ ℕ), 0, (1 / (Γ‘𝐴)))) | ||
Theorem | igamz 24574 | Value of the inverse Gamma function on nonpositive integers. (Contributed by Mario Carneiro, 16-Jul-2017.) |
⊢ (𝐴 ∈ (ℤ ∖ ℕ) → (1/Γ‘𝐴) = 0) | ||
Theorem | igamgam 24575 | Value of the inverse Gamma function in terms of the Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (1/Γ‘𝐴) = (1 / (Γ‘𝐴))) | ||
Theorem | igamlgam 24576 | Value of the inverse Gamma function in terms of the log-Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (1/Γ‘𝐴) = (exp‘-(log Γ‘𝐴))) | ||
Theorem | igamf 24577 | Closure of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.) |
⊢ 1/Γ:ℂ⟶ℂ | ||
Theorem | igamcl 24578 | Closure of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.) |
⊢ (𝐴 ∈ ℂ → (1/Γ‘𝐴) ∈ ℂ) | ||
Theorem | gamigam 24579 | The Gamma function is the inverse of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (Γ‘𝐴) = (1 / (1/Γ‘𝐴))) | ||
Theorem | lgamcvg 24580* | The series 𝐺 converges to log Γ(𝐴) + log(𝐴). (Contributed by Mario Carneiro, 6-Jul-2017.) |
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1)))) & ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) ⇒ ⊢ (𝜑 → seq1( + , 𝐺) ⇝ ((log Γ‘𝐴) + (log‘𝐴))) | ||
Theorem | lgamcvg2 24581* | The series 𝐺 converges to log Γ(𝐴 + 1). (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1)))) & ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) ⇒ ⊢ (𝜑 → seq1( + , 𝐺) ⇝ (log Γ‘(𝐴 + 1))) | ||
Theorem | gamcvg 24582* | The pointwise exponential of the series 𝐺 converges to Γ(𝐴) · 𝐴. (Contributed by Mario Carneiro, 6-Jul-2017.) |
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1)))) & ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) ⇒ ⊢ (𝜑 → (exp ∘ seq1( + , 𝐺)) ⇝ ((Γ‘𝐴) · 𝐴)) | ||
Theorem | lgamp1 24583 | The functional equation of the (log) Gamma function. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (log Γ‘(𝐴 + 1)) = ((log Γ‘𝐴) + (log‘𝐴))) | ||
Theorem | gamp1 24584 | The functional equation of the Gamma function. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (Γ‘(𝐴 + 1)) = ((Γ‘𝐴) · 𝐴)) | ||
Theorem | gamcvg2lem 24585* | Lemma for gamcvg2 24586. (Contributed by Mario Carneiro, 10-Jul-2017.) |
⊢ 𝐹 = (𝑚 ∈ ℕ ↦ ((((𝑚 + 1) / 𝑚)↑𝑐𝐴) / ((𝐴 / 𝑚) + 1))) & ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) & ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1)))) ⇒ ⊢ (𝜑 → (exp ∘ seq1( + , 𝐺)) = seq1( · , 𝐹)) | ||
Theorem | gamcvg2 24586* | An infinite product expression for the gamma function. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ 𝐹 = (𝑚 ∈ ℕ ↦ ((((𝑚 + 1) / 𝑚)↑𝑐𝐴) / ((𝐴 / 𝑚) + 1))) & ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) ⇒ ⊢ (𝜑 → seq1( · , 𝐹) ⇝ ((Γ‘𝐴) · 𝐴)) | ||
Theorem | regamcl 24587 | The Gamma function is real for real input. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝐴 ∈ (ℝ ∖ (ℤ ∖ ℕ)) → (Γ‘𝐴) ∈ ℝ) | ||
Theorem | relgamcl 24588 | The log-Gamma function is real for positive real input. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝐴 ∈ ℝ+ → (log Γ‘𝐴) ∈ ℝ) | ||
Theorem | rpgamcl 24589 | The log-Gamma function is positive real for positive real input. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝐴 ∈ ℝ+ → (Γ‘𝐴) ∈ ℝ+) | ||
Theorem | lgam1 24590 | The log-Gamma function at one. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (log Γ‘1) = 0 | ||
Theorem | gam1 24591 | The log-Gamma function at one. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (Γ‘1) = 1 | ||
Theorem | facgam 24592 | The Gamma function generalizes the factorial. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) = (Γ‘(𝑁 + 1))) | ||
Theorem | gamfac 24593 | The Gamma function generalizes the factorial. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ (𝑁 ∈ ℕ → (Γ‘𝑁) = (!‘(𝑁 − 1))) | ||
Theorem | wilthlem1 24594 | The only elements that are equal to their own inverses in the multiplicative group of nonzero elements in ℤ / 𝑃ℤ are 1 and -1≡𝑃 − 1. (Note that from prmdiveq 15329, (𝑁↑(𝑃 − 2)) mod 𝑃 is the modular inverse of 𝑁 in ℤ / 𝑃ℤ. (Contributed by Mario Carneiro, 24-Jan-2015.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 = ((𝑁↑(𝑃 − 2)) mod 𝑃) ↔ (𝑁 = 1 ∨ 𝑁 = (𝑃 − 1)))) | ||
Theorem | wilthlem2 24595* |
Lemma for wilth 24597: induction step. The "hand proof"
version of this
theorem works by writing out the list of all numbers from 1 to
𝑃
− 1 in pairs such that a number is paired with its inverse.
Every number has a unique inverse different from itself except 1
and 𝑃 − 1, and so each pair
multiplies to 1, and 1 and
𝑃
− 1≡-1 multiply to -1, so the full
product is equal
to -1. Here we make this precise by doing the
product pair by
pair.
The induction hypothesis says that every subset 𝑆 of 1...(𝑃 − 1) that is closed under inverse (i.e. all pairs are matched up) and contains 𝑃 − 1 multiplies to -1 mod 𝑃. Given such a set, we take out one element 𝑧 ≠ 𝑃 − 1. If there are no such elements, then 𝑆 = {𝑃 − 1} which forms the base case. Otherwise, 𝑆 ∖ {𝑧, 𝑧↑-1} is also closed under inverse and contains 𝑃 − 1, so the induction hypothesis says that this equals -1; and the remaining two elements are either equal to each other, in which case wilthlem1 24594 gives that 𝑧 = 1 or 𝑃 − 1, and we've already excluded the second case, so the product gives 1; or 𝑧 ≠ 𝑧↑-1 and their product is 1. In either case the accumulated product is unaffected. (Contributed by Mario Carneiro, 24-Jan-2015.) (Proof shortened by AV, 27-Jul-2019.) |
⊢ 𝑇 = (mulGrp‘ℂfld) & ⊢ 𝐴 = {𝑥 ∈ 𝒫 (1...(𝑃 − 1)) ∣ ((𝑃 − 1) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥)} & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑆 ∈ 𝐴) & ⊢ (𝜑 → ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑆 → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃))) ⇒ ⊢ (𝜑 → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = (-1 mod 𝑃)) | ||
Theorem | wilthlem3 24596* | Lemma for wilth 24597. Here we round out the argument of wilthlem2 24595 with the final step of the induction. The induction argument shows that every subset of 1...(𝑃 − 1) that is closed under inverse and contains 𝑃 − 1 multiplies to -1 mod 𝑃, and clearly 1...(𝑃 − 1) itself is such a set. Thus, the product of all the elements is -1, and all that is left is to translate the group sum notation (which we used for its unordered summing capabilities) into an ordered sequence to match the definition of the factorial. (Contributed by Mario Carneiro, 24-Jan-2015.) (Proof shortened by AV, 27-Jul-2019.) |
⊢ 𝑇 = (mulGrp‘ℂfld) & ⊢ 𝐴 = {𝑥 ∈ 𝒫 (1...(𝑃 − 1)) ∣ ((𝑃 − 1) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥)} ⇒ ⊢ (𝑃 ∈ ℙ → 𝑃 ∥ ((!‘(𝑃 − 1)) + 1)) | ||
Theorem | wilth 24597 | Wilson's theorem. A number is prime iff it is greater or equal to 2 and (𝑁 − 1)! is congruent to -1, mod 𝑁, or alternatively if 𝑁 divides (𝑁 − 1)! + 1. In this part of the proof we show the relatively simple reverse implication; see wilthlem3 24596 for the forward implication. This is Metamath 100 proof #51. (Contributed by Mario Carneiro, 24-Jan-2015.) (Proof shortened by Fan Zheng, 16-Jun-2016.) |
⊢ (𝑁 ∈ ℙ ↔ (𝑁 ∈ (ℤ≥‘2) ∧ 𝑁 ∥ ((!‘(𝑁 − 1)) + 1))) | ||
Theorem | wilthimp 24598 | The forward implication of Wilson's theorem wilth 24597 (see wilthlem3 24596), expressed using the modulo operation: For any prime 𝑝 we have (𝑝 − 1)!≡ − 1 (mod 𝑝), see theorem 5.24 in [ApostolNT] p. 116. (Contributed by AV, 21-Jul-2021.) |
⊢ (𝑃 ∈ ℙ → ((!‘(𝑃 − 1)) mod 𝑃) = (-1 mod 𝑃)) | ||
Theorem | ftalem1 24599* | Lemma for fta 24606: "growth lemma". There exists some 𝑟 such that 𝐹 is arbitrarily close in proportion to its dominant term. (Contributed by Mario Carneiro, 14-Sep-2014.) |
⊢ 𝐴 = (coeff‘𝐹) & ⊢ 𝑁 = (deg‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ 𝑇 = (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) / 𝐸) ⇒ ⊢ (𝜑 → ∃𝑟 ∈ ℝ ∀𝑥 ∈ ℂ (𝑟 < (abs‘𝑥) → (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < (𝐸 · ((abs‘𝑥)↑𝑁)))) | ||
Theorem | ftalem2 24600* | Lemma for fta 24606. There exists some 𝑟 such that 𝐹 has magnitude greater than 𝐹(0) outside the closed ball B(0,r). (Contributed by Mario Carneiro, 14-Sep-2014.) |
⊢ 𝐴 = (coeff‘𝐹) & ⊢ 𝑁 = (deg‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑈 = if(if(1 ≤ 𝑠, 𝑠, 1) ≤ 𝑇, 𝑇, if(1 ≤ 𝑠, 𝑠, 1)) & ⊢ 𝑇 = ((abs‘(𝐹‘0)) / ((abs‘(𝐴‘𝑁)) / 2)) ⇒ ⊢ (𝜑 → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ ℂ (𝑟 < (abs‘𝑥) → (abs‘(𝐹‘0)) < (abs‘(𝐹‘𝑥)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |