Certified roots of differentiable systems

This module implements a strong, norm-form Krawczyk test for square systems in LeanCert's ADSupported expression fragment. The center and rational preconditioner are untrusted certificate data; krawczykCheck verifies AD support, center containment, invertibility, a strict infinity-norm contraction bound, and a strict self-map enclosure.

The golden theorem krawczykCheck_sound turns a successful Boolean check into existence and uniqueness of a real root in the supplied box.

@[instance_reducible]

def LeanCert.Engine.intervalRatZero : Zero Core.IntervalRat

Equations

• LeanCert.Engine.intervalRatZero = { zero := LeanCert.Core.IntervalRat.singleton 0 }

@[instance_reducible]

def LeanCert.Engine.intervalRatAdd : Add Core.IntervalRat

Equations

• LeanCert.Engine.intervalRatAdd = { add := LeanCert.Core.IntervalRat.add }

@[instance_reducible]

def LeanCert.Engine.instSMulNatIntervalRat : SMul ℕ Core.IntervalRat

Equations

• LeanCert.Engine.instSMulNatIntervalRat = { smul := fun (n : ℕ) (a : LeanCert.Core.IntervalRat) => { lo := ↑n * a.lo, hi := ↑n * a.hi, le := ⋯ } }

@[instance_reducible]

def LeanCert.Engine.instAddCommMonoidIntervalRat : AddCommMonoid Core.IntervalRat

Equations

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

noncomputable def LeanCert.Engine.finEnv {n : ℕ} (x : Fin n → ℝ) : ℕ → ℝ

Equations

• LeanCert.Engine.finEnv x i = if h : i < n then x ⟨i, h⟩ else 0

noncomputable def LeanCert.Engine.evalFin {n : ℕ} (e : Core.Expr) (x : Fin n → ℝ) : ℝ

Equations

• LeanCert.Engine.evalFin e x = LeanCert.Core.Expr.eval (LeanCert.Engine.finEnv x) e

theorem LeanCert.Engine.evalFin_differentiable {n : ℕ} (e : Core.Expr) (h : ADSupported e) : Differentiable ℝ (evalFin e)

theorem LeanCert.Engine.finEnv_update {n : ℕ} (x : Fin n → ℝ) (j : Fin n) (t : ℝ) : finEnv (Function.update x j t) = finEnv x[↑j ↦ t]

theorem LeanCert.Engine.fderiv_single_eq_deriv_evalAlong {n : ℕ} (e : Core.Expr) (h : ADSupported e) (x : Fin n → ℝ) (j : Fin n) : (fderiv ℝ (evalFin e) x) (Pi.single j 1) = deriv (e.evalAlong (finEnv x) ↑j) (x j)

noncomputable def LeanCert.Engine.systemEval {n : ℕ} (F : Fin n → Core.Expr) (x : Fin n → ℝ) : Fin n → ℝ

Equations

• LeanCert.Engine.systemEval F x i = LeanCert.Engine.evalFin (F i) x

theorem LeanCert.Engine.systemEval_differentiable {n : ℕ} (F : Fin n → Core.Expr) (h : ∀ (i : Fin n), ADSupported (F i)) : Differentiable ℝ (systemEval F)

noncomputable def LeanCert.Engine.jacobianAt {n : ℕ} (F : Fin n → Core.Expr) (x : Fin n → ℝ) : Matrix (Fin n) (Fin n) ℝ

Equations

• LeanCert.Engine.jacobianAt F x = LinearMap.toMatrix' ↑(fderiv ℝ (LeanCert.Engine.systemEval F) x)

theorem LeanCert.Engine.jacobianAt_apply {n : ℕ} (F : Fin n → Core.Expr) (h : ∀ (i : Fin n), ADSupported (F i)) (x : Fin n → ℝ) (i j : Fin n) : jacobianAt F x i j = deriv ((F i).evalAlong (finEnv x) ↑j) (x j)

def LeanCert.Engine.finBoxEnv {n : ℕ} (X : Fin n → Core.IntervalRat) : IntervalEnv

Equations

• LeanCert.Engine.finBoxEnv X i = if h : i < n then X ⟨i, h⟩ else LeanCert.Core.IntervalRat.singleton 0

def LeanCert.Engine.FinBoxMem {n : ℕ} (x : Fin n → ℝ) (X : Fin n → Core.IntervalRat) : Prop

Equations

