Theory: martingale

Theorems

CROSS_ALT

⊢ ∀A B. A × B = general_cross $, A B

Cauchy_Schwarz_inequality

⊢ ∀m u v.
    measure_space m ∧ u ∈ L2_space m ∧ v ∈ L2_space m ⇒
    integrable m (λx. u x * v x) ∧
    ∫ m (λx. abs (u x * v x)) ≤ seminorm 2 m u * seminorm 2 m v

Cauchy_Schwarz_inequality'

⊢ ∀m u v.
    measure_space m ∧ u ∈ L2_space m ∧ v ∈ L2_space m ⇒
    ∫⁺ m (λx. abs (u x * v x)) ≤
    sqrt (∫⁺ m (λx. (u x)²) * ∫⁺ m (λx. (v x)²))

EXISTENCE_OF_PROD_MEASURE

⊢ ∀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'

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

FCP_BIGUNION_CROSS

⊢ ∀f s t.
    fcp_cross (BIGUNION (IMAGE f s)) t =
    BIGUNION (IMAGE (λn. fcp_cross (f n) t) s)

FCP_CROSS_BIGUNION

⊢ ∀f s t.
    fcp_cross t (BIGUNION (IMAGE f s)) =
    BIGUNION (IMAGE (λn. fcp_cross t (f n)) s)

FCP_CROSS_DIFF

⊢ ∀X s t.
    FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ⇒
    fcp_cross (X DIFF s) t = fcp_cross X t DIFF fcp_cross s t

FCP_CROSS_DIFF'

⊢ ∀s X t.
    FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ⇒
    fcp_cross s (X DIFF t) = fcp_cross s X DIFF fcp_cross s t

FCP_INTER_CROSS

⊢ ∀a b c d.
    FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ⇒
    fcp_cross a b ∩ fcp_cross c d = fcp_cross (a ∩ c) (b ∩ d)

FCP_SUBSET_CROSS

⊢ ∀a b c d. a ⊆ b ∧ c ⊆ d ⇒ fcp_cross a c ⊆ fcp_cross b d

FILTRATION

⊢ ∀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

⊢ ∀A a. filtration A a ⇒ ∀n. sub_sigma_algebra (a n) A

FILTRATION_MONO

⊢ ∀A a. filtration A a ⇒ ∀i j. i ≤ j ⇒ subsets (a i) ⊆ subsets (a j)

FILTRATION_SUBSETS

⊢ ∀A a. filtration A a ⇒ ∀n. subsets (a n) ⊆ subsets A

FUBINI

⊢ ∀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'

⊢ ∀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

⊢ ∀m1 m2 f.
    sigma_finite_measure_space m1 ∧ sigma_finite_measure_space m2 ∧
    f ∈ Borel_measurable (measurable_space m1 × measurable_space 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'

⊢ ∀m1 m2 f.
    sigma_finite_measure_space m1 ∧ sigma_finite_measure_space m2 ∧
    f ∈ Borel_measurable (measurable_space m1 × measurable_space 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)))

Hoelder_inequality

⊢ ∀m u v p q.
    measure_space m ∧ 0 < p ∧ 0 < q ∧ p⁻¹ + q⁻¹ = 1 ∧ u ∈ lp_space p m ∧
    v ∈ lp_space q m ⇒
    integrable m (λx. u x * v x) ∧
    ∫ m (λx. abs (u x * v x)) ≤ seminorm p m u * seminorm q m v

Hoelder_inequality'

⊢ ∀m u v p q.
    measure_space m ∧ 0 < p ∧ 0 < q ∧ p⁻¹ + q⁻¹ = 1 ∧ u ∈ lp_space p m ∧
    v ∈ lp_space q m ⇒
    ∫⁺ m (λx. abs (u x * v x)) ≤ seminorm p m u * seminorm q m v

INDICATOR_FN_FCP_CROSS

⊢ ∀s t x y.
    FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ⇒
    𝟙 (fcp_cross s t) (FCP_CONCAT x y) = 𝟙 s x * 𝟙 t y

INFTY_SIGMA_ALGEBRA_BOUNDED

⊢ ∀A a.
    filtration A a ⇒ sub_sigma_algebra (infty_sigma_algebra (space A) a) A

INFTY_SIGMA_ALGEBRA_MAXIMAL

⊢ ∀A a.
    filtration A a ⇒
    ∀n. sub_sigma_algebra (a n) (infty_sigma_algebra (space A) a)

IN_FCP_CROSS

⊢ ∀s a b. s ∈ fcp_cross a b ⇔ ∃t u. s = FCP_CONCAT t u ∧ t ∈ a ∧ u ∈ b

IN_FCP_PROD

⊢ ∀s A B. s ∈ fcp_prod A B ⇔ ∃a b. s = fcp_cross a b ∧ a ∈ A ∧ b ∈ B

IN_MEASURABLE_BOREL_FROM_PROD_SIGMA

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

IN_RN_deriv_property

⊢ ∀f sa nu mu.
    f ∈ RN_deriv_property sa nu mu ⇔
    f ∈ Borel_measurable sa ∧ (∀x. x ∈ space sa ⇒ 0 ≤ f x) ∧
    ∀s. s ∈ subsets sa ⇒ (f * (space sa,subsets sa,mu)) s = nu s

IN_general_cross

⊢ ∀cons s A B.
    s ∈ general_cross cons A B ⇔ ∃a b. s = cons a b ∧ a ∈ A ∧ b ∈ B

IN_general_prod

⊢ ∀cons s A B.
    s ∈ general_prod cons A B ⇔
    ∃a b. s = general_cross cons a b ∧ a ∈ A ∧ b ∈ B

L1_space_alt_integrable

⊢ ∀m f. measure_space m ⇒ (f ∈ L1_space m ⇔ integrable m f)

L2_space_alt_integrable_square

⊢ ∀m f.
    measure_space m ⇒
    (f ∈ L2_space m ⇔
     f ∈ Borel_measurable (measurable_space m) ∧ integrable m (λx. (f x)²))

MARTINGALE_EQ_SUB_SUPER

