## Stream: new members

### Topic: generating function of a_n = 1

#### Julian Berman (Dec 01 2020 at 02:58):

Hi. Any advice for things I'm doing inefficiently or should know about in this proof:

import data.nat.basic
import ring_theory.power_series

open power_series

def ones : power_series ℚ := power_series.mk (λ n, 1)

lemma ones_coeff_one {n : ℕ} : coeff ℚ n ones = 1 := rfl
lemma mul_ones_X_coeff_one {n : ℕ} (h_nonzero : n ≠ 0) : coeff ℚ n (X * ones) = 1 := begin
rw mul_comm,
cases n,
{ tauto },
{ finish },
end

lemma ones_inv : 1 - X = ones⁻¹ := begin
suffices h : (1 - X) * ones = 1,
{ have hc : constant_coeff ℚ ones ≠ 0 := dec_trivial,
rwa power_series.eq_inv_iff_mul_eq_one hc },
{ ext1,
rw sub_mul,
rw coeff_one,
by_cases n = 0,
{ finish },
{ simp only [h, one_mul, add_monoid_hom.map_sub, if_false],
suffices h' : coeff ℚ n (X * ones) = 1,
{ simp only [h', ones_coeff_one, sub_self] },
{ exact mul_ones_X_coeff_one h }}}
end


#### Kenny Lau (Dec 01 2020 at 05:44):

import data.nat.basic
import ring_theory.power_series

open power_series

def ones : power_series ℚ := power_series.mk (λ n, 1)

@[simp] lemma coeff_ones {n : ℕ} : coeff ℚ n ones = 1 := rfl

lemma ones_inv : 1 - X = ones⁻¹ := begin
refine (eq_inv_iff_mul_eq_one _).2 _, { exact one_ne_zero },
ext1 n,
cases n,
{ rw [coeff_zero_eq_constant_coeff_apply, coeff_zero_eq_constant_coeff_apply,
ring_hom.map_mul, constant_coeff_X, zero_mul, sub_zero, if_pos rfl], refl },
{ rw [mul_comm, coeff_succ_mul_X, if_neg (n.succ_ne_zero)], exact sub_self _ }
end


Thanks!

#### Julian Berman (Dec 04 2020 at 00:49):

With the above I was trying to formalize a proof of a second recurrence with generating functions. I'm only partway through, but have 2 minor questions. Code is:

import tactic

import generating_functions

open power_series

def a : ℕ → ℚ
| 0 := 0
| (n + 1) := 2 * a n + 1

def A := mk a

lemma A_def : A = mk a := rfl

-- FIXME
lemma two_lift {φ : power_series ℚ} : 2 * φ = (C ℚ) 2 * φ := by norm_num
lemma A_mul_two : power_series.mk (λ n, 2 * a n) = 2 * A := begin
simp only [A, two_lift],
rw C_mul,
end

-- FIXME: have h : ...
#check a.equations._eqn_2

lemma A_recurrence : shift A = 2 * A + ones := begin
rw ← A_mul_two,
ext1,
simp only [shift_def, A_def, a, coeff_mk, coeff_add, coeff_ones],
end

theorem A_ogf : A = X / ((1 - X) * (1 - 2 * X)) := begin
sorry,
end


where generating_functions contains:

import ring_theory.power_series

import tactic.basic

noncomputable theory
open power_series

variables {k : Type*} [field k]

def div (φ₁ φ₂ : power_series k) := φ₁ * φ₂⁻¹

instance : has_div (power_series k) := ⟨div⟩

lemma div_def (φ₁ φ₂ : power_series k) : φ₁ / φ₂ = φ₁ * φ₂⁻¹ := rfl

@[simp] lemma one_div_eq_inv (φ₁ φ₂ : power_series k) : φ₁ = (1 / φ₂) ↔ φ₁ = φ₂⁻¹ :=
by rw [div_def, one_mul]

def ones := power_series.mk $λ n, (1 : ℚ) lemma ones_def : ones = power_series.mk (λ n, (1 : ℚ)) := rfl @[simp] lemma coeff_ones (n : ℕ) : (coeff ℚ n) ones = 1 := rfl lemma ones_ogf : ones = 1 / (1 - X) := begin simp only [one_div_eq_inv], refine (eq_inv_iff_mul_eq_one _).2 _, { simp only [ring_hom.map_sub, constant_coeff_one, constant_coeff_X, sub_zero, ne.def, not_false_iff, one_ne_zero] }, ext1 n, rw [mul_sub, add_monoid_hom.map_sub, mul_one, coeff_one], cases n, { rw [coeff_zero_eq_constant_coeff_apply, coeff_zero_eq_constant_coeff_apply, ring_hom.map_mul, constant_coeff_X, mul_zero, sub_zero, if_pos rfl], refl }, { rw [coeff_succ_mul_X, if_neg (n.succ_ne_zero)], exact sub_self _ } end /-! The shift operation on a power series takes a₀ + a₁x + ... to a₁ + a₂x + ... -/ def shift (φ : power_series k) : power_series k := power_series.mk$ λ n, (coeff k (n + 1) φ)

lemma shift_def (φ : power_series k) :
shift φ = (power_series.mk \$ λ n, (coeff k (n + 1) φ)) := rfl

/-!
Multiplying a shifted power series by x, then adding its original
constant coefficient equals the original series.
-/
lemma shift_mul_add_constant_is_inv (φ : power_series k) :
(shift φ) * X + (C k (constant_coeff k φ)) = φ := begin
dsimp [shift_def],
ext1,
cases n,
{ simp only [ring_hom.map_add, constant_coeff_C, constant_coeff_X, coeff_zero_eq_constant_coeff,

add_eq_zero_iff, if_false, one_ne_zero, and_false, coeff_succ_mul_X] },
end

@[simp] lemma coeff_add (n : ℕ) (φ₁ φ₂ : power_series k) :
coeff k n (φ₁ + φ₂) = coeff k n φ₁ + coeff k n φ₂ := by simp only [add_monoid_hom.map_add]

lemma C_mul {a : k} {f : ℕ → k} : C k a * mk f = mk (λ n, a * f n) :=
by { ext1, simp only [mul_comm, coeff_mul_C, coeff_mk] }


1) When I write #check 2 * (power_series.mk id), the 2 is coerced into a power_series.C -- how can I write C_mul such that I don't need to manually rw two_liftand A_mul_two?
2) Is a.equations._eqn_2 the way I can refer to the recurrence from a's definition? If I wanted to explicitly add that equation as a hypothesis in a local context how do I do that? have h: a.equations._eqn_2 seems to complain that that isn't a type. The point of doing so was to calculate from that recurrence in my proof of A_recurrence, which seems to just work if I put simp [..., a, ...] there instead of a.equations._eqn_2, but just curious on how to do so anyhow

