English
Sum over all basis elements for a nonempty s equals 1.
Русский
Сумма по всем элементам базиса равна 1.
LaTeX
$$\sum_{j\in s} Lagrange.basis s v j = 1$$
Lean4
theorem sum_basis (hvs : Set.InjOn v s) (hs : s.Nonempty) : ∑ j ∈ s, Lagrange.basis s v j = 1 :=
by
refine eq_of_degrees_lt_of_eval_index_eq s hvs (lt_of_le_of_lt (degree_sum_le _ _) ?_) ?_ ?_
· rw [Nat.cast_withBot, Finset.sup_lt_iff (WithBot.bot_lt_coe #s)]
intro i hi
rw [degree_basis hvs hi, Nat.cast_withBot, WithBot.coe_lt_coe]
exact Nat.pred_lt (card_ne_zero_of_mem hi)
· rw [degree_one, ← WithBot.coe_zero, Nat.cast_withBot, WithBot.coe_lt_coe]
exact Nonempty.card_pos hs
· intro i hi
rw [eval_finset_sum, eval_one, ← add_sum_erase _ _ hi, eval_basis_self hvs hi, add_eq_left]
refine sum_eq_zero fun j hj => ?_
rcases mem_erase.mp hj with ⟨hij, _⟩
rw [eval_basis_of_ne hij hi]