⊢ ∀m a u. martingale m a u ⇔ sub_martingale m a u ∧ super_martingale m a u

MEASURABLE_SPACE_PROD

⊢ ∀M1 M2.
    measure_space M1 ∧ measure_space M2 ⇒
    measurable_space (M1 × M2) = measurable_space M1 × measurable_space M2

Minkowski_inequality

⊢ ∀p m u v.
    measure_space m ∧ 1 ≤ p ∧ u ∈ lp_space p m ∧ v ∈ lp_space p m ⇒
    (λx. u x + v x) ∈ lp_space p m ∧
    seminorm p m (λx. u x + v x) ≤ seminorm p m u + seminorm p m v

Minkowski_inequality'

⊢ ∀p m u v.
    measure_space m ∧ 1 ≤ p ∧ u ∈ lp_space p m ∧ v ∈ lp_space p m ⇒
    seminorm p m (λx. u x + v x) ≤ seminorm p m u + seminorm p m v

PROD_MEASURE_CROSS

⊢ ∀M1 M2 s t.
    measure_space M1 ∧ measure_space M2 ∧ s ∈ measurable_sets M1 ∧
    t ∈ measurable_sets M2 ⇒
    prod_measure M1 M2 (s × t) = measure M1 s * measure M2 t

PROD_SIGMA_OF_GENERATOR

⊢ ∀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

RN_derivI

⊢ ∀f M N.
    measure_space M ∧ measure_space N ∧
    f ∈ Borel_measurable (measurable_space M) ∧
    (∀x. x ∈ m_space M ⇒ 0 ≤ f x) ∧ density_of M f = measure_of N ∧
    measure_space M ∧ measure_space N ∧
    measurable_sets M = measurable_sets N ⇒
    density_of M (RN_deriv' M N) = measure_of N

RN_deriv_1

⊢ ∀m. sigma_finite_measure_space m ⇒ AE x::m. RN_deriv' m m x = 1

RN_deriv_RN_deriv_property

⊢ ∀sa mu nu.
    sigma_finite_measure_space (space sa,subsets sa,mu) ∧
    measure_space (space sa,subsets sa,nu) ∧ nu ≪ (space sa,subsets sa,mu) ⇒
    nu / (space sa,subsets sa,mu) ∈ RN_deriv_property sa nu mu

RN_deriv_integral

⊢ ∀m v f.
    f ∈ Borel_measurable (measurable_space m) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧ sigma_finite_measure_space m ∧
    measure_space (m_space m,measurable_sets m,v) ∧ v ≪ m ⇒
    ∫ (m_space m,measurable_sets m,v) f = ∫ m (λx. (v / m) x * f x)

RN_deriv_inv

⊢ ∀m v.
    sigma_finite_measure_space m ∧
    sigma_finite_measure_space (m_space m,measurable_sets m,v) ∧ v ≪ m ∧
    measure_absolutely_continuous' m (m_space m,measurable_sets m,v) ⇒
    AE x::m. RN_deriv' (m_space m,measurable_sets m,v) m x = ((v / m) x)⁻¹

RN_deriv_mul

⊢ ∀m u v.
    sigma_finite_measure_space m ∧
    sigma_finite_measure_space (m_space m,measurable_sets m,u) ∧
    sigma_finite_measure_space (m_space m,measurable_sets m,v) ∧ u ≪ m ∧
    v ≪ (m_space m,measurable_sets m,u) ⇒
    AE x::m.
      (u / m) x * (v / (m_space m,measurable_sets m,u)) x = (v / m) x

RN_deriv_pos_fn_integral

⊢ ∀m v f.
    f ∈ Borel_measurable (measurable_space m) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧ sigma_finite_measure_space m ∧
    measure_space (m_space m,measurable_sets m,v) ∧ v ≪ m ⇒
    ∫⁺ (m_space m,measurable_sets m,v) f = ∫⁺ m (λx. (v / m) x * f x)

RN_deriv_positive_integral

⊢ ∀M N f.
    sigma_finite_measure_space M ∧ measure_space N ∧
    measure_absolutely_continuous' N M ∧
    measurable_sets M = measurable_sets N ∧
    f ∈ Borel_measurable (measurable_space M) ∧
    (∀x. x ∈ m_space M ⇒ 0 ≤ f x) ⇒
    ∫⁺ N f = ∫⁺ (density_of M (RN_deriv' M N)) f

RN_deriv_property_1

⊢ ∀sa mu.
    measure_space (space sa,subsets sa,mu) ⇒
    (λx. 1) ∈ RN_deriv_property sa mu mu

RN_deriv_property_almost_RN_deriv

⊢ ∀sa mu nu f g.
    sigma_finite_measure_space (space sa,subsets sa,mu) ∧
    sigma_finite_measure_space (space sa,subsets sa,nu) ∧
    nu ≪ (space sa,subsets sa,mu) ∧ f ∈ RN_deriv_property sa nu mu ⇒
    AE x::(space sa,subsets sa,mu). f x = (nu / (space sa,subsets sa,mu)) x

RN_deriv_property_almost_unique

⊢ ∀sa mu nu f g.
    measure_space (space sa,subsets sa,mu) ∧
    sigma_finite_measure_space (space sa,subsets sa,nu) ∧
    f ∈ RN_deriv_property sa nu mu ∧ g ∈ RN_deriv_property sa nu mu ⇒
    AE x::(space sa,subsets sa,mu). f x = g x

RN_deriv_property_mul

⊢ ∀sa lam mu nu dmdl dndm dndl.
    measure_space (space sa,subsets sa,mu) ∧
    measure_space (space sa,subsets sa,nu) ∧
    measure_space (space sa,subsets sa,lam) ∧
    dmdl ∈ RN_deriv_property sa mu lam ∧
    dndm ∈ RN_deriv_property sa nu mu ∧
    (∀x. x ∈ space sa ⇒ dndl x = dmdl x * dndm x) ⇒
    dndl ∈ RN_deriv_property sa nu lam

RN_deriv_property_pos_fn_integral

⊢ ∀sa mu nu dndm f.
    f ∈ Borel_measurable sa ∧ (∀x. x ∈ space sa ⇒ 0 ≤ f x) ∧
    measure_space (space sa,subsets sa,mu) ∧
    measure_space (space sa,subsets sa,nu) ∧
    dndm ∈ RN_deriv_property sa nu mu ⇒
    ∫⁺ (space sa,subsets sa,nu) f =
    ∫⁺ (space sa,subsets sa,mu) (λx. dndm x * f x)

RN_deriv_thm

⊢ ∀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'

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

SIGMA_FINITE_FILTERED_MEASURE_SPACE

⊢ ∀m a.
    sigma_finite_filtered_measure_space m a ⇒
    ∀n. sigma_finite (m_space m,subsets (a n),measure m)

SPACE_PROD

⊢ ∀M1 M2.
    measure_space M1 ∧ measure_space M2 ⇒
    m_space (M1 × M2) = m_space M1 × m_space M2

SUB_SIGMA_ALGEBRA_ANTISYM

⊢ ∀a b. sub_sigma_algebra a b ∧ sub_sigma_algebra b a ⇒ a = b

SUB_SIGMA_ALGEBRA_MEASURE_SPACE

⊢ ∀m a.
    measure_space m ∧ sub_sigma_algebra a (measurable_space m) ⇒
    measure_space (m_space m,subsets a,measure m)

SUB_SIGMA_ALGEBRA_ORDER

⊢ Order sub_sigma_algebra

SUB_SIGMA_ALGEBRA_REFL

⊢ ∀a. sigma_algebra a ⇒ sub_sigma_algebra a a

SUB_SIGMA_ALGEBRA_TRANS

⊢ ∀a b c.
    sub_sigma_algebra a b ∧ sub_sigma_algebra b c ⇒ sub_sigma_algebra a c

TONELLI

⊢ ∀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

⊢ ∀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'

⊢ ∀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

continuity_lemma

⊢ ∀s m u.
    measure_space m ∧ open s ∧ (∀t. t ∈ s ⇒ integrable m (Normal ∘ u t)) ∧
    (∀x. x ∈ m_space m ⇒ (λt. u t x) continuous_on s) ∧
    (∃w. integrable m w ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ w x ∧ w x ≠ +∞) ∧
         ∀t x. t ∈ s ∧ x ∈ m_space m ⇒ Normal (abs (u t x)) ≤ w x) ⇒
    (λt. real (∫ m (Normal ∘ u t))) continuous_on s

continuity_univ_lemma

⊢ ∀m u.
    measure_space m ∧ (∀t. integrable m (Normal ∘ u t)) ∧
    (∀x. x ∈ m_space m ⇒ (λt. u t x) continuous_on 𝕌(:real)) ∧
    (∃w. integrable m w ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ w x ∧ w x ≠ +∞) ∧
         ∀t x. x ∈ m_space m ⇒ Normal (abs (u t x)) ≤ w x) ⇒
    (λt. real (∫ m (Normal ∘ u t))) continuous_on 𝕌(:real)

density_RN_deriv

⊢ ∀M N.
    sigma_finite_measure_space M ∧ measure_space N ∧
    measure_absolutely_continuous' N M ∧
    measurable_sets M = measurable_sets N ⇒
    density_of M (RN_deriv' M N) = measure_of N

density_eq

⊢ ∀m f g.
    measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ g x) ∧
    (∀x. x ∈ m_space m ⇒ f x = g x) ⇒
    density m f = density m g

density_of_pos_fn

⊢ ∀M f.
    measure_space M ∧ (∀x. x ∈ m_space M ⇒ 0 ≤ f x) ⇒
    density_of M f =
    (m_space M,measurable_sets M,
     (λs. if s ∈ measurable_sets M then ∫⁺ M (λx. f x * 𝟙 s x) else 0))

differentiable_lemma

⊢ ∀s m u.
    measure_space m ∧ open s ∧ connected s ∧
    (∀t. t ∈ s ⇒ integrable m (Normal ∘ u t)) ∧
    (∀x. x ∈ m_space m ⇒ (λt. u t x) differentiable_on s) ∧
    (∃w. integrable m w ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ w x ∧ w x ≠ +∞) ∧
         ∀t x.
           t ∈ s ∧ x ∈ m_space m ⇒ Normal (abs (diff1 (λt. u t x) t)) ≤ w x) ⇒
    ∀t. t ∈ s ⇒
        integrable m (λx. Normal (diff1 (λt. u t x) t)) ∧
        ((λt. real (∫ m (Normal ∘ u t))) has_vector_derivative
         real (∫ m (λx. Normal (diff1 (λt. u t x) t)))) (at t within s)

