Sound interval evaluation of real expressions

Each backend operation must enclose its real result for every real member of the input intervals. Structural induction then gives the same guarantee for a complete expression. The theorem does not restrict variable values to rationals or to the interval's endpoint representation.

def FloatLib.Numerics.Interval.RealFunction : ℕ → Type

Curried real functions; arity zero is a real constant.

noncomputable def FloatLib.Numerics.Interval.RealFunction.apply {n : ℕ} (f : RealFunction n) (args : List ℝ) : ℝ

Apply a curried real function to its argument list. Successful extension evaluation checks the arity before this interpretation is used.

def FloatLib.Numerics.Interval.Extension.Sound (E : Extension) (f : RealFunction E.arity) : Prop

A successful user enclosure contains the result for every real input member. The argument count is checked by the common evaluator, independently of the user's procedure.

theorem FloatLib.Numerics.Interval.Extension.constant_sound (bounds : Backend.Config → Option (Interval ℚ)) (c : ℝ) (h : ∀ (config : Backend.Config) (output : Interval ℚ), bounds config = some output → ContainsReal some output c) : (constant bounds).Sound c

A certified constant enclosure satisfies the common extension contract.

structure FloatLib.Numerics.Interval.ConstantBounds (c : ℝ) : Type

Rational lower and upper bounds for a real constant, indexed by requested precision.

• bounds : ℕ → Interval ℚ

  Compute the lower and upper endpoints.

• valid (precision : ℕ) : ↑(self.bounds precision).lo ≤ c ∧ c ≤ ↑(self.bounds precision).hi

  The constant lies between those endpoints at every precision.

def FloatLib.Numerics.Interval.ConstantBounds.toExtension {c : ℝ} (certificate : ConstantBounds c) : Extension

Adapt proved constant bounds to the general enclosure evaluator.

theorem FloatLib.Numerics.Interval.ConstantBounds.toExtension_sound {c : ℝ} (certificate : ConstantBounds c) : certificate.toExtension.Sound c

Ordinary endpoint inequalities suffice to certify a constant enclosure.

theorem FloatLib.Numerics.Interval.Extension.unary_sound (bounds : Backend.Config → Interval ℚ → Option (Interval ℚ)) (f : ℝ → ℝ) (h : ∀ (config : Backend.Config) (I J : Interval ℚ) (x : ℝ), bounds config I = some J → ContainsReal some I x → ContainsReal some J (f x)) : (unary bounds).Sound f

Lift an existing unary containment theorem to a registered enclosure.

theorem FloatLib.Numerics.Interval.Extension.binary_sound (bounds : Backend.Config → Interval ℚ → Interval ℚ → Option (Interval ℚ)) (f : ℝ → ℝ → ℝ) (h : ∀ (config : Backend.Config) (I J K : Interval ℚ) (x y : ℝ), bounds config I J = some K → ContainsReal some I x → ContainsReal some J y → ContainsReal some K (f x y)) : (binary bounds).Sound f

Lift an existing binary containment theorem to a registered enclosure.

noncomputable def FloatLib.Numerics.Interval.UnaryOp.eval : UnaryOp → ℝ → ℝ

Real interpretation of a unary expression operation.

noncomputable def FloatLib.Numerics.Interval.BinaryOp.eval : BinaryOp → ℝ → ℝ → ℝ

Real interpretation of a binary expression operation.

noncomputable def FloatLib.Numerics.Interval.TernaryOp.eval : TernaryOp → ℝ → ℝ → ℝ → ℝ

Real interpretation of a three-input expression operation.

noncomputable def FloatLib.Numerics.Interval.Expr.eval (e : Expr) (env : ℕ → ℝ) (functions : ℕ → List ℝ → ℝ := fun (x : ℕ) (x_1 : List ℝ) => 0) : ℝ

Evaluate an expression at arbitrary real variable values.

noncomputable def FloatLib.Numerics.Interval.Expr.evalArgs (args : List Expr) (env : ℕ → ℝ) (functions : ℕ → List ℝ → ℝ) : List ℝ

Real interpretation of the ordered arguments of a registered call.

structure FloatLib.Numerics.Interval.Backend.Sound {α : Type u_1} (B : Backend α) (functions : ℕ → List ℝ → ℝ := fun (x : ℕ) (x_1 : List ℝ) => 0) : Prop

Containment contracts for all successful operations of an interval backend.

• const {q : ℚ} {I : Interval α} : B.const? q = some I → ContainsReal B.decode I ↑q

  The constant enclosure contains its exact rational value.

• unary {op : UnaryOp} {I J : Interval α} {x : ℝ} : B.unary? op I = some J → ContainsReal B.decode I x → ContainsReal B.decode J (op.eval x)

  Unary operations enclose the result at every real input member.

• binary {op : BinaryOp} {I J K : Interval α} {x y : ℝ} : B.binary? op I J = some K → ContainsReal B.decode I x → ContainsReal B.decode J y → ContainsReal B.decode K (op.eval x y)

  Binary operations enclose the result at every pair of real input members.

• ternary {op : TernaryOp} {I J K L : Interval α} {x y z : ℝ} : B.ternary? op I J K = some L → ContainsReal B.decode I x → ContainsReal B.decode J y → ContainsReal B.decode K z → ContainsReal B.decode L (op.eval x y z)

  Three-input operations enclose the result at every combination of real input members.

• call {index : ℕ} {inputs : List (Interval α)} {output : Interval α} {values : List ℝ} : B.call? index inputs = some output → List.Forall₂ (fun (I : Interval α) (x : ℝ) => ContainsReal B.decode I x) inputs values → ContainsReal B.decode output (functions index values)

  Registered operations enclose all real tuples in their input intervals.

theorem FloatLib.Numerics.Interval.Expr.containsReal_eval? {α : Type u_1} (e : Expr) {B : Backend α} {functions : ℕ → List ℝ → ℝ} (hB : B.Sound functions) {env : ℕ → Option (Interval α)} {values : ℕ → ℝ} (henv : ∀ (i : ℕ) (I : Interval α), env i = some I → ContainsReal B.decode I (values i)) {I : Interval α} (h : e.eval? B env = some I) : ContainsReal B.decode I (e.eval values functions)

A successful expression evaluation encloses the exact real value throughout the input box.

Only variables actually supplied by the interval environment need a membership proof. A missing variable prevents successful evaluation, so it cannot create an unproved assumption.