Theory "real_sigma"

Signature

Definitions

REAL_SUM_IMAGE_DEF

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

Theorems

NESTED_REAL_SUM_IMAGE_REVERSE

⊢ ∀f s s'.
    FINITE s ∧ FINITE s' ⇒ (∑ (λx. ∑ (f x) s') s = ∑ (λx. ∑ (λy. f y x) s) s')

REAL_SUM_IMAGE_0

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

REAL_SUM_IMAGE_ADD

⊢ ∀s. FINITE s ⇒ ∀f f'. ∑ (λx. f x + f' x) s = ∑ f s + ∑ f' s

REAL_SUM_IMAGE_CMUL

⊢ ∀P. FINITE P ⇒ ∀f c. ∑ (λx. c * f x) P = c * ∑ f P

REAL_SUM_IMAGE_CONST_EQ_1_EQ_INV_CARD

⊢ ∀P. FINITE P ⇒
      ∀f. (∑ f P = 1) ∧ (∀x y. x ∈ P ∧ y ∈ P ⇒ (f x = f y)) ⇒
          ∀x. x ∈ P ⇒ (f x = (&CARD P)⁻¹)

REAL_SUM_IMAGE_COUNT

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

REAL_SUM_IMAGE_CROSS_SYM

⊢ ∀f s1 s2.
    FINITE s1 ∧ FINITE s2 ⇒
    (∑ (λ(x,y). f (x,y)) (s1 × s2) = ∑ (λ(y,x). f (x,y)) (s2 × s1))

REAL_SUM_IMAGE_DISJOINT_UNION

⊢ ∀P P'.
    FINITE P ∧ FINITE P' ∧ DISJOINT P P' ⇒ ∀f. ∑ f (P ∪ P') = ∑ f P + ∑ f P'

REAL_SUM_IMAGE_EQ

⊢ ∀s f f'. FINITE s ∧ (∀x. x ∈ s ⇒ (f x = f' x)) ⇒ (∑ f s = ∑ f' s)

REAL_SUM_IMAGE_EQ_CARD

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

REAL_SUM_IMAGE_EQ_sum

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

REAL_SUM_IMAGE_FINITE_CONST

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

REAL_SUM_IMAGE_FINITE_CONST2

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

REAL_SUM_IMAGE_FINITE_CONST3

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

REAL_SUM_IMAGE_FINITE_SAME

⊢ ∀P. FINITE P ⇒
      ∀f p. p ∈ P ∧ (∀q. q ∈ P ⇒ (f p = f q)) ⇒ (∑ f P = &CARD P * f p)

REAL_SUM_IMAGE_IF_ELIM

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

REAL_SUM_IMAGE_IMAGE

⊢ ∀P. FINITE P ⇒
      ∀f'. INJ f' P (IMAGE f' P) ⇒ ∀f. ∑ f (IMAGE f' P) = ∑ (f ∘ f') P

REAL_SUM_IMAGE_INTER_ELIM

⊢ ∀P. FINITE P ⇒ ∀f P'. (∀x. x ∉ P' ⇒ (f x = 0)) ⇒ (∑ f (P ∩ P') = ∑ f P)

REAL_SUM_IMAGE_INTER_NONZERO

⊢ ∀P. FINITE P ⇒ ∀f. ∑ f (P ∩ (λp. f p ≠ 0)) = ∑ f P

REAL_SUM_IMAGE_INV_CARD_EQ_1

⊢ ∀P. P ≠ ∅ ∧ FINITE P ⇒ (∑ (λs. if s ∈ P then (&CARD P)⁻¹ else 0) P = 1)

REAL_SUM_IMAGE_IN_IF

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

REAL_SUM_IMAGE_IN_IF_ALT

⊢ ∀s f z. FINITE s ⇒ (∑ f s = ∑ (λx. if x ∈ s then f x else z) s)

REAL_SUM_IMAGE_MONO

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

REAL_SUM_IMAGE_MONO_SET

⊢ ∀f s t. FINITE s ∧ FINITE t ∧ s ⊆ t ∧ (∀x. x ∈ t ⇒ 0 ≤ f x) ⇒ ∑ f s ≤ ∑ f t

REAL_SUM_IMAGE_NEG

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

REAL_SUM_IMAGE_NONZERO

⊢ ∀P. FINITE P ⇒
      ∀f. (∀x. x ∈ P ⇒ 0 ≤ f x) ∧ (∃x. x ∈ P ∧ f x ≠ 0) ⇒ (∑ f P ≠ 0 ⇔ P ≠ ∅)

REAL_SUM_IMAGE_POS

⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ ∑ f s

REAL_SUM_IMAGE_POS_MEM_LE

⊢ ∀P. FINITE P ⇒ ∀f. (∀x. x ∈ P ⇒ 0 ≤ f x) ⇒ ∀x. x ∈ P ⇒ f x ≤ ∑ f P

REAL_SUM_IMAGE_POW

⊢ ∀a s. FINITE s ⇒ ((∑ a s)² = ∑ (λ(i,j). a i * a j) (s × s))

REAL_SUM_IMAGE_REAL_SUM_IMAGE

⊢ ∀s s' f.
    FINITE s ∧ FINITE s' ⇒
    (∑ (λx. ∑ (f x) s') s = ∑ (λx. f (FST x) (SND x)) (s × s'))

REAL_SUM_IMAGE_SING

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

REAL_SUM_IMAGE_SPOS

⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ∀f. (∀x. x ∈ s ⇒ 0 < f x) ⇒ 0 < ∑ f s

REAL_SUM_IMAGE_SUB

⊢ ∀s f f'. FINITE s ⇒ (∑ (λx. f x − f' x) s = ∑ f s − ∑ f' s)

REAL_SUM_IMAGE_THM

⊢ ∀f. (∑ f ∅ = 0) ∧
      ∀e s. FINITE s ⇒ (∑ f (e INSERT s) = f e + ∑ f (s DELETE e))

SEQ_REAL_SUM_IMAGE

⊢ ∀s. FINITE s ⇒
      ∀f f'. (∀x. x ∈ s ⇒ (λn. f n x) ⟶ f' x) ⇒ (λn. ∑ (f n) s) ⟶ ∑ f' s