differentiable_lemma'

⊢ ∀s m u.
    measure_space m ∧ open s ∧ connected s ∧
    (∀t. t ∈ s ⇒ integrable m (Normal ∘ u t)) ∧
    (∀x. x ∈ m_space m ⇒ (λt. u t x) differentiable_on s) ∧
    (∃w. integrable m w ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ w x ∧ w x ≠ +∞) ∧
         ∀t x.
           t ∈ s ∧ x ∈ m_space m ⇒ Normal (abs (diff1 (λt. u t x) t)) ≤ w x) ⇒
    (λt. real (∫ m (Normal ∘ u t))) differentiable_on s ∧
    ∀t. t ∈ s ⇒
        integrable m (λx. Normal (diff1 (λt. u t x) t)) ∧
        diff1 (λt. real (∫ m (Normal ∘ u t))) t =
        real (∫ m (λx. Normal (diff1 (λt. u t x) t)))

differentiable_univ_lemma

⊢ ∀m u.
    measure_space m ∧ (∀t. integrable m (Normal ∘ u t)) ∧
    (∀x. x ∈ m_space m ⇒ (λt. u t x) differentiable_on 𝕌(:real)) ∧
    (∃w. integrable m w ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ w x ∧ w x ≠ +∞) ∧
         ∀t x. x ∈ m_space m ⇒ Normal (abs (diff1 (λt. u t x) t)) ≤ w x) ⇒
    ∀t. integrable m (λx. Normal (diff1 (λt. u t x) t)) ∧
        ((λt. real (∫ m (Normal ∘ u t))) has_vector_derivative
         real (∫ m (λx. Normal (diff1 (λt. u t x) t)))) (at t)

