Theory "lebesgue"

Signature

Definitions

RADON_F_def

⊢ ∀m v.
    RADON_F m v =
    {f |
     f ∈ Borel_measurable (m_space m,measurable_sets m) ∧ (∀x. 0 ≤ f x) ∧
     ∀A. A ∈ measurable_sets m ⇒ ∫⁺ m (λx. f x * 𝟙 A x) ≤ measure v A}

RADON_F_integrals_def

⊢ ∀m v. RADON_F_integrals m v = {r | ∃f. (r = ∫⁺ m f) ∧ f ∈ RADON_F m v}

RN_deriv_def

⊢ ∀v m.
    v / m =
    @f. f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
        (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
        ∀s. s ∈ measurable_sets m ⇒ ((f * m) s = v s)

density_def

⊢ ∀m f. density m f = (m_space m,measurable_sets m,f * m)

density_measure_def

⊢ ∀m f. f * m = (λs. ∫⁺ m (λx. f x * 𝟙 s x))

distr_def

⊢ ∀m f. distr m f = (λs. measure m (PREIMAGE f s ∩ m_space m))

finite_space_integral_def

⊢ ∀m f.
    finite_space_integral m f =
    ∑ (λr. r * measure m (PREIMAGE f {r} ∩ m_space m)) (IMAGE f (m_space m))

fn_seq_def

⊢ ∀m f.
    fn_seq m f =
    (λn x.
         ∑
           (λk.
                &k / 2 pow n *
                𝟙
                  {x |
                   x ∈ m_space m ∧ &k / 2 pow n ≤ f x ∧
                   f x < (&k + 1) / 2 pow n} x) (count (4 ** n)) +
         2 pow n * 𝟙 {x | x ∈ m_space m ∧ 2 pow n ≤ f x} x)

fn_seq_integral_def

⊢ ∀m f.
    fn_seq_integral m f =
    (λn.
         ∑
           (λk.
                &k / 2 pow n *
                measure m
                  {x |
                   x ∈ m_space m ∧ &k / 2 pow n ≤ f x ∧
                   f x < (&k + 1) / 2 pow n}) (count (4 ** n)) +
         2 pow n * measure m {x | x ∈ m_space m ∧ 2 pow n ≤ f x})

integrable_def

⊢ ∀m f.
    integrable m f ⇔
    f ∈ Borel_measurable (m_space m,measurable_sets m) ∧ ∫⁺ m f⁺ ≠ +∞ ∧
    ∫⁺ m f⁻ ≠ +∞

integral_def

⊢ ∀m f. ∫ m f = ∫⁺ m f⁺ − ∫⁺ m f⁻

measure_absolutely_continuous_def

⊢ ∀v m. v ≪ m ⇔ ∀s. s ∈ measurable_sets m ∧ (measure m s = 0) ⇒ (v s = 0)

norm_def

⊢ ∀m u p.
    norm m u p =
    if p < +∞ then ∫ m (λx. abs (u x) powr p) powr p⁻¹
    else inf {c | 0 < c ∧ (measure m {x | c ≤ abs (u x)} = 0)}

pos_fn_integral_def

⊢ ∀m f. ∫⁺ m f = sup {r | (∃g. r ∈ psfis m g ∧ ∀x. x ∈ m_space m ⇒ g x ≤ f x)}

pos_simple_fn_def

⊢ ∀m f s a x.
    pos_simple_fn m f s a x ⇔
    (∀t. t ∈ m_space m ⇒ 0 ≤ f t) ∧
    (∀t. t ∈ m_space m ⇒ (f t = ∑ (λi. Normal (x i) * 𝟙 (a i) t) s)) ∧
    (∀i. i ∈ s ⇒ a i ∈ measurable_sets m) ∧ FINITE s ∧ (∀i. i ∈ s ⇒ 0 ≤ x i) ∧
    (∀i j. i ∈ s ∧ j ∈ s ∧ i ≠ j ⇒ DISJOINT (a i) (a j)) ∧
    (BIGUNION (IMAGE a s) = m_space m)

pos_simple_fn_integral_def

⊢ ∀m s a x.
    pos_simple_fn_integral m s a x = ∑ (λi. Normal (x i) * measure m (a i)) s

psfis_def

⊢ ∀m f.
    psfis m f = IMAGE (λ(s,a,x). pos_simple_fn_integral m s a x) (psfs m f)

psfs_def

⊢ ∀m f. psfs m f = {(s,a,x) | pos_simple_fn m f s a x}

Theorems

BOREL_INDUCT

⊢ ∀f m P.
    measure_space m ∧ f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
    (∀x. 0 ≤ f x) ∧
    (∀f g.
       f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
       g ∈ Borel_measurable (m_space m,measurable_sets m) ∧
       (∀x. x ∈ m_space m ⇒ (f x = g x)) ∧ P f ⇒
       P g) ∧ (∀A. A ∈ measurable_sets m ⇒ P (𝟙 A)) ∧
    (∀f c.
       f ∈ Borel_measurable (m_space m,measurable_sets m) ∧ 0 ≤ c ∧
       (∀x. 0 ≤ f x) ∧ P f ⇒
       P (λx. c * f x)) ∧
    (∀f g.
       f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
       g ∈ Borel_measurable (m_space m,measurable_sets m) ∧ (∀x. 0 ≤ f x) ∧
       P f ∧ (∀x. 0 ≤ g x) ∧ P g ⇒
       P (λx. f x + g x)) ∧
    (∀u. (∀i. u i ∈ Borel_measurable (m_space m,measurable_sets m)) ∧
         (∀i x. 0 ≤ u i x) ∧ (∀x. mono_increasing (λi. u i x)) ∧ (∀i. P (u i)) ⇒
         P (λx. sup (IMAGE (λi. u i x) 𝕌(:num)))) ⇒
    P f

IN_MEASURABLE_BOREL_POS_SIMPLE_FN

⊢ ∀m f.
    measure_space m ∧ (∃s a x. pos_simple_fn m f s a x) ⇒
    f ∈ Borel_measurable (m_space m,measurable_sets m)

IN_psfis

⊢ ∀m r f.
    r ∈ psfis m f ⇒
    ∃s a x. pos_simple_fn m f s a x ∧ (r = pos_simple_fn_integral m s a x)

IN_psfis_eq

⊢ ∀m r f.
    r ∈ psfis m f ⇔
    ∃s a x. pos_simple_fn m f s a x ∧ (r = pos_simple_fn_integral m s a x)

Radon_Nikodym

⊢ ∀m v.
    measure_space m ∧ sigma_finite m ∧
    measure_space (m_space m,measurable_sets m,v) ∧ v ≪ m ⇒
    ∃f. f ∈ Borel_measurable (m_space m,measurable_sets m) ∧ (∀x. 0 ≤ f x) ∧
        ∀s. s ∈ measurable_sets m ⇒ ((f * m) s = v s)

Radon_Nikodym'

⊢ ∀m v.
    measure_space m ∧ sigma_finite m ∧
    measure_space (m_space m,measurable_sets m,v) ∧ v ≪ m ⇒
    ∃f. f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
        (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
        ∀s. s ∈ measurable_sets m ⇒ ((f * m) s = v s)

Radon_Nikodym_finite

⊢ ∀M N.
    measure_space M ∧ measure_space N ∧ (m_space M = m_space N) ∧
    (measurable_sets M = measurable_sets N) ∧ measure M (m_space M) ≠ +∞ ∧
    measure N (m_space N) ≠ +∞ ∧ measure N ≪ M ⇒
    ∃f. f ∈ Borel_measurable (m_space M,measurable_sets M) ∧ (∀x. 0 ≤ f x) ∧
        ∀A. A ∈ measurable_sets M ⇒ (∫⁺ M (λx. f x * 𝟙 A x) = measure N A)

Radon_Nikodym_finite_arbitrary

⊢ ∀M N.
    measure_space M ∧ measure_space N ∧ (m_space M = m_space N) ∧
    (measurable_sets M = measurable_sets N) ∧ measure M (m_space M) ≠ +∞ ∧
    measure N ≪ M ⇒
    ∃f. f ∈ Borel_measurable (m_space M,measurable_sets M) ∧ (∀x. 0 ≤ f x) ∧
        ∀A. A ∈ measurable_sets M ⇒ (∫⁺ M (λx. f x * 𝟙 A x) = measure N A)

Radon_Nikodym_sigma_finite

⊢ ∀M N.
    measure_space M ∧ measure_space N ∧ (m_space M = m_space N) ∧
    (measurable_sets M = measurable_sets N) ∧ sigma_finite M ∧ measure N ≪ M ⇒
    ∃f. f ∈ Borel_measurable (m_space M,measurable_sets M) ∧ (∀x. 0 ≤ f x) ∧
        ∀A. A ∈ measurable_sets M ⇒ (∫⁺ M (λx. f x * 𝟙 A x) = measure N A)

density_fn_plus

⊢ ∀M f.
    density M f⁺ =
    (m_space M,measurable_sets M,(λA. ∫⁺ M (λx. max 0 (f x * 𝟙 A x))))

ext_suminf_cmult_indicator

⊢ ∀A f x i.
    disjoint_family A ∧ x ∈ A i ∧ (∀i. 0 ≤ f i) ⇒
    (suminf (λn. f n * 𝟙 (A n) x) = f i)

finite_integrable_function_exists

⊢ ∀m. measure_space m ∧ sigma_finite m ⇒
      ∃h. h ∈ Borel_measurable (m_space m,measurable_sets m) ∧ ∫⁺ m h ≠ +∞ ∧
          (∀x. x ∈ m_space m ⇒ 0 < h x ∧ h x < +∞) ∧ ∀x. 0 ≤ h x

finite_space_POW_integral_reduce

⊢ ∀m f.
    measure_space m ∧ (POW (m_space m) = measurable_sets m) ∧
    FINITE (m_space m) ∧ (∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ f x ≠ +∞) ∧
    measure m (m_space m) < +∞ ⇒
    (∫ m f = ∑ (λx. f x * measure m {x}) (m_space m))

finite_space_integral_reduce

⊢ ∀m f.
    measure_space m ∧ f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
    (∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ f x ≠ +∞) ∧ FINITE (m_space m) ∧
    measure m (m_space m) < +∞ ∧ integrable m f ⇒
    (∫ m f = finite_space_integral m f)

finite_support_integral_reduce

⊢ ∀m f.
    measure_space m ∧ f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
    (∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ f x ≠ +∞) ∧ FINITE (IMAGE f (m_space m)) ∧
    integrable m f ∧ measure m (m_space m) < +∞ ⇒
    (∫ m f = finite_space_integral m f)

integrable_AE_normal

⊢ ∀m f. measure_space m ∧ integrable m f ⇒ AE x::m. f x < +∞

integrable_abs

⊢ ∀m f. measure_space m ∧ integrable m f ⇒ integrable m (abs ∘ f)

integrable_abs_bound_exists

⊢ ∀m u.
    measure_space m ∧ integrable m (abs ∘ u) ⇒
    ∃w. integrable m w ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ w x) ∧
        ∀x. x ∈ m_space m ⇒ abs (u x) ≤ w x

integrable_add

⊢ ∀m f g.
    measure_space m ∧ integrable m f ∧ integrable m g ∧
    (∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ g x ≠ −∞ ∨ f x ≠ +∞ ∧ g x ≠ +∞) ⇒
    integrable m (λx. f x + g x)

integrable_add_lemma

⊢ ∀m f g.
    measure_space m ∧ integrable m f ∧ integrable m g ⇒
    integrable m (λx. f⁺ x + g⁺ x) ∧ integrable m (λx. f⁻ x + g⁻ x)

integrable_add_pos

⊢ ∀m f g.
    measure_space m ∧ integrable m f ∧ integrable m g ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ g x) ⇒
    integrable m (λx. f x + g x)

