Structure real_measureTheory

signature real_measureTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val additive_def : thm
    val closed_cdi_def : thm
    val countably_additive_def : thm
    val countably_subadditive_def : thm
    val increasing_def : thm
    val inf_measure_def : thm
    val lambda_system_def : thm
    val m_space_def : thm
    val measurable_sets_def : thm
    val measure_def : thm
    val measure_preserving_def : thm
    val measure_space_def : thm
    val mono_convergent_def : thm
    val outer_measure_space_def : thm
    val positive_def : thm
    val smallest_closed_cdi_def : thm
    val subadditive_def : thm
  
  (*  Theorems  *)
    val ADDITIVE : thm
    val ADDITIVE_INCREASING : thm
    val ADDITIVE_SUM : thm
    val ALGEBRA_SUBSET_LAMBDA_SYSTEM : thm
    val CARATHEODORY : thm
    val CARATHEODORY_LEMMA : thm
    val CLOSED_CDI_COMPL : thm
    val CLOSED_CDI_DISJOINT : thm
    val CLOSED_CDI_DUNION : thm
    val CLOSED_CDI_INCREASING : thm
    val COUNTABLY_ADDITIVE : thm
    val COUNTABLY_ADDITIVE_ADDITIVE : thm
    val COUNTABLY_SUBADDITIVE : thm
    val COUNTABLY_SUBADDITIVE_SUBADDITIVE : thm
    val INCREASING : thm
    val INCREASING_ADDITIVE_SUMMABLE : thm
    val INF_MEASURE_AGREES : thm
    val INF_MEASURE_CLOSE : thm
    val INF_MEASURE_COUNTABLY_SUBADDITIVE : thm
    val INF_MEASURE_EMPTY : thm
    val INF_MEASURE_INCREASING : thm
    val INF_MEASURE_LE : thm
    val INF_MEASURE_NONEMPTY : thm
    val INF_MEASURE_OUTER : thm
    val INF_MEASURE_POS : thm
    val INF_MEASURE_POS0 : thm
    val INF_MEASURE_POSITIVE : thm
    val IN_MEASURE_PRESERVING : thm
    val LAMBDA_SYSTEM_ADDITIVE : thm
    val LAMBDA_SYSTEM_ALGEBRA : thm
    val LAMBDA_SYSTEM_CARATHEODORY : thm
    val LAMBDA_SYSTEM_COMPL : thm
    val LAMBDA_SYSTEM_EMPTY : thm
    val LAMBDA_SYSTEM_INCREASING : thm
    val LAMBDA_SYSTEM_INTER : thm
    val LAMBDA_SYSTEM_POSITIVE : thm
    val LAMBDA_SYSTEM_STRONG_ADDITIVE : thm
    val LAMBDA_SYSTEM_STRONG_SUM : thm
    val MEASURABLE_POW_TO_POW : thm
    val MEASURABLE_POW_TO_POW_IMAGE : thm
    val MEASURABLE_RANGE_REDUCE : thm
    val MEASURABLE_SETS_SUBSET_SPACE : thm
    val MEASURE_ADDITIVE : thm
    val MEASURE_COMPL : thm
    val MEASURE_COMPL_SUBSET : thm
    val MEASURE_COUNTABLE_INCREASING : thm
    val MEASURE_COUNTABLY_ADDITIVE : thm
    val MEASURE_DOWN : thm
    val MEASURE_EMPTY : thm
    val MEASURE_PRESERVING_LIFT : thm
    val MEASURE_PRESERVING_SUBSET : thm
    val MEASURE_PRESERVING_UP_LIFT : thm
    val MEASURE_PRESERVING_UP_SIGMA : thm
    val MEASURE_PRESERVING_UP_SUBSET : thm
    val MEASURE_REAL_SUM_IMAGE : thm
    val MEASURE_SPACE_ADDITIVE : thm
    val MEASURE_SPACE_BIGINTER : thm
    val MEASURE_SPACE_BIGUNION : thm
    val MEASURE_SPACE_CMUL : thm
    val MEASURE_SPACE_DIFF : thm
    val MEASURE_SPACE_EMPTY_MEASURABLE : thm
    val MEASURE_SPACE_INCREASING : thm
    val MEASURE_SPACE_INTER : thm
    val MEASURE_SPACE_IN_MSPACE : thm
    val MEASURE_SPACE_MSPACE_MEASURABLE : thm
    val MEASURE_SPACE_POSITIVE : thm
    val MEASURE_SPACE_REDUCE : thm
    val MEASURE_SPACE_RESTRICTED : thm
    val MEASURE_SPACE_SUBSET : thm
    val MEASURE_SPACE_SUBSET_MSPACE : thm
    val MEASURE_SPACE_UNION : thm
    val MONOTONE_CONVERGENCE : thm
    val MONOTONE_CONVERGENCE2 : thm
    val MONOTONE_CONVERGENCE_BIGINTER : thm
    val MONOTONE_CONVERGENCE_BIGINTER2 : thm
    val OUTER_MEASURE_SPACE_POSITIVE : thm
    val SIGMA_PROPERTY_DISJOINT_LEMMA : thm
    val SIGMA_PROPERTY_DISJOINT_LEMMA1 : thm
    val SIGMA_PROPERTY_DISJOINT_LEMMA2 : thm
    val SIGMA_SUBSET_MEASURABLE_SETS : thm
    val SMALLEST_CLOSED_CDI : thm
    val SPACE_SMALLEST_CLOSED_CDI : thm
    val STRONG_MEASURE_SPACE_SUBSET : thm
    val SUBADDITIVE : thm
    val affine_borel_measurable : thm
    val borel_measurable_SIGMA_borel_measurable : thm
    val borel_measurable_eq_borel_measurable : thm
    val borel_measurable_ge_iff : thm
    val borel_measurable_gr_iff : thm
    val borel_measurable_le_iff : thm
    val borel_measurable_leq_borel_measurable : thm
    val borel_measurable_less_borel_measurable : thm
    val borel_measurable_less_iff : thm
    val borel_measurable_neq_borel_measurable : thm
    val borel_measurable_plus_borel_measurable : thm
    val borel_measurable_square : thm
    val borel_measurable_sub_borel_measurable : thm
    val borel_measurable_times_borel_measurable : thm
    val finite_additivity_sufficient_for_finite_spaces : thm
    val finite_additivity_sufficient_for_finite_spaces2 : thm
    val mono_convergent_borel_measurable : thm
  
  val real_measure_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [real_borel] Parent theory of "real_measure"
   
   [additive_def]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀m. increasing m ⇔
            ∀s t.
              s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧ s ⊆ t ⇒
              measure m s ≤ measure m t
   
   [inf_measure_def]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀sp sts mu. m_space (sp,sts,mu) = sp
   
   [measurable_sets_def]  Definition
      
      ⊢ ∀sp sts mu. measurable_sets (sp,sts,mu) = sts
   
   [measure_def]  Definition
      
      ⊢ ∀sp sts mu. measure (sp,sts,mu) = mu
   
   [measure_preserving_def]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀m. measure_space m ⇔
            sigma_algebra (m_space m,measurable_sets m) ∧ positive m ∧
            countably_additive m
   
   [mono_convergent_def]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀m. outer_measure_space m ⇔
            positive m ∧ increasing m ∧ countably_subadditive m
   
   [positive_def]  Definition
      
      ⊢ ∀m. positive m ⇔
            measure m ∅ = 0 ∧ ∀s. s ∈ measurable_sets m ⇒ 0 ≤ measure m s
   
   [smallest_closed_cdi_def]  Definition
      
      ⊢ ∀a. smallest_closed_cdi a =
            (space a,BIGINTER {b | subsets a ⊆ b ∧ closed_cdi (space a,b)})
   
   [subadditive_def]  Definition
      
      ⊢ ∀m. subadditive m ⇔
            ∀s t.
              s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
              measure m (s ∪ t) ≤ measure m s + measure m t
   
   [ADDITIVE]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀m. algebra (m_space m,measurable_sets m) ∧ positive m ∧ additive m ⇒
            increasing m
   
   [ADDITIVE_SUM]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p s. closed_cdi p ∧ s ∈ subsets p ⇒ space p DIFF s ∈ subsets p
   
   [CLOSED_CDI_DISJOINT]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p s t.
          ∅ ∈ subsets p ∧ closed_cdi p ∧ s ∈ subsets p ∧ t ∈ subsets p ∧
          DISJOINT s t ⇒
          s ∪ t ∈ subsets p
   
   [CLOSED_CDI_INCREASING]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀m. algebra (m_space m,measurable_sets m) ∧ positive m ∧
            countably_additive m ⇒
            additive m
   
   [COUNTABLY_SUBADDITIVE]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀m. algebra (m_space m,measurable_sets m) ∧ positive m ∧
            countably_subadditive m ⇒
            subadditive m
   
   [INCREASING]  Theorem
      
      ⊢ ∀m s t.
          increasing m ∧ s ⊆ t ∧ s ∈ measurable_sets m ∧
          t ∈ measurable_sets m ⇒
          measure m s ≤ measure m t
   
   [INCREASING_ADDITIVE_SUMMABLE]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀m. algebra (m_space m,measurable_sets m) ∧ positive m ⇒
            inf_measure m ∅ = 0
   
   [INF_MEASURE_INCREASING]  Theorem
      
      ⊢ ∀m. algebra (m_space m,measurable_sets m) ∧ positive m ⇒
            increasing (m_space m,POW (m_space m),inf_measure m)
   
   [INF_MEASURE_LE]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀m g.
          algebra (m_space m,measurable_sets m) ∧ positive m ∧
          g ⊆ m_space m ⇒
          0 ≤ inf_measure m g
   
   [INF_MEASURE_POS0]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀m. algebra (m_space m,measurable_sets m) ∧ positive m ⇒
            positive (m_space m,POW (m_space m),inf_measure m)
   
   [IN_MEASURE_PRESERVING]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀g0 lam l1 l2.
          algebra g0 ∧ positive (space g0,subsets g0,lam) ⇒
          additive (space g0,lambda_system g0 lam,lam)
   
   [LAMBDA_SYSTEM_ALGEBRA]  Theorem
      
      ⊢ ∀g0 lam.
          algebra g0 ∧ positive (space g0,subsets g0,lam) ⇒
          algebra (space g0,lambda_system g0 lam)
   
   [LAMBDA_SYSTEM_CARATHEODORY]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀g0 lam.
          algebra g0 ∧ positive (space g0,subsets g0,lam) ⇒
          ∅ ∈ lambda_system g0 lam
   
   [LAMBDA_SYSTEM_INCREASING]  Theorem
      
      ⊢ ∀g0 lam.
          increasing (space g0,subsets g0,lam) ⇒
          increasing (space g0,lambda_system g0 lam,lam)
   
   [LAMBDA_SYSTEM_INTER]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀g0 lam.
          positive (space g0,subsets g0,lam) ⇒
          positive (space g0,lambda_system g0 lam,lam)
   
   [LAMBDA_SYSTEM_STRONG_ADDITIVE]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀m s. measure_space m ∧ s ∈ measurable_sets m ⇒ s ⊆ m_space m
   
   [MEASURE_ADDITIVE]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀m. measure_space m ⇒ measure m ∅ = 0
   
   [MEASURE_PRESERVING_LIFT]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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_SPACE_ADDITIVE]  Theorem
      
      ⊢ ∀m. measure_space m ⇒ additive m
   
   [MEASURE_SPACE_BIGINTER]  Theorem
      
      ⊢ ∀m s.
          measure_space m ∧ (∀n. s n ∈ measurable_sets m) ⇒
          BIGINTER (IMAGE s 𝕌(:num)) ∈ measurable_sets m
   
   [MEASURE_SPACE_BIGUNION]  Theorem
      
      ⊢ ∀m s.
          measure_space m ∧ (∀n. s n ∈ measurable_sets m) ⇒
          BIGUNION (IMAGE s 𝕌(:num)) ∈ measurable_sets m
   
   [MEASURE_SPACE_CMUL]  Theorem
      
      ⊢ ∀m c.
          measure_space m ∧ 0 ≤ c ⇒
          measure_space (m_space m,measurable_sets m,(λa. c * measure m a))
   
   [MEASURE_SPACE_DIFF]  Theorem
      
      ⊢ ∀m s t.
          measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
          s DIFF t ∈ measurable_sets m
   
   [MEASURE_SPACE_EMPTY_MEASURABLE]  Theorem
      
      ⊢ ∀m. measure_space m ⇒ ∅ ∈ measurable_sets m
   
   [MEASURE_SPACE_INCREASING]  Theorem
      
      ⊢ ∀m. measure_space m ⇒ increasing m
   
   [MEASURE_SPACE_INTER]  Theorem
      
      ⊢ ∀m s t.
          measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
          s ∩ t ∈ measurable_sets m
   
   [MEASURE_SPACE_IN_MSPACE]  Theorem
      
      ⊢ ∀m A.
          measure_space m ∧ A ∈ measurable_sets m ⇒
          ∀x. x ∈ A ⇒ x ∈ m_space m
   
   [MEASURE_SPACE_MSPACE_MEASURABLE]  Theorem
      
      ⊢ ∀m. measure_space m ⇒ m_space m ∈ measurable_sets m
   
   [MEASURE_SPACE_POSITIVE]  Theorem
      
      ⊢ ∀m. measure_space m ⇒ positive m
   
   [MEASURE_SPACE_REDUCE]  Theorem
      
      ⊢ ∀m. (m_space m,measurable_sets m,measure m) = m
   
   [MEASURE_SPACE_RESTRICTED]  Theorem
      
      ⊢ ∀m s.
          measure_space m ∧ s ∈ measurable_sets m ⇒
          measure_space (s,IMAGE (λt. s ∩ t) (measurable_sets m),measure m)
   
   [MEASURE_SPACE_SUBSET]  Theorem
      
      ⊢ ∀s s' m.
          s' ⊆ s ∧ measure_space (s,POW s,m) ⇒ measure_space (s',POW s',m)
   
   [MEASURE_SPACE_SUBSET_MSPACE]  Theorem
      
      ⊢ ∀A m. measure_space m ∧ A ∈ measurable_sets m ⇒ A ⊆ m_space m
   
   [MEASURE_SPACE_UNION]  Theorem
      
      ⊢ ∀m s t.
          measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
          s ∪ t ∈ measurable_sets m
   
   [MONOTONE_CONVERGENCE]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀m. outer_measure_space m ⇒ positive m
   
   [SIGMA_PROPERTY_DISJOINT_LEMMA]  Theorem
      
      ⊢ ∀sp a p.
          algebra (sp,a) ∧ a ⊆ p ∧ closed_cdi (sp,p) ⇒
          subsets (sigma sp a) ⊆ p
   
   [SIGMA_PROPERTY_DISJOINT_LEMMA1]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀a m.
          measure_space m ∧ a ⊆ measurable_sets m ⇒
          subsets (sigma (m_space m) a) ⊆ measurable_sets m
   
   [SMALLEST_CLOSED_CDI]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀a. space (smallest_closed_cdi a) = space a
   
   [STRONG_MEASURE_SPACE_SUBSET]  Theorem
      
      ⊢ ∀s s'.
          s' ⊆ m_space s ∧ measure_space s ∧ POW s' ⊆ measurable_sets s ⇒
          measure_space (s',POW s',measure s)
   
   [SUBADDITIVE]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀m f s.
          measure_space m ∧ FINITE s ∧
          (∀i. i ∈ s ⇒ f i ∈ borel_measurable (m_space m,measurable_sets m)) ⇒
          (λx. SIGMA (λi. f i x) s) ∈
          borel_measurable (m_space m,measurable_sets m)
   
   [borel_measurable_eq_borel_measurable]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀m. sigma_algebra (m_space m,measurable_sets m) ∧
            FINITE (m_space m) ∧ positive m ∧ additive m ⇒
            measure_space m
   
   [mono_convergent_borel_measurable]  Theorem
      
      ⊢ ∀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)
   
   
*)
end

HOL 4, Kananaskis-14