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