integrable_bound_exists

⊢ ∀m u.
    measure_space m ∧ integrable m u ⇒
    ∃w. integrable m w ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ w x) ∧
        ∀x. x ∈ m_space m ⇒ abs (u x) ≤ w x

integrable_bounded

⊢ ∀m f g.
    measure_space m ∧ integrable m f ∧
    g ∈ Borel_measurable (m_space m,measurable_sets m) ∧
    (∀x. x ∈ m_space m ⇒ abs (g x) ≤ f x) ⇒
    integrable m g

integrable_cmul

⊢ ∀m f c. measure_space m ∧ integrable m f ⇒ integrable m (λx. Normal c * f x)

integrable_const

⊢ ∀m c.
    measure_space m ∧ measure m (m_space m) < +∞ ⇒ integrable m (λx. Normal c)

integrable_eq

⊢ ∀m f g.
    measure_space m ∧ integrable m f ∧ (∀x. x ∈ m_space m ⇒ (f x = g x)) ⇒
    integrable m g

integrable_eq_AE

⊢ ∀m f g.
    complete_measure_space m ∧ integrable m f ∧ (AE x::m. f x = g x) ⇒
    integrable m g

integrable_finite_integral

⊢ ∀m f. measure_space m ∧ integrable m f ⇒ ∫ m f ≠ +∞ ∧ ∫ m f ≠ −∞

