2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "arithmetics/primes.ma".
13 include "arithmetics/bigops.ma".
17 notation "∑_{ ident i < n | p } f"
19 for @{'bigop $n plus 0 (λ${ident i}. $p) (λ${ident i}. $f)}.
21 notation "∑_{ ident i < n } f"
23 for @{'bigop $n plus 0 (λ${ident i}.true) (λ${ident i}. $f)}.
25 notation "∑_{ ident j ∈ [a,b[ } f"
27 for @{'bigop ($b-$a) plus 0 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
28 (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
30 notation "∑_{ ident j ∈ [a,b[ | p } f"
32 for @{'bigop ($b-$a) plus 0 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
33 (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
35 notation "∏_{ ident i < n | p} f"
37 for @{'bigop $n times 1 (λ${ident i}.$p) (λ${ident i}. $f)}.
39 notation "∏_{ ident i < n } f"
41 for @{'bigop $n times 1 (λ${ident i}.true) (λ${ident i}. $f)}.
43 notation "∏_{ ident j ∈ [a,b[ } f"
45 for @{'bigop ($b-$a) times 1 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
46 (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
48 notation "∏_{ ident j ∈ [a,b[ | p } f"
50 for @{'bigop ($b-$a) times 1 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
51 (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
53 (* instances of associative and commutative operations *)
55 definition plusA ≝ mk_Aop nat 0 plus (λa.refl ? a) (λn.sym_eq ??? (plus_n_O n))
56 (λa,b,c.sym_eq ??? (associative_plus a b c)).
58 definition plusAC ≝ mk_ACop nat 0 plusA commutative_plus.
60 definition timesA ≝ mk_Aop nat 1 times
61 (λa.sym_eq ??? (plus_n_O a)) (λn.sym_eq ??? (times_n_1 n))
62 (λa,b,c.sym_eq ??? (associative_times a b c)).
64 definition timesAC ≝ mk_ACop nat 1 timesA commutative_times.
66 definition natD ≝ mk_Dop nat 0 plusAC times (λn.(sym_eq ??? (times_n_O n)))
67 distributive_times_plus.
69 (********************************************************)
71 theorem sigma_const: ∀n:nat. ∑_{i<n} 1 = n.
72 #n elim n // #n1 >bigop_Strue //
75 (* monotonicity; these roperty should be expressed at a more
79 ∀n.∀p:nat → bool.∀g1,g2:nat → nat.
80 (∀i.i<n → p i = true → g1 i ≤ g2 i ) →
81 ∏_{i < n | p i} (g1 i) ≤ ∏_{i < n | p i} (g2 i).
84 |#n1 #Hind #Hle cases (true_or_false (p n1)) #Hcase
85 [ >bigop_Strue // >bigop_Strue // @le_times
86 [@Hle // |@Hind #i #lti #Hpi @Hle [@lt_to_le @le_S_S @lti|@Hpi]]
87 |>bigop_Sfalse // >bigop_Sfalse // @Hind
88 #i #lti #Hpi @Hle [@lt_to_le @le_S_S @lti|@Hpi]
93 theorem exp_sigma: ∀n,a,p.
94 ∏_{i < n | p i} a = exp a (∑_{i < n | p i} 1).
95 #n #a #p elim n // #n1 cases (true_or_false (p n1)) #Hcase
96 [>bigop_Strue // >bigop_Strue // |>bigop_Sfalse // >bigop_Sfalse //]
99 theorem times_pi: ∀n,p,f,g.
100 ∏_{i<n|p i}(f i*g i) = ∏_{i<n|p i}(f i) * ∏_{i<n|p i}(g i).
101 #n #p #f #g elim n // #n1 cases (true_or_false (p n1)) #Hcase #Hind
102 [>bigop_Strue // >bigop_Strue // >bigop_Strue //
103 |>bigop_Sfalse // >bigop_Sfalse // >bigop_Sfalse //
108 ∏_{i < n | p i} 1 = 1.
109 #n #p elim n // #n1 #Hind cases (true_or_false (p n1)) #Hc
110 [>bigop_Strue >Hind // |>bigop_Sfalse // ]
113 theorem exp_pi: ∀n,m,p,f.
114 ∏_{i < n | p i}(exp (f i) m) = exp (∏_{i < n | p i}(f i)) m.
117 |#m1 #Hind >times_pi >Hind %