• LeanCert.Engine.FinBoxMem x X = ∀ (i : Fin n), x i ∈ X i

def LeanCert.Engine.intervalJacobian {n : ℕ} (F : Fin n → Core.Expr) (X : Fin n → Core.IntervalRat) (cfg : EvalConfig := { }) : Matrix (Fin n) (Fin n) Core.IntervalRat

Equations

• LeanCert.Engine.intervalJacobian F X cfg i j = LeanCert.Engine.Optimization.derivIntervalCoreN (F i) (LeanCert.Engine.finBoxEnv X) (↑j) cfg

theorem LeanCert.Engine.finEnv_mem_finBoxEnv {n : ℕ} {x : Fin n → ℝ} {X : Fin n → Core.IntervalRat} (hx : FinBoxMem x X) (i : ℕ) : finEnv x i ∈ finBoxEnv X i

theorem LeanCert.Engine.jacobianAt_mem_intervalJacobian {n : ℕ} (F : Fin n → Core.Expr) (h : ∀ (i : Fin n), ADSupported (F i)) (X : Fin n → Core.IntervalRat) (x : Fin n → ℝ) (hx : FinBoxMem x X) (cfg : EvalConfig) (i j : Fin n) : jacobianAt F x i j ∈ intervalJacobian F X cfg i j

noncomputable def LeanCert.Engine.matrixCLM {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) : (Fin n → ℝ) →L[ℝ] Fin n → ℝ

Equations

• LeanCert.Engine.matrixCLM A = { toLinearMap := A.mulVecLin, cont := ⋯ }

noncomputable def LeanCert.Engine.newtonMap {n : ℕ} (Y : Matrix (Fin n) (Fin n) ℝ) (F : Fin n → Core.Expr) (x : Fin n → ℝ) : Fin n → ℝ

Equations

• LeanCert.Engine.newtonMap Y F x = x - Y.mulVec (LeanCert.Engine.systemEval F x)

theorem LeanCert.Engine.newtonMap_differentiable {n : ℕ} (Y : Matrix (Fin n) (Fin n) ℝ) (F : Fin n → Core.Expr) (h : ∀ (i : Fin n), ADSupported (F i)) : Differentiable ℝ (newtonMap Y F)

theorem LeanCert.Engine.newtonMap_fderiv_matrix {n : ℕ} (Y : Matrix (Fin n) (Fin n) ℝ) (F : Fin n → Core.Expr) (h : ∀ (i : Fin n), ADSupported (F i)) (x : Fin n → ℝ) : LinearMap.toMatrix' ↑(fderiv ℝ (newtonMap Y F) x) = 1 - Y * jacobianAt F x

def LeanCert.Engine.finBoxSet {n : ℕ} (X : Fin n → Core.IntervalRat) : Set (Fin n → ℝ)

Equations

• LeanCert.Engine.finBoxSet X = {x : Fin n → ℝ | LeanCert.Engine.FinBoxMem x X}

theorem LeanCert.Engine.finBoxSet_closed {n : ℕ} (X : Fin n → Core.IntervalRat) : IsClosed (finBoxSet X)

theorem LeanCert.Engine.finBoxSet_convex {n : ℕ} (X : Fin n → Core.IntervalRat) : Convex ℝ (finBoxSet X)

theorem LeanCert.Engine.contraction_unique_fixedPoint_in_finBox {n : ℕ} (X : Fin n → Core.IntervalRat) (m : Fin n → ℝ) (hm : FinBoxMem m X) (g : (Fin n → ℝ) → Fin n → ℝ) (hmap : Set.MapsTo g (finBoxSet X) (finBoxSet X)) (q : ℝ) (hq0 : 0 ≤ q) (hq1 : q < 1) (hdiff : ∀ x ∈ finBoxSet X, DifferentiableAt ℝ g x) (hderiv : ∀ x ∈ finBoxSet X, ‖fderiv ℝ g x‖ ≤ q) : ∃! x : Fin n → ℝ, FinBoxMem x X ∧ g x = x

def LeanCert.Engine.intervalIdentity {n : ℕ} : Matrix (Fin n) (Fin n) Core.IntervalRat

Equations

• LeanCert.Engine.intervalIdentity i j = LeanCert.Core.IntervalRat.singleton (if i = j then 1 else 0)

def LeanCert.Engine.ratMulInterval {n : ℕ} (Y : Matrix (Fin n) (Fin n) ℚ) (J : Matrix (Fin n) (Fin n) Core.IntervalRat) : Matrix (Fin n) (Fin n) Core.IntervalRat

