Theory "measure"

Signature

Definitions

additive_def

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

caratheodory_sets_def

⊢ ∀sp m.
    caratheodory_sets sp m =
    {a | a ⊆ sp ∧ ∀q. q ⊆ sp ⇒ (m q = m (q ∩ a) + m (q DIFF a))}

complete_measure_space_def

⊢ ∀m. complete_measure_space m ⇔
      measure_space m ∧ ∀s. null_set m s ⇒ ∀t. t ⊆ s ⇒ t ∈ measurable_sets m

complete_of_def

⊢ ∀m. complete_of m =
      (m_space m,{s ∪ n | s ∈ measurable_sets m ∧ ∃t. n ⊆ t ∧ null_set m t},
       measure m)

countable_covers_def

⊢ ∀sts.
    countable_covers sts =
    (λa. {f | f ∈ (𝕌(:num) → sts) ∧ a ⊆ BIGUNION (IMAGE f 𝕌(:num))})

countably_additive_def

⊢ ∀m. countably_additive m ⇔
      ∀f. f ∈ (𝕌(:num) → measurable_sets m) ∧
          (∀i j. i ≠ j ⇒ DISJOINT (f i) (f j)) ∧
          BIGUNION (IMAGE f 𝕌(:num)) ∈ measurable_sets m ⇒
          (measure m (BIGUNION (IMAGE f 𝕌(:num))) = suminf (measure m ∘ f))

countably_subadditive_def

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

finite_additive_def

⊢ ∀m. finite_additive m ⇔
      ∀f n.
        (∀i. i < n ⇒ f i ∈ measurable_sets m) ∧
        (∀i j. i < n ∧ j < n ∧ i ≠ j ⇒ DISJOINT (f i) (f j)) ∧
        BIGUNION (IMAGE f (count n)) ∈ measurable_sets m ⇒
        (measure m (BIGUNION (IMAGE f (count n))) =
         ∑ (measure m ∘ f) (count n))

finite_subadditive_def

⊢ ∀m. finite_subadditive m ⇔
      ∀f n.
        (∀i. i < n ⇒ f i ∈ measurable_sets m) ∧
        BIGUNION (IMAGE f (count n)) ∈ measurable_sets m ⇒
        measure m (BIGUNION (IMAGE f (count n))) ≤ ∑ (measure m ∘ f) (count n)

increasing_def

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

m_space_def

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

measurable_sets_def

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

measure_def

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

measure_preserving_def

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

measure_space_def

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

null_set_def

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

outer_measure_def

⊢ ∀m C.
    outer_measure m C = (λa. inf {r | (∃f. f ∈ C a ∧ (suminf (m ∘ f) = r))})

outer_measure_space_def

⊢ ∀m. outer_measure_space m ⇔
      subset_class (m_space m) (measurable_sets m) ∧ ∅ ∈ measurable_sets m ∧
      positive m ∧ increasing m ∧ countably_subadditive m

positive_def

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

premeasure_def

⊢ ∀m. premeasure m ⇔ positive m ∧ countably_additive m

sigma_finite_def

⊢ ∀m. sigma_finite m ⇔
      ∃f. f ∈ (𝕌(:num) → measurable_sets m) ∧ (∀n. f n ⊆ f (SUC n)) ∧
          (BIGUNION (IMAGE f 𝕌(:num)) = m_space m) ∧ ∀n. measure m (f n) < +∞

sigma_finite_measure_space_def

⊢ ∀m. sigma_finite_measure_space m ⇔ measure_space m ∧ sigma_finite m

subadditive_def

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

Theorems

ADDITIVE

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

ADDITIVE_INCREASING

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

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)) ⇒
    (∑ (measure m ∘ f) (count n) = measure m (BIGUNION (IMAGE f (count n))))

ALGEBRA_COUNTABLY_ADDITIVE_ADDITIVE

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

ALGEBRA_PREMEASURE_ADDITIVE

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

