Equality of two finite sums

Stream: new members

[Joan Domingo Pasarin]

Hi all. I'm new to Lean and I'm trying to finish the following proof:

import Mathlib

open Real

noncomputable def f (x : ℝ) : ℝ := ∑ k ∈ Finset.Icc 3 ⌊ (log x)/(log 2) ⌋, x^(1/k - 1/3)
noncomputable def u (n : ℕ) : ℝ := ∑ k ∈ Finset.Icc 4 n, 2^((n/k:ℝ) - (n/3:ℝ))

theorem prop_3_sub_3 (n : ℕ) (hn : n ≥ 3) : f (2^n) = 1 + u n := by
  have sum_bound : ⌊(log (2^n))/(log 2)⌋ = n := by norm_num
  rw [f, u, sum_bound]
  rw [← Finset.add_sum_Ioc_eq_sum_Icc (by linarith)]
  rw [← Finset.Ioc_eq_Icc]
  congr 1

Is there a lemma I can apply to unfold the two sums and proof equality of the summands? I've tried to apply Finset.sum_congr but it's not working. I suspect it's due to the fact that the n on the lhs is coerced but the one on the rhs isn't.

Also, sorry if this isn't the channel to ask this.

[Bbbbbbbbba]

What version of Mathlib are you using? My Mathlib cannot find Finset.Ioc_eq_Icc.

[Bbbbbbbbba]

Should I replace it with rw [← Finset.Icc_add_one_left_eq_Ioc]?

[Yongxi Lin (Aaron)]

That lemma indeed does not exist

[Yongxi Lin (Aaron)]

@Joan Domingo Pasarin
I don't know whether this is your intension, but you are using the floor function for ℤ (Int.floor) instead of the one for ℕ (Nat.floor) in your definition of f, so a (probably not very satisfying) solution is to change your definition of f:

noncomputable def f (x : ℝ) : ℝ := ∑ k ∈ Finset.Icc 3 ⌊(log x)/(log 2)⌋₊, x^(1/k - 1/3)

If you want to keep your original definition, then you are right that things are not working because of the coercions. One side is summing over a subset of integers and the other is summing over a subset of natural numbers, so in order to turn one side into the other, you need a lemma like Finset.sum_preimage_of_bij or Finset.sum_preimage.

[Joan Domingo Pasarin]

That's weird, it works for me. How can I check the mathlib version?

What version of Mathlib are you using? My Mathlib cannot find Finset.Ioc_eq_Icc.

[Bbbbbbbbba]

If you are in a project, what does lakefile.toml say?

[Joan Domingo Pasarin]

It doesn't fix any version. It says

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"

The lake-manifest.json says I'm using revision 3de2350.

[Bbbbbbbbba]

Hmm that seems fairly new

[Bbbbbbbbba]

Maybe you had it somewhere else in your project? Have you checked your #mwe locally as such?

[Joan Domingo Pasarin]

Ah, yes that is it. It's a lemma in the project:

lemma Finset.Ioc_eq_Icc (M N : ℕ) : Finset.Ioc N M = Finset.Icc (N + 1) M := by
  ext a; simp only [Finset.mem_Ioc, Finset.mem_Icc]; constructor <;> intro ⟨h₁, h₂⟩ <;> omega

[Bbbbbbbbba]

Joan Domingo Pasarin said:

Hi all. I'm new to Lean and I'm trying to finish the following proof:

import Mathlib

open Real

noncomputable def f (x : ℝ) : ℝ := ∑ k ∈ Finset.Icc 3 ⌊ (log x)/(log 2) ⌋, x^(1/k - 1/3)
noncomputable def u (n : ℕ) : ℝ := ∑ k ∈ Finset.Icc 4 n, 2^((n/k:ℝ) - (n/3:ℝ))

theorem prop_3_sub_3 (n : ℕ) (hn : n ≥ 3) : f (2^n) = 1 + u n := by
  have sum_bound : ⌊(log (2^n))/(log 2)⌋ = n := by norm_num
  rw [f, u, sum_bound]
  rw [← Finset.add_sum_Ioc_eq_sum_Icc (by linarith)]
  rw [← Finset.Ioc_eq_Icc]
  congr 1

Is there a lemma I can apply to unfold the two sums and proof equality of the summands? I've tried to apply Finset.sum_congr but it's not working. I suspect it's due to the fact that the n on the lhs is coerced but the one on the rhs isn't.

Also, sorry if this isn't the channel to ask this.

In the definition of f, 1/3 is parsed as (1 : ℤ) / (3 : ℤ) = 0. Is this intended?

[Joan Domingo Pasarin]

Probably not. It should be real divison.

[Bbbbbbbbba]

import Mathlib

open Real

noncomputable def f (x : ℝ) : ℝ := ∑ k ∈ Finset.Icc 3 ⌊ (log x)/(log 2) ⌋, x^((1/k:ℝ) - (1/3:ℝ))
noncomputable def u (n : ℕ) : ℝ := ∑ k ∈ Finset.Icc 4 n, 2^((n/k:ℝ) - (n/3:ℝ))

lemma Finset.Ioc_eq_Icc (M N : ℕ) : Finset.Ioc N M = Finset.Icc (N + 1) M := by
  ext a; simp only [Finset.mem_Ioc, Finset.mem_Icc]; constructor <;> intro ⟨h₁, h₂⟩ <;> omega

theorem prop_3_sub_3 (n : ℕ) (hn : n ≥ 3) : f (2^n) = 1 + u n := by
  have sum_bound : ⌊(log (2^n))/(log 2)⌋ = n := by norm_num
  rw [f, u, sum_bound]
  rw [← Finset.add_sum_Ioc_eq_sum_Icc (by linarith)]
  rw [← Finset.Ioc_eq_Icc]
  congr 1
  · rify; simp
  calc
   _ = ∑ k ∈ Finset.Ioc 3 n, ((2 : ℝ) ^ n) ^ ((1/k:ℝ) - (1/3:ℝ)) := by
     convert Finset.sum_image ?_
     · change Finset.Ioc 3 (n : ℤ) = Finset.image Nat.cast (Finset.Ioc 3 n)
       ext k; simp only [Finset.mem_Ioc, Finset.mem_image]; constructor
       · intro ⟨hk1, hk2⟩; use k.toNat; omega
       · omega
     · simp
   _ = _ := by
     apply Finset.sum_congr rfl
     intro k hk
     rw [← rpow_natCast 2 n, ← rpow_mul zero_le_two]
     ring_nf

[Bbbbbbbbba]

Amusingly, if I change the last ring_nf to ring, it prints that "The ring tactic failed to close the goal. Use ring_nf to obtain a normal form."... Except that it did close the goal :rolling_on_the_floor_laughing:

[Joan Domingo Pasarin]

Wow, thank you! I definitely couldn't have come up with the last part on my own. I'll see if the maintainers of the project want to keep the definition of f as it is right now or change the floor function in it.

[Ruben Van de Velde]

That happens when the LHS and RHS of the expression aren't in scope for the ring tactic, but they're equal once you normalised some subexpressions that are in scope