Structure integralTheory
signature integralTheory =
sig
type thm = Thm.thm
(* Definitions *)
val Dint : thm
val division : thm
val dsize : thm
val fine : thm
val gauge : thm
val integrable : thm
val integral : thm
val rsum : thm
val tdiv : thm
(* Theorems *)
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_UNIQ : thm
val DINT_WRONG : thm
val DIVISION_0 : thm
val DIVISION_1 : thm
val DIVISION_APPEND : 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_EQ : thm
val DIVISION_EXISTS : thm
val DIVISION_GT : thm
val DIVISION_INTERMEDIATE : thm
val DIVISION_INTERMEDIATE' : thm
val DIVISION_LBOUND : thm
val DIVISION_LBOUND_LT : thm
val DIVISION_LE : thm
val DIVISION_LE_SUC : thm
val DIVISION_LHS : thm
val DIVISION_LT : thm
val DIVISION_LT_GEN : thm
val DIVISION_MONO_LE : thm
val DIVISION_MONO_LE_SUC : thm
val DIVISION_RHS : thm
val DIVISION_SINGLE : thm
val DIVISION_THM : thm
val DIVISION_UBOUND : thm
val DIVISION_UBOUND_LT : thm
val DSIZE_EQ : thm
val Dint_has_integral : thm
val FINE_MIN : thm
val FTC1 : thm
val GAUGE_MIN : 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_NULL : thm
val INTEGRAL_SUB : thm
val INTEGRATION_BY_PARTS : thm
val RSUM_BOUND : thm
val RSUM_DIFF_BOUND : thm
val STRADDLE_LEMMA : thm
val SUP_INTERVAL : thm
val TDIV_BOUNDS : thm
val TDIV_LE : thm
val gauge_alt : thm
val gauge_alt_univ : thm
val integrable_eq_integrable_on : thm
val integral_new_to_old : thm
val integral_old_to_new : thm
val integral_grammars : type_grammar.grammar * term_grammar.grammar
(*
[integration] Parent theory of "integral"
[powser] Parent theory of "integral"
[Dint] Definition
⊢ ∀a b f k.
Dint (a,b) f k ⇔
∀e. 0 < e ⇒
∃g. gauge (λx. a ≤ x ∧ x ≤ b) g ∧
∀D p.
tdiv (a,b) (D,p) ∧ fine g (D,p) ⇒
abs (rsum (D,p) f − k) < e
[division] Definition
⊢ ∀a b D.
division (a,b) D ⇔
D 0 = a ∧ ∃N. (∀n. n < N ⇒ D n < D (SUC n)) ∧ ∀n. n ≥ N ⇒ D n = b
[dsize] Definition
⊢ ∀D. dsize D =
@N. (∀n. n < N ⇒ D n < D (SUC n)) ∧ ∀n. n ≥ N ⇒ D n = D N
[fine] Definition
⊢ ∀g D p. fine g (D,p) ⇔ ∀n. n < dsize D ⇒ D (SUC n) − D n < g (p n)
[gauge] Definition
⊢ ∀E g. gauge E g ⇔ ∀x. E x ⇒ 0 < g x
[integrable] Definition
⊢ ∀a b f. integrable (a,b) f ⇔ ∃i. Dint (a,b) f i
[integral] Definition
⊢ ∀a b f. integral (a,b) f = @i. Dint (a,b) f i
[rsum] Definition
⊢ ∀D p f.
rsum (D,p) f = sum (0,dsize D) (λn. f (p n) * (D (SUC n) − D n))
[tdiv] Definition
⊢ ∀a b D p.
tdiv (a,b) (D,p) ⇔
division (a,b) D ∧ ∀n. D n ≤ p n ∧ p n ≤ D (SUC n)
[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_UNIQ] Theorem
⊢ ∀a b f k1 k2. a ≤ b ∧ Dint (a,b) f k1 ∧ Dint (a,b) f k2 ⇒ k1 = k2
[DINT_WRONG] Theorem
⊢ ∀a b f i. b < a ⇒ Dint (a,b) f i
[DIVISION_0] Theorem
⊢ ∀a b. a = b ⇒ dsize (λn. if n = 0 then a else b) = 0
[DIVISION_1] Theorem
⊢ ∀a b. a < b ⇒ dsize (λn. if n = 0 then a else b) = 1
[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_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_EQ] Theorem
⊢ ∀D a b. division (a,b) D ⇒ (a = b ⇔ dsize D = 0)
[DIVISION_EXISTS] Theorem
⊢ ∀a b g.
a ≤ b ∧ gauge (λx. a ≤ x ∧ x ≤ b) g ⇒
∃D p. tdiv (a,b) (D,p) ∧ fine g (D,p)
[DIVISION_GT] Theorem
⊢ ∀D a b. division (a,b) D ⇒ ∀n. n < dsize D ⇒ D n < D (dsize D)
[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_INTERMEDIATE'] Theorem
⊢ ∀d a b c.
division (a,b) d ∧ a ≤ c ∧ c ≤ b ∧ a < b ⇒
∃n. n < dsize d ∧ d n ≤ c ∧ c ≤ d (SUC n)
[DIVISION_LBOUND] Theorem
⊢ ∀D a b. division (a,b) D ⇒ ∀r. a ≤ D r
[DIVISION_LBOUND_LT] Theorem
⊢ ∀D a b. division (a,b) D ∧ dsize D ≠ 0 ⇒ ∀n. a < D (SUC n)
[DIVISION_LE] Theorem
⊢ ∀D a b. division (a,b) D ⇒ a ≤ b
[DIVISION_LE_SUC] Theorem
⊢ ∀d a b. division (a,b) d ⇒ ∀n. d n ≤ d (SUC n)
[DIVISION_LHS] Theorem
⊢ ∀D a b. division (a,b) D ⇒ D 0 = a
[DIVISION_LT] Theorem
⊢ ∀D a b. division (a,b) D ⇒ ∀n. n < dsize D ⇒ D 0 < D (SUC n)
[DIVISION_LT_GEN] Theorem
⊢ ∀D a b m n. division (a,b) D ∧ m < n ∧ n ≤ dsize D ⇒ D m < D 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)
[DIVISION_RHS] Theorem
⊢ ∀D a b. division (a,b) D ⇒ D (dsize D) = b
[DIVISION_SINGLE] Theorem
⊢ ∀a b. a ≤ b ⇒ division (a,b) (λn. if n = 0 then a else b)
[DIVISION_THM] Theorem
⊢ ∀D a b.
division (a,b) D ⇔
D 0 = a ∧ (∀n. n < dsize D ⇒ D n < D (SUC n)) ∧
∀n. n ≥ dsize D ⇒ D n = b
[DIVISION_UBOUND] Theorem
⊢ ∀D a b. division (a,b) D ⇒ ∀r. D r ≤ b
[DIVISION_UBOUND_LT] Theorem
⊢ ∀D a b n. division (a,b) D ∧ n < dsize D ⇒ D n < b
[DSIZE_EQ] Theorem
⊢ ∀a b D.
division (a,b) D ⇒
sum (0,dsize D) (λn. D (SUC n) − D n) − (b − a) = 0
[Dint_has_integral] Theorem
⊢ ∀f a b k.
a ≤ b ⇒ (Dint (a,b) f k ⇔ (f has_integral k) (interval [(a,b)]))
[FINE_MIN] Theorem
⊢ ∀g1 g2 D p.
fine (λx. if g1 x < g2 x then g1 x else g2 x) (D,p) ⇒
fine g1 (D,p) ∧ fine g2 (D,p)
[FTC1] Theorem
⊢ ∀f f' a b.
a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ (f diffl f' x) x) ⇒
Dint (a,b) f' (f b − f a)
[GAUGE_MIN] Theorem
⊢ ∀E g1 g2.
gauge E g1 ∧ gauge E g2 ⇒
gauge E (λx. if g1 x < g2 x then g1 x else g2 x)
[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_NULL] Theorem
⊢ ∀f a. Dint (a,a) f 0
[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)
[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)
[STRADDLE_LEMMA] Theorem
⊢ ∀f f' a b e.
(∀x. a ≤ x ∧ x ≤ b ⇒ (f diffl f' x) x) ∧ 0 < e ⇒
∃g. gauge (λx. a ≤ x ∧ x ≤ b) g ∧
∀x u v.
a ≤ u ∧ u ≤ x ∧ x ≤ v ∧ v ≤ b ∧ v − u < g x ⇒
abs (f v − f u − f' x * (v − u)) ≤ e * (v − u)
[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
[gauge_alt] Theorem
⊢ ∀c E g.
0 < c ⇒
(gauge E g ⇔ gauge (λx. ball (x,if E x then c * g x else 1)))
[gauge_alt_univ] Theorem
⊢ ∀c g. 0 < c ⇒ (gauge 𝕌(:real) g ⇔ gauge (λx. ball (x,c * g x)))
[integrable_eq_integrable_on] Theorem
⊢ ∀f a b.
a ≤ b ⇒ (integrable (a,b) f ⇔ f integrable_on interval [(a,b)])
[integral_new_to_old] Theorem
⊢ ∀f a b.
a ≤ b ∧ f integrable_on interval [(a,b)] ⇒
integration$integral (interval [(a,b)]) f = integral (a,b) f
[integral_old_to_new] Theorem
⊢ ∀f a b.
a ≤ b ∧ integrable (a,b) f ⇒
integral (a,b) f = integration$integral (interval [(a,b)]) f
*)
end
HOL 4, Trindemossen-1