# Zulip Chat Archive

## 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,
rw [sub_mul, add_monoid_hom.map_sub, one_mul, coeff_one],
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
```

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

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 `shift`ed 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,
ring_hom.coe_add_monoid_hom, zero_add, mul_zero, ring_hom.map_mul] },
{ simp only [nat.succ_eq_add_one, coeff_C, add_zero, coeff_mk, add_monoid_hom.map_add,
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_lift`

and `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" :-)

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

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)

#### Bhavik Mehta (Jan 12 2021 at 20:50):

Go ahead!

Last updated: May 14 2021 at 07:19 UTC