# Theorems (or conjectures) for the theory of proveit.numbers.absolute_value¶

In [1]:
import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
from proveit import IndexedVar, ExprRange
from proveit import a, b, c, k, n, r, x, y, theta
from proveit.logic import And, Equals, Forall, Iff, InSet, NotEquals
from proveit.numbers import (Abs, Add, subtract, frac, Mult, Neg, Exp, Sum,
Less, LessEq, greater, greater_eq, number_ordering)
from proveit.numbers import (zero, one, e, i,
ZeroSet, Natural, NaturalPos, Integer, IntegerNonZero, IntegerNonPos,
Rational, RationalNonZero, RationalNonNeg, RationalPos, RationalNonPos,
Real, RealNeg, RealNonNeg, RealPos, RealNonPos,
Complex, ComplexNonZero)
from proveit.core_expr_types import x_1_to_n

In [2]:
%begin theorems

Defining theorems for theory 'proveit.numbers.absolute_value'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions


Basic closure theorems

In [3]:
abs_zero_closure = Forall(a, InSet(Abs(a), ZeroSet), domain=ZeroSet)

abs_zero_closure (conjecture without proof):

In [4]:
abs_integer_closure = Forall(
a,
InSet(Abs(a), Natural),
domain=Integer)

abs_integer_closure (conjecture without proof):

In [5]:
abs_integer_nonzero_closure = Forall(
a,
InSet(Abs(a), NaturalPos),
domain=IntegerNonZero)

abs_integer_nonzero_closure (conjecture without proof):

In [6]:
abs_rational_closure = Forall(
a,
InSet(Abs(a), RationalNonNeg),
domain=Rational)

abs_rational_closure (conjecture without proof):

In [7]:
abs_rational_nonzero_closure = Forall(
a,
InSet(Abs(a), RationalPos),
domain=RationalNonZero)

abs_rational_nonzero_closure (conjecture without proof):

In [8]:
abs_complex_closure = Forall(
a,
InSet(Abs(a), RealNonNeg),
domain=Complex)

abs_complex_closure (conjecture without proof):

In [9]:
abs_nonzero_closure = Forall(
a,
InSet(Abs(a), RealPos),
domain=ComplexNonZero)

abs_nonzero_closure (conjecture without proof):

Non-Negativity, Non-Zero, & Positive Definiteness Theorems

In [10]:
abs_is_non_neg = Forall(
a,
greater_eq(Abs(a), zero),
domain=Complex)

abs_is_non_neg (conjecture without proof):

In [11]:
abs_not_eq_zero = Forall(
a,
NotEquals(Abs(a), zero),
domain=Complex,
conditions=[NotEquals(a, zero)])

abs_not_eq_zero (conjecture without proof):

In [12]:
abs_pos_def = Forall(
a,
Iff(Equals(Abs(a), zero), Equals(a, zero)),
domain=Complex)

abs_pos_def (conjecture without proof):

#### Equality¶

In [13]:
abs_eq = Forall((x, y), Equals(Abs(x), Abs(y)), condition=Equals(x, y), domain=Complex)

abs_eq (conjecture without proof):

#### Evenness¶

In [14]:
abs_even = Forall(
x,
Equals(Abs(Neg(x)), Abs(x)),
domain = Complex)

abs_even (conjecture without proof):

In [15]:
abs_even_rev = Forall(
x,
Equals(Abs(x), Abs(Neg(x))),
domain = Complex)

abs_even_rev (conjecture without proof):

In [16]:
abs_non_neg_elim = Forall(
x,
Equals(Abs(x), x),
condition = greater_eq(x, zero))

abs_non_neg_elim (conjecture without proof):

In [17]:
abs_neg_elim = Forall(
x,
Equals(Abs(x), Neg(x)),
condition = LessEq(x, zero))

abs_neg_elim (conjecture without proof):

In [18]:
abs_diff_reversal = Forall(
(a, b), Equals(Abs(subtract(a, b)), Abs(subtract(b, a))),
domain = Complex)

abs_diff_reversal (conjecture without proof):

In [19]:
double_abs_elem = Forall(
x,
Equals(Abs(Abs(x)), Abs(x)),
domain = Complex)

double_abs_elem (conjecture without proof):

In [20]:
abs_ineq = Forall(
(x, y),
Iff(LessEq(Abs(x), y),
And(LessEq(Neg(y), x), LessEq(x, y))),
domain = Real,
conditions = [greater_eq(y, zero)])

abs_ineq (conjecture without proof):

### Bounding the absolute value¶

In [21]:
strict_upper_bound = Forall((a, c), Less(Abs(a), c),
conditions=number_ordering(Less(Neg(c), a), Less(a, c)))

strict_upper_bound (conjecture without proof):

In [22]:
weak_upper_bound = Forall((a, c), LessEq(Abs(a), c),
conditions=number_ordering(LessEq(Neg(c), a), LessEq(a, c)))

weak_upper_bound (conjecture without proof):

In [23]:
from proveit.numbers import Max
strict_upper_bound_asym_interval = (
Forall((a, b, c),
Less(Abs(a), Max(Abs(b), Abs(c))),
domain = Real,
conditions=[number_ordering(Less(b, a), Less(a, c))]))

strict_upper_bound_asym_interval (conjecture without proof):

In [24]:
from proveit.numbers import Max
weak_upper_bound_asym_interval = (
Forall((a, b, c),
LessEq(Abs(a), Max(Abs(b), Abs(c))),
domain = Real,
conditions = [number_ordering(LessEq(b, a), LessEq(a, c))]))

weak_upper_bound_asym_interval (conjecture without proof):

Absolute values of complex numbers in polar form

In [25]:
complex_unit_length = Forall(
theta, Equals(Abs(Exp(e, Mult(i, theta))), one),
domain=Real)

complex_unit_length (conjecture without proof):

In [26]:
complex_polar_mag_using_abs = Forall(
(r, theta), Equals(Abs(Mult(r, Exp(e, Mult(i, theta)))), Abs(r)),
domain=Real)

complex_polar_mag_using_abs (conjecture without proof):

Triangle Inequality

In [27]:
triangle_inequality = Forall(
(a, b),
domain=Complex)

triangle_inequality (conjecture without proof):

Prove the generalized triangle inequality using induction on the triangle inequality

In [28]:
generalized_triangle_inequality = Forall(
domain=Complex),
domain=NaturalPos)

generalized_triangle_inequality (conjecture without proof):

Multiplicativity (and Preservation of Division)

In [29]:
abs_prod = Forall(
n,
Forall(x_1_to_n,
Equals(Abs(Mult(x_1_to_n)),
Mult(ExprRange(k, Abs(IndexedVar(x, k)), one, n))),
domain = Complex),
domain = NaturalPos)

abs_prod (conjecture without proof):

In [30]:
abs_frac = Forall(
(a, b),
Equals(Abs(frac(a, b)), frac(Abs(a), Abs(b))),
domain = Complex,
conditions=[NotEquals(b, zero)])

abs_frac (conjecture without proof):

See the proveit.trigonometry theory package for facts related to absolute values of complex numbers in polar form.

In [31]:
%end theorems

These theorems may now be imported from the theory package: proveit.numbers.absolute_value