Equations

• LeanCert.Engine.ratMulInterval Y J i j = ∑ k : Fin n, LeanCert.Core.IntervalRat.scale (Y i k) (J k j)

def LeanCert.Engine.preconditionedJacobian {n : ℕ} (Y : Matrix (Fin n) (Fin n) ℚ) (J : Matrix (Fin n) (Fin n) Core.IntervalRat) : Matrix (Fin n) (Fin n) Core.IntervalRat

Equations

• LeanCert.Engine.preconditionedJacobian Y J i j = (LeanCert.Engine.intervalIdentity i j).sub (LeanCert.Engine.ratMulInterval Y J i j)

theorem LeanCert.Engine.mem_interval_sum {ι : Type u_1} [Fintype ι] (s : Finset ι) (x : ι → ℝ) (I : ι → Core.IntervalRat) (h : ∀ i ∈ s, x i ∈ I i) : ∑ i ∈ s, x i ∈ ∑ i ∈ s, I i

theorem LeanCert.Engine.mem_ratMulInterval {n : ℕ} (Y : Matrix (Fin n) (Fin n) ℚ) (Jreal : Matrix (Fin n) (Fin n) ℝ) (J : Matrix (Fin n) (Fin n) Core.IntervalRat) (hJ : ∀ (i j : Fin n), Jreal i j ∈ J i j) (i j : Fin n) : ((Y.map fun (q : ℚ) => ↑q) * Jreal) i j ∈ ratMulInterval Y J i j

theorem LeanCert.Engine.mem_preconditionedJacobian {n : ℕ} (Y : Matrix (Fin n) (Fin n) ℚ) (Jreal : Matrix (Fin n) (Fin n) ℝ) (J : Matrix (Fin n) (Fin n) Core.IntervalRat) (hJ : ∀ (i j : Fin n), Jreal i j ∈ J i j) (i j : Fin n) : (1 - (Y.map fun (q : ℚ) => ↑q) * Jreal) i j ∈ preconditionedJacobian Y J i j

def LeanCert.Engine.intervalAbsBound (I : Core.IntervalRat) : ℚ

Equations

• LeanCert.Engine.intervalAbsBound I = max |I.lo| |I.hi|

def LeanCert.Engine.intervalMatrixRowBound {n : ℕ} (A : Matrix (Fin n) (Fin n) Core.IntervalRat) (i : Fin n) : ℚ

Equations

• LeanCert.Engine.intervalMatrixRowBound A i = ∑ j : Fin n, LeanCert.Engine.intervalAbsBound (A i j)

def LeanCert.Engine.intervalMatrixBound {n : ℕ} (A : Matrix (Fin n) (Fin n) Core.IntervalRat) : ℚ

Equations

• LeanCert.Engine.intervalMatrixBound A = List.foldl max 0 (List.ofFn fun (i : Fin n) => LeanCert.Engine.intervalMatrixRowBound A i)

theorem LeanCert.Engine.abs_le_intervalAbsBound {x : ℝ} {I : Core.IntervalRat} (hx : x ∈ I) : |x| ≤ ↑(intervalAbsBound I)

theorem LeanCert.Engine.intervalMatrixRowBound_le_bound {n : ℕ} (A : Matrix (Fin n) (Fin n) Core.IntervalRat) (i : Fin n) : intervalMatrixRowBound A i ≤ intervalMatrixBound A

theorem LeanCert.Engine.matrix_norm_le_intervalMatrixBound {n : ℕ} (R : Matrix (Fin n) (Fin n) ℝ) (A : Matrix (Fin n) (Fin n) Core.IntervalRat) (hmem : ∀ (i j : Fin n), R i j ∈ A i j) : ‖R‖ ≤ ↑(intervalMatrixBound A)

theorem LeanCert.Engine.newtonMap_fderiv_norm_le {n : ℕ} (Y : Matrix (Fin n) (Fin n) ℚ) (F : Fin n → Core.Expr) (h : ∀ (i : Fin n), ADSupported (F i)) (X : Fin n → Core.IntervalRat) (x : Fin n → ℝ) (hx : FinBoxMem x X) (cfg : EvalConfig) : ‖fderiv ℝ (newtonMap (Y.map fun (q : ℚ) => ↑q) F) x‖ ≤ ↑(intervalMatrixBound (preconditionedJacobian Y (intervalJacobian F X cfg)))

