Nuprl - IteratedBinops

Origin Definitions Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
IteratedBinopsNuprl Section: IteratedBinops - Iterated Binary Operations

Selected Objects
Introduction Introductory Remarks

def is_ident
(u is an identity element for operation f on A)
is_ident(A; f; u) == x:A. f(u,x) = x & f(x,u) = x

THM binary_ident_unique
A binary operation has at most one identity value.
f:(AAA), u,v:A. is_ident(A; f; u)  is_ident(A; f; v)  u = v

THM intmul_ident_one
is_ident(; (x,y. xy); 1)

THM natmul_ident_one
is_ident(; (x,y. xy); 1)

THM intadd_ident_zero
is_ident(; (x,y. x+y); 0)

THM natadd_ident_zero
is_ident(; (x,y. x+y); 0)

def is_assoc
Associativity of a function
is_assoc(A; x,z.f(x;z)) == x,y,z:A. f(x;f(y;z)) = f(f(x;y);z)  A

def is_assoc_sep
Associativity of a function
is_assoc_sep(A; f) == is_assoc(A; x,y.(f(x,y)))

THM is_assoc_intmul
is_assoc_sep(; (x,y. xy))

THM is_assoc_intadd
is_assoc_sep(; (x,y. x+y))

def is_commutative
Commutativity of a function
is_commutative(A; x,z.f(x;z)) == x,z:A. f(x;z) = f(z;x)  A

def is_commutative_sep
Commutativity of a function
is_commutative_sep(A; f) == is_commutative(A; x,z.(f(x,z)))

THM is_commutative_sep_intmul
is_commutative_sep(; (x,y. xy))

THM is_commutative_sep_intadd
is_commutative_sep(; (x,y. x+y))

THM split_int_domain
P:(Prop), a:.
(b:{...a}. P(a,b))

((b:{...a}. P(a,b))  (b:{a...}. P(a,b)))  (b:. P(a,b))

THM all_int_pairs_via_all_splits
P:(Prop).
(a:, b:{...a}. P(a,b))

(a:. (b:{...a}. P(a,b))  (b:{a...}. P(a,b)))  (a,b:. P(a,b))

THM int_seg_upper_ind
P:(Prop), a:.
(b:{a...}. (c:{a..b}. P(a,c))  P(a,b))  (b:{a...}. P(a,b))

THM split_int_domain_by_norm_lower
P:(Prop), a:.
(b:{...a}. P(a,a)  P(a,b))  (b:{a...}. P(a,b))  (b:. P(a,b))

THM int_segs_from_base_by_upper_ind
P:(Prop), a:.
(b:{...a}. P(a,b))

(b:{a+1...}. (c:{a..b}. P(a,c))  P(a,b))  (b:. P(a,b))

THM all_int_segs_by_upper_ind
P:(Prop).
(a:, b:{...a}. P(a,b))

(a:, b:{a+1...}. (c:{a..b}. P(a,c))  P(a,b))  (a,b:. P(a,b))

def iter_via_intseg
Iteration of a binary operator over a finite sequence of values. Some special cases of this iteration operator include sum, product and exponentiation:

i:{a..b}. e(i) Iter(x,y. x+y;0) i:{a..b}. e(i)

i:b. e(i) Iter(x,y. x+y;0) i:{0..b}. e(i)

i:{a..b}. e(i) Iter(x,y. xy;1) i:{a..b}. e(i)

i:b. e(i) Iter(x,y. xy;1) i:{0..b}. e(i)

eb Iter(x,y. xy;1) :{0..b}. e

Or i:{a..b}. e(i) Iter(x,y. x  y;False) i:{a..b}. e(i)

Or i:b. e(i) Iter(x,y. x  y;False) i:{0..b}. e(i)

And i:{a..b}. e(i) Iter(x,y. x & y;True) i:{a..b}. e(i)

And i:b. e(i) Iter(x,y. x & y;True) i:{0..b}. e(i)

Iter(f;u) i:{a..b}. e(i)
== if a<b f((Iter(f;u) i:{a..b-1}. e(i)),e(b-1)) else u fi
(recursive)

THM exponent_zero
x:. x0 = 1

THM exponent_one
x:. x1 = x

THM iter_via_intseg_null
Iteration over a null sequence is the identity element.
f:(AAA), u:A, a,b:, e:({a..b}A). ba  (Iter(f;u) i:{a..b}. e(i)) = u

THM iter_via_intseg_nullnorm
f:(AAA), u:A, a,b:, e:({a..b}A).
ba  (Iter(f;u) i:{a..b}. e(i)) = (Iter(f;u) i:{a..a}. e(i))