integrable_fn_minus

⊢ ∀m f. measure_space m ∧ integrable m f ⇒ integrable m f⁻

integrable_fn_plus

⊢ ∀m f. measure_space m ∧ integrable m f ⇒ integrable m f⁺

integrable_from_abs

⊢ ∀m u.
    measure_space m ∧ u ∈ Borel_measurable (m_space m,measurable_sets m) ∧
    integrable m (abs ∘ u) ⇒
    integrable m u

integrable_from_bound_exists

⊢ ∀m u.
    measure_space m ∧ u ∈ Borel_measurable (m_space m,measurable_sets m) ∧
    (∃w. integrable m w ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ w x) ∧
         ∀x. x ∈ m_space m ⇒ abs (u x) ≤ w x) ⇒
    integrable m u

integrable_indicator

⊢ ∀m s.
    measure_space m ∧ s ∈ measurable_sets m ∧ measure m s < +∞ ⇒
    integrable m (𝟙 s)

integrable_indicator_pow

⊢ ∀m s n.
    measure_space m ∧ s ∈ measurable_sets m ∧ measure m s < +∞ ∧ 0 < n ⇒
    integrable m (λx. 𝟙 s x pow n)

integrable_infty

⊢ ∀m f s.
    measure_space m ∧ integrable m f ∧ s ∈ measurable_sets m ∧
    (∀x. x ∈ s ⇒ (f x = +∞)) ⇒
    (measure m s = 0)

integrable_infty_null

⊢ ∀m f.
    measure_space m ∧ integrable m f ⇒
    null_set m {x | x ∈ m_space m ∧ (f x = +∞)}

integrable_mul_indicator

⊢ ∀m s f.
    measure_space m ∧ s ∈ measurable_sets m ∧ measure m s < +∞ ∧
    (∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ f x ≠ +∞) ∧ integrable m f ⇒
    integrable m (λx. f x * 𝟙 s x)

integrable_normal_integral

⊢ ∀m f. measure_space m ∧ integrable m f ⇒ ∃r. ∫ m f = Normal r

integrable_not_infty

⊢ ∀m f.
    measure_space m ∧ integrable m f ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
    ∃g. integrable m g ∧ (∀x. 0 ≤ g x) ∧ (∀x. g x ≠ +∞) ∧ (∫ m f = ∫ m g)

integrable_not_infty_alt

⊢ ∀m f.
    measure_space m ∧ integrable m f ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
    integrable m (λx. if f x = +∞ then 0 else f x) ∧
    (∫ m f = ∫ m (λx. if f x = +∞ then 0 else f x))

integrable_not_infty_alt2

⊢ ∀m f.
    measure_space m ∧ integrable m f ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
    integrable m (λx. if f x = +∞ then 0 else f x) ∧
    (∫⁺ m f = ∫⁺ m (λx. if f x = +∞ then 0 else f x))

integrable_not_infty_alt3

⊢ ∀m f.
    measure_space m ∧ integrable m f ⇒
    integrable m (λx. if (f x = −∞) ∨ (f x = +∞) then 0 else f x) ∧
    (∫ m f = ∫ m (λx. if (f x = −∞) ∨ (f x = +∞) then 0 else f x))

integrable_plus_minus

⊢ ∀m f.
    measure_space m ⇒
    (integrable m f ⇔
     f ∈ Borel_measurable (m_space m,measurable_sets m) ∧ integrable m f⁺ ∧
     integrable m f⁻)

integrable_pos

⊢ ∀m f.
    measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
    (integrable m f ⇔
     f ∈ Borel_measurable (m_space m,measurable_sets m) ∧ ∫⁺ m f ≠ +∞)

integrable_sub

⊢ ∀m f g.
    measure_space m ∧ integrable m f ∧ integrable m g ∧
    (∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ g x ≠ +∞) ⇒
    integrable m (λx. f x − g x)

integrable_sum

⊢ ∀m f s.
    FINITE s ∧ measure_space m ∧ (∀i. i ∈ s ⇒ integrable m (f i)) ∧
    (∀i x. i ∈ s ∧ x ∈ m_space m ⇒ f i x ≠ +∞ ∧ f i x ≠ −∞) ⇒
    integrable m (λx. ∑ (λi. f i x) s)

integrable_zero

⊢ ∀m c. measure_space m ⇒ integrable m (λx. 0)

integral_abs_eq_0

⊢ ∀m f.
    measure_space m ∧ f ∈ Borel_measurable (m_space m,measurable_sets m) ⇒
    ((∫ m (abs ∘ f) = 0) ⇔ AE x::m. (abs ∘ f) x = 0) ∧
    ((AE x::m. (abs ∘ f) x = 0) ⇔
     (measure m {x | x ∈ m_space m ∧ f x ≠ 0} = 0))

integral_abs_imp_integrable

⊢ ∀m f.
    measure_space m ∧ f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
    (∫ m (abs ∘ f) = 0) ⇒
    integrable m f

integral_abs_pos_fn

⊢ ∀m f. measure_space m ⇒ (∫ m (abs ∘ f) = ∫⁺ m (abs ∘ f))

integral_add

⊢ ∀m f g.
    measure_space m ∧ integrable m f ∧ integrable m g ∧
    (∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ g x ≠ −∞ ∨ f x ≠ +∞ ∧ g x ≠ +∞) ⇒
    (∫ m (λx. f x + g x) = ∫ m f + ∫ m g)

integral_add_lemma

⊢ ∀m f f1 f2.
    measure_space m ∧ integrable m f ∧ integrable m f1 ∧ integrable m f2 ∧
    (∀x. x ∈ m_space m ⇒ (f x = f1 x − f2 x)) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ f1 x) ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f2 x) ∧
    (∀x. x ∈ m_space m ⇒ f1 x ≠ +∞ ∨ f2 x ≠ +∞) ⇒
    (∫ m f = ∫⁺ m f1 − ∫⁺ m f2)

integral_add_lemma'

⊢ ∀m f f1 f2.
    measure_space m ∧ integrable m f ∧ integrable m f1 ∧ integrable m f2 ∧
    (∀x. x ∈ m_space m ⇒ (f x = f1 x − f2 x)) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ f1 x) ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f2 x) ⇒
    (∫ m f = ∫⁺ m f1 − ∫⁺ m f2)

