Formal power series

Stream: LftCM22

[Thomas Browning]

Here's a thread for the formal power series project (I'll dump some code here when it's a bit more polished)

[Tyler Raven Billingsley]

Hi power series people! I have the first part (sine identity) down to proving the following:

 ∀ k : ℕ, (coeff ℂ (2 * k + 1)) (sin ℂ) = (-1) ^ k * (coeff ℂ (2 * k + 1)) (exp ℂ)

I'm not sure how to manipulate the relevant power series coefficients.

[Sam van G]

@Anatole Dedecker @Phil Wood and I worked on this a little bit and we eventually got somewhere, but the code is on Phil's computer.

[Anatole Dedecker]

Oh yeah we should definitely meet tomorrow to talk about it. Are you working on a common repo/branch, or completely separately ? As Sam said we solved a problem like that on Phil's code, and it was a bit painful because it's all "obvious stuff" and because the coefficients of the sine power series are defined in a strange way, exploiting the fact than natural number division floors the result, but we should be able to replicate it pretty easily now that we've identified the key lemmas for manipulating this

[Anatole Dedecker]

I hope we'll be able to get through the frustrating part of dealing with coercions and docs#algebra_map without too much damage, and if we manage that then it's kind of a good thing because knowing how to work around these kind of things is somewhat of a skill on its own imho

[Thomas Browning]

Here's my code from yesterday, including the lemma that @Tyler Raven Billingsley needs. I think I managed to avoid the worst of the algebra map pain.

import ring_theory.power_series.well_known
import data.complex.basic

namespace power_series

open complex

variables {A : Type*} [ring A] [algebra ℚ A]

lemma coeff_sin_bit0 (n : ℕ) : coeff A (bit0 n) (sin A) = 0 :=
by rw [sin, coeff_mk, if_pos (even_bit0 n)]

lemma nat.bit1_div_bit0 (a b : ℕ) : bit1 a / bit0 b = a / b :=
begin
  have := nat.div_two_mul_two_add_one_of_odd (odd_bit1 a),
  rw [mul_two, ←bit0, ←bit1, nat.bit1_eq_bit1] at this,
  rw [bit0_eq_two_mul, ←nat.div_div_eq_div_mul, this],
end

lemma coeff_sin_bit1 (n : ℕ) : coeff A (bit1 n) (sin A) = (-1) ^ n * coeff A (bit1 n) (exp A) :=
by rw [sin, coeff_mk, if_neg (nat.not_even_bit1 n), nat.bit1_div_bit0, nat.div_one,
  ←mul_one_div, map_mul, map_pow, map_neg, map_one, coeff_exp]

example : sin ℂ = (2 * I)⁻¹ • (rescale I (exp ℂ) - rescale (-I) (exp ℂ)) :=
begin
  ext1 n,
  rw [map_smul, map_sub, coeff_rescale, coeff_rescale, neg_pow I, mul_assoc, ←one_sub_mul],
  rcases n.even_or_odd with (⟨k, rfl⟩ | ⟨k, rfl⟩),
  { rw [←bit0, I_pow_bit0, neg_pow_bit0, one_pow, sub_self, zero_mul, smul_zero, coeff_sin_bit0] },
  { rw [two_mul, ←bit0, ←bit1, neg_pow_bit1, one_pow, sub_neg_eq_add, ←bit0],
    rw [I_pow_bit1, mul_comm ((-1) ^ k) I, mul_assoc, ←mul_assoc, smul_eq_mul,
        inv_mul_cancel_left₀, coeff_sin_bit1],
    exact mul_ne_zero two_ne_zero' I_ne_zero },
end

end power_series

[Anatole Dedecker]

Okay so it seems like you are all working separately, right ? Would you be interested in setting up a lean project to put that in common (or at least set up a branch in mathlib) ? That would be a really good occasion to get some experience with GitHub if you aren't already sed to it (and I should say that, even when working alone on a project, you are still encouraged to set up a lean project / branch of mathlib to be able to share your code later)

[Sam van G]

could we get non-master-branch write permissions (samvang, tyler-billingsley) please ? :smile:

[Thomas Browning]

philmwood as well

[Oliver Nash]

I've just sent an invite to samvang I'll do the others now.

[Oliver Nash]

OK I've sent invites to Tyler and Phil now also. (This is actually the first time I've sent invites --- I believe I've clicked the right buttons but LMK if any issues.)

[Oliver Nash]

(I did mess up the invites but I believe I have done it correctly now --- you may get some confusing emails from GitHub but hopefully all should work.)

[Jake Levinson]

@Oliver Nash Can I get non-master-branch write permissions as well? My github username is jakelev.

[Oliver Nash]

Done

[Sam van G]

It worked for me, thanks @Oliver Nash

[Tyler Raven Billingsley]

@Phil Wood Just realized that your alternate Catalan number recursion formula might be good for the Catalan file in mathlib!

[Phil Wood]

That is a good thought! I need to think a bit on the proof though, since it is a huge mess of rw and nth_rewrite commands at the moment. But if I can get that cleaned up, I may well give PR-ing a try!