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 pos_concave_fn : thm
    val pos_convex_fn : thm
  
  (*  Theorems  *)
    val NESTED_REAL_SUM_IMAGE_REVERSE : 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_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 jensen_concave_SIGMA : thm
    val jensen_convex_SIGMA : thm
    val jensen_pos_concave_SIGMA : thm
    val jensen_pos_convex_SIGMA : thm
  
  val real_sigma_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [iterate] 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}
   
   [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}
   
   [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'
   
   [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_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
   
   [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
   
   
*)
end

HOL 4, Trindemossen-1