8.8. Proofs and Mathlib🔗

There is no HexPolyFastTheory. The theorems above say that each fast operation agrees with a HexPoly or HexTruncatedSeries operation, or describe its result by evaluation, divisibility and degree, and HexPolyTheory translates those into statements about Mathlib's Polynomial. For example, the interpolation plan computes Mathlib's Lagrange interpolant Lagrange.interpolate:
open Hex Hex.DensePoly HexPolyTheory Polynomial

namespace HexPolyFastChapterTheory

variable (plan : InterpPlan ℚ)

/-- The `i`th point of an interpolation plan. -/
def node (i : Fin plan.size) : ℚ :=
  plan.points[i.1]'(byplan:InterpPlan ℚi:Fin plan.size⊢ ↑i < plan.points.size simpAll goals completed! 🐙)

theorem node_injective :
    Function.Injective (node plan) := byplan:InterpPlan ℚ⊢ Function.Injective (node plan)
  intro i j hijplan:InterpPlan ℚi:Fin plan.sizej:Fin plan.sizehij:node plan i = node plan j⊢ i = j
  by_contra hneplan:InterpPlan ℚi:Fin plan.sizej:Fin plan.sizehij:node plan i = node plan jhne:¬i = j⊢ False
  let ys : Array ℚ := Array.ofFn fun k :
    Fin plan.size => if k = i then 1 else 0plan:InterpPlan ℚi:Fin plan.sizej:Fin plan.sizehij:node plan i = node plan jhne:¬i = jys:Array ℚ := Array.ofFn fun k => if k = i then 1 else 0⊢ False
  have hsize : ys.size = plan.size := byplan:InterpPlan ℚ⊢ Function.Injective (node plan) simp [ys]plan:InterpPlan ℚi:Fin plan.sizej:Fin plan.sizehij:node plan i = node plan jhne:¬i = jys:Array ℚ := Array.ofFn fun k => if k = i then 1 else 0hsize:ys.size = plan.size⊢ False
  obtain ⟨p, hp⟩ :
      ∃ p, plan.interpolate? ys = some p := byplan:InterpPlan ℚi:Fin plan.sizej:Fin plan.sizehij:node plan i = node plan jhne:¬i = jys:Array ℚ := Array.ofFn fun k => if k = i then 1 else 0hsize:ys.size = plan.size⊢ ∃ p, plan.interpolate? ys = some p
    cases h : plan.interpolate? ys with
    | none =>noneplan:InterpPlan ℚi:Fin plan.sizej:Fin plan.sizehij:node plan i = node plan jhne:¬i = jys:Array ℚ := Array.ofFn fun k => if k = i then 1 else 0hsize:ys.size = plan.sizeh:plan.interpolate? ys = none⊢ ∃ p, none = some p
      have := (plan.interpolate?_eq_none_iff ys).mp hnoneplan:InterpPlan ℚi:Fin plan.sizej:Fin plan.sizehij:node plan i = node plan jhne:¬i = jys:Array ℚ := Array.ofFn fun k => if k = i then 1 else 0hsize:ys.size = plan.sizeh:plan.interpolate? ys = nonethis:ys.size ≠ plan.size⊢ ∃ p, none = some p
      exact absurd hsize thisAll goals completed! 🐙
    | some p =>someplan:InterpPlan ℚi:Fin plan.sizej:Fin plan.sizehij:node plan i = node plan jhne:¬i = jys:Array ℚ := Array.ofFn fun k => if k = i then 1 else 0hsize:ys.size = plan.sizep:DensePoly ℚh:plan.interpolate? ys = some p⊢ ∃ p_1, some p = some p_1 exact ⟨p, rfl⟩plan:InterpPlan ℚi:Fin plan.sizej:Fin plan.sizehij:node plan i = node plan jhne:¬i = jys:Array ℚ := Array.ofFn fun k => if k = i then 1 else 0hsize:ys.size = plan.sizep:DensePoly ℚhp:plan.interpolate? ys = some p⊢ False
  have hi :=
    (plan.interpolate?_sound ys p hp).2 i i.2plan:InterpPlan ℚi:Fin plan.sizej:Fin plan.sizehij:node plan i = node plan jhne:¬i = jys:Array ℚ := Array.ofFn fun k => if k = i then 1 else 0hsize:ys.size = plan.sizep:DensePoly ℚhp:plan.interpolate? ys = some phi:p.eval plan.points[↑i] = ys.getD (↑i) 0⊢ False
  have hj :=
    (plan.interpolate?_sound ys p hp).2 j j.2plan:InterpPlan ℚi:Fin plan.sizej:Fin plan.sizehij:node plan i = node plan jhne:¬i = jys:Array ℚ := Array.ofFn fun k => if k = i then 1 else 0hsize:ys.size = plan.sizep:DensePoly ℚhp:plan.interpolate? ys = some phi:p.eval plan.points[↑i] = ys.getD (↑i) 0hj:p.eval plan.points[↑j] = ys.getD (↑j) 0⊢ False
  have hij' : plan.points[i.1]'(byplan:InterpPlan ℚi:Fin plan.sizej:Fin plan.sizehij:node plan i = node plan jhne:¬i = jys:Array ℚ := Array.ofFn fun k => if k = i then 1 else 0hsize:ys.size = plan.sizep:DensePoly ℚhp:plan.interpolate? ys = some phi:p.eval plan.points[↑i] = ys.getD (↑i) 0hj:p.eval plan.points[↑j] = ys.getD (↑j) 0⊢ ↑i < plan.points.size simpAll goals completed! 🐙) =
      plan.points[j.1]'(byplan:InterpPlan ℚi:Fin plan.sizej:Fin plan.sizehij:node plan i = node plan jhne:¬i = jys:Array ℚ := Array.ofFn fun k => if k = i then 1 else 0hsize:ys.size = plan.sizep:DensePoly ℚhp:plan.interpolate? ys = some phi:p.eval plan.points[↑i] = ys.getD (↑i) 0hj:p.eval plan.points[↑j] = ys.getD (↑j) 0⊢ ↑j < plan.points.size simpAll goals completed! 🐙) := hijplan:InterpPlan ℚi:Fin plan.sizej:Fin plan.sizehij:node plan i = node plan jhne:¬i = jys:Array ℚ := Array.ofFn fun k => if k = i then 1 else 0hsize:ys.size = plan.sizep:DensePoly ℚhp:plan.interpolate? ys = some phi:p.eval plan.points[↑i] = ys.getD (↑i) 0hj:p.eval plan.points[↑j] = ys.getD (↑j) 0hij':plan.points[↑i] = plan.points[↑j]⊢ False
  rw [hij',plan:InterpPlan ℚi:Fin plan.sizej:Fin plan.sizehij:node plan i = node plan jhne:¬i = jys:Array ℚ := Array.ofFn fun k => if k = i then 1 else 0hsize:ys.size = plan.sizep:DensePoly ℚhp:plan.interpolate? ys = some phi:p.eval plan.points[↑j] = ys.getD (↑i) 0hj:p.eval plan.points[↑j] = ys.getD (↑j) 0hij':plan.points[↑i] = plan.points[↑j]⊢ False hjplan:InterpPlan ℚi:Fin plan.sizej:Fin plan.sizehij:node plan i = node plan jhne:¬i = jys:Array ℚ := Array.ofFn fun k => if k = i then 1 else 0hsize:ys.size = plan.sizep:DensePoly ℚhp:plan.interpolate? ys = some phi:ys.getD (↑j) 0 = ys.getD (↑i) 0hj:p.eval plan.points[↑j] = ys.getD (↑j) 0hij':plan.points[↑i] = plan.points[↑j]⊢ False] at hiplan:InterpPlan ℚi:Fin plan.sizej:Fin plan.sizehij:node plan i = node plan jhne:¬i = jys:Array ℚ := Array.ofFn fun k => if k = i then 1 else 0hsize:ys.size = plan.sizep:DensePoly ℚhp:plan.interpolate? ys = some phi:ys.getD (↑j) 0 = ys.getD (↑i) 0hj:p.eval plan.points[↑j] = ys.getD (↑j) 0hij':plan.points[↑i] = plan.points[↑j]⊢ False
  simp [ys, Ne.symm hne] at hiAll goals completed! 🐙

theorem interpolate?_eq_lagrange (ys : Array ℚ)
    (p : DensePoly ℚ)
    (h : plan.interpolate? ys = some p) :
    toPolynomial p =
      Lagrange.interpolate Finset.univ (node plan)
        (fun i => ys.getD i 0) := byplan:InterpPlan ℚys:Array ℚp:DensePoly ℚh:plan.interpolate? ys = some p⊢ toPolynomial p = (Lagrange.interpolate Finset.univ (node plan)) fun i => ys.getD (↑i) 0
  obtain ⟨hsize, heval⟩ :=
    plan.interpolate?_sound ys p hplan:InterpPlan ℚys:Array ℚp:DensePoly ℚh:plan.interpolate? ys = some phsize:p.size ≤ plan.sizeheval:∀ (i : ℕ) (hi : i < plan.size), p.eval plan.points[i] = ys.getD i 0⊢ toPolynomial p = (Lagrange.interpolate Finset.univ (node plan)) fun i => ys.getD (↑i) 0
  apply Lagrange.eq_interpolate_of_eval_eqhvsplan:InterpPlan ℚys:Array ℚp:DensePoly ℚh:plan.interpolate? ys = some phsize:p.size ≤ plan.sizeheval:∀ (i : ℕ) (hi : i < plan.size), p.eval plan.points[i] = ys.getD i 0⊢ Set.InjOn (node plan) ↑Finset.univdegree_f_ltplan:InterpPlan ℚys:Array ℚp:DensePoly ℚh:plan.interpolate? ys = some phsize:p.size ≤ plan.sizeheval:∀ (i : ℕ) (hi : i < plan.size), p.eval plan.points[i] = ys.getD i 0⊢ (toPolynomial p).degree < ↑Finset.univ.cardeval_fplan:InterpPlan ℚys:Array ℚp:DensePoly ℚh:plan.interpolate? ys = some phsize:p.size ≤ plan.sizeheval:∀ (i : ℕ) (hi : i < plan.size), p.eval plan.points[i] = ys.getD i 0⊢ ∀ i ∈ Finset.univ, Polynomial.eval (node plan i) (toPolynomial p) = ys.getD (↑i) 0
  ·hvsplan:InterpPlan ℚys:Array ℚp:DensePoly ℚh:plan.interpolate? ys = some phsize:p.size ≤ plan.sizeheval:∀ (i : ℕ) (hi : i < plan.size), p.eval plan.points[i] = ys.getD i 0⊢ Set.InjOn (node plan) ↑Finset.univ exact (node_injective plan).injOnAll goals completed! 🐙
  ·degree_f_ltplan:InterpPlan ℚys:Array ℚp:DensePoly ℚh:plan.interpolate? ys = some phsize:p.size ≤ plan.sizeheval:∀ (i : ℕ) (hi : i < plan.size), p.eval plan.points[i] = ys.getD i 0⊢ (toPolynomial p).degree < ↑Finset.univ.card rw [Finset.card_univ,degree_f_ltplan:InterpPlan ℚys:Array ℚp:DensePoly ℚh:plan.interpolate? ys = some phsize:p.size ≤ plan.sizeheval:∀ (i : ℕ) (hi : i < plan.size), p.eval plan.points[i] = ys.getD i 0⊢ (toPolynomial p).degree < ↑(Fintype.card (Fin plan.size)) Fintype.card_fin,degree_f_ltplan:InterpPlan ℚys:Array ℚp:DensePoly ℚh:plan.interpolate? ys = some phsize:p.size ≤ plan.sizeheval:∀ (i : ℕ) (hi : i < plan.size), p.eval plan.points[i] = ys.getD i 0⊢ (toPolynomial p).degree < ↑plan.size
      Polynomial.degree_lt_iff_coeff_zerodegree_f_ltplan:InterpPlan ℚys:Array ℚp:DensePoly ℚh:plan.interpolate? ys = some phsize:p.size ≤ plan.sizeheval:∀ (i : ℕ) (hi : i < plan.size), p.eval plan.points[i] = ys.getD i 0⊢ ∀ (m : ℕ), plan.size ≤ m → (toPolynomial p).coeff m = 0]degree_f_ltplan:InterpPlan ℚys:Array ℚp:DensePoly ℚh:plan.interpolate? ys = some phsize:p.size ≤ plan.sizeheval:∀ (i : ℕ) (hi : i < plan.size), p.eval plan.points[i] = ys.getD i 0⊢ ∀ (m : ℕ), plan.size ≤ m → (toPolynomial p).coeff m = 0
    intro m hmdegree_f_ltplan:InterpPlan ℚys:Array ℚp:DensePoly ℚh:plan.interpolate? ys = some phsize:p.size ≤ plan.sizeheval:∀ (i : ℕ) (hi : i < plan.size), p.eval plan.points[i] = ys.getD i 0m:ℕhm:plan.size ≤ m⊢ (toPolynomial p).coeff m = 0
    rw [coeff_toPolynomialdegree_f_ltplan:InterpPlan ℚys:Array ℚp:DensePoly ℚh:plan.interpolate? ys = some phsize:p.size ≤ plan.sizeheval:∀ (i : ℕ) (hi : i < plan.size), p.eval plan.points[i] = ys.getD i 0m:ℕhm:plan.size ≤ m⊢ p.coeff m = 0]degree_f_ltplan:InterpPlan ℚys:Array ℚp:DensePoly ℚh:plan.interpolate? ys = some phsize:p.size ≤ plan.sizeheval:∀ (i : ℕ) (hi : i < plan.size), p.eval plan.points[i] = ys.getD i 0m:ℕhm:plan.size ≤ m⊢ p.coeff m = 0
    exact coeff_eq_zero_of_size_le p (byplan:InterpPlan ℚys:Array ℚp:DensePoly ℚh:plan.interpolate? ys = some phsize:p.size ≤ plan.sizeheval:∀ (i : ℕ) (hi : i < plan.size), p.eval plan.points[i] = ys.getD i 0m:ℕhm:plan.size ≤ m⊢ p.size ≤ m omegaAll goals completed! 🐙)
  ·eval_fplan:InterpPlan ℚys:Array ℚp:DensePoly ℚh:plan.interpolate? ys = some phsize:p.size ≤ plan.sizeheval:∀ (i : ℕ) (hi : i < plan.size), p.eval plan.points[i] = ys.getD i 0⊢ ∀ i ∈ Finset.univ, Polynomial.eval (node plan i) (toPolynomial p) = ys.getD (↑i) 0 intro i _eval_fplan:InterpPlan ℚys:Array ℚp:DensePoly ℚh:plan.interpolate? ys = some phsize:p.size ≤ plan.sizeheval:∀ (i : ℕ) (hi : i < plan.size), p.eval plan.points[i] = ys.getD i 0i:Fin plan.sizea✝:i ∈ Finset.univ⊢ Polynomial.eval (node plan i) (toPolynomial p) = ys.getD (↑i) 0
    rw [eval_toPolynomialeval_fplan:InterpPlan ℚys:Array ℚp:DensePoly ℚh:plan.interpolate? ys = some phsize:p.size ≤ plan.sizeheval:∀ (i : ℕ) (hi : i < plan.size), p.eval plan.points[i] = ys.getD i 0i:Fin plan.sizea✝:i ∈ Finset.univ⊢ p.eval (node plan i) = ys.getD (↑i) 0]eval_fplan:InterpPlan ℚys:Array ℚp:DensePoly ℚh:plan.interpolate? ys = some phsize:p.size ≤ plan.sizeheval:∀ (i : ℕ) (hi : i < plan.size), p.eval plan.points[i] = ys.getD i 0i:Fin plan.sizea✝:i ∈ Finset.univ⊢ p.eval (node plan i) = ys.getD (↑i) 0
    exact heval i i.2All goals completed! 🐙

end HexPolyFastChapterTheory
The proof that the points of a plan are distinct uses only the public theorems: if two points were equal, the values 1 and 0 at them could not both be interpolated.