DyadicRemainder.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Paired coefficients in a dyadic cyclotomic remainder

Reducing a polynomial of length 2 * m modulo X ^ m + 1 subtracts the upper block of coefficients from the lower block. The construction and the coefficient formulas work over every commutative ring.

def OAI.CirculantHadamard.DyadicRemainder.coefficientPolynomial line 25
Source documentation
The polynomial with the first n entries of a coefficient function.
```
def coefficientPolynomial (n : ℕ) (c : ℕ → R) : R[X] :=
…
```
def OAI.CirculantHadamard.DyadicRemainder.remainder line 29
Source documentation
The difference between coefficient blocks at distance m.
```
def remainder (m : ℕ) (c : ℕ → R) : R[X] :=
…
```
theorem OAI.CirculantHadamard.DyadicRemainder.coefficientPolynomial_coeff line 33
theorem OAI.CirculantHadamard.DyadicRemainder.degree_coefficientPolynomial_lt line 38
theorem OAI.CirculantHadamard.DyadicRemainder.natDegree_coefficientPolynomial_lt line 44
theorem OAI.CirculantHadamard.DyadicRemainder.remainder_coeff line 51
theorem OAI.CirculantHadamard.DyadicRemainder.remainder_coeff_eq_zero line 55
theorem OAI.CirculantHadamard.DyadicRemainder.degree_remainder_lt line 59
theorem OAI.CirculantHadamard.DyadicRemainder.natDegree_remainder_lt line 63
theorem OAI.CirculantHadamard.DyadicRemainder.remainder_eq_sub line 67
theorem OAI.CirculantHadamard.DyadicRemainder.coefficientPolynomial_two_mul line 73
Source documentation
Split the coefficient polynomial into its lower and upper blocks.
```
theorem coefficientPolynomial_two_mul (m : ℕ) (c : ℕ → R) :
    coefficientPolynomial (2 * m) c = coefficientPolynomial m c +
      X ^ m * coefficientPolynomial m (fun i => c (i + m)) := by
…
```
Mentions: OAI.CirculantHadamard.DyadicRemainder.coefficientPolynomial
theorem OAI.CirculantHadamard.DyadicRemainder.remainder_add_mul line 91
Source documentation
The explicit quotient/remainder equation before applying monic division.
```
theorem remainder_add_mul (m : ℕ) (c : ℕ → R) :
    remainder m c + (X ^ m + 1) *
      coefficientPolynomial m (fun i => c (i + m)) = coefficientPolynomial (2 * m) c := by
…
```
Mentions: OAI.CirculantHadamard.DyadicRemainder.remainder, OAI.CirculantHadamard.DyadicRemainder.coefficientPolynomial
theorem OAI.CirculantHadamard.DyadicRemainder.coefficientPolynomial_modByMonic line 101
Source documentation
The canonical monic remainder is exactly the paired coefficient difference.
```
theorem coefficientPolynomial_modByMonic {m : ℕ} (hm : 0 < m) (c : ℕ → R) :
    coefficientPolynomial (2 * m) c %ₘ (X ^ m + 1) = remainder m c := by
…
```
Mentions: OAI.CirculantHadamard.DyadicRemainder.coefficientPolynomial, OAI.CirculantHadamard.DyadicRemainder.remainder
theorem OAI.CirculantHadamard.DyadicRemainder.coefficientPolynomial_modByMonic_coeff line 115
Source documentation
Coefficients below the half-length in the canonical monic remainder.
```
theorem coefficientPolynomial_modByMonic_coeff {m : ℕ} (hm : 0 < m)
    (c : ℕ → R) (j : ℕ) (hj : j < m) :
    (coefficientPolynomial (2 * m) c %ₘ (X ^ m + 1)).coeff j = c j - c (j + m) := by
…
```
Mentions: OAI.CirculantHadamard.DyadicRemainder.coefficientPolynomial
theorem OAI.CirculantHadamard.DyadicRemainder.cyclotomic_two_pow_succ line 121
Source documentation
The dyadic cyclotomic polynomial has the expected two terms.
```
theorem cyclotomic_two_pow_succ (R : Type uR) [CommRing R] (k : ℕ) :
    cyclotomic (2 ^ (k + 1)) R = (X : R[X]) ^ (2 ^ k) + 1 := by
…
```
theorem OAI.CirculantHadamard.DyadicRemainder.coefficientPolynomial_modByMonic_cyclotomic line 126
Source documentation
The remainder statement specialized to the dyadic cyclotomic polynomial.
```
theorem coefficientPolynomial_modByMonic_cyclotomic (k : ℕ) (c : ℕ → R) :
    coefficientPolynomial (2 ^ (k + 1)) c %ₘ cyclotomic (2 ^ (k + 1)) R =
      remainder (2 ^ k) c := by
…
```
Mentions: OAI.CirculantHadamard.DyadicRemainder.coefficientPolynomial, OAI.CirculantHadamard.DyadicRemainder.remainder