Theory "integral"

Parents transc

Signature

Constant	Type
integrable	:complex -> (real -> real) -> bool
integral	:complex -> (real -> real) -> real

Definitions

integrable_def

|- ∀a b f. integrable (a,b) f ⇔ ∃i. Dint (a,b) f i

integral_def

|- ∀a b f. integral (a,b) f = @i. Dint (a,b) f i

Theorems

SUM_SPLIT

|- ∀f n p. sum (m,n) f + sum (m + n,p) f = sum (m,n + p) f

DIVISION_APPEND_EXPLICIT

|- ∀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

|- ∀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_APPEND

|- ∀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)

INTEGRABLE_DINT

|- ∀f a b. integrable (a,b) f ⇒ Dint (a,b) f (integral (a,b) f)

DIVISION_BOUNDS

|- ∀d a b. division (a,b) d ⇒ ∀n. a ≤ d n ∧ d n ≤ b

TDIV_BOUNDS

|- ∀d p a b. tdiv (a,b) (d,p) ⇒ ∀n. a ≤ d n ∧ d n ≤ b ∧ a ≤ p n ∧ p n ≤ b

TDIV_LE

|- ∀d p a b. tdiv (a,b) (d,p) ⇒ a ≤ b

DINT_WRONG

|- ∀a b f i. b < a ⇒ Dint (a,b) f i

DINT_INTEGRAL

|- ∀f a b i. a ≤ b ∧ Dint (a,b) f i ⇒ (integral (a,b) f = i)

DINT_NEG

|- ∀f a b i. Dint (a,b) f i ⇒ Dint (a,b) (λx. -f x) (-i)

DINT_0

|- ∀a b. Dint (a,b) (λx. 0) 0

DINT_ADD

|- ∀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_SUB

|- ∀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)

DSIZE_EQ

|- ∀a b D.
     division (a,b) D ⇒ (sum (0,dsize D) (λn. D (SUC n) − D n) − (b − a) = 0)

DINT_CONST

|- ∀a b c. Dint (a,b) (λx. c) (c * (b − a))

DINT_CMUL

|- ∀f a b c i. Dint (a,b) f i ⇒ Dint (a,b) (λx. c * f x) (c * i)

DINT_LINEAR

|- ∀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)

LT

|- (∀m. m < 0 ⇔ F) ∧ ∀m n. m < SUC n ⇔ (m = n) ∨ m < n

LE_0

|- ∀n. 0 ≤ n

LT_0

|- ∀n. 0 < SUC n

EQ_SUC

|- ∀m n. (SUC m = SUC n) ⇔ (m = n)

LE_LT

|- ∀m n. m ≤ n ⇔ m < n ∨ (m = n)

LT_LE

|- ∀m n. m < n ⇔ m ≤ n ∧ m ≠ n

REAL_LT_MIN

|- ∀x y z. z < min x y ⇔ z < x ∧ z < y

REAL_LE_RMUL1

|- ∀x y z. x ≤ y ∧ 0 ≤ z ⇒ x * z ≤ y * z

REAL_LE_LMUL1

|- ∀x y z. 0 ≤ x ∧ y ≤ z ⇒ x * y ≤ x * z

INTEGRAL_LE

|- ∀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

DINT_LE

|- ∀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_TRIANGLE

|- ∀f a b i j.
     a ≤ b ∧ Dint (a,b) f i ∧ Dint (a,b) (λx. abs (f x)) j ⇒ abs i ≤ j

DINT_EQ

|- ∀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)

INTEGRAL_EQ

|- ∀f g a b i.
     Dint (a,b) f i ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ (f x = g x)) ⇒ Dint (a,b) g i

INTEGRATION_BY_PARTS

|- ∀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)

DIVISION_LE_SUC

|- ∀d a b. division (a,b) d ⇒ ∀n. d n ≤ d (SUC n)

DIVISION_MONO_LE

|- ∀d a b. division (a,b) d ⇒ ∀m n. m ≤ n ⇒ d m ≤ d n

DIVISION_MONO_LE_SUC

|- ∀d a b. division (a,b) d ⇒ ∀n. d n ≤ d (SUC n)

DIVISION_DSIZE_LE

|- ∀a b d n. division (a,b) d ∧ (d (SUC n) = d n) ⇒ dsize d ≤ n

DIVISION_DSIZE_GE

|- ∀a b d n. division (a,b) d ∧ d n < d (SUC n) ⇒ SUC n ≤ dsize d

DIVISION_DSIZE_EQ

|- ∀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

|- ∀a b d n.
     division (a,b) d ∧ (d (SUC n) = d n) ∧ (∀i. i < n ⇒ d i < d (SUC i)) ⇒
     (dsize d = n)

