Structure real_sigmaTheory
signature real_sigmaTheory =
sig
type thm = Thm.thm
(* Definitions *)
val REAL_PROD_IMAGE_DEF : thm
val REAL_SUM_IMAGE_DEF : thm
val concave_fn : thm
val convex_fn : thm
val indicator : thm
val polynomial_function : thm
val pos_concave_fn : thm
val pos_convex_fn : thm
val product : thm
val sum_def : thm
(* Theorems *)
val ABS_LE_0 : thm
val ABS_LE_HALF_POW2 : thm
val CARD_EQ_SUM : thm
val DROP_INDICATOR : thm
val DROP_INDICATOR_ABS_LE_1 : thm
val DROP_INDICATOR_LE_1 : thm
val DROP_INDICATOR_POS_LE : thm
val FINITE_REAL_INTERVAL : thm
val INDICATOR_COMPLEMENT : thm
val INDICATOR_EMPTY : thm
val INF : thm
val INF_CLOSE : thm
val INF_EQ : thm
val INF_FINITE : thm
val INF_FINITE_LEMMA : thm
val INF_GREATER : thm
val INF_INSERT_FINITE : thm
val INF_LE : thm
val INF_SING : thm
val INF_UNIQUE_FINITE : thm
val ITERATE_NONZERO_IMAGE_LEMMA : thm
val LE_INF : thm
val LOWER_BOUND_FINITE_SET_REAL : thm
val MONOIDAL_REAL_ADD : thm
val MONOIDAL_REAL_MUL : thm
val NESTED_REAL_SUM_IMAGE_REVERSE : thm
val NEUTRAL_REAL_ADD : thm
val NEUTRAL_REAL_MUL : thm
val PERMUTES_IN_NUMSEG : thm
val POLYNOMIAL_FUNCTION_ADD : thm
val POLYNOMIAL_FUNCTION_CONST : thm
val POLYNOMIAL_FUNCTION_FINITE_ROOTS : thm
val POLYNOMIAL_FUNCTION_ID : thm
val POLYNOMIAL_FUNCTION_INDUCT : thm
val POLYNOMIAL_FUNCTION_LMUL : thm
val POLYNOMIAL_FUNCTION_MUL : thm
val POLYNOMIAL_FUNCTION_NEG : thm
val POLYNOMIAL_FUNCTION_POW : thm
val POLYNOMIAL_FUNCTION_RMUL : thm
val POLYNOMIAL_FUNCTION_SUB : thm
val POLYNOMIAL_FUNCTION_SUM : thm
val POLYNOMIAL_FUNCTION_o : thm
val POW_NEG_ODD : thm
val POW_POS_EVEN : thm
val PRODUCT_ABS : thm
val PRODUCT_ADD_SPLIT : thm
val PRODUCT_CLAUSES : thm
val PRODUCT_CLAUSES_LEFT : thm
val PRODUCT_CLAUSES_NUMSEG : thm
val PRODUCT_CLAUSES_RIGHT : thm
val PRODUCT_CLOSED : thm
val PRODUCT_CONG : thm
val PRODUCT_CONST : thm
val PRODUCT_CONST_NUMSEG : thm
val PRODUCT_CONST_NUMSEG_1 : thm
val PRODUCT_DELETE : thm
val PRODUCT_DELTA : thm
val PRODUCT_DIV : thm
val PRODUCT_DIV_NUMSEG : thm
val PRODUCT_EQ : thm
val PRODUCT_EQ_0 : thm
val PRODUCT_EQ_0_COUNT : thm
val PRODUCT_EQ_0_NUMSEG : thm
val PRODUCT_EQ_1 : thm
val PRODUCT_EQ_1_COUNT : thm
val PRODUCT_EQ_1_NUMSEG : thm
val PRODUCT_EQ_COUNT : thm
val PRODUCT_EQ_NUMSEG : thm
val PRODUCT_IMAGE : thm
val PRODUCT_INV : thm
val PRODUCT_LE : thm
val PRODUCT_LE_1 : thm
val PRODUCT_LE_NUMSEG : thm
val PRODUCT_MUL : thm
val PRODUCT_MUL_COUNT : thm
val PRODUCT_MUL_GEN : thm
val PRODUCT_MUL_NUMSEG : thm
val PRODUCT_NEG : thm
val PRODUCT_NEG_NUMSEG : thm
val PRODUCT_NEG_NUMSEG_1 : thm
val PRODUCT_OFFSET : thm
val PRODUCT_ONE : thm
val PRODUCT_PAIR : thm
val PRODUCT_PERMUTE : thm
val PRODUCT_PERMUTE_COUNT : thm
val PRODUCT_PERMUTE_NUMSEG : thm
val PRODUCT_POS_LE : thm
val PRODUCT_POS_LE_NUMSEG : thm
val PRODUCT_POS_LT : thm
val PRODUCT_POS_LT_NUMSEG : thm
val PRODUCT_SING : thm
val PRODUCT_SING_NUMSEG : thm
val PRODUCT_SUPERSET : thm
val PRODUCT_SUPPORT : thm
val PRODUCT_UNION : thm
val REAL_ABS_INF_LE : thm
val REAL_ABS_SUP_LE : thm
val REAL_ARCH_INV' : thm
val REAL_ARCH_INV_SUC : thm
val REAL_BOUNDS_LT : thm
val REAL_COMPLETE : thm
val REAL_EQ_SQUARE_ABS : thm
val REAL_HALF : thm
val REAL_IMP_LE_SUP' : thm
val REAL_IMP_SUP_LE' : thm
val REAL_INF_ASCLOSE : thm
val REAL_INF_BOUNDS : thm
val REAL_INF_LE' : thm
val REAL_INF_LE_FINITE : thm
val REAL_INF_LT_FINITE : thm
val REAL_INF_UNIQUE : thm
val REAL_LE_BETWEEN : thm
val REAL_LE_INF : thm
val REAL_LE_INF_FINITE : thm
val REAL_LE_INF_SUBSET : thm
val REAL_LE_LDIV_CANCEL : thm
val REAL_LE_LDIV_EQ_NEG : thm
val REAL_LE_LT_MUL : thm
val REAL_LE_MUL' : thm
val REAL_LE_MUL_EPSILON : thm
val REAL_LE_RDIV_EQ_NEG : thm
val REAL_LE_SQUARE_ABS : thm
val REAL_LE_SUP' : thm
val REAL_LE_SUP_EQ : thm
val REAL_LE_SUP_FINITE : thm
val REAL_LT_BETWEEN : thm
val REAL_LT_INF_FINITE : thm
val REAL_LT_INV2 : thm
val REAL_LT_LCANCEL_IMP : thm
val REAL_LT_LDIV_CANCEL : thm
val REAL_LT_LE_MUL : thm
val REAL_LT_LMUL' : thm
val REAL_LT_LMUL_0_NEG : thm
val REAL_LT_LMUL_NEG_0 : thm
val REAL_LT_LMUL_NEG_0_NEG : thm
val REAL_LT_MAX_BETWEEN : thm
val REAL_LT_MUL' : thm
val REAL_LT_POW2 : thm
val REAL_LT_RDIV_EQ_NEG : thm
val REAL_LT_RMUL' : thm
val REAL_LT_RMUL_0_NEG : thm
val REAL_LT_RMUL_NEG_0 : thm
val REAL_LT_RMUL_NEG_0_NEG : thm
val REAL_LT_SUP_FINITE : thm
val REAL_MAX_REDUCE : thm
val REAL_MIN_LE_BETWEEN : thm
val REAL_MIN_REDUCE : thm
val REAL_MUL_IDEMPOT : thm
val REAL_MUL_SUM : thm
val REAL_MUL_SUM_NUMSEG : thm
val REAL_NEG_NZ : thm
val REAL_OF_NUM_GE : thm
val REAL_OF_NUM_NPRODUCT : thm
val REAL_OF_NUM_SUM : thm
val REAL_OF_NUM_SUM_NUMSEG : thm
val REAL_POLYFUN_EQ_0 : thm
val REAL_POLYFUN_EQ_CONST : thm
val REAL_POLYFUN_FINITE_ROOTS : thm
val REAL_POLYFUN_ROOTBOUND : thm
val REAL_PROD_IMAGE_EMPTY : thm
val REAL_PROD_IMAGE_INSERT : thm
val REAL_PROD_IMAGE_SING : thm
val REAL_PROD_IMAGE_THM : thm
val REAL_SUB_POLYFUN : thm
val REAL_SUB_POLYFUN_ALT : thm
val REAL_SUB_POW : thm
val REAL_SUB_POW_L1 : thm
val REAL_SUB_POW_R1 : thm
val REAL_SUM_IMAGE_0 : thm
val REAL_SUM_IMAGE_ABS_TRIANGLE : thm
val REAL_SUM_IMAGE_ADD : thm
val REAL_SUM_IMAGE_BOUND : thm
val REAL_SUM_IMAGE_CMUL : thm
val REAL_SUM_IMAGE_CONST_EQ_1_EQ_INV_CARD : thm
val REAL_SUM_IMAGE_COUNT : thm
val REAL_SUM_IMAGE_CROSS_SYM : thm
val REAL_SUM_IMAGE_DELETE : thm
val REAL_SUM_IMAGE_DISJOINT_UNION : thm
val REAL_SUM_IMAGE_EMPTY : thm
val REAL_SUM_IMAGE_EQ : thm
val REAL_SUM_IMAGE_EQ_CARD : thm
val REAL_SUM_IMAGE_EQ_sum : thm
val REAL_SUM_IMAGE_FINITE_CONST : thm
val REAL_SUM_IMAGE_FINITE_CONST2 : thm
val REAL_SUM_IMAGE_FINITE_CONST3 : thm
val REAL_SUM_IMAGE_FINITE_SAME : thm
val REAL_SUM_IMAGE_IF_ELIM : thm
val REAL_SUM_IMAGE_IMAGE : thm
val REAL_SUM_IMAGE_IMAGE_LE : thm
val REAL_SUM_IMAGE_INTER_ELIM : thm
val REAL_SUM_IMAGE_INTER_NONZERO : thm
val REAL_SUM_IMAGE_INV_CARD_EQ_1 : thm
val REAL_SUM_IMAGE_IN_IF : thm
val REAL_SUM_IMAGE_IN_IF_ALT : thm
val REAL_SUM_IMAGE_MONO : thm
val REAL_SUM_IMAGE_MONO_LT : thm
val REAL_SUM_IMAGE_MONO_SET : thm
val REAL_SUM_IMAGE_NEG : thm
val REAL_SUM_IMAGE_NONZERO : thm
val REAL_SUM_IMAGE_PERMUTES : thm
val REAL_SUM_IMAGE_POS : thm
val REAL_SUM_IMAGE_POS_LT : thm
val REAL_SUM_IMAGE_POS_MEM_LE : thm
val REAL_SUM_IMAGE_POW : thm
val REAL_SUM_IMAGE_REAL_SUM_IMAGE : thm
val REAL_SUM_IMAGE_SING : thm
val REAL_SUM_IMAGE_SPOS : thm
val REAL_SUM_IMAGE_SUB : thm
val REAL_SUM_IMAGE_SWAP : thm
val REAL_SUM_IMAGE_THM : thm
val REAL_SUM_IMAGE_sum : thm
val REAL_SUP_ASCLOSE : thm
val REAL_SUP_BOUNDS : thm
val REAL_SUP_EQ_INF : thm
val REAL_SUP_LE' : thm
val REAL_SUP_LE_EQ : thm
val REAL_SUP_LE_FINITE : thm
val REAL_SUP_LE_SUBSET : thm
val REAL_SUP_LE_X : thm
val REAL_SUP_LT_FINITE : thm
val REAL_SUP_UNIQUE : thm
val REAL_WLOG_LE : thm
val REAL_WLOG_LT : thm
val REAL_X_LE_SUP : thm
val SUMS_SYM : thm
val SUM_0' : thm
val SUM_ABS' : thm
val SUM_ABS_BOUND : thm
val SUM_ABS_LE' : thm
val SUM_ABS_NUMSEG : thm
val SUM_ABS_TRIANGLE : thm
val SUM_ADD' : thm
val SUM_ADD_COUNT : thm
val SUM_ADD_GEN : thm
val SUM_ADD_NUMSEG : thm
val SUM_ADD_SPLIT : thm
val SUM_BIGUNION_NONZERO : thm
val SUM_BIJECTION : thm
val SUM_BOUND' : thm
val SUM_BOUND_GEN : thm
val SUM_BOUND_LT : thm
val SUM_BOUND_LT_ALL : thm
val SUM_BOUND_LT_GEN : thm
val SUM_CASES : thm
val SUM_CASES_1 : thm
val SUM_CLAUSES : thm
val SUM_CLAUSES_LEFT : thm
val SUM_CLAUSES_NUMSEG : thm
val SUM_CLAUSES_RIGHT : thm
val SUM_CLOSED : thm
val SUM_COMBINE_L : thm
val SUM_COMBINE_R : thm
val SUM_CONG : thm
val SUM_CONST : thm
val SUM_CONST_NUMSEG : thm
val SUM_DEGENERATE : thm
val SUM_DELETE : thm
val SUM_DELETE_CASES : thm
val SUM_DELTA : thm
val SUM_DIFF' : thm
val SUM_DIFFS' : thm
val SUM_DIFFS_ALT : thm
val SUM_EQ' : thm
val SUM_EQ_0' : thm
val SUM_EQ_0_NUMSEG : thm
val SUM_EQ_COUNT : thm
val SUM_EQ_GENERAL : thm
val SUM_EQ_GENERAL_INVERSES : thm
val SUM_EQ_NUMSEG : thm
val SUM_EQ_SUPERSET : thm
val SUM_GP : thm
val SUM_GP_BASIC : thm
val SUM_GP_MULTIPLIED : thm
val SUM_GROUP' : thm
val SUM_IMAGE : thm
val SUM_IMAGE_GEN : thm
val SUM_IMAGE_LE : thm
val SUM_IMAGE_NONZERO : thm
val SUM_INCL_EXCL : thm
val SUM_INJECTION : thm
val SUM_LE' : thm
val SUM_LE_INCLUDED : thm
val SUM_LE_NUMSEG : thm
val SUM_LMUL : thm
val SUM_LT' : thm
val SUM_LT_ALL : thm
val SUM_MULTICOUNT : thm
val SUM_MULTICOUNT_GEN : thm
val SUM_NEG' : thm
val SUM_OFFSET' : thm
val SUM_OFFSET_0 : thm
val SUM_PAIR : thm
val SUM_PARTIAL_PRE : thm
val SUM_PARTIAL_SUC : thm
val SUM_PERMUTATIONS_COMPOSE_L : thm
val SUM_PERMUTATIONS_COMPOSE_L_COUNT : thm
val SUM_PERMUTATIONS_COMPOSE_L_NUMSEG : thm
val SUM_PERMUTATIONS_COMPOSE_R : thm
val SUM_PERMUTATIONS_COMPOSE_R_COUNT : thm
val SUM_PERMUTATIONS_COMPOSE_R_NUMSEG : thm
val SUM_PERMUTATIONS_INVERSE : thm
val SUM_PERMUTE : thm
val SUM_PERMUTE_COUNT : thm
val SUM_PERMUTE_NUMSEG : thm
val SUM_POS_BOUND : thm
val SUM_POS_EQ_0 : thm
val SUM_POS_EQ_0_NUMSEG : thm
val SUM_POS_LE : thm
val SUM_POS_LE_NUMSEG : thm
val SUM_POS_LT : thm
val SUM_POS_LT_ALL : thm
val SUM_RESTRICT : thm
val SUM_RESTRICT_SET : thm
val SUM_RMUL : thm
val SUM_SING : thm
val SUM_SING_NUMSEG : thm
val SUM_SUB' : thm
val SUM_SUBSET : thm
val SUM_SUBSET_SIMPLE : thm
val SUM_SUB_NUMSEG : thm
val SUM_SUM_PRODUCT : thm
val SUM_SUM_RESTRICT : thm
val SUM_SUPERSET : thm
val SUM_SUPPORT : thm
val SUM_SWAP : thm
val SUM_SWAP_COUNT : thm
val SUM_SWAP_NUMSEG : thm
val SUM_TRIV_NUMSEG : thm
val SUM_UNION : thm
val SUM_UNION_EQ : thm
val SUM_UNION_LZERO : thm
val SUM_UNION_NONZERO : thm
val SUM_UNION_RZERO : thm
val SUM_ZERO_EXISTS : thm
val SUP : thm
val SUP_EQ : thm
val SUP_FINITE : thm
val SUP_FINITE_LEMMA : thm
val SUP_INSERT_FINITE : thm
val SUP_MONO : thm
val SUP_SING : thm
val SUP_UNION : thm
val SUP_UNIQUE : thm
val SUP_UNIQUE_FINITE : thm
val UPPER_BOUND_FINITE_SET_REAL : thm
val inf_alt : thm
val jensen_concave_SIGMA : thm
val jensen_convex_SIGMA : thm
val jensen_pos_concave_SIGMA : thm
val jensen_pos_convex_SIGMA : thm
val real_INFINITE : thm
val sum_real : thm
val sup_alt : thm
(*
[cardinal] Parent theory of "real_sigma"
[iterate] Parent theory of "real_sigma"
[real] Parent theory of "real_sigma"
[res_quan] Parent theory of "real_sigma"
[REAL_PROD_IMAGE_DEF] Definition
⊢ ∀f s. ∏ f s = ITSET (λe acc. f e * acc) s 1
[REAL_SUM_IMAGE_DEF] Definition
⊢ ∀f s. SIGMA f s = ITSET (λe acc. f e + acc) s 0
[concave_fn] Definition
⊢ concave_fn = {f | (λx. -f x) ∈ convex_fn}
[convex_fn] Definition
⊢ convex_fn =
{f |
∀x y t.
0 ≤ t ∧ t ≤ 1 ⇒
f (t * x + (1 − t) * y) ≤ t * f x + (1 − t) * f y}
[indicator] Definition
⊢ ∀s. indicator s = (λx. if x ∈ s then 1 else 0)
[polynomial_function] Definition
⊢ ∀p. polynomial_function p ⇔
∃m c. ∀x. p x = sum {0 .. m} (λi. c i * x pow i)
[pos_concave_fn] Definition
⊢ pos_concave_fn = {f | (λx. -f x) ∈ pos_convex_fn}
[pos_convex_fn] Definition
⊢ pos_convex_fn =
{f |
∀x y t.
0 < x ∧ 0 < y ∧ 0 ≤ t ∧ t ≤ 1 ⇒
f (t * x + (1 − t) * y) ≤ t * f x + (1 − t) * f y}
[product] Definition
⊢ product = iterate $*
[sum_def] Definition
⊢ sum = iterate $+
[ABS_LE_0] Theorem
⊢ ∀x. abs x ≤ 0 ⇔ x = 0
[ABS_LE_HALF_POW2] Theorem
⊢ ∀x y. abs (x * y) ≤ 1 / 2 * (x² + y²)
[CARD_EQ_SUM] Theorem
⊢ ∀s. FINITE s ⇒ &CARD s = sum s (λx. 1)
[DROP_INDICATOR] Theorem
⊢ ∀s x. indicator s x = if x ∈ s then 1 else 0
[DROP_INDICATOR_ABS_LE_1] Theorem
⊢ ∀s x. abs (indicator s x) ≤ 1
[DROP_INDICATOR_LE_1] Theorem
⊢ ∀s x. indicator s x ≤ 1
[DROP_INDICATOR_POS_LE] Theorem
⊢ ∀s x. 0 ≤ indicator s x
[FINITE_REAL_INTERVAL] Theorem
⊢ (∀a. INFINITE {x | a < x}) ∧ (∀a. INFINITE {x | a ≤ x}) ∧
(∀b. INFINITE {x | x < b}) ∧ (∀b. INFINITE {x | x ≤ b}) ∧
(∀a b. FINITE {x | a < x ∧ x < b} ⇔ b ≤ a) ∧
(∀a b. FINITE {x | a ≤ x ∧ x < b} ⇔ b ≤ a) ∧
(∀a b. FINITE {x | a < x ∧ x ≤ b} ⇔ b ≤ a) ∧
∀a b. FINITE {x | a ≤ x ∧ x ≤ b} ⇔ b ≤ a
[INDICATOR_COMPLEMENT] Theorem
⊢ ∀s. indicator (𝕌(:α) DIFF s) = (λx. 1 − indicator s x)
[INDICATOR_EMPTY] Theorem
⊢ indicator ∅ = (λx. 0)
[INF] Theorem
⊢ ∀s. s ≠ ∅ ∧ (∃b. ∀x. x ∈ s ⇒ b ≤ x) ⇒
(∀x. x ∈ s ⇒ inf s ≤ x) ∧ ∀b. (∀x. x ∈ s ⇒ b ≤ x) ⇒ b ≤ inf s
[INF_CLOSE] Theorem
⊢ ∀p e. (∃x. x ∈ p) ∧ 0 < e ⇒ ∃x. x ∈ p ∧ x < inf p + e
[INF_EQ] Theorem
⊢ ∀s t.
s ≠ ∅ ∧ (∃b. ∀x. x ∈ s ⇒ b ≤ x) ∧ t ≠ ∅ ∧
(∃b. ∀x. x ∈ t ⇒ b ≤ x) ∧
(∀a. (∀x. x ∈ s ⇒ a ≤ x) ⇔ ∀x. x ∈ t ⇒ a ≤ x) ⇒
inf s = inf t
[INF_FINITE] Theorem
⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ inf s ∈ s ∧ ∀x. x ∈ s ⇒ inf s ≤ x
[INF_FINITE_LEMMA] Theorem
⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ∃b. b ∈ s ∧ ∀x. x ∈ s ⇒ b ≤ x
[INF_GREATER] Theorem
⊢ ∀p z. (∃x. x ∈ p) ∧ inf p < z ⇒ ∃x. x ∈ p ∧ x < z
[INF_INSERT_FINITE] Theorem
⊢ ∀x s.
FINITE s ⇒ inf (x INSERT s) = if s = ∅ then x else min x (inf s)
[INF_LE] Theorem
⊢ ∀p r. (∃z. ∀x. x ∈ p ⇒ z ≤ x) ∧ (∃x. x ∈ p ∧ x ≤ r) ⇒ inf p ≤ r
[INF_SING] Theorem
⊢ ∀a. inf {a} = a
[INF_UNIQUE_FINITE] Theorem
⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (inf s = a ⇔ a ∈ s ∧ ∀y. y ∈ s ⇒ a ≤ y)
[ITERATE_NONZERO_IMAGE_LEMMA] Theorem
⊢ ∀op s f g a.
monoidal op ∧ FINITE s ∧ g a = neutral op ∧
(∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ∧ x ≠ y ⇒ g (f x) = neutral op) ⇒
iterate op {f x | x | x ∈ s ∧ f x ≠ a} g = iterate op s (g ∘ f)
[LE_INF] Theorem
⊢ ∀p r. (∃x. x ∈ p) ∧ (∀x. x ∈ p ⇒ r ≤ x) ⇒ r ≤ inf p
[LOWER_BOUND_FINITE_SET_REAL] Theorem
⊢ ∀f s. FINITE s ⇒ ∃a. ∀x. x ∈ s ⇒ a ≤ f x
[MONOIDAL_REAL_ADD] Theorem
⊢ monoidal $+
[MONOIDAL_REAL_MUL] Theorem
⊢ monoidal $*
[NESTED_REAL_SUM_IMAGE_REVERSE] Theorem
⊢ ∀f s s'.
FINITE s ∧ FINITE s' ⇒
SIGMA (λx. SIGMA (f x) s') s = SIGMA (λx. SIGMA (λy. f y x) s) s'
[NEUTRAL_REAL_ADD] Theorem
⊢ neutral $+ = 0
[NEUTRAL_REAL_MUL] Theorem
⊢ neutral $* = 1
[PERMUTES_IN_NUMSEG] Theorem
⊢ ∀p n i. p permutes {1 .. n} ∧ i ∈ {1 .. n} ⇒ 1 ≤ p i ∧ p i ≤ n
[POLYNOMIAL_FUNCTION_ADD] Theorem
⊢ ∀p q.
polynomial_function p ∧ polynomial_function q ⇒
polynomial_function (λx. p x + q x)
[POLYNOMIAL_FUNCTION_CONST] Theorem
⊢ ∀c. polynomial_function (λx. c)
[POLYNOMIAL_FUNCTION_FINITE_ROOTS] Theorem
⊢ ∀p a. polynomial_function p ⇒ (FINITE {x | p x = a} ⇔ ¬∀x. p x = a)
[POLYNOMIAL_FUNCTION_ID] Theorem
⊢ polynomial_function (λx. x)
[POLYNOMIAL_FUNCTION_INDUCT] Theorem
⊢ ∀P. P (λx. x) ∧ (∀c. P (λx. c)) ∧
(∀p q. P p ∧ P q ⇒ P (λx. p x + q x)) ∧
(∀p q. P p ∧ P q ⇒ P (λx. p x * q x)) ⇒
∀p. polynomial_function p ⇒ P p
[POLYNOMIAL_FUNCTION_LMUL] Theorem
⊢ ∀p c. polynomial_function p ⇒ polynomial_function (λx. c * p x)
[POLYNOMIAL_FUNCTION_MUL] Theorem
⊢ ∀p q.
polynomial_function p ∧ polynomial_function q ⇒
polynomial_function (λx. p x * q x)
[POLYNOMIAL_FUNCTION_NEG] Theorem
⊢ ∀p. polynomial_function (λx. -p x) ⇔ polynomial_function p
[POLYNOMIAL_FUNCTION_POW] Theorem
⊢ ∀p n. polynomial_function p ⇒ polynomial_function (λx. p x pow n)
[POLYNOMIAL_FUNCTION_RMUL] Theorem
⊢ ∀p c. polynomial_function p ⇒ polynomial_function (λx. p x * c)
[POLYNOMIAL_FUNCTION_SUB] Theorem
⊢ ∀p q.
polynomial_function p ∧ polynomial_function q ⇒
polynomial_function (λx. p x − q x)
[POLYNOMIAL_FUNCTION_SUM] Theorem
⊢ ∀s p.
FINITE s ∧ (∀i. i ∈ s ⇒ polynomial_function (λx. p x i)) ⇒
polynomial_function (λx. sum s (p x))
[POLYNOMIAL_FUNCTION_o] Theorem
⊢ ∀p q.
polynomial_function p ∧ polynomial_function q ⇒
polynomial_function (p ∘ q)
[POW_NEG_ODD] Theorem
⊢ ∀x. x < 0 ⇒ (x pow n < 0 ⇔ ODD n)
[POW_POS_EVEN] Theorem
⊢ ∀x. x < 0 ⇒ (0 < x pow n ⇔ EVEN n)
[PRODUCT_ABS] Theorem
⊢ ∀f s. FINITE s ⇒ product s (λx. abs (f x)) = abs (product s f)
[PRODUCT_ADD_SPLIT] Theorem
⊢ ∀f m n p.
m ≤ n + 1 ⇒
product {m .. n + p} f =
product {m .. n} f * product {n + 1 .. n + p} f
[PRODUCT_CLAUSES] Theorem
⊢ (∀f. product ∅ f = 1) ∧
∀x f s.
FINITE s ⇒
product (x INSERT s) f =
if x ∈ s then product s f else f x * product s f
[PRODUCT_CLAUSES_LEFT] Theorem
⊢ ∀f m n. m ≤ n ⇒ product {m .. n} f = f m * product {m + 1 .. n} f
[PRODUCT_CLAUSES_NUMSEG] Theorem
⊢ (∀m. product {m .. 0} f = if m = 0 then f 0 else 1) ∧
∀m n.
product {m .. SUC n} f =
if m ≤ SUC n then product {m .. n} f * f (SUC n)
else product {m .. n} f
[PRODUCT_CLAUSES_RIGHT] Theorem
⊢ ∀f m n.
0 < n ∧ m ≤ n ⇒ product {m .. n} f = product {m .. n − 1} f * f n
[PRODUCT_CLOSED] Theorem
⊢ ∀P f s.
P 1 ∧ (∀x y. P x ∧ P y ⇒ P (x * y)) ∧ (∀a. a ∈ s ⇒ P (f a)) ⇒
P (product s f)
[PRODUCT_CONG] Theorem
⊢ (∀f g s.
(∀x. x ∈ s ⇒ f x = g x) ⇒ product s (λi. f i) = product s g) ∧
(∀f g a b.
(∀i. a ≤ i ∧ i ≤ b ⇒ f i = g i) ⇒
product {a .. b} (λi. f i) = product {a .. b} g) ∧
∀f g p.
(∀x. p x ⇒ f x = g x) ⇒
product {y | p y} (λi. f i) = product {y | p y} g
[PRODUCT_CONST] Theorem
⊢ ∀c s. FINITE s ⇒ product s (λx. c) = c pow CARD s
[PRODUCT_CONST_NUMSEG] Theorem
⊢ ∀c m n. product {m .. n} (λx. c) = c pow (n + 1 − m)
[PRODUCT_CONST_NUMSEG_1] Theorem
⊢ ∀c n. product {1 .. n} (λx. c) = c pow n
[PRODUCT_DELETE] Theorem
⊢ ∀f s a.
FINITE s ∧ a ∈ s ⇒ f a * product (s DELETE a) f = product s f
[PRODUCT_DELTA] Theorem
⊢ ∀s a.
product s (λx. if x = a then b else 1) = if a ∈ s then b else 1
[PRODUCT_DIV] Theorem
⊢ ∀f g s.
FINITE s ⇒ product s (λx. f x / g x) = product s f / product s g
[PRODUCT_DIV_NUMSEG] Theorem
⊢ ∀f g m n.
product {m .. n} (λx. f x / g x) =
product {m .. n} f / product {m .. n} g
[PRODUCT_EQ] Theorem
⊢ ∀f g s. (∀x. x ∈ s ⇒ f x = g x) ⇒ product s f = product s g
[PRODUCT_EQ_0] Theorem
⊢ ∀f s. FINITE s ⇒ (product s f = 0 ⇔ ∃x. x ∈ s ∧ f x = 0)
[PRODUCT_EQ_0_COUNT] Theorem
⊢ ∀f n. product (count n) f = 0 ⇔ ∃i. i < n ∧ f i = 0
[PRODUCT_EQ_0_NUMSEG] Theorem
⊢ ∀f m n. product {m .. n} f = 0 ⇔ ∃x. m ≤ x ∧ x ≤ n ∧ f x = 0
[PRODUCT_EQ_1] Theorem
⊢ ∀f s. (∀x. x ∈ s ⇒ f x = 1) ⇒ product s f = 1
[PRODUCT_EQ_1_COUNT] Theorem
⊢ ∀f n. (∀i. i < n ⇒ f i = 1) ⇒ product (count n) f = 1
[PRODUCT_EQ_1_NUMSEG] Theorem
⊢ ∀f m n. (∀i. m ≤ i ∧ i ≤ n ⇒ f i = 1) ⇒ product {m .. n} f = 1
[PRODUCT_EQ_COUNT] Theorem
⊢ ∀f g n.
(∀i. i < n ⇒ f i = g i) ⇒
product (count n) f = product (count n) g
[PRODUCT_EQ_NUMSEG] Theorem
⊢ ∀f g m n.
(∀i. m ≤ i ∧ i ≤ n ⇒ f i = g i) ⇒
product {m .. n} f = product {m .. n} g
[PRODUCT_IMAGE] Theorem
⊢ ∀f g s.
(∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒
product (IMAGE f s) g = product s (g ∘ f)
[PRODUCT_INV] Theorem
⊢ ∀f s. FINITE s ⇒ product s (λx. (f x)⁻¹) = (product s f)⁻¹
[PRODUCT_LE] Theorem
⊢ ∀f s.
FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x ∧ f x ≤ g x) ⇒
product s f ≤ product s g
[PRODUCT_LE_1] Theorem
⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x ∧ f x ≤ 1) ⇒ product s f ≤ 1
[PRODUCT_LE_NUMSEG] Theorem
⊢ ∀f m n.
(∀i. m ≤ i ∧ i ≤ n ⇒ 0 ≤ f i ∧ f i ≤ g i) ⇒
product {m .. n} f ≤ product {m .. n} g
[PRODUCT_MUL] Theorem
⊢ ∀f g s.
FINITE s ⇒ product s (λx. f x * g x) = product s f * product s g
[PRODUCT_MUL_COUNT] Theorem
⊢ ∀f g n.
product (count n) (λx. f x * g x) =
product (count n) f * product (count n) g
[PRODUCT_MUL_GEN] Theorem
⊢ ∀f g s.
FINITE {x | x ∈ s ∧ f x ≠ 1} ∧ FINITE {x | x ∈ s ∧ g x ≠ 1} ⇒
product s (λx. f x * g x) = product s f * product s g
[PRODUCT_MUL_NUMSEG] Theorem
⊢ ∀f g m n.
product {m .. n} (λx. f x * g x) =
product {m .. n} f * product {m .. n} g
[PRODUCT_NEG] Theorem
⊢ ∀f s. FINITE s ⇒ product s (λi. -f i) = -1 pow CARD s * product s f
[PRODUCT_NEG_NUMSEG] Theorem
⊢ ∀f m n.
product {m .. n} (λi. -f i) =
-1 pow (n + 1 − m) * product {m .. n} f
[PRODUCT_NEG_NUMSEG_1] Theorem
⊢ ∀f n. product {1 .. n} (λi. -f i) = -1 pow n * product {1 .. n} f
[PRODUCT_OFFSET] Theorem
⊢ ∀f m p.
product {m + p .. n + p} f = product {m .. n} (λi. f (i + p))
[PRODUCT_ONE] Theorem
⊢ ∀s. product s (λn. 1) = 1
[PRODUCT_PAIR] Theorem
⊢ ∀f m n.
product {2 * m .. 2 * n + 1} f =
product {m .. n} (λi. f (2 * i) * f (2 * i + 1))
[PRODUCT_PERMUTE] Theorem
⊢ ∀f p s. p permutes s ⇒ product s f = product s (f ∘ p)
[PRODUCT_PERMUTE_COUNT] Theorem
⊢ ∀f p n.
p permutes count n ⇒
product (count n) f = product (count n) (f ∘ p)
[PRODUCT_PERMUTE_NUMSEG] Theorem
⊢ ∀f p m n.
p permutes count n DIFF count m ⇒
product (count n DIFF count m) f =
product (count n DIFF count m) (f ∘ p)
[PRODUCT_POS_LE] Theorem
⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ product s f
[PRODUCT_POS_LE_NUMSEG] Theorem
⊢ ∀f m n. (∀x. m ≤ x ∧ x ≤ n ⇒ 0 ≤ f x) ⇒ 0 ≤ product {m .. n} f
[PRODUCT_POS_LT] Theorem
⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 < f x) ⇒ 0 < product s f
[PRODUCT_POS_LT_NUMSEG] Theorem
⊢ ∀f m n. (∀x. m ≤ x ∧ x ≤ n ⇒ 0 < f x) ⇒ 0 < product {m .. n} f
[PRODUCT_SING] Theorem
⊢ ∀f x. product {x} f = f x
[PRODUCT_SING_NUMSEG] Theorem
⊢ ∀f n. product {n .. n} f = f n
[PRODUCT_SUPERSET] Theorem
⊢ ∀f u v.
u ⊆ v ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ f x = 1) ⇒ product v f = product u f
[PRODUCT_SUPPORT] Theorem
⊢ ∀f s. product (support $* f s) f = product s f
[PRODUCT_UNION] Theorem
⊢ ∀f s t.
FINITE s ∧ FINITE t ∧ DISJOINT s t ⇒
product (s ∪ t) f = product s f * product t f
[REAL_ABS_INF_LE] Theorem
⊢ ∀s a. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ abs x ≤ a) ⇒ abs (inf s) ≤ a
[REAL_ABS_SUP_LE] Theorem
⊢ ∀s a. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ abs x ≤ a) ⇒ abs (sup s) ≤ a
[REAL_ARCH_INV'] Theorem
⊢ ∀x. 0 < x ⇒ ∃n. (&n)⁻¹ < x
[REAL_ARCH_INV_SUC] Theorem
⊢ ∀x. 0 < x ⇒ ∃n. (&SUC n)⁻¹ < x
[REAL_BOUNDS_LT] Theorem
⊢ ∀x k. -k < x ∧ x < k ⇔ abs x < k
[REAL_COMPLETE] Theorem
⊢ ∀P. (∃x. P x) ∧ (∃M. ∀x. P x ⇒ x ≤ M) ⇒
∃M. (∀x. P x ⇒ x ≤ M) ∧ ∀M'. (∀x. P x ⇒ x ≤ M') ⇒ M ≤ M'
[REAL_EQ_SQUARE_ABS] Theorem
⊢ ∀x y. abs x = abs y ⇔ x² = y²
[REAL_HALF] Theorem
⊢ (∀e. 0 < e / 2 ⇔ 0 < e) ∧ (∀e. e / 2 + e / 2 = e) ∧
∀e. 2 * (e / 2) = e
[REAL_IMP_LE_SUP'] Theorem
⊢ ∀p x. (∃z. ∀r. r ∈ p ⇒ r ≤ z) ∧ (∃r. r ∈ p ∧ x ≤ r) ⇒ x ≤ sup p
[REAL_IMP_SUP_LE'] Theorem
⊢ ∀p x. (∃r. r ∈ p) ∧ (∀r. r ∈ p ⇒ r ≤ x) ⇒ sup p ≤ x
[REAL_INF_ASCLOSE] Theorem
⊢ ∀s l e. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ abs (x − l) ≤ e) ⇒ abs (inf s − l) ≤ e
[REAL_INF_BOUNDS] Theorem
⊢ ∀s a b. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ a ≤ x ∧ x ≤ b) ⇒ a ≤ inf s ∧ inf s ≤ b
[REAL_INF_LE'] Theorem
⊢ ∀p x.
(∃y. y ∈ p) ∧ (∃y. ∀z. z ∈ p ⇒ y ≤ z) ⇒
(inf p ≤ x ⇔ ∀y. (∀z. z ∈ p ⇒ y ≤ z) ⇒ y ≤ x)
[REAL_INF_LE_FINITE] Theorem
⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (inf s ≤ a ⇔ ∃x. x ∈ s ∧ x ≤ a)
[REAL_INF_LT_FINITE] Theorem
⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (inf s < a ⇔ ∃x. x ∈ s ∧ x < a)
[REAL_INF_UNIQUE] Theorem
⊢ ∀s b.
(∀x. x ∈ s ⇒ b ≤ x) ∧ (∀b'. b < b' ⇒ ∃x. x ∈ s ∧ x < b') ⇒
inf s = b
[REAL_LE_BETWEEN] Theorem
⊢ ∀a b. a ≤ b ⇔ ∃x. a ≤ x ∧ x ≤ b
[REAL_LE_INF] Theorem
⊢ ∀s b. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ b ≤ x) ⇒ b ≤ inf s
[REAL_LE_INF_FINITE] Theorem
⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (a ≤ inf s ⇔ ∀x. x ∈ s ⇒ a ≤ x)
[REAL_LE_INF_SUBSET] Theorem
⊢ ∀s t. t ≠ ∅ ∧ t ⊆ s ∧ (∃b. ∀x. x ∈ s ⇒ b ≤ x) ⇒ inf s ≤ inf t
[REAL_LE_LDIV_CANCEL] Theorem
⊢ ∀x y z. 0 < x ∧ 0 < y ∧ 0 < z ⇒ (z / x ≤ z / y ⇔ y ≤ x)
[REAL_LE_LDIV_EQ_NEG] Theorem
⊢ ∀x y z. z < 0 ⇒ (x ≤ y / z ⇔ y ≤ x * z)
[REAL_LE_LT_MUL] Theorem
⊢ ∀x y. 0 ≤ x ∧ 0 < y ⇒ 0 ≤ x * y
[REAL_LE_MUL'] Theorem
⊢ ∀x y. x ≤ 0 ∧ y ≤ 0 ⇒ 0 ≤ x * y
[REAL_LE_MUL_EPSILON] Theorem
⊢ ∀x y. (∀z. 0 < z ∧ z < 1 ⇒ z * x ≤ y) ⇒ x ≤ y
[REAL_LE_RDIV_EQ_NEG] Theorem
⊢ ∀x y z. z < 0 ⇒ (y / z ≤ x ⇔ x * z ≤ y)
[REAL_LE_SQUARE_ABS] Theorem
⊢ ∀x y. abs x ≤ abs y ⇔ x² ≤ y²
[REAL_LE_SUP'] Theorem
⊢ ∀s a b y. y ∈ s ∧ a ≤ y ∧ (∀x. x ∈ s ⇒ x ≤ b) ⇒ a ≤ sup s
[REAL_LE_SUP_EQ] Theorem
⊢ ∀p x.
(∃y. y ∈ p) ∧ (∃y. ∀z. z ∈ p ⇒ z ≤ y) ⇒
(x ≤ sup p ⇔ ∀y. (∀z. z ∈ p ⇒ z ≤ y) ⇒ x ≤ y)
[REAL_LE_SUP_FINITE] Theorem
⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (a ≤ sup s ⇔ ∃x. x ∈ s ∧ a ≤ x)
[REAL_LT_BETWEEN] Theorem
⊢ ∀a b. a < b ⇔ ∃x. a < x ∧ x < b
[REAL_LT_INF_FINITE] Theorem
⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (a < inf s ⇔ ∀x. x ∈ s ⇒ a < x)
[REAL_LT_INV2] Theorem
⊢ ∀x y. 0 < x ∧ x < y ⇒ y⁻¹ < x⁻¹
[REAL_LT_LCANCEL_IMP] Theorem
⊢ ∀x y z. 0 < x ∧ x * y < x * z ⇒ y < z
[REAL_LT_LDIV_CANCEL] Theorem
⊢ ∀x y z. 0 < x ∧ 0 < y ∧ 0 < z ⇒ (z / x < z / y ⇔ y < x)
[REAL_LT_LE_MUL] Theorem
⊢ ∀x y. 0 < x ∧ 0 ≤ y ⇒ 0 ≤ x * y
[REAL_LT_LMUL'] Theorem
⊢ ∀x y z. x < 0 ⇒ (x * y < x * z ⇔ z < y)
[REAL_LT_LMUL_0_NEG] Theorem
⊢ ∀x y. 0 < x * y ∧ x < 0 ⇒ y < 0
[REAL_LT_LMUL_NEG_0] Theorem
⊢ ∀x y. x * y < 0 ∧ 0 < x ⇒ y < 0
[REAL_LT_LMUL_NEG_0_NEG] Theorem
⊢ ∀x y. x * y < 0 ∧ x < 0 ⇒ 0 < y
[REAL_LT_MAX_BETWEEN] Theorem
⊢ ∀x b d. x < max b d ∧ b ≤ x ⇒ x < d
[REAL_LT_MUL'] Theorem
⊢ ∀x y. x < 0 ∧ y < 0 ⇒ 0 < x * y
[REAL_LT_POW2] Theorem
⊢ ∀n. 0 < 2 pow n
[REAL_LT_RDIV_EQ_NEG] Theorem
⊢ ∀x y z. z < 0 ⇒ (y / z < x ⇔ x * z < y)
[REAL_LT_RMUL'] Theorem
⊢ ∀x y z. z < 0 ⇒ (x * z < y * z ⇔ y < x)
[REAL_LT_RMUL_0_NEG] Theorem
⊢ ∀x y. 0 < x * y ∧ y < 0 ⇒ x < 0
[REAL_LT_RMUL_NEG_0] Theorem
⊢ ∀x y. x * y < 0 ∧ 0 < y ⇒ x < 0
[REAL_LT_RMUL_NEG_0_NEG] Theorem
⊢ ∀x y. x * y < 0 ∧ y < 0 ⇒ 0 < x
[REAL_LT_SUP_FINITE] Theorem
⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (a < sup s ⇔ ∃x. x ∈ s ∧ a < x)
[REAL_MAX_REDUCE] Theorem
⊢ ∀x y. x ≤ y ∨ x < y ⇒ max x y = y ∧ max y x = y
[REAL_MIN_LE_BETWEEN] Theorem
⊢ ∀x a c. min a c ≤ x ∧ x < a ⇒ c ≤ x
[REAL_MIN_REDUCE] Theorem
⊢ ∀x y. x ≤ y ∨ x < y ⇒ min x y = x ∧ min y x = x
[REAL_MUL_IDEMPOT] Theorem
⊢ ∀r. r * r = r ⇔ r = 0 ∨ r = 1
[REAL_MUL_SUM] Theorem
⊢ ∀s t f g.
FINITE s ∧ FINITE t ⇒
sum s f * sum t g = sum s (λi. sum t (λj. f i * g j))
[REAL_MUL_SUM_NUMSEG] Theorem
⊢ ∀f g m n p q.
sum {m .. n} f * sum {p .. q} g =
sum {m .. n} (λi. sum {p .. q} (λj. f i * g j))
[REAL_NEG_NZ] Theorem
⊢ ∀x. x < 0 ⇒ x ≠ 0
[REAL_OF_NUM_GE] Theorem
⊢ ∀m n. &m ≥ &n ⇔ m ≥ n
[REAL_OF_NUM_NPRODUCT] Theorem
⊢ ∀f s. FINITE s ⇒ &nproduct s f = product s (λx. &f x)
[REAL_OF_NUM_SUM] Theorem
⊢ ∀f s. FINITE s ⇒ &nsum s f = sum s (λx. &f x)
[REAL_OF_NUM_SUM_NUMSEG] Theorem
⊢ ∀f m n. &nsum {m .. n} f = sum {m .. n} (λi. &f i)
[REAL_POLYFUN_EQ_0] Theorem
⊢ ∀n c.
(∀x. sum {0 .. n} (λi. c i * x pow i) = 0) ⇔
∀i. i ∈ {0 .. n} ⇒ c i = 0
[REAL_POLYFUN_EQ_CONST] Theorem
⊢ ∀n c k.
(∀x. sum {0 .. n} (λi. c i * x pow i) = k) ⇔
c 0 = k ∧ ∀i. i ∈ {1 .. n} ⇒ c i = 0
[REAL_POLYFUN_FINITE_ROOTS] Theorem
⊢ ∀n c.
FINITE {x | sum {0 .. n} (λi. c i * x pow i) = 0} ⇔
∃i. i ∈ {0 .. n} ∧ c i ≠ 0
[REAL_POLYFUN_ROOTBOUND] Theorem
⊢ ∀n c.
¬(∀i. i ∈ {0 .. n} ⇒ c i = 0) ⇒
FINITE {x | sum {0 .. n} (λi. c i * x pow i) = 0} ∧
CARD {x | sum {0 .. n} (λi. c i * x pow i) = 0} ≤ n
[REAL_PROD_IMAGE_EMPTY] Theorem
⊢ ∀f. ∏ f ∅ = 1
[REAL_PROD_IMAGE_INSERT] Theorem
⊢ ∀f e s. FINITE s ⇒ ∏ f (e INSERT s) = f e * ∏ f (s DELETE e)
[REAL_PROD_IMAGE_SING] Theorem
⊢ ∀f e. ∏ f {e} = f e
[REAL_PROD_IMAGE_THM] Theorem
⊢ ∀f. ∏ f ∅ = 1 ∧
∀e s. FINITE s ⇒ ∏ f (e INSERT s) = f e * ∏ f (s DELETE e)
[REAL_SUB_POLYFUN] Theorem
⊢ ∀a x y n.
1 ≤ n ⇒
sum {0 .. n} (λi. a i * x pow i) −
sum {0 .. n} (λi. a i * y pow i) =
(x − y) *
sum {0 .. n − 1}
(λj. sum {j + 1 .. n} (λi. a i * y pow (i − j − 1)) * x pow j)
[REAL_SUB_POLYFUN_ALT] Theorem
⊢ ∀a x y n.
1 ≤ n ⇒
sum {0 .. n} (λi. a i * x pow i) −
sum {0 .. n} (λi. a i * y pow i) =
(x − y) *
sum {0 .. n − 1}
(λj.
sum {0 .. n − j − 1} (λk. a (j + k + 1) * y pow k) *
x pow j)
[REAL_SUB_POW] Theorem
⊢ ∀x y n.
1 ≤ n ⇒
x pow n − y pow n =
(x − y) * sum {0 .. n − 1} (λi. x pow i * y pow (n − 1 − i))
[REAL_SUB_POW_L1] Theorem
⊢ ∀x n.
1 ≤ n ⇒ 1 − x pow n = (1 − x) * sum {0 .. n − 1} (λi. x pow i)
[REAL_SUB_POW_R1] Theorem
⊢ ∀x n.
1 ≤ n ⇒ x pow n − 1 = (x − 1) * sum {0 .. n − 1} (λi. x pow i)
[REAL_SUM_IMAGE_0] Theorem
⊢ ∀s. FINITE s ⇒ SIGMA (λx. 0) s = 0
[REAL_SUM_IMAGE_ABS_TRIANGLE] Theorem
⊢ ∀f s. FINITE s ⇒ abs (SIGMA f s) ≤ SIGMA (abs ∘ f) s
[REAL_SUM_IMAGE_ADD] Theorem
⊢ ∀s. FINITE s ⇒
∀f f'. SIGMA (λx. f x + f' x) s = SIGMA f s + SIGMA f' s
[REAL_SUM_IMAGE_BOUND] Theorem
⊢ ∀s f b. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ b) ⇒ SIGMA f s ≤ &CARD s * b
[REAL_SUM_IMAGE_CMUL] Theorem
⊢ ∀P. FINITE P ⇒ ∀f c. SIGMA (λx. c * f x) P = c * SIGMA f P
[REAL_SUM_IMAGE_CONST_EQ_1_EQ_INV_CARD] Theorem
⊢ ∀P. FINITE P ⇒
∀f. SIGMA f P = 1 ∧ (∀x y. x ∈ P ∧ y ∈ P ⇒ f x = f y) ⇒
∀x. x ∈ P ⇒ f x = (&CARD P)⁻¹
[REAL_SUM_IMAGE_COUNT] Theorem
⊢ ∀f n. SIGMA f (count n) = sum (0,n) f
[REAL_SUM_IMAGE_CROSS_SYM] Theorem
⊢ ∀f s1 s2.
FINITE s1 ∧ FINITE s2 ⇒
SIGMA (λ(x,y). f (x,y)) (s1 × s2) =
SIGMA (λ(y,x). f (x,y)) (s2 × s1)
[REAL_SUM_IMAGE_DELETE] Theorem
⊢ ∀f s a. FINITE s ∧ a ∈ s ⇒ sum (s DELETE a) f = SIGMA f s − f a
[REAL_SUM_IMAGE_DISJOINT_UNION] Theorem
⊢ ∀P P'.
FINITE P ∧ FINITE P' ∧ DISJOINT P P' ⇒
∀f. SIGMA f (P ∪ P') = SIGMA f P + SIGMA f P'
[REAL_SUM_IMAGE_EMPTY] Theorem
⊢ ∀f. SIGMA f ∅ = 0
[REAL_SUM_IMAGE_EQ] Theorem
⊢ ∀s f f'.
FINITE s ∧ (∀x. x ∈ s ⇒ f x = f' x) ⇒ SIGMA f s = SIGMA f' s
[REAL_SUM_IMAGE_EQ_CARD] Theorem
⊢ ∀P. FINITE P ⇒ SIGMA (λx. if x ∈ P then 1 else 0) P = &CARD P
[REAL_SUM_IMAGE_EQ_sum] Theorem
⊢ ∀n r. sum (0,n) r = SIGMA r (count n)
[REAL_SUM_IMAGE_FINITE_CONST] Theorem
⊢ ∀P. FINITE P ⇒ ∀f x. (∀y. f y = x) ⇒ SIGMA f P = &CARD P * x
[REAL_SUM_IMAGE_FINITE_CONST2] Theorem
⊢ ∀P. FINITE P ⇒
∀f x. (∀y. y ∈ P ⇒ f y = x) ⇒ SIGMA f P = &CARD P * x
[REAL_SUM_IMAGE_FINITE_CONST3] Theorem
⊢ ∀P. FINITE P ⇒ ∀c. SIGMA (λx. c) P = &CARD P * c
[REAL_SUM_IMAGE_FINITE_SAME] Theorem
⊢ ∀P. FINITE P ⇒
∀f p.
p ∈ P ∧ (∀q. q ∈ P ⇒ f p = f q) ⇒ SIGMA f P = &CARD P * f p
[REAL_SUM_IMAGE_IF_ELIM] Theorem
⊢ ∀s P f.
FINITE s ∧ (∀x. x ∈ s ⇒ P x) ⇒
SIGMA (λx. if P x then f x else 0) s = SIGMA f s
[REAL_SUM_IMAGE_IMAGE] Theorem
⊢ ∀P. FINITE P ⇒
∀f'.
INJ f' P (IMAGE f' P) ⇒
∀f. SIGMA f (IMAGE f' P) = SIGMA (f ∘ f') P
[REAL_SUM_IMAGE_IMAGE_LE] Theorem
⊢ ∀f g s.
FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ g (f x)) ⇒
SIGMA g (IMAGE f s) ≤ SIGMA (g ∘ f) s
[REAL_SUM_IMAGE_INTER_ELIM] Theorem
⊢ ∀P. FINITE P ⇒
∀f P'. (∀x. x ∉ P' ⇒ f x = 0) ⇒ SIGMA f (P ∩ P') = SIGMA f P
[REAL_SUM_IMAGE_INTER_NONZERO] Theorem
⊢ ∀P. FINITE P ⇒ ∀f. SIGMA f (P ∩ (λp. f p ≠ 0)) = SIGMA f P
[REAL_SUM_IMAGE_INV_CARD_EQ_1] Theorem
⊢ ∀P. P ≠ ∅ ∧ FINITE P ⇒
SIGMA (λs. if s ∈ P then (&CARD P)⁻¹ else 0) P = 1
[REAL_SUM_IMAGE_IN_IF] Theorem
⊢ ∀P. FINITE P ⇒
∀f. SIGMA f P = SIGMA (λx. if x ∈ P then f x else 0) P
[REAL_SUM_IMAGE_IN_IF_ALT] Theorem
⊢ ∀s f z.
FINITE s ⇒ SIGMA f s = SIGMA (λx. if x ∈ s then f x else z) s
[REAL_SUM_IMAGE_MONO] Theorem
⊢ ∀P. FINITE P ⇒
∀f f'. (∀x. x ∈ P ⇒ f x ≤ f' x) ⇒ SIGMA f P ≤ SIGMA f' P
[REAL_SUM_IMAGE_MONO_LT] Theorem
⊢ ∀f g s.
FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ∧ (∃x. x ∈ s ∧ f x < g x) ⇒
SIGMA f s < SIGMA g s
[REAL_SUM_IMAGE_MONO_SET] Theorem
⊢ ∀f s t.
FINITE s ∧ FINITE t ∧ s ⊆ t ∧ (∀x. x ∈ t ⇒ 0 ≤ f x) ⇒
SIGMA f s ≤ SIGMA f t
[REAL_SUM_IMAGE_NEG] Theorem
⊢ ∀P. FINITE P ⇒ ∀f. SIGMA (λx. -f x) P = -SIGMA f P
[REAL_SUM_IMAGE_NONZERO] Theorem
⊢ ∀P. FINITE P ⇒
∀f. (∀x. x ∈ P ⇒ 0 ≤ f x) ∧ (∃x. x ∈ P ∧ f x ≠ 0) ⇒
(SIGMA f P ≠ 0 ⇔ P ≠ ∅)
[REAL_SUM_IMAGE_PERMUTES] Theorem
⊢ ∀f p s. FINITE s ∧ p PERMUTES s ⇒ SIGMA f s = SIGMA (f ∘ p) s
[REAL_SUM_IMAGE_POS] Theorem
⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ SIGMA f s
[REAL_SUM_IMAGE_POS_LT] Theorem
⊢ ∀f s.
FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ∧ (∃x. x ∈ s ∧ 0 < f x) ⇒
0 < SIGMA f s
[REAL_SUM_IMAGE_POS_MEM_LE] Theorem
⊢ ∀P. FINITE P ⇒
∀f. (∀x. x ∈ P ⇒ 0 ≤ f x) ⇒ ∀x. x ∈ P ⇒ f x ≤ SIGMA f P
[REAL_SUM_IMAGE_POW] Theorem
⊢ ∀a s. FINITE s ⇒ (SIGMA a s)² = SIGMA (λ(i,j). a i * a j) (s × s)
[REAL_SUM_IMAGE_REAL_SUM_IMAGE] Theorem
⊢ ∀s s' f.
FINITE s ∧ FINITE s' ⇒
SIGMA (λx. SIGMA (f x) s') s =
SIGMA (λx. f (FST x) (SND x)) (s × s')
[REAL_SUM_IMAGE_SING] Theorem
⊢ ∀f e. SIGMA f {e} = f e
[REAL_SUM_IMAGE_SPOS] Theorem
⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ∀f. (∀x. x ∈ s ⇒ 0 < f x) ⇒ 0 < SIGMA f s
[REAL_SUM_IMAGE_SUB] Theorem
⊢ ∀s f f'.
FINITE s ⇒ SIGMA (λx. f x − f' x) s = SIGMA f s − SIGMA f' s
[REAL_SUM_IMAGE_SWAP] Theorem
⊢ ∀f s t.
FINITE s ∧ FINITE t ⇒
SIGMA (λi. SIGMA (f i) t) s = SIGMA (λj. SIGMA (λi. f i j) s) t
[REAL_SUM_IMAGE_THM] Theorem
⊢ ∀f. SIGMA f ∅ = 0 ∧
∀e s.
FINITE s ⇒ SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e)
[REAL_SUM_IMAGE_sum] Theorem
⊢ ∀f s. FINITE s ⇒ SIGMA f s = sum s f
[REAL_SUP_ASCLOSE] Theorem
⊢ ∀s l e. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ abs (x − l) ≤ e) ⇒ abs (sup s − l) ≤ e
[REAL_SUP_BOUNDS] Theorem
⊢ ∀s a b. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ a ≤ x ∧ x ≤ b) ⇒ a ≤ sup s ∧ sup s ≤ b
[REAL_SUP_EQ_INF] Theorem
⊢ ∀s. s ≠ ∅ ∧ (∃B. ∀x. x ∈ s ⇒ abs x ≤ B) ⇒
(sup s = inf s ⇔ ∃a. s = {a})
[REAL_SUP_LE'] Theorem
⊢ ∀s b. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ x ≤ b) ⇒ sup s ≤ b
[REAL_SUP_LE_EQ] Theorem
⊢ ∀s y.
s ≠ ∅ ∧ (∃b. ∀x. x ∈ s ⇒ x ≤ b) ⇒ (sup s ≤ y ⇔ ∀x. x ∈ s ⇒ x ≤ y)
[REAL_SUP_LE_FINITE] Theorem
⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (sup s ≤ a ⇔ ∀x. x ∈ s ⇒ x ≤ a)
[REAL_SUP_LE_SUBSET] Theorem
⊢ ∀s t. s ≠ ∅ ∧ s ⊆ t ∧ (∃b. ∀x. x ∈ t ⇒ x ≤ b) ⇒ sup s ≤ sup t
[REAL_SUP_LE_X] Theorem
⊢ ∀P x. (∃r. P r) ∧ (∀r. P r ⇒ r ≤ x) ⇒ sup P ≤ x
[REAL_SUP_LT_FINITE] Theorem
⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (sup s < a ⇔ ∀x. x ∈ s ⇒ x < a)
[REAL_SUP_UNIQUE] Theorem
⊢ ∀s b.
(∀x. x ∈ s ⇒ x ≤ b) ∧ (∀b'. b' < b ⇒ ∃x. x ∈ s ∧ b' < x) ⇒
sup s = b
[REAL_WLOG_LE] Theorem
⊢ (∀x y. P x y ⇔ P y x) ∧ (∀x y. x ≤ y ⇒ P x y) ⇒ ∀x y. P x y
[REAL_WLOG_LT] Theorem
⊢ (∀x. P x x) ∧ (∀x y. P x y ⇔ P y x) ∧ (∀x y. x < y ⇒ P x y) ⇒
∀x y. P x y
[REAL_X_LE_SUP] Theorem
⊢ ∀P x.
(∃r. P r) ∧ (∃z. ∀r. P r ⇒ r ≤ z) ∧ (∃r. P r ∧ x ≤ r) ⇒ x ≤ sup P
[SUMS_SYM] Theorem
⊢ ∀s t. {x + y | x ∈ s ∧ y ∈ t} = {y + x | y ∈ t ∧ x ∈ s}
[SUM_0'] Theorem
⊢ ∀s. sum s (λn. 0) = 0
[SUM_ABS'] Theorem
⊢ ∀f s. FINITE s ⇒ abs (sum s f) ≤ sum s (λx. abs (f x))
[SUM_ABS_BOUND] Theorem
⊢ ∀s f b.
FINITE s ∧ (∀x. x ∈ s ⇒ abs (f x) ≤ b) ⇒
abs (sum s f) ≤ &CARD s * b
[SUM_ABS_LE'] Theorem
⊢ ∀f g s.
FINITE s ∧ (∀x. x ∈ s ⇒ abs (f x) ≤ g x) ⇒
abs (sum s f) ≤ sum s g
[SUM_ABS_NUMSEG] Theorem
⊢ ∀f m n. abs (sum {m .. n} f) ≤ sum {m .. n} (λi. abs (f i))
[SUM_ABS_TRIANGLE] Theorem
⊢ ∀s f b. FINITE s ∧ sum s (λa. abs (f a)) ≤ b ⇒ abs (sum s f) ≤ b
[SUM_ADD'] Theorem
⊢ ∀f g s. FINITE s ⇒ sum s (λx. f x + g x) = sum s f + sum s g
[SUM_ADD_COUNT] Theorem
⊢ ∀f g n.
sum (count n) (λx. f x + g x) = sum (count n) f + sum (count n) g
[SUM_ADD_GEN] Theorem
⊢ ∀f g s.
FINITE {x | x ∈ s ∧ f x ≠ 0} ∧ FINITE {x | x ∈ s ∧ g x ≠ 0} ⇒
sum s (λx. f x + g x) = sum s f + sum s g
[SUM_ADD_NUMSEG] Theorem
⊢ ∀f g m n.
sum {m .. n} (λi. f i + g i) = sum {m .. n} f + sum {m .. n} g
[SUM_ADD_SPLIT] Theorem
⊢ ∀f m n p.
m ≤ n + 1 ⇒
sum {m .. n + p} f = sum {m .. n} f + sum {n + 1 .. n + p} f
[SUM_BIGUNION_NONZERO] Theorem
⊢ ∀f s.
FINITE s ∧ (∀t. t ∈ s ⇒ FINITE t) ∧
(∀t1 t2 x. t1 ∈ s ∧ t2 ∈ s ∧ t1 ≠ t2 ∧ x ∈ t1 ∧ x ∈ t2 ⇒ f x = 0) ⇒
sum (BIGUNION s) f = sum s (λt. sum t f)
[SUM_BIJECTION] Theorem
⊢ ∀f p s.
(∀x. x ∈ s ⇒ p x ∈ s) ∧ (∀y. y ∈ s ⇒ ∃!x. x ∈ s ∧ p x = y) ⇒
sum s f = sum s (f ∘ p)
[SUM_BOUND'] Theorem
⊢ ∀s f b. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ b) ⇒ sum s f ≤ &CARD s * b
[SUM_BOUND_GEN] Theorem
⊢ ∀s f b.
FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x ≤ b / &CARD s) ⇒ sum s f ≤ b
[SUM_BOUND_LT] Theorem
⊢ ∀s f b.
FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ b) ∧ (∃x. x ∈ s ∧ f x < b) ⇒
sum s f < &CARD s * b
[SUM_BOUND_LT_ALL] Theorem
⊢ ∀s f b.
FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < b) ⇒ sum s f < &CARD s * b
[SUM_BOUND_LT_GEN] Theorem
⊢ ∀s f b.
FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < b / &CARD s) ⇒ sum s f < b
[SUM_CASES] Theorem
⊢ ∀s P f g.
FINITE s ⇒
sum s (λx. if P x then f x else g x) =
sum {x | x ∈ s ∧ P x} f + sum {x | x ∈ s ∧ ¬P x} g
[SUM_CASES_1] Theorem
⊢ ∀s a.
FINITE s ∧ a ∈ s ⇒
sum s (λx. if x = a then y else f x) = sum s f + (y − f a)
[SUM_CLAUSES] Theorem
⊢ (∀f. sum ∅ f = 0) ∧
∀x f s.
FINITE s ⇒
sum (x INSERT s) f = if x ∈ s then sum s f else f x + sum s f
[SUM_CLAUSES_LEFT] Theorem
⊢ ∀f m n. m ≤ n ⇒ sum {m .. n} f = f m + sum {m + 1 .. n} f
[SUM_CLAUSES_NUMSEG] Theorem
⊢ (∀m. sum {m .. 0} f = if m = 0 then f 0 else 0) ∧
∀m n.
sum {m .. SUC n} f =
if m ≤ SUC n then sum {m .. n} f + f (SUC n) else sum {m .. n} f
[SUM_CLAUSES_RIGHT] Theorem
⊢ ∀f m n. 0 < n ∧ m ≤ n ⇒ sum {m .. n} f = sum {m .. n − 1} f + f n
[SUM_CLOSED] Theorem
⊢ ∀P f s.
P 0 ∧ (∀x y. P x ∧ P y ⇒ P (x + y)) ∧ (∀a. a ∈ s ⇒ P (f a)) ⇒
P (sum s f)
[SUM_COMBINE_L] Theorem
⊢ ∀f m n p.
0 < n ∧ m ≤ n ∧ n ≤ p + 1 ⇒
sum {m .. n − 1} f + sum {n .. p} f = sum {m .. p} f
[SUM_COMBINE_R] Theorem
⊢ ∀f m n p.
m ≤ n + 1 ∧ n ≤ p ⇒
sum {m .. n} f + sum {n + 1 .. p} f = sum {m .. p} f
[SUM_CONG] Theorem
⊢ (∀f g s. (∀x. x ∈ s ⇒ f x = g x) ⇒ sum s (λi. f i) = sum s g) ∧
(∀f g a b.
(∀i. a ≤ i ∧ i ≤ b ⇒ f i = g i) ⇒
sum {a .. b} (λi. f i) = sum {a .. b} g) ∧
∀f g p.
(∀x. p x ⇒ f x = g x) ⇒ sum {y | p y} (λi. f i) = sum {y | p y} g
[SUM_CONST] Theorem
⊢ ∀c s. FINITE s ⇒ sum s (λn. c) = &CARD s * c
[SUM_CONST_NUMSEG] Theorem
⊢ ∀c m n. sum {m .. n} (λn. c) = &(n + 1 − m) * c
[SUM_DEGENERATE] Theorem
⊢ ∀f s. INFINITE {x | x ∈ s ∧ f x ≠ 0} ⇒ sum s f = 0
[SUM_DELETE] Theorem
⊢ ∀f s a. FINITE s ∧ a ∈ s ⇒ sum (s DELETE a) f = sum s f − f a
[SUM_DELETE_CASES] Theorem
⊢ ∀f s a.
FINITE s ⇒
sum (s DELETE a) f = if a ∈ s then sum s f − f a else sum s f
[SUM_DELTA] Theorem
⊢ ∀s a. sum s (λx. if x = a then b else 0) = if a ∈ s then b else 0
[SUM_DIFF'] Theorem
⊢ ∀f s t. FINITE s ∧ t ⊆ s ⇒ sum (s DIFF t) f = sum s f − sum t f
[SUM_DIFFS'] Theorem
⊢ ∀m n.
sum {m .. n} (λk. f k − f (k + 1)) =
if m ≤ n then f m − f (n + 1) else 0
[SUM_DIFFS_ALT] Theorem
⊢ ∀m n.
sum {m .. n} (λk. f (k + 1) − f k) =
if m ≤ n then f (n + 1) − f m else 0
[SUM_EQ'] Theorem
⊢ ∀f g s. (∀x. x ∈ s ⇒ f x = g x) ⇒ sum s f = sum s g
[SUM_EQ_0'] Theorem
⊢ ∀f s. (∀x. x ∈ s ⇒ f x = 0) ⇒ sum s f = 0
[SUM_EQ_0_NUMSEG] Theorem
⊢ ∀f m n. (∀i. m ≤ i ∧ i ≤ n ⇒ f i = 0) ⇒ sum {m .. n} f = 0
[SUM_EQ_COUNT] Theorem
⊢ ∀f g n. (∀i. i < n ⇒ f i = g i) ⇒ sum (count n) f = sum (count n) g
[SUM_EQ_GENERAL] Theorem
⊢ ∀s t f g h.
(∀y. y ∈ t ⇒ ∃!x. x ∈ s ∧ h x = y) ∧
(∀x. x ∈ s ⇒ h x ∈ t ∧ g (h x) = f x) ⇒
sum s f = sum t g
[SUM_EQ_GENERAL_INVERSES] Theorem
⊢ ∀s t f g h k.
(∀y. y ∈ t ⇒ k y ∈ s ∧ h (k y) = y) ∧
(∀x. x ∈ s ⇒ h x ∈ t ∧ k (h x) = x ∧ g (h x) = f x) ⇒
sum s f = sum t g
[SUM_EQ_NUMSEG] Theorem
⊢ ∀f g m n.
(∀i. m ≤ i ∧ i ≤ n ⇒ f i = g i) ⇒ sum {m .. n} f = sum {m .. n} g
[SUM_EQ_SUPERSET] Theorem
⊢ ∀f s t.
FINITE t ∧ t ⊆ s ∧ (∀x. x ∈ t ⇒ f x = g x) ∧
(∀x. x ∈ s ∧ x ∉ t ⇒ f x = 0) ⇒
sum s f = sum t g
[SUM_GP] Theorem
⊢ ∀x m n.
sum {m .. n} (λi. x pow i) =
if n < m then 0
else if x = 1 then &(n + 1 − m)
else (x pow m − x pow SUC n) / (1 − x)
[SUM_GP_BASIC] Theorem
⊢ ∀x n. (1 − x) * sum {0 .. n} (λi. x pow i) = 1 − x pow SUC n
[SUM_GP_MULTIPLIED] Theorem
⊢ ∀x m n.
m ≤ n ⇒
(1 − x) * sum {m .. n} (λi. x pow i) = x pow m − x pow SUC n
[SUM_GROUP'] Theorem
⊢ ∀f g s t.
FINITE s ∧ IMAGE f s ⊆ t ⇒
sum t (λy. sum {x | x ∈ s ∧ f x = y} g) = sum s g
[SUM_IMAGE] Theorem
⊢ ∀f g s.
(∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒
sum (IMAGE f s) g = sum s (g ∘ f)
[SUM_IMAGE_GEN] Theorem
⊢ ∀f g s.
FINITE s ⇒
sum s g = sum (IMAGE f s) (λy. sum {x | x ∈ s ∧ f x = y} g)
[SUM_IMAGE_LE] Theorem
⊢ ∀f g s.
FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ g (f x)) ⇒
sum (IMAGE f s) g ≤ sum s (g ∘ f)
[SUM_IMAGE_NONZERO] Theorem
⊢ ∀d i s.
FINITE s ∧
(∀x y. x ∈ s ∧ y ∈ s ∧ x ≠ y ∧ i x = i y ⇒ d (i x) = 0) ⇒
sum (IMAGE i s) d = sum s (d ∘ i)
[SUM_INCL_EXCL] Theorem
⊢ ∀s t f.
FINITE s ∧ FINITE t ⇒
sum s f + sum t f = sum (s ∪ t) f + sum (s ∩ t) f
[SUM_INJECTION] Theorem
⊢ ∀f p s.
FINITE s ∧ (∀x. x ∈ s ⇒ p x ∈ s) ∧
(∀x y. x ∈ s ∧ y ∈ s ∧ p x = p y ⇒ x = y) ⇒
sum s (f ∘ p) = sum s f
[SUM_LE'] Theorem
⊢ ∀f g s. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒ sum s f ≤ sum s g
[SUM_LE_INCLUDED] Theorem
⊢ ∀f g s t i.
FINITE s ∧ FINITE t ∧ (∀y. y ∈ t ⇒ 0 ≤ g y) ∧
(∀x. x ∈ s ⇒ ∃y. y ∈ t ∧ i y = x ∧ f x ≤ g y) ⇒
sum s f ≤ sum t g
[SUM_LE_NUMSEG] Theorem
⊢ ∀f g m n.
(∀i. m ≤ i ∧ i ≤ n ⇒ f i ≤ g i) ⇒ sum {m .. n} f ≤ sum {m .. n} g
[SUM_LMUL] Theorem
⊢ ∀f c s. sum s (λx. c * f x) = c * sum s f
[SUM_LT'] Theorem
⊢ ∀f g s.
FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ∧ (∃x. x ∈ s ∧ f x < g x) ⇒
sum s f < sum s g
[SUM_LT_ALL] Theorem
⊢ ∀f g s.
FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < g x) ⇒ sum s f < sum s g
[SUM_MULTICOUNT] Theorem
⊢ ∀R s t k.
FINITE s ∧ FINITE t ∧ (∀j. j ∈ t ⇒ CARD {i | i ∈ s ∧ R i j} = k) ⇒
sum s (λi. &CARD (equiv_class R t i)) = &(k * CARD t)
[SUM_MULTICOUNT_GEN] Theorem
⊢ ∀R s t k.
FINITE s ∧ FINITE t ∧
(∀j. j ∈ t ⇒ CARD {i | i ∈ s ∧ R i j} = k j) ⇒
sum s (λi. &CARD (equiv_class R t i)) = sum t (λi. &k i)
[SUM_NEG'] Theorem
⊢ ∀f s. sum s (λx. -f x) = -sum s f
[SUM_OFFSET'] Theorem
⊢ ∀p f m n. sum {m + p .. n + p} f = sum {m .. n} (λi. f (i + p))
[SUM_OFFSET_0] Theorem
⊢ ∀f m n. m ≤ n ⇒ sum {m .. n} f = sum {0 .. n − m} (λi. f (i + m))
[SUM_PAIR] Theorem
⊢ ∀f m n.
sum {2 * m .. 2 * n + 1} f =
sum {m .. n} (λi. f (2 * i) + f (2 * i + 1))
[SUM_PARTIAL_PRE] Theorem
⊢ ∀f g m n.
sum {m .. n} (λk. f k * (g k − g (k − 1))) =
if m ≤ n then
f (n + 1) * g n − f m * g (m − 1) −
sum {m .. n} (λk. g k * (f (k + 1) − f k))
else 0
[SUM_PARTIAL_SUC] Theorem
⊢ ∀f g m n.
sum {m .. n} (λk. f k * (g (k + 1) − g k)) =
if m ≤ n then
f (n + 1) * g (n + 1) − f m * g m −
sum {m .. n} (λk. g (k + 1) * (f (k + 1) − f k))
else 0
[SUM_PERMUTATIONS_COMPOSE_L] Theorem
⊢ ∀f s q.
q permutes s ⇒
sum {p | p permutes s} f = sum {p | p permutes s} (λp. f (q ∘ p))
[SUM_PERMUTATIONS_COMPOSE_L_COUNT] Theorem
⊢ ∀f n q.
q permutes count n ⇒
sum {p | p permutes count n} f =
sum {p | p permutes count n} (λp. f (q ∘ p))
[SUM_PERMUTATIONS_COMPOSE_L_NUMSEG] Theorem
⊢ ∀f m n q.
q permutes count n DIFF count m ⇒
sum {p | p permutes count n DIFF count m} f =
sum {p | p permutes count n DIFF count m} (λp. f (q ∘ p))
[SUM_PERMUTATIONS_COMPOSE_R] Theorem
⊢ ∀f s q.
q permutes s ⇒
sum {p | p permutes s} f = sum {p | p permutes s} (λp. f (p ∘ q))
[SUM_PERMUTATIONS_COMPOSE_R_COUNT] Theorem
⊢ ∀f n q.
q permutes count n ⇒
sum {p | p permutes count n} f =
sum {p | p permutes count n} (λp. f (p ∘ q))
[SUM_PERMUTATIONS_COMPOSE_R_NUMSEG] Theorem
⊢ ∀f m n q.
q permutes count n DIFF count m ⇒
sum {p | p permutes count n DIFF count m} f =
sum {p | p permutes count n DIFF count m} (λp. f (p ∘ q))
[SUM_PERMUTATIONS_INVERSE] Theorem
⊢ ∀f n.
sum {p | p permutes count n} f =
sum {p | p permutes count n} (λp. f (inverse p))
[SUM_PERMUTE] Theorem
⊢ ∀f p s. p permutes s ⇒ sum s f = sum s (f ∘ p)
[SUM_PERMUTE_COUNT] Theorem
⊢ ∀f p n.
p permutes count n ⇒ sum (count n) f = sum (count n) (f ∘ p)
[SUM_PERMUTE_NUMSEG] Theorem
⊢ ∀f p m n.
p permutes count n DIFF count m ⇒
sum (count n DIFF count m) f = sum (count n DIFF count m) (f ∘ p)
[SUM_POS_BOUND] Theorem
⊢ ∀f b s.
FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ∧ sum s f ≤ b ⇒
∀x. x ∈ s ⇒ f x ≤ b
[SUM_POS_EQ_0] Theorem
⊢ ∀f s.
FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ∧ sum s f = 0 ⇒
∀x. x ∈ s ⇒ f x = 0
[SUM_POS_EQ_0_NUMSEG] Theorem
⊢ ∀f m n.
(∀p. m ≤ p ∧ p ≤ n ⇒ 0 ≤ f p) ∧ sum {m .. n} f = 0 ⇒
∀p. m ≤ p ∧ p ≤ n ⇒ f p = 0
[SUM_POS_LE] Theorem
⊢ ∀s. (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ sum s f
[SUM_POS_LE_NUMSEG] Theorem
⊢ ∀m n f. (∀p. m ≤ p ∧ p ≤ n ⇒ 0 ≤ f p) ⇒ 0 ≤ sum {m .. n} f
[SUM_POS_LT] Theorem
⊢ ∀f s.
FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ∧ (∃x. x ∈ s ∧ 0 < f x) ⇒
0 < sum s f
[SUM_POS_LT_ALL] Theorem
⊢ ∀s f. FINITE s ∧ s ≠ ∅ ∧ (∀i. i ∈ s ⇒ 0 < f i) ⇒ 0 < sum s f
[SUM_RESTRICT] Theorem
⊢ ∀f s. FINITE s ⇒ sum s (λx. if x ∈ s then f x else 0) = sum s f
[SUM_RESTRICT_SET] Theorem
⊢ ∀P s f.
sum {x | x ∈ s ∧ P x} f = sum s (λx. if P x then f x else 0)
[SUM_RMUL] Theorem
⊢ ∀f c s. sum s (λx. f x * c) = sum s f * c
[SUM_SING] Theorem
⊢ ∀f x. sum {x} f = f x
[SUM_SING_NUMSEG] Theorem
⊢ ∀f n. sum {n .. n} f = f n
[SUM_SUB'] Theorem
⊢ ∀f g s. FINITE s ⇒ sum s (λx. f x − g x) = sum s f − sum s g
[SUM_SUBSET] Theorem
⊢ ∀u v f.
FINITE u ∧ FINITE v ∧ (∀x. x ∈ u DIFF v ⇒ f x ≤ 0) ∧
(∀x. x ∈ v DIFF u ⇒ 0 ≤ f x) ⇒
sum u f ≤ sum v f
[SUM_SUBSET_SIMPLE] Theorem
⊢ ∀u v f.
FINITE v ∧ u ⊆ v ∧ (∀x. x ∈ v DIFF u ⇒ 0 ≤ f x) ⇒
sum u f ≤ sum v f
[SUM_SUB_NUMSEG] Theorem
⊢ ∀f g m n.
sum {m .. n} (λi. f i − g i) = sum {m .. n} f − sum {m .. n} g
[SUM_SUM_PRODUCT] Theorem
⊢ ∀s t x.
FINITE s ∧ (∀i. i ∈ s ⇒ FINITE (t i)) ⇒
sum s (λi. sum (t i) (x i)) =
sum {(i,j) | i ∈ s ∧ j ∈ t i} (λ(i,j). x i j)
[SUM_SUM_RESTRICT] Theorem
⊢ ∀R f s t.
FINITE s ∧ FINITE t ⇒
sum s (λx. sum (equiv_class R t x) (λy. f x y)) =
sum t (λy. sum {x | x ∈ s ∧ R x y} (λx. f x y))
[SUM_SUPERSET] Theorem
⊢ ∀f u v. u ⊆ v ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ f x = 0) ⇒ sum v f = sum u f
[SUM_SUPPORT] Theorem
⊢ ∀f s. sum (support $+ f s) f = sum s f
[SUM_SWAP] Theorem
⊢ ∀f s t.
FINITE s ∧ FINITE t ⇒
sum s (λi. sum t (f i)) = sum t (λj. sum s (λi. f i j))
[SUM_SWAP_COUNT] Theorem
⊢ ∀f m n.
sum (count m) (λi. sum (count n) (f i)) =
sum (count n) (λj. sum (count m) (λi. f i j))
[SUM_SWAP_NUMSEG] Theorem
⊢ ∀a b c d f.
sum {a .. b} (λi. sum {c .. d} (f i)) =
sum {c .. d} (λj. sum {a .. b} (λi. f i j))
[SUM_TRIV_NUMSEG] Theorem
⊢ ∀f m n. n < m ⇒ sum {m .. n} f = 0
[SUM_UNION] Theorem
⊢ ∀f s t.
FINITE s ∧ FINITE t ∧ DISJOINT s t ⇒
sum (s ∪ t) f = sum s f + sum t f
[SUM_UNION_EQ] Theorem
⊢ ∀s t u.
FINITE u ∧ s ∩ t = ∅ ∧ s ∪ t = u ⇒ sum s f + sum t f = sum u f
[SUM_UNION_LZERO] Theorem
⊢ ∀f u v.
FINITE v ∧ (∀x. x ∈ u ∧ x ∉ v ⇒ f x = 0) ⇒
sum (u ∪ v) f = sum v f
[SUM_UNION_NONZERO] Theorem
⊢ ∀f s t.
FINITE s ∧ FINITE t ∧ (∀x. x ∈ s ∩ t ⇒ f x = 0) ⇒
sum (s ∪ t) f = sum s f + sum t f
[SUM_UNION_RZERO] Theorem
⊢ ∀f u v.
FINITE u ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ f x = 0) ⇒
sum (u ∪ v) f = sum u f
[SUM_ZERO_EXISTS] Theorem
⊢ ∀u s.
FINITE s ∧ sum s u = 0 ⇒
(∀i. i ∈ s ⇒ u i = 0) ∨ ∃j k. j ∈ s ∧ u j < 0 ∧ k ∈ s ∧ u k > 0
[SUP] Theorem
⊢ ∀s. s ≠ ∅ ∧ (∃b. ∀x. x ∈ s ⇒ x ≤ b) ⇒
(∀x. x ∈ s ⇒ x ≤ sup s) ∧ ∀b. (∀x. x ∈ s ⇒ x ≤ b) ⇒ sup s ≤ b
[SUP_EQ] Theorem
⊢ ∀s t. (∀b. (∀x. x ∈ s ⇒ x ≤ b) ⇔ ∀x. x ∈ t ⇒ x ≤ b) ⇒ sup s = sup t
[SUP_FINITE] Theorem
⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ sup s ∈ s ∧ ∀x. x ∈ s ⇒ x ≤ sup s
[SUP_FINITE_LEMMA] Theorem
⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ∃b. b ∈ s ∧ ∀x. x ∈ s ⇒ x ≤ b
[SUP_INSERT_FINITE] Theorem
⊢ ∀x s.
FINITE s ⇒ sup (x INSERT s) = if s = ∅ then x else max x (sup s)
[SUP_MONO] Theorem
⊢ ∀p q.
(∃b. ∀n. p n ≤ b) ∧ (∃c. ∀n. q n ≤ c) ∧ (∀n. p n ≤ q n) ⇒
sup (IMAGE p 𝕌(:num)) ≤ sup (IMAGE q 𝕌(:num))
[SUP_SING] Theorem
⊢ ∀a. sup {a} = a
[SUP_UNION] Theorem
⊢ ∀s t.
s ≠ ∅ ∧ t ≠ ∅ ∧ (∃b. ∀x. x ∈ s ⇒ x ≤ b) ∧ (∃c. ∀x. x ∈ t ⇒ x ≤ c) ⇒
sup (s ∪ t) = max (sup s) (sup t)
[SUP_UNIQUE] Theorem
⊢ ∀s b. (∀c. (∀x. x ∈ s ⇒ x ≤ c) ⇔ b ≤ c) ⇒ sup s = b
[SUP_UNIQUE_FINITE] Theorem
⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ (sup s = a ⇔ a ∈ s ∧ ∀y. y ∈ s ⇒ y ≤ a)
[UPPER_BOUND_FINITE_SET_REAL] Theorem
⊢ ∀f s. FINITE s ⇒ ∃a. ∀x. x ∈ s ⇒ f x ≤ a
[inf_alt] Theorem
⊢ ∀s. s ≠ ∅ ∧ (∃b. ∀x. x ∈ s ⇒ b ≤ x) ⇒
inf s =
@a. (∀x. x ∈ s ⇒ a ≤ x) ∧ ∀b. (∀x. x ∈ s ⇒ b ≤ x) ⇒ b ≤ a
[jensen_concave_SIGMA] Theorem
⊢ ∀s. FINITE s ⇒
∀f g g'.
SIGMA g s = 1 ∧ (∀x. x ∈ s ⇒ 0 ≤ g x ∧ g x ≤ 1) ∧
f ∈ concave_fn ⇒
SIGMA (λx. g x * f (g' x)) s ≤ f (SIGMA (λx. g x * g' x) s)
[jensen_convex_SIGMA] Theorem
⊢ ∀s. FINITE s ⇒
∀f g g'.
SIGMA g s = 1 ∧ (∀x. x ∈ s ⇒ 0 ≤ g x ∧ g x ≤ 1) ∧
f ∈ convex_fn ⇒
f (SIGMA (λx. g x * g' x) s) ≤ SIGMA (λx. g x * f (g' x)) s
[jensen_pos_concave_SIGMA] Theorem
⊢ ∀s. FINITE s ⇒
∀f g g'.
SIGMA g s = 1 ∧ (∀x. x ∈ s ⇒ 0 ≤ g x ∧ g x ≤ 1) ∧
(∀x. x ∈ s ⇒ 0 < g x ⇒ 0 < g' x) ∧ f ∈ pos_concave_fn ⇒
SIGMA (λx. g x * f (g' x)) s ≤ f (SIGMA (λx. g x * g' x) s)
[jensen_pos_convex_SIGMA] Theorem
⊢ ∀s. FINITE s ⇒
∀f g g'.
SIGMA g s = 1 ∧ (∀x. x ∈ s ⇒ 0 ≤ g x ∧ g x ≤ 1) ∧
(∀x. x ∈ s ⇒ 0 < g x ⇒ 0 < g' x) ∧ f ∈ pos_convex_fn ⇒
f (SIGMA (λx. g x * g' x) s) ≤ SIGMA (λx. g x * f (g' x)) s
[real_INFINITE] Theorem
⊢ INFINITE 𝕌(:real)
[sum_real] Theorem
⊢ ∀f n. sum {0 .. n} f = sum (0,SUC n) f
[sup_alt] Theorem
⊢ sup s = @a. (∀x. x ∈ s ⇒ x ≤ a) ∧ ∀b. (∀x. x ∈ s ⇒ x ≤ b) ⇒ a ≤ b
*)
end
HOL 4, Trindemossen-2