Theory: power series

Definition: power-series
PowerSeries(X;r) ==  bag(X) ⟶ |r|

Lemma: power-series_wf
∀[X:Type]. ∀[r:CRng].  (PowerSeries(X;r) ∈ Type)

Definition: fps-coeff
f[b] ==  f b

Lemma: fps-coeff_wf
∀[X:Type]. ∀[r:CRng]. ∀[f:PowerSeries(X;r)]. ∀[b:bag(X)].  (f[b] ∈ |r|)

Lemma: fps-ext

∀[X:Type]. ∀[r:CRng]. ∀[f,g:PowerSeries(X;r)].  uiff(f = g ∈ PowerSeries(X;r);∀b:bag(X). (f[b] = g[b] ∈ |r|))

Definition: fps-zero
0 == λb.0

Lemma: fps-zero_wf
∀[X:Type]. ∀[r:CRng]. (0 ∈ PowerSeries(X;r))

Definition: fps-one
1 == λb.if bag-null(b) then 1 else 0 fi

Lemma: fps-one_wf
∀[X:Type]. ∀[r:CRng]. (1 ∈ PowerSeries(X;r))

Lemma: fps-non-trivial
∀[X:Type]. ∀[r:CRng]. ¬(1 = 0 ∈ PowerSeries(X;r)) supposing ¬(1 = 0 ∈ |r|)

Definition: fps-single
<c> == λb.if bag-eq(eq;b;c) then 1 else 0 fi

Lemma: fps-single_wf
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[c:bag(X)]. (<c> ∈ PowerSeries(X;r))

Definition: fps-atom
atom(x) == <{x}>

Lemma: fps-atom_wf
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. (atom(x) ∈ PowerSeries(X;r))

Definition: fps-add
(f+g) == λb.(+r f[b] g[b])

Lemma: fps-add_wf
∀[X:Type]. ∀[r:CRng]. ∀[f,g:PowerSeries(X;r)]. ((f+g) ∈ PowerSeries(X;r))

Definition: fps-neg
-(f) == λb.(-r (f b))

Lemma: fps-neg_wf
∀[X:Type]. ∀[r:CRng]. ∀[f:PowerSeries(X;r)]. (-(f) ∈ PowerSeries(X;r))

Definition: fps-sub
(f-g) == (f+-(g))

Lemma: fps-sub_wf
∀[X:Type]. ∀[r:CRng]. ∀[f,g:PowerSeries(X;r)]. ((f-g) ∈ PowerSeries(X;r))

Definition: fps-mul
(f*g) == λb.Σ(p∈bag-partitions(eq;b)). * f[fst(p)] g[snd(p)]

Lemma: fps-mul_wf
∀[X:Type]

  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f,g:PowerSeries(X;r)].  ((f*g) ∈ PowerSeries(X;r)) supposing valueall-type(X)

Lemma: fps-mul-coeff-bag-rep-simple
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[n:ℕ]. ∀[k:ℕn + 1]. ∀[r:CRng]. ∀[f,g:PowerSeries(X;r)]. ∀[x:X].
    (f*g)[bag-rep(n;x)] = (* f[bag-rep(k;x)] g[bag-rep(n - k;x)]) ∈ |r|
    supposing ∀i:ℕn + 1. ((¬(i = k ∈ ℤ)) ⇒ (f[bag-rep(i;x)] = 0 ∈ |r|))
  supposing valueall-type(X)

Lemma: fps-mul-coeff0
∀[eq:Top]. ∀[r:CRng]. ∀[f,g:Top].  ((f*g)[{}] ~ (f[{}] * g[{}]) +r 0)

Lemma: fps-mul-comm
∀[X:Type]. ∀[eq:EqDecider(X)].
  ∀[r:CRng]. ∀[f,g:PowerSeries(X;r)].  ((f*g) = (g*f) ∈ PowerSeries(X;r)) supposing valueall-type(X)

Lemma: fps-add-comm
∀[X:Type]. ∀[r:CRng]. ∀[f,g:PowerSeries(X;r)].  ((f+g) = (g+f) ∈ PowerSeries(X;r))

Lemma: fps-mul-assoc
∀[X:Type]. ∀[eq:EqDecider(X)].

  ∀[r:CRng]. ∀[f,g,h:PowerSeries(X;r)].  (((f*g)*h) = (f*(g*h)) ∈ PowerSeries(X;r)) supposing valueall-type(X)

Lemma: fps-add-assoc
∀[X:Type]. ∀[r:CRng]. ∀[f,g,h:PowerSeries(X;r)]. (((f+g)+h) = (f+(g+h)) ∈ PowerSeries(X;r))

Definition: fps-rng

fps-rng(r) ==  <PowerSeries(X;r), λf,g. tt, λf,g. tt, λf,g. (f+g), 0, λf.-(f), λf,g. (f*g), 1, λf,g. (inl f)>

Lemma: fps-rng_wf
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. (fps-rng(r) ∈ CRng) supposing valueall-type(X)

Definition: fps-add-grp
fps-add-grp(r) == fps-rng(r)↓+gp

Lemma: fps-add-grp_wf
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. (fps-add-grp(r) ∈ AbGrp) supposing valueall-type(X)

Lemma: fps-mul-single-general
∀[X:Type]
 ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[c:bag(X)]. ∀[f:PowerSeries(X;r)].
 ((<c>*f) = (λb.case bag-diff(eq;b;c) of inl(d) => f[d] | inr(z) => 0) ∈ PowerSeries(X;r))
 supposing valueall-type(X)

Lemma: fps-mul-single
∀[X:Type]

  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[b,c:bag(X)].  ((<b>*<c>) = <b + c> ∈ PowerSeries(X;r)) supposing valueall-type(X)

Definition: fps-summation
fps-summation(r;b;x.f[x]) ==  Σ(x∈b). f[x]

Lemma: fps-summation_wf
∀[X:Type]. ∀[r:CRng]. ∀[T:Type]. ∀[f:T ⟶ PowerSeries(X;r)]. ∀[b:bag(T)].
  (fps-summation(r;b;x.f[x]) ∈ PowerSeries(X;r))

Lemma: fps-summation-coeff
∀[X:Type]. ∀[r:CRng]. ∀[T:Type]. ∀[f:T ⟶ PowerSeries(X;r)]. ∀[b:bag(T)].
  ∀m:bag(X). (fps-summation(r;b;x.f[x])[m] = Σ(x∈b). f[x][m] ∈ |r|)

Definition: fps-div-coeff
fps-div-coeff(eq;r;f;g;x;b)

==r x * (f[b] +r (-r Σ(p∈[p∈bag-partitions(eq;b)|¬_bbag-null(fst(p))]). g[fst(p)] * fps-div-coeff(eq;r;f;g;x;snd(p))))