ALGEBRA_PREMEASURE_COMPL

⊢ ∀m s.
    algebra (m_space m,measurable_sets m) ∧ premeasure m ∧
    s ∈ measurable_sets m ∧ measure m s < +∞ ⇒
    (measure m (m_space m DIFF s) = measure m (m_space m) − measure m s)

ALGEBRA_PREMEASURE_COUNTABLE_INCREASING

⊢ ∀m s f.
    algebra (m_space m,measurable_sets m) ∧ premeasure m ∧
    f ∈ (𝕌(:num) → measurable_sets m) ∧ (f 0 = ∅) ∧ (∀n. f n ⊆ f (SUC n)) ∧
    (s = BIGUNION (IMAGE f 𝕌(:num))) ∧ s ∈ measurable_sets m ⇒
    (sup (IMAGE (measure m ∘ f) 𝕌(:num)) = measure m s)

ALGEBRA_PREMEASURE_COUNTABLY_SUBADDITIVE

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

ALGEBRA_PREMEASURE_DIFF_SUBSET

⊢ ∀m s t.
    algebra (m_space m,measurable_sets m) ∧ premeasure m ∧
    s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧ s ⊆ t ∧ measure m s < +∞ ⇒
    (measure m (t DIFF s) = measure m t − measure m s)

ALGEBRA_PREMEASURE_FINITE_ADDITIVE

⊢ ∀m. algebra (m_space m,measurable_sets m) ∧ premeasure m ⇒ finite_additive m

ALGEBRA_PREMEASURE_FINITE_SUBADDITIVE

⊢ ∀m. algebra (m_space m,measurable_sets m) ∧ premeasure m ⇒
      finite_subadditive m

ALGEBRA_PREMEASURE_INCREASING

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

ALGEBRA_PREMEASURE_STRONG_ADDITIVE

⊢ ∀m s t.
    algebra (m_space m,measurable_sets m) ∧ premeasure m ∧
    s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
    (measure m (s ∪ t) + measure m (s ∩ t) = measure m s + measure m t)

ALGEBRA_PREMEASURE_SUBADDITIVE

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

BIGUNION_IMAGE_Q

⊢ ∀a f.
    sigma_algebra a ∧ f ∈ (ℚ → subsets a) ⇒ BIGUNION (IMAGE f ℚ) ∈ subsets a

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

CARATHEODORY_RING

