Extending a function by zero

Stream: Is there code for X?

[Xavier Xarles]

I would like to define a function ℕ → ℝ from a given list L of real numbers, by assigning to every n less than the length on L its element L[n], and otherwise 0. This is what I did, with two elementary lemmas on the definition.

import Mathlib.Data.Real.Basic
import Mathlib.Data.List.Basic

open Real List

def ext0 (L : List ℝ) : ℕ → ℝ := by
  intro n
  by_cases (n < L.length)
  · exact L[n]
  · exact 0

lemma ext00 (L : List ℝ) (h: 0< L.length):
    ext0 L 0 = L[0]'h := by
  unfold ext0
  rw [@dite_eq_iff]
  constructor
  use h

lemma ext0l (L : List ℝ) (h: 0< L.length):
    ext0 L (L.length-1) = L[L.length-1] := by
  unfold ext0
  rw [@dite_eq_iff]
  constructor
  simp
  rw [propext (Nat.lt_iff_le_pred h)]

I am not sure about defining if using by_cases. Is there a better way?

[Damiano Testa]

I think that your definition is actually equivalent to what is below (and I golfed a little bit your lemmas):

def ext0 (L : List ℝ) (n : ℕ) : ℝ :=
  if h : n < L.length then L[n] else 0

lemma ext00 (L : List ℝ) (h: 0< L.length):
    ext0 L 0 = L[0]'h := by
  simp [ext0, dite_eq_iff, h]

lemma ext0l (L : List ℝ) (h: 0< L.length):
    ext0 L (L.length-1) = L[L.length-1] := by
  simp [ext0, dite_eq_iff, Nat.lt_iff_le_pred h]

[Adam Topaz]

why not just L[n]!? Or if you don't want a panic, L[n]?.getD default?