Lemma: fps-div-coeff_wf
∀[X:Type]

  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f,g:PowerSeries(X;r)]. ∀[x:|r|]. ∀[b:bag(X)].  (fps-div-coeff(eq;r;f;g;x;b) ∈ |r|)

  supposing valueall-type(X)

Lemma: fps-div-coeff-property
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f,g:PowerSeries(X;r)]. ∀[x:|r|].
    (g*λb.fps-div-coeff(eq;r;f;g;x;b)) = f ∈ PowerSeries(X;r) supposing (g[{}] * x) = 1 ∈ |r|
  supposing valueall-type(X)

Definition: fps-div
(f÷g) ==  λb.fps-div-coeff(eq;r;f;g;x;b)

Lemma: fps-div_wf
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:|r|]. ∀[f,g:PowerSeries(X;r)].  ((f÷g) ∈ PowerSeries(X;r))
  supposing valueall-type(X)

Lemma: fps-div-property
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f,g:PowerSeries(X;r)]. ∀[x:|r|].
    (g*(f÷g)) = f ∈ PowerSeries(X;r) supposing (g[{}] * x) = 1 ∈ |r|
  supposing valueall-type(X)

Definition: fps-moebius
fps-moebius(eq;r) ==  λb.eval z = bag-moebius(eq;b) in int-to-ring(r;z)

Lemma: fps-moebius_wf
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng].  (fps-moebius(eq;r) ∈ PowerSeries(X;r))

Lemma: fps-div-unique
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f,g:PowerSeries(X;r)]. ∀[x:|r|].
    ∀q:PowerSeries(X;r)

      q = (f÷g) ∈ PowerSeries(X;r) supposing ((g*q) = f ∈ PowerSeries(X;r)) ∧ ((g[{}] * x) = 1 ∈ |r|)

  supposing valueall-type(X)

Lemma: fps-mul-div
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f,g,h:PowerSeries(X;r)]. ∀[x:|r|].
    (h*(f÷g)) = ((h*f)÷g) ∈ PowerSeries(X;r) supposing (g[{}] * x) = 1 ∈ |r|
  supposing valueall-type(X)

Lemma: fps-moebius-eq

∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng].  (fps-moebius(eq;r) = (1÷λb.1) ∈ PowerSeries(X;r)) supposing valueall-type(X)

