# Theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation

```section ‹Lagrange Interpolation›

text ‹This section introduces the function @{term "interpolate"}, which constructs the Lagrange
interpolation polynomials for a given set of points, followed by a theorem of its correctness.›

theory Lagrange_Interpolation
imports "HOL-Algebra.Polynomial_Divisibility"
begin

text ‹A finite product in a domain is \$0\$ if and only if at least one factor is. This could be added
to @{theory "HOL-Algebra.FiniteProduct"} or @{theory "HOL-Algebra.Ring"}.›
lemma (in domain) finprod_zero_iff:
assumes "finite A"
assumes "⋀a. a ∈ A ⟹ f a ∈ carrier R"
shows "finprod R f A = 𝟬 ⟷ (∃x ∈ A. f x = 𝟬)"
using assms
proof (induct A rule: finite_induct)
case empty
then show ?case by simp
next
case (insert y F)
moreover have "f ∈ F → carrier R" using insert by blast
ultimately show ?case by (simp add:integral_iff)
qed

lemma (in ring) poly_of_const_in_carrier:
assumes "s ∈ carrier R"
shows "poly_of_const s ∈ carrier (poly_ring R)"
using poly_of_const_def assms

lemma (in ring) eval_poly_of_const:
assumes "x ∈ carrier R"
shows "eval (poly_of_const x) y = x"

lemma (in ring) eval_in_carrier_2:
assumes "x ∈ carrier (poly_ring R)"
assumes "y ∈ carrier R"
shows "eval x y ∈ carrier R"
using eval_in_carrier univ_poly_carrier polynomial_incl assms by blast

lemma (in domain) poly_mult_degree_le_1:
assumes "x ∈ carrier (poly_ring R)"
assumes "y ∈ carrier (poly_ring R)"
shows "degree (x ⊗⇘poly_ring R⇙ y) ≤ degree x + degree y"
proof -
have "degree (x ⊗⇘poly_ring R⇙ y) = (if x = [] ∨ y = [] then 0 else degree x + degree y)"
unfolding univ_poly_mult
by (metis univ_poly_carrier assms(1,2) carrier_is_subring poly_mult_degree_eq)
thus ?thesis by (metis nat_le_linear zero_le)
qed

lemma (in domain) poly_mult_degree_le:
assumes "x ∈ carrier (poly_ring R)"
assumes "y ∈ carrier (poly_ring R)"
assumes "degree x ≤ n"
assumes "degree y ≤ m"
shows "degree (x ⊗⇘poly_ring R⇙ y) ≤ n + m"
using poly_mult_degree_le_1 assms add_mono by force

assumes "x ∈ carrier (poly_ring R)" "degree x ≤ n"
assumes "y ∈ carrier (poly_ring R)" "degree y ≤ n"
shows "degree (x ⊕⇘poly_ring R⇙ y) ≤ n"

lemma (in domain) poly_sub_degree_le:
assumes "x ∈ carrier (poly_ring R)" "degree x ≤ n"
assumes "y ∈ carrier (poly_ring R)" "degree y ≤ n"
shows "degree (x ⊖⇘poly_ring R⇙ y) ≤ n"
proof -
interpret x:cring "poly_ring R"
using carrier_is_subring domain.univ_poly_is_cring domain_axioms by auto

show ?thesis
unfolding a_minus_def
using assms univ_poly_a_inv_degree carrier_is_subring poly_add_degree_le x.a_inv_closed
by simp
qed

lemma (in domain) poly_sum_degree_le:
assumes "finite A"
assumes "⋀x. x ∈ A ⟹ degree (f x) ≤ n"
assumes "⋀x. x ∈ A ⟹ f x ∈ carrier (poly_ring R)"
shows "degree (finsum (poly_ring R) f A) ≤ n"
using assms
proof (induct A rule:finite_induct)
case empty
interpret x:cring "poly_ring R"
using carrier_is_subring domain.univ_poly_is_cring domain_axioms by auto
show ?case using empty by (simp add:univ_poly_zero)
next
case (insert x F)
interpret x:cring "poly_ring R"
using carrier_is_subring domain.univ_poly_is_cring domain_axioms by auto
have a: "degree (f x ⊕⇘poly_ring R⇙ finsum (poly_ring R) f F) ≤ n"
using insert poly_add_degree_le x.finsum_closed by auto
show ?case using insert a by auto
qed

definition (in ring) lagrange_basis_polynomial_aux where
"lagrange_basis_polynomial_aux S =
(⨂⇘poly_ring R⇙ s ∈ S. X ⊖⇘poly_ring R⇙ (poly_of_const s))"

lemma (in domain) lagrange_aux_eval:
assumes "finite S"
assumes "S ⊆ carrier R"
assumes "x ∈ carrier R"
shows "(eval (lagrange_basis_polynomial_aux S) x) = (⨂s ∈ S. x ⊖ s)"
proof -
interpret x:ring_hom_cring "poly_ring R" "R" "(λp. eval p x)"
by (rule eval_cring_hom[OF carrier_is_subring assms(3)])

have "⋀a. a ∈ S ⟹ X ⊖⇘poly_ring R⇙ poly_of_const a ∈ carrier (poly_ring R)"
by (meson poly_of_const_in_carrier carrier_is_subring assms(2) cring.cring_simprules(4)
domain_def subsetD univ_poly_is_domain var_closed(1))

moreover have "⋀s. s ∈ S ⟹ eval (X ⊖⇘poly_ring R⇙ poly_of_const s) x = x ⊖ s"
using assms var_closed carrier_is_subring poly_of_const_in_carrier subsetD[OF assms(2)]

moreover have "a_minus R x ∈ S → carrier R"
using assms by blast

ultimately show ?thesis
qed

lemma (in domain) lagrange_aux_poly:
assumes "finite S"
assumes "S ⊆ carrier R"
shows "lagrange_basis_polynomial_aux S ∈ carrier (poly_ring R)"
proof -
have a:"subring (carrier R) R"
using carrier_is_subring assms by blast

have b: "⋀a. a ∈ S ⟹ X ⊖⇘poly_ring R⇙ poly_of_const a ∈ carrier (poly_ring R)"
by (meson poly_of_const_in_carrier a assms(2) cring.cring_simprules(4) domain_def subsetD
univ_poly_is_domain var_closed(1))

interpret x:cring "poly_ring R"
using carrier_is_subring domain.univ_poly_is_cring domain_axioms by auto

show ?thesis
using lagrange_basis_polynomial_aux_def b x.finprod_closed[OF Pi_I] by simp
qed

lemma (in domain) poly_prod_degree_le:
assumes "finite A"
assumes "⋀x. x ∈ A ⟹ f x ∈ carrier (poly_ring R)"
shows "degree (finprod (poly_ring R) f A) ≤ (∑x ∈ A. degree (f x))"
using assms
proof (induct A rule:finite_induct)
case empty
interpret x:cring "poly_ring R"
using carrier_is_subring domain.univ_poly_is_cring domain_axioms by auto
next
case (insert x F)
interpret x:cring "poly_ring R"
using carrier_is_subring domain.univ_poly_is_cring domain_axioms by auto
have a:"f ∈ F → carrier (poly_ring R)"
using insert by blast
have b:"f x ∈ carrier (poly_ring R)"
using insert by blast
have "degree (finprod (poly_ring R) f (insert x F)) = degree (f x ⊗⇘poly_ring R⇙ finprod (poly_ring R) f F)"
using a b insert by simp
also have "... ≤ degree (f x) + degree (finprod (poly_ring R) f F)"
using poly_mult_degree_le x.finprod_closed[OF a] b by auto
also have "... ≤ degree (f x) + (∑y ∈ F. degree (f y))"
using insert(3) a add_mono by auto
also have "... = (∑y ∈ (insert x F). degree (f y))" using insert by simp
finally show ?case by simp
qed

lemma (in domain) lagrange_aux_degree:
assumes "finite S"
assumes "S ⊆ carrier R"
shows "degree (lagrange_basis_polynomial_aux S) ≤ card S"
proof -
interpret x:cring "poly_ring R"
using carrier_is_subring domain.univ_poly_is_cring domain_axioms by auto

have "degree X ≤ 1" by (simp add:var_def)
moreover have "⋀y. y∈ S ⟹ degree (poly_of_const y) ≤ 1" by (simp add:poly_of_const_def)
ultimately have a: "⋀y. y∈ S ⟹ degree (X ⊖⇘poly_ring R⇙ poly_of_const y) ≤ 1"
by (meson assms(2) in_mono poly_of_const_in_carrier poly_sub_degree_le var_closed[OF carrier_is_subring])

have b:"⋀y. y ∈ S ⟹ (X ⊖⇘poly_ring R⇙ poly_of_const y) ∈ carrier (poly_ring R)"
by (meson subsetD x.minus_closed var_closed(1)[OF carrier_is_subring] poly_of_const_in_carrier assms(2))

have "degree (lagrange_basis_polynomial_aux S) ≤ (∑y ∈ S. degree (X ⊖⇘poly_ring R⇙ poly_of_const y))"
using lagrange_basis_polynomial_aux_def b poly_prod_degree_le[OF assms(1)] by auto
also have "... ≤ (∑y ∈ S. 1)"
using sum_mono a by force
also have "... = card S" by simp
finally show ?thesis by simp
qed

definition (in ring) lagrange_basis_polynomial where
"lagrange_basis_polynomial S x = lagrange_basis_polynomial_aux S
⊗⇘poly_ring R⇙ (poly_of_const (inv⇘R⇙ (⨂s ∈ S. x ⊖ s)))"

lemma (in field)
assumes "finite S"
assumes "S ⊆ carrier R"
assumes "x ∈ carrier R - S"
shows
lagrange_one: "eval (lagrange_basis_polynomial S x) x = 𝟭" and
lagrange_degree: "degree (lagrange_basis_polynomial S x) ≤ card S" and
lagrange_zero: "⋀s. s ∈ S ⟹ eval (lagrange_basis_polynomial S x) s = 𝟬" and
lagrange_poly: "lagrange_basis_polynomial S x ∈ carrier (poly_ring R)"
proof -
interpret x:ring_hom_cring "poly_ring R" "R" "(λp. eval p x)"
using assms carrier_is_subring eval_cring_hom by blast

define p where "p = lagrange_basis_polynomial_aux S"
have a:"eval p x = (⨂s ∈ S. x ⊖ s)"
using assms by (simp add:p_def lagrange_aux_eval)

have b:"p ∈ carrier (poly_ring R)" using assms

have "⋀y. y ∈ S ⟹ a_minus R x y ∈ carrier R"
using assms by blast

hence c:"finprod R (a_minus R x) S ∈ Units R"
using finprod_closed[OF Pi_I] assms

have "eval (lagrange_basis_polynomial S x) x =
(⨂s ∈ S. x ⊖ s) ⊗ eval (poly_of_const (inv finprod R (a_minus R x) S)) x"
using poly_of_const_in_carrier Units_inv_closed c p_def[symmetric]
by (simp add: lagrange_basis_polynomial_def x.hom_mult[OF b] a)
also have "... =  𝟭"
using poly_of_const_in_carrier Units_inv_closed c eval_poly_of_const by simp
finally show "eval (lagrange_basis_polynomial S x) x = 𝟭" by simp

have "degree (lagrange_basis_polynomial S x) ≤ degree p + degree (poly_of_const (inv finprod R (a_minus R x) S))"
unfolding lagrange_basis_polynomial_def p_def[symmetric]
using poly_mult_degree_le[OF b] poly_of_const_in_carrier Units_inv_closed c by auto
also have "... ≤ card S + 0"
using add_mono lagrange_aux_degree[OF assms(1) assms(2)] p_def poly_of_const_def by auto
finally show "degree (lagrange_basis_polynomial S x) ≤ card S" by simp

show "⋀s. s ∈ S ⟹ eval (lagrange_basis_polynomial S x) s = 𝟬"
proof -
fix s
assume d:"s ∈ S"

interpret s:ring_hom_cring "poly_ring R" "R" "(λp. eval p s)"
using eval_cring_hom carrier_is_subring assms d by blast

have "eval p s = finprod R (a_minus R s) S"
using subsetD[OF assms(2) d] assms
also have "... = 𝟬"
using subsetD[OF assms(2)] d assms by (simp add: finprod_zero_iff)
finally have "eval p s = 𝟬⇘R⇙" by simp

moreover have "eval (poly_of_const (inv finprod R (a_minus R x) S)) s ∈ carrier R"
using s.hom_closed poly_of_const_in_carrier  Units_inv_closed c by blast

ultimately show "eval (lagrange_basis_polynomial S x) s = 𝟬"
using poly_of_const_in_carrier Units_inv_closed c
by (simp add:lagrange_basis_polynomial_def Let_def p_def[symmetric] s.hom_mult[OF b])
qed

interpret r:cring "poly_ring R"
using carrier_is_subring domain.univ_poly_is_cring domain_axioms by auto

show "lagrange_basis_polynomial S x ∈ carrier (poly_ring R)"
using lagrange_basis_polynomial_def p_def[symmetric] poly_of_const_in_carrier Units_inv_closed
a b c by simp
qed

definition (in ring) interpolate where
"interpolate S f =
(⨁⇘poly_ring R⇙s ∈ S. lagrange_basis_polynomial (S - {s}) s ⊗⇘poly_ring R⇙ (poly_of_const (f s)))"

text ‹Let @{term "f"} be a function and @{term "S"} be a finite subset of the domain of the field.
Then @{term "interpolate S f"} will return a polynomial with degree less than @{term "card S"}
interpolating @{term "f"} on @{term "S"}.›

theorem (in field)
assumes "finite S"
assumes "S ⊆ carrier R"
assumes "f ` S ⊆ carrier R"
shows
interpolate_poly: "interpolate S f ∈ carrier (poly_ring R)" and
interpolate_degree: "degree (interpolate S f) ≤ card S - 1" and
interpolate_eval: "⋀s. s ∈ S ⟹ eval (interpolate S f) s = f s"
proof -
interpret r:cring "poly_ring R"
using carrier_is_subring domain.univ_poly_is_cring domain_axioms by auto

