Zulip Chat Archive

Stream: new members

Topic: generating function of a_n = 1


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Julian Berman (Dec 01 2020 at 12:56):

Thanks!

view this post on Zulip 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_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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Julian Berman (Dec 04 2020 at 01:06):

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

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 04 2020 at 01:12):

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

view this post on Zulip Julian Berman (Dec 04 2020 at 01:12):

(Hopefully that makes more sense?)

view this post on Zulip Julian Berman (Dec 04 2020 at 01:13):

OK will try that, thanks.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 04 2020 at 01:15):

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

view this post on Zulip Julian Berman (Dec 04 2020 at 01:15):

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

view this post on Zulip Kevin Buzzard (Dec 04 2020 at 01:16):

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

view this post on Zulip Kevin Buzzard (Dec 04 2020 at 01:17):

set_option pp.numerals false

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 04 2020 at 01:19):

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

view this post on Zulip Julian Berman (Dec 04 2020 at 01:19):

ah.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Bhavik Mehta (Jan 12 2021 at 20:50):

Go ahead!


Last updated: May 14 2021 at 07:19 UTC