integral_cmul

⊢ ∀m f c.
    measure_space m ∧ integrable m f ⇒
    (∫ m (λx. Normal c * f x) = Normal c * ∫ m f)

integral_cmul_indicator

⊢ ∀m s c.
    measure_space m ∧ s ∈ measurable_sets m ∧ measure m s < +∞ ⇒
    (∫ m (λx. Normal c * 𝟙 s x) = Normal c * measure m s)

integral_cmul_infty

⊢ ∀m s.
    measure_space m ∧ s ∈ measurable_sets m ⇒
    (∫ m (λx. +∞ * 𝟙 s x) = +∞ * measure m s)

integral_cong

⊢ ∀m f g.
    measure_space m ∧ (∀x. x ∈ m_space m ⇒ (f x = g x)) ⇒ (∫ m f = ∫ m g)

integral_cong_AE

⊢ ∀m f g. measure_space m ∧ (AE x::m. f x = g x) ⇒ (∫ m f = ∫ m g)

integral_const

⊢ ∀m c.
    measure_space m ∧ measure m (m_space m) < +∞ ⇒
    (∫ m (λx. Normal c) = Normal c * measure m (m_space m))

integral_eq_0

⊢ ∀m f.
    f ∈ Borel_measurable (m_space m,measurable_sets m) ∧ measure_space m ∧
    (AE x::m. 0 ≤ f x) ⇒
    ((∫ m f = 0) ⇔ (measure m {x | x ∈ m_space m ∧ f x ≠ 0} = 0))

integral_indicator

⊢ ∀m s. measure_space m ∧ s ∈ measurable_sets m ⇒ (∫ m (𝟙 s) = measure m s)

integral_indicator_pow

⊢ ∀m s n.
    measure_space m ∧ s ∈ measurable_sets m ∧ 0 < n ⇒
    (∫ m (λx. 𝟙 s x pow n) = measure m s)

integral_indicator_pow_eq

⊢ ∀m s n.
    measure_space m ∧ s ∈ measurable_sets m ∧ 0 < n ⇒
    (∫ m (λx. 𝟙 s x pow n) = ∫ m (𝟙 s))

integral_mono

⊢ ∀m f1 f2.
    measure_space m ∧ integrable m f1 ∧ integrable m f2 ∧
    (∀x. x ∈ m_space m ⇒ f1 x ≤ f2 x) ⇒
    ∫ m f1 ≤ ∫ m f2

integral_mspace

⊢ ∀m f. measure_space m ⇒ (∫ m f = ∫ m (λx. f x * 𝟙 (m_space m) x))

integral_null_set

⊢ ∀m f N.
    measure_space m ∧ f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
    N ∈ null_set m ⇒
    integrable m (λx. f x * 𝟙 N x) ∧ (∫ m (λx. f x * 𝟙 N x) = 0)

integral_pos

⊢ ∀m f. measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒ 0 ≤ ∫ m f

integral_pos_fn

⊢ ∀m f. measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒ (∫ m f = ∫⁺ m f)

integral_posinf

⊢ ∀m. measure_space m ∧ 0 < measure m (m_space m) ⇒ (∫ m (λx. +∞) = +∞)

integral_sequence