Definition: fps-slice
[f]_n == λb.if (#(b) =_z n) then f b else 0 fi

Lemma: fps-slice_wf
∀[X:Type]. ∀[r:CRng]. ∀[n:ℤ]. ∀[f:PowerSeries(X;r)]. ([f]_n ∈ PowerSeries(X;r))

Lemma: fps-slice-slice
∀[X:Type]. ∀[r:CRng]. ∀[m,n:ℤ]. ∀[f:PowerSeries(X;r)].
 ([[f]_m]_n = if (n =_z m) then [f]_m else 0 fi ∈ PowerSeries(X;r))

Lemma: fps-zero-slice
∀[X:Type]. ∀[r:CRng]. ∀[n:ℤ]. ([0]_n = 0 ∈ PowerSeries(X;r))

Lemma: fps-one-slice
∀[X:Type]. ∀[r:CRng]. ∀[n:ℤ]. ([1]_n = if (n =_z 0) then 1 else 0 fi ∈ PowerSeries(X;r))

Lemma: fps-single-slice
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[c:bag(X)]. ∀[n:ℤ].
 ([<c>]_n = if (#(c) =_z n) then <c> else 0 fi ∈ PowerSeries(X;r))

Lemma: fps-add-slice

∀[X:Type]. ∀[r:CRng]. ∀[n:ℤ]. ∀[f,g:PowerSeries(X;r)].  ([(f+g)]_n = ([f]_n+[g]_n) ∈ PowerSeries(X;r))

Lemma: fps-neg-slice
∀[X:Type]. ∀[r:CRng]. ∀[n:ℤ]. ∀[g:PowerSeries(X;r)]. ([-(g)]_n = -([g]_n) ∈ PowerSeries(X;r))

Lemma: fps-sub-slice

∀[X:Type]. ∀[r:CRng]. ∀[n:ℤ]. ∀[f,g:PowerSeries(X;r)].  ([(f-g)]_n = ([f]_n-[g]_n) ∈ PowerSeries(X;r))

Lemma: fps-mul-slice
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[n:ℕ]. ∀[f,g:PowerSeries(X;r)].
    ([(f*g)]_n = fps-summation(r;upto(n + 1);k.([f]_k*[g]_n - k)) ∈ PowerSeries(X;r))
  supposing valueall-type(X)

Lemma: mon_assoc_fps
∀[X:Type]. ∀[r:CRng]. ∀[a,b,c:PowerSeries(X;r)].  ((a+(b+c)) = ((a+b)+c) ∈ PowerSeries(X;r))

Lemma: mon_ident_fps

∀[X:Type]. ∀[r:CRng]. ∀[a:PowerSeries(X;r)].  (((a+0) = a ∈ PowerSeries(X;r)) ∧ ((0+a) = a ∈ PowerSeries(X;r)))

Lemma: negerse_fps

∀[X:Type]. ∀[r:CRng]. ∀[a:PowerSeries(X;r)].  (((a+-(a)) = 0 ∈ PowerSeries(X;r)) ∧ ((-(a)+a) = 0 ∈ PowerSeries(X;r)))

Lemma: neg_thru_op_fps
∀[X:Type]. ∀[r:CRng]. ∀[a,b:PowerSeries(X;r)].  (-((a+b)) = (-(b)+-(a)) ∈ PowerSeries(X;r))

Lemma: neg_inv_fps
∀[X:Type]. ∀[r:CRng]. ∀[a:PowerSeries(X;r)].  (-(-(a)) = a ∈ PowerSeries(X;r))

Lemma: neg_id_fps
∀[X:Type]. ∀[r:CRng].  (-(0) = 0 ∈ PowerSeries(X;r))

Lemma: neg_assoc_fps
∀[X:Type]. ∀[r:CRng]. ∀[a,b:PowerSeries(X;r)].
  (((a+(-(a)+b)) = b ∈ PowerSeries(X;r)) ∧ ((-(a)+(a+b)) = b ∈ PowerSeries(X;r)))

Lemma: iabgrp_op_inv_assoc_fps
∀[X:Type]. ∀[r:CRng]. ∀[a,b:PowerSeries(X;r)].
  (((a+(-(a)+b)) = b ∈ PowerSeries(X;r)) ∧ ((-(a)+(a+b)) = b ∈ PowerSeries(X;r)))

Lemma: abmonoid_comm_fps
∀[X:Type]. ∀[r:CRng]. ∀[a,b:PowerSeries(X;r)].  ((a+b) = (b+a) ∈ PowerSeries(X;r))

Lemma: abmonoid_ac_1_fps
∀[X:Type]. ∀[r:CRng]. ∀[a,b,c:PowerSeries(X;r)].  ((a+(b+c)) = (b+(a+c)) ∈ PowerSeries(X;r))

Lemma: mul_over_plus_fps
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[a,b,c:PowerSeries(X;r)].

    (((a*(b+c)) = ((a*b)+(a*c)) ∈ PowerSeries(X;r)) ∧ (((b+c)*a) = ((b*a)+(c*a)) ∈ PowerSeries(X;r)))

  supposing valueall-type(X)

Lemma: mul_over_minus_fps
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[a,b:PowerSeries(X;r)].
    (((-(a)*b) = -((a*b)) ∈ PowerSeries(X;r)) ∧ ((a*-(b)) = -((a*b)) ∈ PowerSeries(X;r)))
  supposing valueall-type(X)

Lemma: mul_zero_fps
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[a:PowerSeries(X;r)].
    (((0*a) = 0 ∈ PowerSeries(X;r)) ∧ ((a*0) = 0 ∈ PowerSeries(X;r)))
  supposing valueall-type(X)

Lemma: mul_assoc_fps
∀[X:Type]

  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[a,b,c:PowerSeries(X;r)].  ((a*(b*c)) = ((a*b)*c) ∈ PowerSeries(X;r))

  supposing valueall-type(X)

Lemma: mul_one_fps
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[a:PowerSeries(X;r)].
    (((a*1) = a ∈ PowerSeries(X;r)) ∧ ((1*a) = a ∈ PowerSeries(X;r)))
  supposing valueall-type(X)

Lemma: mul_comm_fps
∀[X:Type]

  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[a,b:PowerSeries(X;r)].  ((a*b) = (b*a) ∈ PowerSeries(X;r)) supposing valueall-type(X)

Lemma: mul_ac_1_fps
∀[X:Type]

  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[a,b,c:PowerSeries(X;r)].  ((a*(b*c)) = (b*(a*c)) ∈ PowerSeries(X;r))

  supposing valueall-type(X)

Lemma: fps-moebius-inversion
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f,g:PowerSeries(X;r)].
    g = (f*fps-moebius(eq;r)) ∈ PowerSeries(X;r) supposing f = (g*λb.1) ∈ PowerSeries(X;r)
  supposing valueall-type(X)

Lemma: bag-moebius-inversion
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f,g:bag(X) ⟶ |r|].

    ∀b:bag(X). ((g b) = Σ(p∈bag-partitions(eq;b)). (f (fst(p))) * int-to-ring(r;bag-moebius(eq;snd(p))) ∈ |r|)

    supposing ∀b:bag(X). ((f b) = Σ(s∈sub-bags(eq;b)). g s ∈ |r|)
  supposing valueall-type(X)

Definition: int-moebius
int-moebius(n) ==  bag-moebius(IntDeq;factors(n))

Lemma: int-moebius_wf
∀[n:ℕ⁺]. (int-moebius(n) ∈ ℤ)

Lemma: int-moebius-inversion-general
∀[r:CRng]. ∀[f,g:ℕ⁺ ⟶ |r|].

  ∀n:ℕ⁺. (g[n] = Σ i|n. f[i] * int-to-ring(r;int-moebius(n ÷ i)) ∈ |r|) supposing ∀n:ℕ⁺. (f[n] = Σ i|n. g[i] ∈ |r|)

Lemma: int-moebius-inversion

∀[f,g:ℕ⁺ ⟶ ℤ].  ∀n:ℕ⁺. (g[n] = Σ i|n. f[i] * int-moebius(n ÷ i)  ∈ ℤ) supposing ∀n:ℕ⁺. (f[n] = Σ i|n. g[i]  ∈ ℤ)

Definition: fps-product
Π(x∈b).f[x] == Πx ∈ b. f[x]

Lemma: fps-product_wf
∀[X:Type]

  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[T:Type]. ∀[f:T ⟶ PowerSeries(X;r)]. ∀[b:bag(T)].  (Π(x∈b).f[x] ∈ PowerSeries(X;r))

supposing valueall-type(X)

Lemma: fps-product-reindex
∀[X:Type]
∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[T,A:Type]. ∀[g:T ⟶ A]. ∀[h:A ⟶ T].

    ∀[f:T ⟶ PowerSeries(X;r)]. ∀[b:bag(T)].  (Π(x∈b).f[x] = Π(x∈bag-map(g;b)).f[h x] ∈ PowerSeries(X;r))

    supposing ∀x:T. (x = (h (g x)) ∈ T)
  supposing valueall-type(X)

Lemma: fps-product-append
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[T:Type]. ∀[f:T ⟶ PowerSeries(X;r)]. ∀[b,c:bag(T)].
    (Π(x∈b + c).f[x] = (Π(x∈b).f[x]*Π(x∈c).f[x]) ∈ PowerSeries(X;r))
  supposing valueall-type(X)

Lemma: fps-product-single
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[T:Type]. ∀[f:T ⟶ PowerSeries(X;r)]. ∀[t:T].
    (Π(x∈{t}).f[x] = f[t] ∈ PowerSeries(X;r))
  supposing valueall-type(X)

Lemma: fps-product-upto
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[k:ℕ⁺]. ∀[f:ℕk ⟶ PowerSeries(X;r)].
    (Π(x∈upto(k)).f[x] = (f[0]*Π(x∈upto(k - 1)).f[x + 1]) ∈ PowerSeries(X;r))
  supposing valueall-type(X)

Definition: fps-scalar-mul
(c)*f ==  λb.(c * f[b])

Lemma: fps-scalar-mul_wf
∀[X:Type]. ∀[r:CRng]. ∀[c:|r|]. ∀[f:PowerSeries(X;r)].  ((c)*f ∈ PowerSeries(X;r))

Lemma: fps-scalar-mul-property
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng].
    ((IsAction(|r|;*;1;PowerSeries(X;r);λc,f. (c)*f)
    ∧ IsBilinear(|r|;PowerSeries(X;r);PowerSeries(X;r);+r;λf,g. (f+g);λf,g. (f+g);λc,f. (c)*f))
    ∧ (∀c:|r|. Dist1op2opLR(PowerSeries(X;r);λf.(c)*f;λf,g. (f*g))))
  supposing valueall-type(X)

Lemma: fps-scalar-mul-rng-add

∀[X:Type]. ∀[r:CRng]. ∀[c1,c2:|r|]. ∀[f:PowerSeries(X;r)].  ((c1 +r c2)*f = ((c1)*f+(c2)*f) ∈ PowerSeries(X;r))

Lemma: fps-scalar-mul-mul
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[c:|r|]. ∀[f,g:PowerSeries(X;r)].
    (((c)*(f*g) = ((c)*f*g) ∈ PowerSeries(X;r)) ∧ ((c)*(f*g) = (f*(c)*g) ∈ PowerSeries(X;r)))
  supposing valueall-type(X)

