Theory integral

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

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

⊢ ∀D. dsize D = @N. (∀n. n < N ⇒ D n < D (SUC n)) ∧ ∀n. n ≥ N ⇒ D n = D N

⊢ ∀g D p. fine g (D,p) ⇔ ∀n. n < dsize D ⇒ D (SUC n) − D n < g (p n)

⊢ ∀E g. gauge E g ⇔ ∀x. E x ⇒ 0 < g x

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

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

⊢ ∀D p f. rsum (D,p) f = sum (0,dsize D) (λn. f (p n) * (D (SUC n) − D n))

⊢ ∀a b D p.
    tdiv (a,b) (D,p) ⇔ division (a,b) D ∧ ∀n. D n ≤ p n ∧ p n ≤ D (SUC n)

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

⊢ ∀a b. Dint (a,b) (λx. 0) 0

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

⊢ ∀a b f k1 k2. a ≤ b ∧ Dint (a,b) f k1 ∧ Dint (a,b) f k2 ⇒ k1 = k2

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

⊢ ∀a b. a = b ⇒ dsize (λn. if n = 0 then a else b) = 0

⊢ ∀a b. a < b ⇒ dsize (λn. if n = 0 then a else b) = 1

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

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

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

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

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

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

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

⊢ ∀D a b. division (a,b) D ⇒ (a = b ⇔ dsize D = 0)

⊢ ∀a b g.
    a ≤ b ∧ gauge (λx. a ≤ x ∧ x ≤ b) g ⇒
    ∃D p. tdiv (a,b) (D,p) ∧ fine g (D,p)

⊢ ∀D a b. division (a,b) D ⇒ ∀n. n < dsize D ⇒ D n < D (dsize D)

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

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

⊢ ∀D a b. division (a,b) D ⇒ ∀r. a ≤ D r

⊢ ∀D a b. division (a,b) D ∧ dsize D ≠ 0 ⇒ ∀n. a < D (SUC n)

⊢ ∀D a b. division (a,b) D ⇒ a ≤ b

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

⊢ ∀D a b. division (a,b) D ⇒ D 0 = a

⊢ ∀D a b. division (a,b) D ⇒ ∀n. n < dsize D ⇒ D 0 < D (SUC n)

⊢ ∀D a b m n. division (a,b) D ∧ m < n ∧ n ≤ dsize D ⇒ D m < D n

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

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

⊢ ∀D a b. division (a,b) D ⇒ D (dsize D) = b

⊢ ∀a b. a ≤ b ⇒ division (a,b) (λn. if n = 0 then a else b)

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

⊢ ∀D a b. division (a,b) D ⇒ ∀r. D r ≤ b

⊢ ∀D a b n. division (a,b) D ∧ n < dsize D ⇒ D n < b

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

⊢ ∀f a b k.
    a ≤ b ⇒ (Dint (a,b) f k ⇔ (f has_integral k) (interval [(a,b)]))

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

⊢ ∀f f' a b.
    a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ (f diffl f' x) x) ⇒
    Dint (a,b) f' (f b − f a)

⊢ ∀E g1 g2.
    gauge E g1 ∧ gauge E g2 ⇒
    gauge E (λx. if g1 x < g2 x then g1 x else g2 x)

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

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

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

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

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

⊢ ∀a b c. integrable (a,b) (λx. c)

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

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

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

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

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

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

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

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

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

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

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

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

⊢ ∀f a b c.
    a ≤ b ∧ b ≤ c ∧ integrable (a,c) f ⇒
    integral (a,c) f = integral (a,b) f + integral (b,c) f

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

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

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

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

⊢ ∀f a. Dint (a,a) f 0

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

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

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

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

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

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

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

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

⊢ ∀E g. gauge E g ⇔ ∀x. x ∈ E ⇒ 0 < g x

⊢ ∀c E g.
    0 < c ⇒ (gauge E g ⇔ gauge (λx. ball (x,if E x then c * g x else 1)))

⊢ ∀c g. 0 < c ⇒ (gauge 𝕌(:real) g ⇔ gauge (λx. ball (x,c * g x)))

⊢ ∀f a b. a ≤ b ⇒ (integrable (a,b) f ⇔ f integrable_on interval [(a,b)])

⊢ ∀f a b.
    a ≤ b ∧ f integrable_on interval [(a,b)] ⇒
    integration$integral (interval [(a,b)]) f = integral (a,b) f

⊢ ∀f a b.
    a ≤ b ∧ integrable (a,b) f ⇒
    integral (a,b) f = integration$integral (interval [(a,b)]) f