Structure lebesgueTheory


Source File Identifier index Theory binding index

signature lebesgueTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val RADON_F_def : thm
    val RADON_F_integrals_def : thm
    val RN_deriv_def : thm
    val density_def : thm
    val density_measure_def : thm
    val distr_def : thm
    val finite_space_integral_def : thm
    val fn_seq_def : thm
    val fn_seq_integral_def : thm
    val integrable_def : thm
    val integral_def : thm
    val measure_absolutely_continuous_def : thm
    val pos_fn_integral_def : thm
    val pos_simple_fn_def : thm
    val pos_simple_fn_integral_def : thm
    val psfis_def : thm
    val psfs_def : thm
    val seq_sup_def : thm
  
  (*  Theorems  *)
    val BOREL_INDUCT : thm
    val EXTREAL_SUP_FUN_SEQ_IMAGE : thm
    val EXTREAL_SUP_FUN_SEQ_MONO_IMAGE : thm
    val EXTREAL_SUP_SEQ : thm
    val IN_MEASURABLE_BOREL_POS_SIMPLE_FN : thm
    val IN_psfis : thm
    val IN_psfis_eq : thm
    val RN_deriv_thm : thm
    val RN_deriv_thm' : thm
    val Radon_Nikodym : thm
    val Radon_Nikodym' : thm
    val Radon_Nikodym_finite : thm
    val Radon_Nikodym_finite_arbitrary : thm
    val Radon_Nikodym_sigma_finite : thm
    val density_fn_plus : thm
    val ext_suminf_cmult_indicator : thm
    val finite_integrable_function_exists : thm
    val finite_space_POW_integral_reduce : thm
    val finite_space_integral_reduce : thm
    val finite_support_integral_reduce : thm
    val integrable_AE_finite : thm
    val integrable_AE_normal : thm
    val integrable_abs : thm
    val integrable_abs_alt : thm
    val integrable_abs_bound_exists : thm
    val integrable_add : thm
    val integrable_add' : thm
    val integrable_add_lemma : thm
    val integrable_add_pos : thm
    val integrable_ainv : thm
    val integrable_bound_exists : thm
    val integrable_bounded : thm
    val integrable_cmul : thm
    val integrable_cong : thm
    val integrable_cong_AE : thm
    val integrable_cong_AE_alt : thm
    val integrable_const : thm
    val integrable_eq : thm
    val integrable_eq_AE : thm
    val integrable_eq_AE_alt : thm
    val integrable_finite_integral : thm
    val integrable_fn_minus : thm
    val integrable_fn_plus : thm
    val integrable_from_abs : thm
    val integrable_from_bound_exists : thm
    val integrable_indicator : thm
    val integrable_indicator_pow : thm
    val integrable_infty : thm
    val integrable_infty_null : thm
    val integrable_measurable : thm
    val integrable_mul_indicator : thm
    val integrable_normal_integral : thm
    val integrable_not_infty : thm
    val integrable_not_infty_alt : thm
    val integrable_not_infty_alt2 : thm
    val integrable_not_infty_alt3 : thm
    val integrable_plus_minus : thm
    val integrable_pos : thm
    val integrable_sub : thm
    val integrable_sub' : thm
    val integrable_sum : thm
    val integrable_sum' : thm
    val integrable_zero : thm
    val integral_abs_eq_0 : thm
    val integral_abs_imp_integrable : thm
    val integral_abs_pos_fn : thm
    val integral_add : thm
    val integral_add' : thm
    val integral_add3 : thm
    val integral_add_lemma : thm
    val integral_add_lemma' : thm
    val integral_cmul : thm
    val integral_cmul_indicator : thm
    val integral_cmul_infty : thm
    val integral_cmul_infty' : thm
    val integral_cong : thm
    val integral_cong_AE : thm
    val integral_const : thm
    val integral_eq_0 : thm
    val integral_indicator : thm
    val integral_indicator_pow : thm
    val integral_indicator_pow_eq : thm
    val integral_mono : thm
    val integral_mono_AE : thm
    val integral_mspace : thm
    val integral_neg : thm
    val integral_neginf : thm
    val integral_null_set : thm
    val integral_pos : thm
    val integral_pos_fn : thm
    val integral_posinf : thm
    val integral_sequence : thm
    val integral_split : thm
    val integral_split' : thm
    val integral_sub : thm
    val integral_sub' : thm
    val integral_sum : thm
    val integral_sum' : thm
    val integral_triangle_ineq : thm
    val integral_triangle_ineq' : thm
    val integral_zero : thm
    val lebesgue_monotone_convergence : thm
    val lebesgue_monotone_convergence_AE : thm
    val lebesgue_monotone_convergence_decreasing : thm
    val lebesgue_monotone_convergence_decreasing' : thm
    val lebesgue_monotone_convergence_subset : thm
    val lemma_fn_seq_measurable : thm
    val lemma_fn_seq_mono_increasing : thm
    val lemma_fn_seq_positive : thm
    val lemma_fn_seq_sup : thm
    val markov_ineq : thm
    val markov_inequality : thm
    val measurable_sequence : thm
    val measure_density_indicator : thm
    val measure_restricted : thm
    val measure_space_density : thm
    val measure_space_density' : thm
    val measure_space_distr : thm
    val measure_subadditive_finite : thm
    val pos_fn_integrable_AE_finite : thm
    val pos_fn_integral_add : thm
    val pos_fn_integral_add3 : thm
    val pos_fn_integral_cmul : thm
    val pos_fn_integral_cmul_indicator : thm
    val pos_fn_integral_cmul_infty : thm
    val pos_fn_integral_cmult : thm
    val pos_fn_integral_cmult' : thm
    val pos_fn_integral_cong : thm
    val pos_fn_integral_cong_AE : thm
    val pos_fn_integral_const : thm
    val pos_fn_integral_density : thm
    val pos_fn_integral_density' : thm
    val pos_fn_integral_disjoint_sets : thm
    val pos_fn_integral_disjoint_sets_sum : thm
    val pos_fn_integral_eq_0 : thm
    val pos_fn_integral_indicator : thm
    val pos_fn_integral_infty_null : thm
    val pos_fn_integral_mono : thm
    val pos_fn_integral_mono_AE : thm
    val pos_fn_integral_mspace : thm
    val pos_fn_integral_null_set : thm
    val pos_fn_integral_pos : thm
    val pos_fn_integral_pos_simple_fn : thm
    val pos_fn_integral_split : thm
    val pos_fn_integral_sub : thm
    val pos_fn_integral_sum : thm
    val pos_fn_integral_sum_cmul_indicator : thm
    val pos_fn_integral_suminf : thm
    val pos_fn_integral_zero : thm
    val pos_simple_fn_add : thm
    val pos_simple_fn_add_alt : thm
    val pos_simple_fn_cmul : thm
    val pos_simple_fn_cmul_alt : thm
    val pos_simple_fn_indicator : thm
    val pos_simple_fn_indicator_alt : thm
    val pos_simple_fn_integral_add : thm
    val pos_simple_fn_integral_add_alt : thm
    val pos_simple_fn_integral_cmul : thm
    val pos_simple_fn_integral_cmul_alt : thm
    val pos_simple_fn_integral_indicator : thm
    val pos_simple_fn_integral_mono : thm
    val pos_simple_fn_integral_not_infty : thm
    val pos_simple_fn_integral_present : thm
    val pos_simple_fn_integral_sub : thm
    val pos_simple_fn_integral_sum : thm
    val pos_simple_fn_integral_sum_alt : thm
    val pos_simple_fn_integral_unique : thm
    val pos_simple_fn_integral_zero : thm
    val pos_simple_fn_integral_zero_alt : thm
    val pos_simple_fn_le : thm
    val pos_simple_fn_max : thm
    val pos_simple_fn_not_infty : thm
    val pos_simple_fn_thm1 : thm
    val psfis_add : thm
    val psfis_cmul : thm
    val psfis_indicator : thm
    val psfis_intro : thm
    val psfis_mono : thm
    val psfis_not_infty : thm
    val psfis_pos : thm
    val psfis_present : thm
    val psfis_sub : thm
    val psfis_sum : thm
    val psfis_unique : thm
    val psfis_zero : thm
    val seq_sup_compute : thm
  
  val lebesgue_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [borel] Parent theory of "lebesgue"
   
   [RADON_F_def]  Definition
      
      ⊢ ∀m v.
          RADON_F m v =
          {f |
           f ∈ Borel_measurable (measurable_space m) ∧ (∀x. 0 ≤ f x) ∧
           ∀A. A ∈ measurable_sets m ⇒ ∫⁺ m (λx. f x * 𝟙 A x) ≤ measure v A}
   
   [RADON_F_integrals_def]  Definition
      
      ⊢ ∀m v.
          RADON_F_integrals m v = {r | ∃f. r = ∫⁺ m f ∧ f ∈ RADON_F m v}
   
   [RN_deriv_def]  Definition
      
      ⊢ ∀v m.
          v / m =
          @f. f ∈ Borel_measurable (measurable_space m) ∧
              (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
              ∀s. s ∈ measurable_sets m ⇒ (f * m) s = v s
   
   [density_def]  Definition
      
      ⊢ ∀m f. density m f = (m_space m,measurable_sets m,f * m)
   
   [density_measure_def]  Definition
      
      ⊢ ∀m f. f * m = (λs. ∫⁺ m (λx. f x * 𝟙 s x))
   
   [distr_def]  Definition
      
      ⊢ ∀m f. distr m f = (λs. measure m (PREIMAGE f s ∩ m_space m))
   
   [finite_space_integral_def]  Definition
      
      ⊢ ∀m f.
          finite_space_integral m f =
          ∑ (λr. r * measure m (PREIMAGE f {r} ∩ m_space m))
            (IMAGE f (m_space m))
   
   [fn_seq_def]  Definition
      
      ⊢ ∀m f.
          fn_seq m f =
          (λn x.
               ∑
                 (λk.
                      &k / 2 pow n *
                      𝟙
                        {x |
                         x ∈ m_space m ∧ &k / 2 pow n ≤ f x ∧
                         f x < (&k + 1) / 2 pow n} x) (count (4 ** n)) +
               2 pow n * 𝟙 {x | x ∈ m_space m ∧ 2 pow n ≤ f x} x)
   
   [fn_seq_integral_def]  Definition
      
      ⊢ ∀m f.
          fn_seq_integral m f =
          (λn.
               ∑
                 (λk.
                      &k / 2 pow n *
                      measure m
                        {x |
                         x ∈ m_space m ∧ &k / 2 pow n ≤ f x ∧
                         f x < (&k + 1) / 2 pow n}) (count (4 ** n)) +
               2 pow n * measure m {x | x ∈ m_space m ∧ 2 pow n ≤ f x})
   
   [integrable_def]  Definition
      
      ⊢ ∀m f.
          integrable m f ⇔
          f ∈ Borel_measurable (measurable_space m) ∧ ∫⁺ m f⁺ ≠ +∞ ∧
          ∫⁺ m f⁻ ≠ +∞
   
   [integral_def]  Definition
      
      ⊢ ∀m f. ∫ m f = ∫⁺ m f⁺ − ∫⁺ m f⁻
   
   [measure_absolutely_continuous_def]  Definition
      
      ⊢ ∀v m. v ≪ m ⇔ ∀s. s ∈ measurable_sets m ∧ measure m s = 0 ⇒ v s = 0
   
   [pos_fn_integral_def]  Definition
      
      ⊢ ∀m f.
          ∫⁺ m f =
          sup {r | (∃g. r ∈ psfis m g ∧ ∀x. x ∈ m_space m ⇒ g x ≤ f x)}
   
   [pos_simple_fn_def]  Definition
      
      ⊢ ∀m f s a x.
          pos_simple_fn m f s a x ⇔
          (∀t. t ∈ m_space m ⇒ 0 ≤ f t) ∧
          (∀t. t ∈ m_space m ⇒ f t = ∑ (λi. Normal (x i) * 𝟙 (a i) t) s) ∧
          (∀i. i ∈ s ⇒ a i ∈ measurable_sets m) ∧ FINITE s ∧
          (∀i. i ∈ s ⇒ 0 ≤ x i) ∧
          (∀i j. i ∈ s ∧ j ∈ s ∧ i ≠ j ⇒ DISJOINT (a i) (a j)) ∧
          BIGUNION (IMAGE a s) = m_space m
   
   [pos_simple_fn_integral_def]  Definition
      
      ⊢ ∀m s a x.
          pos_simple_fn_integral m s a x =
          ∑ (λi. Normal (x i) * measure m (a i)) s
   
   [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}
   
   [seq_sup_def]  Definition
      
      ⊢ (∀P. seq_sup P 0 = @r. r ∈ P ∧ sup P < r + 1) ∧
        ∀P n.
          seq_sup P (SUC n) =
          @r. r ∈ P ∧ sup P < r + Normal ((1 / 2) pow SUC n) ∧
              seq_sup P n < r ∧ r < sup P
   
   [BOREL_INDUCT]  Theorem
      
      ⊢ ∀f m P.
          measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ∧
          (∀x. 0 ≤ f x) ∧
          (∀f g.
             f ∈ Borel_measurable (measurable_space m) ∧
             g ∈ Borel_measurable (measurable_space m) ∧
             (∀x. x ∈ m_space m ⇒ f x = g x) ∧ P f ⇒
             P g) ∧ (∀A. A ∈ measurable_sets m ⇒ P (𝟙 A)) ∧
          (∀f c.
             f ∈ Borel_measurable (measurable_space m) ∧ 0 ≤ c ∧
             (∀x. 0 ≤ f x) ∧ P f ⇒
             P (λx. c * f x)) ∧
          (∀f g.
             f ∈ Borel_measurable (measurable_space m) ∧
             g ∈ Borel_measurable (measurable_space m) ∧ (∀x. 0 ≤ f x) ∧
             P f ∧ (∀x. 0 ≤ g x) ∧ P g ⇒
             P (λx. f x + g x)) ∧
          (∀u. (∀i. u i ∈ Borel_measurable (measurable_space m)) ∧
               (∀i x. 0 ≤ u i x) ∧ (∀x. mono_increasing (λi. u i x)) ∧
               (∀i. P (u i)) ⇒
               P (λx. sup (IMAGE (λi. u i x) 𝕌(:num)))) ⇒
          P f
   
   [EXTREAL_SUP_FUN_SEQ_IMAGE]  Theorem
      
      ⊢ ∀P P' f.
          (∃x. P x) ∧ (∃z. z ≠ +∞ ∧ ∀x. P x ⇒ x ≤ z) ∧ P = IMAGE f P' ⇒
          ∃g. (∀n. g n ∈ P') ∧ sup (IMAGE (λn. f (g n)) 𝕌(:num)) = sup P
   
   [EXTREAL_SUP_FUN_SEQ_MONO_IMAGE]  Theorem
      
      ⊢ ∀f P P'.
          (∃x. P x) ∧ (∃z. z ≠ +∞ ∧ ∀x. P x ⇒ x ≤ z) ∧ P = IMAGE f P' ∧
          (∀g1 g2. g1 ∈ P' ∧ g2 ∈ P' ∧ (∀x. g1 x ≤ g2 x) ⇒ f g1 ≤ f g2) ∧
          (∀g1 g2. g1 ∈ P' ∧ g2 ∈ P' ⇒ (λx. max (g1 x) (g2 x)) ∈ P') ⇒
          ∃g. (∀n. g n ∈ P') ∧ (∀x n. g n x ≤ g (SUC n) x) ∧
              sup (IMAGE (λn. f (g n)) 𝕌(:num)) = sup P
   
   [EXTREAL_SUP_SEQ]  Theorem
      
      ⊢ ∀P. (∃x. P x) ∧ (∃z. z ≠ +∞ ∧ ∀x. P x ⇒ x ≤ z) ⇒
            ∃x. (∀n. x n ∈ P) ∧ (∀n. x n ≤ x (SUC n)) ∧
                sup (IMAGE x 𝕌(:num)) = sup P
   
   [IN_MEASURABLE_BOREL_POS_SIMPLE_FN]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧ (∃s a x. pos_simple_fn m f s a x) ⇒
          f ∈ Borel_measurable (measurable_space m)
   
   [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
   
   [IN_psfis_eq]  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
   
   [RN_deriv_thm]  Theorem
      
      ⊢ ∀m v.
          measure_space m ∧
          (∃f. f ∈ Borel_measurable (measurable_space m) ∧
               (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
               ∀s. s ∈ measurable_sets m ⇒ (f * m) s = v s) ⇒
          ∀s. s ∈ measurable_sets m ⇒ (v / m * m) s = v s
   
   [RN_deriv_thm']  Theorem
      
      ⊢ ∀f m v.
          measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ∧
          (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
          (∀s. s ∈ measurable_sets m ⇒ (f * m) s = v s) ⇒
          measure_space_eq (density m (v / m))
            (m_space m,measurable_sets m,v)
   
   [Radon_Nikodym]  Theorem
      
      ⊢ ∀m v.
          measure_space m ∧ sigma_finite m ∧
          measure_space (m_space m,measurable_sets m,v) ∧ v ≪ m ⇒
          ∃f. f ∈ Borel_measurable (measurable_space m) ∧ (∀x. 0 ≤ f x) ∧
              ∀s. s ∈ measurable_sets m ⇒ (f * m) s = v s
   
   [Radon_Nikodym']  Theorem
      
      ⊢ ∀m v.
          measure_space m ∧ sigma_finite m ∧
          measure_space (m_space m,measurable_sets m,v) ∧ v ≪ m ⇒
          ∃f. f ∈ Borel_measurable (measurable_space m) ∧
              (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
              ∀s. s ∈ measurable_sets m ⇒ (f * m) s = v s
   
   [Radon_Nikodym_finite]  Theorem
      
      ⊢ ∀M N.
          measure_space M ∧ measure_space N ∧ m_space M = m_space N ∧
          measurable_sets M = measurable_sets N ∧
          measure M (m_space M) ≠ +∞ ∧ measure N (m_space N) ≠ +∞ ∧
          measure N ≪ M ⇒
          ∃f. f ∈ Borel_measurable (measurable_space M) ∧ (∀x. 0 ≤ f x) ∧
              ∀A. A ∈ measurable_sets M ⇒
                  ∫⁺ M (λx. f x * 𝟙 A x) = measure N A
   
   [Radon_Nikodym_finite_arbitrary]  Theorem
      
      ⊢ ∀M N.
          measure_space M ∧ measure_space N ∧ m_space M = m_space N ∧
          measurable_sets M = measurable_sets N ∧
          measure M (m_space M) ≠ +∞ ∧ measure N ≪ M ⇒
          ∃f. f ∈ Borel_measurable (measurable_space M) ∧ (∀x. 0 ≤ f x) ∧
              ∀A. A ∈ measurable_sets M ⇒
                  ∫⁺ M (λx. f x * 𝟙 A x) = measure N A
   
   [Radon_Nikodym_sigma_finite]  Theorem
      
      ⊢ ∀M N.
          measure_space M ∧ measure_space N ∧ m_space M = m_space N ∧
          measurable_sets M = measurable_sets N ∧ sigma_finite M ∧
          measure N ≪ M ⇒
          ∃f. f ∈ Borel_measurable (measurable_space M) ∧ (∀x. 0 ≤ f x) ∧
              ∀A. A ∈ measurable_sets M ⇒
                  ∫⁺ M (λx. f x * 𝟙 A x) = measure N A
   
   [density_fn_plus]  Theorem
      
      ⊢ ∀M f.
          density M f⁺ =
          (m_space M,measurable_sets M,(λA. ∫⁺ M (λx. max 0 (f x * 𝟙 A x))))
   
   [ext_suminf_cmult_indicator]  Theorem
      
      ⊢ ∀A f x i.
          disjoint_family A ∧ x ∈ A i ∧ (∀i. 0 ≤ f i) ⇒
          suminf (λn. f n * 𝟙 (A n) x) = f i
   
   [finite_integrable_function_exists]  Theorem
      
      ⊢ ∀m. measure_space m ∧ sigma_finite m ⇒
            ∃h. h ∈ Borel_measurable (measurable_space m) ∧ ∫⁺ m h ≠ +∞ ∧
                (∀x. x ∈ m_space m ⇒ 0 < h x ∧ h x < +∞) ∧ ∀x. 0 ≤ h x
   
   [finite_space_POW_integral_reduce]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧ POW (m_space m) = measurable_sets m ∧
          FINITE (m_space m) ∧ (∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ f x ≠ +∞) ∧
          measure m (m_space m) < +∞ ⇒
          ∫ m f = ∑ (λx. f x * measure m {x}) (m_space m)
   
   [finite_space_integral_reduce]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ∧
          (∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ f x ≠ +∞) ∧ FINITE (m_space m) ∧
          measure m (m_space m) < +∞ ∧ integrable m f ⇒
          ∫ m f = finite_space_integral m f
   
   [finite_support_integral_reduce]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ∧
          (∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ f x ≠ +∞) ∧
          FINITE (IMAGE f (m_space m)) ∧ integrable m f ∧
          measure m (m_space m) < +∞ ⇒
          ∫ m f = finite_space_integral m f
   
   [integrable_AE_finite]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧ integrable m f ⇒
          AE x::m. f x = (Normal ∘ real ∘ f) x
   
   [integrable_AE_normal]  Theorem
      
      ⊢ ∀m f. measure_space m ∧ integrable m f ⇒ AE x::m. f x < +∞
   
   [integrable_abs]  Theorem
      
      ⊢ ∀m f. measure_space m ∧ integrable m f ⇒ integrable m (abs ∘ f)
   
   [integrable_abs_alt]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ⇒
          (integrable m (abs ∘ f) ⇔ ∫⁺ m (abs ∘ f) ≠ +∞)
   
   [integrable_abs_bound_exists]  Theorem
      
      ⊢ ∀m u.
          measure_space m ∧ integrable m (abs ∘ u) ⇒
          ∃w. integrable m w ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ w x) ∧
              ∀x. x ∈ m_space m ⇒ abs (u x) ≤ w x
   
   [integrable_add]  Theorem
      
      ⊢ ∀m f g.
          measure_space m ∧ integrable m f ∧ integrable m g ∧
          (∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ g x ≠ −∞ ∨ f x ≠ +∞ ∧ g x ≠ +∞) ⇒
          integrable m (λx. f x + g x)
   
   [integrable_add']  Theorem
      
      ⊢ ∀m f g.
          measure_space m ∧ integrable m f ∧ integrable m g ⇒
          integrable m (λx. f x + g x)
   
   [integrable_add_lemma]  Theorem
      
      ⊢ ∀m f g.
          measure_space m ∧ integrable m f ∧ integrable m g ⇒
          integrable m (λx. f⁺ x + g⁺ x) ∧ integrable m (λx. f⁻ x + g⁻ x)
   
   [integrable_add_pos]  Theorem
      
      ⊢ ∀m f g.
          measure_space m ∧ integrable m f ∧ integrable m g ∧
          (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ g x) ⇒
          integrable m (λx. f x + g x)
   
   [integrable_ainv]  Theorem
      
      ⊢ ∀m f. measure_space m ∧ integrable m f ⇒ integrable m (λx. -f x)
   
   [integrable_bound_exists]  Theorem
      
      ⊢ ∀m u.
          measure_space m ∧ integrable m u ⇒
          ∃w. integrable m w ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ w x) ∧
              ∀x. x ∈ m_space m ⇒ abs (u x) ≤ w x
   
   [integrable_bounded]  Theorem
      
      ⊢ ∀m f g.
          measure_space m ∧ integrable m f ∧
          g ∈ Borel_measurable (measurable_space m) ∧
          (∀x. x ∈ m_space m ⇒ abs (g x) ≤ f x) ⇒
          integrable m g
   
   [integrable_cmul]  Theorem
      
      ⊢ ∀m f c.
          measure_space m ∧ integrable m f ⇒
          integrable m (λx. Normal c * f x)
   
   [integrable_cong]  Theorem
      
      ⊢ ∀m f g.
          measure_space m ∧ (∀x. x ∈ m_space m ⇒ f x = g x) ⇒
          (integrable m f ⇔ integrable m g)
   
   [integrable_cong_AE]  Theorem
      
      ⊢ ∀m f g.
          complete_measure_space m ∧ (AE x::m. f x = g x) ⇒
          (integrable m f ⇔ integrable m g)
   
   [integrable_cong_AE_alt]  Theorem
      
      ⊢ ∀m f g.
          measure_space m ∧ (AE x::m. f x = g x) ∧
          f ∈ Borel_measurable (measurable_space m) ∧
          g ∈ Borel_measurable (measurable_space m) ⇒
          (integrable m f ⇔ integrable m g)
   
   [integrable_const]  Theorem
      
      ⊢ ∀m c.
          measure_space m ∧ measure m (m_space m) < +∞ ⇒
          integrable m (λx. Normal c)
   
   [integrable_eq]  Theorem
      
      ⊢ ∀m f g.
          measure_space m ∧ integrable m f ∧
          (∀x. x ∈ m_space m ⇒ f x = g x) ⇒
          integrable m g
   
   [integrable_eq_AE]  Theorem
      
      ⊢ ∀m f g.
          complete_measure_space m ∧ integrable m f ∧ (AE x::m. f x = g x) ⇒
          integrable m g
   
   [integrable_eq_AE_alt]  Theorem
      
      ⊢ ∀m f g.
          measure_space m ∧ integrable m f ∧ (AE x::m. f x = g x) ∧
          g ∈ Borel_measurable (measurable_space m) ⇒
          integrable m g
   
   [integrable_finite_integral]  Theorem
      
      ⊢ ∀m f. measure_space m ∧ integrable m f ⇒ ∫ m f ≠ +∞ ∧ ∫ m f ≠ −∞
   
   [integrable_fn_minus]  Theorem
      
      ⊢ ∀m f. measure_space m ∧ integrable m f ⇒ integrable m f⁻
   
   [integrable_fn_plus]  Theorem
      
      ⊢ ∀m f. measure_space m ∧ integrable m f ⇒ integrable m f⁺
   
   [integrable_from_abs]  Theorem
      
      ⊢ ∀m u.
          measure_space m ∧ u ∈ Borel_measurable (measurable_space m) ∧
          integrable m (abs ∘ u) ⇒
          integrable m u
   
   [integrable_from_bound_exists]  Theorem
      
      ⊢ ∀m u.
          measure_space m ∧ u ∈ Borel_measurable (measurable_space m) ∧
          (∃w. integrable m w ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ w x) ∧
               ∀x. x ∈ m_space m ⇒ abs (u x) ≤ w x) ⇒
          integrable m u
   
   [integrable_indicator]  Theorem
      
      ⊢ ∀m s.
          measure_space m ∧ s ∈ measurable_sets m ∧ measure m s < +∞ ⇒
          integrable m (𝟙 s)
   
   [integrable_indicator_pow]  Theorem
      
      ⊢ ∀m s n.
          measure_space m ∧ s ∈ measurable_sets m ∧ measure m s < +∞ ∧
          0 < n ⇒
          integrable m (λx. 𝟙 s x pow n)
   
   [integrable_infty]  Theorem
      
      ⊢ ∀m f s.
          measure_space m ∧ integrable m f ∧ s ∈ measurable_sets m ∧
          (∀x. x ∈ s ⇒ f x = +∞) ⇒
          measure m s = 0
   
   [integrable_infty_null]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧ integrable m f ⇒
          null_set m {x | x ∈ m_space m ∧ f x = +∞}
   
   [integrable_measurable]  Theorem
      
      ⊢ ∀m f. integrable m f ⇒ f ∈ Borel_measurable (measurable_space m)
   
   [integrable_mul_indicator]  Theorem
      
      ⊢ ∀m s f.
          measure_space m ∧ s ∈ measurable_sets m ∧ integrable m f ⇒
          integrable m (λx. f x * 𝟙 s x)
   
   [integrable_normal_integral]  Theorem
      
      ⊢ ∀m f. measure_space m ∧ integrable m f ⇒ ∃r. ∫ m f = Normal r
   
   [integrable_not_infty]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧ integrable m f ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
          ∃g. integrable m g ∧ (∀x. 0 ≤ g x) ∧ (∀x. g x ≠ +∞) ∧
              ∫ m f = ∫ m g
   
   [integrable_not_infty_alt]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧ integrable m f ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
          integrable m (λx. if f x = +∞ then 0 else f x) ∧
          ∫ m f = ∫ m (λx. if f x = +∞ then 0 else f x)
   
   [integrable_not_infty_alt2]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧ integrable m f ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
          integrable m (λx. if f x = +∞ then 0 else f x) ∧
          ∫⁺ m f = ∫⁺ m (λx. if f x = +∞ then 0 else f x)
   
   [integrable_not_infty_alt3]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧ integrable m f ⇒
          integrable m (λx. if f x = −∞ ∨ f x = +∞ then 0 else f x) ∧
          ∫ m f = ∫ m (λx. if f x = −∞ ∨ f x = +∞ then 0 else f x)
   
   [integrable_plus_minus]  Theorem
      
      ⊢ ∀m f.
          measure_space m ⇒
          (integrable m f ⇔
           f ∈ Borel_measurable (measurable_space m) ∧ integrable m f⁺ ∧
           integrable m f⁻)
   
   [integrable_pos]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
          (integrable m f ⇔
           f ∈ Borel_measurable (measurable_space m) ∧ ∫⁺ m f ≠ +∞)
   
   [integrable_sub]  Theorem
      
      ⊢ ∀m f g.
          measure_space m ∧ integrable m f ∧ integrable m g ∧
          (∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ g x ≠ +∞) ⇒
          integrable m (λx. f x − g x)
   
   [integrable_sub']  Theorem
      
      ⊢ ∀m f g.
          measure_space m ∧ integrable m f ∧ integrable m g ⇒
          integrable m (λx. f x − g x)
   
   [integrable_sum]  Theorem
      
      ⊢ ∀m f s.
          FINITE s ∧ measure_space m ∧ (∀i. i ∈ s ⇒ integrable m (f i)) ∧
          (∀i x. i ∈ s ∧ x ∈ m_space m ⇒ f i x ≠ +∞ ∧ f i x ≠ −∞) ⇒
          integrable m (λx. ∑ (λi. f i x) s)
   
   [integrable_sum']  Theorem
      
      ⊢ ∀m f s.
          FINITE s ∧ measure_space m ∧ (∀i. i ∈ s ⇒ integrable m (f i)) ⇒
          integrable m (λx. ∑ (λi. f i x) s)
   
   [integrable_zero]  Theorem
      
      ⊢ ∀m c. measure_space m ⇒ integrable m (λx. 0)
   
   [integral_abs_eq_0]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ⇒
          (∫ m (abs ∘ f) = 0 ⇔ AE x::m. (abs ∘ f) x = 0) ∧
          ((AE x::m. (abs ∘ f) x = 0) ⇔
           measure m {x | x ∈ m_space m ∧ f x ≠ 0} = 0)
   
   [integral_abs_imp_integrable]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ∧
          ∫ m (abs ∘ f) = 0 ⇒
          integrable m f
   
   [integral_abs_pos_fn]  Theorem
      
      ⊢ ∀m f. measure_space m ⇒ ∫ m (abs ∘ f) = ∫⁺ m (abs ∘ f)
   
   [integral_add]  Theorem
      
      ⊢ ∀m f g.
          measure_space m ∧ integrable m f ∧ integrable m g ∧
          (∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ g x ≠ −∞ ∨ f x ≠ +∞ ∧ g x ≠ +∞) ⇒
          ∫ m (λx. f x + g x) = ∫ m f + ∫ m g
   
   [integral_add']  Theorem
      
      ⊢ ∀m f g.
          measure_space m ∧ integrable m f ∧ integrable m g ⇒
          ∫ m (λx. f x + g x) = ∫ m f + ∫ m g
   
   [integral_add3]  Theorem
      
      ⊢ ∀m f g h.
          measure_space m ∧ integrable m f ∧ integrable m g ∧
          integrable m h ⇒
          ∫ m (λx. f x + g x + h x) = ∫ m f + ∫ m g + ∫ m h
   
   [integral_add_lemma]  Theorem
      
      ⊢ ∀m f f1 f2.
          measure_space m ∧ integrable m f ∧ integrable m f1 ∧
          integrable m f2 ∧ (∀x. x ∈ m_space m ⇒ f x = f1 x − f2 x) ∧
          (∀x. x ∈ m_space m ⇒ 0 ≤ f1 x) ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f2 x) ∧
          (∀x. x ∈ m_space m ⇒ f1 x ≠ +∞ ∨ f2 x ≠ +∞) ⇒
          ∫ m f = ∫⁺ m f1 − ∫⁺ m f2
   
   [integral_add_lemma']  Theorem
      
      ⊢ ∀m f f1 f2.
          measure_space m ∧ integrable m f ∧ integrable m f1 ∧
          integrable m f2 ∧ (∀x. x ∈ m_space m ⇒ f x = f1 x − f2 x) ∧
          (∀x. x ∈ m_space m ⇒ 0 ≤ f1 x) ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f2 x) ⇒
          ∫ m f = ∫⁺ m f1 − ∫⁺ m f2
   
   [integral_cmul]  Theorem
      
      ⊢ ∀m f c.
          measure_space m ∧ integrable m f ⇒
          ∫ m (λx. Normal c * f x) = Normal c * ∫ m f
   
   [integral_cmul_indicator]  Theorem
      
      ⊢ ∀m s c.
          measure_space m ∧ s ∈ measurable_sets m ∧ measure m s < +∞ ⇒
          ∫ m (λx. Normal c * 𝟙 s x) = Normal c * measure m s
   
   [integral_cmul_infty]  Theorem
      
      ⊢ ∀m s.
          measure_space m ∧ s ∈ measurable_sets m ⇒
          ∫ m (λx. +∞ * 𝟙 s x) = +∞ * measure m s
   
   [integral_cmul_infty']  Theorem
      
      ⊢ ∀m s.
          measure_space m ∧ s ∈ measurable_sets m ⇒
          ∫ m (λx. −∞ * 𝟙 s x) = −∞ * measure m s
   
   [integral_cong]  Theorem
      
      ⊢ ∀m f g.
          measure_space m ∧ (∀x. x ∈ m_space m ⇒ f x = g x) ⇒ ∫ m f = ∫ m g
   
   [integral_cong_AE]  Theorem
      
      ⊢ ∀m f g. measure_space m ∧ (AE x::m. f x = g x) ⇒ ∫ m f = ∫ m g
   
   [integral_const]  Theorem
      
      ⊢ ∀m c.
          measure_space m ∧ measure m (m_space m) < +∞ ⇒
          ∫ m (λx. Normal c) = Normal c * measure m (m_space m)
   
   [integral_eq_0]  Theorem
      
      ⊢ ∀m f.
          f ∈ Borel_measurable (measurable_space m) ∧ measure_space m ∧
          (AE x::m. 0 ≤ f x) ⇒
          (∫ m f = 0 ⇔ measure m {x | x ∈ m_space m ∧ f x ≠ 0} = 0)
   
   [integral_indicator]  Theorem
      
      ⊢ ∀m s.
          measure_space m ∧ s ∈ measurable_sets m ⇒ ∫ m (𝟙 s) = measure m s
   
   [integral_indicator_pow]  Theorem
      
      ⊢ ∀m s n.
          measure_space m ∧ s ∈ measurable_sets m ∧ 0 < n ⇒
          ∫ m (λx. 𝟙 s x pow n) = measure m s
   
   [integral_indicator_pow_eq]  Theorem
      
      ⊢ ∀m s n.
          measure_space m ∧ s ∈ measurable_sets m ∧ 0 < n ⇒
          ∫ m (λx. 𝟙 s x pow n) = ∫ m (𝟙 s)
   
   [integral_mono]  Theorem
      
      ⊢ ∀m f1 f2.
          measure_space m ∧ integrable m f1 ∧ integrable m f2 ∧
          (∀x. x ∈ m_space m ⇒ f1 x ≤ f2 x) ⇒
          ∫ m f1 ≤ ∫ m f2
   
   [integral_mono_AE]  Theorem
      
      ⊢ ∀m f g. measure_space m ∧ (AE x::m. f x ≤ g x) ⇒ ∫ m f ≤ ∫ m g
   
   [integral_mspace]  Theorem
      
      ⊢ ∀m f. measure_space m ⇒ ∫ m f = ∫ m (λx. f x * 𝟙 (m_space m) x)
   
   [integral_neg]  Theorem
      
      ⊢ ∀m f. measure_space m ∧ (∀x. x ∈ m_space m ⇒ f x ≤ 0) ⇒ ∫ m f ≤ 0
   
   [integral_neginf]  Theorem
      
      ⊢ ∀m. measure_space m ∧ 0 < measure m (m_space m) ⇒ ∫ m (λx. −∞) = −∞
   
   [integral_null_set]  Theorem
      
      ⊢ ∀m f N.
          measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ∧
          N ∈ null_set m ⇒
          integrable m (λx. f x * 𝟙 N x) ∧ ∫ m (λx. f x * 𝟙 N x) = 0
   
   [integral_pos]  Theorem
      
      ⊢ ∀m f. measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒ 0 ≤ ∫ m f
   
   [integral_pos_fn]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒ ∫ m f = ∫⁺ m f
   
   [integral_posinf]  Theorem
      
      ⊢ ∀m. measure_space m ∧ 0 < measure m (m_space m) ⇒ ∫ m (λx. +∞) = +∞
   
   [integral_sequence]  Theorem
      
      ⊢ ∀m f.
          (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧ measure_space m ∧
          f ∈ Borel_measurable (measurable_space m) ⇒
          ∫⁺ m f = sup (IMAGE (λi. ∫⁺ m (fn_seq m f i)) 𝕌(:num))
   
   [integral_split]  Theorem
      
      ⊢ ∀m f s.
          measure_space m ∧ s ∈ measurable_sets m ∧
          (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
          f ∈ Borel_measurable (measurable_space m) ⇒
          ∫ m f =
          ∫ m (λx. f x * 𝟙 s x) + ∫ m (λx. f x * 𝟙 (m_space m DIFF s) x)
   
   [integral_split']  Theorem
      
      ⊢ ∀m f s.
          measure_space m ∧ integrable m f ∧ s ∈ measurable_sets m ⇒
          ∫ m f =
          ∫ m (λx. f x * 𝟙 s x) + ∫ m (λx. f x * 𝟙 (m_space m DIFF s) x)
   
   [integral_sub]  Theorem
      
      ⊢ ∀m f g.
          measure_space m ∧ integrable m f ∧ integrable m g ∧
          (∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ g x ≠ +∞ ∨ f x ≠ +∞ ∧ g x ≠ −∞) ⇒
          ∫ m (λx. f x − g x) = ∫ m f − ∫ m g
   
   [integral_sub']  Theorem
      
      ⊢ ∀m f g.
          measure_space m ∧ integrable m f ∧ integrable m g ⇒
          ∫ m (λx. f x − g x) = ∫ m f − ∫ m g
   
   [integral_sum]  Theorem
      
      ⊢ ∀m f s.
          FINITE s ∧ measure_space m ∧ (∀i. i ∈ s ⇒ integrable m (f i)) ∧
          (∀x i. i ∈ s ∧ x ∈ m_space m ⇒ f i x ≠ +∞ ∧ f i x ≠ −∞) ⇒
          ∫ m (λx. ∑ (λi. f i x) s) = ∑ (λi. ∫ m (f i)) s
   
   [integral_sum']  Theorem
      
      ⊢ ∀m f s.
          FINITE s ∧ measure_space m ∧ (∀i. i ∈ s ⇒ integrable m (f i)) ⇒
          ∫ m (λx. ∑ (λi. f i x) s) = ∑ (λi. ∫ m (f i)) s
   
   [integral_triangle_ineq]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧ integrable m f ⇒ abs (∫ m f) ≤ ∫ m (abs ∘ f)
   
   [integral_triangle_ineq']  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧ integrable m f ⇒ abs (∫ m f) ≤ ∫⁺ m (abs ∘ f)
   
   [integral_zero]  Theorem
      
      ⊢ ∀m. measure_space m ⇒ ∫ m (λx. 0) = 0
   
   [lebesgue_monotone_convergence]  Theorem
      
      ⊢ ∀m f fi.
          measure_space m ∧
          (∀i. fi i ∈ Borel_measurable (measurable_space m)) ∧
          (∀i x. x ∈ m_space m ⇒ 0 ≤ fi i x) ∧
          (∀x. x ∈ m_space m ⇒ mono_increasing (λi. fi i x)) ∧
          (∀x. x ∈ m_space m ⇒ sup (IMAGE (λi. fi i x) 𝕌(:num)) = f x) ⇒
          ∫⁺ m f = sup (IMAGE (λi. ∫⁺ m (fi i)) 𝕌(:num))
   
   [lebesgue_monotone_convergence_AE]  Theorem
      
      ⊢ ∀m f fi.
          measure_space m ∧
          (∀i. fi i ∈ Borel_measurable (measurable_space m)) ∧
          (AE x::m. ∀i. fi i x ≤ fi (SUC i) x ∧ 0 ≤ fi i x) ∧
          (∀x. x ∈ m_space m ⇒ sup (IMAGE (λi. fi i x) 𝕌(:num)) = f x) ⇒
          ∫⁺ m f⁺ = sup (IMAGE (λi. ∫⁺ m (fi i)⁺) 𝕌(:num))
   
   [lebesgue_monotone_convergence_decreasing]  Theorem
      
      ⊢ ∀m f fi.
          measure_space m ∧
          (∀i. fi i ∈ Borel_measurable (measurable_space m)) ∧
          (∀i x. x ∈ m_space m ⇒ 0 ≤ fi i x ∧ fi i x < +∞) ∧
          (∀i. ∫⁺ m (fi i) ≠ +∞) ∧
          (∀x. x ∈ m_space m ⇒ mono_decreasing (λi. fi i x)) ∧
          (∀x. x ∈ m_space m ⇒ inf (IMAGE (λi. fi i x) 𝕌(:num)) = f x) ⇒
          ∫⁺ m f = inf (IMAGE (λi. ∫⁺ m (fi i)) 𝕌(:num))
   
   [lebesgue_monotone_convergence_decreasing']  Theorem
      
      ⊢ ∀m f fi A.
          measure_space m ∧
          (∀i. fi i ∈ Borel_measurable (measurable_space m)) ∧
          (∀i x. x ∈ m_space m ⇒ 0 ≤ fi i x ∧ fi i x < +∞) ∧
          (∀i. ∫⁺ m (fi i) ≠ +∞) ∧
          (∀x. x ∈ m_space m ⇒ mono_decreasing (λi. fi i x)) ∧
          (∀x. x ∈ m_space m ⇒ inf (IMAGE (λi. fi i x) 𝕌(:num)) = f x) ∧
          A ∈ measurable_sets m ⇒
          ∫⁺ m (λx. f x * 𝟙 A x) =
          inf (IMAGE (λi. ∫⁺ m (λx. fi i x * 𝟙 A x)) 𝕌(:num))
   
   [lebesgue_monotone_convergence_subset]  Theorem
      
      ⊢ ∀m f fi A.
          measure_space m ∧
          (∀i. fi i ∈ Borel_measurable (measurable_space m)) ∧
          (∀i x. x ∈ m_space m ⇒ 0 ≤ fi i x) ∧
          (∀x. x ∈ m_space m ⇒ sup (IMAGE (λi. fi i x) 𝕌(:num)) = f x) ∧
          (∀x. x ∈ m_space m ⇒ mono_increasing (λi. fi i x)) ∧
          A ∈ measurable_sets m ⇒
          ∫⁺ m (λx. f x * 𝟙 A x) =
          sup (IMAGE (λi. ∫⁺ m (λx. fi i x * 𝟙 A x)) 𝕌(:num))
   
   [lemma_fn_seq_measurable]  Theorem
      
      ⊢ ∀m f n.
          measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
          f ∈ Borel_measurable (measurable_space m) ⇒
          fn_seq m f n ∈ Borel_measurable (measurable_space m)
   
   [lemma_fn_seq_mono_increasing]  Theorem
      
      ⊢ ∀m f x. 0 ≤ f x ⇒ mono_increasing (λn. fn_seq m f n x)
   
   [lemma_fn_seq_positive]  Theorem
      
      ⊢ ∀m f n x. 0 ≤ f x ⇒ 0 ≤ fn_seq m f n x
   
   [lemma_fn_seq_sup]  Theorem
      
      ⊢ ∀m f x.
          x ∈ m_space m ∧ 0 ≤ f x ⇒
          sup (IMAGE (λn. fn_seq m f n x) 𝕌(:num)) = f x
   
   [markov_ineq]  Theorem
      
      ⊢ ∀m f c.
          measure_space m ∧ integrable m f ∧ 0 < c ⇒
          measure m ({x | c ≤ abs (f x)} ∩ m_space m) ≤ c⁻¹ * ∫ m (abs ∘ f)
   
   [markov_inequality]  Theorem
      
      ⊢ ∀m f a c.
          measure_space m ∧ integrable m f ∧ a ∈ measurable_sets m ∧ 0 < c ⇒
          measure m ({x | c ≤ abs (f x)} ∩ a) ≤
          c⁻¹ * ∫ m (λx. abs (f x) * 𝟙 a x)
   
   [measurable_sequence]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ⇒
          (∃fi ri.
             (∀x. mono_increasing (λi. fi i x)) ∧
             (∀x. x ∈ m_space m ⇒ sup (IMAGE (λi. fi i x) 𝕌(:num)) = f⁺ x) ∧
             (∀i. ri i ∈ psfis m (fi i)) ∧ (∀i x. fi i x ≤ f⁺ x) ∧
             (∀i x. 0 ≤ fi i x) ∧
             ∫⁺ m f⁺ = sup (IMAGE (λi. ∫⁺ m (fi i)) 𝕌(:num))) ∧
          ∃gi vi.
            (∀x. mono_increasing (λi. gi i x)) ∧
            (∀x. x ∈ m_space m ⇒ sup (IMAGE (λi. gi i x) 𝕌(:num)) = f⁻ x) ∧
            (∀i. vi i ∈ psfis m (gi i)) ∧ (∀i x. gi i x ≤ f⁻ x) ∧
            (∀i x. 0 ≤ gi i x) ∧
            ∫⁺ m f⁻ = sup (IMAGE (λi. ∫⁺ m (gi i)) 𝕌(:num))
   
   [measure_density_indicator]  Theorem
      
      ⊢ ∀m s t.
          measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
          measure (density m (𝟙 s)) t = measure m (s ∩ t)
   
   [measure_restricted]  Theorem
      
      ⊢ ∀m s t.
          measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
          measure
            (m_space m,measurable_sets m,(λA. ∫⁺ m (λx. 𝟙 s x * 𝟙 A x))) t =
          measure m (s ∩ t)
   
   [measure_space_density]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ∧
          (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
          measure_space (density m f)
   
   [measure_space_density']  Theorem
      
      ⊢ ∀M f.
          measure_space M ∧ f ∈ Borel_measurable (measurable_space M) ⇒
          measure_space (density M f⁺)
   
   [measure_space_distr]  Theorem
      
      ⊢ ∀M B f.
          measure_space M ∧ sigma_algebra B ∧
          f ∈ measurable (measurable_space M) B ⇒
          measure_space (space B,subsets B,distr M f)
   
   [measure_subadditive_finite]  Theorem
      
      ⊢ ∀J A M.
          measure_space M ∧ FINITE J ∧ IMAGE A J ⊆ measurable_sets M ⇒
          measure M (BIGUNION {A i | i ∈ J}) ≤ ∑ (λi. measure M (A i)) J
   
   [pos_fn_integrable_AE_finite]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
          f ∈ Borel_measurable (measurable_space m) ∧ ∫⁺ m f ≠ +∞ ⇒
          AE x::m. f x = (Normal ∘ real ∘ f) x
   
   [pos_fn_integral_add]  Theorem
      
      ⊢ ∀m f g.
          measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
          (∀x. x ∈ m_space m ⇒ 0 ≤ g x) ∧
          f ∈ Borel_measurable (measurable_space m) ∧
          g ∈ Borel_measurable (measurable_space m) ⇒
          ∫⁺ m (λx. f x + g x) = ∫⁺ m f + ∫⁺ m g
   
   [pos_fn_integral_add3]  Theorem
      
      ⊢ ∀m f g h.
          measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
          (∀x. x ∈ m_space m ⇒ 0 ≤ g x) ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ h x) ∧
          f ∈ Borel_measurable (measurable_space m) ∧
          g ∈ Borel_measurable (measurable_space m) ∧
          h ∈ Borel_measurable (measurable_space m) ⇒
          ∫⁺ m (λx. f x + g x + h x) = ∫⁺ m f + ∫⁺ m g + ∫⁺ m h
   
   [pos_fn_integral_cmul]  Theorem
      
      ⊢ ∀m f c.
          measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧ 0 ≤ c ⇒
          ∫⁺ m (λx. Normal c * f x) = Normal c * ∫⁺ m f
   
   [pos_fn_integral_cmul_indicator]  Theorem
      
      ⊢ ∀m s c.
          measure_space m ∧ s ∈ measurable_sets m ∧ 0 ≤ c ⇒
          ∫⁺ m (λx. Normal c * 𝟙 s x) = Normal c * measure m s
   
   [pos_fn_integral_cmul_infty]  Theorem
      
      ⊢ ∀m s.
          measure_space m ∧ s ∈ measurable_sets m ⇒
          ∫⁺ m (λx. +∞ * 𝟙 s x) = +∞ * measure m s
   
   [pos_fn_integral_cmult]  Theorem
      
      ⊢ ∀f c m.
          measure_space m ∧ 0 ≤ c ∧
          f ∈ Borel_measurable (measurable_space m) ⇒
          ∫⁺ m (λx. c * f⁺ x) = c * ∫⁺ m f⁺
   
   [pos_fn_integral_cmult']  Theorem
      
      ⊢ ∀f c m.
          measure_space m ∧ 0 ≤ c ∧
          f ∈ Borel_measurable (measurable_space m) ⇒
          ∫⁺ m (λx. max 0 (c * f x)) = c * ∫⁺ m (λx. max 0 (f x))
   
   [pos_fn_integral_cong]  Theorem
      
      ⊢ ∀m u v.
          measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ u x) ∧
          (∀x. x ∈ m_space m ⇒ 0 ≤ v x) ∧ (∀x. x ∈ m_space m ⇒ u x = v x) ⇒
          ∫⁺ m u = ∫⁺ m v
   
   [pos_fn_integral_cong_AE]  Theorem
      
      ⊢ ∀m u v.
          measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ u x) ∧
          (∀x. x ∈ m_space m ⇒ 0 ≤ v x) ∧ (AE x::m. u x = v x) ⇒
          ∫⁺ m u = ∫⁺ m v
   
   [pos_fn_integral_const]  Theorem
      
      ⊢ ∀m c.
          measure_space m ∧ measure m (m_space m) < +∞ ∧ 0 ≤ c ⇒
          ∫⁺ m (λx. Normal c) = Normal c * measure m (m_space m)
   
   [pos_fn_integral_density]  Theorem
      
      ⊢ ∀m f g.
          measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ∧
          g ∈ Borel_measurable (measurable_space m) ∧ (AE x::m. 0 ≤ f x) ∧
          (∀x. 0 ≤ g x) ⇒
          ∫⁺ (density m f⁺) g = ∫⁺ m (λx. f⁺ x * g x)
   
   [pos_fn_integral_density']  Theorem
      
      ⊢ ∀f g M.
          measure_space M ∧ f ∈ Borel_measurable (measurable_space M) ∧
          g ∈ Borel_measurable (measurable_space M) ∧ (AE x::M. 0 ≤ f x) ∧
          (∀x. 0 ≤ g x) ⇒
          ∫⁺
            (m_space M,measurable_sets M,
             (λA. ∫⁺ M (λx. max 0 (f x * 𝟙 A x)))) (λx. max 0 (g x)) =
          ∫⁺ M (λx. max 0 (f x * g x))
   
   [pos_fn_integral_disjoint_sets]  Theorem
      
      ⊢ ∀m f s t.
          measure_space m ∧ DISJOINT s t ∧ s ∈ measurable_sets m ∧
          t ∈ measurable_sets m ∧
          f ∈ Borel_measurable (measurable_space m) ∧
          (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
          ∫⁺ m (λx. f x * 𝟙 (s ∪ t) x) =
          ∫⁺ m (λx. f x * 𝟙 s x) + ∫⁺ m (λx. f x * 𝟙 t x)
   
   [pos_fn_integral_disjoint_sets_sum]  Theorem
      
      ⊢ ∀m f s a.
          FINITE s ∧ measure_space m ∧
          (∀i. i ∈ s ⇒ a i ∈ measurable_sets m) ∧
          (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
          (∀i j. i ∈ s ∧ j ∈ s ∧ i ≠ j ⇒ DISJOINT (a i) (a j)) ∧
          f ∈ Borel_measurable (measurable_space m) ⇒
          ∫⁺ m (λx. f x * 𝟙 (BIGUNION (IMAGE a s)) x) =
          ∑ (λi. ∫⁺ m (λx. f x * 𝟙 (a i) x)) s
   
   [pos_fn_integral_eq_0]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
          f ∈ Borel_measurable (measurable_space m) ⇒
          (∫⁺ m f = 0 ⇔ measure m {x | x ∈ m_space m ∧ f x ≠ 0} = 0)
   
   [pos_fn_integral_indicator]  Theorem
      
      ⊢ ∀m s.
          measure_space m ∧ s ∈ measurable_sets m ⇒
          ∫⁺ m (𝟙 s) = measure m s
   
   [pos_fn_integral_infty_null]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
          f ∈ Borel_measurable (measurable_space m) ∧ ∫⁺ m f ≠ +∞ ⇒
          null_set m {x | x ∈ m_space m ∧ f x = +∞}
   
   [pos_fn_integral_mono]  Theorem
      
      ⊢ ∀m f g.
          (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧ (∀x. x ∈ m_space m ⇒ f x ≤ g x) ⇒
          ∫⁺ m f ≤ ∫⁺ m g
   
   [pos_fn_integral_mono_AE]  Theorem
      
      ⊢ ∀m u v.
          measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ u x) ∧
          (∀x. x ∈ m_space m ⇒ 0 ≤ v x) ∧ (AE x::m. u x ≤ v x) ⇒
          ∫⁺ m u ≤ ∫⁺ m v
   
   [pos_fn_integral_mspace]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
          ∫⁺ m f = ∫⁺ m (λx. f x * 𝟙 (m_space m) x)
   
   [pos_fn_integral_null_set]  Theorem
      
      ⊢ ∀m f N.
          measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧ N ∈ null_set m ⇒
          ∫⁺ m (λx. f x * 𝟙 N x) = 0
   
   [pos_fn_integral_pos]  Theorem
      
      ⊢ ∀m f. measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒ 0 ≤ ∫⁺ m f
   
   [pos_fn_integral_pos_simple_fn]  Theorem
      
      ⊢ ∀m f s a x.
          measure_space m ∧ pos_simple_fn m f s a x ⇒
          ∫⁺ m f = pos_simple_fn_integral m s a x
   
   [pos_fn_integral_split]  Theorem
      
      ⊢ ∀m f s.
          measure_space m ∧ s ∈ measurable_sets m ∧
          (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
          f ∈ Borel_measurable (measurable_space m) ⇒
          ∫⁺ m f =
          ∫⁺ m (λx. f x * 𝟙 s x) + ∫⁺ m (λx. f x * 𝟙 (m_space m DIFF s) x)
   
   [pos_fn_integral_sub]  Theorem
      
      ⊢ ∀m f g.
          measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ∧
          g ∈ Borel_measurable (measurable_space m) ∧
          (∀x. x ∈ m_space m ⇒ 0 ≤ g x) ∧ (∀x. x ∈ m_space m ⇒ g x ≤ f x) ∧
          (∀x. x ∈ m_space m ⇒ g x ≠ +∞) ∧ ∫⁺ m g ≠ +∞ ⇒
          ∫⁺ m (λx. f x − g x) = ∫⁺ m f − ∫⁺ m g
   
   [pos_fn_integral_sum]  Theorem
      
      ⊢ ∀m f s.
          FINITE s ∧ measure_space m ∧
          (∀i. i ∈ s ⇒ ∀x. x ∈ m_space m ⇒ 0 ≤ f i x) ∧
          (∀i. i ∈ s ⇒ f i ∈ Borel_measurable (measurable_space m)) ⇒
          ∫⁺ m (λx. ∑ (λi. f i x) s) = ∑ (λi. ∫⁺ m (f i)) s
   
   [pos_fn_integral_sum_cmul_indicator]  Theorem
      
      ⊢ ∀m s a x.
          measure_space m ∧ FINITE s ∧ (∀i. i ∈ s ⇒ 0 ≤ x i) ∧
          (∀i. i ∈ s ⇒ a i ∈ measurable_sets m) ⇒
          ∫⁺ m (λt. ∑ (λi. Normal (x i) * 𝟙 (a i) t) s) =
          ∑ (λi. Normal (x i) * measure m (a i)) s
   
   [pos_fn_integral_suminf]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧ (∀i x. x ∈ m_space m ⇒ 0 ≤ f i x) ∧
          (∀i. f i ∈ Borel_measurable (measurable_space m)) ⇒
          ∫⁺ m (λx. suminf (λi. f i x)) = suminf (λi. ∫⁺ m (f i))
   
   [pos_fn_integral_zero]  Theorem
      
      ⊢ ∀m. measure_space m ⇒ ∫⁺ m (λx. 0) = 0
   
   [pos_simple_fn_add]  Theorem
      
      ⊢ ∀m f g s a x s' a' x'.
          measure_space m ∧ pos_simple_fn m f s a x ∧
          pos_simple_fn m g s' a' x' ⇒
          ∃s'' a'' x''. pos_simple_fn m (λt. f t + g t) s'' a'' x''
   
   [pos_simple_fn_add_alt]  Theorem
      
      ⊢ ∀m f g s a x y.
          measure_space m ∧ pos_simple_fn m f s a x ∧
          pos_simple_fn m g s a y ⇒
          pos_simple_fn m (λt. f t + g t) s a (λi. x i + y i)
   
   [pos_simple_fn_cmul]  Theorem
      
      ⊢ ∀m f z s a x.
          measure_space m ∧ pos_simple_fn m f s a x ∧ 0 ≤ z ⇒
          ∃s' a' x'. pos_simple_fn m (λt. Normal z * f t) s' a' x'
   
   [pos_simple_fn_cmul_alt]  Theorem
      
      ⊢ ∀m f s a x z.
          measure_space m ∧ 0 ≤ z ∧ pos_simple_fn m f s a x ⇒
          pos_simple_fn m (λt. Normal z * f t) s a (λi. z * x i)
   
   [pos_simple_fn_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_indicator_alt]  Theorem
      
      ⊢ ∀m s.
          measure_space m ∧ s ∈ measurable_sets m ⇒
          pos_simple_fn m (𝟙 s) {0; 1}
            (λi. if i = 0 then m_space m DIFF s else s)
            (λi. if i = 0 then 0 else 1)
   
   [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_add_alt]  Theorem
      
      ⊢ ∀m f s a x g y.
          measure_space m ∧ pos_simple_fn m f s a x ∧
          pos_simple_fn m g s a y ⇒
          pos_simple_fn_integral m s a x + pos_simple_fn_integral m s a y =
          pos_simple_fn_integral m s a (λi. x i + y i)
   
   [pos_simple_fn_integral_cmul]  Theorem
      
      ⊢ ∀m f s a x z.
          measure_space m ∧ pos_simple_fn m f s a x ∧ 0 ≤ z ⇒
          pos_simple_fn m (λx. Normal z * f x) s a (λi. z * x i) ∧
          pos_simple_fn_integral m s a (λi. z * x i) =
          Normal z * pos_simple_fn_integral m s a x
   
   [pos_simple_fn_integral_cmul_alt]  Theorem
      
      ⊢ ∀m f s a x z.
          measure_space m ∧ 0 ≤ z ∧ pos_simple_fn m f s a x ⇒
          ∃s' a' x'.
            pos_simple_fn m (λt. Normal z * f t) s' a' x' ∧
            pos_simple_fn_integral m s' a' x' =
            Normal z * pos_simple_fn_integral m s a x
   
   [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. 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_not_infty]  Theorem
      
      ⊢ ∀m f s a x.
          measure_space m ∧ pos_simple_fn m f s a x ⇒
          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 = ∑ (λi. Normal (z i) * 𝟙 (c i) t) k) ∧
            (∀t. t ∈ m_space m ⇒ g t = ∑ (λi. Normal (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. i ∈ k ⇒ 0 ≤ z i) ∧ (∀i. i ∈ k ⇒ 0 ≤ z' i) ∧
            (∀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
   
   [pos_simple_fn_integral_sub]  Theorem
      
      ⊢ ∀m f s a x g s' b y.
          measure_space m ∧ measure m (m_space m) ≠ +∞ ∧
          (∀x. x ∈ m_space m ⇒ g x ≤ f x) ∧
          (∀x. x ∈ m_space m ⇒ g x ≠ +∞) ∧ 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_sum]  Theorem
      
      ⊢ ∀m f s a x P.
          measure_space m ∧ (∀i. i ∈ P ⇒ pos_simple_fn m (f i) s a (x i)) ∧
          (∀i t. i ∈ P ⇒ f i t ≠ −∞) ∧ FINITE P ∧ P ≠ ∅ ⇒
          pos_simple_fn m (λt. ∑ (λi. f i t) P) s a (λi. ∑ (λj. x j i) P) ∧
          pos_simple_fn_integral m s a (λj. ∑ (λi. x i j) P) =
          ∑ (λi. pos_simple_fn_integral m s a (x i)) P
   
   [pos_simple_fn_integral_sum_alt]  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)) ∧
          (∀i t. i ∈ P ⇒ f i t ≠ −∞) ∧ FINITE P ∧ P ≠ ∅ ⇒
          ∃c k z.
            pos_simple_fn m (λt. ∑ (λi. f i t) P) k c z ∧
            pos_simple_fn_integral m k c z =
            ∑ (λi. pos_simple_fn_integral m (s i) (a i) (x i)) P
   
   [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
   
   [pos_simple_fn_integral_zero]  Theorem
      
      ⊢ ∀m s a x.
          measure_space m ∧ pos_simple_fn m (λt. 0) s a x ⇒
          pos_simple_fn_integral m s a x = 0
   
   [pos_simple_fn_integral_zero_alt]  Theorem
      
      ⊢ ∀m g s a x.
          measure_space m ∧ pos_simple_fn m g s a x ∧
          (∀x. x ∈ m_space m ⇒ g x = 0) ⇒
          pos_simple_fn_integral m s a x = 0
   
   [pos_simple_fn_le]  Theorem
      
      ⊢ ∀m f g s a x x' i.
          measure_space m ∧ pos_simple_fn m f s a x ∧
          pos_simple_fn m g s a x' ∧ (∀x. x ∈ m_space m ⇒ g x ≤ f x) ∧
          i ∈ s ∧ a i ≠ ∅ ⇒
          Normal (x' i) ≤ Normal (x i)
   
   [pos_simple_fn_max]  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'' a'' x''. pos_simple_fn m (λx. max (f x) (g x)) s'' a'' x''
   
   [pos_simple_fn_not_infty]  Theorem
      
      ⊢ ∀m f s a x.
          pos_simple_fn m f s a x ⇒ ∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ f x ≠ +∞
   
   [pos_simple_fn_thm1]  Theorem
      
      ⊢ ∀m f s a x i y.
          measure_space m ∧ pos_simple_fn m f s a x ∧ i ∈ s ∧ y ∈ a i ⇒
          f y = Normal (x i)
   
   [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_cmul]  Theorem
      
      ⊢ ∀m f a z.
          measure_space m ∧ a ∈ psfis m f ∧ 0 ≤ z ⇒
          Normal z * a ∈ psfis m (λx. Normal z * f x)
   
   [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. i ∈ P ⇒ 0 ≤ x i) ∧ FINITE P ⇒
          ∑ (λi. Normal (x i) * measure m (a i)) P ∈
          psfis m (λt. ∑ (λi. Normal (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_not_infty]  Theorem
      
      ⊢ ∀m f a. measure_space m ∧ a ∈ psfis m f ⇒ a ≠ −∞
   
   [psfis_pos]  Theorem
      
      ⊢ ∀m f a.
          measure_space m ∧ a ∈ psfis m f ⇒ ∀x. x ∈ m_space m ⇒ 0 ≤ f x
   
   [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 = ∑ (λi. Normal (z i) * 𝟙 (c i) t) k) ∧
            (∀t. t ∈ m_space m ⇒ g t = ∑ (λi. Normal (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. i ∈ k ⇒ 0 ≤ z i) ∧ (∀i. i ∈ k ⇒ 0 ≤ z' i) ∧
            (∀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
   
   [psfis_sub]  Theorem
      
      ⊢ ∀m f g a b.
          measure_space m ∧ measure m (m_space m) ≠ +∞ ∧
          (∀x. x ∈ m_space m ⇒ g x ≤ f x) ∧
          (∀x. x ∈ m_space m ⇒ g x ≠ +∞) ∧ a ∈ psfis m f ∧ b ∈ psfis m g ⇒
          a − b ∈ psfis m (λx. f x − g x)
   
   [psfis_sum]  Theorem
      
      ⊢ ∀m f a P.
          measure_space m ∧ (∀i. i ∈ P ⇒ a i ∈ psfis m (f i)) ∧
          (∀i t. i ∈ P ⇒ f i t ≠ −∞) ∧ FINITE P ⇒
          ∑ a P ∈ psfis m (λt. ∑ (λi. f i t) P)
   
   [psfis_unique]  Theorem
      
      ⊢ ∀m f a b. measure_space m ∧ a ∈ psfis m f ∧ b ∈ psfis m f ⇒ a = b
   
   [psfis_zero]  Theorem
      
      ⊢ ∀m a. measure_space m ⇒ (a ∈ psfis m (λx. 0) ⇔ a = 0)
   
   [seq_sup_compute]  Theorem
      
      ⊢ (∀P. seq_sup P 0 = @r. r ∈ P ∧ sup P < r + 1) ∧
        (∀P n.
           seq_sup P (NUMERAL (BIT1 n)) =
           @r. r ∈ P ∧ sup P < r + Normal ((1 / 2) pow NUMERAL (BIT1 n)) ∧
               seq_sup P (NUMERAL (BIT1 n) − 1) < r ∧ r < sup P) ∧
        ∀P n.
          seq_sup P (NUMERAL (BIT2 n)) =
          @r. r ∈ P ∧ sup P < r + Normal ((1 / 2) pow NUMERAL (BIT2 n)) ∧
              seq_sup P (NUMERAL (BIT1 n)) < r ∧ r < sup P
   
   
*)
end


Source File Identifier index Theory binding index

HOL 4, Trindemossen-1