have a:"⋀x. x ∈ S ⟹ lagrange_basis_polynomial (S - {x}) x ∈ carrier (poly_ring R)"
by (meson lagrange_poly assms Diff_iff finite_Diff in_mono insertI1 subset_insertI2 subset_insert_iff)

have b:"⋀x. x ∈ S ⟹ f x ∈ carrier R" using assms by blast

have c:"⋀x. x ∈ S ⟹ degree (lagrange_basis_polynomial (S - {x}) x) ≤ card S - 1"
by (metis (full_types) lagrange_degree  DiffI Diff_insert_absorb assms(1) assms(2)
card_Diff_singleton finite_insert insert_subset mk_disjoint_insert)

have d: "⋀x. x ∈ S ⟹
degree (lagrange_basis_polynomial (S - {x}) x ⊗⇘poly_ring R⇙ poly_of_const (f x)) ≤ (card S - 1) + 0"
using poly_of_const_in_carrier[OF b] poly_mult_degree_le[OF a] c poly_of_const_def by fastforce

show "interpolate S f ∈ carrier (poly_ring R)"
using interpolate_def poly_of_const_in_carrier a b by simp

show "degree (interpolate S f) ≤ card S - 1"
using poly_sum_degree_le[OF assms(1) d] poly_of_const_in_carrier[OF b] interpolate_def a by simp

