Structure integralTheory
signature integralTheory =
sig
type thm = Thm.thm
(* Definitions *)
val integrable_def : thm
val integral_def : thm
(* Theorems *)
val BOLZANO_LEMMA_ALT : thm
val CONT_UNIFORM : thm
val DINT_0 : thm
val DINT_ADD : thm
val DINT_CMUL : thm
val DINT_COMBINE : thm
val DINT_CONST : thm
val DINT_DELTA : thm
val DINT_DELTA_LEFT : thm
val DINT_DELTA_RIGHT : thm
val DINT_EQ : thm
val DINT_FINITE_SPIKE : thm
val DINT_INTEGRAL : thm
val DINT_LE : thm
val DINT_LINEAR : thm
val DINT_NEG : thm
val DINT_POINT_SPIKE : thm
val DINT_SUB : thm
val DINT_TRIANGLE : thm
val DINT_WRONG : thm
val DIVISION_APPEND : thm
val DIVISION_APPEND_EXPLICIT : thm
val DIVISION_APPEND_STRONG : thm
val DIVISION_BOUNDS : thm
val DIVISION_DSIZE_EQ : thm
val DIVISION_DSIZE_EQ_ALT : thm
val DIVISION_DSIZE_GE : thm
val DIVISION_DSIZE_LE : thm
val DIVISION_INTERMEDIATE : thm
val DIVISION_LE_SUC : thm
val DIVISION_MONO_LE : thm
val DIVISION_MONO_LE_SUC : thm
val DSIZE_EQ : thm
val EQ_SUC : thm
val GAUGE_MIN_FINITE : thm
val INTEGRABLE_ADD : thm
val INTEGRABLE_CAUCHY : thm
val INTEGRABLE_CMUL : thm
val INTEGRABLE_COMBINE : thm
val INTEGRABLE_CONST : thm
val INTEGRABLE_CONTINUOUS : thm
val INTEGRABLE_DINT : thm
val INTEGRABLE_LIMIT : thm
val INTEGRABLE_POINT_SPIKE : thm
val INTEGRABLE_SPLIT_SIDES : thm
val INTEGRABLE_SUBINTERVAL : thm
val INTEGRABLE_SUBINTERVAL_LEFT : thm
val INTEGRABLE_SUBINTERVAL_RIGHT : thm
val INTEGRAL_0 : thm
val INTEGRAL_ADD : thm
val INTEGRAL_BY_PARTS : thm
val INTEGRAL_CMUL : thm
val INTEGRAL_COMBINE : thm
val INTEGRAL_CONST : thm
val INTEGRAL_EQ : thm
val INTEGRAL_LE : thm
val INTEGRAL_MVT1 : thm
val INTEGRAL_SUB : thm
val INTEGRATION_BY_PARTS : thm
val LE_0 : thm
val LE_LT : thm
val LT : thm
val LT_0 : thm
val LT_LE : thm
val REAL_ARCH_POW : thm
val REAL_ARCH_POW2 : thm
val REAL_LE_INV2 : thm
val REAL_LE_LMUL1 : thm
val REAL_LE_RMUL1 : thm
val REAL_LT_MIN : thm
val REAL_POW_LBOUND : thm
val REAL_POW_LE_1 : thm
val REAL_POW_MONO : thm
val RSUM_BOUND : thm
val RSUM_DIFF_BOUND : thm
val SUM_DIFFS : thm
val SUM_EQ_0 : thm
val SUM_SPLIT : thm
val SUP_INTERVAL : thm
val TDIV_BOUNDS : thm
val TDIV_LE : thm
val num_MAX : thm
val integral_grammars : type_grammar.grammar * term_grammar.grammar
(*
[transc] Parent theory of "integral"
[integrable_def] Definition
⊢ ∀a b f. integrable (a,b) f ⇔ ∃i. Dint (a,b) f i
[integral_def] Definition
⊢ ∀a b f. integral (a,b) f = @i. Dint (a,b) f i
[BOLZANO_LEMMA_ALT] Theorem
⊢ ∀P. (∀a b c. a ≤ b ∧ b ≤ c ∧ P a b ∧ P b c ⇒ P a c) ∧
(∀x. ∃d. 0 < d ∧ ∀a b. a ≤ x ∧ x ≤ b ∧ b − a < d ⇒ P a b) ⇒
∀a b. a ≤ b ⇒ P a b
[CONT_UNIFORM] Theorem
⊢ ∀f a b.
a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ⇒
∀e. 0 < e ⇒
∃d. 0 < d ∧
∀x y.
a ≤ x ∧ x ≤ b ∧ a ≤ y ∧ y ≤ b ∧ abs (x − y) < d ⇒
abs (f x − f y) < e
[DINT_0] Theorem
⊢ ∀a b. Dint (a,b) (λx. 0) 0
[DINT_ADD] Theorem
⊢ ∀f g a b i j.
Dint (a,b) f i ∧ Dint (a,b) g j ⇒
Dint (a,b) (λx. f x + g x) (i + j)
[DINT_CMUL] Theorem
⊢ ∀f a b c i. Dint (a,b) f i ⇒ Dint (a,b) (λx. c * f x) (c * i)
[DINT_COMBINE] Theorem
⊢ ∀f a b c i j.
a ≤ b ∧ b ≤ c ∧ Dint (a,b) f i ∧ Dint (b,c) f j ⇒
Dint (a,c) f (i + j)
[DINT_CONST] Theorem
⊢ ∀a b c. Dint (a,b) (λx. c) (c * (b − a))
[DINT_DELTA] Theorem
⊢ ∀a b c. Dint (a,b) (λx. if x = c then 1 else 0) 0
[DINT_DELTA_LEFT] Theorem
⊢ ∀a b. Dint (a,b) (λx. if x = a then 1 else 0) 0
[DINT_DELTA_RIGHT] Theorem
⊢ ∀a b. Dint (a,b) (λx. if x = b then 1 else 0) 0
[DINT_EQ] Theorem
⊢ ∀f g a b i j.
a ≤ b ∧ Dint (a,b) f i ∧ Dint (a,b) g j ∧
(∀x. a ≤ x ∧ x ≤ b ⇒ (f x = g x)) ⇒
(i = j)
[DINT_FINITE_SPIKE] Theorem
⊢ ∀f g a b s i.
FINITE s ∧ (∀x. a ≤ x ∧ x ≤ b ∧ x ∉ s ⇒ (f x = g x)) ∧
Dint (a,b) f i ⇒
Dint (a,b) g i
[DINT_INTEGRAL] Theorem
⊢ ∀f a b i. a ≤ b ∧ Dint (a,b) f i ⇒ (integral (a,b) f = i)
[DINT_LE] Theorem
⊢ ∀f g a b i j.
a ≤ b ∧ Dint (a,b) f i ∧ Dint (a,b) g j ∧
(∀x. a ≤ x ∧ x ≤ b ⇒ f x ≤ g x) ⇒
i ≤ j
[DINT_LINEAR] Theorem
⊢ ∀f g a b i j.
Dint (a,b) f i ∧ Dint (a,b) g j ⇒
Dint (a,b) (λx. m * f x + n * g x) (m * i + n * j)
[DINT_NEG] Theorem
⊢ ∀f a b i. Dint (a,b) f i ⇒ Dint (a,b) (λx. -f x) (-i)
[DINT_POINT_SPIKE] Theorem
⊢ ∀f g a b c i.
(∀x. a ≤ x ∧ x ≤ b ∧ x ≠ c ⇒ (f x = g x)) ∧ Dint (a,b) f i ⇒
Dint (a,b) g i
[DINT_SUB] Theorem
⊢ ∀f g a b i j.
Dint (a,b) f i ∧ Dint (a,b) g j ⇒
Dint (a,b) (λx. f x − g x) (i − j)
[DINT_TRIANGLE] Theorem
⊢ ∀f a b i j.
a ≤ b ∧ Dint (a,b) f i ∧ Dint (a,b) (λx. abs (f x)) j ⇒ abs i ≤ j
[DINT_WRONG] Theorem
⊢ ∀a b f i. b < a ⇒ Dint (a,b) f i
[DIVISION_APPEND] Theorem
⊢ ∀a b c.
(∃D1 p1. tdiv (a,b) (D1,p1) ∧ fine g (D1,p1)) ∧
(∃D2 p2. tdiv (b,c) (D2,p2) ∧ fine g (D2,p2)) ⇒
∃D p. tdiv (a,c) (D,p) ∧ fine g (D,p)
[DIVISION_APPEND_EXPLICIT] Theorem
⊢ ∀a b c g d1 p1 d2 p2.
tdiv (a,b) (d1,p1) ∧ fine g (d1,p1) ∧ tdiv (b,c) (d2,p2) ∧
fine g (d2,p2) ⇒
tdiv (a,c)
((λn. if n < dsize d1 then d1 n else d2 (n − dsize d1)),
(λn. if n < dsize d1 then p1 n else p2 (n − dsize d1))) ∧
fine g
((λn. if n < dsize d1 then d1 n else d2 (n − dsize d1)),
(λn. if n < dsize d1 then p1 n else p2 (n − dsize d1))) ∧
∀f. rsum
((λn. if n < dsize d1 then d1 n else d2 (n − dsize d1)),
(λn. if n < dsize d1 then p1 n else p2 (n − dsize d1))) f =
rsum (d1,p1) f + rsum (d2,p2) f
[DIVISION_APPEND_STRONG] Theorem
⊢ ∀a b c D1 p1 D2 p2.
tdiv (a,b) (D1,p1) ∧ fine g (D1,p1) ∧ tdiv (b,c) (D2,p2) ∧
fine g (D2,p2) ⇒
∃D p.
tdiv (a,c) (D,p) ∧ fine g (D,p) ∧
∀f. rsum (D,p) f = rsum (D1,p1) f + rsum (D2,p2) f
[DIVISION_BOUNDS] Theorem
⊢ ∀d a b. division (a,b) d ⇒ ∀n. a ≤ d n ∧ d n ≤ b
[DIVISION_DSIZE_EQ] Theorem
⊢ ∀a b d n.
division (a,b) d ∧ d n < d (SUC n) ∧
(d (SUC (SUC n)) = d (SUC n)) ⇒
(dsize d = SUC n)
[DIVISION_DSIZE_EQ_ALT] Theorem
⊢ ∀a b d n.
division (a,b) d ∧ (d (SUC n) = d n) ∧
(∀i. i < n ⇒ d i < d (SUC i)) ⇒
(dsize d = n)
[DIVISION_DSIZE_GE] Theorem
⊢ ∀a b d n. division (a,b) d ∧ d n < d (SUC n) ⇒ SUC n ≤ dsize d
[DIVISION_DSIZE_LE] Theorem
⊢ ∀a b d n. division (a,b) d ∧ (d (SUC n) = d n) ⇒ dsize d ≤ n
[DIVISION_INTERMEDIATE] Theorem
⊢ ∀d a b c.
division (a,b) d ∧ a ≤ c ∧ c ≤ b ⇒
∃n. n ≤ dsize d ∧ d n ≤ c ∧ c ≤ d (SUC n)
[DIVISION_LE_SUC] Theorem
⊢ ∀d a b. division (a,b) d ⇒ ∀n. d n ≤ d (SUC n)
[DIVISION_MONO_LE] Theorem
⊢ ∀d a b. division (a,b) d ⇒ ∀m n. m ≤ n ⇒ d m ≤ d n
[DIVISION_MONO_LE_SUC] Theorem
⊢ ∀d a b. division (a,b) d ⇒ ∀n. d n ≤ d (SUC n)
[DSIZE_EQ] Theorem
⊢ ∀a b D.
division (a,b) D ⇒
(sum (0,dsize D) (λn. D (SUC n) − D n) − (b − a) = 0)
[EQ_SUC] Theorem
⊢ ∀m n. (SUC m = SUC n) ⇔ (m = n)
[GAUGE_MIN_FINITE] Theorem
⊢ ∀s gs n.
(∀m. m ≤ n ⇒ gauge s (gs m)) ⇒
∃g. gauge s g ∧
∀d p. fine g (d,p) ⇒ ∀m. m ≤ n ⇒ fine (gs m) (d,p)
[INTEGRABLE_ADD] Theorem
⊢ ∀f g a b.
a ≤ b ∧ integrable (a,b) f ∧ integrable (a,b) g ⇒
integrable (a,b) (λx. f x + g x)
[INTEGRABLE_CAUCHY] Theorem
⊢ ∀f a b.
integrable (a,b) f ⇔
∀e. 0 < e ⇒
∃g. gauge (λx. a ≤ x ∧ x ≤ b) g ∧
∀d1 p1 d2 p2.
tdiv (a,b) (d1,p1) ∧ fine g (d1,p1) ∧
tdiv (a,b) (d2,p2) ∧ fine g (d2,p2) ⇒
abs (rsum (d1,p1) f − rsum (d2,p2) f) < e
[INTEGRABLE_CMUL] Theorem
⊢ ∀f a b c.
a ≤ b ∧ integrable (a,b) f ⇒ integrable (a,b) (λx. c * f x)
[INTEGRABLE_COMBINE] Theorem
⊢ ∀f a b c.
a ≤ b ∧ b ≤ c ∧ integrable (a,b) f ∧ integrable (b,c) f ⇒
integrable (a,c) f
[INTEGRABLE_CONST] Theorem
⊢ ∀a b c. integrable (a,b) (λx. c)
[INTEGRABLE_CONTINUOUS] Theorem
⊢ ∀f a b. (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ⇒ integrable (a,b) f
[INTEGRABLE_DINT] Theorem
⊢ ∀f a b. integrable (a,b) f ⇒ Dint (a,b) f (integral (a,b) f)
[INTEGRABLE_LIMIT] Theorem
⊢ ∀f a b.
(∀e. 0 < e ⇒
∃g. (∀x. a ≤ x ∧ x ≤ b ⇒ abs (f x − g x) ≤ e) ∧
integrable (a,b) g) ⇒
integrable (a,b) f
[INTEGRABLE_POINT_SPIKE] Theorem
⊢ ∀f g a b c.
(∀x. a ≤ x ∧ x ≤ b ∧ x ≠ c ⇒ (f x = g x)) ∧ integrable (a,b) f ⇒
integrable (a,b) g
[INTEGRABLE_SPLIT_SIDES] Theorem
⊢ ∀f a b c.
a ≤ c ∧ c ≤ b ∧ integrable (a,b) f ⇒
∃i. ∀e.
0 < e ⇒
∃g. gauge (λx. a ≤ x ∧ x ≤ b) g ∧
∀d1 p1 d2 p2.
tdiv (a,c) (d1,p1) ∧ fine g (d1,p1) ∧
tdiv (c,b) (d2,p2) ∧ fine g (d2,p2) ⇒
abs (rsum (d1,p1) f + rsum (d2,p2) f − i) < e
[INTEGRABLE_SUBINTERVAL] Theorem
⊢ ∀f a b c d.
a ≤ c ∧ c ≤ d ∧ d ≤ b ∧ integrable (a,b) f ⇒ integrable (c,d) f
[INTEGRABLE_SUBINTERVAL_LEFT] Theorem
⊢ ∀f a b c. a ≤ c ∧ c ≤ b ∧ integrable (a,b) f ⇒ integrable (a,c) f
[INTEGRABLE_SUBINTERVAL_RIGHT] Theorem
⊢ ∀f a b c. a ≤ c ∧ c ≤ b ∧ integrable (a,b) f ⇒ integrable (c,b) f
[INTEGRAL_0] Theorem
⊢ ∀a b. a ≤ b ⇒ (integral (a,b) (λx. 0) = 0)
[INTEGRAL_ADD] Theorem
⊢ ∀f g a b.
a ≤ b ∧ integrable (a,b) f ∧ integrable (a,b) g ⇒
(integral (a,b) (λx. f x + g x) =
integral (a,b) f + integral (a,b) g)
[INTEGRAL_BY_PARTS] Theorem
⊢ ∀f g f' g' a b.
a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ (f diffl f' x) x) ∧
(∀x. a ≤ x ∧ x ≤ b ⇒ (g diffl g' x) x) ∧
integrable (a,b) (λx. f' x * g x) ∧
integrable (a,b) (λx. f x * g' x) ⇒
(integral (a,b) (λx. f x * g' x) =
f b * g b − f a * g a − integral (a,b) (λx. f' x * g x))
[INTEGRAL_CMUL] Theorem
⊢ ∀f c a b.
a ≤ b ∧ integrable (a,b) f ⇒
(integral (a,b) (λx. c * f x) = c * integral (a,b) f)
[INTEGRAL_COMBINE] Theorem
⊢ ∀f a b c.
a ≤ b ∧ b ≤ c ∧ integrable (a,c) f ⇒
(integral (a,c) f = integral (a,b) f + integral (b,c) f)
[INTEGRAL_CONST] Theorem
⊢ ∀a b c. a ≤ b ⇒ (integral (a,b) (λx. c) = c * (b − a))
[INTEGRAL_EQ] Theorem
⊢ ∀f g a b i.
Dint (a,b) f i ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ (f x = g x)) ⇒
Dint (a,b) g i
[INTEGRAL_LE] Theorem
⊢ ∀f g a b i j.
a ≤ b ∧ integrable (a,b) f ∧ integrable (a,b) g ∧
(∀x. a ≤ x ∧ x ≤ b ⇒ f x ≤ g x) ⇒
integral (a,b) f ≤ integral (a,b) g
[INTEGRAL_MVT1] Theorem
⊢ ∀f a b.
a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ⇒
∃x. a ≤ x ∧ x ≤ b ∧ (integral (a,b) f = f x * (b − a))
[INTEGRAL_SUB] Theorem
⊢ ∀f g a b.
a ≤ b ∧ integrable (a,b) f ∧ integrable (a,b) g ⇒
(integral (a,b) (λx. f x − g x) =
integral (a,b) f − integral (a,b) g)
[INTEGRATION_BY_PARTS] Theorem
⊢ ∀f g f' g' a b.
a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ (f diffl f' x) x) ∧
(∀x. a ≤ x ∧ x ≤ b ⇒ (g diffl g' x) x) ⇒
Dint (a,b) (λx. f' x * g x + f x * g' x) (f b * g b − f a * g a)
[LE_0] Theorem
⊢ ∀n. 0 ≤ n
[LE_LT] Theorem
⊢ ∀m n. m ≤ n ⇔ m < n ∨ (m = n)
[LT] Theorem
⊢ (∀m. m < 0 ⇔ F) ∧ ∀m n. m < SUC n ⇔ (m = n) ∨ m < n
[LT_0] Theorem
⊢ ∀n. 0 < SUC n
[LT_LE] Theorem
⊢ ∀m n. m < n ⇔ m ≤ n ∧ m ≠ n
[REAL_ARCH_POW] Theorem
⊢ ∀x y. 1 < x ⇒ ∃n. y < x pow n
[REAL_ARCH_POW2] Theorem
⊢ ∀x. ∃n. x < 2 pow n
[REAL_LE_INV2] Theorem
⊢ ∀x y. 0 < x ∧ x ≤ y ⇒ y⁻¹ ≤ x⁻¹
[REAL_LE_LMUL1] Theorem
⊢ ∀x y z. 0 ≤ x ∧ y ≤ z ⇒ x * y ≤ x * z
[REAL_LE_RMUL1] Theorem
⊢ ∀x y z. x ≤ y ∧ 0 ≤ z ⇒ x * z ≤ y * z
[REAL_LT_MIN] Theorem
⊢ ∀x y z. z < min x y ⇔ z < x ∧ z < y
[REAL_POW_LBOUND] Theorem
⊢ ∀x n. 0 ≤ x ⇒ 1 + &n * x ≤ (1 + x) pow n
[REAL_POW_LE_1] Theorem
⊢ ∀n x. 1 ≤ x ⇒ 1 ≤ x pow n
[REAL_POW_MONO] Theorem
⊢ ∀m n x. 1 ≤ x ∧ m ≤ n ⇒ x pow m ≤ x pow n
[RSUM_BOUND] Theorem
⊢ ∀a b d p e f.
tdiv (a,b) (d,p) ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ abs (f x) ≤ e) ⇒
abs (rsum (d,p) f) ≤ e * (b − a)
[RSUM_DIFF_BOUND] Theorem
⊢ ∀a b d p e f g.
tdiv (a,b) (d,p) ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ abs (f x − g x) ≤ e) ⇒
abs (rsum (d,p) f − rsum (d,p) g) ≤ e * (b − a)
[SUM_DIFFS] Theorem
⊢ ∀m n. sum (m,n) (λi. d (SUC i) − d i) = d (m + n) − d m
[SUM_EQ_0] Theorem
⊢ (∀r. m ≤ r ∧ r < m + n ⇒ (f r = 0)) ⇒ (sum (m,n) f = 0)
[SUM_SPLIT] Theorem
⊢ ∀f n p. sum (m,n) f + sum (m + n,p) f = sum (m,n + p) f
[SUP_INTERVAL] Theorem
⊢ ∀P a b.
(∃x. a ≤ x ∧ x ≤ b ∧ P x) ⇒
∃s. a ≤ s ∧ s ≤ b ∧ ∀y. y < s ⇔ ∃x. a ≤ x ∧ x ≤ b ∧ P x ∧ y < x
[TDIV_BOUNDS] Theorem
⊢ ∀d p a b.
tdiv (a,b) (d,p) ⇒ ∀n. a ≤ d n ∧ d n ≤ b ∧ a ≤ p n ∧ p n ≤ b
[TDIV_LE] Theorem
⊢ ∀d p a b. tdiv (a,b) (d,p) ⇒ a ≤ b
[num_MAX] Theorem
⊢ ∀P. (∃x. P x) ∧ (∃M. ∀x. P x ⇒ x ≤ M) ⇔ ∃m. P m ∧ ∀x. P x ⇒ x ≤ m
*)
end
HOL 4, Kananaskis-14