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 ⇒ y⁻¹ ≤ 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)