Lemma: fps-scalar-mul-add
∀[X:Type]

  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[c:|r|]. ∀[f,g:PowerSeries(X;r)].  ((c)*(f+g) = ((c)*f+(c)*g) ∈ PowerSeries(X;r))

  supposing valueall-type(X)

Lemma: fps-scalar-mul-zero
∀[X:Type]. ∀[r:CRng]. ∀[f:PowerSeries(X;r)].  ((0)*f = 0 ∈ PowerSeries(X;r))

Lemma: fps-zero-scalar-mul
∀[X:Type]. ∀[r:CRng]. ∀[c:|r|].  ((c)*0 = 0 ∈ PowerSeries(X;r))

Lemma: fps-scalar-mul-one
∀[X:Type]. ∀[r:CRng]. ∀[f:PowerSeries(X;r)].  ((1)*f = f ∈ PowerSeries(X;r))

Lemma: fps-scalar-mul-slice

∀[X:Type]. ∀[r:CRng]. ∀[c:|r|]. ∀[n:ℤ]. ∀[g:PowerSeries(X;r)].  ([(c)*g]_n = (c)*[g]_n ∈ PowerSeries(X;r))

Lemma: fps-div-one
∀[X:Type]

  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f:PowerSeries(X;r)].  ((f÷1) = f ∈ PowerSeries(X;r)) supposing valueall-type(X)

Lemma: fps-geometric-slice_lemma
∀[X:Type]
∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[m:ℕ]. ∀[n:ℕ⁺m + 1]. ∀[g:PowerSeries(X;r)].

    [(1÷(1-g))]_m = ([(1÷(1-g))]_m - n*g) ∈ PowerSeries(X;r) supposing g = [g]_n ∈ PowerSeries(X;r)

supposing valueall-type(X)

Lemma: fps-geometric-slice_lemma2
∀[X:Type]
∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[n:ℕ⁺]. ∀[m:ℕn]. ∀[g:PowerSeries(X;r)].

    [(1÷(1-g))]_m = if (m =_z 0) then 1 else 0 fi  ∈ PowerSeries(X;r) supposing g = [g]_n ∈ PowerSeries(X;r)

supposing valueall-type(X)

Definition: fps-exp
(f)^(n) == f ↑fps-rng(r) n

Lemma: fps-exp_wf
∀[X:Type]

  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f:PowerSeries(X;r)]. ∀[n:ℕ].  ((f)^(n) ∈ PowerSeries(X;r)) supposing valueall-type(X)

Lemma: fps-exp-zero
∀[X:Type]

  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f:PowerSeries(X;r)].  ((f)^(0) = 1 ∈ PowerSeries(X;r)) supposing valueall-type(X)

Lemma: fps-exp-unroll
∀[X:Type]

  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[n:ℕ⁺]. ∀[f:PowerSeries(X;r)].  ((f)^(n) = ((f)^(n - 1)*f) ∈ PowerSeries(X;r))

supposing valueall-type(X)

Lemma: fps-exp-add
∀[X:Type]

  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[n,m:ℕ]. ∀[f:PowerSeries(X;r)].  ((f)^(n + m) = ((f)^(n)*(f)^(m)) ∈ PowerSeries(X;r))

supposing valueall-type(X)

Lemma: fps-exp-one
∀[X:Type]

  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f:PowerSeries(X;r)].  ((f)^(1) = f ∈ PowerSeries(X;r)) supposing valueall-type(X)

Lemma: fps-single-bag-rep
∀[X:Type]

  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. ∀[n:ℕ].  (<bag-rep(n;x)> = (atom(x))^(n) ∈ PowerSeries(X;r))

  supposing valueall-type(X)

Lemma: fps-exp-linear-coeff
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[x,y:X].
    ∀[r:CRng]. ∀[k:|r|]. ∀[m,n:ℕ].
      ((((k)*atom(x)+atom(y)))^(m)[bag-rep(n;x)] = if (n =_z m) then k ↑r m else 0 fi  ∈ |r|)
    supposing ¬(x = y ∈ X)
  supposing valueall-type(X)

Lemma: fps-geometric-slice
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[m:ℕ]. ∀[n:ℕ⁺]. ∀[g:PowerSeries(X;r)].
    [(1÷(1-g))]_m = if (m rem n =_z 0) then (g)^(m ÷ n) else 0 fi  ∈ PowerSeries(X;r)
    supposing g = [g]_n ∈ PowerSeries(X;r)
  supposing valueall-type(X)

Lemma: fps-geometric-slice1
∀[X:Type]

  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[m:ℕ]. ∀[g:PowerSeries(X;r)].  ([(1÷(1-[g]_1))]_m = ([g]_1)^(m) ∈ PowerSeries(X;r))

supposing valueall-type(X)

Definition: fps-elim
fps-elim(x) == λf,b. if bag-deq-member(eq;x;b) then 0 else f[b] fi

Lemma: fps-elim_wf

∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X].  (fps-elim(x) ∈ PowerSeries(X;r) ⟶ PowerSeries(X;r))

Lemma: fps-elim-hom
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X].
    (FunThru2op(PowerSeries(X;r);PowerSeries(X;r);λf,g. (f+g);λf,g. (f+g);fps-elim(x))
    ∧ FunThru2op(PowerSeries(X;r);PowerSeries(X;r);λf,g. (f*g);λf,g. (f*g);fps-elim(x))
    ∧ ((fps-elim(x) 1) = 1 ∈ PowerSeries(X;r)))
  supposing valueall-type(X)

Lemma: fps-elim-div
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f,g:PowerSeries(X;r)]. ∀[z:|r|]. ∀[x:X].
    (fps-elim(x) (f÷g)) = (fps-elim(x) f÷fps-elim(x) g) ∈ PowerSeries(X;r)
    supposing (¬((fps-elim(x) f) = 0 ∈ PowerSeries(X;r))) ∧ ((g[{}] * z) = 1 ∈ |r|)
  supposing valueall-type(X)

Definition: fps-elim-x
f(x:=0) ==  fps-elim(x) f

Lemma: fps-elim-x_wf

∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f:PowerSeries(X;r)]. ∀[x:X].  (f(x:=0) ∈ PowerSeries(X;r))

Lemma: fps-elim-x-mul
∀[X:Type]

  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. ∀[f,g:PowerSeries(X;r)].  ((f*g)(x:=0) = (f(x:=0)*g(x:=0)) ∈ PowerSeries(X;r))

supposing valueall-type(X)

Lemma: fps-elim-x-add
∀[X:Type]

  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. ∀[f,g:PowerSeries(X;r)].  ((f+g)(x:=0) = (f(x:=0)+g(x:=0)) ∈ PowerSeries(X;r))

supposing valueall-type(X)

Lemma: fps-elim-x-neg

∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. ∀[g:PowerSeries(X;r)].  (-(g)(x:=0) = -(g(x:=0)) ∈ PowerSeries(X;r))

