Theory "util_prob"

Signature

Definitions

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

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

IN_PAIR

⊢ ∀x X Y. x ∈ pair X Y ⇔ FST x ∈ X ∧ SND x ∈ Y

PAIR_UNIV

⊢ pair 𝕌(:α) 𝕌(:β) = 𝕌(:α # β)

PAIRED_BETA_THM

⊢ ∀f z. UNCURRY f z = f (FST z) (SND z)

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 x⁻¹ = -lg x

logr_inv

⊢ ∀b x. 0 < x ⇒ logr b 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 x⁻¹

neg_logr

⊢ ∀b x. 0 < x ⇒ -logr b x = logr b x⁻¹

lg_pow

⊢ ∀n. lg (2 pow n) = &n

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}))

K_PARTIAL

⊢ ∀x. K x = (λz. x)

IN_o

⊢ ∀x f s. x ∈ s ∘ f ⇔ f x ∈ s

IN_PROD_SETS

⊢ ∀s a b. s ∈ prod_sets a b ⇔ ∃t u. s = t × u ∧ t ∈ a ∧ u ∈ b

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 = ∅

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}

GBIGUNION_IMAGE

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

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_R

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

SUMS_ZERO

⊢ K 0 sums 0

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 ∘ 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

MINIMAL_EXISTS_IMP

⊢ ∀P. (∃n. P n) ⇒ ∃m. P m ∧ ∀n. n < m ⇒ ¬P n

MINIMAL_EQ_IMP

⊢ ∀m p. p m ∧ (∀n. n < m ⇒ ¬p n) ⇒ m = minimal p

MINIMAL_SUC

⊢ ∀n p.
      SUC n = minimal p ∧ p (SUC n) ⇔ ¬p 0 ∧ n = minimal (p ∘ SUC) ∧ p (SUC n)

MINIMAL_EQ

⊢ ∀p m. p m ∧ m = minimal p ⇔ p m ∧ ∀n. n < m ⇒ ¬p n

MINIMAL_SUC_IMP

⊢ ∀n p. p (SUC n) ∧ ¬p 0 ∧ n = minimal (p ∘ SUC) ⇒ SUC n = minimal p