differentiable_univ_lemma'

⊢ ∀m u.
    measure_space m ∧ (∀t. integrable m (Normal ∘ u t)) ∧
    (∀x. x ∈ m_space m ⇒ (λt. u t x) differentiable_on 𝕌(:real)) ∧
    (∃w. integrable m w ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ w x ∧ w x ≠ +∞) ∧
         ∀t x. x ∈ m_space m ⇒ Normal (abs (diff1 (λt. u t x) t)) ≤ w x) ⇒
    (λt. real (∫ m (Normal ∘ u t))) differentiable_on 𝕌(:real) ∧
    ∀t. integrable m (λx. Normal (diff1 (λt. u t x) t)) ∧
        diff1 (λt. real (∫ m (Normal ∘ u t))) t =
        real (∫ m (λx. Normal (diff1 (λt. u t x) t)))

exhausting_sequence_CROSS

⊢ ∀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_cross

⊢ ∀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

⊢ ∀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

⊢ ∀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

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

fatou_lemma

⊢ ∀m f.
    measure_space m ∧ (∀x n. x ∈ m_space m ⇒ 0 ≤ f n x) ∧
    (∀n. f n ∈ Borel_measurable (measurable_space m)) ⇒
    ∫⁺ m (λx. liminf (λn. f n x)) ≤ liminf (λn. ∫⁺ m (f n))

fatou_lemma'

⊢ ∀m f w.
    measure_space m ∧ ∫⁺ m w < +∞ ∧
    (∀x n. x ∈ m_space m ⇒ 0 ≤ f n x ∧ f n x ≤ w x ∧ w x < +∞) ∧
    (∀n. f n ∈ Borel_measurable (measurable_space m)) ⇒
    limsup (λn. ∫⁺ m (f n)) ≤ ∫⁺ m (λx. limsup (λn. f n x))

fcp_cross_UNIV

⊢ FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ⇒ fcp_cross 𝕌(:α[β]) 𝕌(:α[γ]) = 𝕌(:α[β + γ])

fcp_cross_alt

⊢ ∀A B. fcp_cross A B = general_cross FCP_CONCAT A B

fcp_prod_alt

⊢ ∀A B. fcp_prod A B = general_prod FCP_CONCAT A B

fcp_sigma_alt

⊢ ∀A B. fcp_sigma A B = general_sigma FCP_CONCAT A B

filtration_from_measurable_functions

⊢ ∀m X A.
    measure_space m ∧ (∀n. X n ∈ Borel_measurable (measurable_space m)) ∧
    (∀n. A n = sigma (m_space m) (λn. Borel) X (count1 n)) ⇒
    filtration (measurable_space m) A

fubini_general

⊢ ∀cons car cdr X Y A B u v f.
    pair_operation cons car cdr ∧ sigma_finite_measure_space (X,A,u) ∧
    sigma_finite_measure_space (Y,B,v) ∧
    f ∈ Borel_measurable (general_sigma cons (X,A) (Y,B)) ∧
    (∫⁺ (general_prod_measure_space cons (X,A,u) (Y,B,v)) (abs ∘ f) ≠ +∞ ∨
     ∫⁺ (Y,B,v) (λy. ∫⁺ (X,A,u) (λx. (abs ∘ f) (cons x y))) ≠ +∞ ∨
     ∫⁺ (X,A,u) (λx. ∫⁺ (Y,B,v) (λy. (abs ∘ f) (cons x y))) ≠ +∞) ⇒
    ∫⁺ (general_prod_measure_space cons (X,A,u) (Y,B,v)) (abs ∘ f) ≠ +∞ ∧
    ∫⁺ (Y,B,v) (λy. ∫⁺ (X,A,u) (λx. (abs ∘ f) (cons x y))) ≠ +∞ ∧
    ∫⁺ (X,A,u) (λx. ∫⁺ (Y,B,v) (λy. (abs ∘ f) (cons x y))) ≠ +∞ ∧
    integrable (general_prod_measure_space cons (X,A,u) (Y,B,v)) f ∧
    (AE y::(Y,B,v). integrable (X,A,u) (λx. f (cons x y))) ∧
    (AE x::(X,A,u). integrable (Y,B,v) (λy. f (cons x y))) ∧
    integrable (X,A,u) (λx. ∫ (Y,B,v) (λy. f (cons x y))) ∧
    integrable (Y,B,v) (λy. ∫ (X,A,u) (λx. f (cons x y))) ∧
    ∫ (general_prod_measure_space cons (X,A,u) (Y,B,v)) f =
    ∫ (Y,B,v) (λy. ∫ (X,A,u) (λx. f (cons x y))) ∧
    ∫ (general_prod_measure_space cons (X,A,u) (Y,B,v)) f =
    ∫ (X,A,u) (λx. ∫ (Y,B,v) (λy. f (cons x y)))

general_BIGUNION_CROSS

⊢ ∀cons f s t.
    general_cross cons (BIGUNION (IMAGE f s)) t =
    BIGUNION (IMAGE (λn. general_cross cons (f n) t) s)

general_CROSS_BIGUNION

⊢ ∀cons f s t.
    general_cross cons t (BIGUNION (IMAGE f s)) =
    BIGUNION (IMAGE (λn. general_cross cons t (f n)) s)

general_CROSS_DIFF

⊢ ∀cons car cdr X s t.
    pair_operation cons car cdr ⇒
    general_cross cons (X DIFF s) t =
    general_cross cons X t DIFF general_cross cons s t

general_CROSS_DIFF'

⊢ ∀cons car cdr s X t.
    pair_operation cons car cdr ⇒
    general_cross cons s (X DIFF t) =
    general_cross cons s X DIFF general_cross cons s t

general_INTER_CROSS

⊢ ∀cons car cdr a b c d.
    pair_operation cons car cdr ⇒
    general_cross cons a b ∩ general_cross cons c d =
    general_cross cons (a ∩ c) (b ∩ d)