THM iter_via_intseg_singleton
Iteration over a singleton is just the value for the one index.
f:(AAA), u:A.
is_ident(A; f; u)

(a,b:, e:({a..b}A). a+1 = b  (Iter(f;u) i:{a..b}. e(i)) = e(a))

THM sum_via_intseg_singleton
a,b:, e:({a..b}). a+1 = b  ( i:{a..b}. e(i)) = e(a)

THM mul_via_intseg_singleton
a,b:, e:({a..b}). a+1 = b  ( i:{a..b}. e(i)) = e(a)

THM iter_via_intseg_notnull
Splitting the last element from the range of iteration.
f:(AAA), u:A, a,b:, e:({a..b}A).
a<b

(c:.
(b = c+1  (Iter(f;u) i:{a..b}. e(i)) = f((Iter(f;u) i:{a..c}. e(i)),e(c)))

THM mul_via_intseg_notnull
a,b:, e:({a..b}).
a<b  (c:. b = c+1  ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))e(c))

THM sum_via_intseg_notnull
a,b:, e:({a..b}).
a<b  (c:. b = c+1  ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))+e(c))

THM iter_via_intseg_split_last
Splitting the last element from the domain of iteration.
f:(AAA), u:A, a,b:, e:({a..b}A).
a<b  (Iter(f;u) i:{a..b}. e(i)) = f((Iter(f;u) i:{a..b-1}. e(i)),e(b-1))

THM iter_via_intseg_all_units
Iterating over only identity values gives the identity value itself.
f:(AAA), u:A.
is_ident(A; f; u)