def LeanCert.Engine.pointIntervalEnv {n : ℕ} (m : Fin n → ℚ) : IntervalEnv

Equations

• LeanCert.Engine.pointIntervalEnv m i = if h : i < n then LeanCert.Core.IntervalRat.singleton (m ⟨i, h⟩) else LeanCert.Core.IntervalRat.singleton 0

def LeanCert.Engine.pointEvalIntervals {n : ℕ} (F : Fin n → Core.Expr) (m : Fin n → ℚ) (cfg : EvalConfig := { }) : Fin n → Core.IntervalRat

Equations

• LeanCert.Engine.pointEvalIntervals F m cfg i = LeanCert.Internal.Rational.evalTotalCore (F i) (LeanCert.Engine.pointIntervalEnv m) cfg

def LeanCert.Engine.intervalRatMatVec {n : ℕ} (Y : Matrix (Fin n) (Fin n) ℚ) (v : Fin n → Core.IntervalRat) : Fin n → Core.IntervalRat

Equations

• LeanCert.Engine.intervalRatMatVec Y v i = ∑ j : Fin n, LeanCert.Core.IntervalRat.scale (Y i j) (v j)

def LeanCert.Engine.newtonCenterInterval {n : ℕ} (F : Fin n → Core.Expr) (m : Fin n → ℚ) (Y : Matrix (Fin n) (Fin n) ℚ) (cfg : EvalConfig := { }) : Fin n → Core.IntervalRat

Equations

• LeanCert.Engine.newtonCenterInterval F m Y cfg i = (LeanCert.Core.IntervalRat.singleton (m i)).sub (LeanCert.Engine.intervalRatMatVec Y (LeanCert.Engine.pointEvalIntervals F m cfg) i)

theorem LeanCert.Engine.finEnv_ratCast_mem_pointIntervalEnv {n : ℕ} (m : Fin n → ℚ) (i : ℕ) : finEnv (fun (j : Fin n) => ↑(m j)) i ∈ pointIntervalEnv m i

theorem LeanCert.Engine.systemEval_mem_pointEvalIntervals {n : ℕ} (F : Fin n → Core.Expr) (h : ∀ (i : Fin n), ADSupported (F i)) (m : Fin n → ℚ) (cfg : EvalConfig) (i : Fin n) : systemEval F (fun (j : Fin n) => ↑(m j)) i ∈ pointEvalIntervals F m cfg i

theorem LeanCert.Engine.newtonMap_center_mem {n : ℕ} (F : Fin n → Core.Expr) (h : ∀ (i : Fin n), ADSupported (F i)) (m : Fin n → ℚ) (Y : Matrix (Fin n) (Fin n) ℚ) (cfg : EvalConfig) (i : Fin n) : newtonMap (Y.map fun (q : ℚ) => ↑q) F (fun (j : Fin n) => ↑(m j)) i ∈ newtonCenterInterval F m Y cfg i

def LeanCert.Engine.coordinateRadius {n : ℕ} (X : Fin n → Core.IntervalRat) (m : Fin n → ℚ) (i : Fin n) : ℚ

Equations

• LeanCert.Engine.coordinateRadius X m i = max (m i - (X i).lo) ((X i).hi - m i)

def LeanCert.Engine.boxRadius {n : ℕ} (X : Fin n → Core.IntervalRat) (m : Fin n → ℚ) : ℚ

Equations

• LeanCert.Engine.boxRadius X m = List.foldl max 0 (List.ofFn fun (i : Fin n) => LeanCert.Engine.coordinateRadius X m i)

theorem LeanCert.Engine.coordinateRadius_le_boxRadius {n : ℕ} (X : Fin n → Core.IntervalRat) (m : Fin n → ℚ) (i : Fin n) : coordinateRadius X m i ≤ boxRadius X m

theorem LeanCert.Engine.abs_sub_center_le_coordinateRadius {n : ℕ} {X : Fin n → Core.IntervalRat} {m : Fin n → ℚ} {x : Fin n → ℝ} (hx : FinBoxMem x X) (i : Fin n) : |x i - ↑(m i)| ≤ ↑(coordinateRadius X m i)

theorem LeanCert.Engine.boxRadius_nonneg {n : ℕ} (X : Fin n → Core.IntervalRat) (m : Fin n → ℚ) : 0 ≤ boxRadius X m

