Theory "integration"

Signature

Definitions

FINE

⊢ ∀d s. d FINE s ⇔ ∀x k. (x,k) ∈ s ⇒ k ⊆ d x

absolutely_integrable_on

⊢ ∀f s.
    f absolutely_integrable_on s ⇔
    f integrable_on s ∧ (λx. abs (f x)) integrable_on s

content

⊢ ∀s. content s =
      if s = ∅ then 0 else interval_upperbound s − interval_lowerbound s

division_of

⊢ ∀s i.
    s division_of i ⇔
    FINITE s ∧ (∀k. k ∈ s ⇒ k ⊆ i ∧ k ≠ ∅ ∧ ∃a b. k = interval [(a,b)]) ∧
    (∀k1 k2. k1 ∈ s ∧ k2 ∈ s ∧ k1 ≠ k2 ⇒ (interior k1 ∩ interior k2 = ∅)) ∧
    (BIGUNION s = i)

division_points

⊢ ∀k d.
    division_points k d =
    {(j,x) |
     1 ≤ j ∧ j ≤ 1 ∧ interval_lowerbound k < x ∧ x < interval_upperbound k ∧
     ∃i. i ∈ d ∧ ((interval_lowerbound i = x) ∨ (interval_upperbound i = x))}

equiintegrable_on

⊢ ∀fs i.
    fs equiintegrable_on i ⇔
    (∀f. f ∈ fs ⇒ f integrable_on i) ∧
    ∀e. 0 < e ⇒
        ∃d. gauge d ∧
            ∀f p.
              f ∈ fs ∧ p tagged_division_of i ∧ d FINE p ⇒
              abs (sum p (λ(x,k). content k * f x) − ∫ i f) < e

gauge_def

⊢ ∀d. gauge d ⇔ ∀x. x ∈ d x ∧ open (d x)

has_bounded_setvariation_on

⊢ ∀f s.
    f has_bounded_setvariation_on s ⇔
    ∃B. ∀d t. d division_of t ∧ t ⊆ s ⇒ sum d (λk. abs (f k)) ≤ B

has_bounded_variation_on

⊢ ∀f s.
    f has_bounded_variation_on s ⇔
    (λk. f (interval_upperbound k) − f (interval_lowerbound k)) has_bounded_setvariation_on
    s

has_integral_compact_interval

⊢ ∀f y i.
    (f has_integral_compact_interval y) i ⇔
    ∀e. 0 < e ⇒
        ∃d. gauge d ∧
            ∀p. p tagged_division_of i ∧ d FINE p ⇒
                abs (sum p (λ(x,k). content k * f x) − y) < e

has_integral_def

⊢ ∀f y i.
    (f has_integral y) i ⇔
    if ∃a b. i = interval [(a,b)] then (f has_integral_compact_interval y) i
    else
      ∀e. 0 < e ⇒
          ∃B. 0 < B ∧
              ∀a b.
                ball (0,B) ⊆ interval [(a,b)] ⇒
                ∃z. ((λx. if x ∈ i then f x else 0) has_integral_compact_interval
                     z) (interval [(a,b)]) ∧ abs (z − y) < e

indicator

⊢ ∀s. indicator s = (λx. if x ∈ s then 1 else 0)

integrable_on

⊢ ∀f i. f integrable_on i ⇔ ∃y. (f has_integral y) i

integral

⊢ ∀i f. ∫ i f = @y. (f has_integral y) i

interval_lowerbound

⊢ ∀s. interval_lowerbound s = if s = ∅ then 0 else inf s

interval_upperbound

⊢ ∀s. interval_upperbound s = if s = ∅ then 0 else sup s

negligible

⊢ ∀s. negligible s ⇔ ∀a b. (indicator s has_integral 0) (interval [(a,b)])

operative

⊢ ∀op f.
    operative op f ⇔
    (∀a b.
       (content (interval [(a,b)]) = 0) ⇒ (f (interval [(a,b)]) = neutral op)) ∧
    ∀a b c.
      f (interval [(a,b)]) =
      op (f (interval [(a,b)] ∩ {x | x ≤ c}))
        (f (interval [(a,b)] ∩ {x | x ≥ c}))

set_variation

⊢ ∀s f.
    set_variation s f =
    sup {sum d (λk. abs (f k)) | (∃t. d division_of t ∧ t ⊆ s)}

tagged_division_of

⊢ ∀s i.
    s tagged_division_of i ⇔
    s tagged_partial_division_of i ∧ (BIGUNION {k | (∃x. (x,k) ∈ s)} = i)

tagged_partial_division_of

⊢ ∀s i.
    s tagged_partial_division_of i ⇔
    FINITE s ∧
    (∀x k. (x,k) ∈ s ⇒ x ∈ k ∧ k ⊆ i ∧ ∃a b. k = interval [(a,b)]) ∧
    ∀x1 k1 x2 k2.
      (x1,k1) ∈ s ∧ (x2,k2) ∈ s ∧ (x1,k1) ≠ (x2,k2) ⇒
      (interior k1 ∩ interior k2 = ∅)

vector_variation

⊢ ∀s f.
    vector_variation s f =
    set_variation s
      (λk. f (interval_upperbound k) − f (interval_lowerbound k))

Theorems

ABSOLUTELY_INTEGRABLE_0

⊢ ∀s. (λx. 0) absolutely_integrable_on s

ABSOLUTELY_INTEGRABLE_ABS

⊢ ∀f s.
    f absolutely_integrable_on s ⇒ (λx. abs (f x)) absolutely_integrable_on s

ABSOLUTELY_INTEGRABLE_ABSOLUTELY_INTEGRABLE_BOUND

⊢ ∀f g s.
    (∀x. x ∈ s ⇒ abs (f x) ≤ abs (g x)) ∧ f integrable_on s ∧
    g absolutely_integrable_on s ⇒
    f absolutely_integrable_on s

ABSOLUTELY_INTEGRABLE_ABSOLUTELY_INTEGRABLE_COMPONENT_LBOUND

⊢ ∀f g s.
    (∀x i. x ∈ s ⇒ f x ≤ g x) ∧ f absolutely_integrable_on s ∧
    g integrable_on s ⇒
    g absolutely_integrable_on s

ABSOLUTELY_INTEGRABLE_ABSOLUTELY_INTEGRABLE_COMPONENT_UBOUND

⊢ ∀f g s.
    (∀x i. x ∈ s ⇒ f x ≤ g x) ∧ f integrable_on s ∧
    g absolutely_integrable_on s ⇒
    f absolutely_integrable_on s

ABSOLUTELY_INTEGRABLE_ABSOLUTELY_INTEGRABLE_LBOUND

⊢ ∀f g s.
    (∀x. x ∈ s ⇒ f x ≤ g x) ∧ f absolutely_integrable_on s ∧ g integrable_on s ⇒
    g absolutely_integrable_on s

ABSOLUTELY_INTEGRABLE_ABSOLUTELY_INTEGRABLE_UBOUND

⊢ ∀f g s.
    (∀x. x ∈ s ⇒ f x ≤ g x) ∧ f integrable_on s ∧ g absolutely_integrable_on s ⇒
    f absolutely_integrable_on s

ABSOLUTELY_INTEGRABLE_ABS_EQ

⊢ ∀f s.
    f absolutely_integrable_on s ⇔
    f integrable_on s ∧ (λx. abs (f x)) integrable_on s

ABSOLUTELY_INTEGRABLE_ADD

⊢ ∀f g s.
    f absolutely_integrable_on s ∧ g absolutely_integrable_on s ⇒
    (λx. f x + g x) absolutely_integrable_on s

ABSOLUTELY_INTEGRABLE_BOUNDED_SETVARIATION

⊢ ∀f s.
    f absolutely_integrable_on s ⇒ (λk. ∫ k f) has_bounded_setvariation_on s

ABSOLUTELY_INTEGRABLE_BOUNDED_SETVARIATION_EQ

⊢ ∀f a b.
    f absolutely_integrable_on interval [(a,b)] ⇔
    f integrable_on interval [(a,b)] ∧
    (λk. ∫ k f) has_bounded_setvariation_on interval [(a,b)]

ABSOLUTELY_INTEGRABLE_BOUNDED_SETVARIATION_UNIV_EQ

⊢ ∀f. f absolutely_integrable_on 𝕌(:real) ⇔
      f integrable_on 𝕌(:real) ∧
      (λk. ∫ k f) has_bounded_setvariation_on 𝕌(:real)

ABSOLUTELY_INTEGRABLE_CMUL

⊢ ∀f s c.
    f absolutely_integrable_on s ⇒ (λx. c * f x) absolutely_integrable_on s

ABSOLUTELY_INTEGRABLE_COMPONENTWISE

⊢ ∀f s. f absolutely_integrable_on s ⇔ (λx. f x) absolutely_integrable_on s

ABSOLUTELY_INTEGRABLE_CONST

⊢ ∀a b c. (λx. c) absolutely_integrable_on interval [(a,b)]

ABSOLUTELY_INTEGRABLE_CONTINUOUS

⊢ ∀f a b.
    f continuous_on interval [(a,b)] ⇒
    f absolutely_integrable_on interval [(a,b)]

ABSOLUTELY_INTEGRABLE_EQ

⊢ ∀f g s.
    (∀x. x ∈ s ⇒ (f x = g x)) ∧ f absolutely_integrable_on s ⇒
    g absolutely_integrable_on s

ABSOLUTELY_INTEGRABLE_IMP_ABS_INTEGRABLE

⊢ ∀f s. f absolutely_integrable_on s ⇒ (λx. abs (f x)) integrable_on s

ABSOLUTELY_INTEGRABLE_IMP_INTEGRABLE

⊢ ∀f s. f absolutely_integrable_on s ⇒ f integrable_on s

ABSOLUTELY_INTEGRABLE_INF

⊢ ∀fs s k.
    FINITE k ∧ k ≠ ∅ ∧ (∀i. i ∈ k ⇒ (λx. fs x i) absolutely_integrable_on s) ⇒
    (λx. inf (IMAGE (fs x) k)) absolutely_integrable_on s

ABSOLUTELY_INTEGRABLE_INTEGRABLE_BOUND

⊢ ∀f g s.
    (∀x. x ∈ s ⇒ abs (f x) ≤ g x) ∧ f integrable_on s ∧ g integrable_on s ⇒
    f absolutely_integrable_on s

ABSOLUTELY_INTEGRABLE_LE

⊢ ∀f s. f absolutely_integrable_on s ⇒ abs (∫ s f) ≤ ∫ s (λx. abs (f x))

ABSOLUTELY_INTEGRABLE_LINEAR

⊢ ∀f h s.
    f absolutely_integrable_on s ∧ linear h ⇒ h ∘ f absolutely_integrable_on s

ABSOLUTELY_INTEGRABLE_MAX

⊢ ∀f g s.
    f absolutely_integrable_on s ∧ g absolutely_integrable_on s ⇒
    (λx. max (f x) (g x)) absolutely_integrable_on s

ABSOLUTELY_INTEGRABLE_MIN

⊢ ∀f g s.
    f absolutely_integrable_on s ∧ g absolutely_integrable_on s ⇒
    (λx. min (f x) (g x)) absolutely_integrable_on s

ABSOLUTELY_INTEGRABLE_NEG

⊢ ∀f s. f absolutely_integrable_on s ⇒ (λx. -f x) absolutely_integrable_on s

ABSOLUTELY_INTEGRABLE_ON_NULL

⊢ ∀f a b.
    (content (interval [(a,b)]) = 0) ⇒
    f absolutely_integrable_on interval [(a,b)]

ABSOLUTELY_INTEGRABLE_ON_SUBINTERVAL

⊢ ∀f s a b.
    f absolutely_integrable_on s ∧ interval [(a,b)] ⊆ s ⇒
    f absolutely_integrable_on interval [(a,b)]

ABSOLUTELY_INTEGRABLE_RESTRICT_INTER

⊢ ∀f s t.
    (λx. if x ∈ s then f x else 0) absolutely_integrable_on t ⇔
    f absolutely_integrable_on s ∩ t

ABSOLUTELY_INTEGRABLE_RESTRICT_UNIV

⊢ ∀f s.
    (λx. if x ∈ s then f x else 0) absolutely_integrable_on 𝕌(:real) ⇔
    f absolutely_integrable_on s

ABSOLUTELY_INTEGRABLE_SET_VARIATION

⊢ ∀f a b.
    f absolutely_integrable_on interval [(a,b)] ⇒
    (set_variation (interval [(a,b)]) (λk. ∫ k f) =
     ∫ (interval [(a,b)]) (λx. abs (f x)))

ABSOLUTELY_INTEGRABLE_SPIKE

⊢ ∀f g s t.
    negligible s ∧ (∀x. x ∈ t DIFF s ⇒ (g x = f x)) ⇒
    f absolutely_integrable_on t ⇒
    g absolutely_integrable_on t

ABSOLUTELY_INTEGRABLE_SUB

⊢ ∀f g s.
    f absolutely_integrable_on s ∧ g absolutely_integrable_on s ⇒
    (λx. f x − g x) absolutely_integrable_on s

ABSOLUTELY_INTEGRABLE_SUM

⊢ ∀f s t.
    FINITE t ∧ (∀a. a ∈ t ⇒ f a absolutely_integrable_on s) ⇒
    (λx. sum t (λa. f a x)) absolutely_integrable_on s

ABSOLUTELY_INTEGRABLE_SUP

⊢ ∀fs s k.
    FINITE k ∧ k ≠ ∅ ∧ (∀i. i ∈ k ⇒ (λx. fs x i) absolutely_integrable_on s) ⇒
    (λx. sup (IMAGE (fs x) k)) absolutely_integrable_on s

ABS_LE_L1

⊢ ∀x. abs x ≤ sum (1 .. 1) (λi. abs x)

ABS_TRIANGLE_LE

⊢ ∀x y. abs x + abs y ≤ e ⇒ abs (x + y) ≤ e

ADDITIVE_CONTENT_DIVISION

⊢ ∀d a b.
    d division_of interval [(a,b)] ⇒
    (sum d content = content (interval [(a,b)]))

ADDITIVE_CONTENT_TAGGED_DIVISION

⊢ ∀d a b.
    d tagged_division_of interval [(a,b)] ⇒
    (sum d (λ(x,l). content l) = content (interval [(a,b)]))

ADDITIVE_TAGGED_DIVISION_1

⊢ ∀f p a b.
    a ≤ b ∧ p tagged_division_of interval [(a,b)] ⇒
    (sum p (λ(x,k). f (interval_upperbound k) − f (interval_lowerbound k)) =
     f b − f a)

ANTIDERIVATIVE_CONTINUOUS

⊢ ∀f a b.
    f continuous_on interval [(a,b)] ⇒
    ∃g. ∀x.
      x ∈ interval [(a,b)] ⇒
      (g has_vector_derivative f x) (at x within interval [(a,b)])

ANTIDERIVATIVE_INTEGRAL_CONTINUOUS

⊢ ∀f a b.
    f continuous_on interval [(a,b)] ⇒
    ∃g. ∀u v.
      u ∈ interval [(a,b)] ∧ v ∈ interval [(a,b)] ∧ u ≤ v ⇒
      (f has_integral g v − g u) (interval [(u,v)])

APPROXIMABLE_ON_DIVISION

⊢ ∀f d a b e.
    0 ≤ e ∧ d division_of interval [(a,b)] ∧
    (∀i. i ∈ d ⇒ ∃g. (∀x. x ∈ i ⇒ abs (f x − g x) ≤ e) ∧ g integrable_on i) ⇒
    ∃g. (∀x. x ∈ interval [(a,b)] ⇒ abs (f x − g x) ≤ e) ∧
        g integrable_on interval [(a,b)]

BEPPO_LEVI_DECREASING

⊢ ∀f s.
    (∀k. f k integrable_on s) ∧ (∀k x. x ∈ s ⇒ f (SUC k) x ≤ f k x) ∧
    bounded {∫ s (f k) | k ∈ 𝕌(:num)} ⇒
    ∃g k. negligible k ∧ ∀x. x ∈ s DIFF k ⇒ ((λk. f k x) ⟶ g x) sequentially

BEPPO_LEVI_INCREASING

⊢ ∀f s.
    (∀k. f k integrable_on s) ∧ (∀k x. x ∈ s ⇒ f k x ≤ f (SUC k) x) ∧
    bounded {∫ s (f k) | k ∈ 𝕌(:num)} ⇒
    ∃g k. negligible k ∧ ∀x. x ∈ s DIFF k ⇒ ((λk. f k x) ⟶ g x) sequentially

BEPPO_LEVI_MONOTONE_CONVERGENCE_DECREASING

⊢ ∀f s.
    (∀k. f k integrable_on s) ∧ (∀k x. x ∈ s ⇒ f (SUC k) x ≤ f k x) ∧
    bounded {∫ s (f k) | k ∈ 𝕌(:num)} ⇒
    ∃g k.
      negligible k ∧ (∀x. x ∈ s DIFF k ⇒ ((λk. f k x) ⟶ g x) sequentially) ∧
      g integrable_on s ∧ ((λk. ∫ s (f k)) ⟶ ∫ s g) sequentially

BEPPO_LEVI_MONOTONE_CONVERGENCE_DECREASING_AE

⊢ ∀f s.
    (∀k. f k integrable_on s) ∧
    (∀k. ∃t. negligible t ∧ ∀x. x ∈ s DIFF t ⇒ f (SUC k) x ≤ f k x) ∧
    bounded {∫ s (f k) | k ∈ 𝕌(:num)} ⇒
    ∃g k.
      negligible k ∧ (∀x. x ∈ s DIFF k ⇒ ((λk. f k x) ⟶ g x) sequentially) ∧
      g integrable_on s ∧ ((λk. ∫ s (f k)) ⟶ ∫ s g) sequentially

BEPPO_LEVI_MONOTONE_CONVERGENCE_INCREASING

⊢ ∀f s.
    (∀k. f k integrable_on s) ∧ (∀k x. x ∈ s ⇒ f k x ≤ f (SUC k) x) ∧
    bounded {∫ s (f k) | k ∈ 𝕌(:num)} ⇒
    ∃g k.
      negligible k ∧ (∀x. x ∈ s DIFF k ⇒ ((λk. f k x) ⟶ g x) sequentially) ∧
      g integrable_on s ∧ ((λk. ∫ s (f k)) ⟶ ∫ s g) sequentially

BEPPO_LEVI_MONOTONE_CONVERGENCE_INCREASING_AE

⊢ ∀f s.
    (∀k. f k integrable_on s) ∧
    (∀k. ∃t. negligible t ∧ ∀x. x ∈ s DIFF t ⇒ f k x ≤ f (SUC k) x) ∧
    bounded {∫ s (f k) | k ∈ 𝕌(:num)} ⇒
    ∃g k.
      negligible k ∧ (∀x. x ∈ s DIFF k ⇒ ((λk. f k x) ⟶ g x) sequentially) ∧
      g integrable_on s ∧ ((λk. ∫ s (f k)) ⟶ ∫ s g) sequentially

BOUNDED_EQUIINTEGRAL_OVER_THIN_TAGGED_PARTIAL_DIVISION

⊢ ∀fs f a b e.
    fs equiintegrable_on interval [(a,b)] ∧ f ∈ fs ∧
    (∀h x. h ∈ fs ∧ x ∈ interval [(a,b)] ⇒ abs (h x) ≤ abs (f x)) ∧ 0 < e ⇒
    ∃d. gauge d ∧
        ∀c p h.
          c ∈ interval [(a,b)] ∧
          p tagged_partial_division_of interval [(a,b)] ∧ d FINE p ∧ h ∈ fs ∧
          (∀x k. (x,k) ∈ p ⇒ k ∩ {x | x = c} ≠ ∅) ⇒
          sum p (λ(x,k). abs (∫ k h)) < e

BOUNDED_SETVARIATION_ABSOLUTELY_INTEGRABLE

⊢ ∀f. f integrable_on 𝕌(:real) ∧
      (λk. ∫ k f) has_bounded_setvariation_on 𝕌(:real) ⇒
      f absolutely_integrable_on 𝕌(:real)

BOUNDED_SETVARIATION_ABSOLUTELY_INTEGRABLE_INTERVAL

⊢ ∀f a b.
    f integrable_on interval [(a,b)] ∧
    (λk. ∫ k f) has_bounded_setvariation_on interval [(a,b)] ⇒
    f absolutely_integrable_on interval [(a,b)]

CONTENT_0_SUBSET

⊢ ∀s a b.
    s ⊆ interval [(a,b)] ∧ (content (interval [(a,b)]) = 0) ⇒ (content s = 0)

CONTENT_0_SUBSET_GEN

⊢ ∀s t. s ⊆ t ∧ bounded t ∧ (content t = 0) ⇒ (content s = 0)

CONTENT_CLOSED_INTERVAL

⊢ ∀a b. a ≤ b ⇒ (content (interval [(a,b)]) = b − a)

CONTENT_CLOSED_INTERVAL_CASES

⊢ ∀a b. content (interval [(a,b)]) = if a ≤ b then b − a else 0

CONTENT_DOUBLESPLIT

⊢ ∀a b c e.
    0 < e ⇒ ∃d. 0 < d ∧ content (interval [(a,b)] ∩ {x | abs (x − c) ≤ d}) < e

CONTENT_EMPTY

⊢ content ∅ = 0

CONTENT_EQ_0