⊢ ∀m f.
    (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧ measure_space m ∧
    f ∈ Borel_measurable (m_space m,measurable_sets m) ⇒
    (∫⁺ m f = sup (IMAGE (λi. ∫⁺ m (fn_seq m f i)) 𝕌(:num)))

integral_split

⊢ ∀m f s.
    measure_space m ∧ s ∈ measurable_sets m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
    f ∈ Borel_measurable (m_space m,measurable_sets m) ⇒
    (∫ m f = ∫ m (λx. f x * 𝟙 s x) + ∫ m (λx. f x * 𝟙 (m_space m DIFF s) x))

integral_split'

⊢ ∀m f s.
    measure_space m ∧ integrable m f ∧ s ∈ measurable_sets m ⇒
    (∫ m f = ∫ m (λx. f x * 𝟙 s x) + ∫ m (λx. f x * 𝟙 (m_space m DIFF s) x))

integral_sum

⊢ ∀m f s.
    FINITE s ∧ measure_space m ∧ (∀i. i ∈ s ⇒ integrable m (f i)) ∧
    (∀x i. i ∈ s ∧ x ∈ m_space m ⇒ f i x ≠ +∞ ∧ f i x ≠ −∞) ⇒
    (∫ m (λx. ∑ (λi. f i x) s) = ∑ (λi. ∫ m (f i)) s)

integral_triangle_ineq

⊢ ∀m f. measure_space m ∧ integrable m f ⇒ abs (∫ m f) ≤ ∫ m (abs ∘ f)

integral_triangle_ineq'

⊢ ∀m f. measure_space m ∧ integrable m f ⇒ abs (∫ m f) ≤ ∫⁺ m (abs ∘ f)

integral_zero

⊢ ∀m. measure_space m ⇒ (∫ m (λx. 0) = 0)

lebesgue_monotone_convergence

⊢ ∀m f fi.
    measure_space m ∧
    (∀i. fi i ∈ Borel_measurable (m_space m,measurable_sets m)) ∧
    (∀i x. x ∈ m_space m ⇒ 0 ≤ fi i x) ∧
    (∀x. x ∈ m_space m ⇒ mono_increasing (λi. fi i x)) ∧
    (∀x. x ∈ m_space m ⇒ (sup (IMAGE (λi. fi i x) 𝕌(:num)) = f x)) ⇒
    (∫⁺ m f = sup (IMAGE (λi. ∫⁺ m (fi i)) 𝕌(:num)))

lebesgue_monotone_convergence_AE

⊢ ∀m f fi.
    measure_space m ∧
    (∀i. fi i ∈ Borel_measurable (m_space m,measurable_sets m)) ∧
    (AE x::m. ∀i. fi i x ≤ fi (SUC i) x ∧ 0 ≤ fi i x) ∧
    (∀x. x ∈ m_space m ⇒ (sup (IMAGE (λi. fi i x) 𝕌(:num)) = f x)) ⇒
    (∫⁺ m f⁺ = sup (IMAGE (λi. ∫⁺ m (fi i)⁺) 𝕌(:num)))

lebesgue_monotone_convergence_decreasing

⊢ ∀m f fi.
    measure_space m ∧
    (∀i. fi i ∈ Borel_measurable (m_space m,measurable_sets m)) ∧
    (∀i x. x ∈ m_space m ⇒ 0 ≤ fi i x ∧ fi i x < +∞) ∧
    (∀i. ∫⁺ m (fi i) ≠ +∞) ∧
    (∀x. x ∈ m_space m ⇒ mono_decreasing (λi. fi i x)) ∧
    (∀x. x ∈ m_space m ⇒ (inf (IMAGE (λi. fi i x) 𝕌(:num)) = f x)) ⇒
    (∫⁺ m f = inf (IMAGE (λi. ∫⁺ m (fi i)) 𝕌(:num)))

lebesgue_monotone_convergence_subset

⊢ ∀m f fi A.
    measure_space m ∧
    (∀i. fi i ∈ Borel_measurable (m_space m,measurable_sets m)) ∧
    (∀i x. x ∈ m_space m ⇒ 0 ≤ fi i x) ∧
    (∀x. x ∈ m_space m ⇒ (sup (IMAGE (λi. fi i x) 𝕌(:num)) = f x)) ∧
    (∀x. x ∈ m_space m ⇒ mono_increasing (λi. fi i x)) ∧ A ∈ measurable_sets m ⇒
    (∫⁺ m (λx. f x * 𝟙 A x) =
     sup (IMAGE (λi. ∫⁺ m (λx. fi i x * 𝟙 A x)) 𝕌(:num)))

lemma_fn_seq_measurable

⊢ ∀m f n.
    measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
    f ∈ Borel_measurable (m_space m,measurable_sets m) ⇒
    fn_seq m f n ∈ Borel_measurable (m_space m,measurable_sets m)

lemma_fn_seq_mono_increasing

⊢ ∀m f x. 0 ≤ f x ⇒ mono_increasing (λn. fn_seq m f n x)

lemma_fn_seq_positive

⊢ ∀m f n x. 0 ≤ f x ⇒ 0 ≤ fn_seq m f n x

lemma_fn_seq_sup

⊢ ∀m f x.
    x ∈ m_space m ∧ 0 ≤ f x ⇒ (sup (IMAGE (λn. fn_seq m f n x) 𝕌(:num)) = f x)

markov_ineq

⊢ ∀m f c.
    measure_space m ∧ integrable m f ∧ 0 < c ⇒
    measure m ({x | c ≤ abs (f x)} ∩ m_space m) ≤ c⁻¹ * ∫ m (abs ∘ f)

markov_inequality

⊢ ∀m f a c.
    measure_space m ∧ integrable m f ∧ a ∈ measurable_sets m ∧ 0 < c ⇒
    measure m ({x | c ≤ abs (f x)} ∩ a) ≤ c⁻¹ * ∫ m (λx. abs (f x) * 𝟙 a x)

measurable_sequence

⊢ ∀m f.
    measure_space m ∧ f ∈ Borel_measurable (m_space m,measurable_sets m) ⇒
    (∃fi ri.
       (∀x. mono_increasing (λi. fi i x)) ∧
       (∀x. x ∈ m_space m ⇒ (sup (IMAGE (λi. fi i x) 𝕌(:num)) = f⁺ x)) ∧
       (∀i. ri i ∈ psfis m (fi i)) ∧ (∀i x. fi i x ≤ f⁺ x) ∧
       (∀i x. 0 ≤ fi i x) ∧ (∫⁺ m f⁺ = sup (IMAGE (λi. ∫⁺ m (fi i)) 𝕌(:num)))) ∧
    ∃gi vi.
      (∀x. mono_increasing (λi. gi i x)) ∧
      (∀x. x ∈ m_space m ⇒ (sup (IMAGE (λi. gi i x) 𝕌(:num)) = f⁻ x)) ∧
      (∀i. vi i ∈ psfis m (gi i)) ∧ (∀i x. gi i x ≤ f⁻ x) ∧
      (∀i x. 0 ≤ gi i x) ∧ (∫⁺ m f⁻ = sup (IMAGE (λi. ∫⁺ m (gi i)) 𝕌(:num)))

measure_density_indicator

⊢ ∀m s t.
    measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
    (measure (density m (𝟙 s)) t = measure m (s ∩ t))

measure_restricted

⊢ ∀m s t.
    measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
    (measure (m_space m,measurable_sets m,(λA. ∫⁺ m (λx. 𝟙 s x * 𝟙 A x))) t =
     measure m (s ∩ t))

measure_space_density

⊢ ∀m f.
    measure_space m ∧ f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
    measure_space (density m f)

measure_space_density'

⊢ ∀M f.
    measure_space M ∧ f ∈ Borel_measurable (m_space M,measurable_sets M) ⇒
    measure_space (density M f⁺)

measure_space_distr

⊢ ∀M B f.
    measure_space M ∧ sigma_algebra B ∧
    f ∈ measurable (m_space M,measurable_sets M) B ⇒
    measure_space (space B,subsets B,distr M f)

measure_subadditive_finite

⊢ ∀I A M.
    measure_space M ∧ FINITE I ∧ IMAGE A I ⊆ measurable_sets M ⇒
    measure M (BIGUNION {A i | i ∈ I}) ≤ ∑ (λi. measure M (A i)) I

pos_fn_integral_add

⊢ ∀m f g.
    measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ g x) ∧
    f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
    g ∈ Borel_measurable (m_space m,measurable_sets m) ⇒
    (∫⁺ m (λx. f x + g x) = ∫⁺ m f + ∫⁺ m g)

pos_fn_integral_cmul

⊢ ∀m f c.
    measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧ 0 ≤ c ⇒
    (∫⁺ m (λx. Normal c * f x) = Normal c * ∫⁺ m f)

pos_fn_integral_cmul_indicator

⊢ ∀m s c.
    measure_space m ∧ s ∈ measurable_sets m ∧ 0 ≤ c ⇒
    (∫⁺ m (λx. Normal c * 𝟙 s x) = Normal c * measure m s)

pos_fn_integral_cmul_infty

⊢ ∀m s.
    measure_space m ∧ s ∈ measurable_sets m ⇒
    (∫⁺ m (λx. +∞ * 𝟙 s x) = +∞ * measure m s)

pos_fn_integral_cmult

⊢ ∀f c m.
    measure_space m ∧ 0 ≤ c ∧
    f ∈ Borel_measurable (m_space m,measurable_sets m) ⇒
    (∫⁺ m (λx. c * f⁺ x) = c * ∫⁺ m f⁺)

pos_fn_integral_cmult'

⊢ ∀f c m.
    measure_space m ∧ 0 ≤ c ∧
    f ∈ Borel_measurable (m_space m,measurable_sets m) ⇒
    (∫⁺ m (λx. max 0 (c * f x)) = c * ∫⁺ m (λx. max 0 (f x)))