num_MAX

|- ∀P. (∃x. P x) ∧ (∃M. ∀x. P x ⇒ x ≤ M) ⇔ ∃m. P m ∧ ∀x. P x ⇒ x ≤ m

DIVISION_INTERMEDIATE

|- ∀d a b c.
     division (a,b) d ∧ a ≤ c ∧ c ≤ b ⇒
     ∃n. n ≤ dsize d ∧ d n ≤ c ∧ c ≤ d (SUC n)

DINT_COMBINE

|- ∀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)

SUM_EQ_0

|- (∀r. m ≤ r ∧ r < m + n ⇒ (f r = 0)) ⇒ (sum (m,n) f = 0)

DINT_DELTA_LEFT

|- ∀a b. Dint (a,b) (λx. if x = a then 1 else 0) 0

DINT_DELTA_RIGHT

|- ∀a b. Dint (a,b) (λx. if x = b then 1 else 0) 0

DINT_DELTA

|- ∀a b c. Dint (a,b) (λx. if x = c then 1 else 0) 0

DINT_POINT_SPIKE

|- ∀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_FINITE_SPIKE

|- ∀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

REAL_POW_LBOUND

|- ∀x n. 0 ≤ x ⇒ 1 + &n * x ≤ (1 + x) pow n

REAL_ARCH_POW

|- ∀x y. 1 < x ⇒ ∃n. y < x pow n

REAL_ARCH_POW2

|- ∀x. ∃n. x < 2 pow n

REAL_POW_LE_1

|- ∀n x. 1 ≤ x ⇒ 1 ≤ x pow n

REAL_POW_MONO

|- ∀m n x. 1 ≤ x ∧ m ≤ n ⇒ x pow m ≤ x pow n

REAL_LE_INV2

|- ∀x y. 0 < x ∧ x ≤ y ⇒ inv y ≤ inv x

GAUGE_MIN_FINITE

|- ∀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_CAUCHY

|- ∀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

SUM_DIFFS

|- ∀m n. sum (m,n) (λi. d (SUC i) − d i) = d (m + n) − d m

RSUM_BOUND

|- ∀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

|- ∀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)

INTEGRABLE_LIMIT

|- ∀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_CONST

|- ∀a b c. integrable (a,b) (λx. c)

INTEGRABLE_ADD

|- ∀f g a b.
     a ≤ b ∧ integrable (a,b) f ∧ integrable (a,b) g ⇒
     integrable (a,b) (λx. f x + g x)

INTEGRABLE_CMUL

|- ∀f a b c. a ≤ b ∧ integrable (a,b) f ⇒ integrable (a,b) (λx. c * f x)

INTEGRABLE_COMBINE

|- ∀f a b c.
     a ≤ b ∧ b ≤ c ∧ integrable (a,b) f ∧ integrable (b,c) f ⇒
     integrable (a,c) f

INTEGRABLE_POINT_SPIKE

|- ∀f g a b c.
     (∀x. a ≤ x ∧ x ≤ b ∧ x ≠ c ⇒ (f x = g x)) ∧ integrable (a,b) f ⇒
     integrable (a,b) g

SUP_INTERVAL

|- ∀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

BOLZANO_LEMMA_ALT

|- ∀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

|- ∀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

INTEGRABLE_CONTINUOUS

|- ∀f a b. (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ⇒ integrable (a,b) f

INTEGRABLE_SPLIT_SIDES

|- ∀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_LEFT

|- ∀f a b c. a ≤ c ∧ c ≤ b ∧ integrable (a,b) f ⇒ integrable (a,c) f

INTEGRABLE_SUBINTERVAL_RIGHT

|- ∀f a b c. a ≤ c ∧ c ≤ b ∧ integrable (a,b) f ⇒ integrable (c,b) f

INTEGRABLE_SUBINTERVAL

|- ∀f a b c d. a ≤ c ∧ c ≤ d ∧ d ≤ b ∧ integrable (a,b) f ⇒ integrable (c,d) f

INTEGRAL_0

|- ∀a b. a ≤ b ⇒ (integral (a,b) (λx. 0) = 0)

INTEGRAL_CONST

|- ∀a b c. a ≤ b ⇒ (integral (a,b) (λx. c) = c * (b − a))

INTEGRAL_CMUL

|- ∀f c a b.
     a ≤ b ∧ integrable (a,b) f ⇒
     (integral (a,b) (λx. c * f x) = c * integral (a,b) f)

INTEGRAL_ADD

|- ∀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_SUB

|- ∀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

|- ∀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_COMBINE

|- ∀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_MVT1

|- ∀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))