English
For i≠j in s, the interpolant on s splits into two interpolants on the deletions of i or j, weighted by basis divisors.
Русский
Если i,j ∈ s и i ≠ j, то интерполянт на s распадается на сумму двух слагаемых: интерполянт на s\\{j} умноженный на basisDivisor(v(i),v(j) и интерполянт на s\\{i} умноженный на basisDivisor(v(j),v(i)).
LaTeX
$$$ \\operatorname{interpolate}(s,v)r = \\operatorname{interpolate}(s\\setminus\\{j\\},v)r \\cdot \\operatorname{basisDivisor}(v(i),v(j)) \\\\quad + \\operatorname{interpolate}(s\\setminus\\{i\\},v)r \\cdot \\operatorname{basisDivisor}(v(j),v(i)). $$$
Lean4
theorem interpolate_eq_add_interpolate_erase (hvs : Set.InjOn v s) (hi : i ∈ s) (hj : j ∈ s) (hij : i ≠ j) :
interpolate s v r =
interpolate (s.erase j) v r * basisDivisor (v i) (v j) + interpolate (s.erase i) v r * basisDivisor (v j) (v i) :=
by
rw [interpolate_eq_sum_interpolate_insert_sdiff _ hvs ⟨i, mem_insert_self i { j }⟩ _,
sum_insert (notMem_singleton.mpr hij), sum_singleton, basis_pair_left hij, basis_pair_right hij,
sdiff_insert_insert_of_mem_of_notMem hi (notMem_singleton.mpr hij), sdiff_singleton_eq_erase, pair_comm,
sdiff_insert_insert_of_mem_of_notMem hj (notMem_singleton.mpr hij.symm), sdiff_singleton_eq_erase]
exact insert_subset_iff.mpr ⟨hi, singleton_subset_iff.mpr hj⟩