general_SUBSET_CROSS

⊢ ∀cons a b c d.
    a ⊆ b ∧ c ⊆ d ⇒ general_cross cons a c ⊆ general_cross cons b d

general_cross_empty

⊢ general_cross cons ∅ B = ∅ ∧ general_cross cons A ∅ = ∅

general_cross_reduce

⊢ ∀cons car cdr s t.
    pair_operation cons car cdr ⇒
    (t ≠ ∅ ⇒ IMAGE car (general_cross cons s t) = s) ∧
    (s ≠ ∅ ⇒ IMAGE cdr (general_cross cons s t) = t)

general_prod_measure_space_def

⊢ ∀cons m1 m2.
    general_prod_measure_space cons m1 m2 =
    (general_cross cons (m_space m1) (m_space m2),
     subsets
       (general_sigma cons (measurable_space m1) (measurable_space m2)),
     (λs. ∫⁺ m2 (λy. ∫⁺ m1 (λx. 𝟙 s (cons x y)))))

general_sigma_of_generator

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

indicator_fn_general_cross

⊢ ∀cons car cdr s t x y.
    pair_operation cons car cdr ⇒
    𝟙 (general_cross cons s t) (cons x y) = 𝟙 s x * 𝟙 t y

integrable_AE_finite

⊢ ∀m f.
    measure_space m ∧ integrable m f ⇒ AE x::m. f x = (Normal ∘ real ∘ f) x

integrable_add'

⊢ ∀m f g.
    measure_space m ∧ integrable m f ∧ integrable m g ⇒
    integrable m (λx. f x + g x)

integrable_bounded_exists

⊢ ∀m fi.
    measure_space m ∧
    (∃w0. integrable m w0 ∧ ∀i x. x ∈ m_space m ⇒ abs (fi i x) ≤ w0 x) ⇒
    ∃w. integrable m w ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ w x) ∧
        (AE x::m. w x ≠ +∞) ∧ ∀i x. x ∈ m_space m ⇒ abs (fi i x) ≤ w x

integrable_cong_AE

⊢ ∀m f g.
    complete_measure_space m ∧ (AE x::m. f x = g x) ⇒
    (integrable m f ⇔ integrable m g)

integrable_cong_AE_alt

⊢ ∀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_cong_measure

⊢ ∀sp sts u v f.
    measure_space (sp,sts,u) ∧ (∀s. s ∈ sts ⇒ u s = v s) ⇒
    (integrable (sp,sts,u) f ⇔ integrable (sp,sts,v) f)

integrable_cong_measure'

⊢ ∀m1 m2 f.
    measure_space m1 ∧ measure_space_eq m1 m2 ⇒
    (integrable m1 f ⇔ integrable m2 f)

integrable_eq_AE_alt

⊢ ∀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_measurable

⊢ ∀m f. integrable m f ⇒ f ∈ Borel_measurable (measurable_space m)

integrable_sub'

⊢ ∀m f g.
    measure_space m ∧ integrable m f ∧ integrable m g ⇒
    integrable m (λx. f x − g x)

integrable_sum'

⊢ ∀m f s.
    FINITE s ∧ measure_space m ∧ (∀i. i ∈ s ⇒ integrable m (f i)) ⇒
    integrable m (λx. ∑ (λi. f i x) s)

integral_add'

⊢ ∀m f g.
    measure_space m ∧ integrable m f ∧ integrable m g ⇒
    ∫ m (λx. f x + g x) = ∫ m f + ∫ m g

integral_add3

⊢ ∀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_cong_measure

⊢ ∀sp sts u v f.
    measure_space (sp,sts,u) ∧ (∀s. s ∈ sts ⇒ u s = v s) ⇒
    ∫ (sp,sts,u) f = ∫ (sp,sts,v) f

integral_cong_measure'

⊢ ∀m1 m2 f. measure_space m1 ∧ measure_space_eq m1 m2 ⇒ ∫ m1 f = ∫ m2 f

integral_density

⊢ ∀m f g.
    measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ∧
    g ∈ Borel_measurable (measurable_space m) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
    (integrable (density m f) g ⇔ integrable m (λx. f x * g x)) ∧
    ∫ (density m f) g = ∫ m (λx. f x * g x)

integral_disjoint_sets

⊢ ∀m f s t.
    measure_space m ∧ integrable m f ∧ DISJOINT s t ∧
    s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
    ∫ m (λx. f x * 𝟙 (s ∪ t) x) =
    ∫ m (λx. f x * 𝟙 s x) + ∫ m (λx. f x * 𝟙 t x)

integral_disjoint_sets_sum

⊢ ∀m f s a.
    FINITE s ∧ measure_space m ∧ integrable m f ∧
    (∀i. i ∈ s ⇒ a i ∈ measurable_sets m) ∧ disjoint_family_on a s ⇒
    ∫ m (λx. f x * 𝟙 (BIGUNION (IMAGE a s)) x) =
    ∑ (λi. ∫ m (λx. f x * 𝟙 (a i) x)) s

integral_distr

⊢ ∀M B f u.
    measure_space M ∧ sigma_algebra B ∧
    f ∈ measurable (measurable_space 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))

integral_eq_0_imp_AE_0

⊢ ∀m f.
    measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ∧
    (∀s. s ∈ measurable_sets m ⇒ ∫ m (λx. f x * 𝟙 s x) = 0) ⇒
    AE x::m. f x = 0

integral_eq_imp_AE_eq

⊢ ∀m f g.
    measure_space m ∧ integrable m f ∧ integrable m g ∧
    (∀s. s ∈ measurable_sets m ⇒
         ∫ m (λx. f x * 𝟙 s x) = ∫ m (λx. g x * 𝟙 s x)) ⇒
    AE x::m. f x = g x

integral_mono_AE

⊢ ∀m f g. measure_space m ∧ (AE x::m. f x ≤ g x) ⇒ ∫ m f ≤ ∫ m g

integral_sub'

⊢ ∀m f g.
    measure_space m ∧ integrable m f ∧ integrable m g ⇒
    ∫ m (λx. f x − g x) = ∫ m f − ∫ m g

