summing over real.logb

Stream: new members

[Callum Cassidy-Nolan]

This theorem :

open_locale big_operators

theorem why :
    ∃ (v : ℝ ), v = ∑ i in finset.Icc 2 100, (real.logb i 2) := sorry

creates the problem:

failed to synthesize type class instance for
v : ℝ
⊢ locally_finite_order ℝ

this doesn't happen if I change the sum term to be (real.logb 2 2) so I don't know what the issue is here, any hints?

[Anne Baanen]

finset.Icc 2 100 has to be finite by definiion, and there are more than finitely many real numbers in the interval [2, 100]

[Anne Baanen]

Do you instead want to sum over the integers in that range?

[Yaël Dillies]

You probably want

lemma here_is_why : ∃ v, v = ∑ i in finset.Icc (2 : ℕ) 100, (real.logb i 2) := sorry

[Callum Cassidy-Nolan]

Oh yeah I did want to sum over the integers in that range, it always had, but this time for some reason it hadn't...

[Callum Cassidy-Nolan]

Thanks for the tips!

[Kevin Buzzard]

Lean can infer that i must be a real and you didn't specify the types of 2 and 100 so it went with the path of least resistance. If you don't give it any clues at all it guesses nat but you gave it a clue with real.logb