Self-convolution coefficients of a formal power series

PowerSeries.coeff_mul gives the coefficients of a product as a sum over Finset.antidiagonal. For a recursion that reads off one coefficient from strictly earlier ones the equivalent sum over Finset.range is what is wanted, so this file names the two shapes that occur, for a square and for a cube, and records the translation.

Both are stated for an arbitrary coefficient function f : ℕ → R rather than for the coefficients of a given series: the congruence lemmas compare two such functions, and the truncation lemmas feed in a modified one.

The load-bearing facts are PowerSeries.selfConvTwo_congr and PowerSeries.selfConvThree_congr. When f 0 = 0 the convolution at index n depends only on the values of f strictly below n, because the extreme terms of the sum each carry a factor f 0. That is what makes a recursion defined through these convolutions well founded.

Main definitions

• PowerSeries.selfConvTwo, PowerSeries.selfConvThree: the Finset.range-form convolution sums computing the coefficients of a square and of a cube.

Main results

• PowerSeries.selfConvTwo_def, PowerSeries.selfConvThree_def: the defining formulas, as named lemmas. Rewrite with these rather than unfolding the definitions.
• PowerSeries.coeff_pow_two_eq_selfConvTwo, PowerSeries.coeff_pow_three_eq_selfConvThree: those sums do compute the coefficients of w ^ 2 and w ^ 3.
• PowerSeries.coeff_mul_congr: the n-th coefficient of q * v, for q with vanishing constant coefficient, depends only on the coefficients of v strictly below n.
• PowerSeries.selfConvTwo_congr_le, PowerSeries.selfConvThree_congr_le: the convolution at m depends only on the values of the function on [0, m]. No hypothesis is needed.
• PowerSeries.selfConvTwo_congr, PowerSeries.selfConvThree_congr: for a function vanishing at 0, that bound sharpens to the values strictly below n.
• PowerSeries.selfConvTwo_truncate, PowerSeries.selfConvThree_truncate and their _of_lt companions: truncating the function above n leaves the convolution unchanged at n (needing f 0 = 0) and at every smaller index (needing nothing).
• PowerSeries.selfConvTwo_eq_zero, PowerSeries.selfConvThree_eq_zero: a function vanishing below d has square vanishing below 2 * d and cube vanishing below 3 * d.

Provenance

Adapted from the AINTLIB HasseWeil project (github.com/CBirkbeck/AINTLIB, Apache-2.0, pinned by TauCetiRoadmap/EllipticCurves/README.md at dev/hasse-weil @ 513e83879e2f), HasseWeil/FormalGroup.lean, declarations conv₂ and conv₃ together with the coefficient lemmas coeff_formalW_sq and coeff_formalW_cube.

Changes from the source. The source states its two convolution-coefficient lemmas only for its formalW, although neither proof uses anything about that series; they are stated here for an arbitrary series. The truncation lemmas likewise assumed formalW, and are stated here for any f vanishing at 0, as consequences of the sharper congruence lemmas. The source works throughout over a CommRing; nothing here needs more than a Semiring.

def PowerSeries.selfConvTwo {R : Type u_1} [Semiring R] (f : ℕ → R) (n : ℕ) : R

The n-th coefficient of the square of the series with coefficients f.

Equations

• PowerSeries.selfConvTwo f n = ∑ i ∈ Finset.range (n + 1), f i * f (n - i)

theorem PowerSeries.selfConvTwo_def {R : Type u_1} [Semiring R] (f : ℕ → R) (n : ℕ) : selfConvTwo f n = ∑ i ∈ Finset.range (n + 1), f i * f (n - i)

The defining formula for selfConvTwo.

def PowerSeries.selfConvThree {R : Type u_1} [Semiring R] (f : ℕ → R) (n : ℕ) : R

The n-th coefficient of the cube of the series with coefficients f.

Equations

• PowerSeries.selfConvThree f n = ∑ i ∈ Finset.range (n + 1), ∑ j ∈ Finset.range (n - i + 1), f i * f j * f (n - i - j)

theorem PowerSeries.selfConvThree_def {R : Type u_1} [Semiring R] (f : ℕ → R) (n : ℕ) : selfConvThree f n = ∑ i ∈ Finset.range (n + 1), ∑ j ∈ Finset.range (n - i + 1), f i * f j * f (n - i - j)

The defining formula for selfConvThree.

