cast/coerce ∏ to \R

Stream: new members

[Ralf Stephan]

What am I doing wrong? Please comment.

import Mathlib

set_option autoImplicit false

open Finset Nat
open BigOperators

lemma h₂ {a b c : ℝ} (h: a = b): a * (c / b) = c := by sorry

theorem h₃ {n : ℕ} {k : ℝ}: (∏ k in Icc 1 n, (1 + k) / k) * ((n + 2) / (n + 1))
    = n + 2 := by
  apply h₂ (a := ((∏ k in Icc 1 n, (1 + k) / k) : ℝ))
        (b := ((n + 1) : ℝ))
        (c := ((n + 2) : ℝ))
  sorry

tactic 'apply' failed, failed to unify
  (∏ k in Icc 1 n, (1 + ↑k) / ↑k) * ((↑n + 2) / (↑n + 1)) = ↑n + 2
with
  (∏ k in Icc 1 n, (1 + k) / k) * ((n + 2) / (n + 1)) = n + 2
n : ℕ
k : ℝ
⊢ (∏ k in Icc 1 n, (1 + k) / k) * ((n + 2) / (n + 1)) = n + 2

Is the n under the ∏ the problem?

Thanks,

[Kevin Buzzard]

You have both a bounded and unbounded variable k in h3, and the one in the goal is a natural so lemma h2 (which is false if b=0 so can't be proved) doesn't apply because it's about real numbers.

[Kevin Buzzard]

h3 isn't true either because all those divisions are natural divisions ie they throw away the remainder

[Ralf Stephan]

I removed a lot of code to get the mwe. what to do about the k?

[Kyle Miller]

Since n and k are natural numbers in (∏ k in Icc 1 n, (1 + k) / k) * ((n + 2) / (n + 1)) make sure to put in a type ascription as a hint somewhere. This should help: (∏ k in Icc 1 n, (1 + k) / k) * ((n + 2) / (n + 1) : ℝ)

[Kevin Buzzard]

Well you could remove the k that isn't doing anything, and you could replace the first (1 + k) with (1 + k : \R)

[Ralf Stephan]

The two different ns are no problem?

[Kevin Buzzard]

There's only one n. Do you understand the concept of free and bound variables?

[Kevin Buzzard]

You're taking a product over k and that makes a new variable k. But you're not taking a product over n

[Ralf Stephan]

Need to look that up. Intuitively, free is implicit?

[Ralf Stephan]

Bummer, in the real code I have an induction over k, that no longer works because it's now real. Can I rewrite a goal by changing a variable from N to R? (after the induction)

[Kevin Buzzard]

If you want to work out whether $\sum_{i=1}^{3}(i+n)=37$ is true or false then you don't have enough information because you don't know n. If i told you that n=10 then you could do the calculation. Here n is a free variable. But you don't have to know what i is to work out the sum, because i is bound, it appears locally and runs from 1 to 3 and then disappears. You have both a free k and a bound k in h3

[Kevin Buzzard]

Yes, lean automatically coerces from naturals to reals when asked -- indeed that's what all those little up-arrows are indicating in the error message you posted earlier

[Ralf Stephan]

Many thanks!

[Kevin Buzzard]

Indeed it was the presence of the up arrows which alerted me to what was going on