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

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

%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

abs_zero_closure = Forall(a, InSet(Abs(a), ZeroSet), domain=ZeroSet)

abs_zero_closure (conjecture without proof):

abs_integer_closure = Forall(
    a,
    InSet(Abs(a), Natural),
    domain=Integer)

abs_integer_closure (conjecture without proof):

abs_integer_nonzero_closure = Forall(
    a,
    InSet(Abs(a), NaturalPos),
    domain=IntegerNonZero)

abs_integer_nonzero_closure (conjecture without proof):

abs_rational_closure = Forall(
    a,
    InSet(Abs(a), RationalNonNeg),
    domain=Rational)

abs_rational_closure (conjecture without proof):

abs_rational_nonzero_closure = Forall(
    a,
    InSet(Abs(a), RationalPos),
    domain=RationalNonZero)

abs_rational_nonzero_closure (conjecture without proof):

abs_complex_closure = Forall(
    a,
    InSet(Abs(a), RealNonNeg),
    domain=Complex)

abs_complex_closure (conjecture without proof):

abs_nonzero_closure = Forall(
    a,
    InSet(Abs(a), RealPos),
    domain=ComplexNonZero)

abs_nonzero_closure (conjecture without proof):

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

abs_is_non_neg = Forall(
    a,
    greater_eq(Abs(a), zero),
    domain=Complex)

abs_is_non_neg (conjecture without proof):

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

abs_not_eq_zero (conjecture without proof):

abs_pos_def = Forall(
    a,
    Iff(Equals(Abs(a), zero), Equals(a, zero)),
    domain=Complex)

abs_pos_def (conjecture without proof):

Equality

abs_eq = Forall((x, y), Equals(Abs(x), Abs(y)), condition=Equals(x, y), domain=Complex)

abs_eq (conjecture without proof):

Evenness

abs_even = Forall(
    x,
    Equals(Abs(Neg(x)), Abs(x)),
    domain = Complex)

abs_even (conjecture without proof):

abs_even_rev = Forall(
    x,
    Equals(Abs(x), Abs(Neg(x))),
    domain = Complex)

abs_even_rev (conjecture without proof):

abs_non_neg_elim = Forall(
    x,
    Equals(Abs(x), x),
    condition = greater_eq(x, zero))

abs_non_neg_elim (conjecture without proof):

abs_neg_elim = Forall(
    x,
    Equals(Abs(x), Neg(x)),
    condition = LessEq(x, zero))

abs_neg_elim (conjecture without proof):

abs_diff_reversal = Forall(
    (a, b), Equals(Abs(subtract(a, b)), Abs(subtract(b, a))),
    domain = Complex)

abs_diff_reversal (conjecture without proof):

double_abs_elem = Forall(
    x,
    Equals(Abs(Abs(x)), Abs(x)),
    domain = Complex)

double_abs_elem (conjecture without proof):

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

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):

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):

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):

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

complex_unit_length = Forall(
    theta, Equals(Abs(Exp(e, Mult(i, theta))), one),
    domain=Real)

complex_unit_length (conjecture without proof):

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

triangle_inequality = Forall(
    (a, b),
    LessEq(Abs(Add(a,b)), Add(Abs(a), Abs(b))),
    domain=Complex)

triangle_inequality (conjecture without proof):

Prove the generalized triangle inequality using induction on the triangle inequality

generalized_triangle_inequality = Forall(
    n, Forall(x_1_to_n, LessEq(Abs(Add(x_1_to_n)), 
                               Add(ExprRange(k, Abs(IndexedVar(x, k)), one, n))),
              domain=Complex),
    domain=NaturalPos)

generalized_triangle_inequality (conjecture without proof):

Multiplicativity (and Preservation of Division)

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):

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.

%end theorems

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