Lemma: fps-elim-x-elim-x

∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. ∀[g:PowerSeries(X;r)].  (g(x:=0)(x:=0) = g(x:=0) ∈ PowerSeries(X;r))

Lemma: fps-elim-x-elim-y
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x,y:X]. ∀[g:PowerSeries(X;r)].
  (g(x:=0)(y:=0) = g(y:=0)(x:=0) ∈ PowerSeries(X;r))

Lemma: fps-elim-x-one
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X].  (1(x:=0) = 1 ∈ PowerSeries(X;r))

Lemma: fps-elim-x-atom
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x,y:X].
  (atom(y)(x:=0) = if eq x y then 0 else atom(y) fi  ∈ PowerSeries(X;r))

Lemma: fps-elim-x-zero
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X].  (0(x:=0) = 0 ∈ PowerSeries(X;r))

Lemma: fps-elim-x-sub
∀[X:Type]

  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. ∀[f,g:PowerSeries(X;r)].  ((f-g)(x:=0) = (f(x:=0)-g(x:=0)) ∈ PowerSeries(X;r))

  supposing valueall-type(X)

Definition: fps-compose
g(x:=f) ==  λbs.Σ(L∈bag-parts'(eq;bs;x)). g[hd(L) + bag-rep(||tl(L)||;x)] * Πa ∈ tl(L). f[a]

Lemma: fps-compose_wf
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. ∀[g,f:PowerSeries(X;r)].  (g(x:=f) ∈ PowerSeries(X;r))
  supposing valueall-type(X)

Lemma: fps-compose-add
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. ∀[g,f,h:PowerSeries(X;r)].
    ((g+h)(x:=f) = (g(x:=f)+h(x:=f)) ∈ PowerSeries(X;r))
  supposing valueall-type(X)

Lemma: fps-compose-neg
∀[X:Type]

  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. ∀[g,f:PowerSeries(X;r)].  (-(g)(x:=f) = -(g(x:=f)) ∈ PowerSeries(X;r))

  supposing valueall-type(X)

Lemma: fps-compose-scalar-mul
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[c:|r|]. ∀[x:X]. ∀[g,f:PowerSeries(X;r)].
    ((c)*g(x:=f) = (c)*g(x:=f) ∈ PowerSeries(X;r))
  supposing valueall-type(X)

Lemma: fps-compose-sub
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. ∀[g,f,h:PowerSeries(X;r)].
    ((g-h)(x:=f) = (g(x:=f)-h(x:=f)) ∈ PowerSeries(X;r))
  supposing valueall-type(X)

Lemma: fps-compose-one
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. ∀[f:PowerSeries(X;r)].  (1(x:=f) = 1 ∈ PowerSeries(X;r))
  supposing valueall-type(X)

Lemma: fps-compose-zero
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. ∀[f:PowerSeries(X;r)].  (0(x:=f) = 0 ∈ PowerSeries(X;r))
  supposing valueall-type(X)

Lemma: fps-compose-atom-neq
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x,y:X].
    ∀[f:PowerSeries(X;r)]. (atom(y)(x:=f) = atom(y) ∈ PowerSeries(X;r)) supposing ¬(x = y ∈ X)
  supposing valueall-type(X)

Lemma: fps-compose-atom-eq
∀[X:Type]

  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. ∀[f:PowerSeries(X;r)].  (atom(x)(x:=f) = (f-(f[{}])*1) ∈ PowerSeries(X;r))

supposing valueall-type(X)

Lemma: fps-compose-atom
∀[X:Type]
∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x,y:X]. ∀[f:PowerSeries(X;r)].

    atom(y)(x:=f) = if eq y x then f else atom(y) fi  ∈ PowerSeries(X;r) supposing f[{}] = 0 ∈ |r|

  supposing valueall-type(X)

Lemma: fps-compose-mul
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. ∀[g,f,h:PowerSeries(X;r)].
    ((g*h)(x:=f) = (g(x:=f)*h(x:=f)) ∈ PowerSeries(X;r))
  supposing valueall-type(X)

Lemma: fps-compose-exp
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. ∀[g,f:PowerSeries(X;r)]. ∀[n:ℕ].
    ((g)^(n)(x:=f) = (g(x:=f))^(n) ∈ PowerSeries(X;r))
  supposing valueall-type(X)

Lemma: fps-compose-fps-product
∀[X:Type]

  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. ∀[f:PowerSeries(X;r)]. ∀[T:Type]. ∀[b:bag(T)]. ∀[G:T ⟶ PowerSeries(X;r)].

(Π(i∈b).G[i](x:=f) = Π(i∈b).G[i](x:=f) ∈ PowerSeries(X;r))
 supposing valueall-type(X)

Lemma: fps-compose-single-disjoint
∀[X:Type]
 ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. ∀[v:bag(X)].
 ((¬x ↓∈ v) ⇒ (∀[f:PowerSeries(X;r)]. (<v>(x:=f) = <v> ∈ PowerSeries(X;r))))
 supposing valueall-type(X)

