Theorems (or conjectures) for the theory of proveit.trigonometry

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 a, b, r, t, theta
from proveit.logic import Forall, Equals, InSet, Difference
from proveit.numbers import Real, RealPos, RealNeg, RealNonNeg, RealNonPos
from proveit.numbers import IntervalCC, IntervalOO, IntervalOC, IntervalCO
from proveit.numbers import zero, one, two, e, i, pi
from proveit.numbers import Add, subtract, Neg, Abs, Mult, Div, Exp
from proveit.numbers import Less, LessEq, greater, greater_eq
from proveit.trigonometry import Sin, Cos

%begin theorems

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

Closure

real_closure = Forall(theta, InSet(Sin(theta), Real),
                      domain=Real)

real_closure (conjecture without proof):

Trigonometric bounds

sine_interval = Forall(theta, InSet(Sin(theta), IntervalCC(Neg(one), one)),
                      domain=Real)

sine_interval (conjecture without proof):

sine_nonneg_interval = Forall(theta, InSet(Sin(theta), IntervalCC(zero, one)),
                              domain=IntervalCC(zero, pi))

sine_nonneg_interval (conjecture without proof):

sine_pos_interval = Forall(theta, InSet(Sin(theta), IntervalOC(zero, one)),
                                domain=IntervalOO(zero, pi))

sine_pos_interval (conjecture without proof):

sine_nonpos_interval = Forall(theta, InSet(Sin(theta), IntervalCC(Neg(one), zero)),
                              domain=IntervalCC(Neg(pi), zero))

sine_nonpos_interval (conjecture without proof):

sine_neg_interval = Forall(theta, InSet(Sin(theta), IntervalCO(Neg(one), zero)),
                           domain=IntervalOO(Neg(pi), zero))

sine_neg_interval (conjecture without proof):

Additionally, we could exclude 1 and -1 if we exclude $\theta = \pm \pi / 2$ (e.g., use the set difference).

These linear bounds on the sine function are easy to see visually in comparing the sine function to a line.

![linearBoundsOnSine.png]

Bounding regions of $y = \sin\theta$ by the chord $y = \frac{2\theta}{\pi}$

sine_linear_bound = Forall(theta, greater_eq(Sin(Abs(theta)), Div(Mult(two, Abs(theta)), pi)),
                           domain=Real, condition=LessEq(Abs(theta), Div(pi, two)))

sine_linear_bound (conjecture without proof):

sine_linear_bound_nonneg = Forall(
    theta, greater_eq(Sin(theta), Div(Mult(two, theta), pi)),
    domain=RealNonNeg, condition=LessEq(theta, Div(pi, two)))

sine_linear_bound_nonneg (conjecture without proof):

sine_linear_bound_nonpos = Forall(
    theta, LessEq(Sin(theta), Div(Mult(two, theta), pi)),
    domain=RealNonPos, condition=LessEq(Neg(theta), Div(pi, two)))

sine_linear_bound_nonpos (conjecture without proof):

Bounding $y = \sin\theta$ by $y = \theta$

sine_linear_bound_by_arg =(
    Forall(theta,
           LessEq(Sin(Abs(theta)), Abs(theta)),
           domain=Real))

sine_linear_bound_by_arg (conjecture without proof):

sine_linear_bound_by_arg_pos =(
    Forall(theta,
           Less(Sin(theta), theta),
           domain=RealPos))

sine_linear_bound_by_arg_pos (conjecture without proof):

sine_linear_bound_by_arg_nonneg =(
    Forall(theta,
           LessEq(Sin(theta), theta),
           domain=RealNonNeg))

sine_linear_bound_by_arg_nonneg (conjecture without proof):

sine_linear_bound_by_arg_neg =(
    Forall(theta,
           Less(theta, Sin(theta)),
           domain=RealNeg))

sine_linear_bound_by_arg_neg (conjecture without proof):

sine_linear_bound_by_arg_nonpos =(
    Forall(theta,
           LessEq(theta, Sin(theta)),
           domain=RealNonPos))

sine_linear_bound_by_arg_nonpos (conjecture without proof):

Trigonometry theorems related to complex numbers in polar form

complex_unit_circle_chord_length = Forall(
    (a, b), Equals(Abs(subtract(Exp(e, Mult(i, a)), Exp(e, Mult(i, b)))), 
                   Mult(two, Sin(Div(Abs(subtract(a, b)), two)))),
    domain=Real)

complex_unit_circle_chord_length (conjecture without proof):

complex_circle_chord_length = Forall(
    r, Forall((a, b), Equals(Abs(subtract(Mult(r, Exp(e, Mult(i, a))), 
                                          Mult(r, Exp(e, Mult(i, b))))), 
                             Mult(two, r, Sin(Div(Abs(subtract(a, b)), two)))),
              domain=Real),
    domain=RealNonNeg)

complex_circle_chord_length (conjecture without proof):

abs_sin = Forall(
        t,
        Equals(Abs(Sin(t)), Sin(Abs(t))),
        domain=Real)

abs_sin (conjecture without proof):

abs_cos = Forall(
        t,
        Equals(Abs(Cos(t)), Cos(Abs(t))),
        domain=Real)

abs_cos (conjecture without proof):

%end theorems

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