Structure real_lebesgueTheory

signature real_lebesgueTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val RN_deriv_def : thm
    val countable_space_integral_def : thm
    val finite_space_integral_def : thm
    val fn_minus_def : thm
    val fn_plus_def : thm
    val integrable_def : thm
    val integral_def : thm
    val mon_upclose_def : thm
    val mon_upclose_help_def : thm
    val mono_increasing_def : thm
    val nnfis_def : thm
    val nonneg_def : thm
    val pos_fn_integral_def : thm
    val pos_simple_fn_def : thm
    val pos_simple_fn_integral_def : thm
    val prod_measure_def : thm
    val prod_measure_space_def : thm
    val psfis_def : thm
    val psfs_def : thm
    val upclose_def : thm
  
  (*  Theorems  *)
    val IN_psfis : thm
    val borel_measurable_mon_conv_psfis : thm
    val countable_space_integral_reduce : thm
    val finite_POW_RN_deriv_reduce : thm
    val finite_POW_prod_measure_reduce : thm
    val finite_integral_on_set : thm
    val finite_space_POW_integral_reduce : thm
    val finite_space_integral_reduce : thm
    val fn_plus_fn_minus_borel_measurable : thm
    val fn_plus_fn_minus_borel_measurable_iff : thm
    val indicator_fn_split : thm
    val integral_add : thm
    val integral_borel_measurable : thm
    val integral_cmul_indicator : thm
    val integral_indicator_fn : thm
    val integral_mono : thm
    val integral_times : thm
    val integral_zero : thm
    val markov_ineq : thm
    val measure_space_finite_prod_measure_POW1 : thm
    val measure_space_finite_prod_measure_POW2 : thm
    val measure_split : thm
    val mon_upclose_help_compute : thm
    val mon_upclose_psfis : thm
    val mono_increasing_converges_to_sup : thm
    val nnfis_add : thm
    val nnfis_borel_measurable : thm
    val nnfis_dom_conv : thm
    val nnfis_integral : thm
    val nnfis_minus_nnfis_integral : thm
    val nnfis_mon_conv : thm
    val nnfis_mono : thm
    val nnfis_pos_on_mspace : thm
    val nnfis_times : thm
    val nnfis_unique : thm
    val pos_psfis : thm
    val pos_simple_fn_integral_REAL_SUM_IMAGE : thm
    val pos_simple_fn_integral_add : thm
    val pos_simple_fn_integral_indicator : thm
    val pos_simple_fn_integral_mono : thm
    val pos_simple_fn_integral_mono_on_mspace : thm
    val pos_simple_fn_integral_mult : thm
    val pos_simple_fn_integral_present : thm
    val pos_simple_fn_integral_unique : thm
    val psfis_REAL_SUM_IMAGE : thm
    val psfis_add : thm
    val psfis_borel_measurable : thm
    val psfis_equiv : thm
    val psfis_indicator : thm
    val psfis_intro : thm
    val psfis_mono : thm
    val psfis_mono_conv_mono : thm
    val psfis_mult : thm
    val psfis_nnfis : thm
    val psfis_nonneg : thm
    val psfis_present : thm
    val psfis_unique : thm
    val upclose_psfis : thm
  
  val real_lebesgue_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [real_measure] Parent theory of "real_lebesgue"
   
   [RN_deriv_def]  Definition
      
      ⊢ ∀m v.
          RN_deriv m v =
          @f. measure_space m ∧
              measure_space (m_space m,measurable_sets m,v) ∧
              f ∈ borel_measurable (m_space m,measurable_sets m) ∧
              ∀a. a ∈ measurable_sets m ⇒
                  integral m (λx. f x * 𝟙 a x) = v a
   
   [countable_space_integral_def]  Definition
      
      ⊢ ∀m f.
          countable_space_integral m f =
          (let
             e = enumerate (IMAGE f (m_space m))
           in
             suminf ((λr. r * measure m (PREIMAGE f {r} ∩ m_space m)) ∘ e))
   
   [finite_space_integral_def]  Definition
      
      ⊢ ∀m f.
          finite_space_integral m f =
          SIGMA (λr. r * measure m (PREIMAGE f {r} ∩ m_space m))
            (IMAGE f (m_space m))
   
   [fn_minus_def]  Definition
      
      ⊢ ∀f. fn_minus f = (λx. if 0 ≤ f x then 0 else -f x)
   
   [fn_plus_def]  Definition
      
      ⊢ ∀f. fn_plus f = (λx. if 0 ≤ f x then f x else 0)
   
   [integrable_def]  Definition
      
      ⊢ ∀m f.
          integrable m f ⇔
          measure_space m ∧ (∃x. x ∈ nnfis m (fn_plus f)) ∧
          ∃y. y ∈ nnfis m (fn_minus f)
   
   [integral_def]  Definition
      
      ⊢ ∀m f.
          integral m f =
          (@i. i ∈ nnfis m (fn_plus f)) − @j. j ∈ nnfis m (fn_minus f)
   
   [mon_upclose_def]  Definition
      
      ⊢ ∀u m. mon_upclose u m = mon_upclose_help m u m
   
   [mon_upclose_help_def]  Definition
      
      ⊢ (∀u m. mon_upclose_help 0 u m = u m 0) ∧
        ∀n u m.
          mon_upclose_help (SUC n) u m =
          upclose (u m (SUC n)) (mon_upclose_help n u m)
   
   [mono_increasing_def]  Definition
      
      ⊢ ∀f. mono_increasing f ⇔ ∀m n. m ≤ n ⇒ f m ≤ f n
   
   [nnfis_def]  Definition
      
      ⊢ ∀m f.
          nnfis m f =
          {y |
           ∃u x.
             mono_convergent u f (m_space m) ∧ (∀n. x n ∈ psfis m (u n)) ∧
             x ⟶ y}
   
   [nonneg_def]  Definition
      
      ⊢ ∀f. nonneg f ⇔ ∀x. 0 ≤ f x
   
   [pos_fn_integral_def]  Definition
      
      ⊢ ∀m f.
          pos_fn_integral m f =
          sup {r | (∃g. r ∈ psfis m g ∧ ∀x. g x ≤ f x)}
   
   [pos_simple_fn_def]  Definition
      
      ⊢ ∀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. x i * 𝟙 (a i) t) s) ∧
          (∀i. i ∈ s ⇒ a i ∈ measurable_sets m) ∧ (∀i. 0 ≤ x i) ∧
          FINITE s ∧ (∀i j. i ∈ s ∧ j ∈ s ∧ i ≠ j ⇒ DISJOINT (a i) (a j)) ∧
          BIGUNION (IMAGE a s) = m_space m
   
   [pos_simple_fn_integral_def]  Definition
      
      ⊢ ∀m s a x.
          pos_simple_fn_integral m s a x =
          SIGMA (λi. x i * measure m (a i)) s
   
   [prod_measure_def]  Definition
      
      ⊢ ∀m0 m1.
          prod_measure m0 m1 =
          (λa. integral m0 (λs0. measure m1 (PREIMAGE (λs1. (s0,s1)) a)))
   
   [prod_measure_space_def]  Definition
      
      ⊢ ∀m0 m1.
          prod_measure_space m0 m1 =
          (m_space m0 × m_space m1,
           subsets
             (sigma (m_space m0 × m_space m1)
                (prod_sets (measurable_sets m0) (measurable_sets m1))),
           prod_measure m0 m1)
   
   [psfis_def]  Definition
      
      ⊢ ∀m f.
          psfis m f =
          IMAGE (λ(s,a,x). pos_simple_fn_integral m s a x) (psfs m f)
   
   [psfs_def]  Definition
      
      ⊢ ∀m f. psfs m f = {(s,a,x) | pos_simple_fn m f s a x}
   
   [upclose_def]  Definition
      
      ⊢ ∀f g. upclose f g = (λt. max (f t) (g t))
   
   [IN_psfis]  Theorem
      
      ⊢ ∀m r f.
          r ∈ psfis m f ⇒
          ∃s a x.
            pos_simple_fn m f s a x ∧ r = pos_simple_fn_integral m s a x
   
   [borel_measurable_mon_conv_psfis]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧
          f ∈ borel_measurable (m_space m,measurable_sets m) ∧
          (∀t. t ∈ m_space m ⇒ 0 ≤ f t) ⇒
          ∃u x. mono_convergent u f (m_space m) ∧ ∀n. x n ∈ psfis m (u n)
   
   [countable_space_integral_reduce]  Theorem
      
      ⊢ ∀m f p n.
          measure_space m ∧ positive m ∧
          f ∈ borel_measurable (m_space m,measurable_sets m) ∧
          COUNTABLE (IMAGE f (m_space m)) ∧
          INFINITE (IMAGE (fn_plus f) (m_space m)) ∧
          INFINITE (IMAGE (fn_minus f) (m_space m)) ∧
          (λr. r * measure m (PREIMAGE (fn_minus f) {r} ∩ m_space m)) ∘
          enumerate (IMAGE (fn_minus f) (m_space m)) sums n ∧
          (λr. r * measure m (PREIMAGE (fn_plus f) {r} ∩ m_space m)) ∘
          enumerate (IMAGE (fn_plus f) (m_space m)) sums p ⇒
          integral m f = p − n
   
   [finite_POW_RN_deriv_reduce]  Theorem
      
      ⊢ ∀m v.
          measure_space m ∧ FINITE (m_space m) ∧
          measure_space (m_space m,measurable_sets m,v) ∧
          POW (m_space m) = measurable_sets m ∧
          (∀x. measure m {x} = 0 ⇒ v {x} = 0) ⇒
          ∀x. x ∈ m_space m ∧ measure m {x} ≠ 0 ⇒
              RN_deriv m v x = v {x} / measure m {x}
   
   [finite_POW_prod_measure_reduce]  Theorem
      
      ⊢ ∀m0 m1.
          measure_space m0 ∧ measure_space m1 ∧ FINITE (m_space m0) ∧
          FINITE (m_space m1) ∧ POW (m_space m0) = measurable_sets m0 ∧
          POW (m_space m1) = measurable_sets m1 ⇒
          ∀a0 a1.
            a0 ∈ measurable_sets m0 ∧ a1 ∈ measurable_sets m1 ⇒
            prod_measure m0 m1 (a0 × a1) = measure m0 a0 * measure m1 a1
   
   [finite_integral_on_set]  Theorem
      
      ⊢ ∀m f a.
          measure_space m ∧ FINITE (m_space m) ∧
          f ∈ borel_measurable (m_space m,measurable_sets m) ∧
          a ∈ measurable_sets m ⇒
          integral m (λx. f x * 𝟙 a x) =
          SIGMA (λr. r * measure m (PREIMAGE f {r} ∩ a)) (IMAGE f a)
   
   [finite_space_POW_integral_reduce]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧ POW (m_space m) = measurable_sets m ∧
          FINITE (m_space m) ⇒
          integral m f = SIGMA (λx. f x * measure m {x}) (m_space m)
   
   [finite_space_integral_reduce]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧
          f ∈ borel_measurable (m_space m,measurable_sets m) ∧
          FINITE (m_space m) ⇒
          integral m f = finite_space_integral m f
   
   [fn_plus_fn_minus_borel_measurable]  Theorem
      
      ⊢ ∀f m.
          measure_space m ∧
          f ∈ borel_measurable (m_space m,measurable_sets m) ⇒
          fn_plus f ∈ borel_measurable (m_space m,measurable_sets m) ∧
          fn_minus f ∈ borel_measurable (m_space m,measurable_sets m)
   
   [fn_plus_fn_minus_borel_measurable_iff]  Theorem
      
      ⊢ ∀f m.
          measure_space m ⇒
          (f ∈ borel_measurable (m_space m,measurable_sets m) ⇔
           fn_plus f ∈ borel_measurable (m_space m,measurable_sets m) ∧
           fn_minus f ∈ borel_measurable (m_space m,measurable_sets m))
   
   [indicator_fn_split]  Theorem
      
      ⊢ ∀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 ⇒ 𝟙 a = (λx. SIGMA (λi. 𝟙 (a ∩ b i) x) r)
   
   [integral_add]  Theorem
      
      ⊢ ∀m f g.
          integrable m f ∧ integrable m g ⇒
          integrable m (λt. f t + g t) ∧
          integral m (λt. f t + g t) = integral m f + integral m g
   
   [integral_borel_measurable]  Theorem
      
      ⊢ ∀m f.
          integrable m f ⇒
          f ∈ borel_measurable (m_space m,measurable_sets m)
   
   [integral_cmul_indicator]  Theorem
      
      ⊢ ∀m s c.
          measure_space m ∧ s ∈ measurable_sets m ⇒
          integral m (λx. c * 𝟙 s x) = c * measure m s
   
   [integral_indicator_fn]  Theorem
      
      ⊢ ∀m a.
          measure_space m ∧ a ∈ measurable_sets m ⇒
          integral m (𝟙 a) = measure m a ∧ integrable m (𝟙 a)
   
   [integral_mono]  Theorem
      
      ⊢ ∀m f g.
          integrable m f ∧ integrable m g ∧ (∀t. t ∈ m_space m ⇒ f t ≤ g t) ⇒
          integral m f ≤ integral m g
   
   [integral_times]  Theorem
      
      ⊢ ∀m f a.
          integrable m f ⇒
          integrable m (λt. a * f t) ∧
          integral m (λt. a * f t) = a * integral m f
   
   [integral_zero]  Theorem
      
      ⊢ ∀m. measure_space m ⇒ integral m (λx. 0) = 0
   
   [markov_ineq]  Theorem
      
      ⊢ ∀m f a n.
          integrable m f ∧ 0 < a ∧ integrable m (λx. abs (f x) pow n) ⇒
          measure m (PREIMAGE f {y | a ≤ y} ∩ m_space m) ≤
          integral m (λx. abs (f x) pow n) / a pow n
   
   [measure_space_finite_prod_measure_POW1]  Theorem
      
      ⊢ ∀m0 m1.
          measure_space m0 ∧ measure_space m1 ∧ FINITE (m_space m0) ∧
          FINITE (m_space m1) ∧ POW (m_space m0) = measurable_sets m0 ∧
          POW (m_space m1) = measurable_sets m1 ⇒
          measure_space (prod_measure_space m0 m1)
   
   [measure_space_finite_prod_measure_POW2]  Theorem
      
      ⊢ ∀m0 m1.
          measure_space m0 ∧ measure_space m1 ∧ FINITE (m_space m0) ∧
          FINITE (m_space m1) ∧ POW (m_space m0) = measurable_sets m0 ∧
          POW (m_space m1) = measurable_sets m1 ⇒
          measure_space
            (m_space m0 × m_space m1,POW (m_space m0 × m_space m1),
             prod_measure m0 m1)
   
   [measure_split]  Theorem
      
      ⊢ ∀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
   
   [mon_upclose_help_compute]  Theorem
      
      ⊢ (∀u m. mon_upclose_help 0 u m = u m 0) ∧
        (∀n u m.
           mon_upclose_help (NUMERAL (BIT1 n)) u m =
           upclose (u m (NUMERAL (BIT1 n)))
             (mon_upclose_help (NUMERAL (BIT1 n) − 1) u m)) ∧
        ∀n u m.
          mon_upclose_help (NUMERAL (BIT2 n)) u m =
          upclose (u m (NUMERAL (BIT2 n)))
            (mon_upclose_help (NUMERAL (BIT1 n)) u m)
   
   [mon_upclose_psfis]  Theorem
      
      ⊢ ∀m u.
          measure_space m ∧ (∀n n'. ∃a. a ∈ psfis m (u n n')) ⇒
          ∃c. ∀n. c n ∈ psfis m (mon_upclose u n)
   
   [mono_increasing_converges_to_sup]  Theorem
      
      ⊢ ∀f r.
          (∀i. 0 ≤ f i) ∧ mono_increasing f ∧ f ⟶ r ⇒
          r = sup (IMAGE f 𝕌(:num))
   
   [nnfis_add]  Theorem
      
      ⊢ ∀f g m a b.
          measure_space m ∧ a ∈ nnfis m f ∧ b ∈ nnfis m g ⇒
          a + b ∈ nnfis m (λw. f w + g w)
   
   [nnfis_borel_measurable]  Theorem
      
      ⊢ ∀m f a.
          measure_space m ∧ a ∈ nnfis m f ⇒
          f ∈ borel_measurable (m_space m,measurable_sets m)
   
   [nnfis_dom_conv]  Theorem
      
      ⊢ ∀m f g b.
          measure_space m ∧
          f ∈ borel_measurable (m_space m,measurable_sets m) ∧
          b ∈ nnfis m g ∧ (∀t. t ∈ m_space m ⇒ f t ≤ g t) ∧
          (∀t. t ∈ m_space m ⇒ 0 ≤ f t) ⇒
          ∃a. a ∈ nnfis m f ∧ a ≤ b
   
   [nnfis_integral]  Theorem
      
      ⊢ ∀m f a.
          measure_space m ∧ a ∈ nnfis m f ⇒
          integrable m f ∧ integral m f = a
   
   [nnfis_minus_nnfis_integral]  Theorem
      
      ⊢ ∀m f g a b.
          measure_space m ∧ a ∈ nnfis m f ∧ b ∈ nnfis m g ⇒
          integrable m (λt. f t − g t) ∧ integral m (λt. f t − g t) = a − b
   
   [nnfis_mon_conv]  Theorem
      
      ⊢ ∀f m h x y.
          measure_space m ∧ mono_convergent f h (m_space m) ∧
          (∀n. x n ∈ nnfis m (f n)) ∧ x ⟶ y ⇒
          y ∈ nnfis m h
   
   [nnfis_mono]  Theorem
      
      ⊢ ∀f g m a b.
          measure_space m ∧ a ∈ nnfis m f ∧ b ∈ nnfis m g ∧
          (∀w. w ∈ m_space m ⇒ f w ≤ g w) ⇒
          a ≤ b
   
   [nnfis_pos_on_mspace]  Theorem
      
      ⊢ ∀f m a.
          measure_space m ∧ a ∈ nnfis m f ⇒ ∀x. x ∈ m_space m ⇒ 0 ≤ f x
   
   [nnfis_times]  Theorem
      
      ⊢ ∀f m a z.
          measure_space m ∧ a ∈ nnfis m f ∧ 0 ≤ z ⇒
          z * a ∈ nnfis m (λw. z * f w)
   
   [nnfis_unique]  Theorem
      
      ⊢ ∀f m a b. measure_space m ∧ a ∈ nnfis m f ∧ b ∈ nnfis m f ⇒ a = b
   
   [pos_psfis]  Theorem
      
      ⊢ ∀r m f. measure_space m ∧ r ∈ psfis m f ⇒ 0 ≤ r
   
   [pos_simple_fn_integral_REAL_SUM_IMAGE]  Theorem
      
      ⊢ ∀m f s a x P.
          measure_space m ∧
          (∀i. i ∈ P ⇒ pos_simple_fn m (f i) (s i) (a i) (x i)) ∧ FINITE P ⇒
          ∃s' a' x'.
            pos_simple_fn m (λt. SIGMA (λi. f i t) P) s' a' x' ∧
            pos_simple_fn_integral m s' a' x' =
            SIGMA (λi. pos_simple_fn_integral m (s i) (a i) (x i)) P
   
   [pos_simple_fn_integral_add]  Theorem
      
      ⊢ ∀m f s a x g s' b y.
          measure_space m ∧ pos_simple_fn m f s a x ∧
          pos_simple_fn m g s' b y ⇒
          ∃s'' c z.
            pos_simple_fn m (λx. f x + g x) s'' c z ∧
            pos_simple_fn_integral m s a x +
            pos_simple_fn_integral m s' b y =
            pos_simple_fn_integral m s'' c z
   
   [pos_simple_fn_integral_indicator]  Theorem
      
      ⊢ ∀m A.
          measure_space m ∧ A ∈ measurable_sets m ⇒
          ∃s a x.
            pos_simple_fn m (𝟙 A) s a x ∧
            pos_simple_fn_integral m s a x = measure m A
   
   [pos_simple_fn_integral_mono]  Theorem
      
      ⊢ ∀m f s a x g s' b y.
          measure_space m ∧ pos_simple_fn m f s a x ∧
          pos_simple_fn m g s' b y ∧ (∀x. f x ≤ g x) ⇒
          pos_simple_fn_integral m s a x ≤ pos_simple_fn_integral m s' b y
   
   [pos_simple_fn_integral_mono_on_mspace]  Theorem
      
      ⊢ ∀m f s a x g s' b y.
          measure_space m ∧ pos_simple_fn m f s a x ∧
          pos_simple_fn m g s' b y ∧ (∀x. x ∈ m_space m ⇒ f x ≤ g x) ⇒
          pos_simple_fn_integral m s a x ≤ pos_simple_fn_integral m s' b y
   
   [pos_simple_fn_integral_mult]  Theorem
      
      ⊢ ∀m f s a x.
          measure_space m ∧ pos_simple_fn m f s a x ⇒
          ∀z. 0 ≤ z ⇒
              ∃s' b y.
                pos_simple_fn m (λx. z * f x) s' b y ∧
                pos_simple_fn_integral m s' b y =
                z * pos_simple_fn_integral m s a x
   
   [pos_simple_fn_integral_present]  Theorem
      
      ⊢ ∀m f s a x g s' b y.
          measure_space m ∧ pos_simple_fn m f s a x ∧
          pos_simple_fn m g s' b y ⇒
          ∃z z' c k.
            (∀t. t ∈ m_space m ⇒ f t = SIGMA (λi. z i * 𝟙 (c i) t) k) ∧
            (∀t. t ∈ m_space m ⇒ g t = SIGMA (λi. z' i * 𝟙 (c i) t) k) ∧
            pos_simple_fn_integral m s a x = pos_simple_fn_integral m k c z ∧
            pos_simple_fn_integral m s' b y =
            pos_simple_fn_integral m k c z' ∧ FINITE k ∧
            (∀i j. i ∈ k ∧ j ∈ k ∧ i ≠ j ⇒ DISJOINT (c i) (c j)) ∧
            (∀i. i ∈ k ⇒ c i ∈ measurable_sets m) ∧
            BIGUNION (IMAGE c k) = m_space m ∧ (∀i. 0 ≤ z i) ∧ ∀i. 0 ≤ z' i
   
   [pos_simple_fn_integral_unique]  Theorem
      
      ⊢ ∀m f s a x s' b y.
          measure_space m ∧ pos_simple_fn m f s a x ∧
          pos_simple_fn m f s' b y ⇒
          pos_simple_fn_integral m s a x = pos_simple_fn_integral m s' b y
   
   [psfis_REAL_SUM_IMAGE]  Theorem
      
      ⊢ ∀m f a P.
          measure_space m ∧ (∀i. i ∈ P ⇒ a i ∈ psfis m (f i)) ∧ FINITE P ⇒
          SIGMA a P ∈ psfis m (λt. SIGMA (λi. f i t) P)
   
   [psfis_add]  Theorem
      
      ⊢ ∀m f g a b.
          measure_space m ∧ a ∈ psfis m f ∧ b ∈ psfis m g ⇒
          a + b ∈ psfis m (λx. f x + g x)
   
   [psfis_borel_measurable]  Theorem
      
      ⊢ ∀m f a.
          measure_space m ∧ a ∈ psfis m f ⇒
          f ∈ borel_measurable (m_space m,measurable_sets m)
   
   [psfis_equiv]  Theorem
      
      ⊢ ∀f g a m.
          measure_space m ∧ a ∈ psfis m f ∧ (∀t. 0 ≤ g t) ∧
          (∀t. t ∈ m_space m ⇒ f t = g t) ⇒
          a ∈ psfis m g
   
   [psfis_indicator]  Theorem
      
      ⊢ ∀m A.
          measure_space m ∧ A ∈ measurable_sets m ⇒
          measure m A ∈ psfis m (𝟙 A)
   
   [psfis_intro]  Theorem
      
      ⊢ ∀m a x P.
          measure_space m ∧ (∀i. i ∈ P ⇒ a i ∈ measurable_sets m) ∧
          (∀i. 0 ≤ x i) ∧ FINITE P ⇒
          SIGMA (λi. x i * measure m (a i)) P ∈
          psfis m (λt. SIGMA (λi. x i * 𝟙 (a i) t) P)
   
   [psfis_mono]  Theorem
      
      ⊢ ∀m f g a b.
          measure_space m ∧ a ∈ psfis m f ∧ b ∈ psfis m g ∧
          (∀x. x ∈ m_space m ⇒ f x ≤ g x) ⇒
          a ≤ b
   
   [psfis_mono_conv_mono]  Theorem
      
      ⊢ ∀m f u x y r s.
          measure_space m ∧ mono_convergent u f (m_space m) ∧
          (∀n. x n ∈ psfis m (u n)) ∧ (∀m n. m ≤ n ⇒ x m ≤ x n) ∧ x ⟶ y ∧
          r ∈ psfis m s ∧ (∀a. a ∈ m_space m ⇒ s a ≤ f a) ⇒
          r ≤ y
   
   [psfis_mult]  Theorem
      
      ⊢ ∀m f a.
          measure_space m ∧ a ∈ psfis m f ⇒
          ∀z. 0 ≤ z ⇒ z * a ∈ psfis m (λx. z * f x)
   
   [psfis_nnfis]  Theorem
      
      ⊢ ∀m f a. measure_space m ∧ a ∈ psfis m f ⇒ a ∈ nnfis m f
   
   [psfis_nonneg]  Theorem
      
      ⊢ ∀m f a. a ∈ psfis m f ⇒ nonneg f
   
   [psfis_present]  Theorem
      
      ⊢ ∀m f g a b.
          measure_space m ∧ a ∈ psfis m f ∧ b ∈ psfis m g ⇒
          ∃z z' c k.
            (∀t. t ∈ m_space m ⇒ f t = SIGMA (λi. z i * 𝟙 (c i) t) k) ∧
            (∀t. t ∈ m_space m ⇒ g t = SIGMA (λi. z' i * 𝟙 (c i) t) k) ∧
            a = pos_simple_fn_integral m k c z ∧
            b = pos_simple_fn_integral m k c z' ∧ FINITE k ∧
            (∀i j. i ∈ k ∧ j ∈ k ∧ i ≠ j ⇒ DISJOINT (c i) (c j)) ∧
            (∀i. i ∈ k ⇒ c i ∈ measurable_sets m) ∧
            BIGUNION (IMAGE c k) = m_space m ∧ (∀i. 0 ≤ z i) ∧ ∀i. 0 ≤ z' i
   
   [psfis_unique]  Theorem
      
      ⊢ ∀m f a b. measure_space m ∧ a ∈ psfis m f ∧ b ∈ psfis m f ⇒ a = b
   
   [upclose_psfis]  Theorem
      
      ⊢ ∀f g a b m.
          measure_space m ∧ a ∈ psfis m f ∧ b ∈ psfis m g ⇒
          ∃c. c ∈ psfis m (upclose f g)
   
   
*)
end

HOL 4, Kananaskis-14