Structure limTheory
signature limTheory =
sig
type thm = Thm.thm
(* Definitions *)
val contl : thm
val differentiable : thm
val diffl : thm
val tends_real_real : thm
(* Theorems *)
val CONTL_LIM : thm
val CONT_ADD : thm
val CONT_ATTAINS : thm
val CONT_ATTAINS2 : thm
val CONT_ATTAINS_ALL : thm
val CONT_BOUNDED : thm
val CONT_COMPOSE : thm
val CONT_CONST : thm
val CONT_DIV : thm
val CONT_HASSUP : thm
val CONT_INJ_LEMMA : thm
val CONT_INJ_LEMMA2 : thm
val CONT_INJ_RANGE : thm
val CONT_INV : thm
val CONT_INVERSE : thm
val CONT_MUL : thm
val CONT_NEG : thm
val CONT_SUB : thm
val DIFF_ADD : thm
val DIFF_CARAT : thm
val DIFF_CHAIN : thm
val DIFF_CMUL : thm
val DIFF_CONST : thm
val DIFF_CONT : thm
val DIFF_DIV : thm
val DIFF_INV : thm
val DIFF_INVERSE : thm
val DIFF_INVERSE_LT : thm
val DIFF_INVERSE_OPEN : thm
val DIFF_ISCONST : thm
val DIFF_ISCONST_ALL : thm
val DIFF_ISCONST_END : thm
val DIFF_LCONST : thm
val DIFF_LDEC : thm
val DIFF_LINC : thm
val DIFF_LMAX : thm
val DIFF_LMIN : thm
val DIFF_MUL : thm
val DIFF_NEG : thm
val DIFF_POW : thm
val DIFF_SUB : thm
val DIFF_SUM : thm
val DIFF_UNIQ : thm
val DIFF_X : thm
val DIFF_XM1 : thm
val INTERVAL_ABS : thm
val INTERVAL_CLEMMA : thm
val INTERVAL_LEMMA : thm
val INTERVAL_LEMMA_LT : thm
val IVT : thm
val IVT2 : thm
val IVT_DERIVATIVE_0 : thm
val IVT_DERIVATIVE_NEG : thm
val IVT_DERIVATIVE_POS : thm
val LIM : thm
val LIM_ADD : thm
val LIM_AT_LIM : thm
val LIM_CONST : thm
val LIM_DIV : thm
val LIM_EQUAL : thm
val LIM_INV : thm
val LIM_MUL : thm
val LIM_NEG : thm
val LIM_NULL : thm
val LIM_SUB : thm
val LIM_TRANSFORM : thm
val LIM_UNIQ : thm
val LIM_X : thm
val MVT : thm
val MVT_LEMMA : thm
val ROLLE : thm
val contl_eq_continuous_at : thm
val differentiable_alt : thm
val differentiable_has_vector_derivative : thm
val diffl_has_derivative : thm
val diffl_has_derivative' : thm
val diffl_has_vector_derivative : thm
val lim_grammars : type_grammar.grammar * term_grammar.grammar
(*
[derivative] Parent theory of "lim"
[seq] Parent theory of "lim"
[contl] Definition
⊢ ∀f x. f contl x ⇔ ((λh. f (x + h)) -> f x) 0
[differentiable] Definition
⊢ ∀f x. f differentiable x ⇔ ∃l. (f diffl l) x
[diffl] Definition
⊢ ∀f l x. (f diffl l) x ⇔ ((λh. (f (x + h) − f x) / h) -> l) 0
[tends_real_real] Definition
⊢ ∀f l x0. (f -> l) x0 ⇔ (f tends l) (mtop mr1,tendsto (mr1,x0))
[CONTL_LIM] Theorem
⊢ ∀f x. f contl x ⇔ (f -> f x) x
[CONT_ADD] Theorem
⊢ ∀f g x. f contl x ∧ g contl x ⇒ (λx. f x + g x) contl x
[CONT_ATTAINS] Theorem
⊢ ∀f a b.
a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ⇒
∃M. (∀x. a ≤ x ∧ x ≤ b ⇒ f x ≤ M) ∧ ∃x. a ≤ x ∧ x ≤ b ∧ (f x = M)
[CONT_ATTAINS2] Theorem
⊢ ∀f a b.
a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ⇒
∃M. (∀x. a ≤ x ∧ x ≤ b ⇒ M ≤ f x) ∧ ∃x. a ≤ x ∧ x ≤ b ∧ (f x = M)
[CONT_ATTAINS_ALL] Theorem
⊢ ∀f a b.
a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ⇒
∃L M.
L ≤ M ∧ (∀y. L ≤ y ∧ y ≤ M ⇒ ∃x. a ≤ x ∧ x ≤ b ∧ (f x = y)) ∧
∀x. a ≤ x ∧ x ≤ b ⇒ L ≤ f x ∧ f x ≤ M
[CONT_BOUNDED] Theorem
⊢ ∀f a b.
a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ⇒
∃M. ∀x. a ≤ x ∧ x ≤ b ⇒ f x ≤ M
[CONT_COMPOSE] Theorem
⊢ ∀f g x. f contl x ∧ g contl f x ⇒ (λx. g (f x)) contl x
[CONT_CONST] Theorem
⊢ ∀k x. (λx. k) contl x
[CONT_DIV] Theorem
⊢ ∀f g x. f contl x ∧ g contl x ∧ g x ≠ 0 ⇒ (λx. f x / g x) contl x
[CONT_HASSUP] Theorem
⊢ ∀f a b.
a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ⇒
∃M. (∀x. a ≤ x ∧ x ≤ b ⇒ f x ≤ M) ∧
∀N. N < M ⇒ ∃x. a ≤ x ∧ x ≤ b ∧ N < f x
[CONT_INJ_LEMMA] Theorem
⊢ ∀f g x d.
0 < d ∧ (∀z. abs (z − x) ≤ d ⇒ (g (f z) = z)) ∧
(∀z. abs (z − x) ≤ d ⇒ f contl z) ⇒
¬∀z. abs (z − x) ≤ d ⇒ f z ≤ f x
[CONT_INJ_LEMMA2] Theorem
⊢ ∀f g x d.
0 < d ∧ (∀z. abs (z − x) ≤ d ⇒ (g (f z) = z)) ∧
(∀z. abs (z − x) ≤ d ⇒ f contl z) ⇒
¬∀z. abs (z − x) ≤ d ⇒ f x ≤ f z
[CONT_INJ_RANGE] Theorem
⊢ ∀f g x d.
0 < d ∧ (∀z. abs (z − x) ≤ d ⇒ (g (f z) = z)) ∧
(∀z. abs (z − x) ≤ d ⇒ f contl z) ⇒
∃e. 0 < e ∧
∀y. abs (y − f x) ≤ e ⇒ ∃z. abs (z − x) ≤ d ∧ (f z = y)
[CONT_INV] Theorem
⊢ ∀f x. f contl x ∧ f x ≠ 0 ⇒ (λx. (f x)⁻¹) contl x
[CONT_INVERSE] Theorem
⊢ ∀f g x d.
0 < d ∧ (∀z. abs (z − x) ≤ d ⇒ (g (f z) = z)) ∧
(∀z. abs (z − x) ≤ d ⇒ f contl z) ⇒
g contl f x
[CONT_MUL] Theorem
⊢ ∀f g x. f contl x ∧ g contl x ⇒ (λx. f x * g x) contl x
[CONT_NEG] Theorem
⊢ ∀f x. f contl x ⇒ (λx. -f x) contl x
[CONT_SUB] Theorem
⊢ ∀f g x. f contl x ∧ g contl x ⇒ (λx. f x − g x) contl x
[DIFF_ADD] Theorem
⊢ ∀f g l m x.
(f diffl l) x ∧ (g diffl m) x ⇒ ((λx. f x + g x) diffl (l + m)) x
[DIFF_CARAT] Theorem
⊢ ∀f l x.
(f diffl l) x ⇔
∃g. (∀z. f z − f x = g z * (z − x)) ∧ g contl x ∧ (g x = l)
[DIFF_CHAIN] Theorem
⊢ ∀f g l m x.
(f diffl l) (g x) ∧ (g diffl m) x ⇒
((λx. f (g x)) diffl (l * m)) x
[DIFF_CMUL] Theorem
⊢ ∀f c l x. (f diffl l) x ⇒ ((λx. c * f x) diffl (c * l)) x
[DIFF_CONST] Theorem
⊢ ∀k x. ((λx. k) diffl 0) x
[DIFF_CONT] Theorem
⊢ ∀f l x. (f diffl l) x ⇒ f contl x
[DIFF_DIV] Theorem
⊢ ∀f g l m x.
(f diffl l) x ∧ (g diffl m) x ∧ g x ≠ 0 ⇒
((λx. f x / g x) diffl ((l * g x − m * f x) / (g x)²)) x
[DIFF_INV] Theorem
⊢ ∀f l x.
(f diffl l) x ∧ f x ≠ 0 ⇒ ((λx. (f x)⁻¹) diffl -(l / (f x)²)) x
[DIFF_INVERSE] Theorem
⊢ ∀f g l x d.
0 < d ∧ (∀z. abs (z − x) ≤ d ⇒ (g (f z) = z)) ∧
(∀z. abs (z − x) ≤ d ⇒ f contl z) ∧ (f diffl l) x ∧ l ≠ 0 ⇒
(g diffl l⁻¹) (f x)
[DIFF_INVERSE_LT] Theorem
⊢ ∀f g l x d.
0 < d ∧ (∀z. abs (z − x) < d ⇒ (g (f z) = z)) ∧
(∀z. abs (z − x) < d ⇒ f contl z) ∧ (f diffl l) x ∧ l ≠ 0 ⇒
(g diffl l⁻¹) (f x)
[DIFF_INVERSE_OPEN] Theorem
⊢ ∀f g l a x b.
a < x ∧ x < b ∧ (∀z. a < z ∧ z < b ⇒ (g (f z) = z) ∧ f contl z) ∧
(f diffl l) x ∧ l ≠ 0 ⇒
(g diffl l⁻¹) (f x)
[DIFF_ISCONST] Theorem
⊢ ∀f a b.
a < b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ∧
(∀x. a < x ∧ x < b ⇒ (f diffl 0) x) ⇒
∀x. a ≤ x ∧ x ≤ b ⇒ (f x = f a)
[DIFF_ISCONST_ALL] Theorem
⊢ ∀f. (∀x. (f diffl 0) x) ⇒ ∀x y. f x = f y
[DIFF_ISCONST_END] Theorem
⊢ ∀f a b.
a < b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ∧
(∀x. a < x ∧ x < b ⇒ (f diffl 0) x) ⇒
(f b = f a)
[DIFF_LCONST] Theorem
⊢ ∀f x l.
(f diffl l) x ∧ (∃d. 0 < d ∧ ∀y. abs (x − y) < d ⇒ (f y = f x)) ⇒
(l = 0)
[DIFF_LDEC] Theorem
⊢ ∀f x l.
(f diffl l) x ∧ l < 0 ⇒
∃d. 0 < d ∧ ∀h. 0 < h ∧ h < d ⇒ f x < f (x − h)
[DIFF_LINC] Theorem
⊢ ∀f x l.
(f diffl l) x ∧ 0 < l ⇒
∃d. 0 < d ∧ ∀h. 0 < h ∧ h < d ⇒ f x < f (x + h)
[DIFF_LMAX] Theorem
⊢ ∀f x l.
(f diffl l) x ∧ (∃d. 0 < d ∧ ∀y. abs (x − y) < d ⇒ f y ≤ f x) ⇒
(l = 0)
[DIFF_LMIN] Theorem
⊢ ∀f x l.
(f diffl l) x ∧ (∃d. 0 < d ∧ ∀y. abs (x − y) < d ⇒ f x ≤ f y) ⇒
(l = 0)
[DIFF_MUL] Theorem
⊢ ∀f g l m x.
(f diffl l) x ∧ (g diffl m) x ⇒
((λx. f x * g x) diffl (l * g x + m * f x)) x
[DIFF_NEG] Theorem
⊢ ∀f l x. (f diffl l) x ⇒ ((λx. -f x) diffl -l) x
[DIFF_POW] Theorem
⊢ ∀n x. ((λx. x pow n) diffl (&n * x pow (n − 1))) x
[DIFF_SUB] Theorem
⊢ ∀f g l m x.
(f diffl l) x ∧ (g diffl m) x ⇒ ((λx. f x − g x) diffl (l − m)) x
[DIFF_SUM] Theorem
⊢ ∀f f' m n x.
(∀r. m ≤ r ∧ r < m + n ⇒ ((λx. f r x) diffl f' r x) x) ⇒
((λx. sum (m,n) (λn. f n x)) diffl sum (m,n) (λr. f' r x)) x
[DIFF_UNIQ] Theorem
⊢ ∀f l m x. (f diffl l) x ∧ (f diffl m) x ⇒ (l = m)
[DIFF_X] Theorem
⊢ ∀x. ((λx. x) diffl 1) x
[DIFF_XM1] Theorem
⊢ ∀x. x ≠ 0 ⇒ ((λx. x⁻¹) diffl -x⁻¹ ²) x
[INTERVAL_ABS] Theorem
⊢ ∀x z d. x − d ≤ z ∧ z ≤ x + d ⇔ abs (z − x) ≤ d
[INTERVAL_CLEMMA] Theorem
⊢ ∀a b x.
a < x ∧ x < b ⇒ ∃d. 0 < d ∧ ∀y. abs (y − x) ≤ d ⇒ a < y ∧ y < b
[INTERVAL_LEMMA] Theorem
⊢ ∀a b x.
a < x ∧ x < b ⇒ ∃d. 0 < d ∧ ∀y. abs (x − y) < d ⇒ a ≤ y ∧ y ≤ b
[INTERVAL_LEMMA_LT] Theorem
⊢ ∀a b x.
a < x ∧ x < b ⇒ ∃d. 0 < d ∧ ∀y. abs (x − y) < d ⇒ a < y ∧ y < b
[IVT] Theorem
⊢ ∀f a b y.
a ≤ b ∧ (f a ≤ y ∧ y ≤ f b) ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ⇒
∃x. a ≤ x ∧ x ≤ b ∧ (f x = y)
[IVT2] Theorem
⊢ ∀f a b y.
a ≤ b ∧ (f b ≤ y ∧ y ≤ f a) ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ⇒
∃x. a ≤ x ∧ x ≤ b ∧ (f x = y)
[IVT_DERIVATIVE_0] Theorem
⊢ ∀f f' a b.
a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ (f diffl f' x) x) ∧ f' a > 0 ∧
f' b < 0 ⇒
∃z. a < z ∧ z < b ∧ (f' z = 0)
[IVT_DERIVATIVE_NEG] Theorem
⊢ ∀f f' a b y.
a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ (f diffl f' x) x) ∧ f' a < y ∧
f' b > y ⇒
∃z. a < z ∧ z < b ∧ (f' z = y)
[IVT_DERIVATIVE_POS] Theorem
⊢ ∀f f' a b y.
a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ (f diffl f' x) x) ∧ f' a > y ∧
f' b < y ⇒
∃z. a < z ∧ z < b ∧ (f' z = y)
[LIM] Theorem
⊢ ∀f y0 x0.
(f -> y0) x0 ⇔
∀e. 0 < e ⇒
∃d. 0 < d ∧
∀x. 0 < abs (x − x0) ∧ abs (x − x0) < d ⇒
abs (f x − y0) < e
[LIM_ADD] Theorem
⊢ ∀f g l m x. (f -> l) x ∧ (g -> m) x ⇒ ((λx. f x + g x) -> l + m) x
[LIM_AT_LIM] Theorem
⊢ ∀f l a. (f --> l) (at a) ⇔ (f -> l) a
[LIM_CONST] Theorem
⊢ ∀k x. ((λx. k) -> k) x
[LIM_DIV] Theorem
⊢ ∀f g l m x.
(f -> l) x ∧ (g -> m) x ∧ m ≠ 0 ⇒ ((λx. f x / g x) -> l / m) x
[LIM_EQUAL] Theorem
⊢ ∀f g l x0. (∀x. x ≠ x0 ⇒ (f x = g x)) ⇒ ((f -> l) x0 ⇔ (g -> l) x0)
[LIM_INV] Theorem
⊢ ∀f l x. (f -> l) x ∧ l ≠ 0 ⇒ ((λx. (f x)⁻¹) -> l⁻¹) x
[LIM_MUL] Theorem
⊢ ∀f g l m x. (f -> l) x ∧ (g -> m) x ⇒ ((λx. f x * g x) -> l * m) x
[LIM_NEG] Theorem
⊢ ∀f l x. (f -> l) x ⇔ ((λx. -f x) -> -l) x
[LIM_NULL] Theorem
⊢ ∀f l x. (f -> l) x ⇔ ((λx. f x − l) -> 0) x
[LIM_SUB] Theorem
⊢ ∀f g l m x. (f -> l) x ∧ (g -> m) x ⇒ ((λx. f x − g x) -> l − m) x
[LIM_TRANSFORM] Theorem
⊢ ∀f g x0 l. ((λx. f x − g x) -> 0) x0 ∧ (g -> l) x0 ⇒ (f -> l) x0
[LIM_UNIQ] Theorem
⊢ ∀f l m x. (f -> l) x ∧ (f -> m) x ⇒ (l = m)
[LIM_X] Theorem
⊢ ∀x0. ((λx. x) -> x0) x0
[MVT] Theorem
⊢ ∀f a b.
a < b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ∧
(∀x. a < x ∧ x < b ⇒ f differentiable x) ⇒
∃l z. a < z ∧ z < b ∧ (f diffl l) z ∧ (f b − f a = (b − a) * l)
[MVT_LEMMA] Theorem
⊢ ∀f a b.
(λx. f x − (f b − f a) / (b − a) * x) a =
(λx. f x − (f b − f a) / (b − a) * x) b
[ROLLE] Theorem
⊢ ∀f a b.
a < b ∧ (f a = f b) ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ∧
(∀x. a < x ∧ x < b ⇒ f differentiable x) ⇒
∃z. a < z ∧ z < b ∧ (f diffl 0) z
[contl_eq_continuous_at] Theorem
⊢ ∀f x. f contl x ⇔ f continuous at x
[differentiable_alt] Theorem
⊢ ∀f x. f differentiable x ⇔ derivative$differentiable f (at x)
[differentiable_has_vector_derivative] Theorem
⊢ ∀f x. f differentiable x ⇔ ∃l. (f has_vector_derivative l) (at x)
[diffl_has_derivative] Theorem
⊢ ∀f l x. (f diffl l) x ⇔ (f has_derivative (λx. x * l)) (at x)
[diffl_has_derivative'] Theorem
⊢ ∀f l x. (f diffl l) x ⇔ (f has_derivative $* l) (at x)
[diffl_has_vector_derivative] Theorem
⊢ ∀f l x. (f diffl l) x ⇔ (f has_vector_derivative l) (at x)
*)
end
HOL 4, Trindemossen-1