Lemma: fps-compose-single-general
∀[X:Type]
 ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. ∀[b:bag(X)]. ∀[f:PowerSeries(X;r)].
 ((x:=f) = (<(b|¬x)>*((f-(f[{}])*1))^(#((b|x)))) ∈ PowerSeries(X;r))
 supposing valueall-type(X)

Lemma: fps-compose-single
∀[X:Type]
 ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. ∀[b:bag(X)]. ∀[f:PowerSeries(X;r)].
 (x:=f) = (<(b|¬x)>*(f)^(#((b|x)))) ∈ PowerSeries(X;r) supposing f[{}] = 0 ∈ |r|
 supposing valueall-type(X)

Definition: fps-restrict
fps-restrict(eq;r;f;d) == λb.if deq-sub-bag(eq;b;d) then f[b] else 0 fi

Lemma: fps-restrict_wf
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f:PowerSeries(X;r)]. ∀[d:bag(X)].
 (fps-restrict(eq;r;f;d) ∈ PowerSeries(X;r))

Lemma: fps-restrict-summation
∀[X:Type]
 ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f:PowerSeries(X;r)]. ∀[d:bag(X)].
 (fps-restrict(eq;r;f;d) = Σ(x∈sub-bags(eq;d)). (f[x])*<x> ∈ PowerSeries(X;r))
 supposing valueall-type(X)

Lemma: fps-restrict-empty
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f:PowerSeries(X;r)].
 (fps-restrict(eq;r;f;{}) = (f[{}])*1 ∈ PowerSeries(X;r))

Definition: fps-ucont

fps-ucont(X;eq;r;f.G[f]) ==  ∀b:bag(X). ∃d:bag(X). ∀f:PowerSeries(X;r). (G[f][b] = G[fps-restrict(eq;r;f;d)][b] ∈ |r|)

Lemma: fps-ucont_wf

∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[G:PowerSeries(X;r) ⟶ PowerSeries(X;r)].  (fps-ucont(X;eq;r;f.G[f]) ∈ ℙ)

Lemma: fps-ucont-composition
∀[X:Type]
 ∀eq:EqDecider(X). ∀r:CRng. ∀F,G:PowerSeries(X;r) ⟶ PowerSeries(X;r).
 (fps-ucont(X;eq;r;f.F[f]) ⇒ fps-ucont(X;eq;r;f.G[f]) ⇒ fps-ucont(X;eq;r;f.F o G[f]))
 supposing valueall-type(X)

Lemma: fps-linear-ucont-equal
∀[X:Type]
 ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[F,G:PowerSeries(X;r) ⟶ PowerSeries(X;r)].
 F = G ∈ (PowerSeries(X;r) ⟶ PowerSeries(X;r))
 supposing fps-ucont(X;eq;r;f.F[f])
 ∧ fps-ucont(X;eq;r;f.G[f])
 ∧ (∀f,g:PowerSeries(X;r). (F[(f+g)] = (F[f]+F[g]) ∈ PowerSeries(X;r)))
 ∧ (∀f,g:PowerSeries(X;r). (G[(f+g)] = (G[f]+G[g]) ∈ PowerSeries(X;r)))
 ∧ (∀c:|r|. ∀f:PowerSeries(X;r). (F[(c)*f] = (c)*F[f] ∈ PowerSeries(X;r)))
 ∧ (∀c:|r|. ∀f:PowerSeries(X;r). (G[(c)*f] = (c)*G[f] ∈ PowerSeries(X;r)))
 ∧ (∀b:bag(X). (F[] = G[] ∈ PowerSeries(X;r)))
 supposing valueall-type(X)

Lemma: fps-add-ucont-general
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[F,G:PowerSeries(X;r) ⟶ PowerSeries(X;r)].
 (fps-ucont(X;eq;r;f.F[f]) ⇒ fps-ucont(X;eq;r;f.G[f]) ⇒ fps-ucont(X;eq;r;f.(F[f]+G[f])))

Lemma: fps-add-ucont
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[g:PowerSeries(X;r)]. fps-ucont(X;eq;r;f.(f+g))

Lemma: fps-id-ucont
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. fps-ucont(X;eq;r;f.f)

Lemma: fps-mul-ucont

∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[g:PowerSeries(X;r)].  fps-ucont(X;eq;r;f.(f*g)) supposing valueall-type(X)

Lemma: fps-compose-ucont
∀[X:Type]

  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[g:PowerSeries(X;r)].  ∀x:X. fps-ucont(X;eq;r;f.f(x:=g)) supposing valueall-type(X)

Lemma: fps-slice-ucont
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀n:ℕ. fps-ucont(X;eq;r;f.[f]_n)

Lemma: fps-compose-compose
∀[X:Type]

  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f,g,h:PowerSeries(X;r)]. ∀[x:X].  (f(x:=g)(x:=h) = f(x:=g(x:=h)) ∈ PowerSeries(X;r))

supposing valueall-type(X)

Lemma: fps-compose-identity
∀[X:Type]

  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f:PowerSeries(X;r)]. ∀[x:X].  (f(x:=atom(x)) = f ∈ PowerSeries(X;r))

supposing valueall-type(X)

Definition: fps-Pascal
fps-Pascal(r;x;y;f) == ∀b:bag(Atom). (f[({x} + {y}) + b] = (f[{x} + b] +r f[{y} + b]) ∈ |r|)

Lemma: fps-Pascal_wf
∀[r:CRng]. ∀[x,y:Atom]. ∀[f:PowerSeries(r)]. (fps-Pascal(r;x;y;f) ∈ ℙ)

Definition: fps-pascal
Δ(x,y) == (1÷(1-(<{x}>+<{y}>)))

Lemma: fps-pascal_wf
∀[r:CRng]. ∀[x,y:Atom]. (Δ(x,y) ∈ PowerSeries(r))

Lemma: fps-pascal-slice
∀[r:CRng]. ∀[x,y:Atom]. ∀[n:ℕ]. ([Δ(x,y)]_n = ((<{x}>+<{y}>))^(n) ∈ PowerSeries(r))

Lemma: fps-pascal-elim

∀[r:CRng]. ∀[x,y:Atom].  Δ(x,y)(x:=0) = (1÷(1-atom(y))) ∈ PowerSeries(r) supposing (¬(x = y ∈ Atom)) ∧ (¬(1 = 0 ∈ |r|))

Lemma: fps-pascal-symmetry
∀[r:CRng]. ∀[x,y:Atom]. (Δ(x,y) = Δ(y,x) ∈ PowerSeries(r))

Lemma: fps-Pascal-iff
∀[r:CRng]. ∀[x,y:Atom]. ∀[f:PowerSeries(r)].
 fps-Pascal(r;x;y;f) ⇐⇒ f = (((((1-atom(y))*f(x:=0))+((1-atom(x))*f(y:=0)))-f(x:=0)(y:=0))*Δ(x,y)) ∈ PowerSeries(r)
 supposing ¬(x = y ∈ Atom)

Definition: Pascal-completion
Pascal-completion(r;f;g;x;y) == (((((1-atom(y))*f)+((1-atom(x))*g))-f(y:=0))*Δ(x,y))

Lemma: Pascal-completion_wf
∀[r:CRng]. ∀[f,g:PowerSeries(r)]. ∀[x,y:Atom]. (Pascal-completion(r;f;g;x;y) ∈ PowerSeries(r))

Lemma: Pascal-completion-property
∀[r:CRng]. ∀[f,g:PowerSeries(r)]. ∀[x,y:Atom].
 ((Pascal-completion(r;f;g;x;y)(x:=0) = f ∈ PowerSeries(r))
 ∧ (Pascal-completion(r;f;g;x;y)(y:=0) = g ∈ PowerSeries(r))
 ∧ fps-Pascal(r;x;y;Pascal-completion(r;f;g;x;y)))
 ∧ (∀h:PowerSeries(r)
 (fps-Pascal(r;x;y;h)
 ⇒ (h(x:=0) = f ∈ PowerSeries(r))
 ⇒ (h(y:=0) = g ∈ PowerSeries(r))
 ⇒ (h = Pascal-completion(r;f;g;x;y) ∈ PowerSeries(r))))
 supposing (¬(1 = 0 ∈ |r|))
 ∧ (¬(x = y ∈ Atom))
 ∧ (f(x:=0) = f ∈ PowerSeries(r))
 ∧ (g(y:=0) = g ∈ PowerSeries(r))
 ∧ (f(y:=0) = g(x:=0) ∈ PowerSeries(r))