⊢ ∀m0.
    ring (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

CARATHEODORY_SEMIRING

⊢ ∀m0.
    semiring (m_space m0,measurable_sets m0) ∧ premeasure 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

COMPLETE_MEASURE_THM

⊢ ∀m s t. complete_measure_space m ∧ t ∈ null_set m ∧ s ⊆ t ⇒ s ∈ null_set m

COUNTABLY_ADDITIVE

⊢ ∀m s f.
    countably_additive m ∧ f ∈ (𝕌(:num) → measurable_sets m) ∧
    (∀i j. i ≠ j ⇒ DISJOINT (f i) (f j)) ∧ (s = BIGUNION (IMAGE f 𝕌(:num))) ∧
    s ∈ measurable_sets m ⇒
    (suminf (measure m ∘ f) = measure m s)

COUNTABLY_ADDITIVE_ADDITIVE

⊢ ∀m. ∅ ∈ measurable_sets m ∧ positive m ∧ countably_additive m ⇒ additive m

COUNTABLY_ADDITIVE_FINITE_ADDITIVE

⊢ ∀m. ∅ ∈ measurable_sets m ∧ positive m ∧ countably_additive m ⇒
      finite_additive m

COUNTABLY_SUBADDITIVE

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

COUNTABLY_SUBADDITIVE_FINITE_SUBADDITIVE

⊢ ∀m. ∅ ∈ measurable_sets m ∧ positive m ∧ countably_subadditive m ⇒
      finite_subadditive m

COUNTABLY_SUBADDITIVE_SUBADDITIVE

⊢ ∀m. ∅ ∈ measurable_sets m ∧ positive m ∧ countably_subadditive m ⇒
      subadditive m

DYNKIN_SYSTEM_DIFF_SUBSET

⊢ ∀d s t.
    dynkin_system d ∧ s ∈ subsets d ∧ t ∈ subsets d ∧ s ⊆ t ⇒
    t DIFF s ∈ subsets d

DYNKIN_SYSTEM_PREMEASURE_ADDITIVE

⊢ ∀m. dynkin_system (m_space m,measurable_sets m) ∧ premeasure m ⇒ additive m

DYNKIN_SYSTEM_PREMEASURE_FINITE_ADDITIVE

⊢ ∀m. dynkin_system (m_space m,measurable_sets m) ∧ premeasure m ⇒
      finite_additive m

DYNKIN_SYSTEM_PREMEASURE_INCREASING

⊢ ∀m. dynkin_system (m_space m,measurable_sets m) ∧ premeasure m ⇒
      increasing m

FINITE_ADDITIVE

⊢ ∀m s f n.
    finite_additive m ∧ (∀i. i < n ⇒ f i ∈ measurable_sets m) ∧
    (∀i j. i < n ∧ j < n ∧ i ≠ j ⇒ DISJOINT (f i) (f j)) ∧
    (s = BIGUNION (IMAGE f (count n))) ∧ s ∈ measurable_sets m ⇒
    (∑ (measure m ∘ f) (count n) = measure m s)

FINITE_ADDITIVE_ALT

⊢ ∀m s c.
    positive m ∧ finite_additive m ∧ c ⊆ measurable_sets m ∧ FINITE c ∧
    disjoint c ∧ BIGUNION c ∈ measurable_sets m ⇒
    (∑ (measure m) c = measure m (BIGUNION c))

FINITE_IMP_SIGMA_FINITE

⊢ ∀m. measure_space m ∧ measure m (m_space m) ≠ +∞ ⇒ sigma_finite m

FINITE_SUBADDITIVE

⊢ ∀m s f n.
    finite_subadditive m ∧ (∀i. i < n ⇒ f i ∈ measurable_sets m) ∧
    (s = BIGUNION (IMAGE f (count n))) ∧ s ∈ measurable_sets m ⇒
    measure m s ≤ ∑ (measure m ∘ f) (count n)

FINITE_SUBADDITIVE_ALT

⊢ ∀m c.
    positive m ∧ finite_subadditive m ∧ c ⊆ measurable_sets m ∧ FINITE c ∧
    disjoint c ∧ BIGUNION c ∈ measurable_sets m ⇒
    measure m (BIGUNION c) ≤ ∑ (measure m) c

INCREASING

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

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) ∧
    ∀s. s ∈ measurable_sets m2 ⇒
        (measure m1 (PREIMAGE f s ∩ m_space m1) = measure m2 s)

IN_NULL_SET

⊢ ∀m s. s ∈ null_set m ⇔ null_set m s

MEASURABLE_IF

⊢ ∀f g M N P.
    f ∈ measurable (m_space M,measurable_sets M) (m_space N,measurable_sets N) ∧
    g ∈ measurable (m_space M,measurable_sets M) (m_space N,measurable_sets N) ∧
    {x | x ∈ m_space M ∧ P x} ∈ measurable_sets M ∧ measure_space M ⇒
    (λx. if P x then f x else g x) ∈
    measurable (m_space M,measurable_sets M) (m_space N,measurable_sets N)

MEASURABLE_IF_SET

⊢ ∀f g M N A.
    f ∈ measurable (m_space M,measurable_sets M) (m_space N,measurable_sets N) ∧
    g ∈ measurable (m_space M,measurable_sets M) (m_space N,measurable_sets N) ∧
    A ∩ m_space M ∈ measurable_sets M ∧ measure_space M ⇒
    (λx. if x ∈ A then f x else g x) ∈
    measurable (m_space M,measurable_sets M) (m_space N,measurable_sets N)

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_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_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_SETS_SUBSET_SPACE

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

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)