⊢ ∀a b. (content (interval [(a,b)]) = 0) ⇔ b ≤ a

CONTENT_EQ_0_1

⊢ ∀a b. (content (interval [(a,b)]) = 0) ⇔ b ≤ a

CONTENT_EQ_0_GEN

⊢ ∀s. bounded s ⇒ ((content s = 0) ⇔ ∃a. ∀x. x ∈ s ⇒ (x = a))

CONTENT_EQ_0_INTERIOR

⊢ ∀a b. (content (interval [(a,b)]) = 0) ⇔ (interior (interval [(a,b)]) = ∅)

CONTENT_IMAGE_AFFINITY_INTERVAL

⊢ ∀a b m c.
    content (IMAGE (λx. m * x + c) (interval [(a,b)])) =
    abs m pow 1 * content (interval [(a,b)])

CONTENT_IMAGE_STRETCH_INTERVAL

⊢ ∀a b m.
    content (IMAGE (λx. m 1 * x) (interval [(a,b)])) =
    abs (product (1 .. 1) m) * content (interval [(a,b)])

CONTENT_LT_NZ

⊢ ∀a b. 0 < content (interval [(a,b)]) ⇔ content (interval [(a,b)]) ≠ 0

CONTENT_POS_LE

⊢ ∀a b. 0 ≤ content (interval [(a,b)])

CONTENT_POS_LT

⊢ ∀a b. a < b ⇒ 0 < content (interval [(a,b)])

CONTENT_POS_LT_EQ

⊢ ∀a b. 0 < content (interval [(a,b)]) ⇔ a < b

CONTENT_SPLIT

⊢ ∀a b k.
    content (interval [(a,b)]) =
    content (interval [(a,b)] ∩ {x | x ≤ c}) +
    content (interval [(a,b)] ∩ {x | x ≥ c})

CONTENT_SUBSET

⊢ ∀a b c d.
    interval [(a,b)] ⊆ interval [(c,d)] ⇒
    content (interval [(a,b)]) ≤ content (interval [(c,d)])

CONTENT_UNIT

⊢ content (interval [(0,1)]) = 1

CONTINUOUS_ON_VECTOR_VARIATION

⊢ ∀f a b.
    f has_bounded_variation_on interval [(a,b)] ∧
    f continuous_on interval [(a,b)] ⇒
    (λx. vector_variation (interval [(a,x)]) f) continuous_on interval [(a,b)]

CONVEX_CONTAINS_SEGMENT

⊢ ∀s. convex s ⇔ ∀a b. a ∈ s ∧ b ∈ s ⇒ segment [(a,b)] ⊆ s

DECREASING_BOUNDED_VARIATION

⊢ ∀f a b.
    (∀x y. x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒ f y ≤ f x) ⇒
    f has_bounded_variation_on interval [(a,b)]

DECREASING_BOUNDED_VARIATION_GEN

⊢ ∀f s.
    bounded (IMAGE f s) ∧ (∀x y. x ∈ s ∧ y ∈ s ∧ x ≤ y ⇒ f y ≤ f x) ⇒
    f has_bounded_variation_on s

DECREASING_LEFT_LIMIT

⊢ ∀f a b c.
    (∀x y. x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒ f y ≤ f x) ∧
    c ∈ interval [(a,b)] ⇒
    ∃l. (f ⟶ l) (at c within interval [(a,c)])

DECREASING_RIGHT_LIMIT

⊢ ∀f a b c.
    (∀x y. x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒ f y ≤ f x) ∧
    c ∈ interval [(a,b)] ⇒
    ∃l. (f ⟶ l) (at c within interval [(c,b)])

DECREASING_VECTOR_VARIATION

⊢ ∀f a b.
    interval [(a,b)] ≠ ∅ ∧
    (∀x y. x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒ f y ≤ f x) ⇒
    (vector_variation (interval [(a,b)]) f = f a − f b)

DIVISION_1_SORT

⊢ ∀d s.
    d division_of s ∧ (∀k. k ∈ d ⇒ interior k ≠ ∅) ⇒
    ∃n t.
      (IMAGE t (1 .. n) = d) ∧
      ∀i j.
        i ∈ (1 .. n) ∧ j ∈ (1 .. n) ∧ i < j ⇒
        t i ≠ t j ∧ ∀x y. x ∈ t i ∧ y ∈ t j ⇒ x ≤ y

DIVISION_COMMON_POINT_BOUND

⊢ ∀d s x. d division_of s ⇒ CARD {k | k ∈ d ∧ content k ≠ 0 ∧ x ∈ k} ≤ 2 ** 1

DIVISION_CONTAINS

⊢ ∀s i. s division_of i ⇒ ∀x. x ∈ i ⇒ ∃k. x ∈ k ∧ k ∈ s

DIVISION_DISJOINT_UNION

⊢ ∀s1 s2 p1 p2.
    p1 division_of s1 ∧ p2 division_of s2 ∧ (interior s1 ∩ interior s2 = ∅) ⇒
    p1 ∪ p2 division_of s1 ∪ s2

DIVISION_DOUBLESPLIT

⊢ ∀p a b c e.
    p division_of interval [(a,b)] ⇒
    {l ∩ {x | abs (x − c) ≤ e} | l | l ∈ p ∧ l ∩ {x | abs (x − c) ≤ e} ≠ ∅} division_of
    interval [(a,b)] ∩ {x | abs (x − c) ≤ e}

DIVISION_INTER

⊢ ∀s1 s2 p1 p2.
    p1 division_of s1 ∧ p2 division_of s2 ⇒
    {k1 ∩ k2 | k1 ∈ p1 ∧ k2 ∈ p2 ∧ k1 ∩ k2 ≠ ∅} division_of s1 ∩ s2

DIVISION_INTER_1

⊢ ∀d i a b.
    d division_of i ∧ interval [(a,b)] ⊆ i ⇒
    {interval [(a,b)] ∩ k | k | k ∈ d ∧ interval [(a,b)] ∩ k ≠ ∅} division_of
    interval [(a,b)]

DIVISION_OF

⊢ ∀s i.
    s division_of i ⇔
    FINITE s ∧ (∀k. k ∈ s ⇒ k ≠ ∅ ∧ ∃a b. k = interval [(a,b)]) ∧
    (∀k1 k2. k1 ∈ s ∧ k2 ∈ s ∧ k1 ≠ k2 ⇒ (interior k1 ∩ interior k2 = ∅)) ∧
    (BIGUNION s = i)

DIVISION_OF_AFFINITY

⊢ ∀d s m c.
    IMAGE (IMAGE (λx. m * x + c)) d division_of IMAGE (λx. m * x + c) s ⇔
    if m = 0 then if s = ∅ then d = ∅ else d ≠ ∅ ∧ ∀k. k ∈ d ⇒ k ≠ ∅
    else d division_of s

DIVISION_OF_BIGUNION

⊢ ∀f. FINITE f ∧ (∀p. p ∈ f ⇒ p division_of BIGUNION p) ∧
      (∀k1 k2.
         k1 ∈ BIGUNION f ∧ k2 ∈ BIGUNION f ∧ k1 ≠ k2 ⇒
         (interior k1 ∩ interior k2 = ∅)) ⇒
      BIGUNION f division_of BIGUNION (BIGUNION f)

DIVISION_OF_CLOSED

⊢ ∀s i. s division_of i ⇒ closed i

DIVISION_OF_CONTENT_0

⊢ ∀a b d.
    (content (interval [(a,b)]) = 0) ∧ d division_of interval [(a,b)] ⇒
    ∀k. k ∈ d ⇒ (content k = 0)

DIVISION_OF_FINITE

⊢ ∀s i. s division_of i ⇒ FINITE s

DIVISION_OF_NONTRIVIAL

⊢ ∀s a b.
    s division_of interval [(a,b)] ∧ content (interval [(a,b)]) ≠ 0 ⇒
    {k | k ∈ s ∧ content k ≠ 0} division_of interval [(a,b)]

DIVISION_OF_REFLECT

⊢ ∀d s.
    IMAGE (IMAGE (λx. -x)) d division_of IMAGE (λx. -x) s ⇔ d division_of s

DIVISION_OF_SELF

⊢ ∀a b. interval [(a,b)] ≠ ∅ ⇒ {interval [(a,b)]} division_of interval [(a,b)]

DIVISION_OF_SING

⊢ ∀s a. s division_of interval [(a,a)] ⇔ (s = {interval [(a,a)]})

DIVISION_OF_SUBSET

⊢ ∀p q. p division_of BIGUNION p ∧ q ⊆ p ⇒ q division_of BIGUNION q

DIVISION_OF_TAGGED_DIVISION

⊢ ∀s i. s tagged_division_of i ⇒ IMAGE SND s division_of i

DIVISION_OF_TRANSLATION

⊢ ∀d s.
    IMAGE (IMAGE (λx. a + x)) d division_of IMAGE (λx. a + x) s ⇔
    d division_of s

DIVISION_OF_TRIVIAL

⊢ ∀s. s division_of ∅ ⇔ (s = ∅)

DIVISION_OF_UNION_SELF

⊢ ∀p s. p division_of s ⇒ p division_of BIGUNION p

DIVISION_POINTS_FINITE

⊢ ∀d i. d division_of i ⇒ FINITE (division_points i d)

DIVISION_POINTS_PSUBSET

⊢ ∀a b c d.
    d division_of interval [(a,b)] ∧ a < b ∧ a < c ∧ c < b ∧
    (∃l. l ∈ d ∧ ((interval_lowerbound l = c) ∨ (interval_upperbound l = c))) ⇒
    division_points (interval [(a,b)] ∩ {x | x ≤ c})
      {l ∩ {x | x ≤ c} | l | l ∈ d ∧ l ∩ {x | x ≤ c} ≠ ∅} ⊂
    division_points (interval [(a,b)]) d ∧
    division_points (interval [(a,b)] ∩ {x | x ≥ c})
      {l ∩ {x | x ≥ c} | l | l ∈ d ∧ l ∩ {x | x ≥ c} ≠ ∅} ⊂
    division_points (interval [(a,b)]) d

DIVISION_POINTS_SUBSET

⊢ ∀a b c d k.
    d division_of interval [(a,b)] ∧ a < b ∧ a < c ∧ c < b ⇒
    division_points (interval [(a,b)] ∩ {x | x ≤ c})
      {l ∩ {x | x ≤ c} | l | l ∈ d ∧ l ∩ {x | x ≤ c} ≠ ∅} ⊆
    division_points (interval [(a,b)]) d ∧
    division_points (interval [(a,b)] ∩ {x | x ≥ c})
      {l ∩ {x | x ≥ c} | l | l ∈ d ∧ l ∩ {x | x ≥ c} ≠ ∅} ⊆
    division_points (interval [(a,b)]) d

DIVISION_SPLIT

⊢ ∀p a b c.
    p division_of interval [(a,b)] ⇒
    {l ∩ {x | x ≤ c} | l | l ∈ p ∧ l ∩ {x | x ≤ c} ≠ ∅} division_of
    interval [(a,b)] ∩ {x | x ≤ c} ∧
    {l ∩ {x | x ≥ c} | l | l ∈ p ∧ l ∩ {x | x ≥ c} ≠ ∅} division_of
    interval [(a,b)] ∩ {x | x ≥ c}

DIVISION_SPLIT_LEFT_INJ

⊢ ∀d i k1 k2 k c.
    d division_of i ∧ k1 ∈ d ∧ k2 ∈ d ∧ k1 ≠ k2 ∧
    (k1 ∩ {x | x ≤ c} = k2 ∩ {x | x ≤ c}) ⇒
    (content (k1 ∩ {x | x ≤ c}) = 0)

DIVISION_SPLIT_LEFT_RIGHT_INJ

⊢ (∀d i k1 k2 k c.
     d division_of i ∧ k1 ∈ d ∧ k2 ∈ d ∧ k1 ≠ k2 ∧
     (k1 ∩ {x | x ≤ c} = k2 ∩ {x | x ≤ c}) ⇒
     (content (k1 ∩ {x | x ≤ c}) = 0)) ∧
  ∀d i k1 k2 k c.
    d division_of i ∧ k1 ∈ d ∧ k2 ∈ d ∧ k1 ≠ k2 ∧
    (k1 ∩ {x | x ≥ c} = k2 ∩ {x | x ≥ c}) ⇒
    (content (k1 ∩ {x | x ≥ c}) = 0)

DIVISION_SPLIT_RIGHT_INJ

⊢ ∀d i k1 k2 k c.
    d division_of i ∧ k1 ∈ d ∧ k2 ∈ d ∧ k1 ≠ k2 ∧
    (k1 ∩ {x | x ≥ c} = k2 ∩ {x | x ≥ c}) ⇒
    (content (k1 ∩ {x | x ≥ c}) = 0)

DIVISION_UNION_INTERVALS_EXISTS

⊢ ∀a b c d.
    interval [(a,b)] ≠ ∅ ⇒
    ∃p. interval [(a,b)] INSERT p division_of
        interval [(a,b)] ∪ interval [(c,d)]

DOMINATED_CONVERGENCE

⊢ ∀f g h s.
    (∀k. f k integrable_on s) ∧ h integrable_on s ∧
    (∀k x. x ∈ s ⇒ abs (f k x) ≤ h x) ∧
    (∀x. x ∈ s ⇒ ((λk. f k x) ⟶ g x) sequentially) ⇒
    g integrable_on s ∧ ((λk. ∫ s (f k)) ⟶ ∫ s g) sequentially

DOMINATED_CONVERGENCE_ABSOLUTELY_INTEGRABLE

⊢ ∀f g h s.
    (∀k. f k absolutely_integrable_on s) ∧ h integrable_on s ∧
    (∀k x. x ∈ s ⇒ abs (g x) ≤ h x) ∧
    (∀x. x ∈ s ⇒ ((λk. f k x) ⟶ g x) sequentially) ⇒
    g absolutely_integrable_on s

DOMINATED_CONVERGENCE_AE

⊢ ∀f g h s t.
    (∀k. f k integrable_on s) ∧ h integrable_on s ∧ negligible t ∧
    (∀k x. x ∈ s DIFF t ⇒ abs (f k x) ≤ h x) ∧
    (∀x. x ∈ s DIFF t ⇒ ((λk. f k x) ⟶ g x) sequentially) ⇒
    g integrable_on s ∧ ((λk. ∫ s (f k)) ⟶ ∫ s g) sequentially

DOMINATED_CONVERGENCE_INTEGRABLE

⊢ ∀f g h s.
    (∀k. f k absolutely_integrable_on s) ∧ h integrable_on s ∧
    (∀k x. x ∈ s ⇒ abs (g x) ≤ h x) ∧
    (∀x. x ∈ s ⇒ ((λk. f k x) ⟶ g x) sequentially) ⇒
    g integrable_on s

DROP_INDICATOR

⊢ ∀s x. indicator s x = if x ∈ s then 1 else 0

DROP_INDICATOR_ABS_LE_1

⊢ ∀s x. abs (indicator s x) ≤ 1

DROP_INDICATOR_LE_1

⊢ ∀s x. indicator s x ≤ 1

DROP_INDICATOR_POS_LE

⊢ ∀s x. 0 ≤ indicator s x

DSUM_BOUND

⊢ ∀p a b c e.
    p division_of interval [(a,b)] ∧ abs c ≤ e ⇒
    abs (sum p (λl. content l * c)) ≤ e * content (interval [(a,b)])

ELEMENTARY_BIGINTER

⊢ ∀f. FINITE f ∧ f ≠ ∅ ∧ (∀s. s ∈ f ⇒ ∃p. p division_of s) ⇒
      ∃p. p division_of BIGINTER f

ELEMENTARY_BIGUNION_INTERVALS

⊢ ∀f. FINITE f ∧ (∀s. s ∈ f ⇒ ∃a b. s = interval [(a,b)]) ⇒
      ∃p. p division_of BIGUNION f

ELEMENTARY_BOUNDED

⊢ ∀s. (∃p. p division_of s) ⇒ bounded s

ELEMENTARY_COMPACT

⊢ ∀s. (∃d. d division_of s) ⇒ compact s

ELEMENTARY_EMPTY

⊢ ∃p. p division_of ∅

ELEMENTARY_INTER

⊢ ∀s t.
    (∃p. p division_of s) ∧ (∃p. p division_of t) ⇒ ∃p. p division_of s ∩ t

ELEMENTARY_INTERVAL

⊢ ∀a b. ∃p. p division_of interval [(a,b)]

ELEMENTARY_SUBSET_INTERVAL

⊢ ∀s. (∃p. p division_of s) ⇒ ∃a b. s ⊆ interval [(a,b)]

ELEMENTARY_UNION

⊢ ∀s t.
    (∃p. p division_of s) ∧ (∃p. p division_of t) ⇒ ∃p. p division_of s ∪ t

ELEMENTARY_UNION_INTERVAL

⊢ ∀p a b.
    p division_of BIGUNION p ⇒ ∃q. q division_of interval [(a,b)] ∪ BIGUNION p

ELEMENTARY_UNION_INTERVAL_STRONG

⊢ ∀p a b.
    p division_of BIGUNION p ⇒
    ∃q. p ⊆ q ∧ q division_of interval [(a,b)] ∪ BIGUNION p

EMPTY_DIVISION_OF

⊢ ∀s. ∅ division_of s ⇔ (s = ∅)

EQUIINTEGRABLE_ADD

⊢ ∀fs gs s.
    fs equiintegrable_on s ∧ gs equiintegrable_on s ⇒
    {(λx. f x + g x) | f ∈ fs ∧ g ∈ gs} equiintegrable_on s

EQUIINTEGRABLE_CLOSED_INTERVAL_RESTRICTIONS

⊢ ∀f a b.
    f integrable_on interval [(a,b)] ⇒
    {(λx. if x ∈ interval [(c,d)] then f x else 0) |
     c ∈ 𝕌(:real) ∧ d ∈ 𝕌(:real)} equiintegrable_on interval [(a,b)]

EQUIINTEGRABLE_CMUL

⊢ ∀fs s k.
    fs equiintegrable_on s ⇒
    {(λx. c * f x) | abs c ≤ k ∧ f ∈ fs} equiintegrable_on s

EQUIINTEGRABLE_DIVISION

⊢ ∀fs d a b.
    d division_of interval [(a,b)] ⇒
    (fs equiintegrable_on interval [(a,b)] ⇔
     ∀i. i ∈ d ⇒ fs equiintegrable_on i)

EQUIINTEGRABLE_EQ

⊢ ∀fs gs s.
    fs equiintegrable_on s ∧
    (∀g. g ∈ gs ⇒ ∃f. f ∈ fs ∧ ∀x. x ∈ s ⇒ (f x = g x)) ⇒
    gs equiintegrable_on s

EQUIINTEGRABLE_HALFSPACE_RESTRICTIONS_GE

⊢ ∀fs f a b.
    fs equiintegrable_on interval [(a,b)] ∧ f ∈ fs ∧
    (∀h x. h ∈ fs ∧ x ∈ interval [(a,b)] ⇒ abs (h x) ≤ abs (f x)) ⇒
    {(λx. if x ≥ c then h x else 0) | c ∈ 𝕌(:real) ∧ h ∈ fs} equiintegrable_on
    interval [(a,b)]

EQUIINTEGRABLE_HALFSPACE_RESTRICTIONS_GT

⊢ ∀fs f a b.
    fs equiintegrable_on interval [(a,b)] ∧ f ∈ fs ∧
    (∀h x. h ∈ fs ∧ x ∈ interval [(a,b)] ⇒ abs (h x) ≤ abs (f x)) ⇒
    {(λx. if x > c then h x else 0) | c ∈ 𝕌(:real) ∧ h ∈ fs} equiintegrable_on
    interval [(a,b)]

EQUIINTEGRABLE_HALFSPACE_RESTRICTIONS_LE

⊢ ∀fs f a b.
    fs equiintegrable_on interval [(a,b)] ∧ f ∈ fs ∧
    (∀h x. h ∈ fs ∧ x ∈ interval [(a,b)] ⇒ abs (h x) ≤ abs (f x)) ⇒
    {(λx. if x ≤ c then h x else 0) | c ∈ 𝕌(:real) ∧ h ∈ fs} equiintegrable_on
    interval [(a,b)]

EQUIINTEGRABLE_HALFSPACE_RESTRICTIONS_LT

⊢ ∀fs f a b.
    fs equiintegrable_on interval [(a,b)] ∧ f ∈ fs ∧
    (∀h x. h ∈ fs ∧ x ∈ interval [(a,b)] ⇒ abs (h x) ≤ abs (f x)) ⇒
    {(λx. if x < c then h x else 0) | c ∈ 𝕌(:real) ∧ h ∈ fs} equiintegrable_on
    interval [(a,b)]

EQUIINTEGRABLE_LIMIT

⊢ ∀f g a b.
    {f n | n ∈ 𝕌(:num)} equiintegrable_on interval [(a,b)] ∧
    (∀x. x ∈ interval [(a,b)] ⇒ ((λn. f n x) ⟶ g x) sequentially) ⇒
    g integrable_on interval [(a,b)] ∧
    ((λn. ∫ (interval [(a,b)]) (f n)) ⟶ ∫ (interval [(a,b)]) g) sequentially

EQUIINTEGRABLE_NEG

⊢ ∀fs s. fs equiintegrable_on s ⇒ {(λx. -f x) | f ∈ fs} equiintegrable_on s

EQUIINTEGRABLE_ON_NULL

