interpolate_eq_sum_interpolate_insert_sdiff

English

For t ⊇ s with s nonempty, the interpolant on t decomposes as a linear combination of interpolants on supersets of s obtained by inserting elements of s into t\\s, weighted by the Lagrange basis polynomials for s.

Русский

Если t — конечное множество, содержащее s, причём s непусто и s ⊆ t, то интерполянт на t разлагается в сумму по i ∈ s: интерполянт на t с добавлением i в t\\s, умноженный на соответствующий базис Лагранжа для i относительно s.

LaTeX

$$$ \\operatorname{interpolate}(t,v)r = \\sum_{i\\in s} \\operatorname{interpolate}(\\operatorname{insert}(i,t\\setminus s),v)\\,r \\cdot \\operatorname{basis}(s,v,i) $$$

Lean4

theorem interpolate_eq_sum_interpolate_insert_sdiff (hvt : Set.InjOn v t) (hs : s.Nonempty) (hst : s ⊆ t) :
    interpolate t v r = ∑ i ∈ s, interpolate (insert i (t \ s)) v r * Lagrange.basis s v i :=
  by
  symm
  refine eq_interpolate_of_eval_eq _ hvt (lt_of_le_of_lt (degree_sum_le _ _) ?_) fun i hi => ?_
  · simp_rw [Nat.cast_withBot, Finset.sup_lt_iff (WithBot.bot_lt_coe #t), degree_mul]
    intro i hi
    have hs : 1 ≤ #s := Nonempty.card_pos ⟨_, hi⟩
    have hst' : #s ≤ #t := card_le_card hst
    have H : #t = 1 + (#t - #s) + (#s - 1) := by
      rw [add_assoc, tsub_add_tsub_cancel hst' hs, ← add_tsub_assoc_of_le (hs.trans hst'), Nat.succ_add_sub_one,
        zero_add]
    rw [degree_basis (Set.InjOn.mono hst hvt) hi, H, WithBot.coe_add, Nat.cast_withBot,
      WithBot.add_lt_add_iff_right (@WithBot.coe_ne_bot _ (#s - 1))]
    convert degree_interpolate_lt _ (hvt.mono (coe_subset.mpr (insert_subset_iff.mpr ⟨hst hi, sdiff_subset⟩)))
    rw [card_insert_of_notMem (notMem_sdiff_of_mem_right hi), card_sdiff_of_subset hst, add_comm]
  · simp_rw [eval_finset_sum, eval_mul]
    by_cases hi' : i ∈ s
    · rw [← add_sum_erase _ _ hi', eval_basis_self (hvt.mono hst) hi',
        eval_interpolate_at_node _ (hvt.mono (coe_subset.mpr (insert_subset_iff.mpr ⟨hi, sdiff_subset⟩)))
          (mem_insert_self _ _),
        mul_one, add_eq_left]
      refine sum_eq_zero fun j hj => ?_
      rcases mem_erase.mp hj with ⟨hij, _⟩
      rw [eval_basis_of_ne hij hi', mul_zero]
    · have H : (∑ j ∈ s, eval (v i) (Lagrange.basis s v j)) = 1 := by
        rw [← eval_finset_sum, sum_basis (hvt.mono hst) hs, eval_one]
      rw [← mul_one (r i), ← H, mul_sum]
      refine sum_congr rfl fun j hj => ?_
      congr
      exact
        eval_interpolate_at_node _ (hvt.mono (insert_subset_iff.mpr ⟨hst hj, sdiff_subset⟩))
          (mem_insert.mpr (Or.inr (mem_sdiff.mpr ⟨hi, hi'⟩)))

Похожие утверждения