Working with finset.prod

Stream: new members

[Dan Stanescu]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Dan Stanescu]

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]

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]

Computing one example is a very different question to proving theorems

[Kevin Buzzard]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

@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]

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