integral_sum'

⊢ ∀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

lborel_2d_prod_measure

⊢ ∀s. s ∈ measurable_sets lborel_2d ⇒
      measure lborel_2d s = measure (lborel × lborel) s

lebesgue_dominated_convergence

⊢ ∀m f fi.
    measure_space m ∧ (∀i. integrable m (fi i)) ∧
    (∀i x. x ∈ m_space m ⇒ fi i x ≠ +∞ ∧ fi i x ≠ −∞) ∧
    (∀x. x ∈ m_space m ⇒ f x ≠ +∞ ∧ f x ≠ −∞) ∧
    (∀x. x ∈ m_space m ⇒ ((λi. real (fi i x)) ⟶ real (f x)) sequentially) ∧
    (∃w. integrable m w ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ w x ∧ w x ≠ +∞) ∧
         ∀i x. x ∈ m_space m ⇒ abs (fi i x) ≤ w x) ⇒
    integrable m f ∧ ((λi. real (∫ m (fi i))) ⟶ real (∫ m f)) sequentially

lebesgue_dominated_convergence'

⊢ ∀m f fi.
    measure_space m ∧ (∀i. integrable m (fi i)) ∧
    (∀i x. x ∈ m_space m ⇒ fi i x ≠ +∞ ∧ fi i x ≠ −∞) ∧
    (∀x. x ∈ m_space m ⇒ f x ≠ +∞ ∧ f x ≠ −∞) ∧
    (∀x. x ∈ m_space m ⇒ ((λi. fi i x) ⟶ f x) sequentially) ∧
    (∃w. integrable m w ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ w x ∧ w x ≠ +∞) ∧
         ∀i x. x ∈ m_space m ⇒ abs (fi i x) ≤ w x) ⇒
    integrable m f ∧ ((λi. ∫ m (fi i)) ⟶ ∫ m f) sequentially

lp_space_AE_normal

⊢ ∀p m f.
    measure_space m ∧ 0 < p ∧ f ∈ lp_space p m ⇒
    AE x::m. f x ≠ +∞ ∧ f x ≠ −∞

lp_space_add

⊢ ∀p m u v.
    measure_space m ∧ 0 < p ∧ u ∈ lp_space p m ∧ v ∈ lp_space p m ⇒
    (λx. u x + v x) ∈ lp_space p m

lp_space_add_cmul

⊢ ∀p m u v a b.
    measure_space m ∧ 0 < p ∧ u ∈ lp_space p m ∧ v ∈ lp_space p m ⇒
    (λx. Normal a * u x + Normal b * v x) ∈ lp_space p m

lp_space_alt_finite

⊢ ∀p m f.
    0 < p ∧ p ≠ +∞ ⇒
    (f ∈ lp_space p m ⇔
     f ∈ Borel_measurable (measurable_space m) ∧
     ∫⁺ m (λx. abs (f x) powr p) ≠ +∞)

lp_space_alt_finite'

⊢ ∀p m f.
    measure_space m ∧ 0 < p ∧ p ≠ +∞ ⇒
    (f ∈ lp_space p m ⇔
     f ∈ Borel_measurable (measurable_space m) ∧
     ∫ m (λx. abs (f x) powr p) ≠ +∞)

lp_space_alt_infinite

⊢ ∀m f.
    measure_space m ⇒
    (f ∈ L_PosInf m ⇔
     f ∈ Borel_measurable (measurable_space m) ∧
     ∃c. 0 < c ∧ c ≠ +∞ ∧ AE x::m. abs (f x) < c)

lp_space_alt_seminorm

⊢ ∀p m f.
    measure_space m ∧ 0 < p ⇒
    (f ∈ lp_space p m ⇔
     f ∈ Borel_measurable (measurable_space m) ∧ seminorm p m f < +∞)

lp_space_cmul

⊢ ∀p m u r.
    measure_space m ∧ 0 < p ∧ u ∈ lp_space p m ⇒
    (λx. Normal r * u x) ∈ lp_space p m

lp_space_cong

⊢ ∀p m u v.
    measure_space m ∧ 0 < p ∧ (∀x. x ∈ m_space m ⇒ u x = v x) ⇒
    (u ∈ lp_space p m ⇔ v ∈ lp_space p m)

lp_space_cong_AE

⊢ ∀p m u v.
    measure_space m ∧ 0 < p ∧ u ∈ Borel_measurable (measurable_space m) ∧
    v ∈ Borel_measurable (measurable_space m) ∧ (AE x::m. u x = v x) ⇒
    (u ∈ lp_space p m ⇔ v ∈ lp_space p m)

lp_space_sub

⊢ ∀p m u v.
    measure_space m ∧ 0 < p ∧ u ∈ lp_space p m ∧ v ∈ lp_space p m ⇒
    (λx. u x − v x) ∈ lp_space p m

martingale_alt

⊢ ∀m a u.
    martingale m a u ⇔
    sigma_finite_filtered_measure_space m a ∧ (∀n. integrable m (u n)) ∧
    ∀i j s.
      i ≤ j ∧ s ∈ subsets (a i) ⇒
      ∫ m (λx. u i x * 𝟙 s x) = ∫ m (λx. u j x * 𝟙 s x)

martingale_alt_generator

⊢ ∀m a u g.
    (∀n. a n = sigma (m_space m) (g n)) ∧
    (∀n. has_exhausting_sequence (m_space m,g n)) ∧
    (∀n s. s ∈ g n ⇒ measure m s < +∞) ∧
    (∀n s t. s ∈ g n ∧ t ∈ g n ⇒ s ∩ t ∈ g n) ⇒
    (martingale m a u ⇔
     filtered_measure_space m a ∧ (∀n. integrable m (u n)) ∧
     ∀i j s.
       i ≤ j ∧ s ∈ g i ⇒ ∫ m (λx. u i x * 𝟙 s x) = ∫ m (λx. u j x * 𝟙 s x))

measure_space_general_prod_measure