⊢ ∀fs a b.
    (content (interval [(a,b)]) = 0) ⇒ fs equiintegrable_on interval [(a,b)]

EQUIINTEGRABLE_ON_SING

⊢ ∀f a b.
    {f} equiintegrable_on interval [(a,b)] ⇔ f integrable_on interval [(a,b)]

EQUIINTEGRABLE_ON_SPLIT

⊢ ∀fs k a b c.
    fs equiintegrable_on interval [(a,b)] ∩ {x | x ≤ c} ∧
    fs equiintegrable_on interval [(a,b)] ∩ {x | x ≥ c} ⇒
    fs equiintegrable_on interval [(a,b)]

EQUIINTEGRABLE_OPEN_INTERVAL_RESTRICTIONS

⊢ ∀f a b.
    f integrable_on interval [(a,b)] ⇒
    {(λx. if x ∈ interval (c,d) then f x else 0) | c ∈ 𝕌(:real) ∧ d ∈ 𝕌(:real)} equiintegrable_on
    interval [(a,b)]

EQUIINTEGRABLE_REFLECT

⊢ ∀fs a b.
    fs equiintegrable_on interval [(a,b)] ⇒
    {(λx. f (-x)) | f ∈ fs} equiintegrable_on interval [(-b,-a)]

EQUIINTEGRABLE_SUB

⊢ ∀fs gs s.
    fs equiintegrable_on s ∧ gs equiintegrable_on s ⇒
    {(λx. f x − g x) | f ∈ fs ∧ g ∈ gs} equiintegrable_on s

EQUIINTEGRABLE_SUBSET

⊢ ∀fs gs s. fs equiintegrable_on s ∧ gs ⊆ fs ⇒ gs equiintegrable_on s

EQUIINTEGRABLE_SUM

⊢ ∀fs a b.
    fs equiintegrable_on interval [(a,b)] ⇒
    {(λx. sum t (λi. c i * f i x)) |
     FINITE t ∧ (∀i. i ∈ t ⇒ 0 ≤ c i ∧ f i ∈ fs) ∧ (sum t c = 1)} equiintegrable_on
    interval [(a,b)]

EQUIINTEGRABLE_UNIFORM_LIMIT

⊢ ∀fs a b.
    fs equiintegrable_on interval [(a,b)] ⇒
    {g |
     ∀e. 0 < e ⇒ ∃f. f ∈ fs ∧ ∀x. x ∈ interval [(a,b)] ⇒ abs (g x − f x) < e} equiintegrable_on
    interval [(a,b)]

EQUIINTEGRABLE_UNION

⊢ ∀fs gs s.
    fs equiintegrable_on s ∧ gs equiintegrable_on s ⇒
    fs ∪ gs equiintegrable_on s

FATOU

⊢ ∀f g s t B.
    negligible t ∧ (∀n. f n integrable_on s) ∧
    (∀n x. x ∈ s DIFF t ⇒ 0 ≤ f n x) ∧
    (∀x. x ∈ s DIFF t ⇒ ((λn. f n x) ⟶ g x) sequentially) ∧
    (∀n. ∫ s (f n) ≤ B) ⇒
    g integrable_on s ∧ 0 ≤ ∫ s g ∧ ∫ s g ≤ B

FINE_BIGINTER

⊢ ∀f s p. (λx. BIGINTER {f d x | d ∈ s}) FINE p ⇔ ∀d. d ∈ s ⇒ f d FINE p

FINE_BIGUNION

⊢ ∀d ps. (∀p. p ∈ ps ⇒ d FINE p) ⇒ d FINE BIGUNION ps

FINE_DIVISION_EXISTS

⊢ ∀g a b. gauge g ⇒ ∃p. p tagged_division_of interval [(a,b)] ∧ g FINE p

FINE_INTER

⊢ ∀p d1 d2. (λx. d1 x ∩ d2 x) FINE p ⇔ d1 FINE p ∧ d2 FINE p

FINE_SUBSET

⊢ ∀d p q. p ⊆ q ∧ d FINE q ⇒ d FINE p

FINE_UNION

⊢ ∀d p1 p2. d FINE p1 ∧ d FINE p2 ⇒ d FINE p1 ∪ p2

FINITE_POWERSET

⊢ ∀s. FINITE s ⇒ FINITE {t | t ⊆ s}

FLOOR_POS

⊢ ∀x. 0 ≤ x ⇒ ∃n. flr x = n

FORALL_IN_DIVISION

⊢ ∀P d i.
    d division_of i ⇒
    ((∀x. x ∈ d ⇒ P x) ⇔ ∀a b. interval [(a,b)] ∈ d ⇒ P (interval [(a,b)]))

FORALL_IN_DIVISION_NONEMPTY

⊢ ∀P d i.
    d division_of i ⇒
    ((∀x. x ∈ d ⇒ P x) ⇔
     ∀a b. interval [(a,b)] ∈ d ∧ interval [(a,b)] ≠ ∅ ⇒ P (interval [(a,b)]))

FUNDAMENTAL_THEOREM_OF_CALCULUS

