Theory "real_measure"

Parents real_borel

Signature

Constant	Type
additive	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> bool
closed_cdi	:α algebra -> bool
countably_additive	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> bool
countably_subadditive	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> bool
increasing	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> bool
inf_measure	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> bool) -> real
lambda_system	:α algebra -> ((α -> bool) -> real) -> (α -> bool) -> bool
m_space	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> α -> 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
mono_convergent	:(num -> α -> real) -> (α -> real) -> (α -> bool) -> bool
outer_measure_space	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> bool
positive	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> bool
smallest_closed_cdi	:α algebra -> α algebra
subadditive	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> bool

Definitions

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)

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

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

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)

increasing_def

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

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)}

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)}

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) ∧ measure_space m1 ∧ measure_space 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

mono_convergent_def

⊢ ∀u f s.
    mono_convergent u f s ⇔
    (∀x m n. m ≤ n ∧ x ∈ s ⇒ u m x ≤ u n x) ∧ ∀x. x ∈ s ⇒ (λi. u i x) ⟶ f x

outer_measure_space_def

⊢ ∀m. outer_measure_space 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

smallest_closed_cdi_def

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

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

Theorems

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)

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

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)

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_LEMMA

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

CLOSED_CDI_COMPL

⊢ ∀p s. closed_cdi p ∧ s ∈ subsets p ⇒ space p DIFF s ∈ 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_DUNION

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

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

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

COUNTABLY_ADDITIVE_ADDITIVE

⊢ ∀m. algebra (m_space m,measurable_sets m) ∧ positive m ∧
      countably_additive m ⇒
      additive 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_SUBADDITIVE_SUBADDITIVE

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

INCREASING

⊢ ∀m s t.
    increasing m ∧ s ⊆ t ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
    measure m s ≤ measure m 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)

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)

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

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

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

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

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_POSITIVE

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

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)

LAMBDA_SYSTEM_ADDITIVE

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

LAMBDA_SYSTEM_ALGEBRA

⊢ ∀g0 lam.
    algebra g0 ∧ positive (space g0,subsets g0,lam) ⇒
    algebra (space g0,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_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_EMPTY

⊢ ∀g0 lam.
    algebra g0 ∧ positive (space g0,subsets g0,lam) ⇒ ∅ ∈ 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_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_POSITIVE

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

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

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

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

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

⊢ ∀m1 m2 a.
    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_REAL_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_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. c * measure m a))

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_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_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))) ⇒
    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_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_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)))

OUTER_MEASURE_SPACE_POSITIVE

⊢ ∀m. outer_measure_space m ⇒ positive m

SIGMA_PROPERTY_DISJOINT_LEMMA

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

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

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

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

SPACE_SMALLEST_CLOSED_CDI

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

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 = s ∪ t) ⇒
    measure m u ≤ measure m s + measure m t

affine_borel_measurable

⊢ ∀m g.
    measure_space m ∧ g ∈ borel_measurable (m_space m,measurable_sets m) ⇒
    ∀a b. (λx. a + g x * b) ∈ borel_measurable (m_space m,measurable_sets m)

borel_measurable_SIGMA_borel_measurable

⊢ ∀m f s.
    measure_space m ∧ FINITE s ∧
    (∀i. i ∈ s ⇒ f i ∈ borel_measurable (m_space m,measurable_sets m)) ⇒
    (λx. ∑ (λi. f i x) s) ∈ borel_measurable (m_space m,measurable_sets m)

borel_measurable_eq_borel_measurable

⊢ ∀m f g.
    measure_space m ∧ f ∈ borel_measurable (m_space m,measurable_sets m) ∧
    g ∈ borel_measurable (m_space m,measurable_sets m) ⇒
    {w | w ∈ m_space m ∧ (f w = g w)} ∈ measurable_sets m

borel_measurable_ge_iff

⊢ ∀m. measure_space m ⇒
      ∀f. f ∈ borel_measurable (m_space m,measurable_sets m) ⇔
          ∀a. {w | w ∈ m_space m ∧ a ≤ f w} ∈ measurable_sets m

borel_measurable_gr_iff

⊢ ∀m. measure_space m ⇒
      ∀f. f ∈ borel_measurable (m_space m,measurable_sets m) ⇔
          ∀a. {w | w ∈ m_space m ∧ a < f w} ∈ measurable_sets m

borel_measurable_le_iff

⊢ ∀m. measure_space m ⇒
      ∀f. f ∈ borel_measurable (m_space m,measurable_sets m) ⇔
          ∀a. {w | w ∈ m_space m ∧ f w ≤ a} ∈ measurable_sets m

borel_measurable_leq_borel_measurable

⊢ ∀m f g.
    measure_space m ∧ f ∈ borel_measurable (m_space m,measurable_sets m) ∧
    g ∈ borel_measurable (m_space m,measurable_sets m) ⇒
    {w | w ∈ m_space m ∧ f w ≤ g w} ∈ measurable_sets m

borel_measurable_less_borel_measurable

⊢ ∀m f g.
    measure_space m ∧ f ∈ borel_measurable (m_space m,measurable_sets m) ∧
    g ∈ borel_measurable (m_space m,measurable_sets m) ⇒
    {w | w ∈ m_space m ∧ f w < g w} ∈ measurable_sets m

borel_measurable_less_iff

⊢ ∀m. measure_space m ⇒
      ∀f. f ∈ borel_measurable (m_space m,measurable_sets m) ⇔
          ∀a. {w | w ∈ m_space m ∧ f w < a} ∈ measurable_sets m

borel_measurable_neq_borel_measurable

⊢ ∀m f g.
    measure_space m ∧ f ∈ borel_measurable (m_space m,measurable_sets m) ∧
    g ∈ borel_measurable (m_space m,measurable_sets m) ⇒
    {w | w ∈ m_space m ∧ f w ≠ g w} ∈ measurable_sets m

borel_measurable_plus_borel_measurable

⊢ ∀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. f x + g x) ∈ borel_measurable (m_space m,measurable_sets m)

borel_measurable_square

⊢ ∀m f g.
    measure_space m ∧ f ∈ borel_measurable (m_space m,measurable_sets m) ⇒
    (λx. (f x)²) ∈ borel_measurable (m_space m,measurable_sets m)

borel_measurable_sub_borel_measurable

⊢ ∀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. f x − g x) ∈ borel_measurable (m_space m,measurable_sets m)

borel_measurable_times_borel_measurable

⊢ ∀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. f x * g x) ∈ borel_measurable (m_space m,measurable_sets 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)

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

mono_convergent_borel_measurable

⊢ ∀u m f.
    measure_space m ∧
    (∀n. u n ∈ borel_measurable (m_space m,measurable_sets m)) ∧
    mono_convergent u f (m_space m) ⇒
    f ∈ borel_measurable (m_space m,measurable_sets m)