Selected Objects

THM	extend_intseg_upperpart_down	a,b:, P:({a..b}Prop), n:{(a+1)..(b+1)}. P(n-1)  (i:{a..b}. ni  P(i))  (i:{a..b}. n-1i  P(i))
def	prime_mset_complete	prime_mset_complete(f)(x) == if is_prime(x) f(x) else 0 fi
THM	prime_mset_complete_isext	f:(Prime), x:Prime. prime_mset_complete(f)(x) = f(x)
THM	prime_mset_complete_ismin	f:(Prime), x:. prime(x)  prime_mset_complete(f)(x) = 0
def	eval_factorization	The number of which an integer multiset is a factorization {a..b}(f) ==  i:{a..b}. if(i)
THM	eval_factorization_split_mid	a,c,b:, f:({a..b}). ac  cb  {a..b}(f) = {a..c}(f){c..b}(f)
def	prime_factorization_of	f is a factorization of k == (x:Prime. k<x  f(x) = 0) & k = {2..k+1}(prime_mset_complete(f))
THM	prime_factorization_limit	n:, f,g:(Prime). f is a factorization of n g is a factorization of n (x:{2..(n+1)}. prime_mset_complete(f)(x) = prime_mset_complete(g)(x))  f = g
THM	eval_factorization_split_pluck	a,c,b:, f:({a..b}). ac  c<b  {a..b}(f) = {a..c}(f)cf(c){c+1..b}(f)
def	trivial_factorization	trivial_factorization(z)(i) == if i=z 1 else 0 fi
THM	trivial_factorization_comp1	x,y:. x = y  trivial_factorization(x)(y) = 1
THM	trivial_factorization_comp2	x,y:. x  y  trivial_factorization(x)(y) = 0
THM	eval_trivial_factorization	a,b:, j:{a..b}. {a..b}(trivial_factorization(j)) = j
def	reduce_factorization	Removing one member from a factorization multiset reduce_factorization(f; j)(i) == if i=j f(i)-1 else f(i) fi
THM	reduce_factorization_cancel	a,b:, f,g:({a..b}), j:{a..b}. 0<f(j) 0<g(j)  reduce_factorization(f; j) = reduce_factorization(g; j)  f = g
THM	reduce_factorization_bound	a,b:, f:({a..b}), j:{a..b}. 0<f(j)  (i:{a..b}. reduce_factorization(f; j)(i)f(i))
THM	eval_factorization_nat_plus	a:, b:, f:({a..b}). {a..b}(f)
THM	only_positives_prime_fed	f:(Prime), n:. f is a factorization of n  0<n
THM	eval_factorization_one	a:{2...}, b:, f:({a..b}). {a..b}(f) = 1  (i:{a..b}. f(i) = 0)
THM	only_one_factored_by	f:(Prime), n,n':. f is a factorization of n  f is a factorization of n'  n = n'
THM	eval_factorization_one_b	a:{2...}, b:, f:({a..b}). {a..b}(f) = 1  (i:{a..b}. 0<f(i))
THM	eval_factorization_one_c	a:{2...}, b:, f:({a..b}). {a..b}(f) = 1  f = (x.0)
THM	eval_factorization_not_one	a:{2...}, b:, f:({a..b}). {a..b}(f) = 1  (i:{a..b}. f(i) = 0)
THM	eval_factorization_prod	The pairwise sum of factorizations of a couple of numbers factorizes their product. a,b:, f,g:({a..b}). {a..b}(f){a..b}(g) = {a..b}(i.f(i)+g(i))
THM	eval_factorization_pluck	a,b:, f:({a..b}), z:{a..b}. 0<f(z)  {a..b}(f) = z{a..b}(reduce_factorization(f; z))
THM	eval_reduce_factorization_less	a:, b:, f:({a..b}), j:{a..b}. 2j  0<f(j)  {a..b}(reduce_factorization(f; j))<{a..b}(f)
THM	eval_factorization_intseg_null	a,b:, f:({a..b}). ba  {a..b}(f) = 1
THM	eval_factorization_nullnorm	a,b:, f:({a..b}). ba  {a..b}(f) = {a..a}(f)
def	is_prime_factorization	Prime factorization as a multiset on an interval. is_prime_factorization(a; b; f) == i:{a..b}. 0<f(i)  prime(i)
THM	prime_mset_c_is_prime_f	f:(Prime), b:. is_prime_factorization(2; b; prime_mset_complete(f))
THM	sq_stable__is_prime_factorization	a,b:, f:({a..b}). SqStable(is_prime_factorization(a; b; f))
THM	reduce_fac_pres_isprimefac	a,b:, f:({a..b}), j:{a..b}. 0<f(j) is_prime_factorization(a; b; f) is_prime_factorization(a; b; reduce_factorization(f; j))
THM	factor_divides_evalfactorization	a,b:, f:({a..b}), j:{a..b}. 0<f(j)  j | {a..b}(f)
THM	nat_prime_div_each_factorLEMMA	X:.  prime(X) (X1:. X1<X  prime(X1)  (a,b:. X1 | ab  X1 | a  X1 | b)) (W:. 0<W  W<X  (t:. X | tW  X | t))
THM	nat_prime_div_each_factor	X:. prime(X)  (a,b:. X | ab  X | a  X | b)
THM	prime_divs_mul_via_intseg	p:.  prime(p) (a,b:, e:({a..b}). (a<b  p | ( i:{a..b}. e(i))  (i:{a..b}. p | e(i)))
THM	prime_divs_exp	p:. prime(p)  (b,z:. p | zb  b  0 & p | z)
THM	prime_factorization_includes_prime_divisors	a:, b:, f:({a..b}), p:. is_prime_factorization(a; b; f) prime(p)  p | {a..b}(f)  p  {a..b} & 0<f(p)
THM	remove_prime_factor	a:, b:, f:({a..b}), p:. is_prime_factorization(a; b; f) prime(p) p | {a..b}(f)  {a..b}(f) = p{a..b}(reduce_factorization(f; p))
THM	prime_factorization_unique	There is at most one prime factorization of any natural number (given a range of integers to include). a:{2...}, b:, g,h:({a..b}). is_prime_factorization(a; b; g) is_prime_factorization(a; b; h)  {a..b}(g) = {a..b}(h)  g = h
def	split_factor2	(eliminating the power of a composite of two number by adding it to the power of its two factors) split_factor2(g; x; y)(u) == if u=x g(x)+g(xy) ; u=y g(y)+g(xy) ; u=xy 0 else g(u) fi
THM	split_factor2_char	Redistributing the power of a composite of two numbers in a factorization down to the factors produces another factorization of the same number, zeroing the power of the composite and leaving the powers of larger factors untouched. k:{2...}, g:({2..k}), x,y:{2..k}. xy<k x<y {2..k}(g) = {2..k}(split_factor2(g; x; y)) & split_factor2(g; x; y)(xy) = 0 & (u:{2..k}. xy<u  split_factor2(g; x; y)(u) = g(u))
def	split_factor1	split_factor1(g; x)(u) == if u=x g(x)+g(xx)+g(xx) ; u=xx 0 else g(u) fi
THM	split_factor1_char	Redistributing the power of a composite square in a factorization down to the square root produces another factorization of the same number, zeroing the power of the composite and leaving the powers of larger factors untouched. k:{2...}, g:({2..k}), x:{2..k}. xx<k {2..k}(g) = {2..k}(split_factor1(g; x)) & split_factor1(g; x)(xx) = 0 & (u:{2..k}. xx<u  split_factor1(g; x)(u) = g(u))
THM	can_reduce_composite_factor	A composite factor in a factorization can be reduced to power zero, leaving all larger factors' powers unchanged. k:{2...}, g:({2..k}), x,y:{2..k}. xy<k (h:({2..k}).  ({2..k}(g) = {2..k}(h) & h(xy) = 0 & (u:{2..k}. xy<u  h(u) = g(u)))
THM	can_reduce_composite_factor2	k:{2...}, g:({2..k}), z:{2..k}. prime(z) (g':({2..k}).  ({2..k}(g) = {2..k}(g') & g'(z) = 0 & (u:{2..k}. z<u  g'(u) = g(u)))
THM	prime_factorization_existsLEMMA	k:{2...}, n:, g:({2..k}). 2  n < k+1 (i:{2..k}. ni  0<g(i)  prime(i)) (h:({2..k}). {2..k}(g) = {2..k}(h) & is_prime_factorization(2; k; h))
THM	prime_factorization_exists	n:{1...}.  h:({2..(n+1)}). n = {2..n+1}(h) & is_prime_factorization(2; (n+1); h)
def	lelt_int	i  j < k == (ij)(j<k)
THM	lelt_int_vs_lelt	i,j,k:. i  j < k  i  j < k
def	complete_intseg_mset	complete_intseg_mset(a; b; f)(x) == if a  x < b f(x) else 0 fi
THM	complete_intseg_mset_ismin	a,b:, f:({a..b}), x:. a  x < b  complete_intseg_mset(a; b; f)(x) = 0
THM	complete_intseg_mset_isext	a,b:, f:({a..b}), x:{a..b}. complete_intseg_mset(a; b; f)(x) = f(x)
THM	prime_factorization_exists2	Every positive integer can be factored into primes. n:{1...}. f:(Prime). f is a factorization of n
THM	prime_factorization_mset_unique	There is at most one prime factorization of any natural number. n:, f,g:(Prime). f is a factorization of n  g is a factorization of n  f = g
THM	fta_mset	The Fundamental Theorem of Arithmetic (FTA) There is a unique prime factorization for every positive integer. n:{1...}. !f:(Prime). f is a factorization of n

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