Alphabeta MathHow statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Multiplying inequalities of positives
Statement
Let be an ordered field. If and then . If and then .
Facts & Assumptions
Given: Elements of an ordered field .
For a positive multiplier : ; multiplying a strict inequality by a positive element preserves it (Sign rules for products and monotonicity of multiplication).
For : ; the case is [L1] and the case gives (Sign rules for products and monotonicity of multiplication).
The order is transitive: if and then , and likewise for , since the positive cone is closed under addition (Ordered field).
Proof
Assume and ; since , scaling by gives .
Since (from ), scaling by gives .
Assume instead and ; since , from we get .
Since (from ), from we get .
By transitivity, , hence , proving the strict claim.
By transitivity of , , hence , proving the nonstrict claim.
Both the strict and the nonstrict inequalities hold.
Depends on
Used by
- If f is continuous on an interval I and |f'| ≤ M at every interior point, then |f(x) - f(y)| ≤ M|x-y| for all x,y ∈ I, so f is Lipschitz with constant M and uniformly continuous on I Corollary
- x ↦ √x on (0,1] is differentiable with unbounded derivative and is not Lipschitz there, so the boundedness hypothesis in the Lipschitz corollary cannot be dropped Counterexample
- The block sequence 1/1; 1/2, 2/2; 1/3, 2/3, 3/3; … has subsequential limit set exactly [0,1] Example
- The mean value theorem gives |√x - √y| ≤ 1/ι(2) |x - y| for x, y ≥ 1, so the square root is Lipschitz with constant 1/2 on [1,∞) Example
- A null sequence times a bounded sequence is null Lemma
- Factorisation of bⁿ - aⁿ, and the resulting Lipschitz estimate Lemma
- For |r| < 1 the sequence rᵏ is null, and for |r| > 1 the sequence |r|ᵏ diverges to +∞ Lemma
- For every p > 0 and every positive rational α, n^α/(1+p)ⁿ → 0 Lemma
- For every real x, xᵏ/k! → 0 Lemma
- Monotonicity of x ↦ xⁿ and of n ↦ aⁿ Lemma
- Every contractive sequence is Cauchy, hence converges, with error bound |x - xₖ| ≤ cᵏ⁻¹|x₂ - x₁|/(1-c) for k ≥ 1 Theorem
- For aₖ > 0: liminf aₖ₊₁/aₖ ≤ liminf aₖ^1/k ≤ limsup aₖ^1/k ≤ limsup aₖ₊₁/aₖ Theorem
- For bounded nonnegative sequences, limsup(xₖ yₖ) ≤ (limsup xₖ)(limsup yₖ) Theorem
- Square roots exist: a unique √a ≥ 0 with (√a)² = a; the positives are {x² : x ≠ 0} Theorem
- The arithmetic mean, geometric mean inequality Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 5 results over 4 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 (standard reference, not scraped)
- M. Spivak, Calculus, 4th ed., Ch. 1 (standard reference, not scraped)
- Purdue University analysis notes: Ordered fields and absolute value (standard reference, not scraped)