⊢ ∀f f' a b.
    a ≤ b ∧
    (∀x. x ∈ interval [(a,b)] ⇒
         (f has_vector_derivative f' x) (at x within interval [(a,b)])) ⇒
    (f' has_integral f b − f a) (interval [(a,b)])

FUNDAMENTAL_THEOREM_OF_CALCULUS_INTERIOR

⊢ ∀f f' a b.
    a ≤ b ∧ f continuous_on interval [(a,b)] ∧
    (∀x. x ∈ interval (a,b) ⇒ (f has_vector_derivative f' x) (at x)) ⇒
    (f' has_integral f b − f a) (interval [(a,b)])

FUNDAMENTAL_THEOREM_OF_CALCULUS_INTERIOR_STRONG

⊢ ∀f f' s a b.
    COUNTABLE s ∧ a ≤ b ∧ f continuous_on interval [(a,b)] ∧
    (∀x. x ∈ interval (a,b) DIFF s ⇒ (f has_vector_derivative f' x) (at x)) ⇒
    (f' has_integral f b − f a) (interval [(a,b)])

FUNDAMENTAL_THEOREM_OF_CALCULUS_STRONG

⊢ ∀f f' s a b.
    COUNTABLE s ∧ a ≤ b ∧ f continuous_on interval [(a,b)] ∧
    (∀x. x ∈ interval [(a,b)] DIFF s ⇒
         (f has_vector_derivative f' x) (at x within interval [(a,b)])) ⇒
    (f' has_integral f b − f a) (interval [(a,b)])

GAUGE_BALL

⊢ ∀e. 0 < e ⇒ gauge (λx. ball (x,e))

GAUGE_BALL_DEPENDENT

⊢ ∀e. (∀x. 0 < e x) ⇒ gauge (λx. ball (x,e x))

GAUGE_BIGINTER

⊢ ∀f s.
    FINITE s ∧ (∀d. d ∈ s ⇒ gauge (f d)) ⇒
    gauge (λx. BIGINTER {f d x | d ∈ s})

GAUGE_EXISTENCE_LEMMA

⊢ ∀p q. (∀x. ∃d. p x ⇒ 0 < d ∧ q d x) ⇔ ∀x. ∃d. 0 < d ∧ (p x ⇒ q d x)

GAUGE_INTER

⊢ ∀d1 d2. gauge d1 ∧ gauge d2 ⇒ gauge (λx. d1 x ∩ d2 x)

GAUGE_MODIFY

⊢ ∀f. (∀s. open s ⇒ open {x | f x ∈ s}) ⇒
      ∀d. gauge d ⇒ gauge (λx y. d (f x) (f y))

GAUGE_TRIVIAL

⊢ gauge (λx. ball (x,1))

HAS_BOUNDED_SETVARIATION_COMPARISON

⊢ ∀f g s.
    f has_bounded_setvariation_on s ∧
    (∀a b.
       interval [(a,b)] ≠ ∅ ∧ interval [(a,b)] ⊆ s ⇒
       abs (g (interval [(a,b)])) ≤ abs (f (interval [(a,b)]))) ⇒
    g has_bounded_setvariation_on s

HAS_BOUNDED_SETVARIATION_ON

⊢ ∀f s.
    f has_bounded_setvariation_on s ⇔
    ∃B. 0 < B ∧ ∀d t. d division_of t ∧ t ⊆ s ⇒ sum d (λk. abs (f k)) ≤ B

HAS_BOUNDED_SETVARIATION_ON_0

⊢ ∀s. (λx. 0) has_bounded_setvariation_on s

HAS_BOUNDED_SETVARIATION_ON_ABS

⊢ ∀f s.
    (λx. abs (f x)) has_bounded_setvariation_on s ⇔
    f has_bounded_setvariation_on s

HAS_BOUNDED_SETVARIATION_ON_ADD

⊢ ∀f g s.
    f has_bounded_setvariation_on s ∧ g has_bounded_setvariation_on s ⇒
    (λx. f x + g x) has_bounded_setvariation_on s

HAS_BOUNDED_SETVARIATION_ON_CMUL

⊢ ∀f c s.
    f has_bounded_setvariation_on s ⇒
    (λx. c * f x) has_bounded_setvariation_on s

HAS_BOUNDED_SETVARIATION_ON_COMPONENTWISE

⊢ ∀f s.
    f has_bounded_setvariation_on s ⇔ (λk. f k) has_bounded_setvariation_on s

HAS_BOUNDED_SETVARIATION_ON_COMPOSE_LINEAR

⊢ ∀f g s.
    f has_bounded_setvariation_on s ∧ linear g ⇒
    g ∘ f has_bounded_setvariation_on s

HAS_BOUNDED_SETVARIATION_ON_DIVISION

⊢ ∀f a b d.
    operative $+ f ∧ d division_of interval [(a,b)] ⇒
    ((∀k. k ∈ d ⇒ f has_bounded_setvariation_on k) ⇔
     f has_bounded_setvariation_on interval [(a,b)])

HAS_BOUNDED_SETVARIATION_ON_ELEMENTARY

⊢ ∀f s.
    (∃d. d division_of s) ⇒
    (f has_bounded_setvariation_on s ⇔
     ∃B. ∀d. d division_of s ⇒ sum d (λk. abs (f k)) ≤ B)

HAS_BOUNDED_SETVARIATION_ON_EQ

⊢ ∀f g s.
    (∀a b.
       interval [(a,b)] ≠ ∅ ∧ interval [(a,b)] ⊆ s ⇒
       (f (interval [(a,b)]) = g (interval [(a,b)]))) ∧
    f has_bounded_setvariation_on s ⇒
    g has_bounded_setvariation_on s

HAS_BOUNDED_SETVARIATION_ON_IMP_BOUNDED_ON_SUBINTERVALS

⊢ ∀f s.
    f has_bounded_setvariation_on s ⇒
    bounded {f (interval [(c,d)]) | interval [(c,d)] ⊆ s}

HAS_BOUNDED_SETVARIATION_ON_INTERVAL

⊢ ∀f a b.
    f has_bounded_setvariation_on interval [(a,b)] ⇔
    ∃B. ∀d. d division_of interval [(a,b)] ⇒ sum d (λk. abs (f k)) ≤ B

HAS_BOUNDED_SETVARIATION_ON_NEG

⊢ ∀f s.
    (λx. -f x) has_bounded_setvariation_on s ⇔ f has_bounded_setvariation_on s

HAS_BOUNDED_SETVARIATION_ON_NULL

⊢ ∀f s.
    (∀a b. (content (interval [(a,b)]) = 0) ⇒ (f (interval [(a,b)]) = 0)) ∧
    (content s = 0) ∧ bounded s ⇒
    f has_bounded_setvariation_on s

HAS_BOUNDED_SETVARIATION_ON_SUB

⊢ ∀f g s.
    f has_bounded_setvariation_on s ∧ g has_bounded_setvariation_on s ⇒
    (λx. f x − g x) has_bounded_setvariation_on s

HAS_BOUNDED_SETVARIATION_ON_SUBSET

⊢ ∀f s t.
    f has_bounded_setvariation_on s ∧ t ⊆ s ⇒ f has_bounded_setvariation_on t

HAS_BOUNDED_SETVARIATION_ON_SUM

⊢ ∀f s k.
    FINITE k ∧ (∀i. i ∈ k ⇒ f i has_bounded_setvariation_on s) ⇒
    (λx. sum k (λi. f i x)) has_bounded_setvariation_on s

HAS_BOUNDED_SETVARIATION_ON_SUM_AND_SET_VARIATION_SUM_LE

⊢ (∀f s k.
     FINITE k ∧ (∀i. i ∈ k ⇒ f i has_bounded_setvariation_on s) ⇒
     (λx. sum k (λi. f i x)) has_bounded_setvariation_on s) ∧
  ∀f s k.
    FINITE k ∧ (∀i. i ∈ k ⇒ f i has_bounded_setvariation_on s) ⇒
    set_variation s (λx. sum k (λi. f i x)) ≤
    sum k (λi. set_variation s (f i))

HAS_BOUNDED_SETVARIATION_ON_UNIV

⊢ ∀f. f has_bounded_setvariation_on 𝕌(:real) ⇔
      ∃B. ∀d. d division_of BIGUNION d ⇒ sum d (λk. abs (f k)) ≤ B

HAS_BOUNDED_SETVARIATION_REFLECT2_EQ

⊢ ∀f s.
    (λk. f (IMAGE (λx. -x) k)) has_bounded_setvariation_on IMAGE (λx. -x) s ⇔
    f has_bounded_setvariation_on s

HAS_BOUNDED_SETVARIATION_REFLECT2_EQ_AND_SET_VARIATION_REFLECT2

⊢ (∀f s.
     (λk. f (IMAGE (λx. -x) k)) has_bounded_setvariation_on IMAGE (λx. -x) s ⇔
     f has_bounded_setvariation_on s) ∧
  ∀f s.
    set_variation (IMAGE (λx. -x) s) (λk. f (IMAGE (λx. -x) k)) =
    set_variation s f

HAS_BOUNDED_SETVARIATION_TRANSLATION

⊢ ∀f s a.
    f has_bounded_setvariation_on s ⇒
    (λk. f (IMAGE (λx. a + x) k)) has_bounded_setvariation_on
    IMAGE (λx. -a + x) s

HAS_BOUNDED_SETVARIATION_TRANSLATION2_EQ

⊢ ∀a f s.
    (λk. f (IMAGE (λx. a + x) k)) has_bounded_setvariation_on
    IMAGE (λx. -a + x) s ⇔ f has_bounded_setvariation_on s

HAS_BOUNDED_SETVARIATION_TRANSLATION2_EQ_AND_SET_VARIATION_TRANSLATION2

⊢ (∀a f s.
     (λk. f (IMAGE (λx. a + x) k)) has_bounded_setvariation_on
     IMAGE (λx. -a + x) s ⇔ f has_bounded_setvariation_on s) ∧
  ∀a f s.
    set_variation (IMAGE (λx. -a + x) s) (λk. f (IMAGE (λx. a + x) k)) =
    set_variation s f

HAS_BOUNDED_SETVARIATION_WORKS

⊢ ∀f s.
    f has_bounded_setvariation_on s ⇒
    (∀d t. d division_of t ∧ t ⊆ s ⇒ sum d (λk. abs (f k)) ≤ set_variation s f) ∧
    ∀B. (∀d t. d division_of t ∧ t ⊆ s ⇒ sum d (λk. abs (f k)) ≤ B) ⇒
        set_variation s f ≤ B

HAS_BOUNDED_SETVARIATION_WORKS_ON_ELEMENTARY

⊢ ∀f s.
    f has_bounded_setvariation_on s ∧ (∃d. d division_of s) ⇒
    (∀d. d division_of s ⇒ sum d (λk. abs (f k)) ≤ set_variation s f) ∧
    ∀B. (∀d. d division_of s ⇒ sum d (λk. abs (f k)) ≤ B) ⇒
        set_variation s f ≤ B

HAS_BOUNDED_SETVARIATION_WORKS_ON_INTERVAL

⊢ ∀f a b.
    f has_bounded_setvariation_on interval [(a,b)] ⇒
    (∀d. d division_of interval [(a,b)] ⇒
         sum d (λk. abs (f k)) ≤ set_variation (interval [(a,b)]) f) ∧
    ∀B. (∀d. d division_of interval [(a,b)] ⇒ sum d (λk. abs (f k)) ≤ B) ⇒
        set_variation (interval [(a,b)]) f ≤ B

HAS_BOUNDED_VARIATION_AFFINITY2_EQ

⊢ ∀m c f s.
    (λx. f (m * x + c)) has_bounded_variation_on
    IMAGE (λx. m⁻¹ * x + -(m⁻¹ * c)) s ⇔
    (m = 0) ∨ f has_bounded_variation_on s

HAS_BOUNDED_VARIATION_AFFINITY2_EQ_AND_VECTOR_VARIATION_AFFINITY2

⊢ (∀m c f s.
     (λx. f (m * x + c)) has_bounded_variation_on
     IMAGE (λx. m⁻¹ * x + -(m⁻¹ * c)) s ⇔
     (m = 0) ∨ f has_bounded_variation_on s) ∧
  ∀m c f s.
    vector_variation (IMAGE (λx. m⁻¹ * x + -(m⁻¹ * c)) s) (λx. f (m * x + c)) =
    if m = 0 then 0 else vector_variation s f

HAS_BOUNDED_VARIATION_AFFINITY_EQ

⊢ ∀m c f s.
    (λx. f (m * x + c)) has_bounded_variation_on s ⇔
    (m = 0) ∨ f has_bounded_variation_on IMAGE (λx. m * x + c) s

HAS_BOUNDED_VARIATION_AFFINITY_EQ_AND_VECTOR_VARIATION_AFFINITY

⊢ (∀m c f s.
     (λx. f (m * x + c)) has_bounded_variation_on s ⇔
     (m = 0) ∨ f has_bounded_variation_on IMAGE (λx. m * x + c) s) ∧
  ∀m c f s.
    vector_variation s (λx. f (m * x + c)) =
    if m = 0 then 0 else vector_variation (IMAGE (λx. m * x + c) s) f

HAS_BOUNDED_VARIATION_COMPARISON

⊢ ∀f g s.
    f has_bounded_variation_on s ∧
    (∀x y. x ∈ s ∧ y ∈ s ∧ x < y ⇒ dist (g x,g y) ≤ dist (f x,f y)) ⇒
    g has_bounded_variation_on s

HAS_BOUNDED_VARIATION_COMPOSE_DECREASING

⊢ ∀f g a b.
    (∀x y. x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒ f y ≤ f x) ∧
    g has_bounded_variation_on interval [(f b,f a)] ⇒
    g ∘ f has_bounded_variation_on interval [(a,b)]

HAS_BOUNDED_VARIATION_COMPOSE_INCREASING

⊢ ∀f g a b.
    (∀x y. x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒ f x ≤ f y) ∧
    g has_bounded_variation_on interval [(f a,f b)] ⇒
    g ∘ f has_bounded_variation_on interval [(a,b)]

HAS_BOUNDED_VARIATION_DARBOUX

⊢ ∀f a b.
    f has_bounded_variation_on interval [(a,b)] ⇔
    ∃g h.
      (∀x y. x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒ g x ≤ g y) ∧
      (∀x y. x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒ h x ≤ h y) ∧
      ∀x. f x = g x − h x

HAS_BOUNDED_VARIATION_DARBOUX_STRICT

⊢ ∀f a b.
    f has_bounded_variation_on interval [(a,b)] ⇔
    ∃g h.
      (∀x y. x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x < y ⇒ g x < g y) ∧
      (∀x y. x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x < y ⇒ h x < h y) ∧
      ∀x. f x = g x − h x

HAS_BOUNDED_VARIATION_DARBOUX_STRONG

⊢ ∀f a b.
    f has_bounded_variation_on interval [(a,b)] ⇒
    ∃g h.
      (∀x. f x = g x − h x) ∧
      (∀x y. x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒ g x ≤ g y) ∧
      (∀x y. x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒ h x ≤ h y) ∧
      (∀x y. x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x < y ⇒ g x < g y) ∧
      (∀x y. x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x < y ⇒ h x < h y) ∧
      (∀x. x ∈ interval [(a,b)] ∧ f continuous (at x within interval [(a,x)]) ⇒
           g continuous (at x within interval [(a,x)]) ∧
           h continuous (at x within interval [(a,x)])) ∧
      (∀x. x ∈ interval [(a,b)] ∧ f continuous (at x within interval [(x,b)]) ⇒
           g continuous (at x within interval [(x,b)]) ∧
           h continuous (at x within interval [(x,b)])) ∧
      ∀x. x ∈ interval [(a,b)] ∧ f continuous (at x within interval [(a,b)]) ⇒
          g continuous (at x within interval [(a,b)]) ∧
          h continuous (at x within interval [(a,b)])

HAS_BOUNDED_VARIATION_NONTRIVIAL

⊢ ∀f s.
    f has_bounded_variation_on s ⇔
    ∃B. ∀d t.
      d division_of t ∧ t ⊆ s ∧ (∀k. k ∈ d ⇒ interior k ≠ ∅) ⇒
      sum d (λk. abs (f (interval_upperbound k) − f (interval_lowerbound k))) ≤
      B

HAS_BOUNDED_VARIATION_ON_ABS

⊢ ∀f s.
    f has_bounded_variation_on s ⇒ (λx. abs (f x)) has_bounded_variation_on s

HAS_BOUNDED_VARIATION_ON_ADD

⊢ ∀f g s.
    f has_bounded_variation_on s ∧ g has_bounded_variation_on s ⇒
    (λx. f x + g x) has_bounded_variation_on s

HAS_BOUNDED_VARIATION_ON_CLOSURE

⊢ ∀f s.
    is_interval s ∧ f has_bounded_variation_on s ⇒
    f has_bounded_variation_on closure s

HAS_BOUNDED_VARIATION_ON_CMUL

⊢ ∀f c s.
    f has_bounded_variation_on s ⇒ (λx. c * f x) has_bounded_variation_on s

HAS_BOUNDED_VARIATION_ON_COMBINE

⊢ ∀f a b c.
    a ≤ c ∧ c ≤ b ⇒
    (f has_bounded_variation_on interval [(a,b)] ⇔
     f has_bounded_variation_on interval [(a,c)] ∧
     f has_bounded_variation_on interval [(c,b)])

HAS_BOUNDED_VARIATION_ON_COMBINE_GEN

⊢ ∀f s a.
    is_interval s ⇒
    (f has_bounded_variation_on s ⇔
     f has_bounded_variation_on {x | x ∈ s ∧ x ≤ a} ∧
     f has_bounded_variation_on {x | x ∈ s ∧ x ≥ a})

HAS_BOUNDED_VARIATION_ON_COMPONENTWISE

⊢ ∀f s. f has_bounded_variation_on s ⇔ (λx. f x) has_bounded_variation_on s

HAS_BOUNDED_VARIATION_ON_COMPOSE_LINEAR

⊢ ∀f g s.
    f has_bounded_variation_on s ∧ linear g ⇒ g ∘ f has_bounded_variation_on s

HAS_BOUNDED_VARIATION_ON_CONST

⊢ ∀s c. (λx. c) has_bounded_variation_on s

HAS_BOUNDED_VARIATION_ON_DIVISION

⊢ ∀f a b d.
    d division_of interval [(a,b)] ⇒
    ((∀k. k ∈ d ⇒ f has_bounded_variation_on k) ⇔
     f has_bounded_variation_on interval [(a,b)])

HAS_BOUNDED_VARIATION_ON_EMPTY

⊢ ∀f. f has_bounded_variation_on ∅

HAS_BOUNDED_VARIATION_ON_EQ

⊢ ∀f g s.
    (∀x. x ∈ s ⇒ (f x = g x)) ∧ f has_bounded_variation_on s ⇒
    g has_bounded_variation_on s

HAS_BOUNDED_VARIATION_ON_ID

⊢ ∀a b. (λx. x) has_bounded_variation_on interval [(a,b)]

HAS_BOUNDED_VARIATION_ON_IMP_BOUNDED

⊢ ∀f s. f has_bounded_variation_on s ∧ is_interval s ⇒ bounded (IMAGE f s)

HAS_BOUNDED_VARIATION_ON_IMP_BOUNDED_ON_INTERVAL

⊢ ∀f a b.
    f has_bounded_variation_on interval [(a,b)] ⇒
    bounded (IMAGE f (interval [(a,b)]))

HAS_BOUNDED_VARIATION_ON_IMP_BOUNDED_ON_SUBINTERVALS

⊢ ∀f s.
    f has_bounded_variation_on s ⇒
    bounded {f d − f c | interval [(c,d)] ⊆ s ∧ interval [(c,d)] ≠ ∅}

HAS_BOUNDED_VARIATION_ON_INDEFINITE_INTEGRAL_LEFT

⊢ ∀f a b.
    f absolutely_integrable_on interval [(a,b)] ⇒
    (λc. ∫ (interval [(c,b)]) f) has_bounded_variation_on interval [(a,b)]

HAS_BOUNDED_VARIATION_ON_INDEFINITE_INTEGRAL_RIGHT

⊢ ∀f a b.
    f absolutely_integrable_on interval [(a,b)] ⇒
    (λc. ∫ (interval [(a,c)]) f) has_bounded_variation_on interval [(a,b)]

HAS_BOUNDED_VARIATION_ON_MAX

⊢ ∀f g s.
    f has_bounded_variation_on s ∧ g has_bounded_variation_on s ⇒
    (λx. max (f x) (g x)) has_bounded_variation_on s

HAS_BOUNDED_VARIATION_ON_MIN

⊢ ∀f g s.
    f has_bounded_variation_on s ∧ g has_bounded_variation_on s ⇒
    (λx. min (f x) (g x)) has_bounded_variation_on s

HAS_BOUNDED_VARIATION_ON_MUL

⊢ ∀f g a b.
    f has_bounded_variation_on interval [(a,b)] ∧
    g has_bounded_variation_on interval [(a,b)] ⇒
    (λx. f x * g x) has_bounded_variation_on interval [(a,b)]

HAS_BOUNDED_VARIATION_ON_NEG

⊢ ∀f s. f has_bounded_variation_on s ⇒ (λx. -f x) has_bounded_variation_on s

HAS_BOUNDED_VARIATION_ON_NULL

⊢ ∀f s. (content s = 0) ∧ bounded s ⇒ f has_bounded_variation_on s

HAS_BOUNDED_VARIATION_ON_REFLECT

⊢ ∀f s.
    f has_bounded_variation_on IMAGE (λx. -x) s ⇒
    (λx. f (-x)) has_bounded_variation_on s

HAS_BOUNDED_VARIATION_ON_REFLECT_INTERVAL

⊢ ∀f a b.
    f has_bounded_variation_on interval [(-b,-a)] ⇒
    (λx. f (-x)) has_bounded_variation_on interval [(a,b)]

HAS_BOUNDED_VARIATION_ON_SING

⊢ ∀f a. f has_bounded_variation_on {a}

HAS_BOUNDED_VARIATION_ON_SUB

⊢ ∀f g s.
    f has_bounded_variation_on s ∧ g has_bounded_variation_on s ⇒
    (λx. f x − g x) has_bounded_variation_on s

HAS_BOUNDED_VARIATION_ON_SUBSET

⊢ ∀f s t. f has_bounded_variation_on s ∧ t ⊆ s ⇒ f has_bounded_variation_on t

HAS_BOUNDED_VARIATION_ON_SUM

⊢ ∀f s k.
    FINITE k ∧ (∀i. i ∈ k ⇒ f i has_bounded_variation_on s) ⇒
    (λx. sum k (λi. f i x)) has_bounded_variation_on s

HAS_BOUNDED_VARIATION_ON_SUM_AND_SUM_LE

⊢ (∀f s k.
     FINITE k ∧ (∀i. i ∈ k ⇒ f i has_bounded_variation_on s) ⇒
     (λx. sum k (λi. f i x)) has_bounded_variation_on s) ∧
  ∀f s k.
    FINITE k ∧ (∀i. i ∈ k ⇒ f i has_bounded_variation_on s) ⇒
    vector_variation s (λx. sum k (λi. f i x)) ≤
    sum k (λi. vector_variation s (f i))

HAS_BOUNDED_VARIATION_REFLECT2_EQ

⊢ ∀f s.
    (λx. f (-x)) has_bounded_variation_on IMAGE (λx. -x) s ⇔
    f has_bounded_variation_on s

HAS_BOUNDED_VARIATION_REFLECT2_EQ_AND_VECTOR_VARIATION_REFLECT2

⊢ (∀f s.
     (λx. f (-x)) has_bounded_variation_on IMAGE (λx. -x) s ⇔
     f has_bounded_variation_on s) ∧
  ∀f s.
    vector_variation (IMAGE (λx. -x) s) (λx. f (-x)) = vector_variation s f

HAS_BOUNDED_VARIATION_REFLECT_EQ

⊢ ∀f s.
    (λx. f (-x)) has_bounded_variation_on s ⇔
    f has_bounded_variation_on IMAGE (λx. -x) s

HAS_BOUNDED_VARIATION_REFLECT_EQ_AND_VECTOR_VARIATION_REFLECT

⊢ (∀f s.
     (λx. f (-x)) has_bounded_variation_on s ⇔
     f has_bounded_variation_on IMAGE (λx. -x) s) ∧
  ∀f s.
    vector_variation s (λx. f (-x)) = vector_variation (IMAGE (λx. -x) s) f

HAS_BOUNDED_VARIATION_REFLECT_EQ_INTERVAL

⊢ ∀f u v.
    (λx. f (-x)) has_bounded_variation_on interval [(u,v)] ⇔
    f has_bounded_variation_on interval [(-v,-u)]

HAS_BOUNDED_VARIATION_REFLECT_EQ_INTERVAL_AND_VECTOR_VARIATION_REFLECT_INTERVAL

⊢ (∀f u v.
     (λx. f (-x)) has_bounded_variation_on interval [(u,v)] ⇔
     f has_bounded_variation_on interval [(-v,-u)]) ∧
  ∀f u v.
    vector_variation (interval [(u,v)]) (λx. f (-x)) =
    vector_variation (interval [(-v,-u)]) f

HAS_BOUNDED_VARIATION_SUM_LE

⊢ ∀f s k.
    FINITE k ∧ (∀i. i ∈ k ⇒ f i has_bounded_variation_on s) ⇒
    vector_variation s (λx. sum k (λi. f i x)) ≤
    sum k (λi. vector_variation s (f i))

HAS_BOUNDED_VARIATION_TRANSLATION

⊢ ∀f s a.
    f has_bounded_variation_on s ⇒
    (λx. f (a + x)) has_bounded_variation_on IMAGE (λx. -a + x) s

HAS_BOUNDED_VARIATION_TRANSLATION2_EQ

⊢ ∀a f s.
    (λx. f (a + x)) has_bounded_variation_on IMAGE (λx. -a + x) s ⇔
    f has_bounded_variation_on s

HAS_BOUNDED_VARIATION_TRANSLATION2_EQ_AND_VECTOR_VARIATION_TRANSLATION2

⊢ (∀a f s.
     (λx. f (a + x)) has_bounded_variation_on IMAGE (λx. -a + x) s ⇔
     f has_bounded_variation_on s) ∧
  ∀a f s.
    vector_variation (IMAGE (λx. -a + x) s) (λx. f (a + x)) =
    vector_variation s f

HAS_BOUNDED_VARIATION_TRANSLATION_EQ

⊢ ∀a f s.
    (λx. f (a + x)) has_bounded_variation_on s ⇔
    f has_bounded_variation_on IMAGE (λx. a + x) s

HAS_BOUNDED_VARIATION_TRANSLATION_EQ_AND_VECTOR_VARIATION_TRANSLATION

⊢ (∀a f s.
     (λx. f (a + x)) has_bounded_variation_on s ⇔
     f has_bounded_variation_on IMAGE (λx. a + x) s) ∧
  ∀a f s.
    vector_variation s (λx. f (a + x)) =
    vector_variation (IMAGE (λx. a + x) s) f

HAS_BOUNDED_VARIATION_TRANSLATION_EQ_INTERVAL

⊢ ∀a f u v.
    (λx. f (a + x)) has_bounded_variation_on interval [(u,v)] ⇔
    f has_bounded_variation_on interval [(a + u,a + v)]

HAS_BOUNDED_VARIATION_TRANSLATION_EQ_INTERVAL_AND_VECTOR_VARIATION_TRANSLATION_INTERVAL

⊢ (∀a f u v.
     (λx. f (a + x)) has_bounded_variation_on interval [(u,v)] ⇔
     f has_bounded_variation_on interval [(a + u,a + v)]) ∧
  ∀a f u v.
    vector_variation (interval [(u,v)]) (λx. f (a + x)) =
    vector_variation (interval [(a + u,a + v)]) f

HAS_BOUNDED_VECTOR_VARIATION_LEFT_LIMIT

⊢ ∀f a b c.
    f has_bounded_variation_on interval [(a,b)] ∧ c ∈ interval [(a,b)] ⇒
    ∃l. (f ⟶ l) (at c within interval [(a,c)])

HAS_BOUNDED_VECTOR_VARIATION_RIGHT_LIMIT

⊢ ∀f a b c.
    f has_bounded_variation_on interval [(a,b)] ∧ c ∈ interval [(a,b)] ⇒
    ∃l. (f ⟶ l) (at c within interval [(c,b)])

HAS_DERIVATIVE_ZERO_UNIQUE_STRONG_INTERVAL

⊢ ∀f a b k y.
    COUNTABLE k ∧ f continuous_on interval [(a,b)] ∧ (f a = y) ∧
    (∀x. x ∈ interval [(a,b)] DIFF k ⇒
         (f has_derivative (λh. 0)) (at x within interval [(a,b)])) ⇒
    ∀x. x ∈ interval [(a,b)] ⇒ (f x = y)

HAS_INTEGRAL

⊢ ∀f i s.
    (f has_integral i) s ⇔
    ∀e. 0 < e ⇒
        ∃B. 0 < B ∧
            ∀a b.
              ball (0,B) ⊆ interval [(a,b)] ⇒
              ∃z. ((λx. if x ∈ s then f x else 0) has_integral z)
                    (interval [(a,b)]) ∧ abs (z − i) < e

HAS_INTEGRAL_0

⊢ ∀s. ((λx. 0) has_integral 0) s

HAS_INTEGRAL_0_EQ

⊢ ∀i s. ((λx. 0) has_integral i) s ⇔ (i = 0)

HAS_INTEGRAL_ABS_BOUND_INTEGRAL_COMPONENT

⊢ ∀f g s i j.
    (f has_integral i) s ∧ (g has_integral j) s ∧
    (∀x. x ∈ s ⇒ abs (f x) ≤ g x) ⇒
    abs i ≤ j

HAS_INTEGRAL_ADD

⊢ ∀f g s k.
    (f has_integral k) s ∧ (g has_integral l) s ⇒
    ((λx. f x + g x) has_integral k + l) s

HAS_INTEGRAL_AFFINITY

⊢ ∀f i a b m c.
    (f has_integral i) (interval [(a,b)]) ∧ m ≠ 0 ⇒
    ((λx. f (m * x + c)) has_integral (abs m pow 1)⁻¹ * i)
      (IMAGE (λx. m⁻¹ * x + -(m⁻¹ * c)) (interval [(a,b)]))

HAS_INTEGRAL_ALT

⊢ ∀f s i.
    (f has_integral i) s ⇔
    (∀a b. (λx. if x ∈ s then f x else 0) integrable_on interval [(a,b)]) ∧
    ∀e. 0 < e ⇒
        ∃B. 0 < B ∧
            ∀a b.
              ball (0,B) ⊆ interval [(a,b)] ⇒
              abs (∫ (interval [(a,b)]) (λx. if x ∈ s then f x else 0) − i) <
              e

HAS_INTEGRAL_BIGUNION

⊢ ∀f i t.
    FINITE t ∧ (∀s. s ∈ t ⇒ (f has_integral i s) s) ∧
    (∀s s'. s ∈ t ∧ s' ∈ t ∧ s ≠ s' ⇒ negligible (s ∩ s')) ⇒
    (f has_integral sum t i) (BIGUNION t)

HAS_INTEGRAL_BOUND

⊢ ∀f a b i B.
    0 ≤ B ∧ (f has_integral i) (interval [(a,b)]) ∧
    (∀x. x ∈ interval [(a,b)] ⇒ abs (f x) ≤ B) ⇒
    abs i ≤ B * content (interval [(a,b)])

HAS_INTEGRAL_CLOSURE

⊢ ∀f y s.
    negligible (frontier s) ⇒
    ((f has_integral y) (closure s) ⇔ (f has_integral y) s)

HAS_INTEGRAL_CMUL

⊢ ∀f k s c. (f has_integral k) s ⇒ ((λx. c * f x) has_integral c * k) s

HAS_INTEGRAL_COMBINE

⊢ ∀f i j a b c.
    a ≤ c ∧ c ≤ b ∧ (f has_integral i) (interval [(a,c)]) ∧
    (f has_integral j) (interval [(c,b)]) ⇒
    (f has_integral i + j) (interval [(a,b)])

HAS_INTEGRAL_COMBINE_DIVISION

⊢ ∀f s d i.
    d division_of s ∧ (∀k. k ∈ d ⇒ (f has_integral i k) k) ⇒
    (f has_integral sum d i) s

HAS_INTEGRAL_COMBINE_DIVISION_TOPDOWN

⊢ ∀f s d k.
    f integrable_on s ∧ d division_of k ∧ k ⊆ s ⇒
    (f has_integral sum d (λi. ∫ i f)) k

HAS_INTEGRAL_COMBINE_TAGGED_DIVISION

⊢ ∀f s p i.
    p tagged_division_of s ∧ (∀x k. (x,k) ∈ p ⇒ (f has_integral i k) k) ⇒
    (f has_integral sum p (λ(x,k). i k)) s

HAS_INTEGRAL_COMBINE_TAGGED_DIVISION_TOPDOWN

⊢ ∀f a b p.
    f integrable_on interval [(a,b)] ∧ p tagged_division_of interval [(a,b)] ⇒
    (f has_integral sum p (λ(x,k). ∫ k f)) (interval [(a,b)])

HAS_INTEGRAL_COMPONENTWISE

⊢ ∀f s y. (f has_integral y) s ⇔ ((λx. f x) has_integral y) s

HAS_INTEGRAL_COMPONENT_LBOUND

⊢ ∀f a b i.
    (f has_integral i) (interval [(a,b)]) ∧
    (∀x. x ∈ interval [(a,b)] ⇒ B ≤ f x) ⇒
    B * content (interval [(a,b)]) ≤ i

HAS_INTEGRAL_COMPONENT_LE

⊢ ∀f g s i j.
    (f has_integral i) s ∧ (g has_integral j) s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒
    i ≤ j

HAS_INTEGRAL_COMPONENT_LE_AE

⊢ ∀f g s i j k t.
    negligible t ∧ (f has_integral i) s ∧ (g has_integral j) s ∧
    (∀x. x ∈ s DIFF t ⇒ f x ≤ g x) ⇒
    i ≤ j

HAS_INTEGRAL_COMPONENT_NEG

⊢ ∀f s i. (f has_integral i) s ∧ (∀x. x ∈ s ⇒ f x ≤ 0) ⇒ i ≤ 0

HAS_INTEGRAL_COMPONENT_POS

⊢ ∀f s i. (f has_integral i) s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ i

HAS_INTEGRAL_COMPONENT_UBOUND

⊢ ∀f a b i.
    (f has_integral i) (interval [(a,b)]) ∧
    (∀x. x ∈ interval [(a,b)] ⇒ f x ≤ B) ⇒
    i ≤ B * content (interval [(a,b)])

HAS_INTEGRAL_CONST

⊢ ∀a b c.
    ((λx. c) has_integral content (interval [(a,b)]) * c) (interval [(a,b)])

HAS_INTEGRAL_DIFF

⊢ ∀f i j s t.
    (f has_integral i) s ∧ (f has_integral j) t ∧ negligible (t DIFF s) ⇒
    (f has_integral i − j) (s DIFF t)

HAS_INTEGRAL_DROP_LE

⊢ ∀f g s i j.
    (f has_integral i) s ∧ (g has_integral j) s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒
    i ≤ j

HAS_INTEGRAL_DROP_NEG

⊢ ∀f s i. (f has_integral i) s ∧ (∀x. x ∈ s ⇒ f x ≤ 0) ⇒ i ≤ 0

HAS_INTEGRAL_DROP_POS

⊢ ∀f s i. (f has_integral i) s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ i

HAS_INTEGRAL_DROP_POS_AE

⊢ ∀f s t i.
    (f has_integral i) s ∧ negligible t ∧ (∀x. x ∈ s DIFF t ⇒ 0 ≤ f x) ⇒ 0 ≤ i

HAS_INTEGRAL_EMPTY

⊢ ∀f. (f has_integral 0) ∅

HAS_INTEGRAL_EMPTY_EQ

⊢ ∀f i. (f has_integral i) ∅ ⇔ (i = 0)

HAS_INTEGRAL_EQ

⊢ ∀f g k s.
    (∀x. x ∈ s ⇒ (f x = g x)) ∧ (f has_integral k) s ⇒ (g has_integral k) s

HAS_INTEGRAL_EQ_EQ

⊢ ∀f g k s.
    (∀x. x ∈ s ⇒ (f x = g x)) ⇒ ((f has_integral k) s ⇔ (g has_integral k) s)

HAS_INTEGRAL_FACTOR_CONTENT

⊢ ∀f i a b.
    (f has_integral i) (interval [(a,b)]) ⇔
    ∀e. 0 < e ⇒
        ∃d. gauge d ∧
            ∀p. p tagged_division_of interval [(a,b)] ∧ d FINE p ⇒
                abs (sum p (λ(x,k). content k * f x) − i) ≤
                e * content (interval [(a,b)])

HAS_INTEGRAL_INTEGRABLE

⊢ ∀f i s. (f has_integral i) s ⇒ f integrable_on s

HAS_INTEGRAL_INTEGRABLE_INTEGRAL

⊢ ∀f i s. (f has_integral i) s ⇔ f integrable_on s ∧ (∫ s f = i)

HAS_INTEGRAL_INTEGRAL

⊢ ∀f s. f integrable_on s ⇔ (f has_integral ∫ s f) s

HAS_INTEGRAL_INTERIOR

⊢ ∀f y s.
    negligible (frontier s) ⇒
    ((f has_integral y) (interior s) ⇔ (f has_integral y) s)

HAS_INTEGRAL_IS_0

⊢ ∀f s. (∀x. x ∈ s ⇒ (f x = 0)) ⇒ (f has_integral 0) s

HAS_INTEGRAL_LE_AE

⊢ ∀f g s i j t.
    (f has_integral i) s ∧ (g has_integral j) s ∧ negligible t ∧
    (∀x. x ∈ s DIFF t ⇒ f x ≤ g x) ⇒
    i ≤ j

HAS_INTEGRAL_LIM_AT_POSINFINITY

⊢ ∀f l.
    (f has_integral l) {t | 0 ≤ t} ⇔
    (∀a. f integrable_on interval [(0,a)]) ∧
    ((λa. ∫ (interval [(0,a)]) f) ⟶ l) at_posinfinity

HAS_INTEGRAL_LIM_SEQUENTIALLY

⊢ ∀f l.
    (f ⟶ 0) at_posinfinity ∧ (∀n. f integrable_on interval [(0,&n)]) ∧
    ((λn. ∫ (interval [(0,&n)]) f) ⟶ l) sequentially ⇒
    (f has_integral l) {t | 0 ≤ t}

HAS_INTEGRAL_LINEAR

⊢ ∀f y s h. (f has_integral y) s ∧ linear h ⇒ (h ∘ f has_integral h y) s

HAS_INTEGRAL_NEG

⊢ ∀f k s. (f has_integral k) s ⇒ ((λx. -f x) has_integral -k) s

HAS_INTEGRAL_NEGLIGIBLE

⊢ ∀f s t. negligible s ∧ (∀x. x ∈ t DIFF s ⇒ (f x = 0)) ⇒ (f has_integral 0) t

HAS_INTEGRAL_NEGLIGIBLE_EQ

⊢ ∀f s.
    (∀x i. x ∈ s ⇒ 0 ≤ f x) ⇒
    ((f has_integral 0) s ⇔ negligible {x | x ∈ s ∧ f x ≠ 0})

HAS_INTEGRAL_NULL

⊢ ∀f a b.
    (content (interval [(a,b)]) = 0) ⇒ (f has_integral 0) (interval [(a,b)])

HAS_INTEGRAL_NULL_EQ

⊢ ∀f a b i.
    (content (interval [(a,b)]) = 0) ⇒
    ((f has_integral i) (interval [(a,b)]) ⇔ (i = 0))

HAS_INTEGRAL_ON_SUPERSET

⊢ ∀f s t i.
    (∀x. x ∉ s ⇒ (f x = 0)) ∧ s ⊆ t ∧ (f has_integral i) s ⇒
    (f has_integral i) t

HAS_INTEGRAL_REFL

⊢ ∀f a. (f has_integral 0) (interval [(a,a)])

HAS_INTEGRAL_REFLECT

⊢ ∀f i a b.
    ((λx. f (-x)) has_integral i) (interval [(-b,-a)]) ⇔
    (f has_integral i) (interval [(a,b)])

HAS_INTEGRAL_REFLECT_GEN

⊢ ∀f i s.
    ((λx. f (-x)) has_integral i) s ⇔ (f has_integral i) (IMAGE (λx. -x) s)

HAS_INTEGRAL_REFLECT_LEMMA

⊢ ∀f i a b.
    (f has_integral i) (interval [(a,b)]) ⇒
    ((λx. f (-x)) has_integral i) (interval [(-b,-a)])

HAS_INTEGRAL_RESTRICT

⊢ ∀f s t i.
    s ⊆ t ⇒
    (((λx. if x ∈ s then f x else 0) has_integral i) t ⇔ (f has_integral i) s)

HAS_INTEGRAL_RESTRICT_CLOSED_SUBINTERVAL

⊢ ∀f a b c d i.
    (f has_integral i) (interval [(c,d)]) ∧
    interval [(c,d)] ⊆ interval [(a,b)] ⇒
    ((λx. if x ∈ interval [(c,d)] then f x else 0) has_integral i)
      (interval [(a,b)])

HAS_INTEGRAL_RESTRICT_CLOSED_SUBINTERVALS_EQ

⊢ ∀f a b c d i.
    interval [(c,d)] ⊆ interval [(a,b)] ⇒
    (((λx. if x ∈ interval [(c,d)] then f x else 0) has_integral i)
       (interval [(a,b)]) ⇔ (f has_integral i) (interval [(c,d)]))

HAS_INTEGRAL_RESTRICT_INTER

⊢ ∀f s t.
    ((λx. if x ∈ s then f x else 0) has_integral i) t ⇔
    (f has_integral i) (s ∩ t)

HAS_INTEGRAL_RESTRICT_OPEN_SUBINTERVAL

⊢ ∀f a b c d i.
    (f has_integral i) (interval [(c,d)]) ∧
    interval [(c,d)] ⊆ interval [(a,b)] ⇒
    ((λx. if x ∈ interval (c,d) then f x else 0) has_integral i)
      (interval [(a,b)])

HAS_INTEGRAL_RESTRICT_UNIV

⊢ ∀f s i.
    ((λx. if x ∈ s then f x else 0) has_integral i) 𝕌(:real) ⇔
    (f has_integral i) s

HAS_INTEGRAL_SEPARATE_SIDES

⊢ ∀f i a b.
    (f has_integral i) (interval [(a,b)]) ⇒
    ∀e. 0 < e ⇒
        ∃d. gauge d ∧
            ∀p1 p2.
              p1 tagged_division_of interval [(a,b)] ∩ {x | x ≤ c} ∧
              d FINE p1 ∧
              p2 tagged_division_of interval [(a,b)] ∩ {x | x ≥ c} ∧ d FINE p2 ⇒
              abs
                (sum p1 (λ(x,k). content k * f x) +
                 sum p2 (λ(x,k). content k * f x) − i) < e

HAS_INTEGRAL_SPIKE

⊢ ∀f g s t y.
    negligible s ∧ (∀x. x ∈ t DIFF s ⇒ (g x = f x)) ∧ (f has_integral y) t ⇒
    (g has_integral y) t

HAS_INTEGRAL_SPIKE_EQ

⊢ ∀f g s t y.
    negligible s ∧ (∀x. x ∈ t DIFF s ⇒ (g x = f x)) ⇒
    ((f has_integral y) t ⇔ (g has_integral y) t)

HAS_INTEGRAL_SPIKE_FINITE

⊢ ∀f g s t y.
    FINITE s ∧ (∀x. x ∈ t DIFF s ⇒ (g x = f x)) ∧ (f has_integral y) t ⇒
    (g has_integral y) t

HAS_INTEGRAL_SPIKE_FINITE_EQ

⊢ ∀f g s t y.
    FINITE s ∧ (∀x. x ∈ t DIFF s ⇒ (g x = f x)) ⇒
    ((f has_integral y) t ⇔ (g has_integral y) t)

HAS_INTEGRAL_SPIKE_INTERIOR

⊢ ∀f g a b y.
    (∀x. x ∈ interval (a,b) ⇒ (g x = f x)) ∧
    (f has_integral y) (interval [(a,b)]) ⇒
    (g has_integral y) (interval [(a,b)])

HAS_INTEGRAL_SPIKE_INTERIOR_EQ

⊢ ∀f g a b y.
    (∀x. x ∈ interval (a,b) ⇒ (g x = f x)) ⇒
    ((f has_integral y) (interval [(a,b)]) ⇔
     (g has_integral y) (interval [(a,b)]))

HAS_INTEGRAL_SPIKE_SET

⊢ ∀f s t y.
    negligible (s DIFF t ∪ (t DIFF s)) ∧ (f has_integral y) s ⇒
    (f has_integral y) t

HAS_INTEGRAL_SPIKE_SET_EQ

⊢ ∀f s t y.
    negligible (s DIFF t ∪ (t DIFF s)) ⇒
    ((f has_integral y) s ⇔ (f has_integral y) t)

HAS_INTEGRAL_SPLIT

⊢ ∀f a b c.
    (f has_integral i) (interval [(a,b)] ∩ {x | x ≤ c}) ∧
    (f has_integral j) (interval [(a,b)] ∩ {x | x ≥ c}) ⇒
    (f has_integral i + j) (interval [(a,b)])

HAS_INTEGRAL_STRADDLE_NULL

⊢ ∀f g s.
    (∀x. x ∈ s ⇒ 0 ≤ f x ∧ f x ≤ g x) ∧ (g has_integral 0) s ⇒
    (f has_integral 0) s

HAS_INTEGRAL_STRETCH

⊢ ∀f i m a b.
    (f has_integral i) (interval [(a,b)]) ∧ m 1 ≠ 0 ⇒
    ((λx. f (m 1 * x)) has_integral (abs (product (1 .. 1) m))⁻¹ * i)
      (IMAGE (λx. (m 1)⁻¹ * x) (interval [(a,b)]))

HAS_INTEGRAL_SUB

⊢ ∀f g s k l.
    (f has_integral k) s ∧ (g has_integral l) s ⇒
    ((λx. f x − g x) has_integral k − l) s

HAS_INTEGRAL_SUBSET_COMPONENT_LE

⊢ ∀f s t i j.
    s ⊆ t ∧ (f has_integral i) s ∧ (f has_integral j) t ∧
    (∀x. x ∈ t ⇒ 0 ≤ f x) ⇒
    i ≤ j

HAS_INTEGRAL_SUBSET_DROP_LE

⊢ ∀f s t i j.
    s ⊆ t ∧ (f has_integral i) s ∧ (f has_integral j) t ∧
    (∀x. x ∈ t ⇒ 0 ≤ f x) ⇒
    i ≤ j

HAS_INTEGRAL_SUM

⊢ ∀f s t.
    FINITE t ∧ (∀a. a ∈ t ⇒ (f a has_integral i a) s) ⇒
    ((λx. sum t (λa. f a x)) has_integral sum t i) s

HAS_INTEGRAL_TWIDDLE

⊢ ∀f g h r i a b.
    0 < r ∧ (∀x. h (g x) = x) ∧ (∀x. g (h x) = x) ∧ (∀x. g continuous at x) ∧
    (∀u v. ∃w z. IMAGE g (interval [(u,v)]) = interval [(w,z)]) ∧
    (∀u v. ∃w z. IMAGE h (interval [(u,v)]) = interval [(w,z)]) ∧
    (∀u v.
       content (IMAGE g (interval [(u,v)])) = r * content (interval [(u,v)])) ∧
    (f has_integral i) (interval [(a,b)]) ⇒
    ((λx. f (g x)) has_integral r⁻¹ * i) (IMAGE h (interval [(a,b)]))

HAS_INTEGRAL_UNION

⊢ ∀f i j s t.
    (f has_integral i) s ∧ (f has_integral j) t ∧ negligible (s ∩ t) ⇒
    (f has_integral i + j) (s ∪ t)

HAS_INTEGRAL_UNIQUE

⊢ ∀f i k1 k2. (f has_integral k1) i ∧ (f has_integral k2) i ⇒ (k1 = k2)

HENSTOCK_LEMMA

⊢ ∀f a b.
    f integrable_on interval [(a,b)] ⇒
    ∀e. 0 < e ⇒
        ∃d. gauge d ∧
            ∀p. p tagged_partial_division_of interval [(a,b)] ∧ d FINE p ⇒
                sum p (λ(x,k). abs (content k * f x − ∫ k f)) < e

HENSTOCK_LEMMA_PART1

⊢ ∀f a b d e.
    f integrable_on interval [(a,b)] ∧ 0 < e ∧ gauge d ∧
    (∀p. p tagged_division_of interval [(a,b)] ∧ d FINE p ⇒
         abs (sum p (λ(x,k). content k * f x) − ∫ (interval [(a,b)]) f) < e) ⇒
    ∀p. p tagged_partial_division_of interval [(a,b)] ∧ d FINE p ⇒
        abs (sum p (λ(x,k). content k * f x − ∫ k f)) ≤ e

HENSTOCK_LEMMA_PART2

⊢ ∀f a b d e.
    f integrable_on interval [(a,b)] ∧ 0 < e ∧ gauge d ∧
    (∀p. p tagged_division_of interval [(a,b)] ∧ d FINE p ⇒
         abs (sum p (λ(x,k). content k * f x) − ∫ (interval [(a,b)]) f) < e) ⇒
    ∀p. p tagged_partial_division_of interval [(a,b)] ∧ d FINE p ⇒
        sum p (λ(x,k). abs (content k * f x − ∫ k f)) ≤ 2 * 1 * e

INCREASING_BOUNDED_VARIATION

⊢ ∀f a b.
    (∀x y. x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒ f x ≤ f y) ⇒
    f has_bounded_variation_on interval [(a,b)]

INCREASING_BOUNDED_VARIATION_GEN

⊢ ∀f s.
    bounded (IMAGE f s) ∧ (∀x y. x ∈ s ∧ y ∈ s ∧ x ≤ y ⇒ f x ≤ f y) ⇒
    f has_bounded_variation_on s

INCREASING_LEFT_LIMIT

⊢ ∀f a b c.
    (∀x y. x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒ f x ≤ f y) ∧
    c ∈ interval [(a,b)] ⇒
    ∃l. (f ⟶ l) (at c within interval [(a,c)])

INCREASING_RIGHT_LIMIT

⊢ ∀f a b c.
    (∀x y. x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒ f x ≤ f y) ∧
    c ∈ interval [(a,b)] ⇒
    ∃l. (f ⟶ l) (at c within interval [(c,b)])

INCREASING_VECTOR_VARIATION

⊢ ∀f a b.
    interval [(a,b)] ≠ ∅ ∧
    (∀x y. x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒ f x ≤ f y) ⇒
    (vector_variation (interval [(a,b)]) f = f b − f a)

INDEFINITE_INTEGRAL_CONTINUOUS

⊢ ∀f a b c d e.
    f integrable_on interval [(a,b)] ∧ c ∈ interval [(a,b)] ∧
    d ∈ interval [(a,b)] ∧ 0 < e ⇒
    ∃k. 0 < k ∧
        ∀c' d'.
          c' ∈ interval [(a,b)] ∧ d' ∈ interval [(a,b)] ∧ abs (c' − c) ≤ k ∧
          abs (d' − d) ≤ k ⇒
          abs (∫ (interval [(c',d')]) f − ∫ (interval [(c,d)]) f) < e

INDEFINITE_INTEGRAL_CONTINUOUS_LEFT

⊢ ∀f a b.
    f integrable_on interval [(a,b)] ⇒
    (λx. ∫ (interval [(x,b)]) f) continuous_on interval [(a,b)]

INDEFINITE_INTEGRAL_CONTINUOUS_RIGHT

⊢ ∀f a b.
    f integrable_on interval [(a,b)] ⇒
    (λx. ∫ (interval [(a,x)]) f) continuous_on interval [(a,b)]

INDICATOR_EMPTY

⊢ indicator ∅ = (λx. 0)

INTEGRABLE_0

⊢ ∀s. (λx. 0) integrable_on s

INTEGRABLE_ADD

⊢ ∀f g s.
    f integrable_on s ∧ g integrable_on s ⇒ (λx. f x + g x) integrable_on s

INTEGRABLE_AFFINITY

⊢ ∀f a b m c.
    f integrable_on interval [(a,b)] ∧ m ≠ 0 ⇒
    (λx. f (m * x + c)) integrable_on
    IMAGE (λx. m⁻¹ * x + -(m⁻¹ * c)) (interval [(a,b)])

INTEGRABLE_ALT

⊢ ∀f s.
    f integrable_on s ⇔
    (∀a b. (λx. if x ∈ s then f x else 0) integrable_on interval [(a,b)]) ∧
    ∀e. 0 < e ⇒
        ∃B. 0 < B ∧
            ∀a b c d.
              ball (0,B) ⊆ interval [(a,b)] ∧ ball (0,B) ⊆ interval [(c,d)] ⇒
              abs
                (∫ (interval [(a,b)]) (λx. if x ∈ s then f x else 0) −
                 ∫ (interval [(c,d)]) (λx. if x ∈ s then f x else 0)) < e

INTEGRABLE_ALT_SUBSET

⊢ ∀f s.
    f integrable_on s ⇔
    (∀a b. (λx. if x ∈ s then f x else 0) integrable_on interval [(a,b)]) ∧
    ∀e. 0 < e ⇒
        ∃B. 0 < B ∧
            ∀a b c d.
              ball (0,B) ⊆ interval [(a,b)] ∧
              interval [(a,b)] ⊆ interval [(c,d)] ⇒
              abs
                (∫ (interval [(a,b)]) (λx. if x ∈ s then f x else 0) −
                 ∫ (interval [(c,d)]) (λx. if x ∈ s then f x else 0)) < e

INTEGRABLE_BOUNDED_VARIATION

⊢ ∀f a b.
    f has_bounded_variation_on interval [(a,b)] ⇒
    f integrable_on interval [(a,b)]

INTEGRABLE_BOUNDED_VARIATION_BILINEAR_LMUL

⊢ ∀op f g a b.
    bilinear op ∧ f integrable_on interval [(a,b)] ∧
    g has_bounded_variation_on interval [(a,b)] ⇒
    (λx. op (g x) (f x)) integrable_on interval [(a,b)]

INTEGRABLE_BOUNDED_VARIATION_BILINEAR_RMUL

⊢ ∀op f g a b.
    bilinear op ∧ f integrable_on interval [(a,b)] ∧
    g has_bounded_variation_on interval [(a,b)] ⇒
    (λx. op (f x) (g x)) integrable_on interval [(a,b)]

INTEGRABLE_BOUNDED_VARIATION_PRODUCT

⊢ ∀f g a b.
    f integrable_on interval [(a,b)] ∧
    g has_bounded_variation_on interval [(a,b)] ⇒
    (λx. g x * f x) integrable_on interval [(a,b)]

INTEGRABLE_BOUNDED_VARIATION_PRODUCT_ALT

⊢ ∀f g a b.
    f integrable_on interval [(a,b)] ∧
    g has_bounded_variation_on interval [(a,b)] ⇒
    (λx. g x * f x) integrable_on interval [(a,b)]

INTEGRABLE_BY_PARTS

⊢ ∀bop f g f' g' a b c.
    bilinear bop ∧ COUNTABLE c ∧
    (λx. bop (f x) (g x)) continuous_on interval [(a,b)] ∧
    (∀x. x ∈ interval (a,b) DIFF c ⇒
         (f has_vector_derivative f' x) (at x) ∧
         (g has_vector_derivative g' x) (at x)) ∧
    (λx. bop (f x) (g' x)) integrable_on interval [(a,b)] ⇒
    (λx. bop (f' x) (g x)) integrable_on interval [(a,b)]

INTEGRABLE_BY_PARTS_EQ

⊢ ∀bop f g f' g' a b c.
    bilinear bop ∧ COUNTABLE c ∧
    (λx. bop (f x) (g x)) continuous_on interval [(a,b)] ∧
    (∀x. x ∈ interval (a,b) DIFF c ⇒
         (f has_vector_derivative f' x) (at x) ∧
         (g has_vector_derivative g' x) (at x)) ⇒
    ((λx. bop (f x) (g' x)) integrable_on interval [(a,b)] ⇔
     (λx. bop (f' x) (g x)) integrable_on interval [(a,b)])

INTEGRABLE_CASES

⊢ ∀P f g s.
    f integrable_on {x | x ∈ s ∧ P x} ∧ g integrable_on {x | x ∈ s ∧ ¬P x} ⇒
    (λx. if P x then f x else g x) integrable_on s

INTEGRABLE_CAUCHY

⊢ ∀f a b.
    f integrable_on interval [(a,b)] ⇔
    ∀e. 0 < e ⇒
        ∃d. gauge d ∧
            ∀p1 p2.
              p1 tagged_division_of interval [(a,b)] ∧ d FINE p1 ∧
              p2 tagged_division_of interval [(a,b)] ∧ d FINE p2 ⇒
              abs
                (sum p1 (λ(x,k). content k * f x) −
                 sum p2 (λ(x,k). content k * f x)) < e

INTEGRABLE_CMUL

⊢ ∀f c s. f integrable_on s ⇒ (λx. c * f x) integrable_on s

INTEGRABLE_CMUL_EQ

⊢ ∀f s c. (λx. c * f x) integrable_on s ⇔ (c = 0) ∨ f integrable_on s

INTEGRABLE_COMBINE

⊢ ∀f a b c.
    a ≤ c ∧ c ≤ b ∧ f integrable_on interval [(a,c)] ∧
    f integrable_on interval [(c,b)] ⇒
    f integrable_on interval [(a,b)]

INTEGRABLE_COMBINE_DIVISION

⊢ ∀f d s.
    d division_of s ∧ (∀i. i ∈ d ⇒ f integrable_on i) ⇒ f integrable_on s

INTEGRABLE_COMPONENTWISE

⊢ ∀f s. f integrable_on s ⇔ (λx. f x) integrable_on s

INTEGRABLE_CONST

⊢ ∀a b c. (λx. c) integrable_on interval [(a,b)]

INTEGRABLE_CONTINUOUS

⊢ ∀f a b. f continuous_on interval [(a,b)] ⇒ f integrable_on interval [(a,b)]

INTEGRABLE_DECREASING

⊢ ∀f a b.
    (∀x y i. x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒ f y ≤ f x) ⇒
    f integrable_on interval [(a,b)]

INTEGRABLE_DECREASING_PRODUCT

⊢ ∀f g a b.
    f integrable_on interval [(a,b)] ∧
    (∀x y. x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒ g y ≤ g x) ⇒
    (λx. g x * f x) integrable_on interval [(a,b)]

INTEGRABLE_DECREASING_PRODUCT_UNIV

⊢ ∀f g B.
    f integrable_on 𝕌(:real) ∧ (∀x y. x ≤ y ⇒ g y ≤ g x) ∧ (∀x. abs (g x) ≤ B) ⇒
    (λx. g x * f x) integrable_on 𝕌(:real)

INTEGRABLE_EQ

⊢ ∀f g s. (∀x. x ∈ s ⇒ (f x = g x)) ∧ f integrable_on s ⇒ g integrable_on s

INTEGRABLE_INCREASING

⊢ ∀f a b.
    (∀x y i. x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒ f x ≤ f y) ⇒
    f integrable_on interval [(a,b)]

INTEGRABLE_INCREASING_PRODUCT

⊢ ∀f g a b.
    f integrable_on interval [(a,b)] ∧
    (∀x y. x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒ g x ≤ g y) ⇒
    (λx. g x * f x) integrable_on interval [(a,b)]

INTEGRABLE_INCREASING_PRODUCT_UNIV

⊢ ∀f g B.
    f integrable_on 𝕌(:real) ∧ (∀x y. x ≤ y ⇒ g x ≤ g y) ∧ (∀x. abs (g x) ≤ B) ⇒
    (λx. g x * f x) integrable_on 𝕌(:real)

INTEGRABLE_INTEGRAL

⊢ ∀f i. f integrable_on i ⇒ (f has_integral ∫ i f) i

INTEGRABLE_LINEAR

⊢ ∀f h s. f integrable_on s ∧ linear h ⇒ h ∘ f integrable_on s

INTEGRABLE_MIN_CONST

⊢ ∀f s t.
    0 ≤ t ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ∧ (λx. f x) integrable_on s ⇒
    (λx. min (f x) t) integrable_on s

INTEGRABLE_NEG

⊢ ∀f s. f integrable_on s ⇒ (λx. -f x) integrable_on s

INTEGRABLE_ON_ALL_INTERVALS_INTEGRABLE_BOUND

⊢ ∀f g s.
    (∀a b. (λx. if x ∈ s then f x else 0) integrable_on interval [(a,b)]) ∧
    (∀x. x ∈ s ⇒ abs (f x) ≤ g x) ∧ g integrable_on s ⇒
    f integrable_on s

INTEGRABLE_ON_EMPTY

⊢ ∀f. f integrable_on ∅

INTEGRABLE_ON_LITTLE_SUBINTERVALS

⊢ ∀f a b.
    (∀x. x ∈ interval [(a,b)] ⇒
         ∃d. 0 < d ∧
             ∀u v.
               x ∈ interval [(u,v)] ∧ interval [(u,v)] ⊆ ball (x,d) ∧
               interval [(u,v)] ⊆ interval [(a,b)] ⇒
               f integrable_on interval [(u,v)]) ⇒
    f integrable_on interval [(a,b)]

INTEGRABLE_ON_NULL

⊢ ∀f a b. (content (interval [(a,b)]) = 0) ⇒ f integrable_on interval [(a,b)]

INTEGRABLE_ON_REFL

⊢ ∀f a. f integrable_on interval [(a,a)]

INTEGRABLE_ON_SUBDIVISION

⊢ ∀f s d i. d division_of i ∧ f integrable_on s ∧ i ⊆ s ⇒ f integrable_on i

INTEGRABLE_ON_SUBINTERVAL

⊢ ∀f s a b.
    f integrable_on s ∧ interval [(a,b)] ⊆ s ⇒
    f integrable_on interval [(a,b)]

INTEGRABLE_ON_SUPERSET

⊢ ∀f s t.
    (∀x. x ∉ s ⇒ (f x = 0)) ∧ s ⊆ t ∧ f integrable_on s ⇒ f integrable_on t

INTEGRABLE_REFLECT

⊢ ∀f a b.
    (λx. f (-x)) integrable_on interval [(-b,-a)] ⇔
    f integrable_on interval [(a,b)]

INTEGRABLE_REFLECT_GEN

⊢ ∀f s. (λx. f (-x)) integrable_on s ⇔ f integrable_on IMAGE (λx. -x) s

INTEGRABLE_RESTRICT

⊢ ∀f s t.
    s ⊆ t ⇒
    ((λx. if x ∈ s then f x else 0) integrable_on t ⇔ f integrable_on s)

INTEGRABLE_RESTRICT_INTER

⊢ ∀f s t.
    (λx. if x ∈ s then f x else 0) integrable_on t ⇔ f integrable_on s ∩ t

INTEGRABLE_RESTRICT_UNIV

⊢ ∀f s.
    (λx. if x ∈ s then f x else 0) integrable_on 𝕌(:real) ⇔ f integrable_on s

INTEGRABLE_SPIKE

⊢ ∀f g s t.
    negligible s ∧ (∀x. x ∈ t DIFF s ⇒ (g x = f x)) ⇒
    f integrable_on t ⇒
    g integrable_on t

INTEGRABLE_SPIKE_EQ

⊢ ∀f g s t.
    negligible s ∧ (∀x. x ∈ t DIFF s ⇒ (g x = f x)) ⇒
    (f integrable_on t ⇔ g integrable_on t)

INTEGRABLE_SPIKE_FINITE

⊢ ∀f g s.
    FINITE s ∧ (∀x. x ∈ t DIFF s ⇒ (g x = f x)) ⇒
    f integrable_on t ⇒
    g integrable_on t

INTEGRABLE_SPIKE_INTERIOR

⊢ ∀f g a b.
    (∀x. x ∈ interval (a,b) ⇒ (g x = f x)) ⇒
    f integrable_on interval [(a,b)] ⇒
    g integrable_on interval [(a,b)]

INTEGRABLE_SPIKE_SET

⊢ ∀f s t.
    negligible (s DIFF t ∪ (t DIFF s)) ⇒ f integrable_on s ⇒ f integrable_on t

INTEGRABLE_SPIKE_SET_EQ

⊢ ∀f s t.
    negligible (s DIFF t ∪ (t DIFF s)) ⇒
    (f integrable_on s ⇔ f integrable_on t)

INTEGRABLE_SPLIT

⊢ ∀f a b.
    f integrable_on interval [(a,b)] ⇒
    f integrable_on interval [(a,b)] ∩ {x | x ≤ c} ∧
    f integrable_on interval [(a,b)] ∩ {x | x ≥ c}

INTEGRABLE_STRADDLE

⊢ ∀f s.
    (∀e. 0 < e ⇒
         ∃g h i j.
           (g has_integral i) s ∧ (h has_integral j) s ∧ abs (i − j) < e ∧
           ∀x. x ∈ s ⇒ g x ≤ f x ∧ f x ≤ h x) ⇒
    f integrable_on s

INTEGRABLE_STRADDLE_INTERVAL

⊢ ∀f a b.
    (∀e. 0 < e ⇒
         ∃g h i j.
           (g has_integral i) (interval [(a,b)]) ∧
           (h has_integral j) (interval [(a,b)]) ∧ abs (i − j) < e ∧
           ∀x. x ∈ interval [(a,b)] ⇒ g x ≤ f x ∧ f x ≤ h x) ⇒
    f integrable_on interval [(a,b)]

INTEGRABLE_STRETCH

⊢ ∀f m a b.
    f integrable_on interval [(a,b)] ∧ m 1 ≠ 0 ⇒
    (λx. f (m 1 * x)) integrable_on IMAGE (λx. (m 1)⁻¹ * x) (interval [(a,b)])

INTEGRABLE_SUB

⊢ ∀f g s.
    f integrable_on s ∧ g integrable_on s ⇒ (λx. f x − g x) integrable_on s

INTEGRABLE_SUBINTERVAL

⊢ ∀f a b c d.
    f integrable_on interval [(a,b)] ∧ interval [(c,d)] ⊆ interval [(a,b)] ⇒
    f integrable_on interval [(c,d)]

INTEGRABLE_SUM

⊢ ∀f s t.
    FINITE t ∧ (∀a. a ∈ t ⇒ f a integrable_on s) ⇒
    (λx. sum t (λa. f a x)) integrable_on s

INTEGRABLE_UNIFORM_LIMIT

⊢ ∀f a b.
    (∀e. 0 < e ⇒
         ∃g. (∀x. x ∈ interval [(a,b)] ⇒ abs (f x − g x) ≤ e) ∧
             g integrable_on interval [(a,b)]) ⇒
    f integrable_on interval [(a,b)]

INTEGRAL_0

⊢ ∀s. ∫ s (λx. 0) = 0

INTEGRAL_ABS_BOUND_INTEGRAL

⊢ ∀f g s.
    f integrable_on s ∧ g integrable_on s ∧ (∀x. x ∈ s ⇒ abs (f x) ≤ g x) ⇒
    abs (∫ s f) ≤ ∫ s g

INTEGRAL_ABS_BOUND_INTEGRAL_AE

⊢ ∀f g s t.
    f integrable_on s ∧ g integrable_on s ∧ negligible t ∧
    (∀x. x ∈ s DIFF t ⇒ abs (f x) ≤ g x) ⇒
    abs (∫ s f) ≤ ∫ s g

INTEGRAL_ABS_BOUND_INTEGRAL_COMPONENT

⊢ ∀f g s.
    f integrable_on s ∧ g integrable_on s ∧ (∀x. x ∈ s ⇒ abs (f x) ≤ g x) ⇒
    abs (∫ s f) ≤ ∫ s g

INTEGRAL_ADD

⊢ ∀f g s.
    f integrable_on s ∧ g integrable_on s ⇒
    (∫ s (λx. f x + g x) = ∫ s f + ∫ s g)

INTEGRAL_CMUL

⊢ ∀f c s. f integrable_on s ⇒ (∫ s (λx. c * f x) = c * ∫ s f)

INTEGRAL_COMBINE

⊢ ∀f a b c.
    a ≤ c ∧ c ≤ b ∧ f integrable_on interval [(a,b)] ⇒
    (∫ (interval [(a,c)]) f + ∫ (interval [(c,b)]) f = ∫ (interval [(a,b)]) f)

INTEGRAL_COMBINE_DIVISION_BOTTOMUP

⊢ ∀f d s.
    d division_of s ∧ (∀k. k ∈ d ⇒ f integrable_on k) ⇒
    (∫ s f = sum d (λi. ∫ i f))

INTEGRAL_COMBINE_DIVISION_TOPDOWN

⊢ ∀f d s. f integrable_on s ∧ d division_of s ⇒ (∫ s f = sum d (λi. ∫ i f))

INTEGRAL_COMBINE_TAGGED_DIVISION_BOTTOMUP

⊢ ∀f p a b.
    p tagged_division_of interval [(a,b)] ∧
    (∀x k. (x,k) ∈ p ⇒ f integrable_on k) ⇒
    (∫ (interval [(a,b)]) f = sum p (λ(x,k). ∫ k f))

INTEGRAL_COMBINE_TAGGED_DIVISION_TOPDOWN

⊢ ∀f a b p.
    f integrable_on interval [(a,b)] ∧ p tagged_division_of interval [(a,b)] ⇒
    (∫ (interval [(a,b)]) f = sum p (λ(x,k). ∫ k f))

INTEGRAL_COMPONENT

⊢ ∀f s. f integrable_on s ⇒ (∫ s f = ∫ s (λx. f x))

INTEGRAL_COMPONENT_LBOUND

⊢ ∀f a b.
    f integrable_on interval [(a,b)] ∧ (∀x. x ∈ interval [(a,b)] ⇒ B ≤ f x) ⇒
    B * content (interval [(a,b)]) ≤ ∫ (interval [(a,b)]) f

INTEGRAL_COMPONENT_LE

⊢ ∀f g s.
    f integrable_on s ∧ g integrable_on s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒
    ∫ s f ≤ ∫ s g

INTEGRAL_COMPONENT_LE_AE

⊢ ∀f g s k t.
    negligible t ∧ f integrable_on s ∧ g integrable_on s ∧
    (∀x. x ∈ s DIFF t ⇒ f x ≤ g x) ⇒
    ∫ s f ≤ ∫ s g

INTEGRAL_COMPONENT_POS

⊢ ∀f s. f integrable_on s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ ∫ s f

INTEGRAL_COMPONENT_UBOUND

⊢ ∀f a b.
    f integrable_on interval [(a,b)] ∧ (∀x. x ∈ interval [(a,b)] ⇒ f x ≤ B) ⇒
    ∫ (interval [(a,b)]) f ≤ B * content (interval [(a,b)])

INTEGRAL_CONST

⊢ ∀a b c. ∫ (interval [(a,b)]) (λx. c) = content (interval [(a,b)]) * c

INTEGRAL_DIFF

⊢ ∀f s t.
    f integrable_on s ∧ f integrable_on t ∧ negligible (t DIFF s) ⇒
    (∫ (s DIFF t) f = ∫ s f − ∫ t f)

INTEGRAL_DROP_LE

⊢ ∀f g s.
    f integrable_on s ∧ g integrable_on s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒
    ∫ s f ≤ ∫ s g

INTEGRAL_DROP_POS

⊢ ∀f s. f integrable_on s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ ∫ s f

INTEGRAL_DROP_POS_AE

⊢ ∀f s t.
    f integrable_on s ∧ negligible t ∧ (∀x. x ∈ s DIFF t ⇒ 0 ≤ f x) ⇒
    0 ≤ ∫ s f

INTEGRAL_EMPTY

⊢ ∀f. ∫ ∅ f = 0

INTEGRAL_EQ

⊢ ∀f g s. (∀x. x ∈ s ⇒ (f x = g x)) ⇒ (∫ s f = ∫ s g)

INTEGRAL_EQ_0

⊢ ∀f s. (∀x. x ∈ s ⇒ (f x = 0)) ⇒ (∫ s f = 0)

INTEGRAL_EQ_HAS_INTEGRAL

⊢ ∀s f y. f integrable_on s ⇒ ((∫ s f = y) ⇔ (f has_integral y) s)

INTEGRAL_HAS_VECTOR_DERIVATIVE

⊢ ∀f a b.
    f continuous_on interval [(a,b)] ⇒
    ∀x. x ∈ interval [(a,b)] ⇒
        ((λu. ∫ (interval [(a,u)]) f) has_vector_derivative f x)
          (at x within interval [(a,b)])

INTEGRAL_HAS_VECTOR_DERIVATIVE_POINTWISE

⊢ ∀f a b x.
    f integrable_on interval [(a,b)] ∧ x ∈ interval [(a,b)] ∧
    f continuous (at x within interval [(a,b)]) ⇒
    ((λu. ∫ (interval [(a,u)]) f) has_vector_derivative f x)
      (at x within interval [(a,b)])

INTEGRAL_LE_AE

⊢ ∀f g s t.
    f integrable_on s ∧ g integrable_on s ∧ negligible t ∧
    (∀x. x ∈ s DIFF t ⇒ f x ≤ g x) ⇒
    ∫ s f ≤ ∫ s g

INTEGRAL_LINEAR

⊢ ∀f s h. f integrable_on s ∧ linear h ⇒ (∫ s (h ∘ f) = h (∫ s f))

INTEGRAL_NEG

⊢ ∀f s. f integrable_on s ⇒ (∫ s (λx. -f x) = -∫ s f)

INTEGRAL_NULL

⊢ ∀f a b. (content (interval [(a,b)]) = 0) ⇒ (∫ (interval [(a,b)]) f = 0)

INTEGRAL_REFL

⊢ ∀f a. ∫ (interval [(a,a)]) f = 0

INTEGRAL_REFLECT

⊢ ∀f a b. ∫ (interval [(-b,-a)]) (λx. f (-x)) = ∫ (interval [(a,b)]) f

INTEGRAL_REFLECT_GEN

⊢ ∀f s. ∫ s (λx. f (-x)) = ∫ (IMAGE (λx. -x) s) f

INTEGRAL_RESTRICT

⊢ ∀f s t. s ⊆ t ⇒ (∫ t (λx. if x ∈ s then f x else 0) = ∫ s f)

INTEGRAL_RESTRICT_INTER

⊢ ∀f s t. ∫ t (λx. if x ∈ s then f x else 0) = ∫ (s ∩ t) f

INTEGRAL_RESTRICT_UNIV

⊢ ∀f s. ∫ 𝕌(:real) (λx. if x ∈ s then f x else 0) = ∫ s f

INTEGRAL_SPIKE

⊢ ∀f g s t y.
    negligible s ∧ (∀x. x ∈ t DIFF s ⇒ (g x = f x)) ⇒ (∫ t f = ∫ t g)

INTEGRAL_SPIKE_SET

⊢ ∀f s t. negligible (s DIFF t ∪ (t DIFF s)) ⇒ (∫ s f = ∫ t f)

INTEGRAL_SPLIT

⊢ ∀f a b t.
    f integrable_on interval [(a,b)] ⇒
    (∫ (interval [(a,b)]) f =
     ∫ (interval [(a,@f. f = min b t)]) f +
     ∫ (interval [((@f. f = max a t),b)]) f)

INTEGRAL_SPLIT_SIGNED

⊢ ∀f a b t.
    a ≤ t ∧ a ≤ b ∧ f integrable_on interval [(a,@f. f = max b t)] ⇒
    (∫ (interval [(a,b)]) f =
     ∫ (interval [(a,@f. f = t)]) f +
     (if b < t then -1 else 1) *
     ∫ (interval [((@f. f = min b t),@f. f = max b t)]) f)

INTEGRAL_SUB

⊢ ∀f g k l s.
    f integrable_on s ∧ g integrable_on s ⇒
    (∫ s (λx. f x − g x) = ∫ s f − ∫ s g)

INTEGRAL_SUBSET_COMPONENT_LE

⊢ ∀f s t.
    s ⊆ t ∧ f integrable_on s ∧ f integrable_on t ∧ (∀x. x ∈ t ⇒ 0 ≤ f x) ⇒
    ∫ s f ≤ ∫ t f

INTEGRAL_SUBSET_DROP_LE

⊢ ∀f s t.
    s ⊆ t ∧ f integrable_on s ∧ f integrable_on t ∧ (∀x. x ∈ t ⇒ 0 ≤ f x) ⇒
    ∫ s f ≤ ∫ t f

INTEGRAL_SUM

⊢ ∀f s t.
    FINITE t ∧ (∀a. a ∈ t ⇒ f a integrable_on s) ⇒
    (∫ s (λx. sum t (λa. f a x)) = sum t (λa. ∫ s (f a)))

INTEGRAL_UNION

⊢ ∀f s t.
    f integrable_on s ∧ f integrable_on t ∧ negligible (s ∩ t) ⇒
    (∫ (s ∪ t) f = ∫ s f + ∫ t f)

INTEGRAL_UNIQUE

⊢ ∀f y k. (f has_integral y) k ⇒ (∫ k f = y)

INTEGRATION_BY_PARTS

⊢ ∀bop f g f' g' a b c y.
    bilinear bop ∧ a ≤ b ∧ COUNTABLE c ∧
    (λx. bop (f x) (g x)) continuous_on interval [(a,b)] ∧
    (∀x. x ∈ interval (a,b) DIFF c ⇒
         (f has_vector_derivative f' x) (at x) ∧
         (g has_vector_derivative g' x) (at x)) ∧
    ((λx. bop (f x) (g' x)) has_integral bop (f b) (g b) − bop (f a) (g a) − y)
      (interval [(a,b)]) ⇒
    ((λx. bop (f' x) (g x)) has_integral y) (interval [(a,b)])

INTEGRATION_BY_PARTS_SIMPLE

⊢ ∀bop f g f' g' a b y.
    bilinear bop ∧ a ≤ b ∧
    (∀x. x ∈ interval [(a,b)] ⇒
         (f has_vector_derivative f' x) (at x within interval [(a,b)]) ∧
         (g has_vector_derivative g' x) (at x within interval [(a,b)])) ∧
    ((λx. bop (f x) (g' x)) has_integral bop (f b) (g b) − bop (f a) (g a) − y)
      (interval [(a,b)]) ⇒
    ((λx. bop (f' x) (g x)) has_integral y) (interval [(a,b)])

INTERIOR_SUBSET_UNION_INTERVALS

⊢ ∀s i j.
    (∃a b. i = interval [(a,b)]) ∧ (∃c d. j = interval [(c,d)]) ∧
    interior j ≠ ∅ ∧ i ⊆ j ∪ s ∧ (interior i ∩ interior j = ∅) ⇒
    interior i ⊆ interior s

INTERVAL_BISECTION

⊢ ∀P. P ∅ ∧ (∀s t. P s ∧ P t ∧ (interior s ∩ interior t = ∅) ⇒ P (s ∪ t)) ⇒
      ∀a b.
        ¬P (interval [(a,b)]) ⇒
        ∃x. x ∈ interval [(a,b)] ∧
            ∀e. 0 < e ⇒
                ∃c d.
                  x ∈ interval [(c,d)] ∧ interval [(c,d)] ⊆ ball (x,e) ∧
                  interval [(c,d)] ⊆ interval [(a,b)] ∧ ¬P (interval [(c,d)])

INTERVAL_BISECTION_STEP

⊢ ∀P. P ∅ ∧ (∀s t. P s ∧ P t ∧ (interior s ∩ interior t = ∅) ⇒ P (s ∪ t)) ⇒
      ∀a b.
        ¬P (interval [(a,b)]) ⇒
        ∃c d.
          ¬P (interval [(c,d)]) ∧ a ≤ c ∧ c ≤ d ∧ d ≤ b ∧ 2 * (d − c) ≤ b − a

INTERVAL_BOUNDS_EMPTY

⊢ interval_upperbound ∅ = interval_lowerbound ∅

INTERVAL_BOUNDS_NULL

⊢ ∀a b.
    (content (interval [(a,b)]) = 0) ⇒
    (interval_upperbound (interval [(a,b)]) =
     interval_lowerbound (interval [(a,b)]))

INTERVAL_DOUBLESPLIT

⊢ ∀e a b c.
    interval [(a,b)] ∩ {x | abs (x − c) ≤ e} =
    interval [(max a (c − e),min b (c + e))]

INTERVAL_IMAGE_AFFINITY_INTERVAL

⊢ ∀a b m c. ∃u v. IMAGE (λx. m * x + c) (interval [(a,b)]) = interval [(u,v)]

INTERVAL_LOWERBOUND

⊢ ∀a b. a ≤ b ⇒ (interval_lowerbound (interval [(a,b)]) = a)

INTERVAL_LOWERBOUND_NONEMPTY

⊢ ∀a b. interval [(a,b)] ≠ ∅ ⇒ (interval_lowerbound (interval [(a,b)]) = a)

INTERVAL_SPLIT

⊢ ∀a b c.
    (interval [(a,b)] ∩ {x | x ≤ c} = interval [(a,min b c)]) ∧
    (interval [(a,b)] ∩ {x | x ≥ c} = interval [(max a c,b)])

INTERVAL_SUBDIVISION

⊢ ∀a b c.
    c ∈ interval [(a,b)] ⇒
    IMAGE
      (λs.
           interval
             [((@f. f = if 1 ∈ s then c else a),@f. f = if 1 ∈ s then b else c)])
      {s | s ⊆ (1 .. 1)} division_of interval [(a,b)]

INTERVAL_UPPERBOUND

⊢ ∀a b. a ≤ b ⇒ (interval_upperbound (interval [(a,b)]) = b)

INTERVAL_UPPERBOUND_NONEMPTY

⊢ ∀a b. interval [(a,b)] ≠ ∅ ⇒ (interval_upperbound (interval [(a,b)]) = b)

INTER_INTERIOR_BIGUNION_INTERVALS

⊢ ∀s f.
    FINITE f ∧ open s ∧ (∀t. t ∈ f ⇒ ∃a b. t = interval [(a,b)]) ∧
    (∀t. t ∈ f ⇒ (s ∩ interior t = ∅)) ⇒
    (s ∩ interior (BIGUNION f) = ∅)

ITERATE_AND

⊢ ∀p s. FINITE s ⇒ (iterate $/\ s p ⇔ ∀x. x ∈ s ⇒ p x)

ITERATE_NONZERO_IMAGE_LEMMA

⊢ ∀op s f g a.
    monoidal op ∧ FINITE s ∧ (g a = neutral op) ∧
    (∀x y. x ∈ s ∧ y ∈ s ∧ (f x = f y) ∧ x ≠ y ⇒ (g (f x) = neutral op)) ⇒
    (iterate op {f x | x | x ∈ s ∧ f x ≠ a} g = iterate op s (g ∘ f))

ITERATE_SOME

⊢ ∀op.
    monoidal op ⇒
    ∀f s.
      FINITE s ⇒
      (iterate (lifted op) s (λx. SOME (f x)) = SOME (iterate op s f))

MONOIDAL_AND

⊢ monoidal $/\

MONOIDAL_LIFTED

⊢ ∀op. monoidal op ⇒ monoidal (lifted op)

MONOTONE_CONVERGENCE_DECREASING

⊢ ∀f g s.
    (∀k. f k integrable_on s) ∧ (∀k x. x ∈ s ⇒ f (SUC k) x ≤ f k x) ∧
    (∀x. x ∈ s ⇒ ((λk. f k x) ⟶ g x) sequentially) ∧
    bounded {∫ s (f k) | k ∈ 𝕌(:num)} ⇒
    g integrable_on s ∧ ((λk. ∫ s (f k)) ⟶ ∫ s g) sequentially

MONOTONE_CONVERGENCE_DECREASING_AE

⊢ ∀f g s t.
    (∀k. f k integrable_on s) ∧ negligible t ∧
    (∀k x. x ∈ s DIFF t ⇒ f (SUC k) x ≤ f k x) ∧
    (∀x. x ∈ s DIFF t ⇒ ((λk. f k x) ⟶ g x) sequentially) ∧
    bounded {∫ s (f k) | k ∈ 𝕌(:num)} ⇒
    g integrable_on s ∧ ((λk. ∫ s (f k)) ⟶ ∫ s g) sequentially

MONOTONE_CONVERGENCE_INCREASING

⊢ ∀f g s.
    (∀k. f k integrable_on s) ∧ (∀k x. x ∈ s ⇒ f k x ≤ f (SUC k) x) ∧
    (∀x. x ∈ s ⇒ ((λk. f k x) ⟶ g x) sequentially) ∧
    bounded {∫ s (f k) | k ∈ 𝕌(:num)} ⇒
    g integrable_on s ∧ ((λk. ∫ s (f k)) ⟶ ∫ s g) sequentially

MONOTONE_CONVERGENCE_INCREASING_AE

⊢ ∀f g s t.
    (∀k. f k integrable_on s) ∧ negligible t ∧
    (∀k x. x ∈ s DIFF t ⇒ f k x ≤ f (SUC k) x) ∧
    (∀x. x ∈ s DIFF t ⇒ ((λk. f k x) ⟶ g x) sequentially) ∧
    bounded {∫ s (f k) | k ∈ 𝕌(:num)} ⇒
    g integrable_on s ∧ ((λk. ∫ s (f k)) ⟶ ∫ s g) sequentially

MONOTONE_CONVERGENCE_INTERVAL

⊢ ∀f g a b.
    (∀k. f k integrable_on interval [(a,b)]) ∧
    (∀k x. x ∈ interval [(a,b)] ⇒ f k x ≤ f (SUC k) x) ∧
    (∀x. x ∈ interval [(a,b)] ⇒ ((λk. f k x) ⟶ g x) sequentially) ∧
    bounded {∫ (interval [(a,b)]) (f k) | k ∈ 𝕌(:num)} ⇒
    g integrable_on interval [(a,b)] ∧
    ((λk. ∫ (interval [(a,b)]) (f k)) ⟶ ∫ (interval [(a,b)]) g) sequentially

NEGLIGIBLE

⊢ ∀s. negligible s ⇔ ∀t. (indicator s has_integral 0) t

NEGLIGIBLE_BIGUNION

⊢ ∀s. FINITE s ∧ (∀t. t ∈ s ⇒ negligible t) ⇒ negligible (BIGUNION s)

NEGLIGIBLE_BOUNDED_SUBSETS

⊢ ∀s. negligible s ⇔ ∀t. bounded t ∧ t ⊆ s ⇒ negligible t

NEGLIGIBLE_COUNTABLE

⊢ ∀s. COUNTABLE s ⇒ negligible s

NEGLIGIBLE_COUNTABLE_BIGUNION

⊢ ∀s. (∀n. negligible (s n)) ⇒ negligible (BIGUNION {s n | n ∈ 𝕌(:num)})

NEGLIGIBLE_DIFF

⊢ ∀s t. negligible s ⇒ negligible (s DIFF t)

NEGLIGIBLE_EMPTY

⊢ negligible ∅

NEGLIGIBLE_FINITE

⊢ ∀s. FINITE s ⇒ negligible s

NEGLIGIBLE_FRONTIER_INTERVAL

⊢ ∀a b. negligible (interval [(a,b)] DIFF interval (a,b))

NEGLIGIBLE_INSERT

⊢ ∀a s. negligible (a INSERT s) ⇔ negligible s

NEGLIGIBLE_INTER

⊢ ∀s t. negligible s ∨ negligible t ⇒ negligible (s ∩ t)

NEGLIGIBLE_ON_COUNTABLE_INTERVALS

⊢ ∀s. negligible s ⇔ ∀n. negligible (s ∩ interval [(-n,n)])

NEGLIGIBLE_ON_INTERVALS

⊢ ∀s. negligible s ⇔ ∀a b. negligible (s ∩ interval [(a,b)])

NEGLIGIBLE_ON_UNIV

⊢ ∀s. negligible s ⇔ (indicator s has_integral 0) 𝕌(:real)

NEGLIGIBLE_SING

⊢ ∀a. negligible {a}

NEGLIGIBLE_STANDARD_HYPERPLANE

⊢ ∀c. negligible {x | x = c}

NEGLIGIBLE_SUBSET

⊢ ∀s t. negligible s ∧ t ⊆ s ⇒ negligible t

NEGLIGIBLE_UNION

⊢ ∀s t. negligible s ∧ negligible t ⇒ negligible (s ∪ t)

NEGLIGIBLE_UNION_EQ

⊢ ∀s t. negligible (s ∪ t) ⇔ negligible s ∧ negligible t

NEUTRAL_AND

⊢ neutral $/\ ⇔ T

NEUTRAL_LIFTED

⊢ ∀op. monoidal op ⇒ (neutral (lifted op) = SOME (neutral op))

NONNEGATIVE_ABSOLUTELY_INTEGRABLE

⊢ ∀f s.
    (∀x i. x ∈ s ⇒ 0 ≤ f x) ∧ f integrable_on s ⇒ f absolutely_integrable_on s

NONNEGATIVE_ABSOLUTELY_INTEGRABLE_AE

⊢ ∀f s t.
    negligible t ∧ (∀x i. x ∈ s DIFF t ⇒ 0 ≤ f x) ∧ f integrable_on s ⇒
    f absolutely_integrable_on s

OPEN_INTERVAL_LOWERBOUND

⊢ ∀a b. a < b ⇒ (interval_lowerbound (interval (a,b)) = a)

OPEN_INTERVAL_UPPERBOUND

⊢ ∀a b. a < b ⇒ (interval_upperbound (interval (a,b)) = b)

OPERATIVE_1_LE

⊢ ∀op.
    monoidal op ⇒
    ∀f. operative op f ⇔
        (∀a b. b ≤ a ⇒ (f (interval [(a,b)]) = neutral op)) ∧
        ∀a b c.
          a ≤ c ∧ c ≤ b ⇒
          (op (f (interval [(a,c)])) (f (interval [(c,b)])) =
           f (interval [(a,b)]))

OPERATIVE_1_LT

⊢ ∀op.
    monoidal op ⇒
    ∀f. operative op f ⇔
        (∀a b. b ≤ a ⇒ (f (interval [(a,b)]) = neutral op)) ∧
        ∀a b c.
          a < c ∧ c < b ⇒
          (op (f (interval [(a,c)])) (f (interval [(c,b)])) =
           f (interval [(a,b)]))

OPERATIVE_APPROXIMABLE

⊢ ∀f e.
    0 ≤ e ⇒
    operative $/\
      (λi. ∃g. (∀x. x ∈ i ⇒ abs (f x − g x) ≤ e) ∧ g integrable_on i)

OPERATIVE_CONTENT

⊢ operative $+ content

OPERATIVE_DIVISION

⊢ ∀op d a b f.
    monoidal op ∧ operative op f ∧ d division_of interval [(a,b)] ⇒
    (iterate op d f = f (interval [(a,b)]))

OPERATIVE_DIVISION_AND

⊢ ∀P d a b.
    operative $/\ P ∧ d division_of interval [(a,b)] ⇒
    ((∀i. i ∈ d ⇒ P i) ⇔ P (interval [(a,b)]))

OPERATIVE_EMPTY

⊢ ∀op f. operative op f ⇒ (f ∅ = neutral op)

OPERATIVE_FUNCTION_ENDPOINT_DIFF

⊢ ∀f. operative $+ (λk. f (interval_upperbound k) − f (interval_lowerbound k))

OPERATIVE_INTEGRABLE

⊢ ∀f. operative $/\ (λi. f integrable_on i)

OPERATIVE_INTEGRAL

⊢ ∀f. operative (lifted $+)
        (λi. if f integrable_on i then SOME (∫ i f) else NONE)

OPERATIVE_LIFTED_SETVARIATION

⊢ ∀f. operative $+ f ⇒
      operative (lifted $+)
        (λi.
             if f has_bounded_setvariation_on i then SOME (set_variation i f)
             else NONE)

OPERATIVE_LIFTED_VECTOR_VARIATION

⊢ ∀f. operative (lifted $+)
        (λi.
             if f has_bounded_variation_on i then SOME (vector_variation i f)
             else NONE)

OPERATIVE_REAL_FUNCTION_ENDPOINT_DIFF

⊢ ∀f. operative $+ (λk. f (interval_upperbound k) − f (interval_lowerbound k))

OPERATIVE_TAGGED_DIVISION

⊢ ∀op d a b f.
    monoidal op ∧ operative op f ∧ d tagged_division_of interval [(a,b)] ⇒
    (iterate op d (λ(x,l). f l) = f (interval [(a,b)]))

OPERATIVE_TRIVIAL

⊢ ∀op f a b.
    operative op f ∧ (content (interval [(a,b)]) = 0) ⇒
    (f (interval [(a,b)]) = neutral op)

PARTIAL_DIVISION_EXTEND

⊢ ∀p q s t.
    p division_of s ∧ q division_of t ∧ s ⊆ t ⇒ ∃r. p ⊆ r ∧ r division_of t

PARTIAL_DIVISION_EXTEND_1

⊢ ∀a b c d.
    interval [(c,d)] ⊆ interval [(a,b)] ∧ interval [(c,d)] ≠ ∅ ⇒
    ∃p. p division_of interval [(a,b)] ∧ interval [(c,d)] ∈ p

PARTIAL_DIVISION_EXTEND_INTERVAL

⊢ ∀p a b.
    p division_of BIGUNION p ∧ BIGUNION p ⊆ interval [(a,b)] ⇒
    ∃q. p ⊆ q ∧ q division_of interval [(a,b)]

PARTIAL_DIVISION_OF_TAGGED_DIVISION

⊢ ∀s i.
    s tagged_partial_division_of i ⇒
    IMAGE SND s division_of BIGUNION (IMAGE SND s)

PROPERTY_EMPTY_INTERVAL

⊢ ∀P. (∀a b. (content (interval [(a,b)]) = 0) ⇒ P (interval [(a,b)])) ⇒ P ∅

REAL_MUL_POS_LT

⊢ ∀x y. 0 < x * y ⇔ 0 < x ∧ 0 < y ∨ x < 0 ∧ y < 0

REAL_SUP_LE_FINITE

⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (sup s ≤ a ⇔ ∀x. x ∈ s ⇒ x ≤ a)

RSUM_BOUND

⊢ ∀p a b f e.
    p tagged_division_of interval [(a,b)] ∧
    (∀x. x ∈ interval [(a,b)] ⇒ abs (f x) ≤ e) ⇒
    abs (sum p (λ(x,k). content k * f x)) ≤ e * content (interval [(a,b)])

RSUM_COMPONENT_LE

⊢ ∀p a b f g.
    p tagged_division_of interval [(a,b)] ∧
    (∀x. x ∈ interval [(a,b)] ⇒ f x ≤ g x) ⇒
    sum p (λ(x,k). content k * f x) ≤ sum p (λ(x,k). content k * g x)

RSUM_DIFF_BOUND

⊢ ∀e p a b f g.
    p tagged_division_of interval [(a,b)] ∧
    (∀x. x ∈ interval [(a,b)] ⇒ abs (f x − g x) ≤ e) ⇒
    abs (sum p (λ(x,k). content k * f x) − sum p (λ(x,k). content k * g x)) ≤
    e * content (interval [(a,b)])

SECOND_MEAN_VALUE_THEOREM

⊢ ∀f g a b.
    interval [(a,b)] ≠ ∅ ∧ f integrable_on interval [(a,b)] ∧
    (∀x y. x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒ g x ≤ g y) ⇒
    ∃c. c ∈ interval [(a,b)] ∧
        (∫ (interval [(a,b)]) (λx. g x * f x) =
         g a * ∫ (interval [(a,c)]) f + g b * ∫ (interval [(c,b)]) f)

SECOND_MEAN_VALUE_THEOREM_BONNET

⊢ ∀f g a b.
    interval [(a,b)] ≠ ∅ ∧ f integrable_on interval [(a,b)] ∧
    (∀x. x ∈ interval [(a,b)] ⇒ 0 ≤ g x) ∧
    (∀x y. x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒ g x ≤ g y) ⇒
    ∃c. c ∈ interval [(a,b)] ∧
        (∫ (interval [(a,b)]) (λx. g x * f x) = g b * ∫ (interval [(c,b)]) f)

SECOND_MEAN_VALUE_THEOREM_BONNET_FULL

⊢ ∀f g a b.
    interval [(a,b)] ≠ ∅ ∧ f integrable_on interval [(a,b)] ∧
    (∀x. x ∈ interval [(a,b)] ⇒ 0 ≤ g x) ∧
    (∀x y. x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒ g x ≤ g y) ⇒
    ∃c. c ∈ interval [(a,b)] ∧
        ((λx. g x * f x) has_integral g b * ∫ (interval [(c,b)]) f)
          (interval [(a,b)])

SECOND_MEAN_VALUE_THEOREM_FULL

⊢ ∀f g a b.
    interval [(a,b)] ≠ ∅ ∧ f integrable_on interval [(a,b)] ∧
    (∀x y. x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒ g x ≤ g y) ⇒
    ∃c. c ∈ interval [(a,b)] ∧
        ((λx. g x * f x) has_integral
         g a * ∫ (interval [(a,c)]) f + g b * ∫ (interval [(c,b)]) f)
          (interval [(a,b)])

SECOND_MEAN_VALUE_THEOREM_GEN

⊢ ∀f g a b u v.
    interval [(a,b)] ≠ ∅ ∧ f integrable_on interval [(a,b)] ∧
    (∀x. x ∈ interval (a,b) ⇒ u ≤ g x ∧ g x ≤ v) ∧
    (∀x y. x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒ g x ≤ g y) ⇒
    ∃c. c ∈ interval [(a,b)] ∧
        (∫ (interval [(a,b)]) (λx. g x * f x) =
         u * ∫ (interval [(a,c)]) f + v * ∫ (interval [(c,b)]) f)

SECOND_MEAN_VALUE_THEOREM_GEN_FULL

⊢ ∀f g a b u v.
    interval [(a,b)] ≠ ∅ ∧ f integrable_on interval [(a,b)] ∧
    (∀x. x ∈ interval (a,b) ⇒ u ≤ g x ∧ g x ≤ v) ∧
    (∀x y. x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒ g x ≤ g y) ⇒
    ∃c. c ∈ interval [(a,b)] ∧
        ((λx. g x * f x) has_integral
         u * ∫ (interval [(a,c)]) f + v * ∫ (interval [(c,b)]) f)
          (interval [(a,b)])

SETVARIATION_EQUAL_LEMMA

⊢ ∀mf ms ms'.
    (∀s. (ms' (ms s) = s) ∧ (ms (ms' s) = s)) ∧
    (∀f a b.
       interval [(a,b)] ≠ ∅ ⇒
       (mf f (ms (interval [(a,b)])) = f (interval [(a,b)])) ∧
       ∃a' b'.
         interval [(a',b')] ≠ ∅ ∧
         (ms' (interval [(a,b)]) = interval [(a',b')])) ∧
    (∀t u. t ⊆ u ⇒ ms t ⊆ ms u ∧ ms' t ⊆ ms' u) ∧
    (∀d t.
       d division_of t ⇒
       IMAGE ms d division_of ms t ∧ IMAGE ms' d division_of ms' t) ⇒
    (∀f s.
       mf f has_bounded_setvariation_on ms s ⇔ f has_bounded_setvariation_on s) ∧
    ∀f s. set_variation (ms s) (mf f) = set_variation s f

SET_VARIATION

⊢ ∀f s d t.
    f has_bounded_setvariation_on s ∧ d division_of t ∧ t ⊆ s ⇒
    sum d (λk. abs (f k)) ≤ set_variation s f

SET_VARIATION_0

⊢ ∀s. set_variation s (λx. 0) = 0

SET_VARIATION_COMPARISON

⊢ ∀f g s.
    f has_bounded_setvariation_on s ∧
    (∀a b.
       interval [(a,b)] ≠ ∅ ∧ interval [(a,b)] ⊆ s ⇒
       abs (g (interval [(a,b)])) ≤ abs (f (interval [(a,b)]))) ⇒
    set_variation s g ≤ set_variation s f

SET_VARIATION_ELEMENTARY_LEMMA

⊢ ∀f s b.
    (∃d. d division_of s) ⇒
    ((∀d t. d division_of t ∧ t ⊆ s ⇒ sum d (λk. abs (f k)) ≤ b) ⇔
     ∀d. d division_of s ⇒ sum d (λk. abs (f k)) ≤ b)

SET_VARIATION_EQ

⊢ ∀f g s.
    (∀a b.
       interval [(a,b)] ≠ ∅ ∧ interval [(a,b)] ⊆ s ⇒
       (f (interval [(a,b)]) = g (interval [(a,b)]))) ⇒
    (set_variation s f = set_variation s g)

SET_VARIATION_GE_FUNCTION

⊢ ∀f s a b.
    f has_bounded_setvariation_on s ∧ interval [(a,b)] ⊆ s ∧
    interval [(a,b)] ≠ ∅ ⇒
    abs (f (interval [(a,b)])) ≤ set_variation s f

SET_VARIATION_LBOUND

⊢ ∀f s B.
    f has_bounded_setvariation_on s ∧
    (∃d t. d division_of t ∧ t ⊆ s ∧ B ≤ sum d (λk. abs (f k))) ⇒
    B ≤ set_variation s f

SET_VARIATION_LBOUND_ON_INTERVAL

⊢ ∀f a b B.
    f has_bounded_setvariation_on interval [(a,b)] ∧
    (∃d. d division_of interval [(a,b)] ∧ B ≤ sum d (λk. abs (f k))) ⇒
    B ≤ set_variation (interval [(a,b)]) f

SET_VARIATION_MONOTONE

⊢ ∀f s t.
    f has_bounded_setvariation_on s ∧ t ⊆ s ⇒
    set_variation t f ≤ set_variation s f

SET_VARIATION_ON_DIVISION

⊢ ∀f a b d.
    operative $+ f ∧ d division_of interval [(a,b)] ∧
    f has_bounded_setvariation_on interval [(a,b)] ⇒
    (sum d (λk. set_variation k f) = set_variation (interval [(a,b)]) f)

SET_VARIATION_ON_ELEMENTARY

⊢ ∀f s.
    (∃d. d division_of s) ⇒
    (set_variation s f = sup {sum d (λk. abs (f k)) | d division_of s})

SET_VARIATION_ON_INTERVAL

⊢ ∀f a b.
    set_variation (interval [(a,b)]) f =
    sup {sum d (λk. abs (f k)) | d division_of interval [(a,b)]}

SET_VARIATION_ON_NULL

⊢ ∀f s.
    (∀a b. (content (interval [(a,b)]) = 0) ⇒ (f (interval [(a,b)]) = 0)) ∧
    (content s = 0) ∧ bounded s ⇒
    (set_variation s f = 0)

SET_VARIATION_POS_LE

⊢ ∀f s. f has_bounded_setvariation_on s ⇒ 0 ≤ set_variation s f

SET_VARIATION_REFLECT2

⊢ ∀f s.
    set_variation (IMAGE (λx. -x) s) (λk. f (IMAGE (λx. -x) k)) =
    set_variation s f

SET_VARIATION_SUM_LE

⊢ ∀f s k.
    FINITE k ∧ (∀i. i ∈ k ⇒ f i has_bounded_setvariation_on s) ⇒
    set_variation s (λx. sum k (λi. f i x)) ≤
    sum k (λi. set_variation s (f i))

SET_VARIATION_TRANSLATION2

⊢ ∀a f s.
    set_variation (IMAGE (λx. -a + x) s) (λk. f (IMAGE (λx. a + x) k)) =
    set_variation s f

SET_VARIATION_TRIANGLE

⊢ ∀f g s.
    f has_bounded_setvariation_on s ∧ g has_bounded_setvariation_on s ⇒
    set_variation s (λx. f x + g x) ≤ set_variation s f + set_variation s g

SET_VARIATION_UBOUND

⊢ ∀f s B.
    f has_bounded_setvariation_on s ∧
    (∀d t. d division_of t ∧ t ⊆ s ⇒ sum d (λk. abs (f k)) ≤ B) ⇒
    set_variation s f ≤ B

SET_VARIATION_UBOUND_ON_INTERVAL

⊢ ∀f a b B.
    f has_bounded_setvariation_on interval [(a,b)] ∧
    (∀d. d division_of interval [(a,b)] ⇒ sum d (λk. abs (f k)) ≤ B) ⇒
    set_variation (interval [(a,b)]) f ≤ B

SET_VARIATION_WORKS_ON_INTERVAL

⊢ ∀f a b d.
    f has_bounded_setvariation_on interval [(a,b)] ∧
    d division_of interval [(a,b)] ⇒
    sum d (λk. abs (f k)) ≤ set_variation (interval [(a,b)]) f

SUBADDITIVE_CONTENT_DIVISION

⊢ ∀d s a b.
    d division_of s ∧ s ⊆ interval [(a,b)] ⇒
    sum d content ≤ content (interval [(a,b)])

SUM_ABS_ALLSUBSETS_BOUND

⊢ ∀f p e.
    FINITE p ∧ (∀q. q ⊆ p ⇒ abs (sum q f) ≤ e) ⇒
    sum p (λx. abs (f x)) ≤ 2 * 1 * e

SUM_CONTENT_AREA_OVER_THIN_DIVISION

⊢ ∀d a b s c.
    d division_of s ∧ s ⊆ interval [(a,b)] ∧ a ≤ c ∧ c ≤ b ∧
    (∀k. k ∈ d ⇒ k ∩ {x | x = c} ≠ ∅) ⇒
    (b − a) *
    sum d (λk. content k / (interval_upperbound k − interval_lowerbound k)) ≤
    2 * content (interval [(a,b)])

SUM_CONTENT_NULL

⊢ ∀f a b p.
    (content (interval [(a,b)]) = 0) ∧ p tagged_division_of interval [(a,b)] ⇒
    (sum p (λ(x,k). content k * f x) = 0)

SUM_NONZERO_IMAGE_LEMMA

⊢ ∀s f g a.
    FINITE s ∧ (g a = 0) ∧
    (∀x y. x ∈ s ∧ y ∈ s ∧ (f x = f y) ∧ x ≠ y ⇒ (g (f x) = 0)) ⇒
    (sum {f x | x | x ∈ s ∧ f x ≠ a} g = sum s (g ∘ f))

SUM_OVER_TAGGED_DIVISION_LEMMA

⊢ ∀d p i.
    p tagged_division_of i ∧
    (∀u v.
       interval [(u,v)] ≠ ∅ ∧ (content (interval [(u,v)]) = 0) ⇒
       (d (interval [(u,v)]) = 0)) ⇒
    (sum p (λ(x,k). d k) = sum (IMAGE SND p) d)

SUM_OVER_TAGGED_PARTIAL_DIVISION_LEMMA

⊢ ∀d p i.
    p tagged_partial_division_of i ∧
    (∀u v.
       interval [(u,v)] ≠ ∅ ∧ (content (interval [(u,v)]) = 0) ⇒
       (d (interval [(u,v)]) = 0)) ⇒
    (sum p (λ(x,k). d k) = sum (IMAGE SND p) d)

SUP_FINITE

⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ sup s ∈ s ∧ ∀x. x ∈ s ⇒ x ≤ sup s

SUP_FINITE_LEMMA

⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ∃b. b ∈ s ∧ ∀x. x ∈ s ⇒ x ≤ b

TAGGED_DIVISION_BIGUNION

⊢ ∀iset pfn.
    FINITE iset ∧ (∀i. i ∈ iset ⇒ pfn i tagged_division_of i) ∧
    (∀i1 i2. i1 ∈ iset ∧ i2 ∈ iset ∧ i1 ≠ i2 ⇒ (interior i1 ∩ interior i2 = ∅)) ⇒
    BIGUNION (IMAGE pfn iset) tagged_division_of BIGUNION iset

TAGGED_DIVISION_BIGUNION_EXISTS

⊢ ∀d iset i.
    FINITE iset ∧ (∀i. i ∈ iset ⇒ ∃p. p tagged_division_of i ∧ d FINE p) ∧
    (∀i1 i2. i1 ∈ iset ∧ i2 ∈ iset ∧ i1 ≠ i2 ⇒ (interior i1 ∩ interior i2 = ∅)) ∧
    (BIGUNION iset = i) ⇒
    ∃p. p tagged_division_of i ∧ d FINE p

TAGGED_DIVISION_FINER

⊢ ∀p a b d.
    p tagged_division_of interval [(a,b)] ∧ gauge d ⇒
    ∃q. q tagged_division_of interval [(a,b)] ∧ d FINE q ∧
        ∀x k. (x,k) ∈ p ∧ k ⊆ d x ⇒ (x,k) ∈ q

TAGGED_DIVISION_OF

⊢ ∀s i.
    s tagged_division_of i ⇔
    FINITE s ∧
    (∀x k. (x,k) ∈ s ⇒ x ∈ k ∧ k ⊆ i ∧ ∃a b. k = interval [(a,b)]) ∧
    (∀x1 k1 x2 k2.
       (x1,k1) ∈ s ∧ (x2,k2) ∈ s ∧ (x1,k1) ≠ (x2,k2) ⇒
       (interior k1 ∩ interior k2 = ∅)) ∧ (BIGUNION {k | (∃x. (x,k) ∈ s)} = i)

TAGGED_DIVISION_OF_ALT

⊢ ∀p s.
    p tagged_division_of s ⇔
    p tagged_partial_division_of s ∧ ∀x. x ∈ s ⇒ ∃t k. (t,k) ∈ p ∧ x ∈ k

TAGGED_DIVISION_OF_ANOTHER

⊢ ∀p s s'.
    p tagged_partial_division_of s' ∧ (∀t k. (t,k) ∈ p ⇒ k ⊆ s) ∧
    (∀x. x ∈ s ⇒ ∃t k. (t,k) ∈ p ∧ x ∈ k) ⇒
    p tagged_division_of s

TAGGED_DIVISION_OF_EMPTY

⊢ ∅ tagged_division_of ∅

TAGGED_DIVISION_OF_FINITE

⊢ ∀s i. s tagged_division_of i ⇒ FINITE s

TAGGED_DIVISION_OF_NONTRIVIAL

⊢ ∀s a b.
    s tagged_division_of interval [(a,b)] ∧ content (interval [(a,b)]) ≠ 0 ⇒
    {(x,k) | (x,k) ∈ s ∧ content k ≠ 0} tagged_division_of interval [(a,b)]

TAGGED_DIVISION_OF_SELF

⊢ ∀x a b.
    x ∈ interval [(a,b)] ⇒
    {(x,interval [(a,b)])} tagged_division_of interval [(a,b)]

TAGGED_DIVISION_OF_TRIVIAL

⊢ ∀p. p tagged_division_of ∅ ⇔ (p = ∅)

TAGGED_DIVISION_OF_UNION_SELF

⊢ ∀p s. p tagged_division_of s ⇒ p tagged_division_of BIGUNION (IMAGE SND p)

TAGGED_DIVISION_SPLIT_LEFT_INJ

⊢ ∀d i x1 k1 x2 k2 c.
    d tagged_division_of i ∧ (x1,k1) ∈ d ∧ (x2,k2) ∈ d ∧ k1 ≠ k2 ∧
    (k1 ∩ {x | x ≤ c} = k2 ∩ {x | x ≤ c}) ⇒
    (content (k1 ∩ {x | x ≤ c}) = 0)

TAGGED_DIVISION_SPLIT_RIGHT_INJ

⊢ ∀d i x1 k1 x2 k2 c.
    d tagged_division_of i ∧ (x1,k1) ∈ d ∧ (x2,k2) ∈ d ∧ k1 ≠ k2 ∧
    (k1 ∩ {x | x ≥ c} = k2 ∩ {x | x ≥ c}) ⇒
    (content (k1 ∩ {x | x ≥ c}) = 0)

TAGGED_DIVISION_UNION

⊢ ∀s1 s2 p1 p2.
    p1 tagged_division_of s1 ∧ p2 tagged_division_of s2 ∧
    (interior s1 ∩ interior s2 = ∅) ⇒
    p1 ∪ p2 tagged_division_of s1 ∪ s2

TAGGED_DIVISION_UNION_IMAGE_SND

⊢ ∀p s. p tagged_division_of s ⇒ (s = BIGUNION (IMAGE SND p))

TAGGED_DIVISION_UNION_INTERVAL

⊢ ∀a b p1 p2 c.
    p1 tagged_division_of interval [(a,b)] ∩ {x | x ≤ c} ∧
    p2 tagged_division_of interval [(a,b)] ∩ {x | x ≥ c} ⇒
    p1 ∪ p2 tagged_division_of interval [(a,b)]

TAGGED_PARTIAL_DIVISION_COMMON_POINT_BOUND

⊢ ∀p s y.
    p tagged_partial_division_of s ⇒
    CARD {(x,k) | (x,k) ∈ p ∧ y ∈ k ∧ content k ≠ 0} ≤ 2 ** 1

TAGGED_PARTIAL_DIVISION_COMMON_TAGS

⊢ ∀p s x.
    p tagged_partial_division_of s ⇒
    CARD {(x,k) | k | (x,k) ∈ p ∧ content k ≠ 0} ≤ 2 ** 1

TAGGED_PARTIAL_DIVISION_OF_SUBSET

⊢ ∀p s t.
    p tagged_partial_division_of s ∧ s ⊆ t ⇒ p tagged_partial_division_of t

TAGGED_PARTIAL_DIVISION_OF_TRIVIAL

⊢ ∀p. p tagged_partial_division_of ∅ ⇔ (p = ∅)

TAGGED_PARTIAL_DIVISION_OF_UNION_SELF

⊢ ∀p s.
    p tagged_partial_division_of s ⇒
    p tagged_division_of BIGUNION (IMAGE SND p)

TAGGED_PARTIAL_DIVISION_SUBSET

⊢ ∀s t i.
    s tagged_partial_division_of i ∧ t ⊆ s ⇒ t tagged_partial_division_of i

TAG_IN_INTERVAL

⊢ ∀p i k. p tagged_division_of i ∧ (x,k) ∈ p ⇒ x ∈ i

VARIATION_EQUAL_LEMMA

⊢ ∀ms ms'.
    (∀s. (ms' (ms s) = s) ∧ (ms (ms' s) = s)) ∧
    (∀d t.
       d division_of t ⇒
       IMAGE (IMAGE ms) d division_of IMAGE ms t ∧
       IMAGE (IMAGE ms') d division_of IMAGE ms' t) ∧
    (∀a b.
       interval [(a,b)] ≠ ∅ ⇒
       (IMAGE ms' (interval [(a,b)]) = interval [(ms' a,ms' b)]) ∨
       (IMAGE ms' (interval [(a,b)]) = interval [(ms' b,ms' a)])) ⇒
    (∀f s.
       (λx. f (ms' x)) has_bounded_variation_on IMAGE ms s ⇔
       f has_bounded_variation_on s) ∧
    ∀f s. vector_variation (IMAGE ms s) (λx. f (ms' x)) = vector_variation s f

VECTOR_VARIATION_ABS

⊢ ∀f s.
    (λx. f x) has_bounded_variation_on s ⇒
    vector_variation s (λx. abs (f x)) ≤ vector_variation s (λx. f x)

VECTOR_VARIATION_AFFINITY

⊢ ∀m c f s.
    vector_variation s (λx. f (m * x + c)) =
    if m = 0 then 0 else vector_variation (IMAGE (λx. m * x + c) s) f

VECTOR_VARIATION_AFFINITY2

⊢ ∀m c f s.
    vector_variation (IMAGE (λx. m⁻¹ * x + -(m⁻¹ * c)) s) (λx. f (m * x + c)) =
    if m = 0 then 0 else vector_variation s f

VECTOR_VARIATION_COMBINE

⊢ ∀f a b c.
    a ≤ c ∧ c ≤ b ∧ f has_bounded_variation_on interval [(a,b)] ⇒
    (vector_variation (interval [(a,c)]) f +
     vector_variation (interval [(c,b)]) f =
     vector_variation (interval [(a,b)]) f)

VECTOR_VARIATION_COMPARISON

⊢ ∀f g s.
    f has_bounded_variation_on s ∧
    (∀x y. x ∈ s ∧ y ∈ s ∧ x < y ⇒ dist (g x,g y) ≤ dist (f x,f y)) ⇒
    vector_variation s g ≤ vector_variation s f

VECTOR_VARIATION_CONST

⊢ ∀s c. vector_variation s (λx. c) = 0

VECTOR_VARIATION_CONST_EQ

⊢ ∀f s.
    is_interval s ∧ f has_bounded_variation_on s ⇒
    ((vector_variation s f = 0) ⇔ ∃c. ∀x. x ∈ s ⇒ (f x = c))

VECTOR_VARIATION_CONTINUOUS

⊢ ∀f a b c.
    f has_bounded_variation_on interval [(a,b)] ∧ c ∈ interval [(a,b)] ⇒
    ((λx. vector_variation (interval [(a,x)]) f) continuous
     (at c within interval [(a,b)]) ⇔
     f continuous (at c within interval [(a,b)]))

VECTOR_VARIATION_CONTINUOUS_LEFT

⊢ ∀f a b c.
    f has_bounded_variation_on interval [(a,b)] ∧ c ∈ interval [(a,b)] ⇒
    ((λx. vector_variation (interval [(a,x)]) f) continuous
     (at c within interval [(a,c)]) ⇔
     f continuous (at c within interval [(a,c)]))

VECTOR_VARIATION_CONTINUOUS_RIGHT

⊢ ∀f a b c.
    f has_bounded_variation_on interval [(a,b)] ∧ c ∈ interval [(a,b)] ⇒
    ((λx. vector_variation (interval [(a,x)]) f) continuous
     (at c within interval [(c,b)]) ⇔
     f continuous (at c within interval [(c,b)]))

VECTOR_VARIATION_EQ

⊢ ∀f g s.
    (∀x. x ∈ s ⇒ (f x = g x)) ⇒ (vector_variation s f = vector_variation s g)

VECTOR_VARIATION_GE_ABS_FUNCTION

⊢ ∀f s a b.
    f has_bounded_variation_on s ∧ segment [(a,b)] ⊆ s ⇒
    abs (f b − f a) ≤ vector_variation s f

VECTOR_VARIATION_GE_FUNCTION

⊢ ∀f s a b.
    f has_bounded_variation_on s ∧ segment [(a,b)] ⊆ s ⇒
    f b − f a ≤ vector_variation s f

VECTOR_VARIATION_MINUS_FUNCTION_MONOTONE

⊢ ∀f a b c d.
    f has_bounded_variation_on interval [(a,b)] ∧
    interval [(c,d)] ⊆ interval [(a,b)] ∧ interval [(c,d)] ≠ ∅ ⇒
    vector_variation (interval [(c,d)]) f − (f d − f c) ≤
    vector_variation (interval [(a,b)]) f − (f b − f a)

VECTOR_VARIATION_MONOTONE

⊢ ∀f s t.
    f has_bounded_variation_on s ∧ t ⊆ s ⇒
    vector_variation t f ≤ vector_variation s f

VECTOR_VARIATION_NEG

⊢ ∀f s. vector_variation s (λx. -f x) = vector_variation s f

VECTOR_VARIATION_ON_DIVISION

⊢ ∀f a b d.
    d division_of interval [(a,b)] ∧
    f has_bounded_variation_on interval [(a,b)] ⇒
    (sum d (λk. vector_variation k f) = vector_variation (interval [(a,b)]) f)

VECTOR_VARIATION_ON_NULL

⊢ ∀f s. (content s = 0) ∧ bounded s ⇒ (vector_variation s f = 0)

VECTOR_VARIATION_POS_LE

⊢ ∀f s. f has_bounded_variation_on s ⇒ 0 ≤ vector_variation s f

VECTOR_VARIATION_REFLECT

⊢ ∀f s.
    vector_variation s (λx. f (-x)) = vector_variation (IMAGE (λx. -x) s) f

VECTOR_VARIATION_REFLECT2

⊢ ∀f s.
    vector_variation (IMAGE (λx. -x) s) (λx. f (-x)) = vector_variation s f

VECTOR_VARIATION_REFLECT_INTERVAL

⊢ ∀f a b.
    vector_variation (interval [(a,b)]) (λx. f (-x)) =
    vector_variation (interval [(-b,-a)]) f

VECTOR_VARIATION_TRANSLATION

⊢ ∀a f s.
    vector_variation s (λx. f (a + x)) =
    vector_variation (IMAGE (λx. a + x) s) f

VECTOR_VARIATION_TRANSLATION2

⊢ ∀a f s.
    vector_variation (IMAGE (λx. -a + x) s) (λx. f (a + x)) =
    vector_variation s f

VECTOR_VARIATION_TRANSLATION_INTERVAL

⊢ ∀a f u v.
    vector_variation (interval [(u,v)]) (λx. f (a + x)) =
    vector_variation (interval [(a + u,a + v)]) f

VECTOR_VARIATION_TRIANGLE

⊢ ∀f g s.
    f has_bounded_variation_on s ∧ g has_bounded_variation_on s ⇒
    vector_variation s (λx. f x + g x) ≤
    vector_variation s f + vector_variation s g

has_integral

⊢ (f has_integral y) (interval [(a,b)]) ⇔
  ∀e. 0 < e ⇒
      ∃d. gauge d ∧
          ∀p. p tagged_division_of interval [(a,b)] ∧ d FINE p ⇒
              abs (sum p (λ(x,k). content k * f x) − y) < e

has_integral_alt

⊢ (f has_integral y) i ⇔
  if ∃a b. i = interval [(a,b)] then (f has_integral y) i
  else
    ∀e. 0 < e ⇒
        ∃B. 0 < B ∧
            ∀a b.
              ball (0,B) ⊆ interval [(a,b)] ⇒
              ∃z. ((λx. if x ∈ i then f x else 0) has_integral z)
                    (interval [(a,b)]) ∧ abs (z − y) < e

lifted_def

⊢ (lifted op NONE v0 = NONE) ∧ (lifted op (SOME v5) NONE = NONE) ∧
  (lifted op (SOME x) (SOME y) = SOME (op x y))

lifted_ind

⊢ ∀P. (∀op v0. P op NONE v0) ∧ (∀op v5. P op (SOME v5) NONE) ∧
      (∀op x y. P op (SOME x) (SOME y)) ⇒
      ∀v v1 v2. P v v1 v2