pos_fn_integral_cong

⊢ ∀m u v.
    measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ u x) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ v x) ∧ (∀x. x ∈ m_space m ⇒ (u x = v x)) ⇒
    (∫⁺ m u = ∫⁺ m v)

pos_fn_integral_cong_AE

⊢ ∀m u v.
    measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ u x) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ v x) ∧ (AE x::m. u x = v x) ⇒
    (∫⁺ m u = ∫⁺ m v)

pos_fn_integral_density

⊢ ∀m f g.
    measure_space m ∧ f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
    g ∈ Borel_measurable (m_space m,measurable_sets m) ∧ (AE x::m. 0 ≤ f x) ∧
    (∀x. 0 ≤ g x) ⇒
    (∫⁺ (density m f⁺) g = ∫⁺ m (λx. f⁺ x * g x))

pos_fn_integral_density'

⊢ ∀f g M.
    measure_space M ∧ f ∈ Borel_measurable (m_space M,measurable_sets M) ∧
    g ∈ Borel_measurable (m_space M,measurable_sets M) ∧ (AE x::M. 0 ≤ f x) ∧
    (∀x. 0 ≤ g x) ⇒
    (∫⁺ (m_space M,measurable_sets M,(λA. ∫⁺ M (λx. max 0 (f x * 𝟙 A x))))
       (λx. max 0 (g x)) = ∫⁺ M (λx. max 0 (f x * g x)))

pos_fn_integral_disjoint_sets

⊢ ∀m f s t.
    measure_space m ∧ DISJOINT s t ∧ s ∈ measurable_sets m ∧
    t ∈ measurable_sets m ∧
    f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
    (∫⁺ m (λx. f x * 𝟙 (s ∪ t) x) =
     ∫⁺ m (λx. f x * 𝟙 s x) + ∫⁺ m (λx. f x * 𝟙 t x))

pos_fn_integral_disjoint_sets_sum

⊢ ∀m f s a.
    FINITE s ∧ measure_space m ∧ (∀i. i ∈ s ⇒ a i ∈ measurable_sets m) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
    (∀i j. i ∈ s ∧ j ∈ s ∧ i ≠ j ⇒ DISJOINT (a i) (a j)) ∧
    f ∈ Borel_measurable (m_space m,measurable_sets m) ⇒
    (∫⁺ m (λx. f x * 𝟙 (BIGUNION (IMAGE a s)) x) =
     ∑ (λi. ∫⁺ m (λx. f x * 𝟙 (a i) x)) s)

pos_fn_integral_eq_0

⊢ ∀m f.
    measure_space m ∧ nonneg f ∧
    f ∈ Borel_measurable (m_space m,measurable_sets m) ⇒
    ((∫⁺ m f = 0) ⇔ (measure m {x | x ∈ m_space m ∧ f x ≠ 0} = 0))

pos_fn_integral_indicator

⊢ ∀m s. measure_space m ∧ s ∈ measurable_sets m ⇒ (∫⁺ m (𝟙 s) = measure m s)

pos_fn_integral_infty_null

⊢ ∀m f.
    measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
    f ∈ Borel_measurable (m_space m,measurable_sets m) ∧ ∫⁺ m f ≠ +∞ ⇒
    null_set m {x | x ∈ m_space m ∧ (f x = +∞)}

pos_fn_integral_mono

⊢ ∀m f g.
    (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧ (∀x. x ∈ m_space m ⇒ f x ≤ g x) ⇒
    ∫⁺ m f ≤ ∫⁺ m g

pos_fn_integral_mono_AE

⊢ ∀m u v.
    measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ u x) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ v x) ∧ (AE x::m. u x ≤ v x) ⇒
    ∫⁺ m u ≤ ∫⁺ m v

pos_fn_integral_mspace

⊢ ∀m f.
    measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
    (∫⁺ m f = ∫⁺ m (λx. f x * 𝟙 (m_space m) x))

pos_fn_integral_null_set

⊢ ∀m f N.
    measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧ N ∈ null_set m ⇒
    (∫⁺ m (λx. f x * 𝟙 N x) = 0)

pos_fn_integral_pos

⊢ ∀m f. measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒ 0 ≤ ∫⁺ m f

pos_fn_integral_pos_simple_fn

⊢ ∀m f s a x.
    measure_space m ∧ pos_simple_fn m f s a x ⇒
    (∫⁺ m f = pos_simple_fn_integral m s a x)

pos_fn_integral_split

⊢ ∀m f s.
    measure_space m ∧ s ∈ measurable_sets m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
    f ∈ Borel_measurable (m_space m,measurable_sets m) ⇒
    (∫⁺ m f = ∫⁺ m (λx. f x * 𝟙 s x) + ∫⁺ m (λx. f x * 𝟙 (m_space m DIFF s) x))

pos_fn_integral_sub

⊢ ∀m f g.
    measure_space m ∧ f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
    g ∈ Borel_measurable (m_space m,measurable_sets m) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ g x) ∧ (∀x. x ∈ m_space m ⇒ g x ≤ f x) ∧
    (∀x. x ∈ m_space m ⇒ g x ≠ +∞) ∧ ∫⁺ m g ≠ +∞ ⇒
    (∫⁺ m (λx. f x − g x) = ∫⁺ m f − ∫⁺ m g)

pos_fn_integral_sum

⊢ ∀m f s.
    FINITE s ∧ measure_space m ∧ (∀i. i ∈ s ⇒ ∀x. x ∈ m_space m ⇒ 0 ≤ f i x) ∧
    (∀i. i ∈ s ⇒ f i ∈ Borel_measurable (m_space m,measurable_sets m)) ⇒
    (∫⁺ m (λx. ∑ (λi. f i x) s) = ∑ (λi. ∫⁺ m (f i)) s)

pos_fn_integral_sum_cmul_indicator

⊢ ∀m s a x.
    measure_space m ∧ FINITE s ∧ (∀i. i ∈ s ⇒ 0 ≤ x i) ∧
    (∀i. i ∈ s ⇒ a i ∈ measurable_sets m) ⇒
    (∫⁺ m (λt. ∑ (λi. Normal (x i) * 𝟙 (a i) t) s) =
     ∑ (λi. Normal (x i) * measure m (a i)) s)

pos_fn_integral_suminf