Definition: fps-set-to-one
[f]_n(y:=1) == λb.if 0 <z (#y in b) ∨_bn <z #(b) then 0 else f[b + bag-rep(n - #(b);y)] fi

Lemma: fps-set-to-one_wf
∀[r:CRng]. ∀[f:PowerSeries(r)]. ∀[y:Atom]. ∀[n:ℕ]. ([f]_n(y:=1) ∈ PowerSeries(r))

Lemma: fps-set-to-one-ucont
∀[r:CRng]. ∀y:Atom. ∀n:ℕ. fps-ucont(Atom;AtomDeq;r;f.[f]_n(y:=1))

Lemma: fps-set-to-one-neg

∀[r:CRng]. ∀[f:PowerSeries(r)]. ∀[y:Atom]. ∀[n:ℕ].  ([-(f)]_n(y:=1) = -([f]_n(y:=1)) ∈ PowerSeries(r))

Lemma: fps-set-to-one-scalar-mul

∀[r:CRng]. ∀[c:|r|]. ∀[f:PowerSeries(r)]. ∀[y:Atom]. ∀[n:ℕ].  ([(c)*f]_n(y:=1) = (c)*[f]_n(y:=1) ∈ PowerSeries(r))

Lemma: fps-set-to-one-add

∀[r:CRng]. ∀[f,g:PowerSeries(r)]. ∀[y:Atom]. ∀[n:ℕ].  ([(f+g)]_n(y:=1) = ([f]_n(y:=1)+[g]_n(y:=1)) ∈ PowerSeries(r))

Lemma: fps-set-to-one-sub

∀[r:CRng]. ∀[f,g:PowerSeries(r)]. ∀[y:Atom]. ∀[n:ℕ].  ([(f-g)]_n(y:=1) = ([f]_n(y:=1)-[g]_n(y:=1)) ∈ PowerSeries(r))

Lemma: fps-set-to-one-zero
∀[r:CRng]. ∀[y:Atom]. ∀[n:ℕ]. ([0]_n(y:=1) = 0 ∈ PowerSeries(r))

Lemma: fps-set-to-one-single
∀[r:CRng]. ∀[y:Atom]. ∀[n:ℕ]. ∀[b:bag(Atom)].
 ([]_n(y:=1) = if (#(b) =_z n) then <(b|¬y)> else 0 fi ∈ PowerSeries(r))

Lemma: fps-set-to-one-slice
∀[r:CRng]. ∀[y:Atom]. ∀[n,k:ℕ]. ∀[f:PowerSeries(r)].
 ([[f]_k]_n(y:=1) = if (k =_z n) then [f]_n(y:=1) else 0 fi ∈ PowerSeries(r))

Lemma: fps-set-to-one-one

∀[r:CRng]. ∀[y:Atom]. ∀[n:ℕ].  ([1]_n(y:=1) = if (n =_z 0) then 1 else 0 fi  ∈ PowerSeries(r))

Lemma: KozenSilva-lemma
∀[r:CRng]. ∀[x,y:Atom]. ∀[h:PowerSeries(r)]. ∀[n,m:ℕ].
[([h]_n(y:=1)*Δ(x,y))]_m = ([h]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n)) ∈ PowerSeries(r)
supposing (n ≤ m) ∧ (¬(x = y ∈ Atom))

Definition: Moessner-aux

Moessner-aux(r;x;y;h;d;k)==r if (k =_z 0) then h else ([Moessner-aux(r;x;y;h;d;k - 1)]_Σ(d i | i < k)(y:=1)*Δ(x,y)) fi

Lemma: Moessner-aux_wf

∀[r:CRng]. ∀[x,y:Atom]. ∀[h:PowerSeries(r)]. ∀[d:ℕ ⟶ ℕ]. ∀[k:ℕ].  (Moessner-aux(r;x;y;h;d;k) ∈ PowerSeries(r))

Definition: Moessner
Moessner(r;x;y;h;d;k) == [Moessner-aux(r;x;y;h;d;k)]_Σ(d i | i < k + 1)

Lemma: Moessner_wf

∀[r:CRng]. ∀[x,y:Atom]. ∀[h:PowerSeries(r)]. ∀[d:ℕ ⟶ ℕ]. ∀[k:ℕ].  (Moessner(r;x;y;h;d;k) ∈ PowerSeries(r))

Lemma: KozenSilva-theorem
∀[r:CRng]. ∀[x,y:Atom].
∀[h:PowerSeries(r)]. ∀[d:ℕ ⟶ ℕ]. ∀[k:ℕ].
(Moessner(r;x;y;h;d;k)

    = ([h]_d 0(y:=((k ⋅r 1)*atom(x)+atom(y)))*Π(i∈upto(k)).((((k - i) ⋅r 1)*atom(x)+atom(y)))^(d (i + 1)))

    ∈ PowerSeries(r))
  supposing ¬(x = y ∈ Atom)

Lemma: KozenSilva-corollary0
∀[r:CRng]. ∀[x,y:Atom].
  ∀[d:ℕ ⟶ ℕ]. ∀[k:ℕ].
    (Moessner(r;x;y;1;λi.if (i =_z 0) then 0 else d (i - 1) fi ;k)
    = Π(i∈upto(k)).((((k - i) ⋅r 1)*atom(x)+atom(y)))^(d i)
    ∈ PowerSeries(r))
  supposing ¬(x = y ∈ Atom)

Lemma: KozenSilva-corollary1
∀[x,y:Atom].
  ∀[d:ℕ ⟶ ℕ]. ∀[k:ℕ].
    (Moessner(ℤ-rng;x;y;1;λi.if (i =_z 0) then 0 else d (i - 1) fi ;k)
    = Π(i∈upto(k)).(((k - i)*atom(x)+atom(y)))^(d i)
    ∈ PowerSeries(ℤ-rng))
  supposing ¬(x = y ∈ Atom)

Lemma: KozenSilva-corollary2
∀[x,y:Atom].
  ∀[d:ℕ ⟶ ℕ]. ∀[k:ℕ].

    (Moessner(ℤ-rng;x;y;1;λi.if (i =_z 0) then 0 else d (i - 1) fi ;k)[bag-rep(Σ(d i | i < k);x)]

= Π((k - i)^(d i) | i < k)
 ∈ ℤ)
 supposing ¬(x = y ∈ Atom)

Lemma: Moessner-theorem
∀[x,y:Atom].
 ∀[n:ℕ]. ∀[k:ℕ⁺].

    (Moessner(ℤ-rng;x;y;1;λi.if (i =_z 0) then 0 if (i =_z 1) then n else 0 fi ;k)[bag-rep(n;x)] = k^n ∈ ℤ)

  supposing ¬(x = y ∈ Atom)

Lemma: Long-theorem
∀[x,y:Atom].
  ∀[a,b:ℤ]. ∀[n,k:ℕ⁺].
    (Moessner(ℤ-rng;x;y;((a - b)*atom(x)+(b)*atom(y));λi.if (i =_z 0) then 1

                                                         if (i =_z 1) then n - 1

                                                         else 0

                                                         fi ;k)[bag-rep(n;x)]

    = ((a + ((k - 1) * b)) * k^(n - 1))
    ∈ ℤ)
  supposing ¬(x = y ∈ Atom)

Lemma: Paasche-theorem
∀[x,y:Atom].

  ∀[k:ℕ]. (Moessner(ℤ-rng;x;y;1;λi.if (i =_z 0) then 0 else 1 fi ;k)[bag-rep(k;x)] = (k)! ∈ ℤ) supposing ¬(x = y ∈ Atom)

Lemma: Paasche-theorem2

∀[x,y:Atom].  ∀[k:ℕ]. (Moessner(ℤ-rng;x;y;1;λi.i;k)[bag-rep((k * (1 + k)) ÷ 2;x)] = (k)!! ∈ ℤ) supposing ¬(x = y ∈ Atom)

Definition: Longs-algorithm
Longs-algorithm(h;n;a;b;c)
==r if a=0
 then h c
 else if (c) < (0)
 then 0
 else if (b) < (0)
 then 0
 else if b=0
 then eval a' = a - 1 in
 eval c' = c - 1 in
 eval b' = (n a') - c in

                                Longs-algorithm(h;n;a;b;c') + Longs-algorithm(h;n;a';b';c)

else eval b' = b - 1 in
eval c' = c - 1 in

                                Longs-algorithm(h;n;a;b';c) + Longs-algorithm(h;n;a;b;c')

Lemma: Longs-algorithm_wf
∀[h:ℤ ⟶ ℤ]. ∀n:ℕ ⟶ ℕ. ∀a,b,c:ℕ.  (Longs-algorithm(h;n;a;b;c) ∈ ℤ)

Definition: Moessner-alg
Moessner-alg(k;n) ==  Longs-algorithm(λi.if (i =_z 0) then 1 else 0 fi ;λa.k;n;0;k)

Lemma: Moessner-alg_wf
∀[n,k:ℕ].  (Moessner-alg(k;n) ∈ ℤ)

Definition: Paasche-alg-1
Paasche-alg-1(k) ==  Longs-algorithm(λi.if (i =_z 0) then 1 else 0 fi ;λa.a;k;0;k)

Lemma: Paasche-alg-1_wf
∀[k:ℕ]. (Paasche-alg-1(k) ∈ ℤ)

Definition: Paasche-alg-2

Paasche-alg-2(k) ==  Longs-algorithm(λi.if (i =_z 0) then 1 else 0 fi ;λa.((a * (a + 1)) ÷ 2);k;0;(k * (k + 1)) ÷ 2)

Lemma: Paasche-alg-2_wf
∀[k:ℕ]. (Paasche-alg-2(k) ∈ ℤ)

Definition: fps-degree-bound
fps-degree-bound(r;f;d) == ∀[b:bag(Atom)]. f[b] = 0 ∈ |r| supposing d < #(b)

Lemma: fps-degree-bound_wf
∀[r:CRng]. ∀[f:PowerSeries(r)]. ∀[d:ℕ]. (fps-degree-bound(r;f;d) ∈ ℙ)

Definition: fps-support
fps-support(r;f;s) == ∀[b:bag(Atom)]. f[b] = 0 ∈ |r| supposing ¬sub-bag(Atom;b;s)

Lemma: fps-support_wf
∀[r:CRng]. ∀[f:PowerSeries(r)]. ∀[s:bag(Atom)]. (fps-support(r;f;s) ∈ ℙ)

Lemma: fps-support-degree-bound
∀[r:CRng]. ∀[f:PowerSeries(r)]. ∀[s:bag(Atom)]. (fps-support(r;f;s) ⇒ fps-degree-bound(r;f;#(s)))

Definition: fps-deriv
df/dx == λb.(int-to-ring(r;(#x in b) + 1) * (f x.b))

Lemma: fps-deriv_wf
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f:PowerSeries(X;r)]. ∀[x:X]. (df/dx ∈ PowerSeries(X;r))

Lemma: fps-deriv-ucont
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀x:X. fps-ucont(X;eq;r;f.df/dx)

Lemma: fps-deriv-add
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f,g:PowerSeries(X;r)]. ∀[x:X].
 (d(f+g)/dx = (df/dx+dg/dx) ∈ PowerSeries(X;r))

Lemma: fps-deriv-scalar-mul
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f:PowerSeries(X;r)]. ∀[c:|r|]. ∀[x:X].
 (d(c)*f/dx = (c)*df/dx ∈ PowerSeries(X;r))

Lemma: fps-deriv-neg

∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f:PowerSeries(X;r)]. ∀[x:X].  (d-(f)/dx = -(df/dx) ∈ PowerSeries(X;r))

Lemma: fps-deriv-one
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. (d1/dx = 0 ∈ PowerSeries(X;r))

Lemma: fps-deriv-single
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[b:bag(X)]. ∀[x:X].
 (d/dx = (int-to-ring(r;(#x in b)))*<bag-drop(eq;b;x)> ∈ PowerSeries(X;r))

Lemma: fps-deriv-mul
∀[X:Type]
 ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f,g:PowerSeries(X;r)]. ∀[x:X].
 (d(f*g)/dx = ((f*dg/dx)+(df/dx*g)) ∈ PowerSeries(X;r))
 supposing valueall-type(X)

Lemma: fps-deriv-div
∀[X:Type]
 ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f,g:PowerSeries(X;r)]. ∀[x:X]. ∀[u:|r|].
 d(f÷g)/dx = (((df/dx*g)-(f*dg/dx))÷(g*g)) ∈ PowerSeries(X;r) supposing (g[{}] * u) = 1 ∈ |r|
 supposing valueall-type(X)

Lemma: fps-deriv-compose
∀[X:Type]
 ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f,g:PowerSeries(X;r)]. ∀[x:X].
 (df(x:=g)/dx = (df/dx(x:=g)*dg/dx) ∈ PowerSeries(X;r))
 supposing valueall-type(X)

Lemma: fps-deriv-commutes

∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f,g:PowerSeries(X;r)]. ∀[x,y:X].  (ddf/dx/dy = ddf/dy/dx ∈ PowerSeries(X;r))

Definition: mv-polynomial
mv-polynomial(r) == s:bag(Atom) × {f:PowerSeries(r)| fps-support(r;f;s)}

Lemma: mv-polynomial_wf
∀[r:CRng]. (mv-polynomial(r) ∈ Type)

Definition: mvp-add
mvp-add(r;p;q) == let s,f = p in let s',g = q in <bag-lub(AtomDeq;s;s'), (f+g)>

Lemma: mvp-add_wf
∀[r:CRng]. ∀[p,q:mv-polynomial(r)]. (mvp-add(r;p;q) ∈ mv-polynomial(r))

Home Index