Theory "measure"

Parents extreal

Signature

Constant	Type
Borel	:(extreal -> bool) # ((extreal -> bool) -> bool)
additive	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> bool
algebra	:(α -> bool) # ((α -> bool) -> bool) -> bool
closed_cdi	:(α -> bool) # ((α -> bool) -> bool) -> bool
countably_additive	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> bool
countably_subadditive	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> bool
fn_abs	:(α -> extreal) -> α -> extreal
fn_minus	:(α -> extreal) -> α -> extreal
fn_plus	:(α -> extreal) -> α -> extreal
increasing	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> bool
indicator_fn	:(α -> bool) -> α -> extreal
inf_measure	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> bool) -> real
lambda_system	:(α -> bool) # ((α -> bool) -> bool) -> ((α -> bool) -> real) -> (α -> bool) -> bool
m_space	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> α -> bool
measurable	:(α -> bool) # ((α -> bool) -> bool) -> (β -> bool) # ((β -> bool) -> bool) -> (α -> β) -> bool
measurable_sets	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> bool) -> bool
measure	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> bool) -> real
measure_preserving	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (β -> bool) # ((β -> bool) -> bool) # ((β -> bool) -> real) -> (α -> β) -> bool
measure_space	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> bool
null_set	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> bool) -> bool
outer_measure_space	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> bool
pos_simple_fn	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> extreal) -> (num -> bool) -> (num -> α -> bool) -> (num -> real) -> bool
positive	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> bool
sigma	:(α -> bool) -> ((α -> bool) -> bool) -> (α -> bool) # ((α -> bool) -> bool)
sigma_algebra	:(α -> bool) # ((α -> bool) -> bool) -> bool
smallest_closed_cdi	:(α -> bool) # ((α -> bool) -> bool) -> (α -> bool) # ((α -> bool) -> bool)
space	:(α -> bool) # ((α -> bool) -> bool) -> α -> bool
subadditive	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> bool
subset_class	:(α -> bool) -> ((α -> bool) -> bool) -> bool
subsets	:(α -> bool) # ((α -> bool) -> bool) -> (α -> bool) -> bool

Definitions

subsets_def

⊢ ∀x y. subsets (x,y) = y

subset_class_def

⊢ ∀sp sts. subset_class sp sts ⇔ ∀x. x ∈ sts ⇒ x ⊆ sp

subadditive_def

⊢ ∀m.
      subadditive m ⇔
      ∀s t.
          s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
          measure m (s ∪ t) ≤ measure m s + measure m t

space_def

⊢ ∀x y. space (x,y) = x

smallest_closed_cdi_def

⊢ ∀a.
      smallest_closed_cdi a =
      (space a,BIGINTER {b | subsets a ⊆ b ∧ closed_cdi (space a,b)})

sigma_def

⊢ ∀sp st. sigma sp st = (sp,BIGINTER {s | st ⊆ s ∧ sigma_algebra (sp,s)})

sigma_algebra_def

⊢ ∀a.
      sigma_algebra a ⇔
      algebra a ∧ ∀c. COUNTABLE c ∧ c ⊆ subsets a ⇒ BIGUNION c ∈ subsets a

positive_def

⊢ ∀m.
      positive m ⇔
      (measure m ∅ = 0) ∧ ∀s. s ∈ measurable_sets m ⇒ 0 ≤ measure m s

pos_simple_fn_def

