Theory "util_prob"

Signature

Definitions

FUNSET_def

|- ∀P Q. P -> Q = (λf. ∀x. x ∈ P ⇒ f x ∈ Q)

DFUNSET_def

|- ∀P Q. P --> Q = (λf. ∀x. x ∈ P ⇒ f x ∈ Q x)

pair_def

|- ∀X Y. pair X Y = (λ(x,y). x ∈ X ∧ y ∈ Y)

powr_def

|- ∀x a. x powr a = exp (a * ln x)

logr_def

|- ∀a x. logr a x = ln x / ln a

lg_def

|- ∀x. lg x = logr 2 x

countable_def

|- ∀s. countable s ⇔ ∃f. ∀x. x ∈ s ⇒ ∃n. f n = x

enumerate_def

|- ∀s. enumerate s = @f. BIJ f 𝕌(:num) s

schroeder_close_def

|- ∀f s x. schroeder_close f s x ⇔ ∃n. x ∈ FUNPOW (IMAGE f) n s

PREIMAGE_def

|- ∀f s. PREIMAGE f s = {x | f x ∈ s}

prod_sets_def

|- ∀a b. prod_sets a b = {s × t | s ∈ a ∧ t ∈ b}

minimal_def

|- ∀p. minimal p = @n. p n ∧ ∀m. m < n ⇒ ¬p m

Theorems

EQ_T_IMP

|- ∀x. x ⇔ T ⇒ x

EQ_SUBSET_SUBSET

|- ∀s t. (s = t) ⇒ s ⊆ t ∧ t ⊆ s

IN_EQ_UNIV_IMP

|- ∀s. (s = 𝕌(:α)) ⇒ ∀v. v ∈ s

IN_FUNSET

|- ∀f P Q. f ∈ (P -> Q) ⇔ ∀x. x ∈ P ⇒ f x ∈ Q

IN_DFUNSET

|- ∀f P Q. f ∈ P --> Q ⇔ ∀x. x ∈ P ⇒ f x ∈ Q x

IN_PAIR

|- ∀x X Y. x ∈ pair X Y ⇔ FST x ∈ X ∧ SND x ∈ Y

FUNSET_THM

|- ∀s t f x. f ∈ (s -> t) ∧ x ∈ s ⇒ f x ∈ t

UNIV_FUNSET_UNIV

|- 𝕌(:α) -> 𝕌(:β) = 𝕌(:α -> β)

FUNSET_DFUNSET

|- ∀x y. x -> y = x --> K y

PAIR_UNIV

