Structure martingaleTheory
signature martingaleTheory =
sig
type thm = Thm.thm
(* Definitions *)
val fcp_cross_def : thm
val fcp_prod_def : thm
val fcp_sigma_def : thm
val filtered_measure_space_def : thm
val filtration_def : thm
val general_cross_def : thm
val general_prod_def : thm
val general_sigma_def : thm
val infty_sigma_algebra_def : thm
val lborel_2d_def : thm
val lp_space_def : thm
val martingale_def : thm
val pair_operation_def : thm
val prod_measure_def : thm
val prod_measure_space_def : thm
val seminorm_def : thm
val sigma_finite_filtered_measure_space_def : thm
val sub_martingale_def : thm
val sub_sigma_algebra_def : thm
val super_martingale_def : thm
(* Theorems *)
val CROSS_ALT : thm
val Cauchy_Schwarz_inequality : thm
val Cauchy_Schwarz_inequality' : thm
val EXISTENCE_OF_PROD_MEASURE : thm
val EXISTENCE_OF_PROD_MEASURE' : thm
val FCP_BIGUNION_CROSS : thm
val FCP_CROSS_BIGUNION : thm
val FCP_CROSS_DIFF : thm
val FCP_CROSS_DIFF' : thm
val FCP_INTER_CROSS : thm
val FCP_SUBSET_CROSS : 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 Hoelder_inequality : thm
val Hoelder_inequality' : thm
val INDICATOR_FN_FCP_CROSS : thm
val INFTY_SIGMA_ALGEBRA_BOUNDED : thm
val INFTY_SIGMA_ALGEBRA_MAXIMAL : thm
val IN_FCP_CROSS : thm
val IN_FCP_PROD : thm
val IN_MEASURABLE_BOREL_FROM_PROD_SIGMA : thm
val IN_general_cross : thm
val IN_general_prod : thm
val L1_space_alt_integrable : thm
val L2_space_alt_integrable_square : thm
val LIM_SEQUENTIALLY_CESARO : thm
val LIM_SEQUENTIALLY_real_normal : thm
val MARTINGALE_EQ_SUB_SUPER : thm
val Minkowski_inequality : thm
val Minkowski_inequality' : thm
val PROD_SIGMA_OF_GENERATOR : thm
val SIGMA_FINITE_FILTERED_MEASURE_SPACE : 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_cross : thm
val exhausting_sequence_general_cross : thm
val existence_of_prod_measure : thm
val existence_of_prod_measure_general : thm
val ext_liminf_imp_subseq : thm
val ext_liminf_le_subseq : thm
val ext_limsup_imp_subseq : thm
val ext_limsup_le_subseq : thm
val ext_limsup_thm : thm
val fatou_lemma : thm
val fatou_lemma' : thm
val fcp_cross_UNIV : thm
val fcp_cross_alt : thm
val fcp_prod_alt : thm
val fcp_sigma_alt : thm
val filtration_from_measurable_functions : thm
val general_BIGUNION_CROSS : thm
val general_CROSS_BIGUNION : thm
val general_CROSS_DIFF : thm
val general_CROSS_DIFF' : thm
val general_INTER_CROSS : thm
val general_SUBSET_CROSS : thm
val general_sigma_of_generator : thm
val indicator_fn_general_cross : 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 lebesgue_dominated_convergence : thm
val lp_space_AE_normal : thm
val lp_space_add : thm
val lp_space_add_cmul : thm
val lp_space_alt_finite : thm
val lp_space_alt_finite' : thm
val lp_space_alt_infinite : thm
val lp_space_alt_seminorm : thm
val lp_space_cmul : thm
val lp_space_cong : thm
val lp_space_cong_AE : thm
val lp_space_sub : thm
val martingale_alt : thm
val martingale_alt_generator : thm
val measure_space_prod_measure : thm
val pair_operation_FCP_CONCAT : thm
val pair_operation_pair : thm
val pos_fn_integral_cong_measure : thm
val pos_fn_integral_cong_measure' : thm
val pos_fn_integral_distr : thm
val prod_measure_space_alt : thm
val prod_sets_alt : thm
val prod_sigma_alt : thm
val prod_sigma_of_generator : thm
val seminorm_cmul : thm
val seminorm_cong : thm
val seminorm_cong_AE : thm
val seminorm_eq_0 : thm
val seminorm_infty : thm
val seminorm_infty_AE_bound : thm
val seminorm_infty_alt : thm
val seminorm_normal : thm
val seminorm_not_infty : thm
val seminorm_one : thm
val seminorm_pos : thm
val seminorm_powr : thm
val seminorm_two : thm
val seminorm_zero : thm
val sigma_algebra_general_sigma : thm
val sigma_algebra_prod_sigma : thm
val sigma_algebra_prod_sigma' : thm
val sigma_finite_filtered_measure_space_alt : thm
val sigma_finite_filtered_measure_space_alt_all : thm
val sub_martingale_alt : thm
val sub_martingale_alt_generator : thm
val super_martingale_alt : thm
val super_martingale_alt_generator : 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
(*
[fcp] Parent theory of "martingale"
[lebesgue] Parent theory of "martingale"
[fcp_cross_def] Definition
⊢ ∀A B. fcp_cross A B = {FCP_CONCAT a b | a ∈ A ∧ b ∈ B}
[fcp_prod_def] Definition
⊢ ∀a b. fcp_prod a b = {fcp_cross s t | s ∈ a ∧ t ∈ b}
[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
⊢ ∀m a.
filtered_measure_space m a ⇔
measure_space m ∧ filtration (measurable_space m) 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_cross_def] Definition
⊢ ∀cons A B. general_cross cons A B = {cons a b | a ∈ A ∧ b ∈ B}
[general_prod_def] Definition
⊢ ∀cons A B.
general_prod cons A B = {general_cross cons a b | a ∈ A ∧ b ∈ B}
[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))
[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)))
[lp_space_def] Definition
⊢ ∀p m.
lp_space p m =
{f |
f ∈ Borel_measurable (measurable_space m) ∧
if p = +∞ then
∃c. 0 < c ∧ c ≠ +∞ ∧
measure m {x | x ∈ m_space m ∧ c ≤ abs (f x)} = 0
else ∫⁺ m (λx. abs (f x) powr p) ≠ +∞}
[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)
[pair_operation_def] Definition
⊢ ∀cons car cdr.
pair_operation cons car cdr ⇔
(∀a b. car (cons a b) = a ∧ cdr (cons a b) = b) ∧
∀a b c d. cons a b = cons c d ⇔ a = c ∧ b = d
[prod_measure_def] Definition
⊢ ∀m1 m2.
prod_measure m1 m2 = (λs. ∫⁺ m2 (λy. ∫⁺ m1 (λx. 𝟙 s (x,y))))
[prod_measure_space_def] Definition
⊢ ∀m1 m2.
m1 × m2 =
(m_space m1 × m_space m2,
subsets (measurable_space m1 × measurable_space m2),
prod_measure m1 m2)
[seminorm_def] Definition
⊢ ∀p m f.
seminorm p m f =
if p = +∞ then
inf
{c |
0 < c ∧ measure m {x | x ∈ m_space m ∧ c ≤ abs (f x)} = 0}
else ∫⁺ m (λx. abs (f x) powr p) powr p⁻¹
[sigma_finite_filtered_measure_space_def] Definition
⊢ ∀m a.
sigma_finite_filtered_measure_space m a ⇔
filtered_measure_space m a ∧
sigma_finite (m_space m,subsets (a 0),measure 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)
[CROSS_ALT] Theorem
⊢ ∀A B. A × B = general_cross $, A B
[Cauchy_Schwarz_inequality] Theorem
⊢ ∀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'] Theorem
⊢ ∀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] 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)))
[FCP_BIGUNION_CROSS] Theorem
⊢ ∀f s t.
fcp_cross (BIGUNION (IMAGE f s)) t =
BIGUNION (IMAGE (λn. fcp_cross (f n) t) s)
[FCP_CROSS_BIGUNION] Theorem
⊢ ∀f s t.
fcp_cross t (BIGUNION (IMAGE f s)) =
BIGUNION (IMAGE (λn. fcp_cross t (f n)) s)
[FCP_CROSS_DIFF] Theorem
⊢ ∀X s t.
FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ⇒
fcp_cross (X DIFF s) t = fcp_cross X t DIFF fcp_cross s t
[FCP_CROSS_DIFF'] Theorem
⊢ ∀s X t.
FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ⇒
fcp_cross s (X DIFF t) = fcp_cross s X DIFF fcp_cross s t
[FCP_INTER_CROSS] Theorem
⊢ ∀a b c d.
FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ⇒
fcp_cross a b ∩ fcp_cross c d = fcp_cross (a ∩ c) (b ∩ d)
[FCP_SUBSET_CROSS] Theorem
⊢ ∀a b c d. a ⊆ b ∧ c ⊆ d ⇒ fcp_cross a c ⊆ fcp_cross b d
[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 (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'] Theorem
⊢ ∀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] Theorem
⊢ ∀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'] Theorem
⊢ ∀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] Theorem
⊢ ∀s t x y.
FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ⇒
𝟙 (fcp_cross s t) (FCP_CONCAT x y) = 𝟙 s x * 𝟙 t 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_FCP_CROSS] Theorem
⊢ ∀s a b.
s ∈ fcp_cross a b ⇔ ∃t u. s = FCP_CONCAT t u ∧ t ∈ a ∧ u ∈ b
[IN_FCP_PROD] Theorem
⊢ ∀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] 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)
[IN_general_cross] Theorem
⊢ ∀cons s A B.
s ∈ general_cross cons A B ⇔ ∃a b. s = cons a b ∧ a ∈ A ∧ b ∈ B
[IN_general_prod] Theorem
⊢ ∀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] Theorem
⊢ ∀m f. measure_space m ⇒ (f ∈ L1_space m ⇔ integrable m f)
[L2_space_alt_integrable_square] Theorem
⊢ ∀m f.
measure_space m ⇒
(f ∈ L2_space m ⇔
f ∈ Borel_measurable (measurable_space m) ∧
integrable m (λx. (f x)²))
[LIM_SEQUENTIALLY_CESARO] Theorem
⊢ ∀f l.
((λn. f n) --> l) sequentially ⇒
((λn. ∑ f (count1 n) / &SUC n) --> l) sequentially
[LIM_SEQUENTIALLY_real_normal] Theorem
⊢ ∀a l.
(∀n. a n ≠ +∞ ∧ a n ≠ −∞) ⇒
((real ∘ a --> l) sequentially ⇔
∀e. 0 < e ⇒ ∃N. ∀n. N ≤ n ⇒ abs (a n − Normal l) < Normal e)
[MARTINGALE_EQ_SUB_SUPER] Theorem
⊢ ∀m a u.
martingale m a u ⇔ sub_martingale m a u ∧ super_martingale m a u
[Minkowski_inequality] Theorem
⊢ ∀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'] Theorem
⊢ ∀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_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] Theorem
⊢ ∀m a.
sigma_finite_filtered_measure_space m a ⇒
∀n. sigma_finite (m_space m,subsets (a n),measure 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 (measurable_space 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_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)))
[ext_liminf_imp_subseq] Theorem
⊢ ∀a. (∀n. a n ≠ +∞ ∧ a n ≠ −∞) ∧ liminf a ≠ +∞ ∧ liminf a ≠ −∞ ⇒
∃f. (∀m n. m < n ⇒ f m < f n) ∧
(real ∘ a ∘ f --> real (liminf a)) sequentially
[ext_liminf_le_subseq] Theorem
⊢ ∀a f l.
(∀n. a n ≠ +∞ ∧ a n ≠ −∞) ∧ (∀m n. m < n ⇒ f m < f n) ∧
(real ∘ a ∘ f --> l) sequentially ⇒
liminf a ≤ Normal l
[ext_limsup_imp_subseq] Theorem
⊢ ∀a. (∀n. a n ≠ +∞ ∧ a n ≠ −∞) ∧ limsup a ≠ +∞ ∧ limsup a ≠ −∞ ⇒
∃f. (∀m n. m < n ⇒ f m < f n) ∧
(real ∘ a ∘ f --> real (limsup a)) sequentially
[ext_limsup_le_subseq] Theorem
⊢ ∀a f l.
(∀n. a n ≠ +∞ ∧ a n ≠ −∞) ∧ (∀m n. m < n ⇒ f m < f n) ∧
(real ∘ a ∘ f --> l) sequentially ⇒
Normal l ≤ limsup a
[ext_limsup_thm] Theorem
⊢ ∀a l.
(∀n. a n ≠ +∞ ∧ a n ≠ −∞) ⇒
((real ∘ a --> l) sequentially ⇔
limsup a = Normal l ∧ liminf a = Normal l)
[fatou_lemma] Theorem
⊢ ∀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'] Theorem
⊢ ∀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] Theorem
⊢ FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ⇒
fcp_cross 𝕌(:α[β]) 𝕌(:α[γ]) = 𝕌(:α[β + γ])
[fcp_cross_alt] Theorem
⊢ ∀A B. fcp_cross A B = general_cross FCP_CONCAT A B
[fcp_prod_alt] Theorem
⊢ ∀A B. fcp_prod A B = general_prod FCP_CONCAT A B
[fcp_sigma_alt] Theorem
⊢ ∀A B. fcp_sigma A B = general_sigma FCP_CONCAT A B
[filtration_from_measurable_functions] Theorem
⊢ ∀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
[general_BIGUNION_CROSS] Theorem
⊢ ∀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] Theorem
⊢ ∀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] Theorem
⊢ ∀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'] Theorem
⊢ ∀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] Theorem
⊢ ∀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] Theorem
⊢ ∀cons a b c d.
a ⊆ b ∧ c ⊆ d ⇒ general_cross cons a c ⊆ general_cross cons b d
[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)
[indicator_fn_general_cross] Theorem
⊢ ∀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_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 ∧ measure_space_eq m1 m2 ⇒
(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 ∧ measure_space_eq m1 m2 ⇒
∫ m1 f = ∫ m2 f
[integral_distr] Theorem
⊢ ∀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))
[lborel_2d_prod_measure] Theorem
⊢ ∀s. s ∈ measurable_sets lborel_2d ⇒
measure lborel_2d s = measure (lborel × lborel) s
[lebesgue_dominated_convergence] Theorem
⊢ ∀m f fi.
measure_space m ∧ (∀i. integrable m (fi i)) ∧ integrable m f ∧
(∀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) ⇒
((λi. real (∫ m (fi i))) --> real (∫ m f)) sequentially
[lp_space_AE_normal] Theorem
⊢ ∀p m f.
measure_space m ∧ 0 < p ∧ f ∈ lp_space p m ⇒
AE x::m. f x ≠ +∞ ∧ f x ≠ −∞
[lp_space_add] Theorem
⊢ ∀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] Theorem
⊢ ∀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] Theorem
⊢ ∀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'] Theorem
⊢ ∀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] Theorem
⊢ ∀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] Theorem
⊢ ∀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] Theorem
⊢ ∀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] Theorem
⊢ ∀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] Theorem
⊢ ∀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] Theorem
⊢ ∀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] Theorem
⊢ ∀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] Theorem
⊢ ∀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_prod_measure] Theorem
⊢ ∀m1 m2.
sigma_finite_measure_space m1 ∧ sigma_finite_measure_space m2 ⇒
measure_space (m1 × m2)
[pair_operation_FCP_CONCAT] Theorem
⊢ FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ⇒
pair_operation FCP_CONCAT FCP_FST FCP_SND
[pair_operation_pair] Theorem
⊢ pair_operation $, FST SND
[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 ∧ measure_space_eq m1 m2 ∧
(∀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 (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)
[prod_measure_space_alt] Theorem
⊢ ∀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_sets_alt] Theorem
⊢ ∀A B. prod_sets A B = general_prod $, A B
[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)
[seminorm_cmul] Theorem
⊢ ∀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] Theorem
⊢ ∀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] Theorem
⊢ ∀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] Theorem
⊢ ∀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] Theorem
⊢ ∀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] Theorem
⊢ ∀m f.
measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ⇒
AE x::m. abs (f x) ≤ seminorm +∞ m f
[seminorm_infty_alt] Theorem
⊢ ∀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] Theorem
⊢ ∀p m f.
0 < p ∧ p ≠ +∞ ⇒
seminorm p m f = ∫⁺ m (λx. abs (f x) powr p) powr p⁻¹
[seminorm_not_infty] Theorem
⊢ ∀p m f.
measure_space m ∧ 0 < p ∧ f ∈ lp_space p m ⇒
seminorm p m f ≠ +∞ ∧ seminorm p m f ≠ −∞
[seminorm_one] Theorem
⊢ ∀m f. measure_space m ⇒ seminorm 1 m f = ∫⁺ m (abs ∘ f)
[seminorm_pos] Theorem
⊢ ∀p m f. 0 < p ⇒ 0 ≤ seminorm p m f
[seminorm_powr] Theorem
⊢ ∀p m f.
measure_space m ∧ 0 < p ∧ p ≠ +∞ ⇒
seminorm p m f powr p = ∫⁺ m (λx. abs (f x) powr p)
[seminorm_two] Theorem
⊢ ∀m f. measure_space m ⇒ seminorm 2 m f = sqrt (∫⁺ m (λx. (f x)²))
[seminorm_zero] Theorem
⊢ ∀p m. measure_space m ∧ 0 < p ⇒ seminorm p m (λx. 0) = 0
[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_filtered_measure_space_alt] Theorem
⊢ ∀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] Theorem
⊢ ∀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] Theorem
⊢ ∀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] Theorem
⊢ ∀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] Theorem
⊢ ∀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] Theorem
⊢ ∀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))
[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, Trindemossen-1