generating function of a_n = 1

Stream: new members

[Julian Berman]

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]

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]

Thanks!

[Julian Berman]

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?

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Julian Berman]

(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]

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]

(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]

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]

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

[Julian Berman]

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]

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

[Kevin Buzzard]

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

[Julian Berman]

(Hopefully that makes more sense?)

[Julian Berman]

OK will try that, thanks.

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Julian Berman]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

set_option pp.numerals false

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

[Julian Berman]

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]

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

[Julian Berman]

ah.

[Julian Berman]

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]

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]

@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]

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]

@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]

Go ahead!