Also, is e.g. coeff_add useful to add?

#### Kevin Buzzard (Dec 04 2020 at 00:59):

 a.equations._eqn_2 isn't a type (a theorem statement), it's a term (a proof). If you want to add it to the local context then the syntax is have h := a.equations._eqn_2 but simp [..., a, ...] is what you're supposed to be doing. simp [a] means "simp using the equation lemmas of the definition a". You can see them with #print prefix a.

#### Kevin Buzzard (Dec 04 2020 at 01:00):

coeff_add looks fine to me. Note that you can prove it with ... := add_monoid_hom.map_add _ _ _ in term mode.

#### Kevin Buzzard (Dec 04 2020 at 01:02):

Oh wait, coeff is already an additive group hom, so coeff_add is already there. It's called (coeff k n).map_add.

#### Julian Berman (Dec 04 2020 at 01:06):

How does one decided whether that should be marked @[simp] or not for this case?

#### Julian Berman (Dec 04 2020 at 01:07):

(And thanks as usual, very helpful on the first thing -- I guess informally I was expecting to have a proof where I start with the equation from a and then manipulate it with the operations I did, but yeah that's not how the proof appears to turn out)

#### Kevin Buzzard (Dec 04 2020 at 01:08):

The 2 thing is a numeral issue. Any type which has a zero and a one and an add will have a 2, defined to be 1 + 1. In particular you won't see the same behaviour if you use (c : \Q). I'm not quite sure what the question is. Do you want to prove theorems about numerals like 2 specifically?

#### Kevin Buzzard (Dec 04 2020 at 01:09):

(coeff k n).map_add is already marked simp, because #print add_monoid_hom.map_add tells me it is. You can use #print to see all the tags attached to a term.

#### Julian Berman (Dec 04 2020 at 01:10):

Oy, you're correct, though I could swear I added coeff_add after simp didn't finish solving something :(, must be my mistake.

#### Kevin Buzzard (Dec 04 2020 at 01:11):

lemma A_mul_two : power_series.mk (λ n, 2 * a n) = C _ 2 * A := C_mul.symm

#### Julian Berman (Dec 04 2020 at 01:12):

On the number question -- I wanted to write k * A for multiplying a power series by an element of the field, and then be able to push k through C_mul without needing to manually prove a lemma for every different k (or without having to write (C \Q k) instead of k)

#### Julian Berman (Dec 04 2020 at 01:12):

because if I have an equation with lots of multiplications I'll have to rewrite them all

#### Kevin Buzzard (Dec 04 2020 at 01:12):

You could add a coercion from F to power series F if you like.

#### Julian Berman (Dec 04 2020 at 01:12):

(Hopefully that makes more sense?)

#### Julian Berman (Dec 04 2020 at 01:13):

OK will try that, thanks.

#### Kevin Buzzard (Dec 04 2020 at 01:14):

I mean, that's exactly what you're asking for, right? You want to have (x : F) being interpreted as (x : power_series F) and this is exactly a coercion.

#### Julian Berman (Dec 04 2020 at 01:15):

Yes, I think so, I guess I thought that was already existing for 2 * A to work

#### Kevin Buzzard (Dec 04 2020 at 01:15):

No because numerals are different -- they follow the rules I explained above.

#### Julian Berman (Dec 04 2020 at 01:15):

but it sounds like that's just because it's doing 2 = 1 + 1.. yeah

#### Kevin Buzzard (Dec 04 2020 at 01:16):

More precisely it's doing 2 = bit0 1, but bit0 x := x + x.

#### Kevin Buzzard (Dec 04 2020 at 01:17):

set_option pp.numerals false

#check (37 : ℚ) -- bit1 (bit0 (bit1 (bit0 (bit0 has_one.one)))) : ℚ


#### Julian Berman (Dec 04 2020 at 01:18):

interesting thanks, I saw bit0 show up somewhere in a ring homomorphism proof and wondered what it was -- why is it called bit0, I thought that'd refer to the 0th bit of x

#### Kevin Buzzard (Dec 04 2020 at 01:19):

it means "add a 0 to the end of x" :-)

ah.

#### Julian Berman (Dec 05 2020 at 14:25):

I haven't been able to get the coersion working, so hopefully it's OK to ask for another tip. Specifically... (Sorry, accidentally hit enter too soon)

#### Bhavik Mehta (Dec 05 2020 at 21:55):

By the way you might like to look at https://github.com/leanprover-community/mathlib/pull/4259 in which Aaron and I used generating functions to show Euler's partition theorem

#### Julian Berman (Dec 05 2020 at 22:02):

@Bhavik Mehta oh awesome! I will, thanks for the pointer. I'm obviously playing with quite simple things (and getting stuck in quite simple places while doing so both because my math is crusty and my lean is worse) but having fun while doing so... I'm sure will pick up some tips from that.

#### Julian Berman (Dec 05 2020 at 22:04):

I think if I understand what I'm doing a little bit, that things would be easier if there was laurent series implemented

#### Julian Berman (Jan 12 2021 at 20:49):

@Bhavik Mehta I assume you're OK with me pushing a commit to bring that Euler Partition PR up to date with mathlib right? (There's like 2 or 3 small changes it looks like to get it re-passing)