⊢ ∀cons car cdr m1 m2.
    pair_operation cons car cdr ∧ sigma_finite_measure_space m1 ∧
    sigma_finite_measure_space m2 ⇒
    measure_space (general_prod_measure_space cons m1 m2)

measure_space_prod_measure

⊢ ∀m1 m2.
    sigma_finite_measure_space m1 ∧ sigma_finite_measure_space m2 ⇒
    measure_space (m1 × m2)

pair_operation_CONS

⊢ pair_operation CONS HD TL

pair_operation_FCP_CONCAT

⊢ FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ⇒ pair_operation FCP_CONCAT FCP_FST FCP_SND

pair_operation_pair

⊢ pair_operation $, FST SND

pos_fn_integrable_AE_finite

⊢ ∀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_add3

⊢ ∀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_cong'

⊢ ∀sp sts mu nu f g.
    (measure_space (sp,sts,mu) ∨ measure_space (sp,sts,nu)) ∧
    (∀s. s ∈ sts ⇒ mu s = nu s) ∧ (∀x. x ∈ sp ⇒ 0 ≤ f x ∨ 0 ≤ g x) ∧
    (∀x. x ∈ sp ⇒ f x = g x) ⇒
    ∫⁺ (sp,sts,mu) f = ∫⁺ (sp,sts,nu) g

pos_fn_integral_cong_measure

⊢ ∀sp sts u v f.
    measure_space (sp,sts,u) ∧ (∀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'

⊢ ∀m1 m2 f.
    measure_space m1 ∧ measure_space_eq m1 m2 ∧
    (∀x. x ∈ m_space m1 ⇒ 0 ≤ f x) ⇒
    ∫⁺ m1 f = ∫⁺ m2 f

pos_fn_integral_density

⊢ ∀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_of

⊢ ∀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) ⇒
    ∫⁺ (density_of m f) g = ∫⁺ (density m f) g

pos_fn_integral_density_of_reduce

⊢ ∀m f g.
    measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ∧
    g ∈ Borel_measurable (measurable_space m) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ g x) ⇒
    ∫⁺ (density_of m f) g = ∫⁺ m (λx. f x * g x)

pos_fn_integral_density_reduce

⊢ ∀m f g.
    measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ∧
    g ∈ Borel_measurable (measurable_space m) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ g x) ⇒
    ∫⁺ (density m f) g = ∫⁺ m (λx. f x * g x)

pos_fn_integral_distr

⊢ ∀M B f u.
    measure_space M ∧ sigma_algebra B ∧
    f ∈ measurable (measurable_space M) B ∧ u ∈ Borel_measurable B ∧
    (∀x. x ∈ space B ⇒ 0 ≤ u x) ⇒
    ∫⁺ (space B,subsets B,distr M f) u = ∫⁺ M (u ∘ f)

pos_fn_integral_distr_of

⊢ ∀M N f u.
    measure_space M ∧ measure_space N ∧
    f ∈ measurable (measurable_space M) (measurable_space N) ∧
    u ∈ Borel_measurable (measurable_space N) ∧
    (∀x. x ∈ m_space N ⇒ 0 ≤ u x) ⇒
    ∫⁺ (distr_of M N f) u = ∫⁺ M (u ∘ f)

pos_fn_integral_eq_0_imp_AE_0

⊢ ∀m f.
    measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧ ∫⁺ m f = 0 ⇒
    AE x::m. f x = 0

pos_fn_integral_exchange

⊢ ∀m1 m2 f.
    sigma_finite_measure_space m1 ∧ sigma_finite_measure_space m2 ∧
    f ∈ Borel_measurable (measurable_space m1 × measurable_space m2) ∧
    (∀z. z ∈ m_space m1 × m_space m2 ⇒ 0 ≤ f z) ⇒
    ∫⁺ m1 (λx. ∫⁺ m2 (λy. f (x,y))) = ∫⁺ m2 (λy. ∫⁺ m1 (λx. f (x,y)))

prod_measure_space_alt

⊢ ∀m1 m2.
    m1 × m2 =
    (m_space m1 × m_space m2,
     subsets (measurable_space m1 × measurable_space m2),
     (λs. ∫⁺ m2 (λy. ∫⁺ m1 (λx. 𝟙 s (x,y)))))

prod_measure_space_alt_general

⊢ ∀m1 m2. m1 × m2 = general_prod_measure_space $, m1 m2

prod_sets_alt

⊢ ∀A B. prod_sets A B = general_prod $, A B

prod_sigma_alt

⊢ ∀A B. A × B = general_sigma $, A B

prod_sigma_of_generator

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

seminorm_cmul

⊢ ∀p m u r.
    measure_space m ∧ 0 < p ∧ u ∈ Borel_measurable (measurable_space m) ⇒
    seminorm p m (λx. Normal r * u x) = Normal (abs r) * seminorm p m u

seminorm_cong

⊢ ∀m u v p.
    measure_space m ∧ 0 < p ∧
    (u ∈ Borel_measurable (measurable_space m) ∨
     v ∈ Borel_measurable (measurable_space m)) ∧
    (∀x. x ∈ m_space m ⇒ u x = v x) ⇒
    seminorm p m u = seminorm p m v

seminorm_cong_AE

⊢ ∀m u v p.
    measure_space m ∧ 0 < p ∧ u ∈ Borel_measurable (measurable_space m) ∧
    v ∈ Borel_measurable (measurable_space m) ∧ (AE x::m. u x = v x) ⇒
    seminorm p m u = seminorm p m v

seminorm_eq_0

⊢ ∀p m f.
    measure_space m ∧ 0 < p ∧ f ∈ Borel_measurable (measurable_space m) ⇒
    (seminorm p m f = 0 ⇔ AE x::m. f x = 0)

seminorm_infty

⊢ ∀m f.
    seminorm +∞ m f =
    inf {c | 0 < c ∧ measure m {x | x ∈ m_space m ∧ c ≤ abs (f x)} = 0}

seminorm_infty_AE_bound

⊢ ∀m f.
    measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ⇒
    AE x::m. abs (f x) ≤ seminorm +∞ m f

seminorm_infty_alt