(a,b:, e:({a..b}A).
((i:{a..b}. e(i) = u)  (Iter(f;u) i:{a..b}. e(i)) = u)

THM mul_via_intseg_one
a,b:, e:({a..b}). (i:{a..b}. e(i) = 1)  ( i:{a..b}. e(i)) = 1

THM one_exponentiation
x:. 1x = 1

THM iter_via_intseg_shift_rw
Shifting the range of iteration.
f:(AAA), u:A, a,b:, e:({a..b}A), k:.
(Iter(f;u) i:{a..b}. e(i)) = (Iter(f;u) j:{a+k..b+k}. e(j-k))

THM iter_via_intseg_shift
Shifting the range of iteration.
f:(AAA), u:A, a,b,c,d:.
b-a = d-c

(e:({a..b}A), g:({c..d}A).
((i:{a..b}, j:{c..d}. j-i = c-a  e(i) = g(j)  A)
(
((Iter(f;u) i:{a..b}. e(i)) = (Iter(f;u) j:{c..d}. g(j)))

THM iter_via_intseg_comp_binop
Joining two iterations pairwise.
f:(AAA), u:A.
is_commutative_sep(A; f)

is_ident(A; f; u)

is_assoc_sep(A; f)

(a,b:, e,g:({a..b}A).
(f((Iter(f;u) i:{a..b}. e(i)),Iter(f;u) i:{a..b}. g(i))
(=
((Iter(f;u) i:{a..b}. f(e(i),g(i)))
( A)

THM add_via_intseg_addends
Adding two summations pairwise.
a,b:, f,g:({a..b}).
( i:{a..b}. f(i))+( i:{a..b}. g(i)) = ( i:{a..b}. f(i)+g(i))

THM iter_via_intseg_split_mid
Splitting the range of iteration.
f:(AAA), u:A.
is_ident(A; f; u)

is_assoc_sep(A; f)

(a,c,b:, e:({a..b}A).
(ac
(
(cb
(
((Iter(f;u) i:{a..b}. e(i))
(=
(f((Iter(f;u) i:{a..c}. e(i)),Iter(f;u) i:{c..b}. e(i)))

THM iter_via_intseg_amputate_units
Removing units from the ends of the range of iteration preserves the result.
f:(AAA), u:A.
is_ident(A; f; u)

is_assoc_sep(A; f)

(a,b:, c:{a...b}, d:{c..b}, e:({a..b}A).
((i:{a..b}. i<c  di  e(i) = u)
(
((Iter(f;u) i:{a..b}. e(i)) = (Iter(f;u) i:{c..d}. e(i)))

THM iter_via_intseg_split_pluck
Splitting the range of iteration.
f:(AAA), u:A.
is_ident(A; f; u)

is_assoc_sep(A; f)

(a,c,b:, e:({a..b}A).
(ac
(
(c<b
(
((Iter(f;u) i:{a..b}. e(i))
(=
(f((Iter(f;u) i:{a..c}. e(i)),f(e(c),Iter(f;u) i:{c+1..b}. e(i))))

THM sum_via_intseg_split_pluck
Splitting the range of iteration.
a,c,b:, e:({a..b}).
ac

c<b  ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))+e(c)+( i:{c+1..b}. e(i))

THM mul_via_intseg_split_pluck
Splitting the range of iteration.
a,c,b:, e:({a..b}).
ac

c<b  ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))e(c)( i:{c+1..b}. e(i))

THM components_divide_iter_mul
a,b:, e:({a..b}), i:{a..b}. e(i) | ( i:{a..b}. e(i))

THM sum_via_intseg_split_mid
Splitting the range of iteration.
a,c,b:, e:({a..b}).
ac  cb  ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))+( i:{c..b}. e(i))

THM mul_via_intseg_split_mid
Splitting the range of iteration.
a,c,b:, e:({a..b}).
ac  cb  ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))( i:{c..b}. e(i))

THM sum_exponent
i:, x,y:. ixiy = i(x+y)

THM mul_via_intseg_split_last
a,b:, e:({a..b}).
a<b  ( i:{a..b}. e(i)) = ( i:{a..b-1}. e(i))e(b-1)

THM mul_via_intseg_factors
a,b:, f,g:({a..b}).
( i:{a..b}. f(i))( i:{a..b}. g(i)) = ( i:{a..b}. f(i)g(i))

THM exp_reduce1
Corollary to mul via intseg factors
a,b,c:. (ab)c = acbc

THM sum_via_intseg_split_last
a,b:, e:({a..b}).
a<b  ( i:{a..b}. e(i)) = ( i:{a..b-1}. e(i))+e(b-1)

THM and_via_all_intseg_notnull
a,b:, P:({a..b}Prop).
a<b  (c:. b = c+1  ((i:{a..b}. P(i))  (i:{a..c}. P(i)) & P(c)))

THM and_via_all_intseg_split_last
a,b:, P:({a..b}Prop).
a<b  ((i:{a..b}. P(i))  (i:{a..(b-1)}. P(i)) & P(b-1))

THM all_intseg_vs_iter_and
Universal quantification over a finite range is iterated conjunction.
a,b:, P:({a..b}Prop). (i:{a..b}. P(i))  (And i:{a..b}. P(i))

THM or_via_exist_intseg_notnull
a,b:, P:({a..b}Prop).
a<b  (c:. b = c+1  ((i:{a..b}. P(i))  (i:{a..c}. P(i))  P(c)))

THM or_via_exist_intseg_split_last
a,b:, P:({a..b}Prop).
a<b  ((i:{a..b}. P(i))  (i:{a..(b-1)}. P(i))  P(b-1))

THM exist_intseg_null
a,b:, P:({a..b}Prop). ba  (i:{a..b}. P(i))

THM exist_intseg_vs_iter_or
Existential quantification over a finite range is iterated disjunction.
a,b:, P:({a..b}Prop). (i:{a..b}. P(i))  (Or i:{a..b}. P(i))

THM iter_nat_prod_one_iff_factors_one
An iterated product is one iff each value is one.
e:({a..b}). ( i:{a..b}. e(i)) = 1  (i:{a..b}. e(i) = 1)

THM iter_prod_zero_iff_factor_zero
( i:{a..b}. e(i)) = 0  (i:{a..b}. e(i) = 0)

THM zero_ann_iter_via_intseg
(i:{a..b}. e(i) = 0)  ( i:{a..b}. e(i)) = 0

def factorial_tail_via_iter
k!m ==  i:{k-m..k}. i+1

THM factorial_tail_split_mid
n,m,k:. nk-m  mk  k!(n+m) = (k-m)!nk!m

THM factorial_tail_via_iter_null
m,k:. m = 0    k!m = 1

THM factorial_tail_via_iter_zero
m,k:. k<m  k!m = 0

THM factorial_tail_via_iter_step
m,k:. 1  m  k  (k',m':. k' = k-1  m' = m-1  k!m = kk'!m'  )

THM factorial_tail_via_iter_step_rw
m,k:. 1  m  k  k!m = k(k-1)!(m-1)

def factorial_via_iter
k! == k!k

THM factorial_ratio
m,k:. mk  k! = (k-m)!k!m

THM factorial_ratio2
Definition of a commonly used ratio of factorials.
m,k:. mk  k!m = ((k!)  ((k-m)!))

THM mul_via_intseg_null
a,b:, e:({a..b}). ba  ( i:{a..b}. e(i)) = 1

THM sum_via_intseg_null
a,b:, e:({a..b}). ba  ( i:{a..b}. e(i)) = 0

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Origin Definitions Sections DiscrMathExt Doc