⊢ ∀m f s a x.
      pos_simple_fn m f s a x ⇔
      (∀t. 0 ≤ f t) ∧
      (∀t.
           t ∈ m_space m ⇒
           (f t = SIGMA (λi. Normal (x i) * indicator_fn (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)

outer_measure_space_def

⊢ ∀m.
      outer_measure_space m ⇔
      positive m ∧ increasing m ∧ countably_subadditive m

null_set_def

⊢ ∀m s. null_set m s ⇔ s ∈ measurable_sets m ∧ (measure m s = 0)

measure_space_def

⊢ ∀m.
      measure_space m ⇔
      sigma_algebra (m_space m,measurable_sets m) ∧ positive m ∧
      countably_additive m

measure_preserving_def

⊢ ∀m1 m2.
      measure_preserving m1 m2 =
      {f |
       f ∈
       measurable (m_space m1,measurable_sets m1)
         (m_space m2,measurable_sets m2) ∧ measure_space m1 ∧
       measure_space m2 ∧
       ∀s.
           s ∈ measurable_sets m2 ⇒
           (measure m1 (PREIMAGE f s ∩ m_space m1) = measure m2 s)}

measure_def

⊢ ∀sp sts mu. measure (sp,sts,mu) = mu

measurable_sets_def

⊢ ∀sp sts mu. measurable_sets (sp,sts,mu) = sts

measurable_def

⊢ ∀a b.
      measurable a b =
      {f |
       sigma_algebra a ∧ sigma_algebra b ∧ f ∈ (space a -> space b) ∧
       ∀s. s ∈ subsets b ⇒ PREIMAGE f s ∩ space a ∈ subsets a}

m_space_def

⊢ ∀sp sts mu. m_space (sp,sts,mu) = sp

lambda_system_def

⊢ ∀gen lam.
      lambda_system gen lam =
      {l |
       l ∈ subsets gen ∧
       ∀s.
           s ∈ subsets gen ⇒
           (lam (l ∩ s) + lam ((space gen DIFF l) ∩ s) = lam s)}

inf_measure_def

⊢ ∀m s.
      inf_measure m s =
      inf
        {r |
         (∃f.
              f ∈ (𝕌(:num) -> measurable_sets m) ∧
              (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ∧
              s ⊆ BIGUNION (IMAGE f 𝕌(:num)) ∧ measure m ∘ f sums r)}

indicator_fn_def

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

increasing_def

⊢ ∀m.
      increasing m ⇔
      ∀s t.
          s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧ s ⊆ t ⇒
          measure m s ≤ measure m t

fn_plus_def

⊢ ∀f. fn_plus f = (λx. if 0 < f x then f x else 0)

fn_minus_def

⊢ ∀f. fn_minus f = (λx. if f x < 0 then -f x else 0)

fn_abs_def

⊢ ∀f. fn_abs f = (λx. abs (f x))

countably_subadditive_def

⊢ ∀m.
      countably_subadditive m ⇔
      ∀f.
          f ∈ (𝕌(:num) -> measurable_sets m) ∧
          BIGUNION (IMAGE f 𝕌(:num)) ∈ measurable_sets m ∧
          summable (measure m ∘ f) ⇒
          measure m (BIGUNION (IMAGE f 𝕌(:num))) ≤ suminf (measure m ∘ f)

countably_additive_def

⊢ ∀m.
      countably_additive m ⇔
      ∀f.
          f ∈ (𝕌(:num) -> measurable_sets m) ∧
          (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ∧
          BIGUNION (IMAGE f 𝕌(:num)) ∈ measurable_sets m ⇒
          measure m ∘ f sums measure m (BIGUNION (IMAGE f 𝕌(:num)))

closed_cdi_def

⊢ ∀p.
      closed_cdi p ⇔
      subset_class (space p) (subsets p) ∧
      (∀s. s ∈ subsets p ⇒ space p DIFF s ∈ subsets p) ∧
      (∀f.
           f ∈ (𝕌(:num) -> subsets p) ∧ (f 0 = ∅) ∧ (∀n. f n ⊆ f (SUC n)) ⇒
           BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets p) ∧
      ∀f.
          f ∈ (𝕌(:num) -> subsets p) ∧ (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
          BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets p

Borel_def

⊢ Borel = sigma 𝕌(:extreal) (IMAGE (λa. {x | x < a}) 𝕌(:extreal))

algebra_def

⊢ ∀a.
      algebra a ⇔
      subset_class (space a) (subsets a) ∧ ∅ ∈ subsets a ∧
      (∀s. s ∈ subsets a ⇒ space a DIFF s ∈ subsets a) ∧
      ∀s t. s ∈ subsets a ∧ t ∈ subsets a ⇒ s ∪ t ∈ subsets a

additive_def

⊢ ∀m.
      additive m ⇔
      ∀s t.
          s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧ DISJOINT s t ⇒
          (measure m (s ∪ t) = measure m s + measure m t)

Theorems

UNIV_SIGMA_ALGEBRA

⊢ sigma_algebra (𝕌(:α),𝕌(:α -> bool))

SUBSET_BIGINTER

⊢ ∀X P. X ⊆ BIGINTER P ⇔ ∀Y. Y ∈ P ⇒ X ⊆ Y

SUBADDITIVE

⊢ ∀m s t u.
      subadditive m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧
      (u = s ∪ t) ⇒
      measure m u ≤ measure m s + measure m t

STRONG_MEASURE_SPACE_SUBSET

⊢ ∀s s'.
      s' ⊆ m_space s ∧ measure_space s ∧ POW s' ⊆ measurable_sets s ⇒
      measure_space (s',POW s',measure s)

SPACE_SMALLEST_CLOSED_CDI

⊢ ∀a. space (smallest_closed_cdi a) = space a

SPACE_SIGMA

⊢ ∀sp a. space (sigma sp a) = sp

SPACE_BOREL

⊢ space Borel = 𝕌(:extreal)

SPACE

⊢ ∀a. (space a,subsets a) = a

SMALLEST_CLOSED_CDI

⊢ ∀a.
      algebra a ⇒
      subsets a ⊆ subsets (smallest_closed_cdi a) ∧
      closed_cdi (smallest_closed_cdi a) ∧
      subset_class (space a) (subsets (smallest_closed_cdi a))

SIGMA_SUBSET_SUBSETS

⊢ ∀sp a. a ⊆ subsets (sigma sp a)

SIGMA_SUBSET_MEASURABLE_SETS

⊢ ∀a m.
      measure_space m ∧ a ⊆ measurable_sets m ⇒
      subsets (sigma (m_space m) a) ⊆ measurable_sets m

SIGMA_SUBSET

⊢ ∀a b.
      sigma_algebra b ∧ a ⊆ subsets b ⇒
      subsets (sigma (space b) a) ⊆ subsets b

SIGMA_REDUCE

⊢ ∀sp a. (sp,subsets (sigma sp a)) = sigma sp a

SIGMA_PROPERTY_DISJOINT_WEAK

⊢ ∀sp p a.
      algebra (sp,a) ∧ a ⊆ p ∧ subset_class sp p ∧
      (∀s. s ∈ p ⇒ sp DIFF s ∈ p) ∧
      (∀f.
           f ∈ (𝕌(:num) -> p) ∧ (f 0 = ∅) ∧ (∀n. f n ⊆ f (SUC n)) ⇒
           BIGUNION (IMAGE f 𝕌(:num)) ∈ p) ∧
      (∀f.
           f ∈ (𝕌(:num) -> p) ∧ (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
           BIGUNION (IMAGE f 𝕌(:num)) ∈ p) ⇒
      subsets (sigma sp a) ⊆ p

SIGMA_PROPERTY_DISJOINT_LEMMA2

⊢ ∀a.
      algebra a ⇒
      ∀s t.
          s ∈ subsets (smallest_closed_cdi a) ∧
          t ∈ subsets (smallest_closed_cdi a) ⇒
          s ∩ t ∈ subsets (smallest_closed_cdi a)

SIGMA_PROPERTY_DISJOINT_LEMMA1

⊢ ∀a.
      algebra a ⇒
      ∀s t.
          s ∈ subsets a ∧ t ∈ subsets (smallest_closed_cdi a) ⇒
          s ∩ t ∈ subsets (smallest_closed_cdi a)

SIGMA_PROPERTY_DISJOINT_LEMMA

⊢ ∀sp a p.
      algebra (sp,a) ∧ a ⊆ p ∧ closed_cdi (sp,p) ⇒ subsets (sigma sp a) ⊆ p

SIGMA_PROPERTY_DISJOINT

⊢ ∀sp p a.
      algebra (sp,a) ∧ a ⊆ p ∧
      (∀s. s ∈ p ∩ subsets (sigma sp a) ⇒ sp DIFF s ∈ p) ∧
      (∀f.
           f ∈ (𝕌(:num) -> p ∩ subsets (sigma sp a)) ∧ (f 0 = ∅) ∧
           (∀n. f n ⊆ f (SUC n)) ⇒
           BIGUNION (IMAGE f 𝕌(:num)) ∈ p) ∧
      (∀f.
           f ∈ (𝕌(:num) -> p ∩ subsets (sigma sp a)) ∧
           (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
           BIGUNION (IMAGE f 𝕌(:num)) ∈ p) ⇒
      subsets (sigma sp a) ⊆ p

SIGMA_PROPERTY_ALT

⊢ ∀sp p a.
      subset_class sp p ∧ ∅ ∈ p ∧ a ⊆ p ∧
      (∀s. s ∈ p ∩ subsets (sigma sp a) ⇒ sp DIFF s ∈ p) ∧
      (∀f.
           f ∈ (𝕌(:num) -> p ∩ subsets (sigma sp a)) ⇒
           BIGUNION (IMAGE f 𝕌(:num)) ∈ p) ⇒
      subsets (sigma sp a) ⊆ p

SIGMA_PROPERTY

⊢ ∀sp p a.
      subset_class sp p ∧ ∅ ∈ p ∧ a ⊆ p ∧
      (∀s. s ∈ p ∩ subsets (sigma sp a) ⇒ sp DIFF s ∈ p) ∧
      (∀c. COUNTABLE c ∧ c ⊆ p ∩ subsets (sigma sp a) ⇒ BIGUNION c ∈ p) ⇒
      subsets (sigma sp a) ⊆ p

SIGMA_POW

⊢ ∀s. sigma s (POW s) = (s,POW s)

SIGMA_ALGEBRA_SIGMA

⊢ ∀sp sts. subset_class sp sts ⇒ sigma_algebra (sigma sp sts)

SIGMA_ALGEBRA_FN_DISJOINT

⊢ ∀a.
      sigma_algebra a ⇔
      subset_class (space a) (subsets a) ∧ ∅ ∈ subsets a ∧
      (∀s. s ∈ subsets a ⇒ space a DIFF s ∈ subsets a) ∧
      (∀s t. s ∈ subsets a ∧ t ∈ subsets a ⇒ s ∪ t ∈ subsets a) ∧
      ∀f.
          f ∈ (𝕌(:num) -> subsets a) ∧ (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
          BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets a

SIGMA_ALGEBRA_FN_BIGINTER

⊢ ∀a.
      sigma_algebra a ⇒
      subset_class (space a) (subsets a) ∧ ∅ ∈ subsets a ∧
      (∀s. s ∈ subsets a ⇒ space a DIFF s ∈ subsets a) ∧
      ∀f. f ∈ (𝕌(:num) -> subsets a) ⇒ BIGINTER (IMAGE f 𝕌(:num)) ∈ subsets a

SIGMA_ALGEBRA_FN

⊢ ∀a.
      sigma_algebra a ⇔
      subset_class (space a) (subsets a) ∧ ∅ ∈ subsets a ∧
      (∀s. s ∈ subsets a ⇒ space a DIFF s ∈ subsets a) ∧
      ∀f. f ∈ (𝕌(:num) -> subsets a) ⇒ BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets a

SIGMA_ALGEBRA_ENUM

⊢ ∀a f.
      sigma_algebra a ∧ f ∈ (𝕌(:num) -> subsets a) ⇒
      BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets a

SIGMA_ALGEBRA_COUNTABLE_UNION

⊢ ∀a c. sigma_algebra a ∧ COUNTABLE c ∧ c ⊆ subsets a ⇒ BIGUNION c ∈ subsets a

SIGMA_ALGEBRA_BOREL

⊢ sigma_algebra Borel

SIGMA_ALGEBRA_ALT_MONO

⊢ ∀a.
      sigma_algebra a ⇔
      algebra a ∧
      ∀f.
          f ∈ (𝕌(:num) -> subsets a) ∧ (f 0 = ∅) ∧ (∀n. f n ⊆ f (SUC n)) ⇒
          BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets a

SIGMA_ALGEBRA_ALT_DISJOINT

⊢ ∀a.
      sigma_algebra a ⇔
      algebra a ∧
      ∀f.
          f ∈ (𝕌(:num) -> subsets a) ∧ (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
          BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets a

SIGMA_ALGEBRA_ALT

⊢ ∀a.
      sigma_algebra a ⇔
      algebra a ∧
      ∀f. f ∈ (𝕌(:num) -> subsets a) ⇒ BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets a

SIGMA_ALGEBRA_ALGEBRA

⊢ ∀a. sigma_algebra a ⇒ algebra a

SIGMA_ALGEBRA

⊢ ∀p.
      sigma_algebra p ⇔
      subset_class (space p) (subsets p) ∧ ∅ ∈ subsets p ∧
      (∀s. s ∈ subsets p ⇒ space p DIFF s ∈ subsets p) ∧
      ∀c. COUNTABLE c ∧ c ⊆ subsets p ⇒ BIGUNION c ∈ subsets p

POW_SIGMA_ALGEBRA

⊢ sigma_algebra (sp,POW sp)

POW_ALGEBRA

⊢ algebra (sp,POW sp)

OUTER_MEASURE_SPACE_POSITIVE

⊢ ∀m. outer_measure_space m ⇒ positive m

MONOTONE_CONVERGENCE_BIGINTER2

⊢ ∀m f.
      measure_space m ∧ f ∈ (𝕌(:num) -> measurable_sets m) ∧
      (∀n. f (SUC n) ⊆ f n) ⇒
      measure m ∘ f --> measure m (BIGINTER (IMAGE f 𝕌(:num)))

MONOTONE_CONVERGENCE_BIGINTER

⊢ ∀m s f.
      measure_space m ∧ f ∈ (𝕌(:num) -> measurable_sets m) ∧
      (∀n. f (SUC n) ⊆ f n) ∧ (s = BIGINTER (IMAGE f 𝕌(:num))) ⇒
      measure m ∘ f --> measure m s

MONOTONE_CONVERGENCE2

⊢ ∀m f.
      measure_space m ∧ f ∈ (𝕌(:num) -> measurable_sets m) ∧
      (∀n. f n ⊆ f (SUC n)) ⇒
      measure m ∘ f --> measure m (BIGUNION (IMAGE f 𝕌(:num)))

MONOTONE_CONVERGENCE

⊢ ∀m s f.
      measure_space m ∧ f ∈ (𝕌(:num) -> measurable_sets m) ∧
      (∀n. f n ⊆ f (SUC n)) ∧ (s = BIGUNION (IMAGE f 𝕌(:num))) ⇒
      measure m ∘ f --> measure m s

measure_split

⊢ ∀r b m.
      measure_space m ∧ FINITE r ∧ (BIGUNION (IMAGE b r) = m_space m) ∧
      (∀i j. i ∈ r ∧ j ∈ r ∧ i ≠ j ⇒ DISJOINT (b i) (b j)) ∧
      (∀i. i ∈ r ⇒ b i ∈ measurable_sets m) ⇒
      ∀a.
          a ∈ measurable_sets m ⇒
          (measure m a = SIGMA (λi. measure m (a ∩ b i)) r)

MEASURE_SPACE_UNION

⊢ ∀m s t.
      measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
      s ∪ t ∈ measurable_sets m

MEASURE_SPACE_SUBSET_MSPACE

⊢ ∀A m. measure_space m ∧ A ∈ measurable_sets m ⇒ A ⊆ m_space m

MEASURE_SPACE_SUBSET

⊢ ∀s s' m. s' ⊆ s ∧ measure_space (s,POW s,m) ⇒ measure_space (s',POW s',m)

MEASURE_SPACE_RESTRICTED

⊢ ∀m s.
      measure_space m ∧ s ∈ measurable_sets m ⇒
      measure_space (s,IMAGE (λt. s ∩ t) (measurable_sets m),measure m)

MEASURE_SPACE_REDUCE

⊢ ∀m. (m_space m,measurable_sets m,measure m) = m

MEASURE_SPACE_POSITIVE

⊢ ∀m. measure_space m ⇒ positive m

MEASURE_SPACE_MSPACE_MEASURABLE

⊢ ∀m. measure_space m ⇒ m_space m ∈ measurable_sets m

MEASURE_SPACE_INTER

⊢ ∀m s t.
      measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
      s ∩ t ∈ measurable_sets m

MEASURE_SPACE_INCREASING

⊢ ∀m. measure_space m ⇒ increasing m

MEASURE_SPACE_IN_MSPACE

⊢ ∀m A. measure_space m ∧ A ∈ measurable_sets m ⇒ ∀x. x ∈ A ⇒ x ∈ m_space m

MEASURE_SPACE_EMPTY_MEASURABLE

⊢ ∀m. measure_space m ⇒ ∅ ∈ measurable_sets m

MEASURE_SPACE_DIFF

⊢ ∀m s t.
      measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
      s DIFF t ∈ measurable_sets m

MEASURE_SPACE_CMUL

⊢ ∀m c.
      measure_space m ∧ 0 ≤ c ⇒
      measure_space (m_space m,measurable_sets m,(λa. c * measure m a))

MEASURE_SPACE_BIGUNION

⊢ ∀m s.
      measure_space m ∧ (∀n. s n ∈ measurable_sets m) ⇒
      BIGUNION (IMAGE s 𝕌(:num)) ∈ measurable_sets m

MEASURE_SPACE_BIGINTER

⊢ ∀m s.
      measure_space m ∧ (∀n. s n ∈ measurable_sets m) ⇒
      BIGINTER (IMAGE s 𝕌(:num)) ∈ measurable_sets m

MEASURE_SPACE_ADDITIVE

⊢ ∀m. measure_space m ⇒ additive m

MEASURE_REAL_SUM_IMAGE

⊢ ∀m s.
      measure_space m ∧ s ∈ measurable_sets m ∧
      (∀x. x ∈ s ⇒ {x} ∈ measurable_sets m) ∧ FINITE s ⇒
      (measure m s = SIGMA (λx. measure m {x}) s)

MEASURE_PRESERVING_UP_SUBSET

⊢ ∀m1 m2.
      measure_space m1 ∧ a ⊆ measurable_sets m1 ∧
      sigma_algebra (m_space m1,measurable_sets m1) ⇒
      measure_preserving (m_space m1,a,measure m1) m2 ⊆
      measure_preserving m1 m2

MEASURE_PRESERVING_UP_SIGMA

⊢ ∀m1 m2 a.
      measure_space m1 ∧ (measurable_sets m1 = subsets (sigma (m_space m1) a)) ⇒
      measure_preserving (m_space m1,a,measure m1) m2 ⊆
      measure_preserving m1 m2

MEASURE_PRESERVING_UP_LIFT

⊢ ∀m1 m2 f.
      measure_space m1 ∧ f ∈ measure_preserving (m_space m1,a,measure m1) m2 ∧
      sigma_algebra (m_space m1,measurable_sets m1) ∧ a ⊆ measurable_sets m1 ⇒
      f ∈ measure_preserving m1 m2

MEASURE_PRESERVING_SUBSET

⊢ ∀m1 m2 a.
      measure_space m1 ∧ measure_space m2 ∧
      (measurable_sets m2 = subsets (sigma (m_space m2) a)) ⇒
      measure_preserving m1 (m_space m2,a,measure m2) ⊆
      measure_preserving m1 m2

MEASURE_PRESERVING_LIFT

⊢ ∀m1 m2 a f.
      measure_space m1 ∧ measure_space m2 ∧
      (measurable_sets m2 = subsets (sigma (m_space m2) a)) ∧
      f ∈ measure_preserving m1 (m_space m2,a,measure m2) ⇒
      f ∈ measure_preserving m1 m2

MEASURE_EMPTY

⊢ ∀m. measure_space m ⇒ (measure m ∅ = 0)

MEASURE_DOWN

⊢ ∀m0 m1.
      sigma_algebra (m_space m0,measurable_sets m0) ∧
      measurable_sets m0 ⊆ measurable_sets m1 ∧ (measure m0 = measure m1) ∧
      measure_space m1 ⇒
      measure_space m0

MEASURE_COUNTABLY_ADDITIVE

⊢ ∀m s f.
      measure_space m ∧ f ∈ (𝕌(:num) -> measurable_sets m) ∧
      (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ∧ (s = BIGUNION (IMAGE f 𝕌(:num))) ⇒
      measure m ∘ f sums measure m s

MEASURE_COUNTABLE_INCREASING

⊢ ∀m s f.
      measure_space m ∧ f ∈ (𝕌(:num) -> measurable_sets m) ∧ (f 0 = ∅) ∧
      (∀n. f n ⊆ f (SUC n)) ∧ (s = BIGUNION (IMAGE f 𝕌(:num))) ⇒
      measure m ∘ f --> measure m s

MEASURE_COMPL_SUBSET

⊢ ∀m s.
      measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧ t ⊆ s ⇒
      (measure m (s DIFF t) = measure m s − measure m t)

MEASURE_COMPL

⊢ ∀m s.
      measure_space m ∧ s ∈ measurable_sets m ⇒
      (measure m (m_space m DIFF s) = measure m (m_space m) − measure m s)

MEASURE_ADDITIVE

⊢ ∀m s t u.
      measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧
      DISJOINT s t ∧ (u = s ∪ t) ⇒
      (measure m u = measure m s + measure m t)

MEASURABLE_UP_SUBSET

⊢ ∀sp a b c.
      a ⊆ b ∧ sigma_algebra (sp,b) ⇒ measurable (sp,a) c ⊆ measurable (sp,b) c

MEASURABLE_UP_SIGMA

⊢ ∀a b. measurable a b ⊆ measurable (sigma (space a) (subsets a)) b

MEASURABLE_UP_LIFT

⊢ ∀sp a b c f.
      f ∈ measurable (sp,a) c ∧ sigma_algebra (sp,b) ∧ a ⊆ b ⇒
      f ∈ measurable (sp,b) c

MEASURABLE_SUBSET

⊢ ∀a b. measurable a b ⊆ measurable a (sigma (space b) (subsets b))

MEASURABLE_SIGMA_PREIMAGES

⊢ ∀a b f.
      sigma_algebra a ∧ sigma_algebra b ∧ f ∈ (space a -> space b) ∧
      (∀s. s ∈ subsets b ⇒ PREIMAGE f s ∈ subsets a) ⇒
      sigma_algebra (space a,IMAGE (PREIMAGE f) (subsets b))

MEASURABLE_SIGMA

⊢ ∀f a b sp.
      sigma_algebra a ∧ subset_class sp b ∧ f ∈ (space a -> sp) ∧
      (∀s. s ∈ b ⇒ PREIMAGE f s ∩ space a ∈ subsets a) ⇒
      f ∈ measurable a (sigma sp b)

MEASURABLE_SETS_SUBSET_SPACE

⊢ ∀m s. measure_space m ∧ s ∈ measurable_sets m ⇒ s ⊆ m_space m

MEASURABLE_RANGE_REDUCE

⊢ ∀m f s.
      measure_space m ∧
      f ∈ measurable (m_space m,measurable_sets m) (s,POW s) ∧ s ≠ ∅ ⇒
      f ∈
      measurable (m_space m,measurable_sets m)
        (s ∩ IMAGE f (m_space m),POW (s ∩ IMAGE f (m_space m)))

MEASURABLE_PROD_SIGMA

⊢ ∀a a1 a2 f.
      sigma_algebra a ∧ FST ∘ f ∈ measurable a a1 ∧ SND ∘ f ∈ measurable a a2 ⇒
      f ∈
      measurable a
        (sigma (space a1 × space a2) (prod_sets (subsets a1) (subsets a2)))

MEASURABLE_POW_TO_POW_IMAGE

⊢ ∀m f.
      measure_space m ∧ (measurable_sets m = POW (m_space m)) ⇒
      f ∈
      measurable (m_space m,measurable_sets m)
        (IMAGE f (m_space m),POW (IMAGE f (m_space m)))

MEASURABLE_POW_TO_POW

⊢ ∀m f.
      measure_space m ∧ (measurable_sets m = POW (m_space m)) ⇒
      f ∈ measurable (m_space m,measurable_sets m) (𝕌(:β),POW 𝕌(:β))

MEASURABLE_LIFT

⊢ ∀f a b. f ∈ measurable a b ⇒ f ∈ measurable a (sigma (space b) (subsets b))

MEASURABLE_I

⊢ ∀a. sigma_algebra a ⇒ I ∈ measurable a a

MEASURABLE_DIFF_PROPERTY

⊢ ∀a b f.
      sigma_algebra a ∧ sigma_algebra b ∧ f ∈ (space a -> space b) ∧
      (∀s. s ∈ subsets b ⇒ PREIMAGE f s ∈ subsets a) ⇒
      ∀s.
          s ∈ subsets b ⇒
          (PREIMAGE f (space b DIFF s) = space a DIFF PREIMAGE f s)

MEASURABLE_COMP_STRONGER

⊢ ∀f g a b c t.
      f ∈ measurable a b ∧ sigma_algebra c ∧ g ∈ (space b -> space c) ∧
      IMAGE f (space a) ⊆ t ∧
      (∀s. s ∈ subsets c ⇒ PREIMAGE g s ∩ t ∈ subsets b) ⇒
      g ∘ f ∈ measurable a c

MEASURABLE_COMP_STRONG

⊢ ∀f g a b c.
      f ∈ measurable a b ∧ sigma_algebra c ∧ g ∈ (space b -> space c) ∧
      (∀x. x ∈ subsets c ⇒ PREIMAGE g x ∩ IMAGE f (space a) ∈ subsets b) ⇒
      g ∘ f ∈ measurable a c

MEASURABLE_COMP

⊢ ∀f g a b c. f ∈ measurable a b ∧ g ∈ measurable b c ⇒ g ∘ f ∈ measurable a c

MEASURABLE_BOREL

⊢ ∀f a.
      f ∈ measurable a Borel ⇔
      sigma_algebra a ∧ f ∈ (space a -> 𝕌(:extreal)) ∧
      ∀c. PREIMAGE f {x | x < c} ∩ space a ∈ subsets a

MEASURABLE_BIGUNION_PROPERTY

⊢ ∀a b f.
      sigma_algebra a ∧ sigma_algebra b ∧ f ∈ (space a -> space b) ∧
      (∀s. s ∈ subsets b ⇒ PREIMAGE f s ∈ subsets a) ⇒
      ∀c.
          c ⊆ subsets b ⇒
          (PREIMAGE f (BIGUNION c) = BIGUNION (IMAGE (PREIMAGE f) c))

MEASUBABLE_BIGUNION_LEMMA

⊢ ∀a b f.
      sigma_algebra a ∧ sigma_algebra b ∧ f ∈ (space a -> space b) ∧
      (∀s. s ∈ subsets b ⇒ PREIMAGE f s ∈ subsets a) ⇒
      ∀c.
          COUNTABLE c ∧ c ⊆ IMAGE (PREIMAGE f) (subsets b) ⇒
          BIGUNION c ∈ IMAGE (PREIMAGE f) (subsets b)

LAMBDA_SYSTEM_STRONG_SUM

⊢ ∀g0 lam g f n.
      algebra g0 ∧ positive (space g0,subsets g0,lam) ∧ g ∈ subsets g0 ∧
      f ∈ (𝕌(:num) -> lambda_system g0 lam) ∧
      (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
      (sum (0,n) (lam ∘ (λs. s ∩ g) ∘ f) =
       lam (BIGUNION (IMAGE f (count n)) ∩ g))

LAMBDA_SYSTEM_STRONG_ADDITIVE

⊢ ∀g0 lam g l1 l2.
      algebra g0 ∧ positive (space g0,subsets g0,lam) ∧ g ∈ subsets g0 ∧
      DISJOINT l1 l2 ∧ l1 ∈ lambda_system g0 lam ∧ l2 ∈ lambda_system g0 lam ⇒
      (lam ((l1 ∪ l2) ∩ g) = lam (l1 ∩ g) + lam (l2 ∩ g))

LAMBDA_SYSTEM_POSITIVE

⊢ ∀g0 lam.
      positive (space g0,subsets g0,lam) ⇒
      positive (space g0,lambda_system g0 lam,lam)

LAMBDA_SYSTEM_INTER

⊢ ∀g0 lam l1 l2.
      algebra g0 ∧ positive (space g0,subsets g0,lam) ∧
      l1 ∈ lambda_system g0 lam ∧ l2 ∈ lambda_system g0 lam ⇒
      l1 ∩ l2 ∈ lambda_system g0 lam

LAMBDA_SYSTEM_INCREASING

⊢ ∀g0 lam.
      increasing (space g0,subsets g0,lam) ⇒
      increasing (space g0,lambda_system g0 lam,lam)

LAMBDA_SYSTEM_EMPTY

⊢ ∀g0 lam.
      algebra g0 ∧ positive (space g0,subsets g0,lam) ⇒
      ∅ ∈ lambda_system g0 lam

LAMBDA_SYSTEM_COMPL

⊢ ∀g0 lam l.
      algebra g0 ∧ positive (space g0,subsets g0,lam) ∧
      l ∈ lambda_system g0 lam ⇒
      space g0 DIFF l ∈ lambda_system g0 lam

LAMBDA_SYSTEM_CARATHEODORY

⊢ ∀gsig lam.
      sigma_algebra gsig ∧ outer_measure_space (space gsig,subsets gsig,lam) ⇒
      ∀f.
          f ∈ (𝕌(:num) -> lambda_system gsig lam) ∧
          (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
          BIGUNION (IMAGE f 𝕌(:num)) ∈ lambda_system gsig lam ∧
          lam ∘ f sums lam (BIGUNION (IMAGE f 𝕌(:num)))

LAMBDA_SYSTEM_ALGEBRA

⊢ ∀g0 lam.
      algebra g0 ∧ positive (space g0,subsets g0,lam) ⇒
      algebra (space g0,lambda_system g0 lam)

LAMBDA_SYSTEM_ADDITIVE

⊢ ∀g0 lam l1 l2.
      algebra g0 ∧ positive (space g0,subsets g0,lam) ⇒
      additive (space g0,lambda_system g0 lam,lam)

INF_MEASURE_POSITIVE

⊢ ∀m.
      algebra (m_space m,measurable_sets m) ∧ positive m ⇒
      positive (m_space m,POW (m_space m),inf_measure m)

INF_MEASURE_POS0

⊢ ∀m g x.
      algebra (m_space m,measurable_sets m) ∧ positive m ∧
      x ∈
      {r |
       ∃f.
           f ∈ (𝕌(:num) -> measurable_sets m) ∧
           (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ∧
           g ⊆ BIGUNION (IMAGE f 𝕌(:num)) ∧ measure m ∘ f sums r} ⇒
      0 ≤ x

INF_MEASURE_POS

⊢ ∀m g.
      algebra (m_space m,measurable_sets m) ∧ positive m ∧ g ⊆ m_space m ⇒
      0 ≤ inf_measure m g

INF_MEASURE_OUTER

⊢ ∀m.
      algebra (m_space m,measurable_sets m) ∧ positive m ∧ increasing m ⇒
      outer_measure_space (m_space m,POW (m_space m),inf_measure m)

INF_MEASURE_NONEMPTY

⊢ ∀m g s.
      algebra (m_space m,measurable_sets m) ∧ positive m ∧
      s ∈ measurable_sets m ∧ g ⊆ s ⇒
      measure m s ∈
      {r |
       ∃f.
           f ∈ (𝕌(:num) -> measurable_sets m) ∧
           (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ∧
           g ⊆ BIGUNION (IMAGE f 𝕌(:num)) ∧ measure m ∘ f sums r}

INF_MEASURE_LE

⊢ ∀m s x.
      algebra (m_space m,measurable_sets m) ∧ positive m ∧ increasing m ∧
      x ∈
      {r |
       ∃f.
           f ∈ (𝕌(:num) -> measurable_sets m) ∧
           s ⊆ BIGUNION (IMAGE f 𝕌(:num)) ∧ measure m ∘ f sums r} ⇒
      inf_measure m s ≤ x

INF_MEASURE_INCREASING

⊢ ∀m.
      algebra (m_space m,measurable_sets m) ∧ positive m ⇒
      increasing (m_space m,POW (m_space m),inf_measure m)

INF_MEASURE_EMPTY

⊢ ∀m.
      algebra (m_space m,measurable_sets m) ∧ positive m ⇒
      (inf_measure m ∅ = 0)

INF_MEASURE_COUNTABLY_SUBADDITIVE

⊢ ∀m.
      algebra (m_space m,measurable_sets m) ∧ positive m ∧ increasing m ⇒
      countably_subadditive (m_space m,POW (m_space m),inf_measure m)

INF_MEASURE_CLOSE

⊢ ∀m s e.
      algebra (m_space m,measurable_sets m) ∧ positive m ∧ 0 < e ∧
      s ⊆ m_space m ⇒
      ∃f l.
          f ∈ (𝕌(:num) -> measurable_sets m) ∧
          s ⊆ BIGUNION (IMAGE f 𝕌(:num)) ∧
          (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ∧ measure m ∘ f sums l ∧
          l ≤ inf_measure m s + e

INF_MEASURE_AGREES

⊢ ∀m s.
      algebra (m_space m,measurable_sets m) ∧ positive m ∧
      countably_additive m ∧ s ∈ measurable_sets m ⇒
      (inf_measure m s = measure m s)

indicator_fn_suminf

⊢ ∀a x.
      (∀m n. m ≠ n ⇒ DISJOINT (a m) (a n)) ⇒
      (suminf (λi. indicator_fn (a i) x) =
       indicator_fn (BIGUNION (IMAGE a 𝕌(:num))) x)

indicator_fn_split

⊢ ∀r s b.
      FINITE r ∧ (BIGUNION (IMAGE b r) = s) ∧
      (∀i j. i ∈ r ∧ j ∈ r ∧ i ≠ j ⇒ DISJOINT (b i) (b j)) ⇒
      ∀a.
          a ⊆ s ⇒
          (indicator_fn a = (λx. SIGMA (λi. indicator_fn (a ∩ b i) x) r))

INDICATOR_FN_MUL_INTER

⊢ ∀A B.
      (λt. indicator_fn A t * indicator_fn B t) = (λt. indicator_fn (A ∩ B) t)

INCREASING_ADDITIVE_SUMMABLE

⊢ ∀m f.
      algebra (m_space m,measurable_sets m) ∧ positive m ∧ increasing m ∧
      additive m ∧ f ∈ (𝕌(:num) -> measurable_sets m) ∧
      (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
      summable (measure m ∘ f)

INCREASING

⊢ ∀m s t.
      increasing m ∧ s ⊆ t ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
      measure m s ≤ measure m t

IN_SIGMA

⊢ ∀sp a x. x ∈ a ⇒ x ∈ subsets (sigma sp a)

IN_MEASURE_PRESERVING

⊢ ∀m1 m2 f.
      f ∈ measure_preserving m1 m2 ⇔
      f ∈
      measurable (m_space m1,measurable_sets m1)
        (m_space m2,measurable_sets m2) ∧ measure_space m1 ∧
      measure_space m2 ∧
      ∀s.
          s ∈ measurable_sets m2 ⇒
          (measure m1 (PREIMAGE f s ∩ m_space m1) = measure m2 s)

IN_MEASURABLE_BOREL_SUM

⊢ ∀a f g s.
      FINITE s ∧ sigma_algebra a ∧ (∀i. i ∈ s ⇒ f i ∈ measurable a Borel) ∧
      (∀x. x ∈ space a ⇒ (g x = SIGMA (λi. f i x) s)) ⇒
      g ∈ measurable a Borel

IN_MEASURABLE_BOREL_SUB

⊢ ∀a f g h.
      sigma_algebra a ∧ f ∈ measurable a Borel ∧ g ∈ measurable a Borel ∧
      (∀x. x ∈ space a ⇒ (h x = f x − g x)) ⇒
      h ∈ measurable a Borel

IN_MEASURABLE_BOREL_SQR

⊢ ∀a f g.
      sigma_algebra a ∧ f ∈ measurable a Borel ∧
      (∀x. x ∈ space a ⇒ (g x = f x pow 2)) ⇒
      g ∈ measurable a Borel

IN_MEASURABLE_BOREL_POW

⊢ ∀n a f.
      sigma_algebra a ∧ f ∈ measurable a Borel ∧
      (∀x. x ∈ space a ⇒ f x ≠ NegInf ∧ f x ≠ PosInf) ⇒
      (λx. f x pow n) ∈ measurable a Borel

IN_MEASURABLE_BOREL_POS_SIMPLE_FN

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

IN_MEASURABLE_BOREL_PLUS_MINUS

⊢ ∀a f.
      f ∈ measurable a Borel ⇔
      fn_plus f ∈ measurable a Borel ∧ fn_minus f ∈ measurable a Borel

IN_MEASURABLE_BOREL_NEGINF

⊢ ∀f a. f ∈ measurable a Borel ⇒ {x | f x = NegInf} ∩ space a ∈ subsets a

IN_MEASURABLE_BOREL_MUL_INDICATOR_EQ

⊢ ∀a f.
      sigma_algebra a ⇒
      (f ∈ measurable a Borel ⇔
       (λx. f x * indicator_fn (space a) x) ∈ measurable a Borel)

IN_MEASURABLE_BOREL_MUL_INDICATOR

⊢ ∀a f s.
      sigma_algebra a ∧ f ∈ measurable a Borel ∧ s ∈ subsets a ⇒
      (λx. f x * indicator_fn s x) ∈ measurable a Borel

IN_MEASURABLE_BOREL_MUL

⊢ ∀a f g h.
      sigma_algebra a ∧ f ∈ measurable a Borel ∧
      (∀x.
           x ∈ space a ⇒
           f x ≠ NegInf ∧ f x ≠ PosInf ∧ g x ≠ NegInf ∧ g x ≠ PosInf) ∧
      g ∈ measurable a Borel ∧ (∀x. x ∈ space a ⇒ (h x = f x * g x)) ⇒
      h ∈ measurable a Borel

IN_MEASURABLE_BOREL_MONO_SUP

⊢ ∀fn f a.
      sigma_algebra a ∧ (∀n. fn n ∈ measurable a Borel) ∧
      (∀n x. x ∈ space a ⇒ fn n x ≤ fn (SUC n) x) ∧
      (∀x. x ∈ space a ⇒ (f x = sup (IMAGE (λn. fn n x) 𝕌(:num)))) ⇒
      f ∈ measurable a Borel

IN_MEASURABLE_BOREL_MAX

⊢ ∀a f g.
      sigma_algebra a ∧ f ∈ measurable a Borel ∧ g ∈ measurable a Borel ⇒
      (λx. max (f x) (g x)) ∈ measurable a Borel

IN_MEASURABLE_BOREL_LT

⊢ ∀f g a.
      f ∈ measurable a Borel ∧ g ∈ measurable a Borel ⇒
      {x | f x < g x} ∩ space a ∈ subsets a

IN_MEASURABLE_BOREL_LE

⊢ ∀f g a.
      f ∈ measurable a Borel ∧ g ∈ measurable a Borel ⇒
      {x | f x ≤ g x} ∩ space a ∈ subsets a

IN_MEASURABLE_BOREL_INDICATOR

⊢ ∀a A f.
      sigma_algebra a ∧ A ∈ subsets a ∧
      (∀x. x ∈ space a ⇒ (f x = indicator_fn A x)) ⇒
      f ∈ measurable a Borel

IN_MEASURABLE_BOREL_FN_PLUS

⊢ ∀a f. f ∈ measurable a Borel ⇒ fn_plus f ∈ measurable a Borel

IN_MEASURABLE_BOREL_FN_MINUS

⊢ ∀a f. f ∈ measurable a Borel ⇒ fn_minus f ∈ measurable a Borel

IN_MEASURABLE_BOREL_CONST

⊢ ∀a k f.
      sigma_algebra a ∧ (∀x. x ∈ space a ⇒ (f x = k)) ⇒ f ∈ measurable a Borel

IN_MEASURABLE_BOREL_CMUL_INDICATOR

⊢ ∀a z s.
      sigma_algebra a ∧ s ∈ subsets a ⇒
      (λx. Normal z * indicator_fn s x) ∈ measurable a Borel

IN_MEASURABLE_BOREL_CMUL

⊢ ∀a f g z.
      sigma_algebra a ∧ f ∈ measurable a Borel ∧
      (∀x. x ∈ space a ⇒ (g x = Normal z * f x)) ⇒
      g ∈ measurable a Borel

IN_MEASURABLE_BOREL_ALT9

⊢ ∀f a.
      f ∈ measurable a Borel ⇒
      sigma_algebra a ∧ f ∈ (space a -> 𝕌(:extreal)) ∧
      ∀c. {x | f x ≠ c} ∩ space a ∈ subsets a

IN_MEASURABLE_BOREL_ALT8

⊢ ∀f a.
      f ∈ measurable a Borel ⇒
      sigma_algebra a ∧ f ∈ (space a -> 𝕌(:extreal)) ∧
      ∀c. {x | f x = c} ∩ space a ∈ subsets a

IN_MEASURABLE_BOREL_ALT7

⊢ ∀f a.
      f ∈ measurable a Borel ⇒
      sigma_algebra a ∧ f ∈ (space a -> 𝕌(:extreal)) ∧
      ∀c d. {x | c < f x ∧ f x < d} ∩ space a ∈ subsets a

IN_MEASURABLE_BOREL_ALT6

⊢ ∀f a.
      f ∈ measurable a Borel ⇔
      sigma_algebra a ∧ f ∈ (space a -> 𝕌(:extreal)) ∧
      ∀c d. {x | c ≤ f x ∧ f x ≤ d} ∩ space a ∈ subsets a

IN_MEASURABLE_BOREL_ALT5

⊢ ∀f a.
      f ∈ measurable a Borel ⇔
      sigma_algebra a ∧ f ∈ (space a -> 𝕌(:extreal)) ∧
      ∀c d. {x | c < f x ∧ f x ≤ d} ∩ space a ∈ subsets a

IN_MEASURABLE_BOREL_ALT4

⊢ ∀f a.
      f ∈ measurable a Borel ⇔
      sigma_algebra a ∧ f ∈ (space a -> 𝕌(:extreal)) ∧
      ∀c d. {x | c ≤ f x ∧ f x < d} ∩ space a ∈ subsets a

IN_MEASURABLE_BOREL_ALT3

⊢ ∀f a.
      f ∈ measurable a Borel ⇔
      sigma_algebra a ∧ f ∈ (space a -> 𝕌(:extreal)) ∧
      ∀c. {x | c < f x} ∩ space a ∈ subsets a

IN_MEASURABLE_BOREL_ALT2

⊢ ∀f a.
      f ∈ measurable a Borel ⇔
      sigma_algebra a ∧ f ∈ (space a -> 𝕌(:extreal)) ∧
      ∀c. {x | f x ≤ c} ∩ space a ∈ subsets a

IN_MEASURABLE_BOREL_ALT1

⊢ ∀f a.
      f ∈ measurable a Borel ⇔
      sigma_algebra a ∧ f ∈ (space a -> 𝕌(:extreal)) ∧
      ∀c. {x | c ≤ f x} ∩ space a ∈ subsets a

IN_MEASURABLE_BOREL_ALL_MEASURE

⊢ ∀f m.
      f ∈ measurable (m_space m,measurable_sets m) Borel ⇒
      (∀c. {x | f x < c} ∩ m_space m ∈ measurable_sets m) ∧
      (∀c. {x | c ≤ f x} ∩ m_space m ∈ measurable_sets m) ∧
      (∀c. {x | f x ≤ c} ∩ m_space m ∈ measurable_sets m) ∧
      (∀c. {x | c < f x} ∩ m_space m ∈ measurable_sets m) ∧
      (∀c d. {x | c < f x ∧ f x < d} ∩ m_space m ∈ measurable_sets m) ∧
      (∀c d. {x | c ≤ f x ∧ f x < d} ∩ m_space m ∈ measurable_sets m) ∧
      (∀c d. {x | c < f x ∧ f x ≤ d} ∩ m_space m ∈ measurable_sets m) ∧
      (∀c d. {x | c ≤ f x ∧ f x ≤ d} ∩ m_space m ∈ measurable_sets m) ∧
      (∀c. {x | f x = c} ∩ m_space m ∈ measurable_sets m) ∧
      ∀c. {x | f x ≠ c} ∩ m_space m ∈ measurable_sets m

IN_MEASURABLE_BOREL_ALL

⊢ ∀f a.
      f ∈ measurable a Borel ⇒
      (∀c. {x | f x < c} ∩ space a ∈ subsets a) ∧
      (∀c. {x | c ≤ f x} ∩ space a ∈ subsets a) ∧
      (∀c. {x | f x ≤ c} ∩ space a ∈ subsets a) ∧
      (∀c. {x | c < f x} ∩ space a ∈ subsets a) ∧
      (∀c d. {x | c < f x ∧ f x < d} ∩ space a ∈ subsets a) ∧
      (∀c d. {x | c ≤ f x ∧ f x < d} ∩ space a ∈ subsets a) ∧
      (∀c d. {x | c < f x ∧ f x ≤ d} ∩ space a ∈ subsets a) ∧
      (∀c d. {x | c ≤ f x ∧ f x ≤ d} ∩ space a ∈ subsets a) ∧
      (∀c. {x | f x ≠ c} ∩ space a ∈ subsets a) ∧
      ∀c. {x | f x = c} ∩ space a ∈ subsets a

IN_MEASURABLE_BOREL_ADD

⊢ ∀a f g h.
      sigma_algebra a ∧ f ∈ measurable a Borel ∧ g ∈ measurable a Borel ∧
      (∀x. x ∈ space a ⇒ (h x = f x + g x)) ⇒
      h ∈ measurable a Borel

IN_MEASURABLE_BOREL_ABS

⊢ ∀a f g.
      sigma_algebra a ∧ f ∈ measurable a Borel ∧
      (∀x. x ∈ space a ⇒ (g x = abs (f x))) ⇒
      g ∈ measurable a Borel

IN_MEASURABLE_BOREL

⊢ ∀f a.
      f ∈ measurable a Borel ⇔
      sigma_algebra a ∧ f ∈ (space a -> 𝕌(:extreal)) ∧
      ∀c. {x | f x < c} ∩ space a ∈ subsets a

IN_MEASURABLE

⊢ ∀a b f.
      f ∈ measurable a b ⇔
      sigma_algebra a ∧ sigma_algebra b ∧ f ∈ (space a -> space b) ∧
      ∀s. s ∈ subsets b ⇒ PREIMAGE f s ∩ space a ∈ subsets a

IMAGE_SING

⊢ ∀f x. IMAGE f {x} = {f x}

FN_PLUS_POS_ID

⊢ (∀x. 0 ≤ g x) ⇒ (fn_plus g = g)

FN_PLUS_POS

⊢ ∀g x. 0 ≤ fn_plus g x

FN_PLUS_CMUL

⊢ ∀f c.
      (0 ≤ c ⇒ (fn_plus (λx. Normal c * f x) = (λx. Normal c * fn_plus f x))) ∧
      (c ≤ 0 ⇒ (fn_plus (λx. Normal c * f x) = (λx. -Normal c * fn_minus f x)))

FN_PLUS_ADD_LE

⊢ ∀f g x. fn_plus (λx. f x + g x) x ≤ fn_plus f x + fn_plus g x

FN_MINUS_POS_ZERO

⊢ (∀x. 0 ≤ g x) ⇒ (fn_minus g = (λx. 0))

FN_MINUS_POS

⊢ ∀g x. 0 ≤ fn_minus g x

FN_MINUS_CMUL

⊢ ∀f c.
      (0 ≤ c ⇒ (fn_minus (λx. Normal c * f x) = (λx. Normal c * fn_minus f x))) ∧
      (c ≤ 0 ⇒ (fn_minus (λx. Normal c * f x) = (λx. -Normal c * fn_plus f x)))

FN_MINUS_ADD_LE

⊢ ∀f g x. fn_minus (λx. f x + g x) x ≤ fn_minus f x + fn_minus g x

finite_additivity_sufficient_for_finite_spaces2

⊢ ∀m.
      sigma_algebra (m_space m,measurable_sets m) ∧ FINITE (m_space m) ∧
      positive m ∧ additive m ⇒
      measure_space m

finite_additivity_sufficient_for_finite_spaces

⊢ ∀s m.
      sigma_algebra s ∧ FINITE (space s) ∧ positive (space s,subsets s,m) ∧
      additive (space s,subsets s,m) ⇒
      measure_space (space s,subsets s,m)

COUNTABLY_SUBADDITIVE_SUBADDITIVE

⊢ ∀m.
      algebra (m_space m,measurable_sets m) ∧ positive m ∧
      countably_subadditive m ⇒
      subadditive m

COUNTABLY_SUBADDITIVE

⊢ ∀m f s.
      countably_subadditive m ∧ f ∈ (𝕌(:num) -> measurable_sets m) ∧
      summable (measure m ∘ f) ∧ (s = BIGUNION (IMAGE f 𝕌(:num))) ∧
      s ∈ measurable_sets m ⇒
      measure m s ≤ suminf (measure m ∘ f)

COUNTABLY_ADDITIVE_ADDITIVE

⊢ ∀m.
      algebra (m_space m,measurable_sets m) ∧ positive m ∧
      countably_additive m ⇒
      additive m

COUNTABLY_ADDITIVE

⊢ ∀m s f.
      countably_additive m ∧ f ∈ (𝕌(:num) -> measurable_sets m) ∧
      (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ∧
      (s = BIGUNION (IMAGE f 𝕌(:num))) ∧ s ∈ measurable_sets m ⇒
      measure m ∘ f sums measure m s

CLOSED_CDI_INCREASING

⊢ ∀p f.
      closed_cdi p ∧ f ∈ (𝕌(:num) -> subsets p) ∧ (f 0 = ∅) ∧
      (∀n. f n ⊆ f (SUC n)) ⇒
      BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets p

CLOSED_CDI_DUNION

⊢ ∀p s t.
      ∅ ∈ subsets p ∧ closed_cdi p ∧ s ∈ subsets p ∧ t ∈ subsets p ∧
      DISJOINT s t ⇒
      s ∪ t ∈ subsets p

CLOSED_CDI_DISJOINT

⊢ ∀p f.
      closed_cdi p ∧ f ∈ (𝕌(:num) -> subsets p) ∧
      (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
      BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets p

CLOSED_CDI_COMPL

⊢ ∀p s. closed_cdi p ∧ s ∈ subsets p ⇒ space p DIFF s ∈ subsets p

CARATHEODORY_LEMMA

⊢ ∀gsig lam.
      sigma_algebra gsig ∧ outer_measure_space (space gsig,subsets gsig,lam) ⇒
      measure_space (space gsig,lambda_system gsig lam,lam)

CARATHEODORY

⊢ ∀m0.
      algebra (m_space m0,measurable_sets m0) ∧ positive m0 ∧
      countably_additive m0 ⇒
      ∃m.
          (∀s. s ∈ measurable_sets m0 ⇒ (measure m s = measure m0 s)) ∧
          ((m_space m,measurable_sets m) =
           sigma (m_space m0) (measurable_sets m0)) ∧ measure_space m

BOREL_MEASURABLE_SETS9

⊢ ∀c. {c} ∈ subsets Borel

BOREL_MEASURABLE_SETS8

⊢ ∀c d. {x | c < x ∧ x < d} ∈ subsets Borel

BOREL_MEASURABLE_SETS7

⊢ ∀c d. {x | c ≤ x ∧ x ≤ d} ∈ subsets Borel

BOREL_MEASURABLE_SETS6

⊢ ∀c d. {x | c < x ∧ x ≤ d} ∈ subsets Borel

BOREL_MEASURABLE_SETS5

⊢ ∀c d. {x | c ≤ x ∧ x < d} ∈ subsets Borel

BOREL_MEASURABLE_SETS4

⊢ ∀c. {x | c < x} ∈ subsets Borel

BOREL_MEASURABLE_SETS3

⊢ ∀c. {x | x ≤ c} ∈ subsets Borel

BOREL_MEASURABLE_SETS2

⊢ ∀c. {x | c ≤ x} ∈ subsets Borel

BOREL_MEASURABLE_SETS10

⊢ ∀c. {x | x ≠ c} ∈ subsets Borel

BOREL_MEASURABLE_SETS1

⊢ ∀c. {x | x < c} ∈ subsets Borel

BOREL_MEASURABLE_SETS

⊢ (∀c. {x | x < c} ∈ subsets Borel) ∧ (∀c. {x | c ≤ x} ∈ subsets Borel) ∧
  (∀c. {x | c < x} ∈ subsets Borel) ∧ (∀c. {x | x ≤ c} ∈ subsets Borel) ∧
  (∀c d. {x | c < x ∧ x < d} ∈ subsets Borel) ∧
  (∀c d. {x | c ≤ x ∧ x < d} ∈ subsets Borel) ∧
  (∀c d. {x | c < x ∧ x ≤ d} ∈ subsets Borel) ∧
  (∀c d. {x | c ≤ x ∧ x ≤ d} ∈ subsets Borel) ∧ (∀c. {c} ∈ subsets Borel) ∧
  ∀c. {x | x ≠ c} ∈ subsets Borel

BIGUNION_IMAGE_Q

⊢ ∀a f.
      sigma_algebra a ∧ f ∈ (Q_set -> subsets a) ⇒
      BIGUNION (IMAGE f Q_set) ∈ subsets a

ALGEBRA_UNION

⊢ ∀a s t. algebra a ∧ s ∈ subsets a ∧ t ∈ subsets a ⇒ s ∪ t ∈ subsets a

ALGEBRA_SUBSET_LAMBDA_SYSTEM

⊢ ∀m.
      algebra (m_space m,measurable_sets m) ∧ positive m ∧ increasing m ∧
      additive m ⇒
      measurable_sets m ⊆
      lambda_system (m_space m,POW (m_space m)) (inf_measure m)

ALGEBRA_SPACE

⊢ ∀a. algebra a ⇒ space a ∈ subsets a

ALGEBRA_INTER_SPACE

⊢ ∀a s. algebra a ∧ s ∈ subsets a ⇒ (space a ∩ s = s) ∧ (s ∩ space a = s)

ALGEBRA_INTER

⊢ ∀a s t. algebra a ∧ s ∈ subsets a ∧ t ∈ subsets a ⇒ s ∩ t ∈ subsets a

ALGEBRA_FINITE_UNION

⊢ ∀a c. algebra a ∧ FINITE c ∧ c ⊆ subsets a ⇒ BIGUNION c ∈ subsets a

ALGEBRA_EMPTY

⊢ ∀a. algebra a ⇒ ∅ ∈ subsets a

ALGEBRA_DIFF

⊢ ∀a s t. algebra a ∧ s ∈ subsets a ∧ t ∈ subsets a ⇒ s DIFF t ∈ subsets a

ALGEBRA_COMPL

⊢ ∀a s. algebra a ∧ s ∈ subsets a ⇒ space a DIFF s ∈ subsets a

ALGEBRA_ALT_INTER

⊢ ∀a.
      algebra a ⇔
      subset_class (space a) (subsets a) ∧ ∅ ∈ subsets a ∧
      (∀s. s ∈ subsets a ⇒ space a DIFF s ∈ subsets a) ∧
      ∀s t. s ∈ subsets a ∧ t ∈ subsets a ⇒ s ∩ t ∈ subsets a

ADDITIVE_SUM

⊢ ∀m f n.
      algebra (m_space m,measurable_sets m) ∧ positive m ∧ additive m ∧
      f ∈ (𝕌(:num) -> measurable_sets m) ∧
      (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
      (sum (0,n) (measure m ∘ f) = measure m (BIGUNION (IMAGE f (count n))))

ADDITIVE_INCREASING

⊢ ∀m.
      algebra (m_space m,measurable_sets m) ∧ positive m ∧ additive m ⇒
      increasing m

ADDITIVE

⊢ ∀m s t u.
      additive m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧
      DISJOINT s t ∧ (u = s ∪ t) ⇒
      (measure m u = measure m s + measure m t)