⊢ ∀m f.
    measure_space m ∧ (∀i x. x ∈ m_space m ⇒ 0 ≤ f i x) ∧
    (∀i. f i ∈ Borel_measurable (m_space m,measurable_sets m)) ⇒
    (∫⁺ m (λx. suminf (λi. f i x)) = suminf (λi. ∫⁺ m (f i)))

pos_fn_integral_zero

⊢ ∀m. measure_space m ⇒ (∫⁺ m (λx. 0) = 0)

pos_simple_fn_add

⊢ ∀m f g s a x s' a' x'.
    measure_space m ∧ pos_simple_fn m f s a x ∧ pos_simple_fn m g s' a' x' ⇒
    ∃s'' a'' x''. pos_simple_fn m (λt. f t + g t) s'' a'' x''

pos_simple_fn_add_alt

⊢ ∀m f g s a x y.
    measure_space m ∧ pos_simple_fn m f s a x ∧ pos_simple_fn m g s a y ⇒
    pos_simple_fn m (λt. f t + g t) s a (λi. x i + y i)

pos_simple_fn_cmul

⊢ ∀m f z s a x.
    measure_space m ∧ pos_simple_fn m f s a x ∧ 0 ≤ z ⇒
    ∃s' a' x'. pos_simple_fn m (λt. Normal z * f t) s' a' x'

pos_simple_fn_cmul_alt

⊢ ∀m f s a x z.
    measure_space m ∧ 0 ≤ z ∧ pos_simple_fn m f s a x ⇒
    pos_simple_fn m (λt. Normal z * f t) s a (λi. z * x i)

pos_simple_fn_indicator

⊢ ∀m A.
    measure_space m ∧ A ∈ measurable_sets m ⇒
    ∃s a x. pos_simple_fn m (𝟙 A) s a x

pos_simple_fn_indicator_alt

⊢ ∀m s.
    measure_space m ∧ s ∈ measurable_sets m ⇒
    pos_simple_fn m (𝟙 s) {0; 1} (λi. if i = 0 then m_space m DIFF s else s)
      (λi. if i = 0 then 0 else 1)

pos_simple_fn_integral_add

⊢ ∀m f s a x g s' b y.
    measure_space m ∧ pos_simple_fn m f s a x ∧ pos_simple_fn m g s' b y ⇒
    ∃s'' c z.
      pos_simple_fn m (λx. f x + g x) s'' c z ∧
      (pos_simple_fn_integral m s a x + pos_simple_fn_integral m s' b y =
       pos_simple_fn_integral m s'' c z)

pos_simple_fn_integral_add_alt

⊢ ∀m f s a x g y.
    measure_space m ∧ pos_simple_fn m f s a x ∧ pos_simple_fn m g s a y ⇒
    (pos_simple_fn_integral m s a x + pos_simple_fn_integral m s a y =
     pos_simple_fn_integral m s a (λi. x i + y i))

pos_simple_fn_integral_cmul

⊢ ∀m f s a x z.
    measure_space m ∧ pos_simple_fn m f s a x ∧ 0 ≤ z ⇒
    pos_simple_fn m (λx. Normal z * f x) s a (λi. z * x i) ∧
    (pos_simple_fn_integral m s a (λi. z * x i) =
     Normal z * pos_simple_fn_integral m s a x)

pos_simple_fn_integral_cmul_alt

⊢ ∀m f s a x z.
    measure_space m ∧ 0 ≤ z ∧ pos_simple_fn m f s a x ⇒
    ∃s' a' x'.
      pos_simple_fn m (λt. Normal z * f t) s' a' x' ∧
      (pos_simple_fn_integral m s' a' x' =
       Normal z * pos_simple_fn_integral m s a x)

pos_simple_fn_integral_indicator

⊢ ∀m A.
    measure_space m ∧ A ∈ measurable_sets m ⇒
    ∃s a x.
      pos_simple_fn m (𝟙 A) s a x ∧
      (pos_simple_fn_integral m s a x = measure m A)

pos_simple_fn_integral_mono

⊢ ∀m f s a x g s' b y.
    measure_space m ∧ pos_simple_fn m f s a x ∧ pos_simple_fn m g s' b y ∧
    (∀x. x ∈ m_space m ⇒ f x ≤ g x) ⇒
    pos_simple_fn_integral m s a x ≤ pos_simple_fn_integral m s' b y

pos_simple_fn_integral_not_infty

⊢ ∀m f s a x.
    measure_space m ∧ pos_simple_fn m f s a x ⇒
    pos_simple_fn_integral m s a x ≠ −∞

pos_simple_fn_integral_present