theorem LeanCert.Engine.norm_sub_center_le_boxRadius {n : ℕ} {X : Fin n → Core.IntervalRat} {m : Fin n → ℚ} {x : Fin n → ℝ} (hx : FinBoxMem x X) : ‖x - fun (i : Fin n) => ↑(m i)‖ ≤ ↑(boxRadius X m)

def LeanCert.Engine.symmetricInterval (d : ℚ) : Core.IntervalRat

Equations

• LeanCert.Engine.symmetricInterval d = { lo := -|d|, hi := |d|, le := ⋯ }

def LeanCert.Engine.newtonImageEnclosure {n : ℕ} (F : Fin n → Core.Expr) (X : Fin n → Core.IntervalRat) (m : Fin n → ℚ) (Y : Matrix (Fin n) (Fin n) ℚ) (cfg : EvalConfig := { }) : Fin n → Core.IntervalRat

Equations

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

def LeanCert.Engine.intervalStrictInside (I X : Core.IntervalRat) : Bool

Equations

• LeanCert.Engine.intervalStrictInside I X = (decide (X.lo < I.lo) && decide (I.hi < X.hi))

theorem LeanCert.Engine.intervalStrictInside_sound {I X : Core.IntervalRat} (h : intervalStrictInside I X = true) (x : ℝ) : x ∈ I → x ∈ X

theorem LeanCert.Engine.newtonMap_mapsTo_of_imageEnclosure {n : ℕ} (F : Fin n → Core.Expr) (h : ∀ (i : Fin n), ADSupported (F i)) (X : Fin n → Core.IntervalRat) (m : Fin n → ℚ) (hm : FinBoxMem (fun (i : Fin n) => ↑(m i)) X) (Y : Matrix (Fin n) (Fin n) ℚ) (cfg : EvalConfig) (hencl : ∀ (i : Fin n), intervalStrictInside (newtonImageEnclosure F X m Y cfg i) (X i) = true) : Set.MapsTo (newtonMap (Y.map fun (q : ℚ) => ↑q) F) (finBoxSet X) (finBoxSet X)

structure LeanCert.Engine.KrawczykCert (n : ℕ) : Type

• center : Fin n → ℚ
• preconditioner : Matrix (Fin n) (Fin n) ℚ

def LeanCert.Engine.centerInside {n : ℕ} (X : Fin n → Core.IntervalRat) (m : Fin n → ℚ) : Prop

Equations

• LeanCert.Engine.centerInside X m = ∀ (i : Fin n), (X i).lo ≤ m i ∧ m i ≤ (X i).hi

@[instance_reducible]

instance LeanCert.Engine.instDecidableCenterInside {n : ℕ} (X : Fin n → Core.IntervalRat) (m : Fin n → ℚ) : Decidable (centerInside X m)

Equations

• LeanCert.Engine.instDecidableCenterInside X m = id inferInstance

def LeanCert.Engine.krawczykCheck {n : ℕ} (F : Fin n → Core.Expr) (X : Fin n → Core.IntervalRat) (cert : KrawczykCert n) (cfg : EvalConfig := { }) : Bool

Equations

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

def LeanCert.Engine.SystemZero {n : ℕ} (F : Fin n → Core.Expr) (x : Fin n → ℝ) : Prop

Equations

• LeanCert.Engine.SystemZero F x = ∀ (i : Fin n), LeanCert.Engine.evalFin (F i) x = 0

theorem LeanCert.Engine.centerInside_sound {n : ℕ} {X : Fin n → Core.IntervalRat} {m : Fin n → ℚ} (h : centerInside X m) : FinBoxMem (fun (i : Fin n) => ↑(m i)) X

theorem LeanCert.Engine.fixedPoint_iff_systemZero {n : ℕ} (F : Fin n → Core.Expr) (Y : Matrix (Fin n) (Fin n) ℚ) (hdet : Y.det ≠ 0) (x : Fin n → ℝ) : newtonMap (Y.map fun (q : ℚ) => ↑q) F x = x ↔ SystemZero F x

theorem LeanCert.Engine.krawczykCheck_sound {n : ℕ} (F : Fin n → Core.Expr) (X : Fin n → Core.IntervalRat) (cert : KrawczykCert n) (cfg : EvalConfig) (hcheck : krawczykCheck F X cert cfg = true) : ∃! x : Fin n → ℝ, FinBoxMem x X ∧ SystemZero F x