Theory "real_sigma"

Signature

Definitions

REAL_SUM_IMAGE_DEF

|- ∀f s. SIGMA f s = ITSET (λe acc. f e + acc) s 0

Theorems

REAL_SUM_IMAGE_THM

|- ∀f.
     (SIGMA f ∅ = 0) ∧
     ∀e s. FINITE s ⇒ (SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e))

REAL_SUM_IMAGE_SING

|- ∀f e. SIGMA f {e} = f e

REAL_SUM_IMAGE_POS

|- ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ SIGMA f s

REAL_SUM_IMAGE_SPOS

|- ∀s. FINITE s ∧ s ≠ ∅ ⇒ ∀f. (∀x. x ∈ s ⇒ 0 < f x) ⇒ 0 < SIGMA f s

REAL_SUM_IMAGE_NONZERO

|- ∀P.
     FINITE P ⇒
     ∀f.
       (∀x. x ∈ P ⇒ 0 ≤ f x) ∧ (∃x. x ∈ P ∧ f x ≠ 0) ⇒ (SIGMA f P ≠ 0 ⇔ P ≠ ∅)

REAL_SUM_IMAGE_IF_ELIM

|- ∀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_FINITE_SAME

|- ∀P.
     FINITE P ⇒
     ∀f p. p ∈ P ∧ (∀q. q ∈ P ⇒ (f p = f q)) ⇒ (SIGMA f P = &CARD P * f p)

REAL_SUM_IMAGE_FINITE_CONST

|- ∀P. FINITE P ⇒ ∀f x. (∀y. f y = x) ⇒ (SIGMA f P = &CARD P * x)

REAL_SUM_IMAGE_IN_IF

|- ∀P. FINITE P ⇒ ∀f. SIGMA f P = SIGMA (λx. if x ∈ P then f x else 0) P

REAL_SUM_IMAGE_CMUL

|- ∀P. FINITE P ⇒ ∀f c. SIGMA (λx. c * f x) P = c * SIGMA f P

REAL_SUM_IMAGE_NEG

|- ∀P. FINITE P ⇒ ∀f. SIGMA (λx. -f x) P = -SIGMA f P

REAL_SUM_IMAGE_IMAGE

|- ∀P.
     FINITE P ⇒
     ∀f'. INJ f' P (IMAGE f' P) ⇒ ∀f. SIGMA f (IMAGE f' P) = SIGMA (f o f') P

REAL_SUM_IMAGE_DISJOINT_UNION

|- ∀P P'.
     FINITE P ∧ FINITE P' ∧ DISJOINT P P' ⇒
     ∀f. SIGMA f (P ∪ P') = SIGMA f P + SIGMA f P'

REAL_SUM_IMAGE_EQ_CARD

|- ∀P. FINITE P ⇒ (SIGMA (λx. if x ∈ P then 1 else 0) P = &CARD P)

REAL_SUM_IMAGE_INV_CARD_EQ_1

|- ∀P.
     P ≠ ∅ ∧ FINITE P ⇒ (SIGMA (λs. if s ∈ P then inv (&CARD P) else 0) P = 1)

REAL_SUM_IMAGE_INTER_NONZERO

|- ∀P. FINITE P ⇒ ∀f. SIGMA f (P ∩ (λp. f p ≠ 0)) = SIGMA f P

REAL_SUM_IMAGE_INTER_ELIM

|- ∀P.
     FINITE P ⇒
     ∀f P'. (∀x. x ∉ P' ⇒ (f x = 0)) ⇒ (SIGMA f (P ∩ P') = SIGMA f P)

REAL_SUM_IMAGE_COUNT

|- ∀f n. SIGMA f (count n) = sum (0,n) f

REAL_SUM_IMAGE_MONO

|- ∀P. FINITE P ⇒ ∀f f'. (∀x. x ∈ P ⇒ f x ≤ f' x) ⇒ SIGMA f P ≤ SIGMA f' P

REAL_SUM_IMAGE_POS_MEM_LE

|- ∀P. FINITE P ⇒ ∀f. (∀x. x ∈ P ⇒ 0 ≤ f x) ⇒ ∀x. x ∈ P ⇒ f x ≤ SIGMA f P

REAL_SUM_IMAGE_CONST_EQ_1_EQ_INV_CARD

|- ∀P.
     FINITE P ⇒
     ∀f.
       (SIGMA f P = 1) ∧ (∀x y. x ∈ P ∧ y ∈ P ⇒ (f x = f y)) ⇒
       ∀x. x ∈ P ⇒ (f x = inv (&CARD P))

REAL_SUM_IMAGE_ADD

|- ∀s. FINITE s ⇒ ∀f f'. SIGMA (λx. f x + f' x) s = SIGMA f s + SIGMA f' s

REAL_SUM_IMAGE_REAL_SUM_IMAGE

|- ∀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_0

|- ∀s. FINITE s ⇒ (SIGMA (λx. 0) s = 0)

SEQ_REAL_SUM_IMAGE

|- ∀s.
     FINITE s ⇒
     ∀f f'.
       (∀x. x ∈ s ⇒ (λn. f n x) --> f' x) ⇒ (λn. SIGMA (f n) s) --> SIGMA f' s

NESTED_REAL_SUM_IMAGE_REVERSE

|- ∀f s s'.
     FINITE s ∧ FINITE s' ⇒
     (SIGMA (λx. SIGMA (f x) s') s = SIGMA (λx. SIGMA (λy. f y x) s) s')

REAL_SUM_IMAGE_EQ_sum

|- ∀n r. sum (0,n) r = SIGMA r (count n)

REAL_SUM_IMAGE_POW

|- ∀a s. FINITE s ⇒ (SIGMA a s pow 2 = SIGMA (λ(i,j). a i * a j) (s × s))

REAL_SUM_IMAGE_EQ

|- ∀s f f'. FINITE s ∧ (∀x. x ∈ s ⇒ (f x = f' x)) ⇒ (SIGMA f s = SIGMA f' s)

REAL_SUM_IMAGE_IN_IF_ALT

|- ∀s f z. FINITE s ⇒ (SIGMA f s = SIGMA (λx. if x ∈ s then f x else z) s)

REAL_SUM_IMAGE_SUB

|- ∀s f f'. FINITE s ⇒ (SIGMA (λx. f x − f' x) s = SIGMA f s − SIGMA f' s)

REAL_SUM_IMAGE_MONO_SET

|- ∀f s t.
     FINITE s ∧ FINITE t ∧ s ⊆ t ∧ (∀x. x ∈ t ⇒ 0 ≤ f x) ⇒
     SIGMA f s ≤ SIGMA f t

REAL_SUM_IMAGE_CROSS_SYM

|- ∀f s1 s2.
     FINITE s1 ∧ FINITE s2 ⇒
     (SIGMA (λ(x,y). f (x,y)) (s1 × s2) = SIGMA (λ(y,x). f (x,y)) (s2 × s1))