theorem PowerSeries.coeff_mul_congr {R : Type u_1} [Semiring R] {q v v' : PowerSeries R} (hq : constantCoeff q = 0) {n : ℕ} (h : ∀ m < n, (coeff m) v = (coeff m) v') : (coeff n) (q * v) = (coeff n) (q * v')

Multiplying by a series with vanishing constant coefficient makes the n-th coefficient of the product depend only on the coefficients of the other factor strictly below n: the term that would use the n-th one carries the vanishing constant coefficient.

theorem PowerSeries.coeff_pow_two_eq_selfConvTwo {R : Type u_1} [Semiring R] (w : PowerSeries R) (n : ℕ) : (coeff n) (w ^ 2) = selfConvTwo (fun (k : ℕ) => (coeff k) w) n

selfConvTwo computes the coefficients of a square.

theorem PowerSeries.coeff_pow_three_eq_selfConvThree {R : Type u_1} [Semiring R] (w : PowerSeries R) (n : ℕ) : (coeff n) (w ^ 3) = selfConvThree (fun (k : ℕ) => (coeff k) w) n

selfConvThree computes the coefficients of a cube.

theorem PowerSeries.selfConvTwo_congr {R : Type u_1} [Semiring R] {f g : ℕ → R} (hf : f 0 = 0) (hg : g 0 = 0) {n : ℕ} (h : ∀ m < n, f m = g m) : selfConvTwo f n = selfConvTwo g n

selfConvTwo f n depends only on the values of f strictly below n, provided f vanishes at 0: the two extreme terms of the convolution each carry a factor f 0.

theorem PowerSeries.selfConvThree_congr {R : Type u_1} [Semiring R] {f g : ℕ → R} (hf : f 0 = 0) (hg : g 0 = 0) {n : ℕ} (h : ∀ m < n, f m = g m) : selfConvThree f n = selfConvThree g n

The cube analogue of selfConvTwo_congr.

theorem PowerSeries.selfConvTwo_congr_le {R : Type u_1} [Semiring R] {f g : ℕ → R} {m : ℕ} (h : ∀ k ≤ m, f k = g k) : selfConvTwo f m = selfConvTwo g m

selfConvTwo f m depends only on the values of f on [0, m]. Unlike selfConvTwo_congr this needs no hypothesis on f, because every index occurring in the sum is at most m; the vanishing hypothesis there buys the strict bound < m instead.

theorem PowerSeries.selfConvThree_congr_le {R : Type u_1} [Semiring R] {f g : ℕ → R} {m : ℕ} (h : ∀ k ≤ m, f k = g k) : selfConvThree f m = selfConvThree g m

The cube analogue of selfConvTwo_congr_le.

theorem PowerSeries.selfConvTwo_truncate {R : Type u_1} [Semiring R] (f : ℕ → R) (hf : f 0 = 0) (n : ℕ) : selfConvTwo (fun (m : ℕ) => if m < n then f m else 0) n = selfConvTwo f n

Truncating f above n does not change selfConvTwo f n, when f 0 = 0.

theorem PowerSeries.selfConvTwo_truncate_of_lt {R : Type u_1} [Semiring R] (f : ℕ → R) {k n : ℕ} (h : k < n) : selfConvTwo (fun (m : ℕ) => if m < n then f m else 0) k = selfConvTwo f k

Below the truncation index no hypothesis on f is needed.

theorem PowerSeries.selfConvThree_truncate {R : Type u_1} [Semiring R] (f : ℕ → R) (hf : f 0 = 0) (n : ℕ) : selfConvThree (fun (m : ℕ) => if m < n then f m else 0) n = selfConvThree f n

Truncating f above n does not change selfConvThree f n, when f 0 = 0.

theorem PowerSeries.selfConvThree_truncate_of_lt {R : Type u_1} [Semiring R] (f : ℕ → R) {k n : ℕ} (h : k < n) : selfConvThree (fun (m : ℕ) => if m < n then f m else 0) k = selfConvThree f k

The cube analogue of selfConvTwo_truncate_of_lt.

theorem PowerSeries.selfConvTwo_eq_zero {R : Type u_1} [Semiring R] {f : ℕ → R} {d : ℕ} (hf : ∀ k < d, f k = 0) {n : ℕ} (hn : n < 2 * d) : selfConvTwo f n = 0

A series vanishing below degree d has square vanishing below degree 2 * d: in every term of the convolution one of the two factors sits at an index below d.

theorem PowerSeries.selfConvThree_eq_zero {R : Type u_1} [Semiring R] {f : ℕ → R} {d : ℕ} (hf : ∀ k < d, f k = 0) {n : ℕ} (hn : n < 3 * d) : selfConvThree f n = 0

A series vanishing below degree d has cube vanishing below degree 3 * d.