## Stream: new members

### Topic: Working with finset.prod

#### Dan Stanescu (Jul 29 2020 at 18:46):

Assuming I got this set up correctly, is there any reasonably simple way to get the goal in the example?

import data.polynomial
import data.real.basic

noncomputable theory
open_locale big_operators

def binom_l (a : ℝ) : polynomial ℝ := polynomial.X - polynomial.C a

def lagrange_interpolant_v2 (n : ℕ) (i : ℕ) (xData : ℕ → ℝ): polynomial ℝ :=
∏ j in ( finset.range (n+1) \ {i} ),
((1 : ℝ)/(xData i - xData j)) • (binom_l (xData j))

def myX : ℕ → ℝ
| 0 := (1 : ℝ)
| 1 := (2 : ℝ)
| (n+1) := 0

-- The first interpolant (i=0) evaluated at the first point (x 0 = 1.0):
example : polynomial.eval (1 : ℝ) (lagrange_interpolant_v2 1 0 myX) = (1 : ℝ) :=
begin
unfold lagrange_interpolant_v2,
unfold finset.prod,
simp * at *,
--rw polynomial.eval_smul (binom_l _) (1:ℝ),
sorry,
end


#### Kevin Buzzard (Jul 29 2020 at 18:52):

What's the goal? I don't have access to lean right now

#### Kevin Buzzard (Jul 29 2020 at 18:53):

Your definition of myX should have n+2 not n+1 maybe?

#### Kevin Buzzard (Jul 29 2020 at 18:55):

I would be tempted to prove that finset.range 2 \{0} was {1}

#### Dan Stanescu (Jul 29 2020 at 19:01):

Kevin Buzzard said:

Your definition of myX should have n+2 not n+1 maybe?

Only the first two values count, so it shouldn't matter.

#### Dan Stanescu (Jul 29 2020 at 19:06):

Kevin Buzzard said:

I would be tempted to prove that finset.range 2 \{0} was {1}

If this is the only alternative, I probably can go that way in this simple example. But then this won't work very nicely for larger n.

I'm just trying to figure out best ways to manipulate these objects. Ultimately my goal is not to compute the values of these interpolants, but rather to prove/obtain truncation error for interpolation.

#### Kevin Buzzard (Jul 29 2020 at 19:14):

Computing one example is a very different question to proving theorems

#### Kevin Buzzard (Jul 29 2020 at 19:17):

You're right that things shouldn't matter as far as what the function does is concerned, but if you make an obscure implementation then it will be harder to prove theorems. Directly after a definition you should usually make a little API, and the API for myX should be the theorems that myX 0= 1, myX 1=2 and myX n+2=0, which will probably be harder to prove with your definition

#### Dan Stanescu (Jul 29 2020 at 19:20):

I see your point. This myX function is not supposed to appear in any further stuff, though.

But yes, changing to:

def myX : ℕ → ℝ
| 0 := (1 : ℝ)
| 1 := (2 : ℝ)
| (n+2) := 0

@[simp] lemma myX_0 : myX 0 = (1:ℝ) := rfl
@[simp] lemma myX_1 : myX 1 = (2:ℝ) := rfl


simplifies the goal a little bit.

#### Shing Tak Lam (Jul 29 2020 at 22:44):

Is the point of ( finset.range (n+1) \ {i} ) to get the set $\{1, \dots, n\}$? If so, I think just using ( finset.range (n) ) and replacing every occurrence of j with j + 1 will give you nicer goals (and more simp lemmas to be able to use). Plus if you ever want to do induction over n, this definition will be a lot easier to deal with than the set difference definition.

So what I'm suggesting is to use this definition instead

def lagrange_interpolant_v2' (n : ℕ) (i : ℕ) (xData : ℕ → ℝ): polynomial ℝ :=
∏ j in ( finset.range (n) ),
((1 : ℝ)/(xData i - xData (j + 1))) • (binom_l (xData (j + 1)))


the proof follows very nicely with this definition and the simp lemmas about myX.

example : polynomial.eval (1 : ℝ) (lagrange_interpolant_v2' 1 0 myX) = (1 : ℝ) :=
begin
unfold lagrange_interpolant_v2' binom_l,
norm_num,
end


#### Dan Stanescu (Jul 30 2020 at 00:19):

Kevin Buzzard said:

I would be tempted to prove that finset.range 2 \{0} was {1}

It follows easily indeed if I use this:

@[simp] lemma finset_range_2_0 : finset.range 2 \ {0} = {1} :=
begin
have h1 : 2 = nat.succ 1, refl,
rw [ h1, finset.range_succ, finset.range_one ],
refl,
end


after which the proof is basically just rewrites. Unfortunately this becomes very inconvenient for large n. Or at least that's what I think.

#### Yakov Pechersky (Jul 30 2020 at 00:27):

You could try to write a couple of lemmas about finset.range (bit0 n) and finset.range (bit1 n).

#### Kevin Buzzard (Jul 30 2020 at 07:32):

Lean is a theorem prover, not an example computer. Working with examples is always a bit harder, especially straight after a new definition, because the lemmas you need are not there. If you want to work with larger examples you might want to write some more general API for your definition first.

#### Johan Commelin (Jul 30 2020 at 07:36):

@Dan Stanescu I've never really used it, but I hope thatfin_cases would be a helpful tactic.
Also:

lemma finset_range_2_0 : finset.range 2 \ {0} = {1} := dec_trivial


#### Johan Commelin (Jul 30 2020 at 07:37):

(In special cases, Lean is an example computer.)

Last updated: Dec 20 2023 at 11:08 UTC