structure Hex.DensePoly.InterpPlan (F : Type u) [DecidableEq F] [Lean.Grind.Field F] : Type u

An opaque reusable interpolation plan at a distinct point sequence.

• mulData : Hex.DensePoly.MulPlan F
• pointsData : Array F
• evalData : Hex.DensePoly.EvalPlan F
• nodeData : Option ((poly : Hex.DensePoly F) × Hex.DensePoly.PointNode F (mulData self) (pointsData self).toList poly)
• invDerivData : Array F
• distinctData : (pointsData self).toList.Nodup
• evalPointsData : (evalData self).points = pointsData self
• emptyData : nodeData self = none → (pointsData self).toList = []
• invDerivSpec (built : (poly : Hex.DensePoly F) × Hex.DensePoly.PointNode F (mulData self) (pointsData self).toList poly) : nodeData self = some built → invDerivData self = Array.map (fun (x : F) => x⁻¹) ((evalData self).eval built.fst.derivative)

def Hex.DensePoly.InterpPlan.build? {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (mul : MulPlan F) (points : Array F) : Option (InterpPlan F)

Build a reusable interpolation plan exactly when the points are distinct.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.DensePoly.InterpPlan.build?_eq_none_iff {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (mul : MulPlan F) (points : Array F) : build? mul points = none ↔ ¬points.toList.Nodup

Plan construction fails exactly when the point sequence has a duplicate.

def Hex.DensePoly.InterpPlan.points {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : InterpPlan F) : Array F

Planned interpolation points.

Equations

• plan.points = Hex.DensePoly.InterpPlan.pointsData✝ plan

def Hex.DensePoly.InterpPlan.size {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : InterpPlan F) : Nat

Number of planned interpolation points.

Equations

• plan.size = plan.points.size

@[simp]

theorem Hex.DensePoly.InterpPlan.size_points {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : InterpPlan F) : plan.points.size = plan.size

The points accessor has the advertised plan size.

def Hex.DensePoly.InterpPlan.evalPlan {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : InterpPlan F) : EvalPlan F

The cached multipoint plan used for derivative evaluation.

Equations

• plan.evalPlan = Hex.DensePoly.InterpPlan.evalData✝ plan

@[simp]

theorem Hex.DensePoly.InterpPlan.evalPlan_points {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : InterpPlan F) : plan.evalPlan.points = plan.points

The nested evaluation plan uses the same point sequence.

@[simp]

theorem Hex.DensePoly.InterpPlan.evalPlan_size {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : InterpPlan F) : plan.evalPlan.size = plan.size

The nested evaluation plan has the same size.

def Hex.DensePoly.InterpPlan.interpolate? {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : InterpPlan F) (values : Array F) : Option (DensePoly F)

Interpolate a matching value array, rejecting only a count mismatch.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.DensePoly.InterpPlan.interpolate?_eq_none_iff {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : InterpPlan F) (values : Array F) : plan.interpolate? values = none ↔ values.size ≠ plan.size

Interpolation rejects exactly a mismatch between point and value counts.

theorem Hex.DensePoly.InterpPlan.interpolate?_sound {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : InterpPlan F) (values : Array F) (p : DensePoly F) (hsome : plan.interpolate? values = some p) : p.size ≤ plan.size ∧ ∀ (i : Nat) (hi : i < plan.size), p.eval plan.points[i] = values.getD i 0

A successful interpolation has the requested values and no more coefficients than there are points.

theorem Hex.DensePoly.InterpPlan.interpolate?_unique {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : InterpPlan F) (values : Array F) (p q : DensePoly F) (hsome : plan.interpolate? values = some p) (hqsize : q.size ≤ plan.size) (hqvalues : ∀ (i : Nat) (hi : i < plan.size), q.eval plan.points[i] = values.getD i 0) : q = p

The successful interpolation is the unique polynomial of size at most the point count with the supplied values.