Theory "real_sigma"

Signature

Definitions

REAL_SUM_IMAGE_DEF

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

Theorems

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

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_SUB

⊢ ∀s f f'. FINITE s ⇒ (SIGMA (λx. f x − f' x) s = SIGMA f s − 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_SING

⊢ ∀f e. SIGMA f {e} = f e

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_POW

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

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_POS

⊢ ∀f s. FINITE s ∧ (∀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_NEG

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

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_MONO

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

REAL_SUM_IMAGE_INV_CARD_EQ_1

⊢ ∀P. P ≠ ∅ ∧ FINITE P ⇒ (SIGMA (λs. if s ∈ P then (&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_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_IN_IF

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

REAL_SUM_IMAGE_IMAGE

⊢ ∀P.
      FINITE P ⇒
      ∀f'. INJ f' P (IMAGE f' P) ⇒ ∀f. SIGMA f (IMAGE f' P) = SIGMA (f ∘ f') 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_CONST3

⊢ ∀P. FINITE P ⇒ ∀c. SIGMA (λx. c) P = &CARD P * c

REAL_SUM_IMAGE_FINITE_CONST2

⊢ ∀P. FINITE P ⇒ ∀f x. (∀y. y ∈ P ⇒ (f y = x)) ⇒ (SIGMA f P = &CARD P * x)

REAL_SUM_IMAGE_FINITE_CONST

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

REAL_SUM_IMAGE_EQ_sum

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

REAL_SUM_IMAGE_EQ_CARD

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

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

REAL_SUM_IMAGE_COUNT

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

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 = (&CARD P)⁻¹)

REAL_SUM_IMAGE_CMUL

⊢ ∀P. FINITE P ⇒ ∀f c. SIGMA (λx. c * f x) P = c * SIGMA f 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_0

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

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