logo

Demonstrations for the theory of proveit.trigonometry

In [1]:
import proveit
from proveit import a, b, c, r, theta
from proveit.logic import InSet
from proveit.numbers import zero, one, two, e, pi, i
from proveit.numbers import Real, RealPos, RealNeg, RealNonNeg, RealNonPos
from proveit.numbers import IntervalCC, IntervalOC, IntervalCO, IntervalOO
from proveit.numbers import frac, Less, LessEq, Abs, Neg, Add, subtract, Mult, Div, Exp
from proveit.trigonometry import Sin, Cos
%begin demonstrations
In [2]:
Abs(subtract(Exp(e, Mult(i, zero)), Exp(e, Mult(i, Mult(two, pi, theta))))).shallow_simplification(
    assumptions=[InSet(r, RealPos), InSet(theta, Real)])
In [3]:
Abs(subtract(one, Exp(e, Mult(two, pi, i, theta)))).chord_length_simplification(
    assumptions=[InSet(r, RealPos), InSet(theta, Real)])
In [4]:
Abs(subtract(one, Exp(e, Mult(two, pi, i, theta)))).chord_length_simplification(
    assumptions=[InSet(r, RealPos), InSet(theta, Real)], auto_simplify=False)

Deducing bounds (including triangle inequality)

In [5]:
Sin(theta).deduce_in_interval(assumptions=[InSet(theta, Real)])
In [6]:
Sin(theta).deduce_in_interval(assumptions=[InSet(theta, IntervalCC(zero, pi))])
In [7]:
Sin(theta).deduce_in_interval(assumptions=[InSet(theta, IntervalOO(zero, pi))])
In [8]:
Sin(theta).deduce_in_interval(assumptions=[InSet(theta, IntervalCC(Neg(pi), zero))])
In [9]:
Sin(theta).deduce_in_interval(assumptions=[InSet(theta, IntervalOO(Neg(pi), zero))])
In [10]:
Sin(Abs(theta)).deduce_linear_bound(assumptions=[InSet(theta, Real), LessEq(Abs(theta), Div(pi, two))])
In [11]:
Sin(theta).deduce_linear_bound(assumptions=[InSet(theta, RealPos), LessEq(theta, Div(pi, two))])
In [12]:
Sin(theta).deduce_linear_bound(assumptions=[InSet(theta, RealNonNeg), LessEq(theta, Div(pi, two))])
In [13]:
Sin(theta).deduce_linear_bound(assumptions=[InSet(theta, RealNeg), Less(Neg(theta), Div(pi, two))])

Deducing lower bounds: distinguishing between $\sin{\theta} > \theta$ vs. $\sin{\theta} > \frac{2}{\pi}\theta$ depending on domain

In [14]:
Sin(theta).deduce_linear_lower_bound(assumptions=[InSet(theta, RealNeg), Less(Neg(theta), Div(pi, two))])
In [15]:
from proveit.numbers import frac
Sin(Abs(theta)).deduce_linear_lower_bound(assumptions=[InSet(theta, Real), InSet(Abs(theta), IntervalCC(zero, frac(pi, two)))],
        preserve_expr=Sin(Abs(theta)))
In [16]:
Sin(theta).deduce_linear_lower_bound(assumptions=[InSet(theta, RealPos), Less(theta, frac(pi, two))])
In [17]:
Sin(theta).deduce_linear_lower_bound(assumptions=[InSet(theta, RealNonNeg), LessEq(theta, frac(pi, two))])
In [18]:
Sin(theta).deduce_linear_lower_bound(assumptions=[InSet(theta, RealNeg)])
In [19]:
Sin(theta).deduce_linear_lower_bound(assumptions=[InSet(theta, RealNonPos)])

Deducing upper bounds: distinguishing between $\sin{\theta} < \theta$ vs. $\sin{\theta} < \frac{2}{\pi}\theta$ depending on domain

In [20]:
Sin(theta).deduce_linear_upper_bound(assumptions=[InSet(theta, RealNeg), Less(Neg(theta), Div(pi, two))])
In [21]:
Sin(Abs(theta)).deduce_linear_upper_bound(assumptions=[InSet(theta, RealNeg)],
        preserve_expr=Sin(Abs(theta)))
In [22]:
Sin(theta).deduce_linear_upper_bound(assumptions=[InSet(theta, RealPos)])
In [23]:
Sin(theta).deduce_linear_upper_bound(assumptions=[InSet(theta, RealNonNeg)])
In [24]:
Sin(theta).deduce_linear_upper_bound(assumptions=[InSet(theta, IntervalOO(Neg(frac(pi, two)), zero))])
In [25]:
Sin(theta).deduce_linear_upper_bound(assumptions=[InSet(theta, IntervalCC(Neg(frac(pi, two)), zero))])

Magnitudes and lengths

Using the circle choord length formula

In [26]:
Abs(subtract(Mult(r, Exp(e, Mult(i, a))), 
             Mult(r, Exp(e, Mult(i, b))))).simplification(
    assumptions=[InSet(r, RealPos), InSet(a, Real), InSet(b, Real)])
, ,  ⊢  
In [27]:
Abs(subtract(Mult(r, Exp(e, Mult(i, a)), c), 
             Mult(r, c, Exp(e, Mult(i, b))))).simplification(
    assumptions=[InSet(r, RealPos), InSet(c, RealPos), InSet(a, Real), InSet(b, Real)])
, , ,  ⊢  
In [28]:
Abs(subtract(Exp(e, Mult(i, theta)), one)).chord_length_simplification(assumptions=[InSet(theta, Real)])
In [29]:
Abs(subtract(r, Mult(r, Exp(e, Mult(i, theta))))).chord_length_simplification(
    assumptions=[InSet(r, RealPos), InSet(theta, Real)])
In [30]:
Abs(subtract(one, Exp(e, Mult(two, pi, i, theta)))).chord_length_simplification(
    assumptions=[InSet(r, RealPos), InSet(theta, Real)])
In [31]:
Abs(Add(Neg(Exp(e, Mult(two, pi, i, theta))), one)).chord_length_simplification(
    assumptions=[InSet(r, RealPos), InSet(theta, Real)])
In [32]:
%end demonstrations