⊢ ∀m f s a x g s' b y.
    measure_space m ∧ pos_simple_fn m f s a x ∧ pos_simple_fn m g s' b y ⇒
    ∃z z' c k.
      (∀t. t ∈ m_space m ⇒ (f t = ∑ (λi. Normal (z i) * 𝟙 (c i) t) k)) ∧
      (∀t. t ∈ m_space m ⇒ (g t = ∑ (λi. Normal (z' i) * 𝟙 (c i) t) k)) ∧
      (pos_simple_fn_integral m s a x = pos_simple_fn_integral m k c z) ∧
      (pos_simple_fn_integral m s' b y = pos_simple_fn_integral m k c z') ∧
      FINITE k ∧ (∀i. i ∈ k ⇒ 0 ≤ z i) ∧ (∀i. i ∈ k ⇒ 0 ≤ z' i) ∧
      (∀i j. i ∈ k ∧ j ∈ k ∧ i ≠ j ⇒ DISJOINT (c i) (c j)) ∧
      (∀i. i ∈ k ⇒ c i ∈ measurable_sets m) ∧
      (BIGUNION (IMAGE c k) = m_space m)

pos_simple_fn_integral_sub

⊢ ∀m f s a x g s' b y.
    measure_space m ∧ measure m (m_space m) ≠ +∞ ∧
    (∀x. x ∈ m_space m ⇒ g x ≤ f x) ∧ (∀x. x ∈ m_space m ⇒ g x ≠ +∞) ∧
    pos_simple_fn m f s a x ∧ pos_simple_fn m g s' b y ⇒
    ∃s'' c z.
      pos_simple_fn m (λx. f x − g x) s'' c z ∧
      (pos_simple_fn_integral m s a x − pos_simple_fn_integral m s' b y =
       pos_simple_fn_integral m s'' c z)

pos_simple_fn_integral_sum

⊢ ∀m f s a x P.
    measure_space m ∧ (∀i. i ∈ P ⇒ pos_simple_fn m (f i) s a (x i)) ∧
    (∀i t. i ∈ P ⇒ f i t ≠ −∞) ∧ FINITE P ∧ P ≠ ∅ ⇒
    pos_simple_fn m (λt. ∑ (λi. f i t) P) s a (λi. ∑ (λj. x j i) P) ∧
    (pos_simple_fn_integral m s a (λj. ∑ (λi. x i j) P) =
     ∑ (λi. pos_simple_fn_integral m s a (x i)) P)

pos_simple_fn_integral_sum_alt

⊢ ∀m f s a x P.
    measure_space m ∧ (∀i. i ∈ P ⇒ pos_simple_fn m (f i) (s i) (a i) (x i)) ∧
    (∀i t. i ∈ P ⇒ f i t ≠ −∞) ∧ FINITE P ∧ P ≠ ∅ ⇒
    ∃c k z.
      pos_simple_fn m (λt. ∑ (λi. f i t) P) k c z ∧
      (pos_simple_fn_integral m k c z =
       ∑ (λi. pos_simple_fn_integral m (s i) (a i) (x i)) P)

pos_simple_fn_integral_unique

⊢ ∀m f s a x s' b y.
    measure_space m ∧ pos_simple_fn m f s a x ∧ pos_simple_fn m f s' b y ⇒
    (pos_simple_fn_integral m s a x = pos_simple_fn_integral m s' b y)

pos_simple_fn_integral_zero

⊢ ∀m s a x.
    measure_space m ∧ pos_simple_fn m (λt. 0) s a x ⇒
    (pos_simple_fn_integral m s a x = 0)

pos_simple_fn_integral_zero_alt

⊢ ∀m g s a x.
    measure_space m ∧ pos_simple_fn m g s a x ∧
    (∀x. x ∈ m_space m ⇒ (g x = 0)) ⇒
    (pos_simple_fn_integral m s a x = 0)

pos_simple_fn_le

⊢ ∀m f g s a x x' i.
    measure_space m ∧ pos_simple_fn m f s a x ∧ pos_simple_fn m g s a x' ∧
    (∀x. x ∈ m_space m ⇒ g x ≤ f x) ∧ i ∈ s ∧ a i ≠ ∅ ⇒
    Normal (x' i) ≤ Normal (x i)

pos_simple_fn_max

⊢ ∀m f s a x g s' b y.
    measure_space m ∧ pos_simple_fn m f s a x ∧ pos_simple_fn m g s' b y ⇒
    ∃s'' a'' x''. pos_simple_fn m (λx. max (f x) (g x)) s'' a'' x''

pos_simple_fn_not_infty

⊢ ∀m f s a x.
    pos_simple_fn m f s a x ⇒ ∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ f x ≠ +∞

pos_simple_fn_thm1

⊢ ∀m f s a x i y.
    measure_space m ∧ pos_simple_fn m f s a x ∧ i ∈ s ∧ y ∈ a i ⇒
    (f y = Normal (x i))

psfis_add

⊢ ∀m f g a b.
    measure_space m ∧ a ∈ psfis m f ∧ b ∈ psfis m g ⇒
    a + b ∈ psfis m (λx. f x + g x)

psfis_cmul

⊢ ∀m f a z.
    measure_space m ∧ a ∈ psfis m f ∧ 0 ≤ z ⇒
    Normal z * a ∈ psfis m (λx. Normal z * f x)

psfis_indicator

⊢ ∀m A. measure_space m ∧ A ∈ measurable_sets m ⇒ measure m A ∈ psfis m (𝟙 A)

psfis_intro

⊢ ∀m a x P.
    measure_space m ∧ (∀i. i ∈ P ⇒ a i ∈ measurable_sets m) ∧
    (∀i. i ∈ P ⇒ 0 ≤ x i) ∧ FINITE P ⇒
    ∑ (λi. Normal (x i) * measure m (a i)) P ∈
    psfis m (λt. ∑ (λi. Normal (x i) * 𝟙 (a i) t) P)

psfis_mono

⊢ ∀m f g a b.
    measure_space m ∧ a ∈ psfis m f ∧ b ∈ psfis m g ∧
    (∀x. x ∈ m_space m ⇒ f x ≤ g x) ⇒
    a ≤ b

psfis_not_infty

⊢ ∀m f a. measure_space m ∧ a ∈ psfis m f ⇒ a ≠ −∞

psfis_pos

⊢ ∀m f a. measure_space m ∧ a ∈ psfis m f ⇒ ∀x. x ∈ m_space m ⇒ 0 ≤ f x

psfis_present

⊢ ∀m f g a b.
    measure_space m ∧ a ∈ psfis m f ∧ b ∈ psfis m g ⇒
    ∃z z' c k.
      (∀t. t ∈ m_space m ⇒ (f t = ∑ (λi. Normal (z i) * 𝟙 (c i) t) k)) ∧
      (∀t. t ∈ m_space m ⇒ (g t = ∑ (λi. Normal (z' i) * 𝟙 (c i) t) k)) ∧
      (a = pos_simple_fn_integral m k c z) ∧
      (b = pos_simple_fn_integral m k c z') ∧ FINITE k ∧
      (∀i. i ∈ k ⇒ 0 ≤ z i) ∧ (∀i. i ∈ k ⇒ 0 ≤ z' i) ∧
      (∀i j. i ∈ k ∧ j ∈ k ∧ i ≠ j ⇒ DISJOINT (c i) (c j)) ∧
      (∀i. i ∈ k ⇒ c i ∈ measurable_sets m) ∧
      (BIGUNION (IMAGE c k) = m_space m)

psfis_sub

⊢ ∀m f g a b.
    measure_space m ∧ measure m (m_space m) ≠ +∞ ∧
    (∀x. x ∈ m_space m ⇒ g x ≤ f x) ∧ (∀x. x ∈ m_space m ⇒ g x ≠ +∞) ∧
    a ∈ psfis m f ∧ b ∈ psfis m g ⇒
    a − b ∈ psfis m (λx. f x − g x)

psfis_sum

⊢ ∀m f a P.
    measure_space m ∧ (∀i. i ∈ P ⇒ a i ∈ psfis m (f i)) ∧
    (∀i t. i ∈ P ⇒ f i t ≠ −∞) ∧ FINITE P ⇒
    ∑ a P ∈ psfis m (λt. ∑ (λi. f i t) P)

psfis_unique

⊢ ∀m f a b. measure_space m ∧ a ∈ psfis m f ∧ b ∈ psfis m f ⇒ (a = b)

psfis_zero

⊢ ∀m a. measure_space m ⇒ (a ∈ psfis m (λx. 0) ⇔ (a = 0))