The Theory analysis

Parents

fin_set

Children

group_egs

fincomb

metric_spaces

Constants

PolyFunc	( ) SET
PolyEval	LIST
PlusCoeffs	LIST LIST LIST
TimesCoeffs	LIST LIST LIST
$To	( 'a) 'a LIST
$->	( ) BOOL
ClosedInterval	SET
OpenInterval	SET
$Cts	( ) BOOL
$Deriv	( ) BOOL
DerivCoeffs	LIST LIST
Open_R	SET SET
Closed_R	SET SET
Compact_R	SET SET
$-->	( ) BOOL
$--->	( ) ( ) SET BOOL
Series	( )
PowerSeries	( )
$!
Exp
Log
Cos
Sin
ArchimedesConstant
$+#->	( ) BOOL
$-+#>	( ) BOOL
$-+#>+#	( ) BOOL
Sqrt
Tan
Cotan
Sec
Cosec
ArcSin
ArcCos
Sinh
Cosh
Tanh
Cotanh
Sech
Cosech
ArcSinh
TaggedPartition	(( ) ( ) ) SET
RiemannSum	( ) ( ) ( )
Gauge	( SET) SET
$Fine	( SET) (( ) ( ) ) SET
$Int_R	( ) BOOL
CharFun	'a SET 'a
$Int	( ) SET BOOL
$Area	( ) SET BOOL

Aliases

	ArchimedesConstant :
χ	CharFun : 'a SET 'a

Fixity

Right Infix 200:

Area

Cts

Deriv

Int

Int_R

Right Infix 205:

+#->

-+#>

--->

-->

Right Infix 310:

Postfix 200:

-+#>+#

Postfix 330:

Fine

Definitions

PolyFunc	PolyFunc = {A \|( c ( x c) A) ( x x) A ( f g f A g A ( x f x + g x) A) ( f g f A g A ( x f x * g x) A)}
PolyEval	( x PolyEval [] x = 0) ( c l x PolyEval (Cons c l) x = c + x * PolyEval l x)
PlusCoeffs	ConstSpec ( PlusCoeffs' ( l PlusCoeffs' [] l = l) ( l PlusCoeffs' l [] = l) ( c1 l1 c2 l2 PlusCoeffs' (Cons c1 l1) (Cons c2 l2) = Cons (c1 + c2) (PlusCoeffs' l1 l2))) PlusCoeffs
TimesCoeffs	( l TimesCoeffs [] l = []) ( c l1 l2 TimesCoeffs (Cons c l1) l2 = PlusCoeffs (Cons ( 0) (TimesCoeffs l1 l2)) (Map ( x c * x) l2))
To	( f f To 0 = []) ( f n f To (n + 1) = f To n ⁀ [f n])
->	s x s -> x ( e 0 < e ( n m n m Abs (s m - x) < e))
ClosedInterval	x y ClosedInterval x y = {t\|x t t y}
OpenInterval	x y OpenInterval x y = {t\|x < t t < y}
Cts	f x f Cts x ( e 0 < e ( d 0 < d ( y Abs (y - x) < d Abs (f y - f x) < e)))
Deriv	f c x (f Deriv c) x ( e 0 < e ( d 0 < d ( y Abs (y - x) < d y = x Abs ((f y - f x) / (y - x) - c) < e)))
DerivCoeffs	DerivCoeffs [] = [] ( c l DerivCoeffs (Cons c l) = PlusCoeffs l (Cons ( 0) (DerivCoeffs l)))
Open_R	Open_R = {A \| t t A ( x y t OpenInterval x y OpenInterval x y A)}
Closed_R	Closed_R = {A\|~ A Open_R}
Compact_R	Compact_R = {A \| V V Open_R A V ( W W V W Finite A W)}
-->	f c x (f --> c) x ( e 0 < e ( d 0 < d ( y Abs (y - x) < d y = x Abs (f y - c) < e)))
--->	u h X (u ---> h) X ( e 0 < e ( n m y n m y X Abs (u m y - h y) < e))
Series	( s Series s 0 = 0) ( s n Series s (n + 1) = Series s n + s n)
PowerSeries	s n PowerSeries s n = PolyEval (s To n)
!	0 ! = 1 ( m (m + 1) ! = (m + 1) * m !)
Exp	ConstSpec ( Exp' Exp' ( 0) = 1 ( x (Exp' Deriv Exp' x) x)) Exp
Log	ConstSpec ( Log' x Log' (Exp x) = x) Log
Sin Cos	ConstSpec ( (Sin', Cos') Sin' ( 0) = 0 Cos' ( 0) = 1 ( x (Sin' Deriv Cos' x) x) ( x (Cos' Deriv ~ (Sin' x)) x)) (Sin, Cos)
ArchimedesConstant	ConstSpec ( ArchimedesConstant' 0 < ArchimedesConstant' ( x Sin x = 0 ( m x = m * ArchimedesConstant') ( m x = ~ ( m * ArchimedesConstant'))))
+#->	f c a (f +#-> c) a ( e 0 < e ( b a < b ( x a < x x < b Abs (f x - c) < e)))
-+#>	f c f -+#> c ( e 0 < e ( b x b < x Abs (f x - c) < e))
-+#>+#	f f -+#>+# ( x b y b < y x < f y)
Sqrt	ConstSpec ( Sqrt' x 0 x 0 Sqrt' x Sqrt' x ^ 2 = x Sqrt' Cts x) Sqrt
Tan	x Tan x = Sin x * Cos x ^-¹
Cotan	x Cotan x = Cos x * Sin x ^-¹
Sec	x Sec x = Cos x ^-¹
Cosec	x Cosec x = Sin x ^-¹
ArcSin	ConstSpec ( ArcSin' ( x Abs x 1 / 2 * ArcSin' (Sin x) = x) ( x Abs x 1 Sin (ArcSin' x) = x ArcSin' Cts x)) ArcSin
ArcCos	ConstSpec ( ArcCos' ( x 0 x x ArcCos' (Cos x) = x) ( x Abs x 1 Cos (ArcCos' x) = x ArcCos' Cts x)) ArcCos
Sinh	x Sinh x = 1 / 2 * (Exp x - Exp (~ x))
Cosh	x Cosh x = 1 / 2 * (Exp x + Exp (~ x))
Tanh	x Tanh x = Sinh x * Cosh x ^-¹
Cotanh	x Cotanh x = Cosh x * Sinh x ^-¹
Sech	x Sech x = Cosh x ^-¹
Cosech	x Cosech x = Sinh x ^-¹
ArcSinh	ConstSpec ( ArcSinh' x ArcSinh' (Sinh x) = x Sinh (ArcSinh' x) = x ArcSinh' Cts x) ArcSinh
TaggedPartition	t I n (t, I, n) TaggedPartition ( m m < n I m < I (m + 1)) ( m m < n t m ClosedInterval (I m) (I (m + 1)))
RiemannSum	f t I n RiemannSum f (t, I, n) = Series ( m f (t m) * (I (m + 1) - I m)) n
Gauge	G G Gauge ( x G x Open_R x G x)
Fine	t I n G (t, I, n) G Fine ( m m < n ClosedInterval (I m) (I (m + 1)) G (t m))
Int_R	f c f Int_R c ( e 0 < e ( G a b G Gauge a < b ( t I n (t, I, n) TaggedPartition I 0 < a b < I n (t, I, n) G Fine Abs (RiemannSum f (t, I, n) - c) < e)))
CharFun	A x χ A x = (if x A then 1 else 0)
Int	f c A (f Int c) A ( x χ A x * f x) Int_R c
Area	A c A Area c ( sf sf Int_R c ( x χ {y\|(x, y) A} Int_R sf x))

Theorems

PlusCoeffs_consistent	Consistent ( PlusCoeffs' ( l PlusCoeffs' [] l = l) ( l PlusCoeffs' l [] = l) ( c1 l1 c2 l2 PlusCoeffs' (Cons c1 l1) (Cons c2 l2) = Cons (c1 + c2) (PlusCoeffs' l1 l2)))
plus_coeffs_def	( l PlusCoeffs [] l = l) ( l PlusCoeffs l [] = l) ( c1 l1 c2 l2 PlusCoeffs (Cons c1 l1) (Cons c2 l2) = Cons (c1 + c2) (PlusCoeffs l1 l2))
const_eval_thm	c ( x c) = PolyEval [c]
id_eval_thm	( x x) = PolyEval [ 0; 1]
plus_eval_thm	l1 l2 ( x PolyEval l1 x + PolyEval l2 x) = PolyEval (PlusCoeffs l1 l2)
const_times_eval_thm	c l ( x c * PolyEval l x) = PolyEval (Map ( y c * y) l)
times_eval_thm	l1 l2 ( x PolyEval l1 x * PolyEval l2 x) = PolyEval (TimesCoeffs l1 l2)
poly_induction_thm	p ( c p ( x c)) p ( x x) ( f g p f p g p ( x f x + g x)) ( f g p f p g p ( x f x * g x)) ( h h PolyFunc p h)
poly_func_eq_poly_eval_thm	PolyFunc = {f\| l f = PolyEval l}
const_poly_func_thm	c ( x c) PolyFunc
id_poly_func_thm	( x x) PolyFunc
plus_poly_func_thm	f g f PolyFunc g PolyFunc ( x f x + g x) PolyFunc
times_poly_func_thm	f g f PolyFunc g PolyFunc ( x f x * g x) PolyFunc
comp_poly_thm	f g f PolyFunc g PolyFunc ( x f (g x)) PolyFunc
poly_eval_append_thm	l1 l2 x PolyEval (l1 ⁀ l2) x = PolyEval l1 x + x ^ # l1 * PolyEval l2 x
poly_eval_rev_thm	( x PolyEval (Rev []) x = 0) ( c l x PolyEval (Rev (Cons c l)) x = c * x ^ # l + PolyEval (Rev l) x)
poly_diff_powers_thm	n x y (x - y) * PolyEval (Rev (( m y ^ m) To (n + 1))) x = x ^ (n + 1) - y ^ (n + 1)
length_plus_coeffs_thm	l1 l2 # (PlusCoeffs l1 l2) = (if # l2 < # l1 then # l1 else # l2)
poly_linear_div_thm	l1 c l1 = [] ( l2 r # l2 < # l1 ( x PolyEval l1 x) = ( x (x - c) * PolyEval l2 x + r))
poly_remainder_thm	l1 c l1 = [] ( l2 # l2 < # l1 ( x PolyEval l1 x) = ( x (x - c) * PolyEval l2 x + PolyEval l1 c))
poly_factor_thm	l1 c l1 = [] PolyEval l1 c = 0 ( l2 # l2 < # l1 ( x PolyEval l1 x) = ( x (x - c) * PolyEval l2 x))
poly_roots_finite_thm	f c f PolyFunc f c = 0 {x\|f x = 0} Finite
_0__abs_thm	x 0 Abs x
_abs_plus_thm	x y Abs (x + y) Abs x + Abs y
_abs_subtract_thm	x y Abs (x - y) Abs x + Abs y
_abs_plus_minus_thm	x y Abs (x + ~ y) Abs x + Abs y
_abs_diff_bounded_thm	x y z 0 < z (Abs (x + ~ y) < z y + ~ z < x x < y + z)
_abs_plus_bc_thm	x y z Abs x Abs (y + z) Abs x Abs y + Abs z
_abs_abs_minus_thm	x y Abs (Abs x - Abs y) Abs (x - y)
_abs_abs_thm	x Abs (Abs x) = Abs x
_abs_times_thm	x y Abs (x * y) = Abs x * Abs y
_abs___exp_thm	x m Abs (x ^ m) = Abs x ^ m
_abs_eq_0_thm	x Abs x = 0 x = 0
_abs__0_thm	x Abs x 0 x = 0
_abs_0_thm	Abs ( 0) = 0
_abs_recip_thm	x x = 0 Abs (x ^-¹) = Abs x ^-¹
_abs_squared_thm	x Abs x ^ 2 = x ^ 2
_abs_less_times_thm	x t y u Abs x < t Abs y < u Abs x * Abs y < t * u
__0_abs_thm	x x = 0 0 < Abs x
_less_recip_less_thm	x y 0 < x x < y y ^-¹ < x ^-¹
_abs__less_interval_thm	x y (Abs x y x ClosedInterval (~ y) y) (Abs x < y x OpenInterval (~ y) y)
_plus_recip_thm	x y x = 0 y = 0 x ^-¹ + y ^-¹ = (x + y) * x ^-¹ * y ^-¹
_recip_thm	m (m + 1) ^-¹ ^-¹ = (m + 1)
_0_less_recip_thm	m 0 < (m + 1) ^-¹
_recip_not_eq_0_thm	m (m + 1) ^-¹ = 0
__exp_0_1_thm	m 0 ^ (m + 1) = 0 1 ^ m = 1
__exp_square_thm	x x ^ 2 = x * x
__exp_0_less_thm	m x 0 < x 0 < x ^ m
__exp_1_less_mono_thm	x m 1 < x x ^ m < x ^ (m + 1)
__exp_1_less_mono_thm1	x m n 1 < x m < n x ^ m < x ^ n
__times_mono_thm	x y z 0 x y z x * y x * z
__exp__eq_0_thm	m x x = 0 x ^ m =