|- pair 𝕌(:α) 𝕌(:β) = 𝕌(:α # β)

SUBSET_INTER

|- ∀s t u. s ⊆ t ∩ u ⇔ s ⊆ t ∧ s ⊆ u

K_SUBSET

|- ∀x y. K x ⊆ y ⇔ ¬x ∨ 𝕌(:α) ⊆ y

SUBSET_K

|- ∀x y. x ⊆ K y ⇔ x ⊆ ∅ ∨ y

SUBSET_THM

|- ∀P Q. P ⊆ Q ⇒ ∀x. x ∈ P ⇒ x ∈ Q

PAIRED_BETA_THM

|- ∀f z. UNCURRY f z = f (FST z) (SND z)

EMPTY_FUNSET

|- ∀s. ∅ -> s = 𝕌(:α -> β)

FUNSET_EMPTY

|- ∀s f. f ∈ (s -> ∅) ⇔ (s = ∅)

MAX_LE_X

|- ∀m n k. MAX m n ≤ k ⇔ m ≤ k ∧ n ≤ k

X_LE_MAX

|- ∀m n k. k ≤ MAX m n ⇔ k ≤ m ∨ k ≤ n

TRANSFORM_2D_NUM

|- ∀P. (∀m n. P m n ⇒ P n m) ∧ (∀m n. P m (m + n)) ⇒ ∀m n. P m n

TRIANGLE_2D_NUM

|- ∀P. (∀d n. P n (d + n)) ⇒ ∀m n. m ≤ n ⇒ P m n

lg_1

|- lg 1 = 0

logr_1

|- ∀b. logr b 1 = 0

lg_nonzero

|- ∀x. x ≠ 0 ∧ 0 ≤ x ⇒ (lg x ≠ 0 ⇔ x ≠ 1)

lg_mul

|- ∀x y. 0 < x ∧ 0 < y ⇒ (lg (x * y) = lg x + lg y)

logr_mul

|- ∀b x y. 0 < x ∧ 0 < y ⇒ (logr b (x * y) = logr b x + logr b y)

lg_2

|- lg 2 = 1

lg_inv

|- ∀x. 0 < x ⇒ (lg (inv x) = -lg x)

logr_inv

|- ∀b x. 0 < x ⇒ (logr b (inv x) = -logr b x)

logr_div

|- ∀b x y. 0 < x ∧ 0 < y ⇒ (logr b (x / y) = logr b x − logr b y)

neg_lg

|- ∀x. 0 < x ⇒ (-lg x = lg (inv x))

neg_logr

|- ∀b x. 0 < x ⇒ (-logr b x = logr b (inv x))

lg_pow

|- ∀n. lg (2 pow n) = &n

SCHROEDER_CLOSE

|- ∀f s. x ∈ schroeder_close f s ⇔ ∃n. x ∈ FUNPOW (IMAGE f) n s

SCHROEDER_CLOSED

|- ∀f s. IMAGE f (schroeder_close f s) ⊆ schroeder_close f s

SCHROEDER_CLOSE_SUBSET

|- ∀f s. s ⊆ schroeder_close f s

SCHROEDER_CLOSE_SET

|- ∀f s t. f ∈ (s -> s) ∧ t ⊆ s ⇒ schroeder_close f t ⊆ s

SCHROEDER_BERNSTEIN_AUTO

|- ∀s t. t ⊆ s ∧ (∃f. INJ f s t) ⇒ ∃g. BIJ g s t

INJ_IMAGE_BIJ

|- ∀s f. (∃t. INJ f s t) ⇒ BIJ f s (IMAGE f s)

BIJ_SYM_IMP

|- ∀s t. (∃f. BIJ f s t) ⇒ ∃g. BIJ g t s

BIJ_SYM

|- ∀s t. (∃f. BIJ f s t) ⇔ ∃g. BIJ g t s

BIJ_TRANS

|- ∀s t u. (∃f. BIJ f s t) ∧ (∃g. BIJ g t u) ⇒ ∃h. BIJ h s u

SCHROEDER_BERNSTEIN

|- ∀s t. (∃f. INJ f s t) ∧ (∃g. INJ g t s) ⇒ ∃h. BIJ h s t

SURJ_IMP_INJ

|- ∀s t. (∃f. SURJ f s t) ⇒ ∃g. INJ g t s

BIJ_INJ_SURJ

|- ∀s t. (∃f. INJ f s t) ∧ (∃g. SURJ g s t) ⇒ ∃h. BIJ h s t

BIJ_INV

|- ∀f s t.
     BIJ f s t ⇒
     ∃g.
       BIJ g t s ∧ (∀x. x ∈ s ⇒ ((g o f) x = x)) ∧ ∀x. x ∈ t ⇒ ((f o g) x = x)

NUM_2D_BIJ

|- ∃f. BIJ f (𝕌(:num) × 𝕌(:num)) 𝕌(:num)

NUM_2D_BIJ_INV

|- ∃f. BIJ f 𝕌(:num) (𝕌(:num) × 𝕌(:num))

NUM_2D_BIJ_NZ

|- ∃f. BIJ f (𝕌(:num) × (𝕌(:num) DIFF {0})) 𝕌(:num)

NUM_2D_BIJ_NZ_INV

|- ∃f. BIJ f 𝕌(:num) (𝕌(:num) × (𝕌(:num) DIFF {0}))

NUM_2D_BIJ_NZ_ALT

|- ∃f. BIJ f (𝕌(:num) × 𝕌(:num)) (𝕌(:num) DIFF {0})

NUM_2D_BIJ_NZ_ALT_INV

|- ∃f. BIJ f (𝕌(:num) DIFF {0}) (𝕌(:num) × 𝕌(:num))

NUM_2D_BIJ_NZ_ALT2

|- ∃f. BIJ f ((𝕌(:num) DIFF {0}) × (𝕌(:num) DIFF {0})) 𝕌(:num)

NUM_2D_BIJ_NZ_ALT2_INV

|- ∃f. BIJ f 𝕌(:num) ((𝕌(:num) DIFF {0}) × (𝕌(:num) DIFF {0}))

BIGUNION_PAIR

|- ∀s t. BIGUNION {s; t} = s ∪ t

FINITE_COUNTABLE

|- ∀s. FINITE s ⇒ countable s

BIJ_NUM_COUNTABLE

|- ∀s. (∃f. BIJ f 𝕌(:num) s) ⇒ countable s

COUNTABLE_EMPTY

|- countable ∅

COUNTABLE_IMAGE

|- ∀s f. countable s ⇒ countable (IMAGE f s)

COUNTABLE_BIGUNION

|- ∀c. countable c ∧ (∀s. s ∈ c ⇒ countable s) ⇒ countable (BIGUNION c)

COUNTABLE_UNION

|- ∀s t. countable s ∧ countable t ⇒ countable (s ∪ t)

FINITE_INJ

|- ∀f s t. INJ f s t ∧ FINITE t ⇒ FINITE s

INFINITE_INJ

|- ∀f s t. INJ f s t ∧ INFINITE s ⇒ INFINITE t

ENUMERATE

|- ∀s. (∃f. BIJ f 𝕌(:num) s) ⇔ BIJ (enumerate s) 𝕌(:num) s

FINITE_REST

|- ∀s. FINITE (REST s) ⇔ FINITE s

EXPLICIT_ENUMERATE_MONO

|- ∀n s. FUNPOW REST n s ⊆ s

EXPLICIT_ENUMERATE_NOT_EMPTY

|- ∀n s. INFINITE s ⇒ FUNPOW REST n s ≠ ∅

INFINITE_EXPLICIT_ENUMERATE

|- ∀s. INFINITE s ⇒ INJ (λn. CHOICE (FUNPOW REST n s)) 𝕌(:num) s

COUNTABLE_ALT

|- ∀s. countable s ⇔ FINITE s ∨ BIJ (enumerate s) 𝕌(:num) s

DISJOINT_COUNT

|- ∀f.
     (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
     ∀n. DISJOINT (f n) (BIGUNION (IMAGE f (count n)))

K_PARTIAL

|- ∀x. K x = (λz. x)

IN_o

|- ∀x f s. x ∈ s o f ⇔ f x ∈ s

PREIMAGE_ALT

|- ∀f s. PREIMAGE f s = s o f

IN_PREIMAGE

|- ∀f s x. x ∈ PREIMAGE f s ⇔ f x ∈ s

IN_BIGUNION_IMAGE

|- ∀f s y. y ∈ BIGUNION (IMAGE f s) ⇔ ∃x. x ∈ s ∧ y ∈ f x

IN_BIGINTER_IMAGE

|- ∀x f s. x ∈ BIGINTER (IMAGE f s) ⇔ ∀y. y ∈ s ⇒ x ∈ f y

PREIMAGE_EMPTY

|- ∀f. PREIMAGE f ∅ = ∅

PREIMAGE_UNIV

|- ∀f. PREIMAGE f 𝕌(:β) = 𝕌(:α)

PREIMAGE_COMPL

|- ∀f s. PREIMAGE f (COMPL s) = COMPL (PREIMAGE f s)

PREIMAGE_UNION

|- ∀f s t. PREIMAGE f (s ∪ t) = PREIMAGE f s ∪ PREIMAGE f t

PREIMAGE_INTER

|- ∀f s t. PREIMAGE f (s ∩ t) = PREIMAGE f s ∩ PREIMAGE f t

PREIMAGE_BIGUNION

|- ∀f s. PREIMAGE f (BIGUNION s) = BIGUNION (IMAGE (PREIMAGE f) s)

PREIMAGE_COMP

|- ∀f g s. PREIMAGE f (PREIMAGE g s) = PREIMAGE (g o f) s

PREIMAGE_DIFF

|- ∀f s t. PREIMAGE f (s DIFF t) = PREIMAGE f s DIFF PREIMAGE f t

PREIMAGE_I

|- PREIMAGE I = I

IMAGE_I

|- IMAGE I = I

PREIMAGE_K

|- ∀x s. PREIMAGE (K x) s = if x ∈ s then 𝕌(:β) else ∅

PREIMAGE_DISJOINT

|- ∀f s t. DISJOINT s t ⇒ DISJOINT (PREIMAGE f s) (PREIMAGE f t)

PREIMAGE_SUBSET

|- ∀f s t. s ⊆ t ⇒ PREIMAGE f s ⊆ PREIMAGE f t

SUBSET_ADD

|- ∀f n d. (∀n. f n ⊆ f (SUC n)) ⇒ f n ⊆ f (n + d)

DISJOINT_DIFFS

|- ∀f m n.
     (∀n. f n ⊆ f (SUC n)) ∧ (∀n. g n = f (SUC n) DIFF f n) ∧ m ≠ n ⇒
     DISJOINT (g m) (g n)

IMAGE_IMAGE

|- ∀f g s. IMAGE f (IMAGE g s) = IMAGE (f o g) s

IN_PROD_SETS

|- ∀s a b. s ∈ prod_sets a b ⇔ ∃t u. (s = t × u) ∧ t ∈ a ∧ u ∈ b

PREIMAGE_CROSS

|- ∀f a b. PREIMAGE f (a × b) = PREIMAGE (FST o f) a ∩ PREIMAGE (SND o f) b

FUNSET_INTER

|- ∀a b c. a -> b ∩ c = (a -> b) ∩ (a -> c)

UNIV_NEQ_EMPTY

|- 𝕌(:α) ≠ ∅

COUNTABLE_NUM

|- ∀s. countable s

COUNTABLE_IMAGE_NUM

|- ∀f s. countable (IMAGE f s)

COUNTABLE_ENUM

|- ∀c. countable c ⇔ (c = ∅) ∨ ∃f. c = IMAGE f 𝕌(:num)

BIGUNION_IMAGE_UNIV

|- ∀f N.
     (∀n. N ≤ n ⇒ (f n = ∅)) ⇒
     (BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE f (count N)))

BIJ_ALT

|- ∀f s t. BIJ f s t ⇔ f ∈ (s -> t) ∧ ∀y::t. ∃!x::s. y = f x

BIJ_FINITE_SUBSET

|- ∀f s t. BIJ f 𝕌(:num) s ∧ FINITE t ∧ t ⊆ s ⇒ ∃N. ∀n. N ≤ n ⇒ f n ∉ t

NUM_2D_BIJ_SMALL_SQUARE

|- ∀f k.
     BIJ f 𝕌(:num) (𝕌(:num) × 𝕌(:num)) ⇒
     ∃N. count k × count k ⊆ IMAGE f (count N)

NUM_2D_BIJ_BIG_SQUARE

|- ∀f N.
     BIJ f 𝕌(:num) (𝕌(:num) × 𝕌(:num)) ⇒
     ∃k. IMAGE f (count N) ⊆ count k × count k

finite_enumeration_of_sets_has_max_non_empty

|- ∀f s.
     FINITE s ∧ (∀x. f x ∈ s) ∧ (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
     ∃N. ∀n. n ≥ N ⇒ (f n = ∅)

SUBSET_INTER1

|- ∀s t. s ⊆ t ⇒ (s ∩ t = s)

SUBSET_INTER2

|- ∀s t. s ⊆ t ⇒ (t ∩ s = s)

DIFF_DIFF_SUBSET

|- ∀s t. t ⊆ s ⇒ (s DIFF (s DIFF t) = t)

BIGINTER_SUBSET

|- ∀sp s. (∀t. t ∈ s ⇒ t ⊆ sp) ∧ s ≠ ∅ ⇒ BIGINTER s ⊆ sp

DIFF_BIGINTER1

|- ∀sp s. sp DIFF BIGINTER s = BIGUNION (IMAGE (λu. sp DIFF u) s)

DIFF_BIGINTER

|- ∀sp s.
     (∀t. t ∈ s ⇒ t ⊆ sp) ∧ s ≠ ∅ ⇒
     (BIGINTER s = sp DIFF BIGUNION (IMAGE (λu. sp DIFF u) s))

DIFF_INTER

|- ∀s t g. (s DIFF t) ∩ g = s ∩ g DIFF t

DIFF_INTER2

|- ∀s t. s DIFF t ∩ s = s DIFF t

PREIMAGE_COMPL_INTER

|- ∀f t sp. PREIMAGE f (COMPL t) ∩ sp = sp DIFF PREIMAGE f t

PREIMAGE_REAL_COMPL1

|- ∀c. COMPL {x | c < x} = {x | x ≤ c}

PREIMAGE_REAL_COMPL2

|- ∀c. COMPL {x | c ≤ x} = {x | x < c}

PREIMAGE_REAL_COMPL3

|- ∀c. COMPL {x | x ≤ c} = {x | c < x}

PREIMAGE_REAL_COMPL4

|- ∀c. COMPL {x | x < c} = {x | c ≤ x}

ELT_IN_DELETE

|- ∀x s. x ∉ s DELETE x

DELETE_THEN_INSERT

|- ∀s (x::s). x INSERT s DELETE x = s

BIJ_INSERT

|- ∀f e s t.
     e ∉ s ∧ BIJ f (e INSERT s) t ⇒
     ∃u. (f e INSERT u = t) ∧ f e ∉ u ∧ BIJ f s u

FINITE_BIJ

|- ∀f s t. FINITE s ∧ BIJ f s t ⇒ FINITE t ∧ (CARD s = CARD t)

FINITE_BIJ_COUNT

|- ∀s. FINITE s ⇔ ∃c n. BIJ c (count n) s

GBIGUNION_IMAGE

|- ∀s p n. {s | ∃n. p s n} = BIGUNION (IMAGE (λn. {s | p s n}) 𝕌(:γ))

DISJOINT_ALT

|- ∀s t. DISJOINT s t ⇔ ∀x. x ∈ s ⇒ x ∉ t

DISJOINT_DIFF

|- ∀s t. DISJOINT t (s DIFF t) ∧ DISJOINT (s DIFF t) t

COUNTABLE_COUNT

|- ∀n. countable (count n)

COUNTABLE_SUBSET

|- ∀s t. s ⊆ t ∧ countable t ⇒ countable s

LT_SUC

|- ∀a b. a < SUC b ⇔ a < b ∨ (a = b)

LE_SUC

|- ∀a b. a ≤ SUC b ⇔ a ≤ b ∨ (a = SUC b)

HALF_POS

|- 0 < 1 / 2

HALF_LT_1

|- 1 / 2 < 1

HALF_CANCEL

|- 2 * (1 / 2) = 1

X_HALF_HALF

|- ∀x. 1 / 2 * x + 1 / 2 * x = x

ONE_MINUS_HALF

|- 1 − 1 / 2 = 1 / 2

POW_HALF_POS

|- ∀n. 0 < (1 / 2) pow n

POW_HALF_SMALL

|- ∀e. 0 < e ⇒ ∃n. (1 / 2) pow n < e

POW_HALF_MONO

|- ∀m n. m ≤ n ⇒ (1 / 2) pow n ≤ (1 / 2) pow m

REAL_LE_LT_MUL

|- ∀x y. 0 ≤ x ∧ 0 < y ⇒ 0 ≤ x * y

REAL_LT_LE_MUL

|- ∀x y. 0 < x ∧ 0 ≤ y ⇒ 0 ≤ x * y

REAL_MUL_IDEMPOT

|- ∀r. (r * r = r) ⇔ (r = 0) ∨ (r = 1)

REAL_SUP_LE_X

|- ∀P x. (∃r. P r) ∧ (∀r. P r ⇒ r ≤ x) ⇒ sup P ≤ x

REAL_X_LE_SUP

|- ∀P x. (∃r. P r) ∧ (∃z. ∀r. P r ⇒ r ≤ z) ∧ (∃r. P r ∧ x ≤ r) ⇒ x ≤ sup P

INF_DEF_ALT

|- ∀p. inf p = -sup (λr. -r ∈ p)

LE_INF

|- ∀p r. (∃x. x ∈ p) ∧ (∀x. x ∈ p ⇒ r ≤ x) ⇒ r ≤ inf p

INF_LE

|- ∀p r. (∃z. ∀x. x ∈ p ⇒ z ≤ x) ∧ (∃x. x ∈ p ∧ x ≤ r) ⇒ inf p ≤ r

INF_GREATER

|- ∀p z. (∃x. x ∈ p) ∧ inf p < z ⇒ ∃x. x ∈ p ∧ x < z

INF_CLOSE

|- ∀p e. (∃x. x ∈ p) ∧ 0 < e ⇒ ∃x. x ∈ p ∧ x < inf p + e

INCREASING_SEQ

|- ∀f l.
     (∀n. f n ≤ f (SUC n)) ∧ (∀n. f n ≤ l) ∧ (∀e. 0 < e ⇒ ∃n. l < f n + e) ⇒
     f --> l

SEQ_SANDWICH

|- ∀f g h l. f --> l ∧ h --> l ∧ (∀n. f n ≤ g n ∧ g n ≤ h n) ⇒ g --> l

SER_POS

|- ∀f. summable f ∧ (∀n. 0 ≤ f n) ⇒ 0 ≤ suminf f

SER_POS_MONO

|- ∀f. (∀n. 0 ≤ f n) ⇒ mono (λn. sum (0,n) f)

POS_SUMMABLE

|- ∀f. (∀n. 0 ≤ f n) ∧ (∃x. ∀n. sum (0,n) f ≤ x) ⇒ summable f

SUMMABLE_LE

|- ∀f x. summable f ∧ (∀n. sum (0,n) f ≤ x) ⇒ suminf f ≤ x

SUMS_EQ

|- ∀f x. f sums x ⇔ summable f ∧ (suminf f = x)

SUMINF_POS

|- ∀f. (∀n. 0 ≤ f n) ∧ summable f ⇒ 0 ≤ suminf f

SUM_PICK

|- ∀n k x. sum (0,n) (λm. if m = k then x else 0) = if k < n then x else 0

SUM_LT

|- ∀f g m n.
     (∀r. m ≤ r ∧ r < n + m ⇒ f r < g r) ∧ 0 < n ⇒ sum (m,n) f < sum (m,n) g

SUM_CONST

|- ∀n r. sum (0,n) (K r) = &n * r

SUMINF_ADD

|- ∀f g.
     summable f ∧ summable g ⇒
     summable (λn. f n + g n) ∧ (suminf f + suminf g = suminf (λn. f n + g n))

SUMINF_2D

|- ∀f g h.
     (∀m n. 0 ≤ f m n) ∧ (∀n. f n sums g n) ∧ summable g ∧
     BIJ h 𝕌(:num) (𝕌(:num) × 𝕌(:num)) ⇒
     UNCURRY f o h sums suminf g

POW_HALF_SER

|- (λn. (1 / 2) pow (n + 1)) sums 1

SER_POS_COMPARE

|- ∀f g.
     (∀n. 0 ≤ f n) ∧ summable g ∧ (∀n. f n ≤ g n) ⇒
     summable f ∧ suminf f ≤ suminf g

MINIMAL_EXISTS0

|- (∃n. P n) ⇔ ∃n. P n ∧ ∀m. m < n ⇒ ¬P m

MINIMAL_EXISTS

|- ∀P. (∃n. P n) ⇔ P (minimal P) ∧ ∀n. n < minimal P ⇒ ¬P n