MEASURE_COMPL

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

MEASURE_COMPL_SUBSET

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

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))) ⇒
    (sup (IMAGE (measure m ∘ f) 𝕌(:num)) = measure m s)

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))) ⇒
    (suminf (measure m ∘ f) = measure m s)

MEASURE_DIFF_SUBSET

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

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_EMPTY

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

MEASURE_EXTREAL_SUM_IMAGE

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

MEASURE_FINITE_ADDITIVE

⊢ ∀m. measure_space m ⇒ finite_additive m

MEASURE_PRESERVING_LIFT

⊢ ∀m1 m2 a f.
    measure_space m1 ∧ measure_space m2 ∧
    measure_space (m_space m2,a,measure m2) ∧ measure m1 (m_space m1) ≠ +∞ ∧
    measure m2 (m_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_PRESERVING_SUBSET

⊢ ∀m1 m2 a.
    measure_space m1 ∧ measure_space m2 ∧
    measure_space (m_space m2,a,measure m2) ∧ measure m1 (m_space m1) ≠ +∞ ∧
    measure m2 (m_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_UP_LIFT

⊢ ∀m1 m2 f a.
    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_UP_SIGMA

⊢ ∀m1 m2 a.
    (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_SUBSET

⊢ ∀m1 m2 a.
    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_SPACE_ADDITIVE

⊢ ∀m. measure_space m ⇒ additive m

MEASURE_SPACE_BIGINTER

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

MEASURE_SPACE_BIGUNION

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

MEASURE_SPACE_CMUL

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

MEASURE_SPACE_COMPL

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

MEASURE_SPACE_COUNTABLY_SUBADDITIVE

⊢ ∀m. measure_space m ⇒ countably_subadditive 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_EMPTY_MEASURABLE

⊢ ∀m. measure_space m ⇒ ∅ ∈ measurable_sets m

MEASURE_SPACE_FINITE_DIFF

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

MEASURE_SPACE_FINITE_DIFF_SUBSET

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

MEASURE_SPACE_FINITE_MEASURE

⊢ ∀m s.
    measure_space m ∧ s ∈ measurable_sets m ∧ measure m (m_space m) ≠ +∞ ⇒
    measure m s ≠ +∞

MEASURE_SPACE_FINITE_SUBADDITIVE

⊢ ∀m. measure_space m ⇒ finite_subadditive m

MEASURE_SPACE_INCREASING

⊢ ∀m. measure_space m ⇒ increasing 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_IN_MSPACE

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

MEASURE_SPACE_MSPACE_MEASURABLE

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

MEASURE_SPACE_POSITIVE

⊢ ∀m. measure_space m ⇒ positive m

MEASURE_SPACE_REDUCE

⊢ ∀m. (m_space m,measurable_sets m,measure m) = 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_RESTRICTED_MEASURE

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

MEASURE_SPACE_RESTRICTION

⊢ ∀sp sts m sub.
    measure_space (sp,sts,m) ∧ sub ⊆ sts ∧ sigma_algebra (sp,sub) ⇒
    measure_space (sp,sub,m)

MEASURE_SPACE_SPACE

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

MEASURE_SPACE_STRONG_ADDITIVE

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

MEASURE_SPACE_SUBADDITIVE

⊢ ∀m. measure_space m ⇒ subadditive m

MEASURE_SPACE_SUBSET

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

MEASURE_SPACE_SUBSET_MSPACE

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

MEASURE_SPACE_UNION

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

MONOTONE_CONVERGENCE

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

MONOTONE_CONVERGENCE2

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

MONOTONE_CONVERGENCE_BIGINTER

⊢ ∀m s f.
    measure_space m ∧ f ∈ (𝕌(:num) → measurable_sets m) ∧
    (∀n. measure m (f n) ≠ +∞) ∧ (∀n. f (SUC n) ⊆ f n) ∧
    (s = BIGINTER (IMAGE f 𝕌(:num))) ⇒
    (inf (IMAGE (measure m ∘ f) 𝕌(:num)) = measure m s)

MONOTONE_CONVERGENCE_BIGINTER2

⊢ ∀m f.
    measure_space m ∧ f ∈ (𝕌(:num) → measurable_sets m) ∧
    (∀n. measure m (f n) ≠ +∞) ∧ (∀n. f (SUC n) ⊆ f n) ⇒
    (inf (IMAGE (measure m ∘ f) 𝕌(:num)) =
     measure m (BIGINTER (IMAGE f 𝕌(:num))))

NULL_SET_EMPTY

⊢ ∀m. measure_space m ⇒ null_set m ∅

NULL_SET_INTER

⊢ ∀m N1 N2.
    measure_space m ∧ N1 ∈ null_set m ∧ N2 ∈ null_set m ⇒ N1 ∩ N2 ∈ null_set m

NULL_SET_THM

⊢ ∀m s t.
    measure_space m ⇒
    ∅ ∈ null_set m ∧
    (t ∈ null_set m ∧ s ∈ measurable_sets m ∧ s ⊆ t ⇒ s ∈ null_set m) ∧
    ∀f. f ∈ (𝕌(:num) → null_set m) ⇒ BIGUNION (IMAGE f 𝕌(:num)) ∈ null_set m

NULL_SET_UNION

⊢ ∀m N1 N2.
    measure_space m ∧ N1 ∈ null_set m ∧ N2 ∈ null_set m ⇒ N1 ∪ N2 ∈ null_set m

OUTER_MEASURE_CONSTRUCTION

⊢ ∀sp sts m u.
    subset_class sp sts ∧ ∅ ∈ sts ∧ positive (sp,sts,m) ∧
    (u = outer_measure m (countable_covers sts)) ⇒
    outer_measure_space (sp,POW sp,u) ∧ (∀x. x ∈ sts ⇒ u x ≤ m x) ∧
    measure_space (sp,caratheodory_sets sp u,u) ∧
    ∀v. outer_measure_space (sp,POW sp,v) ∧ (∀x. x ∈ sts ⇒ v x ≤ m x) ⇒
        ∀x. x ⊆ sp ⇒ v x ≤ u x

OUTER_MEASURE_SPACE_FINITE_SUBADDITIVE

⊢ ∀m. outer_measure_space m ⇒ finite_subadditive m

OUTER_MEASURE_SPACE_POSITIVE

⊢ ∀m. outer_measure_space m ⇒ positive m

OUTER_MEASURE_SPACE_SUBADDITIVE

⊢ ∀m. outer_measure_space m ⇒ subadditive m

RING_ADDITIVE_EVERYTHING

⊢ ∀m. ring (m_space m,measurable_sets m) ∧ positive m ∧ additive m ⇒
      finite_additive m ∧ increasing m ∧ subadditive m ∧ finite_subadditive m

RING_ADDITIVE_FINITE_ADDITIVE

⊢ ∀m. ring (m_space m,measurable_sets m) ∧ positive m ∧ additive m ⇒
      finite_additive m

RING_ADDITIVE_INCREASING

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

RING_ADDITIVE_STRONG_ADDITIVE

⊢ ∀m s t.
    ring (m_space m,measurable_sets m) ∧ additive m ∧ positive m ∧
    s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
    (measure m (s ∪ t) + measure m (s ∩ t) = measure m s + measure m t)

RING_ADDITIVE_SUBADDITIVE

⊢ ∀m. ring (m_space m,measurable_sets m) ∧ positive m ∧ additive m ⇒
      subadditive m

RING_PREMEASURE_ADDITIVE

⊢ ∀m. ring (m_space m,measurable_sets m) ∧ premeasure m ⇒ additive m

RING_PREMEASURE_COUNTABLE_INCREASING

⊢ ∀m s f.
    ring (m_space m,measurable_sets m) ∧ premeasure m ∧
    f ∈ (𝕌(:num) → measurable_sets m) ∧ (f 0 = ∅) ∧ (∀n. f n ⊆ f (SUC n)) ∧
    (s = BIGUNION (IMAGE f 𝕌(:num))) ∧ s ∈ measurable_sets m ⇒
    (sup (IMAGE (measure m ∘ f) 𝕌(:num)) = measure m s)

RING_PREMEASURE_COUNTABLY_SUBADDITIVE

⊢ ∀m. ring (m_space m,measurable_sets m) ∧ premeasure m ⇒
      countably_subadditive m

RING_PREMEASURE_DIFF_SUBSET

⊢ ∀m s t.
    ring (m_space m,measurable_sets m) ∧ premeasure m ∧
    s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧ s ⊆ t ∧ measure m s < +∞ ⇒
    (measure m (t DIFF s) = measure m t − measure m s)

RING_PREMEASURE_FINITE_ADDITIVE

⊢ ∀m. ring (m_space m,measurable_sets m) ∧ premeasure m ⇒ finite_additive m

RING_PREMEASURE_FINITE_SUBADDITIVE

⊢ ∀m. ring (m_space m,measurable_sets m) ∧ premeasure m ⇒ finite_subadditive m

RING_PREMEASURE_INCREASING

⊢ ∀m. ring (m_space m,measurable_sets m) ∧ premeasure m ⇒ increasing m

RING_PREMEASURE_STRONG_ADDITIVE

⊢ ∀m s t.
    ring (m_space m,measurable_sets m) ∧ premeasure m ∧
    s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
    (measure m (s ∪ t) + measure m (s ∩ t) = measure m s + measure m t)

RING_PREMEASURE_SUBADDITIVE

⊢ ∀m. ring (m_space m,measurable_sets m) ∧ premeasure m ⇒ subadditive m

RING_SUBADDITIVE_FINITE_SUBADDITIVE

⊢ ∀m. ring (m_space m,measurable_sets m) ∧ positive m ∧ subadditive m ⇒
      finite_subadditive m

SEMIRING_FINITE_ADDITIVE_EXTENSION

⊢ ∀m0.
    semiring (m_space m0,measurable_sets m0) ∧ positive m0 ∧
    finite_additive m0 ⇒
    ∃m. ((m_space m,measurable_sets m) =
         smallest_ring (m_space m0) (measurable_sets m0)) ∧
        (∀s. s ∈ measurable_sets m0 ⇒ (measure m s = measure m0 s)) ∧
        positive m ∧ additive m

SEMIRING_PREMEASURE_ADDITIVE

⊢ ∀m. semiring (m_space m,measurable_sets m) ∧ premeasure m ⇒ additive m

SEMIRING_PREMEASURE_EXTENSION

⊢ ∀m0.
    semiring (m_space m0,measurable_sets m0) ∧ premeasure m0 ⇒
    ∃m. ((m_space m,measurable_sets m) =
         smallest_ring (m_space m0) (measurable_sets m0)) ∧
        (∀s. s ∈ measurable_sets m0 ⇒ (measure m s = measure m0 s)) ∧
        premeasure m

SEMIRING_PREMEASURE_FINITE_ADDITIVE

⊢ ∀m. semiring (m_space m,measurable_sets m) ∧ premeasure m ⇒
      finite_additive m

SEMIRING_PREMEASURE_INCREASING

⊢ ∀m. semiring (m_space m,measurable_sets m) ∧ premeasure m ⇒ increasing m

SIGMA_FINITE_ALT

⊢ ∀m. measure_space m ⇒
      (sigma_finite m ⇔
       ∃f. f ∈ (𝕌(:num) → measurable_sets m) ∧
           (BIGUNION (IMAGE f 𝕌(:num)) = m_space m) ∧ ∀n. measure m (f n) < +∞)

SIGMA_FINITE_ALT2

⊢ ∀m. measure_space m ⇒
      (sigma_finite m ⇔
       ∃A. COUNTABLE A ∧ A ⊆ measurable_sets m ∧ (BIGUNION A = m_space m) ∧
           ∀a. a ∈ A ⇒ measure m a ≠ +∞)

SIGMA_SUBSET_MEASURABLE_SETS

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

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)

SUBADDITIVE

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

UNIQUENESS_OF_MEASURE

⊢ ∀sp sts u v.
    subset_class sp sts ∧ (∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∩ t ∈ sts) ∧
    sigma_finite (sp,sts,u) ∧ measure_space (sp,subsets (sigma sp sts),u) ∧
    measure_space (sp,subsets (sigma sp sts),v) ∧ (∀s. s ∈ sts ⇒ (u s = v s)) ⇒
    ∀s. s ∈ subsets (sigma sp sts) ⇒ (u s = v s)

UNIQUENESS_OF_MEASURE_FINITE

⊢ ∀sp sts u v.
    subset_class sp sts ∧ (∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∩ t ∈ sts) ∧
    measure_space (sp,subsets (sigma sp sts),u) ∧
    measure_space (sp,subsets (sigma sp sts),v) ∧ (u sp = v sp) ∧ u sp < +∞ ∧
    (∀s. s ∈ sts ⇒ (u s = v s)) ⇒
    ∀s. s ∈ subsets (sigma sp sts) ⇒ (u s = v s)

countably_additive_alt_eq

⊢ ∀sp M u.
    countably_additive (sp,M,u) ⇔
    ∀A. IMAGE A 𝕌(:num) ⊆ M ⇒
        disjoint_family A ⇒
        BIGUNION {A i | i ∈ 𝕌(:num)} ∈ M ⇒
        (u (BIGUNION {A i | i ∈ 𝕌(:num)}) = suminf (u ∘ A))

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)

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

measure_space_eq

⊢ ∀m1 m2.
    measure_space m1 ∧ (m_space m2 = m_space m1) ∧
    (measurable_sets m2 = measurable_sets m1) ∧
    (∀s. s ∈ measurable_sets m2 ⇒ (measure m2 s = measure m1 s)) ⇒
    measure_space m2

measure_space_trivial

⊢ ∀a. sigma_algebra a ⇒ sigma_finite_measure_space (space a,subsets a,(λs. 0))

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 = ∑ (λi. measure m (a ∩ b i)) r)

null_sets

⊢ null_set M = {N | N ∈ measurable_sets M ∧ (measure M N = 0)}

positive_not_infty

⊢ ∀m. positive m ⇒ ∀s. s ∈ measurable_sets m ⇒ measure m s ≠ −∞

sets_eq_imp_space_eq

⊢ ∀M M'.
    measure_space M ∧ measure_space M' ∧
    (measurable_sets M = measurable_sets M') ⇒
    (m_space M = m_space M')

sigma_finite

⊢ ∀m. measure_space m ∧ sigma_finite m ⇒
      ∃A. IMAGE A 𝕌(:num) ⊆ measurable_sets m ∧
          (BIGUNION {A i | i ∈ 𝕌(:num)} = m_space m) ∧
          ∀i. measure m (A i) ≠ +∞

sigma_finite_disjoint

⊢ ∀m. measure_space m ∧ sigma_finite m ⇒
      ∃A. IMAGE A 𝕌(:num) ⊆ measurable_sets m ∧
          (BIGUNION {A i | i ∈ 𝕌(:num)} = m_space m) ∧
          (∀i. measure m (A i) ≠ +∞) ∧ disjoint_family A