⊢ ∀m f.
    measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ⇒
    seminorm +∞ m f = inf {c | 0 < c ∧ AE x::m. abs (f x) < c}

seminorm_normal

⊢ ∀p m f.
    0 < p ∧ p ≠ +∞ ⇒ seminorm p m f = ∫⁺ m (λx. abs (f x) powr p) powr p⁻¹

seminorm_not_infty

⊢ ∀p m f.
    measure_space m ∧ 0 < p ∧ f ∈ lp_space p m ⇒
    seminorm p m f ≠ +∞ ∧ seminorm p m f ≠ −∞

seminorm_one

⊢ ∀m f. measure_space m ⇒ seminorm 1 m f = ∫⁺ m (abs ∘ f)

seminorm_pos

⊢ ∀p m f. 0 < p ⇒ 0 ≤ seminorm p m f

seminorm_powr

⊢ ∀p m f.
    measure_space m ∧ 0 < p ∧ p ≠ +∞ ⇒
    seminorm p m f powr p = ∫⁺ m (λx. abs (f x) powr p)

seminorm_two

⊢ ∀m f. measure_space m ⇒ seminorm 2 m f = sqrt (∫⁺ m (λx. (f x)²))

seminorm_zero

⊢ ∀p m. measure_space m ∧ 0 < p ⇒ seminorm p m (λx. 0) = 0

sigma_algebra_general_sigma

⊢ ∀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

⊢ ∀a b.
    subset_class (space a) (subsets a) ∧ subset_class (space b) (subsets b) ⇒
    sigma_algebra (fcp_sigma a b)

sigma_algebra_prod_sigma'

⊢ ∀X Y A B.
    subset_class X A ∧ subset_class Y B ⇒
    sigma_algebra (fcp_sigma (X,A) (Y,B))

sigma_finite_filtered_measure_space_alt

⊢ ∀m a.
    sigma_finite_filtered_measure_space m a ⇔
    (measure_space m ∧ filtration (measurable_space m) a) ∧
    sigma_finite (m_space m,subsets (a 0),measure m)

sigma_finite_filtered_measure_space_alt_all

⊢ ∀m a.
    sigma_finite_filtered_measure_space m a ⇔
    measure_space m ∧ filtration (measurable_space m) a ∧
    ∀n. sigma_finite (m_space m,subsets (a n),measure m)

sub_martingale_alt

⊢ ∀m a u.
    sub_martingale m a u ⇔
    sigma_finite_filtered_measure_space m a ∧ (∀n. integrable m (u n)) ∧
    ∀i j s.
      i ≤ j ∧ s ∈ subsets (a i) ⇒
      ∫ m (λx. u i x * 𝟙 s x) ≤ ∫ m (λx. u j x * 𝟙 s x)

sub_martingale_alt_generator

⊢ ∀m a u g.
    (∀n. a n = sigma (m_space m) (g n)) ∧
    (∀n. has_exhausting_sequence (m_space m,g n)) ∧
    (∀n s. s ∈ g n ⇒ measure m s < +∞) ∧ (∀n. semiring (m_space m,g n)) ⇒
    (sub_martingale m a u ⇔
     filtered_measure_space m a ∧ (∀n. integrable m (u n)) ∧
     ∀i j s.
       i ≤ j ∧ s ∈ g i ⇒ ∫ m (λx. u i x * 𝟙 s x) ≤ ∫ m (λx. u j x * 𝟙 s x))

super_martingale_alt

⊢ ∀m a u.
    super_martingale m a u ⇔
    sigma_finite_filtered_measure_space m a ∧ (∀n. integrable m (u n)) ∧
    ∀i j s.
      i ≤ j ∧ s ∈ subsets (a i) ⇒
      ∫ m (λx. u j x * 𝟙 s x) ≤ ∫ m (λx. u i x * 𝟙 s x)

super_martingale_alt_generator

⊢ ∀m a u g.
    (∀n. a n = sigma (m_space m) (g n)) ∧
    (∀n. has_exhausting_sequence (m_space m,g n)) ∧
    (∀n s. s ∈ g n ⇒ measure m s < +∞) ∧ (∀n. semiring (m_space m,g n)) ⇒
    (super_martingale m a u ⇔
     filtered_measure_space m a ∧ (∀n. integrable m (u n)) ∧
     ∀i j s.
       i ≤ j ∧ s ∈ g i ⇒ ∫ m (λx. u j x * 𝟙 s x) ≤ ∫ m (λx. u i x * 𝟙 s x))

tonelli_general

⊢ ∀cons car cdr X Y A B u v f.
    pair_operation cons car cdr ∧ sigma_finite_measure_space (X,A,u) ∧
    sigma_finite_measure_space (Y,B,v) ∧
    f ∈ Borel_measurable (general_sigma cons (X,A) (Y,B)) ∧
    (∀s. s ∈ general_cross cons X Y ⇒ 0 ≤ f s) ⇒
    (∀y. y ∈ Y ⇒ (λx. f (cons x y)) ∈ Borel_measurable (X,A)) ∧
    (∀x. x ∈ X ⇒ (λy. f (cons x y)) ∈ Borel_measurable (Y,B)) ∧
    (λx. ∫⁺ (Y,B,v) (λy. f (cons x y))) ∈ Borel_measurable (X,A) ∧
    (λy. ∫⁺ (X,A,u) (λx. f (cons x y))) ∈ Borel_measurable (Y,B) ∧
    ∫⁺ (general_prod_measure_space cons (X,A,u) (Y,B,v)) f =
    ∫⁺ (Y,B,v) (λy. ∫⁺ (X,A,u) (λx. f (cons x y))) ∧
    ∫⁺ (general_prod_measure_space cons (X,A,u) (Y,B,v)) f =
    ∫⁺ (X,A,u) (λx. ∫⁺ (Y,B,v) (λy. f (cons x y)))

uniqueness_of_prod_measure

⊢ ∀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'

⊢ ∀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

⊢ ∀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'

⊢ ∀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

Theory martingale

Parents

Contents

Type operators

Constants

Definitions

Theorems

Definitions

Theorems