About my theorem

Stream: new members

[Adrian Chu]

I am getting close to finishing proving my theorem

theorem mythm (n : ℕ) (r : fin n → ℕ) (s : ℕ)
    (hn : n ≥ 1) (hr : ∀ i, r i ≥ 1) (hs : s ≥ 1)
    (coprime : ∀ i : fin n, nat.gcd (r i) s = 1) :
    ∃ x : fin n → ℕ, ∃ y : ℕ,
    (∀ i, x i ≥ 1) ∧ (finset.univ.sum (λ i, (x i)^(r i)) = y^s) := sorry

Now I have some lemmas remains to be proven. They all involves the recursive function n_lcm, as defined below.

def fin_n_to_list {n : ℕ} (x: fin n → ℕ) : list ℕ :=
    (list.range n).map (λ i, if h : i < n then x ⟨i, h⟩ else 0)

def n_lcm {n : ℕ} (x : fin n → ℕ) : ℕ :=
    list.foldl nat.lcm 1 (fin_n_to_list x)

lemma n_lcm_geq_1 {n : ℕ} (x : fin n → ℕ) (hx : ∀ i, x i ≥ 1):
    n_lcm x ≥ 1 := sorry

I have read the chapter about induction TPIN a bit, but unfortunately have no idea on how to start proving the above lemma. Can anyone give some directions? Tganks

[Kevin Buzzard]

induction on n, and a proof for the n=2 case, will be the two ingredients that you need.

[Adrian Chu]

I start to see this is a big task. If we use induction, we at least need that lcm (a_1,...,a_n)=lcm(lcm(a_1,..a_(n-1)),a_n). and we dont yet have that either...

[Mario Carneiro]

You can use the multiset fold operation. It requires a proof that the operation is associative, but then you get that theorem for free

[Kevin Buzzard]

You should just need the base case and the n=2 case (for the inductive step). There will be some general theory in the library about how doing an operation to n things via folding is the same as doing it to n-1 things and then doing it once more. The proof will be short.

[Kevin Buzzard]

Well, the proof of the theorem for lists will be short. You'll then have to convert back to your fin n representation.