Structure measureTheory
signature measureTheory =
sig
type thm = Thm.thm
(* Definitions *)
val additive_def : thm
val caratheodory_sets_def : thm
val complete_measure_space_def : thm
val completion_def : thm
val countably_additive_def : thm
val countably_subadditive_def : thm
val exhausting_sequence_def : thm
val finite_additive_def : thm
val finite_subadditive_def : thm
val has_exhausting_sequence : thm
val increasing_def : thm
val m_space_def : thm
val measurable_sets_def : thm
val measure_def : thm
val measure_preserving_def : thm
val measure_space_def : thm
val measure_space_eq_def : thm
val metric_countable_covers_def : thm
val null_set_def : thm
val outer_measure_def : thm
val outer_measure_space_def : thm
val positive_def : thm
val premeasure_def : thm
val sigma_finite : thm
val sigma_finite_measure_space_def : thm
val subadditive_def : thm
(* Theorems *)
val ADDITIVE : thm
val ADDITIVE_INCREASING : thm
val ADDITIVE_SUM : thm
val ALGEBRA_COUNTABLY_ADDITIVE_ADDITIVE : thm
val ALGEBRA_PREMEASURE_ADDITIVE : thm
val ALGEBRA_PREMEASURE_COMPL : thm
val ALGEBRA_PREMEASURE_COUNTABLE_INCREASING : thm
val ALGEBRA_PREMEASURE_COUNTABLY_SUBADDITIVE : thm
val ALGEBRA_PREMEASURE_DIFF_SUBSET : thm
val ALGEBRA_PREMEASURE_FINITE_ADDITIVE : thm
val ALGEBRA_PREMEASURE_FINITE_SUBADDITIVE : thm
val ALGEBRA_PREMEASURE_INCREASING : thm
val ALGEBRA_PREMEASURE_STRONG_ADDITIVE : thm
val ALGEBRA_PREMEASURE_SUBADDITIVE : thm
val BIGUNION_IMAGE_Q : thm
val CARATHEODORY : thm
val CARATHEODORY_RING : thm
val CARATHEODORY_SEMIRING : thm
val COMPLETE_MEASURE_THM : thm
val COMPLETION_STABLE : thm
val COMPLETION_STABLE' : thm
val COMPLETION_SUBSET_SUBSETS : thm
val COUNTABLY_ADDITIVE : thm
val COUNTABLY_ADDITIVE_ADDITIVE : thm
val COUNTABLY_ADDITIVE_FINITE_ADDITIVE : thm
val COUNTABLY_SUBADDITIVE : thm
val COUNTABLY_SUBADDITIVE_FINITE_SUBADDITIVE : thm
val COUNTABLY_SUBADDITIVE_SUBADDITIVE : thm
val DYNKIN_SYSTEM_DIFF_SUBSET : thm
val DYNKIN_SYSTEM_PREMEASURE_ADDITIVE : thm
val DYNKIN_SYSTEM_PREMEASURE_FINITE_ADDITIVE : thm
val DYNKIN_SYSTEM_PREMEASURE_INCREASING : thm
val FINITE_ADDITIVE : thm
val FINITE_ADDITIVE_ALT : thm
val FINITE_IMP_SIGMA_FINITE : thm
val FINITE_SUBADDITIVE : thm
val FINITE_SUBADDITIVE_ALT : thm
val INCREASING : thm
val IN_MEASURE_PRESERVING : thm
val IN_NULL_SET : thm
val MEASURABLE_IF : thm
val MEASURABLE_IF_SET : thm
val MEASURABLE_POW_TO_POW : thm
val MEASURABLE_POW_TO_POW_IMAGE : thm
val MEASURABLE_RANGE_REDUCE : thm
val MEASURABLE_SETS_SUBSET_SPACE : thm
val MEASURE_ADDITIVE : thm
val MEASURE_COMPL : thm
val MEASURE_COMPL_SUBSET : thm
val MEASURE_COUNTABLE_INCREASING : thm
val MEASURE_COUNTABLY_ADDITIVE : thm
val MEASURE_DIFF_SUBSET : thm
val MEASURE_DOWN : thm
val MEASURE_EMPTY : thm
val MEASURE_EXTREAL_SUM_IMAGE : thm
val MEASURE_FINITE_ADDITIVE : thm
val MEASURE_INCREASING : thm
val MEASURE_POSITIVE : thm
val MEASURE_PRESERVING_LIFT : thm
val MEASURE_PRESERVING_SUBSET : thm
val MEASURE_PRESERVING_UP_LIFT : thm
val MEASURE_PRESERVING_UP_SIGMA : thm
val MEASURE_PRESERVING_UP_SUBSET : thm
val MEASURE_SPACE_ADDITIVE : thm
val MEASURE_SPACE_BIGINTER : thm
val MEASURE_SPACE_BIGUNION : thm
val MEASURE_SPACE_CMUL : thm
val MEASURE_SPACE_COMPL : thm
val MEASURE_SPACE_COUNTABLY_SUBADDITIVE : thm
val MEASURE_SPACE_DIFF : thm
val MEASURE_SPACE_EMPTY_MEASURABLE : thm
val MEASURE_SPACE_FINITE_DIFF : thm
val MEASURE_SPACE_FINITE_DIFF_SUBSET : thm
val MEASURE_SPACE_FINITE_MEASURE : thm
val MEASURE_SPACE_FINITE_SUBADDITIVE : thm
val MEASURE_SPACE_INCREASING : thm
val MEASURE_SPACE_INTER : thm
val MEASURE_SPACE_IN_MSPACE : thm
val MEASURE_SPACE_MSPACE_MEASURABLE : thm
val MEASURE_SPACE_POSITIVE : thm
val MEASURE_SPACE_REDUCE : thm
val MEASURE_SPACE_RESTRICTED : thm
val MEASURE_SPACE_RESTRICTED_MEASURE : thm
val MEASURE_SPACE_RESTRICTION : thm
val MEASURE_SPACE_RESTRICTION' : thm
val MEASURE_SPACE_SIGMA_ALGEBRA : thm
val MEASURE_SPACE_SPACE : thm
val MEASURE_SPACE_STRONG_ADDITIVE : thm
val MEASURE_SPACE_SUBADDITIVE : thm
val MEASURE_SPACE_SUBSET : thm
val MEASURE_SPACE_SUBSET_MSPACE : thm
val MEASURE_SPACE_UNION : thm
val MONOTONE_CONVERGENCE : thm
val MONOTONE_CONVERGENCE2 : thm
val MONOTONE_CONVERGENCE_BIGINTER : thm
val MONOTONE_CONVERGENCE_BIGINTER2 : thm
val NULL_SET_BIGUNION : thm
val NULL_SET_BIGUNION' : thm
val NULL_SET_EMPTY : thm
val NULL_SET_INTER : thm
val NULL_SET_INTER' : thm
val NULL_SET_THM : thm
val NULL_SET_UNION : thm
val NULL_SET_UNION' : thm
val OUTER_MEASURE_CONSTRUCTION : thm
val OUTER_MEASURE_SPACE_FINITE_SUBADDITIVE : thm
val OUTER_MEASURE_SPACE_POSITIVE : thm
val OUTER_MEASURE_SPACE_SUBADDITIVE : thm
val RING_ADDITIVE_EVERYTHING : thm
val RING_ADDITIVE_FINITE_ADDITIVE : thm
val RING_ADDITIVE_INCREASING : thm
val RING_ADDITIVE_STRONG_ADDITIVE : thm
val RING_ADDITIVE_SUBADDITIVE : thm
val RING_PREMEASURE_ADDITIVE : thm
val RING_PREMEASURE_COUNTABLE_INCREASING : thm
val RING_PREMEASURE_COUNTABLY_SUBADDITIVE : thm
val RING_PREMEASURE_DIFF_SUBSET : thm
val RING_PREMEASURE_FINITE_ADDITIVE : thm
val RING_PREMEASURE_FINITE_SUBADDITIVE : thm
val RING_PREMEASURE_INCREASING : thm
val RING_PREMEASURE_STRONG_ADDITIVE : thm
val RING_PREMEASURE_SUBADDITIVE : thm
val RING_SUBADDITIVE_FINITE_SUBADDITIVE : thm
val SEMIRING_FINITE_ADDITIVE_EXTENSION : thm
val SEMIRING_PREMEASURE_ADDITIVE : thm
val SEMIRING_PREMEASURE_EXTENSION : thm
val SEMIRING_PREMEASURE_FINITE_ADDITIVE : thm
val SEMIRING_PREMEASURE_INCREASING : thm
val SEMIRING_SIGMA_MONOTONE : thm
val SIGMA_ALGEBRA_COMPLETION : thm
val SIGMA_FINITE_ALT : thm
val SIGMA_FINITE_ALT2 : thm
val SIGMA_SUBSET_MEASURABLE_SETS : thm
val STRONG_MEASURE_SPACE_SUBSET : thm
val SUBADDITIVE : thm
val UNIQUENESS_OF_MEASURE : thm
val UNIQUENESS_OF_MEASURE_FINITE : thm
val countable_covers_def : thm
val countably_additive_alt_eq : thm
val exhausting_sequence_alt : thm
val finite_additivity_sufficient_for_finite_spaces : thm
val finite_additivity_sufficient_for_finite_spaces2 : thm
val has_exhausting_sequence_alt : thm
val has_exhausting_sequence_def : thm
val limsup_suminf_indicator_space : thm
val measure_liminf : thm
val measure_limsup : thm
val measure_limsup_finite : thm
val measure_space_add : thm
val measure_space_add' : thm
val measure_space_cmul : thm
val measure_space_cong : thm
val measure_space_dirac_measure : thm
val measure_space_eq : thm
val measure_space_eq' : thm
val measure_space_eq_comm : thm
val measure_space_eq_trans : thm
val measure_space_measure_eq : thm
val measure_space_sum : thm
val measure_space_suminf : thm
val measure_space_trivial : thm
val measure_split : thm
val null_sets : thm
val positive_not_infty : thm
val sets_eq_imp_space_eq : thm
val sigma_finite_alt : thm
val sigma_finite_alt_exhausting_sequence : thm
val sigma_finite_def : thm
val sigma_finite_disjoint : thm
val sigma_finite_has_exhausting_sequence : thm
val sigma_finite_thm : thm
val measure_grammars : type_grammar.grammar * term_grammar.grammar
(*
[extreal] Parent theory of "measure"
[sigma_algebra] Parent theory of "measure"
[additive_def] Definition
⊢ ∀m. additive m ⇔
∀s t.
s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧
DISJOINT s t ∧ s ∪ t ∈ measurable_sets m ⇒
measure m (s ∪ t) = measure m s + measure m t
[caratheodory_sets_def] Definition
⊢ ∀sp m.
caratheodory_sets sp m =
{a | a ⊆ sp ∧ ∀q. q ⊆ sp ⇒ m q = m (q ∩ a) + m (q DIFF a)}
[complete_measure_space_def] Definition
⊢ ∀m. complete_measure_space m ⇔
measure_space m ∧
∀s. null_set m s ⇒ ∀t. t ⊆ s ⇒ t ∈ measurable_sets m
[completion_def] Definition
⊢ ∀m. completion m =
(m_space m,
{s ∪ n | s ∈ measurable_sets m ∧ ∃t. n ⊆ t ∧ null_set m t})
[countably_additive_def] Definition
⊢ ∀m. countably_additive m ⇔
∀f. f ∈ (𝕌(:num) → measurable_sets m) ∧
(∀i j. i ≠ j ⇒ DISJOINT (f i) (f j)) ∧
BIGUNION (IMAGE f 𝕌(:num)) ∈ measurable_sets m ⇒
measure m (BIGUNION (IMAGE f 𝕌(:num))) =
suminf (measure m ∘ f)
[countably_subadditive_def] Definition
⊢ ∀m. countably_subadditive m ⇔
∀f. f ∈ (𝕌(:num) → measurable_sets m) ∧
BIGUNION (IMAGE f 𝕌(:num)) ∈ measurable_sets m ⇒
measure m (BIGUNION (IMAGE f 𝕌(:num))) ≤
suminf (measure m ∘ f)
[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
[finite_additive_def] Definition
⊢ ∀m. finite_additive m ⇔
∀f n.
(∀i. i < n ⇒ f i ∈ measurable_sets m) ∧
(∀i j. i < n ∧ j < n ∧ i ≠ j ⇒ DISJOINT (f i) (f j)) ∧
BIGUNION (IMAGE f (count n)) ∈ measurable_sets m ⇒
measure m (BIGUNION (IMAGE f (count n))) =
∑ (measure m ∘ f) (count n)
[finite_subadditive_def] Definition
⊢ ∀m. finite_subadditive m ⇔
∀f n.
(∀i. i < n ⇒ f i ∈ measurable_sets m) ∧
BIGUNION (IMAGE f (count n)) ∈ measurable_sets m ⇒
measure m (BIGUNION (IMAGE f (count n))) ≤
∑ (measure m ∘ f) (count n)
[has_exhausting_sequence] Definition
⊢ ∀a. has_exhausting_sequence a ⇔ ∃f. exhausting_sequence a f
[increasing_def] Definition
⊢ ∀m. increasing m ⇔
∀s t.
s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧ s ⊆ t ⇒
measure m s ≤ measure m t
[m_space_def] Definition
⊢ ∀sp sts mu. m_space (sp,sts,mu) = sp
[measurable_sets_def] Definition
⊢ ∀sp sts mu. measurable_sets (sp,sts,mu) = sts
[measure_def] Definition
⊢ ∀sp sts mu. measure (sp,sts,mu) = mu
[measure_preserving_def] Definition
⊢ ∀m1 m2.
measure_preserving m1 m2 =
{f |
f ∈ measurable (measurable_space m1) (measurable_space m2) ∧
∀s. s ∈ measurable_sets m2 ⇒
measure m1 (PREIMAGE f s ∩ m_space m1) = measure m2 s}
[measure_space_def] Definition
⊢ ∀m. measure_space m ⇔
sigma_algebra (measurable_space m) ∧ positive m ∧
countably_additive m
[measure_space_eq_def] Definition
⊢ ∀m1 m2.
measure_space_eq m1 m2 ⇔
m_space m1 = m_space m2 ∧
measurable_sets m1 = measurable_sets m2 ∧
∀s. s ∈ measurable_sets m1 ⇒ measure m1 s = measure m2 s
[metric_countable_covers_def] Definition
⊢ ∀d e sts.
metric_countable_covers d e sts =
(λa.
{f |
f ∈ (𝕌(:num) → sts) ∧ a ⊆ BIGUNION (IMAGE f 𝕌(:num)) ∧
∀i. Normal (set_diameter d (f i)) ≤ e})
[null_set_def] Definition
⊢ ∀m s. null_set m s ⇔ s ∈ measurable_sets m ∧ measure m s = 0
[outer_measure_def] Definition
⊢ ∀m C.
outer_measure m C =
(λa. inf {r | (∃f. f ∈ C a ∧ suminf (m ∘ f) = r)})
[outer_measure_space_def] Definition
⊢ ∀m. outer_measure_space m ⇔
subset_class (m_space m) (measurable_sets m) ∧
∅ ∈ measurable_sets m ∧ positive m ∧ increasing m ∧
countably_subadditive m
[positive_def] Definition
⊢ ∀m. positive m ⇔
measure m ∅ = 0 ∧ ∀s. s ∈ measurable_sets m ⇒ 0 ≤ measure m s
[premeasure_def] Definition
⊢ ∀m. premeasure m ⇔ positive m ∧ countably_additive m
[sigma_finite] Definition
⊢ ∀m. sigma_finite m ⇔
∃f. exhausting_sequence (measurable_space m) f ∧
∀n. measure m (f n) < +∞
[sigma_finite_measure_space_def] Definition
⊢ ∀m. sigma_finite_measure_space m ⇔ measure_space m ∧ sigma_finite m
[subadditive_def] Definition
⊢ ∀m. subadditive m ⇔
∀s t.
s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧
s ∪ t ∈ measurable_sets m ⇒
measure m (s ∪ t) ≤ measure m s + measure m t
[ADDITIVE] Theorem
⊢ ∀m s t u.
additive m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧
DISJOINT s t ∧ u ∈ measurable_sets m ∧ u = s ∪ t ⇒
measure m u = measure m s + measure m t
[ADDITIVE_INCREASING] Theorem
⊢ ∀m. algebra (measurable_space m) ∧ positive m ∧ additive m ⇒
increasing m
[ADDITIVE_SUM] Theorem
⊢ ∀m f n.
algebra (measurable_space m) ∧ positive m ∧ additive m ∧
f ∈ (𝕌(:num) → measurable_sets m) ∧
(∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
∑ (measure m ∘ f) (count n) =
measure m (BIGUNION (IMAGE f (count n)))
[ALGEBRA_COUNTABLY_ADDITIVE_ADDITIVE] Theorem
⊢ ∀m. algebra (measurable_space m) ∧ positive m ∧
countably_additive m ⇒
additive m
[ALGEBRA_PREMEASURE_ADDITIVE] Theorem
⊢ ∀m. algebra (measurable_space m) ∧ premeasure m ⇒ additive m
[ALGEBRA_PREMEASURE_COMPL] Theorem
⊢ ∀m s.
algebra (measurable_space m) ∧ premeasure m ∧
s ∈ measurable_sets m ∧ measure m s < +∞ ⇒
measure m (m_space m DIFF s) =
measure m (m_space m) − measure m s
[ALGEBRA_PREMEASURE_COUNTABLE_INCREASING] Theorem
⊢ ∀m s f.
algebra (measurable_space m) ∧ premeasure m ∧
f ∈ (𝕌(:num) → measurable_sets m) ∧ f 0 = ∅ ∧
(∀n. f n ⊆ f (SUC n)) ∧ s = BIGUNION (IMAGE f 𝕌(:num)) ∧
s ∈ measurable_sets m ⇒
sup (IMAGE (measure m ∘ f) 𝕌(:num)) = measure m s
[ALGEBRA_PREMEASURE_COUNTABLY_SUBADDITIVE] Theorem
⊢ ∀m. algebra (measurable_space m) ∧ premeasure m ⇒
countably_subadditive m
[ALGEBRA_PREMEASURE_DIFF_SUBSET] Theorem
⊢ ∀m s t.
algebra (measurable_space m) ∧ premeasure m ∧
s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧ s ⊆ t ∧
measure m s < +∞ ⇒
measure m (t DIFF s) = measure m t − measure m s
[ALGEBRA_PREMEASURE_FINITE_ADDITIVE] Theorem
⊢ ∀m. algebra (measurable_space m) ∧ premeasure m ⇒ finite_additive m
[ALGEBRA_PREMEASURE_FINITE_SUBADDITIVE] Theorem
⊢ ∀m. algebra (measurable_space m) ∧ premeasure m ⇒
finite_subadditive m
[ALGEBRA_PREMEASURE_INCREASING] Theorem
⊢ ∀m. algebra (measurable_space m) ∧ premeasure m ⇒ increasing m
[ALGEBRA_PREMEASURE_STRONG_ADDITIVE] Theorem
⊢ ∀m s t.
algebra (measurable_space m) ∧ premeasure m ∧
s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
measure m (s ∪ t) + measure m (s ∩ t) = measure m s + measure m t
[ALGEBRA_PREMEASURE_SUBADDITIVE] Theorem
⊢ ∀m. algebra (measurable_space m) ∧ premeasure m ⇒ subadditive m
[BIGUNION_IMAGE_Q] Theorem
⊢ ∀a f.
sigma_algebra a ∧ f ∈ (ℚ꙳ → subsets a) ⇒
BIGUNION (IMAGE f ℚ꙳) ∈ subsets a
[CARATHEODORY] Theorem
⊢ ∀m0.
algebra (measurable_space m0) ∧ positive m0 ∧
countably_additive m0 ⇒
∃m. (∀s. s ∈ measurable_sets m0 ⇒ measure m s = measure m0 s) ∧
measurable_space m = sigma (m_space m0) (measurable_sets m0) ∧
measure_space m
[CARATHEODORY_RING] Theorem
⊢ ∀m0.
ring (measurable_space m0) ∧ positive m0 ∧ countably_additive m0 ⇒
∃m. (∀s. s ∈ measurable_sets m0 ⇒ measure m s = measure m0 s) ∧
measurable_space m = sigma (m_space m0) (measurable_sets m0) ∧
measure_space m
[CARATHEODORY_SEMIRING] Theorem
⊢ ∀m0.
semiring (measurable_space m0) ∧ premeasure m0 ⇒
∃m. (∀s. s ∈ measurable_sets m0 ⇒ measure m s = measure m0 s) ∧
measurable_space m = sigma (m_space m0) (measurable_sets m0) ∧
measure_space m
[COMPLETE_MEASURE_THM] Theorem
⊢ ∀m s t.
complete_measure_space m ∧ t ∈ null_set m ∧ s ⊆ t ⇒
s ∈ null_set m
[COMPLETION_STABLE] Theorem
⊢ ∀m. complete_measure_space m ⇒
space (completion m) = m_space m ∧
subsets (completion m) = measurable_sets m
[COMPLETION_STABLE'] Theorem
⊢ ∀m. complete_measure_space m ⇒ completion m = measurable_space m
[COMPLETION_SUBSET_SUBSETS] Theorem
⊢ ∀m. measure_space m ⇒ measurable_sets m ⊆ subsets (completion m)
[COUNTABLY_ADDITIVE] Theorem
⊢ ∀m s f.
countably_additive m ∧ f ∈ (𝕌(:num) → measurable_sets m) ∧
(∀i j. i ≠ j ⇒ DISJOINT (f i) (f j)) ∧
s = BIGUNION (IMAGE f 𝕌(:num)) ∧ s ∈ measurable_sets m ⇒
suminf (measure m ∘ f) = measure m s
[COUNTABLY_ADDITIVE_ADDITIVE] Theorem
⊢ ∀m. ∅ ∈ measurable_sets m ∧ positive m ∧ countably_additive m ⇒
additive m
[COUNTABLY_ADDITIVE_FINITE_ADDITIVE] Theorem
⊢ ∀m. ∅ ∈ measurable_sets m ∧ positive m ∧ countably_additive m ⇒
finite_additive m
[COUNTABLY_SUBADDITIVE] Theorem
⊢ ∀m f s.
countably_subadditive m ∧ f ∈ (𝕌(:num) → measurable_sets m) ∧
s = BIGUNION (IMAGE f 𝕌(:num)) ∧ s ∈ measurable_sets m ⇒
measure m s ≤ suminf (measure m ∘ f)
[COUNTABLY_SUBADDITIVE_FINITE_SUBADDITIVE] Theorem
⊢ ∀m. ∅ ∈ measurable_sets m ∧ positive m ∧ countably_subadditive m ⇒
finite_subadditive m
[COUNTABLY_SUBADDITIVE_SUBADDITIVE] Theorem
⊢ ∀m. ∅ ∈ measurable_sets m ∧ positive m ∧ countably_subadditive m ⇒
subadditive m
[DYNKIN_SYSTEM_DIFF_SUBSET] Theorem
⊢ ∀d s t.
dynkin_system d ∧ s ∈ subsets d ∧ t ∈ subsets d ∧ s ⊆ t ⇒
t DIFF s ∈ subsets d
[DYNKIN_SYSTEM_PREMEASURE_ADDITIVE] Theorem
⊢ ∀m. dynkin_system (measurable_space m) ∧ premeasure m ⇒ additive m
[DYNKIN_SYSTEM_PREMEASURE_FINITE_ADDITIVE] Theorem
⊢ ∀m. dynkin_system (measurable_space m) ∧ premeasure m ⇒
finite_additive m
[DYNKIN_SYSTEM_PREMEASURE_INCREASING] Theorem
⊢ ∀m. dynkin_system (measurable_space m) ∧ premeasure m ⇒
increasing m
[FINITE_ADDITIVE] Theorem
⊢ ∀m s f n.
finite_additive m ∧ (∀i. i < n ⇒ f i ∈ measurable_sets m) ∧
(∀i j. i < n ∧ j < n ∧ i ≠ j ⇒ DISJOINT (f i) (f j)) ∧
s = BIGUNION (IMAGE f (count n)) ∧ s ∈ measurable_sets m ⇒
∑ (measure m ∘ f) (count n) = measure m s
[FINITE_ADDITIVE_ALT] Theorem
⊢ ∀m s c.
positive m ∧ finite_additive m ∧ c ⊆ measurable_sets m ∧
FINITE c ∧ disjoint c ∧ BIGUNION c ∈ measurable_sets m ⇒
∑ (measure m) c = measure m (BIGUNION c)
[FINITE_IMP_SIGMA_FINITE] Theorem
⊢ ∀m. measure_space m ∧ measure m (m_space m) ≠ +∞ ⇒ sigma_finite m
[FINITE_SUBADDITIVE] Theorem
⊢ ∀m s f n.
finite_subadditive m ∧ (∀i. i < n ⇒ f i ∈ measurable_sets m) ∧
s = BIGUNION (IMAGE f (count n)) ∧ s ∈ measurable_sets m ⇒
measure m s ≤ ∑ (measure m ∘ f) (count n)
[FINITE_SUBADDITIVE_ALT] Theorem
⊢ ∀m c.
positive m ∧ finite_subadditive m ∧ c ⊆ measurable_sets m ∧
FINITE c ∧ disjoint c ∧ BIGUNION c ∈ measurable_sets m ⇒
measure m (BIGUNION c) ≤ ∑ (measure m) c
[INCREASING] Theorem
⊢ ∀m s t.
increasing m ∧ s ⊆ t ∧ s ∈ measurable_sets m ∧
t ∈ measurable_sets m ⇒
measure m s ≤ measure m t
[IN_MEASURE_PRESERVING] Theorem
⊢ ∀m1 m2 f.
f ∈ measure_preserving m1 m2 ⇔
f ∈ measurable (measurable_space m1) (measurable_space m2) ∧
∀s. s ∈ measurable_sets m2 ⇒
measure m1 (PREIMAGE f s ∩ m_space m1) = measure m2 s
[IN_NULL_SET] Theorem
⊢ ∀m s. s ∈ null_set m ⇔ null_set m s
[MEASURABLE_IF] Theorem
⊢ ∀f g M N P.
f ∈ measurable (measurable_space M) (measurable_space N) ∧
g ∈ measurable (measurable_space M) (measurable_space N) ∧
{x | x ∈ m_space M ∧ P x} ∈ measurable_sets M ∧ measure_space M ∧
sigma_algebra (measurable_space N) ⇒
(λx. if P x then f x else g x) ∈
measurable (measurable_space M) (measurable_space N)
[MEASURABLE_IF_SET] Theorem
⊢ ∀f g M N A.
f ∈ measurable (measurable_space M) (measurable_space N) ∧
g ∈ measurable (measurable_space M) (measurable_space N) ∧
A ∩ m_space M ∈ measurable_sets M ∧ measure_space M ∧
sigma_algebra (measurable_space N) ⇒
(λx. if x ∈ A then f x else g x) ∈
measurable (measurable_space M) (measurable_space N)
[MEASURABLE_POW_TO_POW] Theorem
⊢ ∀m f.
measure_space m ∧ measurable_sets m = POW (m_space m) ⇒
f ∈ measurable (measurable_space m) (𝕌(:β),POW 𝕌(:β))
[MEASURABLE_POW_TO_POW_IMAGE] Theorem
⊢ ∀m f.
measure_space m ∧ measurable_sets m = POW (m_space m) ⇒
f ∈
measurable (measurable_space m)
(IMAGE f (m_space m),POW (IMAGE f (m_space m)))
[MEASURABLE_RANGE_REDUCE] Theorem
⊢ ∀m f s.
measure_space m ∧ f ∈ measurable (measurable_space m) (s,POW s) ∧
s ≠ ∅ ⇒
f ∈
measurable (measurable_space m)
(s ∩ IMAGE f (m_space m),POW (s ∩ IMAGE f (m_space m)))
[MEASURABLE_SETS_SUBSET_SPACE] Theorem
⊢ ∀m s. measure_space m ∧ s ∈ measurable_sets m ⇒ s ⊆ m_space m
[MEASURE_ADDITIVE] Theorem
⊢ ∀m s t u.
measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧
DISJOINT s t ∧ u = s ∪ t ⇒
measure m u = measure m s + measure m t
[MEASURE_COMPL] Theorem
⊢ ∀m s.
measure_space m ∧ s ∈ measurable_sets m ∧ measure m s < +∞ ⇒
measure m (m_space m DIFF s) =
measure m (m_space m) − measure m s
[MEASURE_COMPL_SUBSET] Theorem
⊢ ∀m s t.
measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧
t ⊆ s ∧ measure m t < +∞ ⇒
measure m (s DIFF t) = measure m s − measure m t
[MEASURE_COUNTABLE_INCREASING] Theorem
⊢ ∀m s f.
measure_space m ∧ f ∈ (𝕌(:num) → measurable_sets m) ∧ f 0 = ∅ ∧
(∀n. f n ⊆ f (SUC n)) ∧ s = BIGUNION (IMAGE f 𝕌(:num)) ⇒
sup (IMAGE (measure m ∘ f) 𝕌(:num)) = measure m s
[MEASURE_COUNTABLY_ADDITIVE] Theorem
⊢ ∀m s f.
measure_space m ∧ f ∈ (𝕌(:num) → measurable_sets m) ∧
(∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ∧
s = BIGUNION (IMAGE f 𝕌(:num)) ⇒
suminf (measure m ∘ f) = measure m s
[MEASURE_DIFF_SUBSET] Theorem
⊢ ∀m s t.
measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧
t ⊆ s ∧ measure m t < +∞ ⇒
measure m (s DIFF t) = measure m s − measure m t
[MEASURE_DOWN] Theorem
⊢ ∀m0 m1.
sigma_algebra (measurable_space m0) ∧
measurable_sets m0 ⊆ measurable_sets m1 ∧
measure m0 = measure m1 ∧ measure_space m1 ⇒
measure_space m0
[MEASURE_EMPTY] Theorem
⊢ ∀m. measure_space m ⇒ measure m ∅ = 0
[MEASURE_EXTREAL_SUM_IMAGE] Theorem
⊢ ∀m s.
measure_space m ∧ s ∈ measurable_sets m ∧
(∀x. x ∈ s ⇒ {x} ∈ measurable_sets m) ∧ FINITE s ⇒
measure m s = ∑ (λx. measure m {x}) s
[MEASURE_FINITE_ADDITIVE] Theorem
⊢ ∀m. measure_space m ⇒ finite_additive m
[MEASURE_INCREASING] Theorem
⊢ ∀m s t.
measure_space m ∧ s ⊆ t ∧ s ∈ measurable_sets m ∧
t ∈ measurable_sets m ⇒
measure m s ≤ measure m t
[MEASURE_POSITIVE] Theorem
⊢ ∀m s. measure_space m ∧ s ∈ measurable_sets m ⇒ 0 ≤ measure m s
[MEASURE_PRESERVING_LIFT] Theorem
⊢ ∀m1 m2 a f.
measure_space m1 ∧ measure_space m2 ∧
measure_space (m_space m2,a,measure m2) ∧
measure m1 (m_space m1) ≠ +∞ ∧ measure m2 (m_space m2) ≠ +∞ ∧
measurable_sets m2 = subsets (sigma (m_space m2) a) ∧
f ∈ measure_preserving m1 (m_space m2,a,measure m2) ⇒
f ∈ measure_preserving m1 m2
[MEASURE_PRESERVING_SUBSET] Theorem
⊢ ∀m1 m2 a.
measure_space m1 ∧ measure_space m2 ∧
measure_space (m_space m2,a,measure m2) ∧
measure m1 (m_space m1) ≠ +∞ ∧ measure m2 (m_space m2) ≠ +∞ ∧
measurable_sets m2 = subsets (sigma (m_space m2) a) ⇒
measure_preserving m1 (m_space m2,a,measure m2) ⊆
measure_preserving m1 m2
[MEASURE_PRESERVING_UP_LIFT] Theorem
⊢ ∀m1 m2 f a.
f ∈ measure_preserving (m_space m1,a,measure m1) m2 ∧
sigma_algebra (measurable_space m1) ∧ a ⊆ measurable_sets m1 ⇒
f ∈ measure_preserving m1 m2
[MEASURE_PRESERVING_UP_SIGMA] Theorem
⊢ ∀m1 m2 a.
subset_class (m_space m1) a ∧
measurable_sets m1 = subsets (sigma (m_space m1) a) ⇒
measure_preserving (m_space m1,a,measure m1) m2 ⊆
measure_preserving m1 m2
[MEASURE_PRESERVING_UP_SUBSET] Theorem
⊢ ∀m1 m2 a.
a ⊆ measurable_sets m1 ∧ sigma_algebra (measurable_space m1) ⇒
measure_preserving (m_space m1,a,measure m1) m2 ⊆
measure_preserving m1 m2
[MEASURE_SPACE_ADDITIVE] Theorem
⊢ ∀m. measure_space m ⇒ additive m
[MEASURE_SPACE_BIGINTER] Theorem
⊢ ∀m s.
measure_space m ∧ (∀n. s n ∈ measurable_sets m) ⇒
BIGINTER (IMAGE s 𝕌(:num)) ∈ measurable_sets m
[MEASURE_SPACE_BIGUNION] Theorem
⊢ ∀m s.
measure_space m ∧ (∀n. s n ∈ measurable_sets m) ⇒
BIGUNION (IMAGE s 𝕌(:num)) ∈ measurable_sets m
[MEASURE_SPACE_CMUL] Theorem
⊢ ∀m c.
measure_space m ∧ 0 ≤ c ⇒
measure_space
(m_space m,measurable_sets m,(λa. Normal c * measure m a))
[MEASURE_SPACE_COMPL] Theorem
⊢ ∀m s.
measure_space m ∧ s ∈ measurable_sets m ⇒
m_space m DIFF s ∈ measurable_sets m
[MEASURE_SPACE_COUNTABLY_SUBADDITIVE] Theorem
⊢ ∀m. measure_space m ⇒ countably_subadditive m
[MEASURE_SPACE_DIFF] Theorem
⊢ ∀m s t.
measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
s DIFF t ∈ measurable_sets m
[MEASURE_SPACE_EMPTY_MEASURABLE] Theorem
⊢ ∀m. measure_space m ⇒ ∅ ∈ measurable_sets m
[MEASURE_SPACE_FINITE_DIFF] Theorem
⊢ ∀m s.
measure_space m ∧ s ∈ measurable_sets m ∧ measure m s ≠ +∞ ⇒
measure m (m_space m DIFF s) =
measure m (m_space m) − measure m s
[MEASURE_SPACE_FINITE_DIFF_SUBSET] Theorem
⊢ ∀m s t.
measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧
t ⊆ s ∧ measure m s ≠ +∞ ⇒
measure m (s DIFF t) = measure m s − measure m t
[MEASURE_SPACE_FINITE_MEASURE] Theorem
⊢ ∀m s.
measure_space m ∧ s ∈ measurable_sets m ∧
measure m (m_space m) ≠ +∞ ⇒
measure m s ≠ +∞
[MEASURE_SPACE_FINITE_SUBADDITIVE] Theorem
⊢ ∀m. measure_space m ⇒ finite_subadditive m
[MEASURE_SPACE_INCREASING] Theorem
⊢ ∀m. measure_space m ⇒ increasing m
[MEASURE_SPACE_INTER] Theorem
⊢ ∀m s t.
measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
s ∩ t ∈ measurable_sets m
[MEASURE_SPACE_IN_MSPACE] Theorem
⊢ ∀m s.
measure_space m ∧ s ∈ measurable_sets m ⇒
∀x. x ∈ s ⇒ x ∈ m_space m
[MEASURE_SPACE_MSPACE_MEASURABLE] Theorem
⊢ ∀m. measure_space m ⇒ m_space m ∈ measurable_sets m
[MEASURE_SPACE_POSITIVE] Theorem
⊢ ∀m. measure_space m ⇒ positive m
[MEASURE_SPACE_REDUCE] Theorem
⊢ ∀m. (m_space m,measurable_sets m,measure m) = m
[MEASURE_SPACE_RESTRICTED] Theorem
⊢ ∀m s.
measure_space m ∧ s ∈ measurable_sets m ⇒
measure_space (s,IMAGE (λt. s ∩ t) (measurable_sets m),measure m)
[MEASURE_SPACE_RESTRICTED_MEASURE] Theorem
⊢ ∀m s.
measure_space m ∧ s ∈ measurable_sets m ⇒
measure_space
(m_space m,measurable_sets m,(λa. measure m (s ∩ a)))
[MEASURE_SPACE_RESTRICTION] Theorem
⊢ ∀sp sts m sub.
measure_space (sp,sts,m) ∧ sub ⊆ sts ∧ sigma_algebra (sp,sub) ⇒
measure_space (sp,sub,m)
[MEASURE_SPACE_RESTRICTION'] Theorem
⊢ ∀m sts.
measure_space m ∧ sts ⊆ measurable_sets m ∧
sigma_algebra (m_space m,sts) ⇒
measure_space (m_space m,sts,measure m)
[MEASURE_SPACE_SIGMA_ALGEBRA] Theorem
⊢ ∀m. measure_space m ⇒ sigma_algebra (measurable_space m)
[MEASURE_SPACE_SPACE] Theorem
⊢ ∀m. measure_space m ⇒ m_space m ∈ measurable_sets m
[MEASURE_SPACE_STRONG_ADDITIVE] Theorem
⊢ ∀m s t.
measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
measure m (s ∪ t) + measure m (s ∩ t) = measure m s + measure m t
[MEASURE_SPACE_SUBADDITIVE] Theorem
⊢ ∀m. measure_space m ⇒ subadditive m
[MEASURE_SPACE_SUBSET] Theorem
⊢ ∀s s' m.
s' ⊆ s ∧ measure_space (s,POW s,m) ⇒ measure_space (s',POW s',m)
[MEASURE_SPACE_SUBSET_MSPACE] Theorem
⊢ ∀m s. measure_space m ∧ s ∈ measurable_sets m ⇒ s ⊆ m_space m
[MEASURE_SPACE_UNION] Theorem
⊢ ∀m s t.
measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
s ∪ t ∈ measurable_sets m
[MONOTONE_CONVERGENCE] Theorem
⊢ ∀m s f.
measure_space m ∧ f ∈ (𝕌(:num) → measurable_sets m) ∧
(∀n. f n ⊆ f (SUC n)) ∧ s = BIGUNION (IMAGE f 𝕌(:num)) ⇒
sup (IMAGE (measure m ∘ f) 𝕌(:num)) = measure m s
[MONOTONE_CONVERGENCE2] Theorem
⊢ ∀m f.
measure_space m ∧ f ∈ (𝕌(:num) → measurable_sets m) ∧
(∀n. f n ⊆ f (SUC n)) ⇒
sup (IMAGE (measure m ∘ f) 𝕌(:num)) =
measure m (BIGUNION (IMAGE f 𝕌(:num)))
[MONOTONE_CONVERGENCE_BIGINTER] Theorem
⊢ ∀m s f.
measure_space m ∧ f ∈ (𝕌(:num) → measurable_sets m) ∧
(∀n. measure m (f n) ≠ +∞) ∧ (∀n. f (SUC n) ⊆ f n) ∧
s = BIGINTER (IMAGE f 𝕌(:num)) ⇒
inf (IMAGE (measure m ∘ f) 𝕌(:num)) = measure m s
[MONOTONE_CONVERGENCE_BIGINTER2] Theorem
⊢ ∀m f.
measure_space m ∧ f ∈ (𝕌(:num) → measurable_sets m) ∧
(∀n. measure m (f n) ≠ +∞) ∧ (∀n. f (SUC n) ⊆ f n) ⇒
inf (IMAGE (measure m ∘ f) 𝕌(:num)) =
measure m (BIGINTER (IMAGE f 𝕌(:num)))
[NULL_SET_BIGUNION] Theorem
⊢ ∀m f.
measure_space m ∧ (∀n. f n ∈ null_set m) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ null_set m
[NULL_SET_BIGUNION'] Theorem
⊢ ∀m f.
measure_space m ∧ (∀n. null_set m (f n)) ⇒
null_set m (BIGUNION (IMAGE f 𝕌(:num)))
[NULL_SET_EMPTY] Theorem
⊢ ∀m. measure_space m ⇒ null_set m ∅
[NULL_SET_INTER] Theorem
⊢ ∀m N1 N2.
measure_space m ∧ N1 ∈ null_set m ∧ N2 ∈ null_set m ⇒
N1 ∩ N2 ∈ null_set m
[NULL_SET_INTER'] Theorem
⊢ ∀m N1 N2.
measure_space m ∧ null_set m N1 ∧ null_set m N2 ⇒
null_set m (N1 ∩ N2)
[NULL_SET_THM] Theorem
⊢ ∀m s t.
measure_space m ⇒
∅ ∈ null_set m ∧
(t ∈ null_set m ∧ s ∈ measurable_sets m ∧ s ⊆ t ⇒ s ∈ null_set m) ∧
∀f. f ∈ (𝕌(:num) → null_set m) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ null_set m
[NULL_SET_UNION] Theorem
⊢ ∀m N1 N2.
measure_space m ∧ N1 ∈ null_set m ∧ N2 ∈ null_set m ⇒
N1 ∪ N2 ∈ null_set m
[NULL_SET_UNION'] Theorem
⊢ ∀m N1 N2.
measure_space m ∧ null_set m N1 ∧ null_set m N2 ⇒
null_set m (N1 ∪ N2)
[OUTER_MEASURE_CONSTRUCTION] Theorem
⊢ ∀sp sts m u.
subset_class sp sts ∧ ∅ ∈ sts ∧ positive (sp,sts,m) ∧
u = outer_measure m (countable_covers sts) ⇒
outer_measure_space (sp,POW sp,u) ∧ (∀x. x ∈ sts ⇒ u x ≤ m x) ∧
measure_space (sp,caratheodory_sets sp u,u) ∧
∀v. outer_measure_space (sp,POW sp,v) ∧ (∀x. x ∈ sts ⇒ v x ≤ m x) ⇒
∀x. x ⊆ sp ⇒ v x ≤ u x
[OUTER_MEASURE_SPACE_FINITE_SUBADDITIVE] Theorem
⊢ ∀m. outer_measure_space m ⇒ finite_subadditive m
[OUTER_MEASURE_SPACE_POSITIVE] Theorem
⊢ ∀m. outer_measure_space m ⇒ positive m
[OUTER_MEASURE_SPACE_SUBADDITIVE] Theorem
⊢ ∀m. outer_measure_space m ⇒ subadditive m
[RING_ADDITIVE_EVERYTHING] Theorem
⊢ ∀m. ring (measurable_space m) ∧ positive m ∧ additive m ⇒
finite_additive m ∧ increasing m ∧ subadditive m ∧
finite_subadditive m
[RING_ADDITIVE_FINITE_ADDITIVE] Theorem
⊢ ∀m. ring (measurable_space m) ∧ positive m ∧ additive m ⇒
finite_additive m
[RING_ADDITIVE_INCREASING] Theorem
⊢ ∀m. ring (measurable_space m) ∧ positive m ∧ additive m ⇒
increasing m
[RING_ADDITIVE_STRONG_ADDITIVE] Theorem
⊢ ∀m s t.
ring (measurable_space m) ∧ additive m ∧ positive m ∧
s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
measure m (s ∪ t) + measure m (s ∩ t) = measure m s + measure m t
[RING_ADDITIVE_SUBADDITIVE] Theorem
⊢ ∀m. ring (measurable_space m) ∧ positive m ∧ additive m ⇒
subadditive m
[RING_PREMEASURE_ADDITIVE] Theorem
⊢ ∀m. ring (measurable_space m) ∧ premeasure m ⇒ additive m
[RING_PREMEASURE_COUNTABLE_INCREASING] Theorem
⊢ ∀m s f.
ring (measurable_space m) ∧ premeasure m ∧
f ∈ (𝕌(:num) → measurable_sets m) ∧ f 0 = ∅ ∧
(∀n. f n ⊆ f (SUC n)) ∧ s = BIGUNION (IMAGE f 𝕌(:num)) ∧
s ∈ measurable_sets m ⇒
sup (IMAGE (measure m ∘ f) 𝕌(:num)) = measure m s
[RING_PREMEASURE_COUNTABLY_SUBADDITIVE] Theorem
⊢ ∀m. ring (measurable_space m) ∧ premeasure m ⇒
countably_subadditive m
[RING_PREMEASURE_DIFF_SUBSET] Theorem
⊢ ∀m s t.
ring (measurable_space m) ∧ premeasure m ∧
s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧ s ⊆ t ∧
measure m s < +∞ ⇒
measure m (t DIFF s) = measure m t − measure m s
[RING_PREMEASURE_FINITE_ADDITIVE] Theorem
⊢ ∀m. ring (measurable_space m) ∧ premeasure m ⇒ finite_additive m
[RING_PREMEASURE_FINITE_SUBADDITIVE] Theorem
⊢ ∀m. ring (measurable_space m) ∧ premeasure m ⇒ finite_subadditive m
[RING_PREMEASURE_INCREASING] Theorem
⊢ ∀m. ring (measurable_space m) ∧ premeasure m ⇒ increasing m
[RING_PREMEASURE_STRONG_ADDITIVE] Theorem
⊢ ∀m s t.
ring (measurable_space m) ∧ premeasure m ∧
s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
measure m (s ∪ t) + measure m (s ∩ t) = measure m s + measure m t
[RING_PREMEASURE_SUBADDITIVE] Theorem
⊢ ∀m. ring (measurable_space m) ∧ premeasure m ⇒ subadditive m
[RING_SUBADDITIVE_FINITE_SUBADDITIVE] Theorem
⊢ ∀m. ring (measurable_space m) ∧ positive m ∧ subadditive m ⇒
finite_subadditive m
[SEMIRING_FINITE_ADDITIVE_EXTENSION] Theorem
⊢ ∀m0.
semiring (measurable_space m0) ∧ positive m0 ∧ finite_additive m0 ⇒
∃m. measurable_space m =
smallest_ring (m_space m0) (measurable_sets m0) ∧
(∀s. s ∈ measurable_sets m0 ⇒ measure m s = measure m0 s) ∧
positive m ∧ additive m
[SEMIRING_PREMEASURE_ADDITIVE] Theorem
⊢ ∀m. semiring (measurable_space m) ∧ premeasure m ⇒ additive m
[SEMIRING_PREMEASURE_EXTENSION] Theorem
⊢ ∀m0.
semiring (measurable_space m0) ∧ premeasure m0 ⇒
∃m. measurable_space m =
smallest_ring (m_space m0) (measurable_sets m0) ∧
(∀s. s ∈ measurable_sets m0 ⇒ measure m s = measure m0 s) ∧
premeasure m
[SEMIRING_PREMEASURE_FINITE_ADDITIVE] Theorem
⊢ ∀m. semiring (measurable_space m) ∧ premeasure m ⇒
finite_additive m
[SEMIRING_PREMEASURE_INCREASING] Theorem
⊢ ∀m. semiring (measurable_space m) ∧ premeasure m ⇒ increasing m
[SEMIRING_SIGMA_MONOTONE] Theorem
⊢ ∀sp sts u v.
semiring (sp,sts) ∧ has_exhausting_sequence (sp,sts) ∧
measure_space (sp,subsets (sigma sp sts),u) ∧
measure_space (sp,subsets (sigma sp sts),v) ∧
(∀s. s ∈ sts ⇒ u s ≤ v s ∧ v s < +∞) ⇒
∀s. s ∈ subsets (sigma sp sts) ⇒ u s ≤ v s
[SIGMA_ALGEBRA_COMPLETION] Theorem
⊢ ∀m. measure_space m ⇒ sigma_algebra (completion m)
[SIGMA_FINITE_ALT] Theorem
⊢ ∀m. measure_space m ⇒
(sigma_finite m ⇔
∃f. f ∈ (𝕌(:num) → measurable_sets m) ∧
BIGUNION (IMAGE f 𝕌(:num)) = m_space m ∧
∀n. measure m (f n) < +∞)
[SIGMA_FINITE_ALT2] Theorem
⊢ ∀m. measure_space m ⇒
(sigma_finite m ⇔
∃A. countable A ∧ A ⊆ measurable_sets m ∧
BIGUNION A = m_space m ∧ ∀a. a ∈ A ⇒ measure m a ≠ +∞)
[SIGMA_SUBSET_MEASURABLE_SETS] Theorem
⊢ ∀a m.
measure_space m ∧ a ⊆ measurable_sets m ⇒
subsets (sigma (m_space m) a) ⊆ measurable_sets m
[STRONG_MEASURE_SPACE_SUBSET] Theorem
⊢ ∀s s'.
s' ⊆ m_space s ∧ measure_space s ∧ POW s' ⊆ measurable_sets s ⇒
measure_space (s',POW s',measure s)
[SUBADDITIVE] Theorem
⊢ ∀m s t u.
subadditive m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧
u ∈ measurable_sets m ∧ u = s ∪ t ⇒
measure m u ≤ measure m s + measure m t
[UNIQUENESS_OF_MEASURE] Theorem
⊢ ∀sp sts u v.
subset_class sp sts ∧ (∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∩ t ∈ sts) ∧
sigma_finite (sp,sts,u) ∧
measure_space (sp,subsets (sigma sp sts),u) ∧
measure_space (sp,subsets (sigma sp sts),v) ∧
(∀s. s ∈ sts ⇒ u s = v s) ⇒
∀s. s ∈ subsets (sigma sp sts) ⇒ u s = v s
[UNIQUENESS_OF_MEASURE_FINITE] Theorem
⊢ ∀sp sts u v.
subset_class sp sts ∧ (∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∩ t ∈ sts) ∧
measure_space (sp,subsets (sigma sp sts),u) ∧
measure_space (sp,subsets (sigma sp sts),v) ∧ u sp = v sp ∧
u sp < +∞ ∧ (∀s. s ∈ sts ⇒ u s = v s) ⇒
∀s. s ∈ subsets (sigma sp sts) ⇒ u s = v s
[countable_covers_def] Theorem
⊢ ∀sts.
countable_covers sts =
(λa. {f | f ∈ (𝕌(:num) → sts) ∧ a ⊆ BIGUNION (IMAGE f 𝕌(:num))})
[countably_additive_alt_eq] Theorem
⊢ ∀sp M u.
countably_additive (sp,M,u) ⇔
∀A. IMAGE A 𝕌(:num) ⊆ M ⇒
disjoint_family A ⇒
BIGUNION {A i | i ∈ 𝕌(:num)} ∈ M ⇒
u (BIGUNION {A i | i ∈ 𝕌(:num)}) = suminf (u ∘ A)
[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
[finite_additivity_sufficient_for_finite_spaces] Theorem
⊢ ∀s m.
sigma_algebra s ∧ FINITE (space s) ∧
positive (space s,subsets s,m) ∧ additive (space s,subsets s,m) ⇒
measure_space (space s,subsets s,m)
[finite_additivity_sufficient_for_finite_spaces2] Theorem
⊢ ∀m. sigma_algebra (measurable_space m) ∧ FINITE (m_space m) ∧
positive m ∧ additive m ⇒
measure_space m
[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
[limsup_suminf_indicator_space] Theorem
⊢ ∀a A.
sigma_algebra a ∧ (∀n. A n ∈ subsets a) ⇒
limsup A = {x | x ∈ space a ∧ suminf (λn. 𝟙 (A n) x) = +∞}
[measure_liminf] Theorem
⊢ ∀p A.
measure_space p ∧ (∀n. A n ∈ measurable_sets p) ⇒
measure p (liminf A) =
sup (IMAGE (λm. measure p (BIGINTER {A n | m ≤ n})) 𝕌(:num))
[measure_limsup] Theorem
⊢ ∀p A.
measure_space p ∧ measure p (BIGUNION (IMAGE A 𝕌(:num))) < +∞ ∧
(∀n. A n ∈ measurable_sets p) ⇒
measure p (limsup A) =
inf (IMAGE (λm. measure p (BIGUNION {A n | m ≤ n})) 𝕌(:num))
[measure_limsup_finite] Theorem
⊢ ∀p A.
measure_space p ∧ measure p (m_space p) < +∞ ∧
(∀n. A n ∈ measurable_sets p) ⇒
measure p (limsup A) =
inf (IMAGE (λm. measure p (BIGUNION {A n | m ≤ n})) 𝕌(:num))
[measure_space_add] Theorem
⊢ ∀sp sts u v.
measure_space (sp,sts,u) ∧ measure_space (sp,sts,v) ⇒
measure_space (sp,sts,(λs. u s + v s))
[measure_space_add'] Theorem
⊢ ∀a mu nu p.
measure_space (space a,subsets a,mu) ∧
measure_space (space a,subsets a,nu) ∧
(∀s. s ∈ subsets a ⇒ p s = mu s + nu s) ⇒
measure_space (space a,subsets a,p)
[measure_space_cmul] Theorem
⊢ ∀a u v c.
measure_space (space a,subsets a,u) ∧ 0 ≤ c ∧
(∀s. s ∈ subsets a ⇒ v s = c * u s) ⇒
measure_space (space a,subsets a,v)
[measure_space_cong] Theorem
⊢ ∀sp sts u v.
(∀s. s ∈ sts ⇒ u s = v s) ⇒
(measure_space (sp,sts,u) ⇔ measure_space (sp,sts,v))
[measure_space_dirac_measure] Theorem
⊢ ∀a x. sigma_algebra a ⇒ measure_space (space a,subsets a,C 𝟙 x)
[measure_space_eq] Theorem
⊢ ∀m1 m2.
measure_space m1 ∧ m_space m2 = m_space m1 ∧
measurable_sets m2 = measurable_sets m1 ∧
(∀s. s ∈ measurable_sets m2 ⇒ measure m2 s = measure m1 s) ⇒
measure_space m2
[measure_space_eq'] Theorem
⊢ ∀m1 m2.
measure_space m1 ∧ measure_space_eq m1 m2 ⇒ measure_space m2
[measure_space_eq_comm] Theorem
⊢ ∀m1 m2. measure_space_eq m1 m2 ⇒ measure_space_eq m2 m1
[measure_space_eq_trans] Theorem
⊢ ∀m1 m2 m3.
measure_space_eq m1 m2 ∧ measure_space_eq m2 m3 ⇒
measure_space_eq m1 m3
[measure_space_measure_eq] Theorem
⊢ ∀sp sts u v.
measure_space (sp,sts,u) ∧ (∀s. s ∈ sts ⇒ u s = v s) ⇒
measure_space (sp,sts,v)
[measure_space_sum] Theorem
⊢ ∀a f m s.
FINITE s ∧ sigma_algebra a ∧
(∀i. i ∈ s ⇒ measure_space (space a,subsets a,f i)) ∧
(∀t. t ∈ subsets a ⇒ m t = ∑ (C f t) s) ⇒
measure_space (space a,subsets a,m)
[measure_space_suminf] Theorem
⊢ ∀a g m.
(∀n. measure_space (space a,subsets a,g n)) ∧
(∀s. s ∈ subsets a ⇒ m s = suminf (C g s)) ⇒
measure_space (space a,subsets a,m)
[measure_space_trivial] Theorem
⊢ ∀a. sigma_algebra a ⇒
sigma_finite_measure_space (space a,subsets a,(λs. 0))
[measure_split] Theorem
⊢ ∀r b m.
measure_space m ∧ FINITE r ∧ BIGUNION (IMAGE b r) = m_space m ∧
(∀i j. i ∈ r ∧ j ∈ r ∧ i ≠ j ⇒ DISJOINT (b i) (b j)) ∧
(∀i. i ∈ r ⇒ b i ∈ measurable_sets m) ⇒
∀a. a ∈ measurable_sets m ⇒
measure m a = ∑ (λi. measure m (a ∩ b i)) r
[null_sets] Theorem
⊢ null_set M = {N | N ∈ measurable_sets M ∧ measure M N = 0}
[positive_not_infty] Theorem
⊢ ∀m. positive m ⇒ ∀s. s ∈ measurable_sets m ⇒ measure m s ≠ −∞
[sets_eq_imp_space_eq] Theorem
⊢ ∀M M'.
measure_space M ∧ measure_space M' ∧
measurable_sets M = measurable_sets M' ⇒
m_space M = m_space M'
[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 (measurable_space m) f ∧
∀n. measure m (f n) < +∞
[sigma_finite_def] Theorem
⊢ ∀m. sigma_finite m ⇔
∃f. f ∈ (𝕌(:num) → measurable_sets m) ∧ (∀n. f n ⊆ f (SUC n)) ∧
BIGUNION (IMAGE f 𝕌(:num)) = m_space m ∧
∀n. measure m (f n) < +∞
[sigma_finite_disjoint] Theorem
⊢ ∀m. measure_space m ∧ sigma_finite m ⇒
∃A. IMAGE A 𝕌(:num) ⊆ measurable_sets m ∧
BIGUNION {A i | i ∈ 𝕌(:num)} = m_space m ∧
(∀i. measure m (A i) ≠ +∞) ∧ disjoint_family A
[sigma_finite_has_exhausting_sequence] Theorem
⊢ ∀sp sts u.
sigma_finite (sp,sts,u) ⇒ has_exhausting_sequence (sp,sts)
[sigma_finite_thm] Theorem
⊢ ∀m. measure_space m ∧ sigma_finite m ⇒
∃A. IMAGE A 𝕌(:num) ⊆ measurable_sets m ∧
BIGUNION {A i | i ∈ 𝕌(:num)} = m_space m ∧
∀i. measure m (A i) ≠ +∞
*)
end
HOL 4, Trindemossen-1