have e:"subring (carrier R) R"
using carrier_is_subring assms by blast

show "⋀s. s ∈ S ⟹ eval (interpolate S f) s = f s"
proof -
fix s
assume f:"s ∈ S"
interpret s:ring_hom_cring "poly_ring R" "R" "(λp. eval p s)"
using eval_cring_hom[OF e] assms f by blast
have g:"⋀i. i ∈ S ⟹
eval (lagrange_basis_polynomial (S - {i}) i ⊗⇘poly_ring R⇙ poly_of_const (f i)) s =
(if s = i then f s else 𝟬)"
proof -
fix i
assume i_in_S: "i ∈ S"
have "eval (lagrange_basis_polynomial (S - {i}) i ⊗⇘poly_ring R⇙ poly_of_const (f i)) s =
eval (lagrange_basis_polynomial (S - {i}) i) s ⊗ f i"
using b i_in_S poly_of_const_in_carrier
by (simp add: s.hom_mult[OF a] eval_poly_of_const)
also have "... = (if s = i then f s else 𝟬)"
using b i_in_S poly_of_const_in_carrier assms f
apply (cases "s=i", simp, subst lagrange_one, auto)
by (subst lagrange_zero, auto)
finally show
"eval (lagrange_basis_polynomial (S - {i}) i ⊗⇘poly_ring R⇙ poly_of_const (f i)) s =
(if s = i then f s else 𝟬)" by simp
qed

have "eval (interpolate S f) s =
(⨁x∈S. eval (lagrange_basis_polynomial (S - {x}) x ⊗⇘poly_ring R⇙ poly_of_const (f x)) s)"
using  poly_of_const_in_carrier[OF b] a e
by (simp add: interpolate_def s.hom_finsum[OF Pi_I] comp_def)
also have "... =  (⨁x∈S. if s = x then f s else 𝟬)"
using b g by (simp cong: finsum_cong)
also have "... = f s"
using finsum_singleton[OF f assms(1)] f assms by auto
finally show "eval (interpolate S f) s = f s" by simp
qed
qed

end```