Home | Metamath
Proof Explorer Theorem List (p. 255 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | reasinsin 25401 | The arcsine function composed with sin is equal to the identity. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ (-(π / 2)[,](π / 2)) → (arcsin‘(sin‘𝐴)) = 𝐴) | ||
Theorem | asinsinb 25402 | Relationship between sine and arcsine. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (ℜ‘𝐵) ∈ (-(π / 2)(,)(π / 2))) → ((arcsin‘𝐴) = 𝐵 ↔ (sin‘𝐵) = 𝐴)) | ||
Theorem | acoscosb 25403 | Relationship between sine and arcsine. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (ℜ‘𝐵) ∈ (0(,)π)) → ((arccos‘𝐴) = 𝐵 ↔ (cos‘𝐵) = 𝐴)) | ||
Theorem | asinbnd 25404 | The arcsine function has range within a vertical strip of the complex plane with real part between -π / 2 and π / 2. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (ℜ‘(arcsin‘𝐴)) ∈ (-(π / 2)[,](π / 2))) | ||
Theorem | acosbnd 25405 | The arccosine function has range within a vertical strip of the complex plane with real part between 0 and π. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (ℜ‘(arccos‘𝐴)) ∈ (0[,]π)) | ||
Theorem | asinrebnd 25406 | Bounds on the arcsine function. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ (-1[,]1) → (arcsin‘𝐴) ∈ (-(π / 2)[,](π / 2))) | ||
Theorem | asinrecl 25407 | The arcsine function is real in its principal domain. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ (-1[,]1) → (arcsin‘𝐴) ∈ ℝ) | ||
Theorem | acosrecl 25408 | The arccosine function is real in its principal domain. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ (-1[,]1) → (arccos‘𝐴) ∈ ℝ) | ||
Theorem | cosasin 25409 | The cosine of the arcsine of 𝐴 is √(1 − 𝐴↑2). (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (cos‘(arcsin‘𝐴)) = (√‘(1 − (𝐴↑2)))) | ||
Theorem | sinacos 25410 | The sine of the arccosine of 𝐴 is √(1 − 𝐴↑2). (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (sin‘(arccos‘𝐴)) = (√‘(1 − (𝐴↑2)))) | ||
Theorem | atandmneg 25411 | The domain of the arctangent function is closed under negatives. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → -𝐴 ∈ dom arctan) | ||
Theorem | atanneg 25412 | The arctangent function is odd. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → (arctan‘-𝐴) = -(arctan‘𝐴)) | ||
Theorem | atan0 25413 | The arctangent of zero is zero. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (arctan‘0) = 0 | ||
Theorem | atandmcj 25414 | The arctangent function distributes under conjugation. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ dom arctan → (∗‘𝐴) ∈ dom arctan) | ||
Theorem | atancj 25415 | The arctangent function distributes under conjugation. (The condition that ℜ(𝐴) ≠ 0 is necessary because the branch cuts are chosen so that the negative imaginary line "agrees with" neighboring values with negative real part, while the positive imaginary line agrees with values with positive real part. This makes atanneg 25412 true unconditionally but messes up conjugation symmetry, and it is impossible to have both in a single-valued function. The claim is true on the imaginary line between -1 and 1, though.) (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (𝐴 ∈ dom arctan ∧ (∗‘(arctan‘𝐴)) = (arctan‘(∗‘𝐴)))) | ||
Theorem | atanrecl 25416 | The arctangent function is real for all real inputs. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℝ → (arctan‘𝐴) ∈ ℝ) | ||
Theorem | efiatan 25417 | Value of the exponential of an artcangent. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → (exp‘(i · (arctan‘𝐴))) = ((√‘(1 + (i · 𝐴))) / (√‘(1 − (i · 𝐴))))) | ||
Theorem | atanlogaddlem 25418 | Lemma for atanlogadd 25419. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ ((𝐴 ∈ dom arctan ∧ 0 ≤ (ℜ‘𝐴)) → ((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴)))) ∈ ran log) | ||
Theorem | atanlogadd 25419 | The rule √(𝑧𝑤) = (√𝑧)(√𝑤) is not always true on the complex numbers, but it is true when the arguments of 𝑧 and 𝑤 sum to within the interval (-π, π], so there are some cases such as this one with 𝑧 = 1 + i𝐴 and 𝑤 = 1 − i𝐴 which are true unconditionally. This result can also be stated as "√(1 + 𝑧) + √(1 − 𝑧) is analytic". (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → ((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴)))) ∈ ran log) | ||
Theorem | atanlogsublem 25420 | Lemma for atanlogsub 25421. (Contributed by Mario Carneiro, 4-Apr-2015.) |
⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i · 𝐴))))) ∈ (-π(,)π)) | ||
Theorem | atanlogsub 25421 | A variation on atanlogadd 25419, to show that √(1 + i𝑧) / √(1 − i𝑧) = √((1 + i𝑧) / (1 − i𝑧)) under more limited conditions. (Contributed by Mario Carneiro, 4-Apr-2015.) |
⊢ ((𝐴 ∈ dom arctan ∧ (ℜ‘𝐴) ≠ 0) → ((log‘(1 + (i · 𝐴))) − (log‘(1 − (i · 𝐴)))) ∈ ran log) | ||
Theorem | efiatan2 25422 | Value of the exponential of an artcangent. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → (exp‘(i · (arctan‘𝐴))) = ((1 + (i · 𝐴)) / (√‘(1 + (𝐴↑2))))) | ||
Theorem | 2efiatan 25423 | Value of the exponential of an artcangent. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → (exp‘(2 · (i · (arctan‘𝐴)))) = (((2 · i) / (𝐴 + i)) − 1)) | ||
Theorem | tanatan 25424 | The arctangent function is an inverse to tan. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → (tan‘(arctan‘𝐴)) = 𝐴) | ||
Theorem | atandmtan 25425 | The tangent function has range contained in the domain of the arctangent. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) ∈ dom arctan) | ||
Theorem | cosatan 25426 | The cosine of an arctangent. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → (cos‘(arctan‘𝐴)) = (1 / (√‘(1 + (𝐴↑2))))) | ||
Theorem | cosatanne0 25427 | The arctangent function has range contained in the domain of the tangent. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → (cos‘(arctan‘𝐴)) ≠ 0) | ||
Theorem | atantan 25428 | The arctangent function is an inverse to tan. (Contributed by Mario Carneiro, 5-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (arctan‘(tan‘𝐴)) = 𝐴) | ||
Theorem | atantanb 25429 | Relationship between tangent and arctangent. (Contributed by Mario Carneiro, 5-Apr-2015.) |
⊢ ((𝐴 ∈ dom arctan ∧ 𝐵 ∈ ℂ ∧ (ℜ‘𝐵) ∈ (-(π / 2)(,)(π / 2))) → ((arctan‘𝐴) = 𝐵 ↔ (tan‘𝐵) = 𝐴)) | ||
Theorem | atanbndlem 25430 | Lemma for atanbnd 25431. (Contributed by Mario Carneiro, 5-Apr-2015.) |
⊢ (𝐴 ∈ ℝ+ → (arctan‘𝐴) ∈ (-(π / 2)(,)(π / 2))) | ||
Theorem | atanbnd 25431 | The arctangent function is bounded by π / 2 on the reals. (Contributed by Mario Carneiro, 5-Apr-2015.) |
⊢ (𝐴 ∈ ℝ → (arctan‘𝐴) ∈ (-(π / 2)(,)(π / 2))) | ||
Theorem | atanord 25432 | The arctangent function is strictly increasing. (Contributed by Mario Carneiro, 5-Apr-2015.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (arctan‘𝐴) < (arctan‘𝐵))) | ||
Theorem | atan1 25433 | The arctangent of 1 is π / 4. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (arctan‘1) = (π / 4) | ||
Theorem | bndatandm 25434 | A point in the open unit disk is in the domain of the arctangent. (Contributed by Mario Carneiro, 5-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 𝐴 ∈ dom arctan) | ||
Theorem | atans 25435* | The "domain of continuity" of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷} ⇒ ⊢ (𝐴 ∈ 𝑆 ↔ (𝐴 ∈ ℂ ∧ (1 + (𝐴↑2)) ∈ 𝐷)) | ||
Theorem | atans2 25436* | It suffices to show that 1 − i𝐴 and 1 + i𝐴 are in the continuity domain of log to show that 𝐴 is in the continuity domain of arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷} ⇒ ⊢ (𝐴 ∈ 𝑆 ↔ (𝐴 ∈ ℂ ∧ (1 − (i · 𝐴)) ∈ 𝐷 ∧ (1 + (i · 𝐴)) ∈ 𝐷)) | ||
Theorem | atansopn 25437* | The domain of continuity of the arctangent is an open set. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷} ⇒ ⊢ 𝑆 ∈ (TopOpen‘ℂfld) | ||
Theorem | atansssdm 25438* | The domain of continuity of the arctangent is a subset of the actual domain of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷} ⇒ ⊢ 𝑆 ⊆ dom arctan | ||
Theorem | ressatans 25439* | The real number line is a subset of the domain of continuity of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷} ⇒ ⊢ ℝ ⊆ 𝑆 | ||
Theorem | dvatan 25440* | The derivative of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷} ⇒ ⊢ (ℂ D (arctan ↾ 𝑆)) = (𝑥 ∈ 𝑆 ↦ (1 / (1 + (𝑥↑2)))) | ||
Theorem | atancn 25441* | The arctangent is a continuous function. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷} ⇒ ⊢ (arctan ↾ 𝑆) ∈ (𝑆–cn→ℂ) | ||
Theorem | atantayl 25442* | The Taylor series for arctan(𝐴). (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((i · ((-i↑𝑛) − (i↑𝑛))) / 2) · ((𝐴↑𝑛) / 𝑛))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , 𝐹) ⇝ (arctan‘𝐴)) | ||
Theorem | atantayl2 25443* | The Taylor series for arctan(𝐴). (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, ((-1↑((𝑛 − 1) / 2)) · ((𝐴↑𝑛) / 𝑛)))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , 𝐹) ⇝ (arctan‘𝐴)) | ||
Theorem | atantayl3 25444* | The Taylor series for arctan(𝐴). (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) · ((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1)))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , 𝐹) ⇝ (arctan‘𝐴)) | ||
Theorem | leibpilem1 25445 | Lemma for leibpi 25448. (Contributed by Mario Carneiro, 7-Apr-2015.) (Proof shortened by Steven Nguyen, 23-Mar-2023.) |
⊢ ((𝑁 ∈ ℕ0 ∧ (¬ 𝑁 = 0 ∧ ¬ 2 ∥ 𝑁)) → (𝑁 ∈ ℕ ∧ ((𝑁 − 1) / 2) ∈ ℕ0)) | ||
Theorem | leibpilem1OLD 25446 | Obsolete version of leibpilem1 25445 as of 23-Mar-2023. Lemma for leibpi 25448. (Contributed by Mario Carneiro, 7-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝑁 ∈ ℕ0 ∧ (¬ 𝑁 = 0 ∧ ¬ 2 ∥ 𝑁)) → (𝑁 ∈ ℕ ∧ ((𝑁 − 1) / 2) ∈ ℕ0)) | ||
Theorem | leibpilem2 25447* | The Leibniz formula for π. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1))) & ⊢ 𝐺 = (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘))) & ⊢ 𝐴 ∈ V ⇒ ⊢ (seq0( + , 𝐹) ⇝ 𝐴 ↔ seq0( + , 𝐺) ⇝ 𝐴) | ||
Theorem | leibpi 25448 | The Leibniz formula for π. This proof depends on three main facts: (1) the series 𝐹 is convergent, because it is an alternating series (iseralt 15031). (2) Using leibpilem2 25447 to rewrite the series as a power series, it is the 𝑥 = 1 special case of the Taylor series for arctan (atantayl2 25443). (3) Although we cannot directly plug 𝑥 = 1 into atantayl2 25443, Abel's theorem (abelth2 24959) says that the limit along any sequence converging to 1, such as 1 − 1 / 𝑛, of the power series converges to the power series extended to 1, and then since arctan is continuous at 1 (atancn 25441) we get the desired result. This is Metamath 100 proof #26. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1))) ⇒ ⊢ seq0( + , 𝐹) ⇝ (π / 4) | ||
Theorem | leibpisum 25449 | The Leibniz formula for π. This version of leibpi 25448 looks nicer but does not assert that the series is convergent so is not as practically useful. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ Σ𝑛 ∈ ℕ0 ((-1↑𝑛) / ((2 · 𝑛) + 1)) = (π / 4) | ||
Theorem | log2cnv 25450 | Using the Taylor series for arctan(i / 3), produce a rapidly convergent series for log2. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ⇒ ⊢ seq0( + , 𝐹) ⇝ (log‘2) | ||
Theorem | log2tlbnd 25451* | Bound the error term in the series of log2cnv 25450. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ (𝑁 ∈ ℕ0 → ((log‘2) − Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ∈ (0[,](3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))) | ||
Theorem | log2ublem1 25452 | Lemma for log2ub 25455. The proof of log2ub 25455, which is simply the evaluation of log2tlbnd 25451 for 𝑁 = 4, takes the form of the addition of five fractions and showing this is less than another fraction. We could just perform exact arithmetic on these fractions, get a large rational number, and just multiply everything to verify the claim, but as anyone who uses decimal numbers for this task knows, it is often better to pick a common denominator 𝑑 (usually a large power of 10) and work with the closest approximations of the form 𝑛 / 𝑑 for some integer 𝑛 instead. It turns out that for our purposes it is sufficient to take 𝑑 = (3↑7) · 5 · 7, which is also nice because it shares many factors in common with the fractions in question. (Contributed by Mario Carneiro, 17-Apr-2015.) |
⊢ (((3↑7) · (5 · 7)) · 𝐴) ≤ 𝐵 & ⊢ 𝐴 ∈ ℝ & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐹 ∈ ℕ0 & ⊢ 𝐶 = (𝐴 + (𝐷 / 𝐸)) & ⊢ (𝐵 + 𝐹) = 𝐺 & ⊢ (((3↑7) · (5 · 7)) · 𝐷) ≤ (𝐸 · 𝐹) ⇒ ⊢ (((3↑7) · (5 · 7)) · 𝐶) ≤ 𝐺 | ||
Theorem | log2ublem2 25453* | Lemma for log2ub 25455. (Contributed by Mario Carneiro, 17-Apr-2015.) |
⊢ (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...𝐾)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 𝐵) & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐹 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 & ⊢ (𝑁 − 1) = 𝐾 & ⊢ (𝐵 + 𝐹) = 𝐺 & ⊢ 𝑀 ∈ ℕ0 & ⊢ (𝑀 + 𝑁) = 3 & ⊢ ((5 · 7) · (9↑𝑀)) = (((2 · 𝑁) + 1) · 𝐹) ⇒ ⊢ (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 𝐺) | ||
Theorem | log2ublem3 25454 | Lemma for log2ub 25455. In decimal, this is a proof that the first four terms of the series for log2 is less than 53056 / 76545. (Contributed by Mario Carneiro, 17-Apr-2015.) (Proof shortened by AV, 15-Sep-2021.) |
⊢ (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ ;;;;53056 | ||
Theorem | log2ub 25455 | log2 is less than 253 / 365. If written in decimal, this is because log2 = 0.693147... is less than 253/365 = 0.693151... , so this is a very tight bound, at five decimal places. (Contributed by Mario Carneiro, 7-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.) |
⊢ (log‘2) < (;;253 / ;;365) | ||
Theorem | log2le1 25456 | log2 is less than 1. This is just a weaker form of log2ub 25455 when no tight upper bound is required. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
⊢ (log‘2) < 1 | ||
Theorem | birthdaylem1 25457* | Lemma for birthday 25460. (Contributed by Mario Carneiro, 17-Apr-2015.) |
⊢ 𝑆 = {𝑓 ∣ 𝑓:(1...𝐾)⟶(1...𝑁)} & ⊢ 𝑇 = {𝑓 ∣ 𝑓:(1...𝐾)–1-1→(1...𝑁)} ⇒ ⊢ (𝑇 ⊆ 𝑆 ∧ 𝑆 ∈ Fin ∧ (𝑁 ∈ ℕ → 𝑆 ≠ ∅)) | ||
Theorem | birthdaylem2 25458* | For general 𝑁 and 𝐾, count the fraction of injective functions from 1...𝐾 to 1...𝑁. (Contributed by Mario Carneiro, 7-May-2015.) |
⊢ 𝑆 = {𝑓 ∣ 𝑓:(1...𝐾)⟶(1...𝑁)} & ⊢ 𝑇 = {𝑓 ∣ 𝑓:(1...𝐾)–1-1→(1...𝑁)} ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((♯‘𝑇) / (♯‘𝑆)) = (exp‘Σ𝑘 ∈ (0...(𝐾 − 1))(log‘(1 − (𝑘 / 𝑁))))) | ||
Theorem | birthdaylem3 25459* | For general 𝑁 and 𝐾, upper-bound the fraction of injective functions from 1...𝐾 to 1...𝑁. (Contributed by Mario Carneiro, 17-Apr-2015.) |
⊢ 𝑆 = {𝑓 ∣ 𝑓:(1...𝐾)⟶(1...𝑁)} & ⊢ 𝑇 = {𝑓 ∣ 𝑓:(1...𝐾)–1-1→(1...𝑁)} ⇒ ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) → ((♯‘𝑇) / (♯‘𝑆)) ≤ (exp‘-((((𝐾↑2) − 𝐾) / 2) / 𝑁))) | ||
Theorem | birthday 25460* | The Birthday Problem. There is a more than even chance that out of 23 people in a room, at least two of them have the same birthday. Mathematically, this is asserting that for 𝐾 = 23 and 𝑁 = 365, fewer than half of the set of all functions from 1...𝐾 to 1...𝑁 are injective. This is Metamath 100 proof #93. (Contributed by Mario Carneiro, 17-Apr-2015.) |
⊢ 𝑆 = {𝑓 ∣ 𝑓:(1...𝐾)⟶(1...𝑁)} & ⊢ 𝑇 = {𝑓 ∣ 𝑓:(1...𝐾)–1-1→(1...𝑁)} & ⊢ 𝐾 = ;23 & ⊢ 𝑁 = ;;365 ⇒ ⊢ ((♯‘𝑇) / (♯‘𝑆)) < (1 / 2) | ||
Syntax | carea 25461 | Area of regions in the complex plane. |
class area | ||
Definition | df-area 25462* | Define the area of a subset of ℝ × ℝ. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ area = (𝑠 ∈ {𝑡 ∈ 𝒫 (ℝ × ℝ) ∣ (∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) ∈ 𝐿1)} ↦ ∫ℝ(vol‘(𝑠 “ {𝑥})) d𝑥) | ||
Theorem | dmarea 25463* | The domain of the area function is the set of finitely measurable subsets of ℝ × ℝ. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ (𝐴 ∈ dom area ↔ (𝐴 ⊆ (ℝ × ℝ) ∧ ∀𝑥 ∈ ℝ (𝐴 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝐴 “ {𝑥}))) ∈ 𝐿1)) | ||
Theorem | areambl 25464 | The fibers of a measurable region are finitely measurable subsets of ℝ. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ ((𝑆 ∈ dom area ∧ 𝐴 ∈ ℝ) → ((𝑆 “ {𝐴}) ∈ dom vol ∧ (vol‘(𝑆 “ {𝐴})) ∈ ℝ)) | ||
Theorem | areass 25465 | A measurable region is a subset of ℝ × ℝ. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ (𝑆 ∈ dom area → 𝑆 ⊆ (ℝ × ℝ)) | ||
Theorem | dfarea 25466* | Rewrite df-area 25462 self-referentially. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ area = (𝑠 ∈ dom area ↦ ∫ℝ(vol‘(𝑠 “ {𝑥})) d𝑥) | ||
Theorem | areaf 25467 | Area measurement is a function whose values are nonnegative reals. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ area:dom area⟶(0[,)+∞) | ||
Theorem | areacl 25468 | The area of a measurable region is a real number. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ (𝑆 ∈ dom area → (area‘𝑆) ∈ ℝ) | ||
Theorem | areage0 25469 | The area of a measurable region is greater than or equal to zero. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ (𝑆 ∈ dom area → 0 ≤ (area‘𝑆)) | ||
Theorem | areaval 25470* | The area of a measurable region is greater than or equal to zero. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ (𝑆 ∈ dom area → (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥) | ||
Theorem | rlimcnp 25471* | Relate a limit of a real-valued sequence at infinity to the continuity of the function 𝑆(𝑦) = 𝑅(1 / 𝑦) at zero. (Contributed by Mario Carneiro, 1-Mar-2015.) |
⊢ (𝜑 → 𝐴 ⊆ (0[,)+∞)) & ⊢ (𝜑 → 0 ∈ 𝐴) & ⊢ (𝜑 → 𝐵 ⊆ ℝ+) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ 𝐴 ↔ (1 / 𝑥) ∈ 𝐵)) & ⊢ (𝑥 = 0 → 𝑅 = 𝐶) & ⊢ (𝑥 = (1 / 𝑦) → 𝑅 = 𝑆) & ⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (𝐽 ↾t 𝐴) ⇒ ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘0))) | ||
Theorem | rlimcnp2 25472* | Relate a limit of a real-valued sequence at infinity to the continuity of the function 𝑆(𝑦) = 𝑅(1 / 𝑦) at zero. (Contributed by Mario Carneiro, 1-Mar-2015.) |
⊢ (𝜑 → 𝐴 ⊆ (0[,)+∞)) & ⊢ (𝜑 → 0 ∈ 𝐴) & ⊢ (𝜑 → 𝐵 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑆 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑦 ∈ 𝐵 ↔ (1 / 𝑦) ∈ 𝐴)) & ⊢ (𝑦 = (1 / 𝑥) → 𝑆 = 𝑅) & ⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (𝐽 ↾t 𝐴) ⇒ ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) ∈ ((𝐾 CnP 𝐽)‘0))) | ||
Theorem | rlimcnp3 25473* | Relate a limit of a real-valued sequence at infinity to the continuity of the function 𝑆(𝑦) = 𝑅(1 / 𝑦) at zero. (Contributed by Mario Carneiro, 1-Mar-2015.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝑆 ∈ ℂ) & ⊢ (𝑦 = (1 / 𝑥) → 𝑆 = 𝑅) & ⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (𝐽 ↾t (0[,)+∞)) ⇒ ⊢ (𝜑 → ((𝑦 ∈ ℝ+ ↦ 𝑆) ⇝𝑟 𝐶 ↔ (𝑥 ∈ (0[,)+∞) ↦ if(𝑥 = 0, 𝐶, 𝑅)) ∈ ((𝐾 CnP 𝐽)‘0))) | ||
Theorem | xrlimcnp 25474* | Relate a limit of a real-valued sequence at infinity to the continuity of the corresponding extended real function at +∞. Since any ⇝𝑟 limit can be written in the form on the left side of the implication, this shows that real limits are a special case of topological continuity at a point. (Contributed by Mario Carneiro, 8-Sep-2015.) |
⊢ (𝜑 → 𝐴 = (𝐵 ∪ {+∞})) & ⊢ (𝜑 → 𝐵 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ ℂ) & ⊢ (𝑥 = +∞ → 𝑅 = 𝐶) & ⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = ((ordTop‘ ≤ ) ↾t 𝐴) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞))) | ||
Theorem | efrlim 25475* | The limit of the sequence (1 + 𝐴 / 𝑘)↑𝑘 is the exponential function. This is often taken as an alternate definition of the exponential function (see also dfef2 25476). (Contributed by Mario Carneiro, 1-Mar-2015.) |
⊢ 𝑆 = (0(ball‘(abs ∘ − ))(1 / ((abs‘𝐴) + 1))) ⇒ ⊢ (𝐴 ∈ ℂ → (𝑘 ∈ ℝ+ ↦ ((1 + (𝐴 / 𝑘))↑𝑐𝑘)) ⇝𝑟 (exp‘𝐴)) | ||
Theorem | dfef2 25476* | The limit of the sequence (1 + 𝐴 / 𝑘)↑𝑘 as 𝑘 goes to +∞ is (exp‘𝐴). This is another common definition of e. (Contributed by Mario Carneiro, 1-Mar-2015.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = ((1 + (𝐴 / 𝑘))↑𝑘)) ⇒ ⊢ (𝜑 → 𝐹 ⇝ (exp‘𝐴)) | ||
Theorem | cxplim 25477* | A power to a negative exponent goes to zero as the base becomes large. (Contributed by Mario Carneiro, 15-Sep-2014.) (Revised by Mario Carneiro, 18-May-2016.) |
⊢ (𝐴 ∈ ℝ+ → (𝑛 ∈ ℝ+ ↦ (1 / (𝑛↑𝑐𝐴))) ⇝𝑟 0) | ||
Theorem | sqrtlim 25478 | The inverse square root function converges to zero. (Contributed by Mario Carneiro, 18-May-2016.) |
⊢ (𝑛 ∈ ℝ+ ↦ (1 / (√‘𝑛))) ⇝𝑟 0 | ||
Theorem | rlimcxp 25479* | Any power to a positive exponent of a converging sequence also converges. (Contributed by Mario Carneiro, 18-Sep-2014.) |
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑛 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 0) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝑛 ∈ 𝐴 ↦ (𝐵↑𝑐𝐶)) ⇝𝑟 0) | ||
Theorem | o1cxp 25480* | An eventually bounded function taken to a nonnegative power is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 0 ≤ (ℜ‘𝐶)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵↑𝑐𝐶)) ∈ 𝑂(1)) | ||
Theorem | cxp2limlem 25481* | A linear factor grows slower than any exponential with base greater than 1. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 1 < 𝐴) → (𝑛 ∈ ℝ+ ↦ (𝑛 / (𝐴↑𝑐𝑛))) ⇝𝑟 0) | ||
Theorem | cxp2lim 25482* | Any power grows slower than any exponential with base greater than 1. (Contributed by Mario Carneiro, 18-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → (𝑛 ∈ ℝ+ ↦ ((𝑛↑𝑐𝐴) / (𝐵↑𝑐𝑛))) ⇝𝑟 0) | ||
Theorem | cxploglim 25483* | The logarithm grows slower than any positive power. (Contributed by Mario Carneiro, 18-Sep-2014.) |
⊢ (𝐴 ∈ ℝ+ → (𝑛 ∈ ℝ+ ↦ ((log‘𝑛) / (𝑛↑𝑐𝐴))) ⇝𝑟 0) | ||
Theorem | cxploglim2 25484* | Every power of the logarithm grows slower than any positive power. (Contributed by Mario Carneiro, 20-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+) → (𝑛 ∈ ℝ+ ↦ (((log‘𝑛)↑𝑐𝐴) / (𝑛↑𝑐𝐵))) ⇝𝑟 0) | ||
Theorem | divsqrtsumlem 25485* | Lemma for divsqrsum 25487 and divsqrtsum2 25488. (Contributed by Mario Carneiro, 18-May-2016.) |
⊢ 𝐹 = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑛)) − (2 · (√‘𝑥)))) ⇒ ⊢ (𝐹:ℝ+⟶ℝ ∧ 𝐹 ∈ dom ⇝𝑟 ∧ ((𝐹 ⇝𝑟 𝐿 ∧ 𝐴 ∈ ℝ+) → (abs‘((𝐹‘𝐴) − 𝐿)) ≤ (1 / (√‘𝐴)))) | ||
Theorem | divsqrsumf 25486* | The function 𝐹 used in divsqrsum 25487 is a real function. (Contributed by Mario Carneiro, 12-May-2016.) |
⊢ 𝐹 = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑛)) − (2 · (√‘𝑥)))) ⇒ ⊢ 𝐹:ℝ+⟶ℝ | ||
Theorem | divsqrsum 25487* | 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 25488* | 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 25489* | The sum Σ𝑛 ≤ 𝑥(1 / √𝑛) has the asymptotic expansion 2√𝑥 + 𝐿 + 𝑂(1 / √𝑥), for some 𝐿. (Contributed by Mario Carneiro, 10-May-2016.) |
⊢ 𝐹 = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑛)) − (2 · (√‘𝑥)))) & ⊢ (𝜑 → 𝐹 ⇝𝑟 𝐿) ⇒ ⊢ (𝜑 → (𝑦 ∈ ℝ+ ↦ (((𝐹‘𝑦) − 𝐿) · (√‘𝑦))) ∈ 𝑂(1)) | ||
Theorem | cvxcl 25490* | Closure of a 0-1 linear combination in a convex set. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → (𝑥[,]𝑦) ⊆ 𝐷) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) ∈ 𝐷) | ||
Theorem | scvxcvx 25491* | A strictly convex function is convex. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝐷⟶ℝ) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ≤ ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))) | ||
Theorem | jensenlem1 25492* | Lemma for jensen 25494. (Contributed by Mario Carneiro, 4-Jun-2016.) |
⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝐷⟶ℝ) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝑇:𝐴⟶(0[,)+∞)) & ⊢ (𝜑 → 𝑋:𝐴⟶𝐷) & ⊢ (𝜑 → 0 < (ℂfld Σg 𝑇)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑡 ∈ (0[,]1))) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))) & ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐵) & ⊢ (𝜑 → (𝐵 ∪ {𝑧}) ⊆ 𝐴) & ⊢ 𝑆 = (ℂfld Σg (𝑇 ↾ 𝐵)) & ⊢ 𝐿 = (ℂfld Σg (𝑇 ↾ (𝐵 ∪ {𝑧}))) ⇒ ⊢ (𝜑 → 𝐿 = (𝑆 + (𝑇‘𝑧))) | ||
Theorem | jensenlem2 25493* | Lemma for jensen 25494. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝐷⟶ℝ) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝑇:𝐴⟶(0[,)+∞)) & ⊢ (𝜑 → 𝑋:𝐴⟶𝐷) & ⊢ (𝜑 → 0 < (ℂfld Σg 𝑇)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑡 ∈ (0[,]1))) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))) & ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐵) & ⊢ (𝜑 → (𝐵 ∪ {𝑧}) ⊆ 𝐴) & ⊢ 𝑆 = (ℂfld Σg (𝑇 ↾ 𝐵)) & ⊢ 𝐿 = (ℂfld Σg (𝑇 ↾ (𝐵 ∪ {𝑧}))) & ⊢ (𝜑 → 𝑆 ∈ ℝ+) & ⊢ (𝜑 → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆) ∈ 𝐷) & ⊢ (𝜑 → (𝐹‘((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) ⇒ ⊢ (𝜑 → (((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝐵 ∪ {𝑧}))) / 𝐿) ∈ 𝐷 ∧ (𝐹‘((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝐵 ∪ {𝑧}))) / 𝐿)) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝐵 ∪ {𝑧}))) / 𝐿))) | ||
Theorem | jensen 25494* | 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 (𝑇 ∘f · 𝑋)) / (ℂfld Σg 𝑇)) ∈ 𝐷 ∧ (𝐹‘((ℂfld Σg (𝑇 ∘f · 𝑋)) / (ℂfld Σg 𝑇))) ≤ ((ℂfld Σg (𝑇 ∘f · (𝐹 ∘ 𝑋))) / (ℂfld Σg 𝑇)))) | ||
Theorem | amgmlem 25495 | Lemma for amgm 25496. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ 𝑀 = (mulGrp‘ℂfld) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ+) ⇒ ⊢ (𝜑 → ((𝑀 Σg 𝐹)↑𝑐(1 / (♯‘𝐴))) ≤ ((ℂfld Σg 𝐹) / (♯‘𝐴))) | ||
Theorem | amgm 25496 | 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 25497 | The Euler-Mascheroni constant. (The label abbreviates Euler-Mascheroni.) |
class γ | ||
Definition | df-em 25498 | 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 25508. (Contributed by Mario Carneiro, 11-Jul-2014.) |
⊢ γ = Σ𝑘 ∈ ℕ ((1 / 𝑘) − (log‘(1 + (1 / 𝑘)))) | ||
Theorem | logdifbnd 25499 | Bound on the difference of logs. (Contributed by Mario Carneiro, 23-May-2016.) |
⊢ (𝐴 ∈ ℝ+ → ((log‘(𝐴 + 1)) − (log‘𝐴)) ≤ (1 / 𝐴)) | ||
Theorem | logdiflbnd 25500 | Lower bound on the difference of logs. (Contributed by Mario Carneiro, 3-Jul-2017.) |
⊢ (𝐴 ∈ ℝ+ → (1 / (𝐴 + 1)) ≤ ((log‘(𝐴 + 1)) − (log‘𝐴))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |