Big operators and fin
#
Some results about products and sums over the type fin
.
The most important results are the induction formulas fin.prod_univ_cast_succ
and fin.prod_univ_succ
, and the formula fin.prod_const
for the product of a
constant function. These results have variants for sums instead of products.
A sum of a function f : fin 0 → β
is 0
because fin 0
is empty
A product of a function f : fin 0 → β
is 1
because fin 0
is empty
A product of a function f : fin (n + 1) → β
over all fin (n + 1)
is the product of f x
, for some x : fin (n + 1)
times the remaining product
A sum of a function f : fin (n + 1) → β
over all fin (n + 1)
is the sum of f x
,
for some x : fin (n + 1)
plus the remaining product
A product of a function f : fin (n + 1) → β
over all fin (n + 1)
is the product of f 0
plus the remaining product
A sum of a function f : fin (n + 1) → β
over all fin (n + 1)
is the sum of f 0
plus the remaining product
A sum of a function f : fin (n + 1) → β
over all fin (n + 1)
is the sum of
f (fin.last n)
plus the remaining sum
A product of a function f : fin (n + 1) → β
over all fin (n + 1)
is the product of f (fin.last n)
plus the remaining product
For f = (a₁, ..., aₙ)
in αⁿ
, partial_prod f
is (1, a₁, a₁a₂, ..., a₁...aₙ)
in αⁿ⁺¹
.
Equations
- fin.partial_prod f i = (list.take ↑i (list.of_fn f)).prod
For f = (a₁, ..., aₙ)
in αⁿ
, partial_sum f
is
(0, a₁, a₁ + a₂, ..., a₁ + ... + aₙ)
in αⁿ⁺¹
.
Equations
- fin.partial_sum f i = (list.take ↑i (list.of_fn f)).sum