Structure martingaleTheory

signature martingaleTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val exhausting_sequence_def : thm
    val fcp_sigma_def : thm
    val filtered_measure_space_def : thm
    val filtration_def : thm
    val general_filtered_measure_space_def : thm
    val general_filtration_def : thm
    val general_martingale_def : thm
    val general_sigma_def : thm
    val has_exhausting_sequence : thm
    val infty_sigma_algebra_def : thm
    val lborel_2d_def : thm
    val martingale_def : thm
    val prod_measure_def : thm
    val sigma_finite_filtered_measure_space_def : thm
    val sigma_finite_general_filtered_measure_space_def : thm
    val sub_martingale_def : thm
    val sub_sigma_algebra_def : thm
    val super_martingale_def : thm
    val upwards_filtering_def : thm
  
  (*  Theorems  *)
    val EXISTENCE_OF_PROD_MEASURE : thm
    val EXISTENCE_OF_PROD_MEASURE' : thm
    val FILTRATION : thm
    val FILTRATION_BOUNDED : thm
    val FILTRATION_MONO : thm
    val FILTRATION_SUBSETS : thm
    val FUBINI : thm
    val FUBINI' : thm
    val Fubini : thm
    val Fubini' : thm
    val INFTY_SIGMA_ALGEBRA_BOUNDED : thm
    val INFTY_SIGMA_ALGEBRA_MAXIMAL : thm
    val IN_MEASURABLE_BOREL_FROM_PROD_SIGMA : thm
    val MARTINGALE_BOTH_SUB_SUPER : thm
    val POSET_NUM_LE : thm
    val PROD_SIGMA_OF_GENERATOR : thm
    val SIGMA_FINITE_FILTERED_MEASURE_SPACE_I : thm
    val SUB_SIGMA_ALGEBRA_ANTISYM : thm
    val SUB_SIGMA_ALGEBRA_MEASURE_SPACE : thm
    val SUB_SIGMA_ALGEBRA_ORDER : thm
    val SUB_SIGMA_ALGEBRA_REFL : thm
    val SUB_SIGMA_ALGEBRA_TRANS : thm
    val TONELLI : thm
    val UNIQUENESS_OF_PROD_MEASURE : thm
    val UNIQUENESS_OF_PROD_MEASURE' : thm
    val exhausting_sequence_CROSS : thm
    val exhausting_sequence_alt : thm
    val exhausting_sequence_cross : thm
    val exhausting_sequence_general_cross : thm
    val existence_of_prod_measure : thm
    val existence_of_prod_measure_general : thm
    val fcp_sigma_alt : thm
    val filtered_measure_space_alt : thm
    val filtration_alt : thm
    val general_filtered_measure_space_alt : thm
    val general_sigma_of_generator : thm
    val has_exhausting_sequence_alt : thm
    val has_exhausting_sequence_def : thm
    val integrable_cong_measure : thm
    val integrable_cong_measure' : thm
    val integral_cong_measure : thm
    val integral_cong_measure' : thm
    val integral_distr : thm
    val lborel_2d_prod_measure : thm
    val measure_space_prod_measure : thm
    val pos_fn_integral_cong_measure : thm
    val pos_fn_integral_cong_measure' : thm
    val pos_fn_integral_distr : thm
    val prod_sigma_alt : thm
    val prod_sigma_of_generator : thm
    val sigma_algebra_general_sigma : thm
    val sigma_algebra_prod_sigma : thm
    val sigma_algebra_prod_sigma' : thm
    val sigma_finite_alt : thm
    val sigma_finite_alt_exhausting_sequence : thm
    val sigma_finite_filtered_measure_space_alt : thm
    val sigma_finite_has_exhausting_sequence : thm
    val uniqueness_of_prod_measure : thm
    val uniqueness_of_prod_measure' : thm
    val uniqueness_of_prod_measure_general : thm
    val uniqueness_of_prod_measure_general' : thm
  
  val martingale_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [lebesgue] Parent theory of "martingale"
   
   [poset] Parent theory of "martingale"
   
   [exhausting_sequence_def]  Definition
      
      ⊢ ∀a f.
          exhausting_sequence a f ⇔
          f ∈ (𝕌(:num) → subsets a) ∧ (∀n. f n ⊆ f (SUC n)) ∧
          BIGUNION (IMAGE f 𝕌(:num)) = space a
   
   [fcp_sigma_def]  Definition
      
      ⊢ ∀a b.
          fcp_sigma a b =
          sigma (fcp_cross (space a) (space b))
            (fcp_prod (subsets a) (subsets b))
   
   [filtered_measure_space_def]  Definition
      
      ⊢ ∀sp sts m a.
          filtered_measure_space (sp,sts,m) a ⇔
          measure_space (sp,sts,m) ∧ filtration (sp,sts) a
   
   [filtration_def]  Definition
      
      ⊢ ∀A a.
          filtration A a ⇔
          (∀n. sub_sigma_algebra (a n) A) ∧
          ∀i j. i ≤ j ⇒ subsets (a i) ⊆ subsets (a j)
   
   [general_filtered_measure_space_def]  Definition
      
      ⊢ ∀J R sp sts m a.
          filtered_measure_space (J,R) (sp,sts,m) a ⇔
          measure_space (sp,sts,m) ∧ filtration (J,R) (sp,sts) a
   
   [general_filtration_def]  Definition
      
      ⊢ ∀J R A a.
          filtration (J,R) A a ⇔
          poset (J,R) ∧ (∀n. n ∈ J ⇒ sub_sigma_algebra (a n) A) ∧
          ∀i j. i ∈ J ∧ j ∈ J ∧ R i j ⇒ subsets (a i) ⊆ subsets (a j)
   
   [general_martingale_def]  Definition
      
      ⊢ ∀J R m a u.
          martingale (J,R) m a u ⇔
          sigma_finite_filtered_measure_space (J,R) m a ∧
          (∀n. n ∈ J ⇒ integrable m (u n)) ∧
          ∀i j s.
            i ∈ J ∧ j ∈ J ∧ R i j ∧ s ∈ subsets (a i) ⇒
            ∫ m (λx. u i x * 𝟙 s x) = ∫ m (λx. u j x * 𝟙 s x)
   
   [general_sigma_def]  Definition
      
      ⊢ ∀cons A B.
          general_sigma cons A B =
          sigma (general_cross cons (space A) (space B))
            (general_prod cons (subsets A) (subsets B))
   
   [has_exhausting_sequence]  Definition
      
      ⊢ ∀a. has_exhausting_sequence a ⇔ ∃f. exhausting_sequence a f
   
   [infty_sigma_algebra_def]  Definition
      
      ⊢ ∀sp a.
          infty_sigma_algebra sp a =
          sigma sp (BIGUNION (IMAGE (λi. subsets (a i)) 𝕌(:num)))
   
   [lborel_2d_def]  Definition
      
      ⊢ sigma_finite_measure_space lborel_2d ∧
        m_space lborel_2d = 𝕌(:real) × 𝕌(:real) ∧
        measurable_sets lborel_2d =
        subsets ((𝕌(:real),subsets borel) × (𝕌(:real),subsets borel)) ∧
        (∀s t.
           s ∈ subsets borel ∧ t ∈ subsets borel ⇒
           measure lborel_2d (s × t) = lambda s * lambda t) ∧
        ∀s. s ∈ measurable_sets lborel_2d ⇒
            (∀x. (λy. 𝟙 s (x,y)) ∈ Borel_measurable borel) ∧
            (∀y. (λx. 𝟙 s (x,y)) ∈ Borel_measurable borel) ∧
            (λy. ∫⁺ lborel (λx. 𝟙 s (x,y))) ∈ Borel_measurable borel ∧
            (λx. ∫⁺ lborel (λy. 𝟙 s (x,y))) ∈ Borel_measurable borel ∧
            measure lborel_2d s = ∫⁺ lborel (λy. ∫⁺ lborel (λx. 𝟙 s (x,y))) ∧
            measure lborel_2d s = ∫⁺ lborel (λx. ∫⁺ lborel (λy. 𝟙 s (x,y)))
   
   [martingale_def]  Definition
      
      ⊢ ∀m a u.
          martingale m a u ⇔
          sigma_finite_filtered_measure_space m a ∧
          (∀n. integrable m (u n)) ∧
          ∀n s.
            s ∈ subsets (a n) ⇒
            ∫ m (λx. u (SUC n) x * 𝟙 s x) = ∫ m (λx. u n x * 𝟙 s x)
   
   [prod_measure_def]  Definition
      
      ⊢ ∀m1 m2.
          m1 × m2 =
          (m_space m1 × m_space m2,
           subsets
             ((m_space m1,measurable_sets m1) ×
              (m_space m2,measurable_sets m2)),
           (λs. ∫⁺ m2 (λy. ∫⁺ m1 (λx. 𝟙 s (x,y)))))
   
   [sigma_finite_filtered_measure_space_def]  Definition
      
      ⊢ ∀sp sts m a.
          sigma_finite_filtered_measure_space (sp,sts,m) a ⇔
          filtered_measure_space (sp,sts,m) a ∧
          sigma_finite (sp,subsets (a 0),m)
   
   [sigma_finite_general_filtered_measure_space_def]  Definition
      
      ⊢ ∀J R sp sts m a.
          sigma_finite_filtered_measure_space (J,R) (sp,sts,m) a ⇔
          filtered_measure_space (J,R) (sp,sts,m) a ∧
          ∀n. n ∈ J ⇒ sigma_finite (sp,subsets (a n),m)
   
   [sub_martingale_def]  Definition
      
      ⊢ ∀m a u.
          sub_martingale m a u ⇔
          sigma_finite_filtered_measure_space m a ∧
          (∀n. integrable m (u n)) ∧
          ∀n s.
            s ∈ subsets (a n) ⇒
            ∫ m (λx. u n x * 𝟙 s x) ≤ ∫ m (λx. u (SUC n) x * 𝟙 s x)
   
   [sub_sigma_algebra_def]  Definition
      
      ⊢ ∀a b.
          sub_sigma_algebra a b ⇔
          sigma_algebra a ∧ sigma_algebra b ∧ space a = space b ∧
          subsets a ⊆ subsets b
   
   [super_martingale_def]  Definition
      
      ⊢ ∀m a u.
          super_martingale m a u ⇔
          sigma_finite_filtered_measure_space m a ∧
          (∀n. integrable m (u n)) ∧
          ∀n s.
            s ∈ subsets (a n) ⇒
            ∫ m (λx. u (SUC n) x * 𝟙 s x) ≤ ∫ m (λx. u n x * 𝟙 s x)
   
   [upwards_filtering_def]  Definition
      
      ⊢ ∀J R.
          upwards_filtering (J,R) ⇔
          ∀a b. a ∈ J ∧ b ∈ J ⇒ ∃c. c ∈ J ∧ R a c ∧ R b c
   
   [EXISTENCE_OF_PROD_MEASURE]  Theorem
      
      ⊢ ∀X Y A B u v m0.
          sigma_finite_measure_space (X,A,u) ∧
          sigma_finite_measure_space (Y,B,v) ∧
          (∀s t. s ∈ A ∧ t ∈ B ⇒ m0 (s × t) = u s * v t) ⇒
          (∀s. s ∈ subsets ((X,A) × (Y,B)) ⇒
               (∀x. x ∈ X ⇒ (λy. 𝟙 s (x,y)) ∈ Borel_measurable (Y,B)) ∧
               (∀y. y ∈ Y ⇒ (λx. 𝟙 s (x,y)) ∈ Borel_measurable (X,A)) ∧
               (λy. ∫⁺ (X,A,u) (λx. 𝟙 s (x,y))) ∈ Borel_measurable (Y,B) ∧
               (λx. ∫⁺ (Y,B,v) (λy. 𝟙 s (x,y))) ∈ Borel_measurable (X,A)) ∧
          ∃m. sigma_finite_measure_space (X × Y,subsets ((X,A) × (Y,B)),m) ∧
              (∀s. s ∈ prod_sets A B ⇒ m s = m0 s) ∧
              ∀s. s ∈ subsets ((X,A) × (Y,B)) ⇒
                  m s = ∫⁺ (Y,B,v) (λy. ∫⁺ (X,A,u) (λx. 𝟙 s (x,y))) ∧
                  m s = ∫⁺ (X,A,u) (λx. ∫⁺ (Y,B,v) (λy. 𝟙 s (x,y)))
   
   [EXISTENCE_OF_PROD_MEASURE']  Theorem
      
      ⊢ ∀X Y A B u v m0.
          sigma_finite_measure_space (X,A,u) ∧
          sigma_finite_measure_space (Y,B,v) ∧
          (∀s t. s ∈ A ∧ t ∈ B ⇒ m0 (s × t) = u s * v t) ⇒
          (∀s. s ∈ subsets ((X,A) × (Y,B)) ⇒
               (∀x. x ∈ X ⇒ (λy. 𝟙 s (x,y)) ∈ Borel_measurable (Y,B)) ∧
               (∀y. y ∈ Y ⇒ (λx. 𝟙 s (x,y)) ∈ Borel_measurable (X,A)) ∧
               (λy. ∫ (X,A,u) (λx. 𝟙 s (x,y))) ∈ Borel_measurable (Y,B) ∧
               (λx. ∫ (Y,B,v) (λy. 𝟙 s (x,y))) ∈ Borel_measurable (X,A)) ∧
          ∃m. sigma_finite_measure_space (X × Y,subsets ((X,A) × (Y,B)),m) ∧
              (∀s. s ∈ prod_sets A B ⇒ m s = m0 s) ∧
              ∀s. s ∈ subsets ((X,A) × (Y,B)) ⇒
                  m s = ∫ (Y,B,v) (λy. ∫ (X,A,u) (λx. 𝟙 s (x,y))) ∧
                  m s = ∫ (X,A,u) (λx. ∫ (Y,B,v) (λy. 𝟙 s (x,y)))
   
   [FILTRATION]  Theorem
      
      ⊢ ∀A a.
          filtration A a ⇔
          (∀n. sub_sigma_algebra (a n) A) ∧
          (∀n. subsets (a n) ⊆ subsets A) ∧
          ∀i j. i ≤ j ⇒ subsets (a i) ⊆ subsets (a j)
   
   [FILTRATION_BOUNDED]  Theorem
      
      ⊢ ∀A a. filtration A a ⇒ ∀n. sub_sigma_algebra (a n) A
   
   [FILTRATION_MONO]  Theorem
      
      ⊢ ∀A a. filtration A a ⇒ ∀i j. i ≤ j ⇒ subsets (a i) ⊆ subsets (a j)
   
   [FILTRATION_SUBSETS]  Theorem
      
      ⊢ ∀A a. filtration A a ⇒ ∀n. subsets (a n) ⊆ subsets A
   
   [FUBINI]  Theorem
      
      ⊢ ∀X Y A B u v f.
          sigma_finite_measure_space (X,A,u) ∧
          sigma_finite_measure_space (Y,B,v) ∧
          f ∈ Borel_measurable ((X,A) × (Y,B)) ∧
          (∫⁺ ((X,A,u) × (Y,B,v)) (abs ∘ f) ≠ +∞ ∨
           ∫⁺ (Y,B,v) (λy. ∫⁺ (X,A,u) (λx. (abs ∘ f) (x,y))) ≠ +∞ ∨
           ∫⁺ (X,A,u) (λx. ∫⁺ (Y,B,v) (λy. (abs ∘ f) (x,y))) ≠ +∞) ⇒
          ∫⁺ ((X,A,u) × (Y,B,v)) (abs ∘ f) ≠ +∞ ∧
          ∫⁺ (Y,B,v) (λy. ∫⁺ (X,A,u) (λx. (abs ∘ f) (x,y))) ≠ +∞ ∧
          ∫⁺ (X,A,u) (λx. ∫⁺ (Y,B,v) (λy. (abs ∘ f) (x,y))) ≠ +∞ ∧
          integrable ((X,A,u) × (Y,B,v)) f ∧
          (AE y::(Y,B,v). integrable (X,A,u) (λx. f (x,y))) ∧
          (AE x::(X,A,u). integrable (Y,B,v) (λy. f (x,y))) ∧
          integrable (X,A,u) (λx. ∫ (Y,B,v) (λy. f (x,y))) ∧
          integrable (Y,B,v) (λy. ∫ (X,A,u) (λx. f (x,y))) ∧
          ∫ ((X,A,u) × (Y,B,v)) f = ∫ (Y,B,v) (λy. ∫ (X,A,u) (λx. f (x,y))) ∧
          ∫ ((X,A,u) × (Y,B,v)) f = ∫ (X,A,u) (λx. ∫ (Y,B,v) (λy. f (x,y)))
   
   [FUBINI']  Theorem
      
      ⊢ ∀X Y A B u v f.
          sigma_finite_measure_space (X,A,u) ∧
          sigma_finite_measure_space (Y,B,v) ∧
          f ∈ Borel_measurable ((X,A) × (Y,B)) ∧
          (∫ ((X,A,u) × (Y,B,v)) (abs ∘ f) ≠ +∞ ∨
           ∫ (Y,B,v) (λy. ∫ (X,A,u) (λx. (abs ∘ f) (x,y))) ≠ +∞ ∨
           ∫ (X,A,u) (λx. ∫ (Y,B,v) (λy. (abs ∘ f) (x,y))) ≠ +∞) ⇒
          ∫ ((X,A,u) × (Y,B,v)) (abs ∘ f) ≠ +∞ ∧
          ∫ (Y,B,v) (λy. ∫ (X,A,u) (λx. (abs ∘ f) (x,y))) ≠ +∞ ∧
          ∫ (X,A,u) (λx. ∫ (Y,B,v) (λy. (abs ∘ f) (x,y))) ≠ +∞ ∧
          integrable ((X,A,u) × (Y,B,v)) f ∧
          (AE y::(Y,B,v). integrable (X,A,u) (λx. f (x,y))) ∧
          (AE x::(X,A,u). integrable (Y,B,v) (λy. f (x,y))) ∧
          integrable (X,A,u) (λx. ∫ (Y,B,v) (λy. f (x,y))) ∧
          integrable (Y,B,v) (λy. ∫ (X,A,u) (λx. f (x,y))) ∧
          ∫ ((X,A,u) × (Y,B,v)) f = ∫ (Y,B,v) (λy. ∫ (X,A,u) (λx. f (x,y))) ∧
          ∫ ((X,A,u) × (Y,B,v)) f = ∫ (X,A,u) (λx. ∫ (Y,B,v) (λy. f (x,y)))
   
   [Fubini]  Theorem
      
      ⊢ ∀m1 m2 f.
          sigma_finite_measure_space m1 ∧ sigma_finite_measure_space m2 ∧
          f ∈
          Borel_measurable
            ((m_space m1,measurable_sets m1) ×
             (m_space m2,measurable_sets m2)) ∧
          (∫⁺ (m1 × m2) (abs ∘ f) ≠ +∞ ∨
           ∫⁺ m2 (λy. ∫⁺ m1 (λx. (abs ∘ f) (x,y))) ≠ +∞ ∨
           ∫⁺ m1 (λx. ∫⁺ m2 (λy. (abs ∘ f) (x,y))) ≠ +∞) ⇒
          ∫⁺ (m1 × m2) (abs ∘ f) ≠ +∞ ∧
          ∫⁺ m2 (λy. ∫⁺ m1 (λx. (abs ∘ f) (x,y))) ≠ +∞ ∧
          ∫⁺ m1 (λx. ∫⁺ m2 (λy. (abs ∘ f) (x,y))) ≠ +∞ ∧
          integrable (m1 × m2) f ∧
          (AE y::m2. integrable m1 (λx. f (x,y))) ∧
          (AE x::m1. integrable m2 (λy. f (x,y))) ∧
          integrable m1 (λx. ∫ m2 (λy. f (x,y))) ∧
          integrable m2 (λy. ∫ m1 (λx. f (x,y))) ∧
          ∫ (m1 × m2) f = ∫ m2 (λy. ∫ m1 (λx. f (x,y))) ∧
          ∫ (m1 × m2) f = ∫ m1 (λx. ∫ m2 (λy. f (x,y)))
   
   [Fubini']  Theorem
      
      ⊢ ∀m1 m2 f.
          sigma_finite_measure_space m1 ∧ sigma_finite_measure_space m2 ∧
          f ∈
          Borel_measurable
            ((m_space m1,measurable_sets m1) ×
             (m_space m2,measurable_sets m2)) ∧
          (∫ (m1 × m2) (abs ∘ f) ≠ +∞ ∨
           ∫ m2 (λy. ∫ m1 (λx. (abs ∘ f) (x,y))) ≠ +∞ ∨
           ∫ m1 (λx. ∫ m2 (λy. (abs ∘ f) (x,y))) ≠ +∞) ⇒
          ∫ (m1 × m2) (abs ∘ f) ≠ +∞ ∧
          ∫ m2 (λy. ∫ m1 (λx. (abs ∘ f) (x,y))) ≠ +∞ ∧
          ∫ m1 (λx. ∫ m2 (λy. (abs ∘ f) (x,y))) ≠ +∞ ∧
          integrable (m1 × m2) f ∧
          (AE y::m2. integrable m1 (λx. f (x,y))) ∧
          (AE x::m1. integrable m2 (λy. f (x,y))) ∧
          integrable m1 (λx. ∫ m2 (λy. f (x,y))) ∧
          integrable m2 (λy. ∫ m1 (λx. f (x,y))) ∧
          ∫ (m1 × m2) f = ∫ m2 (λy. ∫ m1 (λx. f (x,y))) ∧
          ∫ (m1 × m2) f = ∫ m1 (λx. ∫ m2 (λy. f (x,y)))
   
   [INFTY_SIGMA_ALGEBRA_BOUNDED]  Theorem
      
      ⊢ ∀A a.
          filtration A a ⇒
          sub_sigma_algebra (infty_sigma_algebra (space A) a) A
   
   [INFTY_SIGMA_ALGEBRA_MAXIMAL]  Theorem
      
      ⊢ ∀A a.
          filtration A a ⇒
          ∀n. sub_sigma_algebra (a n) (infty_sigma_algebra (space A) a)
   
   [IN_MEASURABLE_BOREL_FROM_PROD_SIGMA]  Theorem
      
      ⊢ ∀X Y A B f.
          sigma_algebra (X,A) ∧ sigma_algebra (Y,B) ∧
          f ∈ Borel_measurable ((X,A) × (Y,B)) ⇒
          (∀y. y ∈ Y ⇒ (λx. f (x,y)) ∈ Borel_measurable (X,A)) ∧
          ∀x. x ∈ X ⇒ (λy. f (x,y)) ∈ Borel_measurable (Y,B)
   
   [MARTINGALE_BOTH_SUB_SUPER]  Theorem
      
      ⊢ ∀m a u.
          martingale m a u ⇔ sub_martingale m a u ∧ super_martingale m a u
   
   [POSET_NUM_LE]  Theorem
      
      ⊢ poset (𝕌(:num),$<=)
   
   [PROD_SIGMA_OF_GENERATOR]  Theorem
      
      ⊢ ∀X Y E G.
          subset_class X E ∧ subset_class Y G ∧
          has_exhausting_sequence (X,E) ∧ has_exhausting_sequence (Y,G) ⇒
          (X,E) × (Y,G) = sigma X E × sigma Y G
   
   [SIGMA_FINITE_FILTERED_MEASURE_SPACE_I]  Theorem
      
      ⊢ ∀sp sts a m.
          sigma_finite_filtered_measure_space (sp,sts,m) a ⇒
          ∀n. sigma_finite (sp,subsets (a n),m)
   
   [SUB_SIGMA_ALGEBRA_ANTISYM]  Theorem
      
      ⊢ ∀a b. sub_sigma_algebra a b ∧ sub_sigma_algebra b a ⇒ a = b
   
   [SUB_SIGMA_ALGEBRA_MEASURE_SPACE]  Theorem
      
      ⊢ ∀m a.
          measure_space m ∧
          sub_sigma_algebra a (m_space m,measurable_sets m) ⇒
          measure_space (m_space m,subsets a,measure m)
   
   [SUB_SIGMA_ALGEBRA_ORDER]  Theorem
      
      ⊢ Order sub_sigma_algebra
   
   [SUB_SIGMA_ALGEBRA_REFL]  Theorem
      
      ⊢ ∀a. sigma_algebra a ⇒ sub_sigma_algebra a a
   
   [SUB_SIGMA_ALGEBRA_TRANS]  Theorem
      
      ⊢ ∀a b c.
          sub_sigma_algebra a b ∧ sub_sigma_algebra b c ⇒
          sub_sigma_algebra a c
   
   [TONELLI]  Theorem
      
      ⊢ ∀X Y A B u v f.
          sigma_finite_measure_space (X,A,u) ∧
          sigma_finite_measure_space (Y,B,v) ∧
          f ∈ Borel_measurable ((X,A) × (Y,B)) ∧ (∀s. s ∈ X × Y ⇒ 0 ≤ f s) ⇒
          (∀y. y ∈ Y ⇒ (λx. f (x,y)) ∈ Borel_measurable (X,A)) ∧
          (∀x. x ∈ X ⇒ (λy. f (x,y)) ∈ Borel_measurable (Y,B)) ∧
          (λx. ∫⁺ (Y,B,v) (λy. f (x,y))) ∈ Borel_measurable (X,A) ∧
          (λy. ∫⁺ (X,A,u) (λx. f (x,y))) ∈ Borel_measurable (Y,B) ∧
          ∫⁺ ((X,A,u) × (Y,B,v)) f =
          ∫⁺ (Y,B,v) (λy. ∫⁺ (X,A,u) (λx. f (x,y))) ∧
          ∫⁺ ((X,A,u) × (Y,B,v)) f =
          ∫⁺ (X,A,u) (λx. ∫⁺ (Y,B,v) (λy. f (x,y)))
   
   [UNIQUENESS_OF_PROD_MEASURE]  Theorem
      
      ⊢ ∀X Y E G A B u v m m'.
          subset_class X E ∧ subset_class Y G ∧ sigma_finite (X,E,u) ∧
          sigma_finite (Y,G,v) ∧ (∀s t. s ∈ E ∧ t ∈ E ⇒ s ∩ t ∈ E) ∧
          (∀s t. s ∈ G ∧ t ∈ G ⇒ s ∩ t ∈ G) ∧ A = sigma X E ∧
          B = sigma Y G ∧ measure_space (X,subsets A,u) ∧
          measure_space (Y,subsets B,v) ∧
          measure_space (X × Y,subsets (A × B),m) ∧
          measure_space (X × Y,subsets (A × B),m') ∧
          (∀s t. s ∈ E ∧ t ∈ G ⇒ m (s × t) = u s * v t) ∧
          (∀s t. s ∈ E ∧ t ∈ G ⇒ m' (s × t) = u s * v t) ⇒
          ∀x. x ∈ subsets (A × B) ⇒ m x = m' x
   
   [UNIQUENESS_OF_PROD_MEASURE']  Theorem
      
      ⊢ ∀X Y A B u v m m'.
          sigma_finite_measure_space (X,A,u) ∧
          sigma_finite_measure_space (Y,B,v) ∧
          measure_space (X × Y,subsets ((X,A) × (Y,B)),m) ∧
          measure_space (X × Y,subsets ((X,A) × (Y,B)),m') ∧
          (∀s t. s ∈ A ∧ t ∈ B ⇒ m (s × t) = u s * v t) ∧
          (∀s t. s ∈ A ∧ t ∈ B ⇒ m' (s × t) = u s * v t) ⇒
          ∀x. x ∈ subsets ((X,A) × (Y,B)) ⇒ m x = m' x
   
   [exhausting_sequence_CROSS]  Theorem
      
      ⊢ ∀X Y A B f g.
          exhausting_sequence (X,A) f ∧ exhausting_sequence (Y,B) g ⇒
          exhausting_sequence (X × Y,prod_sets A B) (λn. f n × g n)
   
   [exhausting_sequence_alt]  Theorem
      
      ⊢ ∀a f.
          exhausting_sequence a f ⇔
          f ∈ (𝕌(:num) → subsets a) ∧ (∀m n. m ≤ n ⇒ f m ⊆ f n) ∧
          BIGUNION (IMAGE f 𝕌(:num)) = space a
   
   [exhausting_sequence_cross]  Theorem
      
      ⊢ ∀X Y A B f g.
          exhausting_sequence (X,A) f ∧ exhausting_sequence (Y,B) g ⇒
          exhausting_sequence (fcp_cross X Y,fcp_prod A B)
            (λn. fcp_cross (f n) (g n))
   
   [exhausting_sequence_general_cross]  Theorem
      
      ⊢ ∀cons X Y A B f g.
          exhausting_sequence (X,A) f ∧ exhausting_sequence (Y,B) g ⇒
          exhausting_sequence
            (general_cross cons X Y,general_prod cons A B)
            (λn. general_cross cons (f n) (g n))
   
   [existence_of_prod_measure]  Theorem
      
      ⊢ ∀X Y A B u v m0.
          FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ∧
          sigma_finite_measure_space (X,A,u) ∧
          sigma_finite_measure_space (Y,B,v) ∧
          (∀s t. s ∈ A ∧ t ∈ B ⇒ m0 (fcp_cross s t) = u s * v t) ⇒
          (∀s. s ∈ subsets (fcp_sigma (X,A) (Y,B)) ⇒
               (∀x. x ∈ X ⇒
                    (λy. 𝟙 s (FCP_CONCAT x y)) ∈ Borel_measurable (Y,B)) ∧
               (∀y. y ∈ Y ⇒
                    (λx. 𝟙 s (FCP_CONCAT x y)) ∈ Borel_measurable (X,A)) ∧
               (λy. ∫⁺ (X,A,u) (λx. 𝟙 s (FCP_CONCAT x y))) ∈
               Borel_measurable (Y,B) ∧
               (λx. ∫⁺ (Y,B,v) (λy. 𝟙 s (FCP_CONCAT x y))) ∈
               Borel_measurable (X,A)) ∧
          ∃m. sigma_finite_measure_space
                (fcp_cross X Y,subsets (fcp_sigma (X,A) (Y,B)),m) ∧
              (∀s. s ∈ fcp_prod A B ⇒ m s = m0 s) ∧
              ∀s. s ∈ subsets (fcp_sigma (X,A) (Y,B)) ⇒
                  m s =
                  ∫⁺ (Y,B,v) (λy. ∫⁺ (X,A,u) (λx. 𝟙 s (FCP_CONCAT x y))) ∧
                  m s =
                  ∫⁺ (X,A,u) (λx. ∫⁺ (Y,B,v) (λy. 𝟙 s (FCP_CONCAT x y)))
   
   [existence_of_prod_measure_general]  Theorem
      
      ⊢ ∀cons car cdr X Y A B u v m0.
          pair_operation cons car cdr ∧
          sigma_finite_measure_space (X,A,u) ∧
          sigma_finite_measure_space (Y,B,v) ∧
          (∀s t. s ∈ A ∧ t ∈ B ⇒ m0 (general_cross cons s t) = u s * v t) ⇒
          (∀s. s ∈ subsets (general_sigma cons (X,A) (Y,B)) ⇒
               (∀x. x ∈ X ⇒ (λy. 𝟙 s (cons x y)) ∈ Borel_measurable (Y,B)) ∧
               (∀y. y ∈ Y ⇒ (λx. 𝟙 s (cons x y)) ∈ Borel_measurable (X,A)) ∧
               (λy. ∫⁺ (X,A,u) (λx. 𝟙 s (cons x y))) ∈
               Borel_measurable (Y,B) ∧
               (λx. ∫⁺ (Y,B,v) (λy. 𝟙 s (cons x y))) ∈
               Borel_measurable (X,A)) ∧
          ∃m. sigma_finite_measure_space
                (general_cross cons X Y,
                 subsets (general_sigma cons (X,A) (Y,B)),m) ∧
              (∀s. s ∈ general_prod cons A B ⇒ m s = m0 s) ∧
              ∀s. s ∈ subsets (general_sigma cons (X,A) (Y,B)) ⇒
                  m s = ∫⁺ (Y,B,v) (λy. ∫⁺ (X,A,u) (λx. 𝟙 s (cons x y))) ∧
                  m s = ∫⁺ (X,A,u) (λx. ∫⁺ (Y,B,v) (λy. 𝟙 s (cons x y)))
   
   [fcp_sigma_alt]  Theorem
      
      ⊢ ∀A B. fcp_sigma A B = general_sigma FCP_CONCAT A B
   
   [filtered_measure_space_alt]  Theorem
      
      ⊢ ∀m a.
          filtered_measure_space m a ⇔
          measure_space m ∧ filtration (m_space m,measurable_sets m) a
   
   [filtration_alt]  Theorem
      
      ⊢ ∀A a. filtration A a ⇔ filtration (𝕌(:num),$<=) A a
   
   [general_filtered_measure_space_alt]  Theorem
      
      ⊢ ∀sp sts m a.
          filtered_measure_space (sp,sts,m) a ⇔
          filtered_measure_space (𝕌(:num),$<=) (sp,sts,m) a
   
   [general_sigma_of_generator]  Theorem
      
      ⊢ ∀cons car cdr X Y E G.
          pair_operation cons car cdr ∧ subset_class X E ∧
          subset_class Y G ∧ has_exhausting_sequence (X,E) ∧
          has_exhausting_sequence (Y,G) ⇒
          general_sigma cons (X,E) (Y,G) =
          general_sigma cons (sigma X E) (sigma Y G)
   
   [has_exhausting_sequence_alt]  Theorem
      
      ⊢ ∀a. has_exhausting_sequence a ⇔
            ∃f. f ∈ (𝕌(:num) → subsets a) ∧ (∀m n. m ≤ n ⇒ f m ⊆ f n) ∧
                BIGUNION (IMAGE f 𝕌(:num)) = space a
   
   [has_exhausting_sequence_def]  Theorem
      
      ⊢ ∀a. has_exhausting_sequence a ⇔
            ∃f. f ∈ (𝕌(:num) → subsets a) ∧ (∀n. f n ⊆ f (SUC n)) ∧
                BIGUNION (IMAGE f 𝕌(:num)) = space a
   
   [integrable_cong_measure]  Theorem
      
      ⊢ ∀sp sts u v f.
          measure_space (sp,sts,u) ∧ measure_space (sp,sts,v) ∧
          (∀s. s ∈ sts ⇒ u s = v s) ⇒
          (integrable (sp,sts,u) f ⇔ integrable (sp,sts,v) f)
   
   [integrable_cong_measure']  Theorem
      
      ⊢ ∀m1 m2 f.
          measure_space m1 ∧ measure_space m2 ∧ m_space m1 = m_space m2 ∧
          measurable_sets m1 = measurable_sets m2 ∧
          (∀s. s ∈ measurable_sets m1 ⇒ measure m1 s = measure m2 s) ⇒
          (integrable m1 f ⇔ integrable m2 f)
   
   [integral_cong_measure]  Theorem
      
      ⊢ ∀sp sts u v f.
          measure_space (sp,sts,u) ∧ measure_space (sp,sts,v) ∧
          (∀s. s ∈ sts ⇒ u s = v s) ⇒
          ∫ (sp,sts,u) f = ∫ (sp,sts,v) f
   
   [integral_cong_measure']  Theorem
      
      ⊢ ∀m1 m2 f.
          measure_space m1 ∧ measure_space m2 ∧ m_space m1 = m_space m2 ∧
          measurable_sets m1 = measurable_sets m2 ∧
          (∀s. s ∈ measurable_sets m1 ⇒ measure m1 s = measure m2 s) ⇒
          ∫ m1 f = ∫ m2 f
   
   [integral_distr]  Theorem
      
      ⊢ ∀M B f u.
          measure_space M ∧ sigma_algebra B ∧
          f ∈ measurable (m_space M,measurable_sets M) B ∧
          u ∈ Borel_measurable B ⇒
          ∫ (space B,subsets B,distr M f) u = ∫ M (u ∘ f) ∧
          (integrable (space B,subsets B,distr M f) u ⇔
           integrable M (u ∘ f))
   
   [lborel_2d_prod_measure]  Theorem
      
      ⊢ ∀s. s ∈ measurable_sets lborel_2d ⇒
            measure lborel_2d s = measure (lborel × lborel) s
   
   [measure_space_prod_measure]  Theorem
      
      ⊢ ∀m1 m2.
          sigma_finite_measure_space m1 ∧ sigma_finite_measure_space m2 ⇒
          measure_space (m1 × m2)
   
   [pos_fn_integral_cong_measure]  Theorem
      
      ⊢ ∀sp sts u v f.
          measure_space (sp,sts,u) ∧ measure_space (sp,sts,v) ∧
          (∀s. s ∈ sts ⇒ u s = v s) ∧ (∀x. x ∈ sp ⇒ 0 ≤ f x) ⇒
          ∫⁺ (sp,sts,u) f = ∫⁺ (sp,sts,v) f
   
   [pos_fn_integral_cong_measure']  Theorem
      
      ⊢ ∀m1 m2 f.
          measure_space m1 ∧ measure_space m2 ∧ m_space m1 = m_space m2 ∧
          measurable_sets m1 = measurable_sets m2 ∧
          (∀s. s ∈ measurable_sets m1 ⇒ measure m1 s = measure m2 s) ∧
          (∀x. x ∈ m_space m1 ⇒ 0 ≤ f x) ⇒
          ∫⁺ m1 f = ∫⁺ m2 f
   
   [pos_fn_integral_distr]  Theorem
      
      ⊢ ∀M B f u.
          measure_space M ∧ sigma_algebra B ∧
          f ∈ measurable (m_space M,measurable_sets M) B ∧
          u ∈ Borel_measurable B ∧ (∀x. x ∈ space B ⇒ 0 ≤ u x) ⇒
          ∫⁺ (space B,subsets B,distr M f) u = ∫⁺ M (u ∘ f)
   
   [prod_sigma_alt]  Theorem
      
      ⊢ ∀A B. A × B = general_sigma $, A B
   
   [prod_sigma_of_generator]  Theorem
      
      ⊢ ∀X Y E G.
          FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ∧ subset_class X E ∧
          subset_class Y G ∧ has_exhausting_sequence (X,E) ∧
          has_exhausting_sequence (Y,G) ⇒
          fcp_sigma (X,E) (Y,G) = fcp_sigma (sigma X E) (sigma Y G)
   
   [sigma_algebra_general_sigma]  Theorem
      
      ⊢ ∀cons A B.
          subset_class (space A) (subsets A) ∧
          subset_class (space B) (subsets B) ⇒
          sigma_algebra (general_sigma cons A B)
   
   [sigma_algebra_prod_sigma]  Theorem
      
      ⊢ ∀a b.
          subset_class (space a) (subsets a) ∧
          subset_class (space b) (subsets b) ⇒
          sigma_algebra (fcp_sigma a b)
   
   [sigma_algebra_prod_sigma']  Theorem
      
      ⊢ ∀X Y A B.
          subset_class X A ∧ subset_class Y B ⇒
          sigma_algebra (fcp_sigma (X,A) (Y,B))
   
   [sigma_finite_alt]  Theorem
      
      ⊢ ∀m. sigma_finite m ⇔
            ∃f. (f ∈ (𝕌(:num) → measurable_sets m) ∧
                 (∀m n. m ≤ n ⇒ f m ⊆ f n) ∧
                 BIGUNION (IMAGE f 𝕌(:num)) = m_space m) ∧
                ∀n. measure m (f n) < +∞
   
   [sigma_finite_alt_exhausting_sequence]  Theorem
      
      ⊢ ∀m. sigma_finite m ⇔
            ∃f. exhausting_sequence (m_space m,measurable_sets m) f ∧
                ∀n. measure m (f n) < +∞
   
   [sigma_finite_filtered_measure_space_alt]  Theorem
      
      ⊢ ∀sp sts m a.
          sigma_finite_filtered_measure_space (sp,sts,m) a ⇔
          sigma_finite_filtered_measure_space (𝕌(:num),$<=) (sp,sts,m) a
   
   [sigma_finite_has_exhausting_sequence]  Theorem
      
      ⊢ ∀sp sts u.
          sigma_finite (sp,sts,u) ⇒ has_exhausting_sequence (sp,sts)
   
   [uniqueness_of_prod_measure]  Theorem
      
      ⊢ ∀X Y E G A B u v m m'.
          FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ∧ subset_class X E ∧
          subset_class Y G ∧ sigma_finite (X,E,u) ∧ sigma_finite (Y,G,v) ∧
          (∀s t. s ∈ E ∧ t ∈ E ⇒ s ∩ t ∈ E) ∧
          (∀s t. s ∈ G ∧ t ∈ G ⇒ s ∩ t ∈ G) ∧ A = sigma X E ∧
          B = sigma Y G ∧ measure_space (X,subsets A,u) ∧
          measure_space (Y,subsets B,v) ∧
          measure_space (fcp_cross X Y,subsets (fcp_sigma A B),m) ∧
          measure_space (fcp_cross X Y,subsets (fcp_sigma A B),m') ∧
          (∀s t. s ∈ E ∧ t ∈ G ⇒ m (fcp_cross s t) = u s * v t) ∧
          (∀s t. s ∈ E ∧ t ∈ G ⇒ m' (fcp_cross s t) = u s * v t) ⇒
          ∀x. x ∈ subsets (fcp_sigma A B) ⇒ m x = m' x
   
   [uniqueness_of_prod_measure']  Theorem
      
      ⊢ ∀X Y A B u v m m'.
          FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ∧
          sigma_finite_measure_space (X,A,u) ∧
          sigma_finite_measure_space (Y,B,v) ∧
          measure_space (fcp_cross X Y,subsets (fcp_sigma (X,A) (Y,B)),m) ∧
          measure_space (fcp_cross X Y,subsets (fcp_sigma (X,A) (Y,B)),m') ∧
          (∀s t. s ∈ A ∧ t ∈ B ⇒ m (fcp_cross s t) = u s * v t) ∧
          (∀s t. s ∈ A ∧ t ∈ B ⇒ m' (fcp_cross s t) = u s * v t) ⇒
          ∀x. x ∈ subsets (fcp_sigma (X,A) (Y,B)) ⇒ m x = m' x
   
   [uniqueness_of_prod_measure_general]  Theorem
      
      ⊢ ∀cons car cdr X Y E G A B u v m m'.
          pair_operation cons car cdr ∧ subset_class X E ∧
          subset_class Y G ∧ sigma_finite (X,E,u) ∧ sigma_finite (Y,G,v) ∧
          (∀s t. s ∈ E ∧ t ∈ E ⇒ s ∩ t ∈ E) ∧
          (∀s t. s ∈ G ∧ t ∈ G ⇒ s ∩ t ∈ G) ∧ A = sigma X E ∧
          B = sigma Y G ∧ measure_space (X,subsets A,u) ∧
          measure_space (Y,subsets B,v) ∧
          measure_space
            (general_cross cons X Y,subsets (general_sigma cons A B),m) ∧
          measure_space
            (general_cross cons X Y,subsets (general_sigma cons A B),m') ∧
          (∀s t. s ∈ E ∧ t ∈ G ⇒ m (general_cross cons s t) = u s * v t) ∧
          (∀s t. s ∈ E ∧ t ∈ G ⇒ m' (general_cross cons s t) = u s * v t) ⇒
          ∀x. x ∈ subsets (general_sigma cons A B) ⇒ m x = m' x
   
   [uniqueness_of_prod_measure_general']  Theorem
      
      ⊢ ∀cons car cdr X Y A B u v m m'.
          pair_operation cons car cdr ∧
          sigma_finite_measure_space (X,A,u) ∧
          sigma_finite_measure_space (Y,B,v) ∧
          measure_space
            (general_cross cons X Y,
             subsets (general_sigma cons (X,A) (Y,B)),m) ∧
          measure_space
            (general_cross cons X Y,
             subsets (general_sigma cons (X,A) (Y,B)),m') ∧
          (∀s t. s ∈ A ∧ t ∈ B ⇒ m (general_cross cons s t) = u s * v t) ∧
          (∀s t. s ∈ A ∧ t ∈ B ⇒ m' (general_cross cons s t) = u s * v t) ⇒
          ∀x. x ∈ subsets (general_sigma cons (X,A) (Y,B)) ⇒ m x = m' x
   
   
*)
end

HOL 4, Kananaskis-14