Documentation

LeanCert.Validity.Bernstein

Golden theorems for Bernstein polynomial certificates #

checkPolyLowerBound e I c depth recognises e as a univariate rational polynomial (QPoly.ofExpr) and runs the recursive Bernstein certificate QPoly.bernsteinCheck. Recognition doubles as the support proof, so the golden theorems need no ExprSupportedCore premise. All theorems here are kernel-clean; the checker itself may be closed by kernel or native evaluation.

source
def LeanCert.Validity.Bernstein.checkPolyBound (cmp : Engine.QPoly.Cmp) (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) (depth : ℕ) :
Bool

Generic Bernstein checker over reified expressions.

Equations
Instances For
    source
    def LeanCert.Validity.Bernstein.checkPolyLowerBound (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) (depth : ℕ) :
    Bool

    ∀ x ∈ I, c ≤ e x by Bernstein coefficients.

    Equations
    Instances For
      source
      def LeanCert.Validity.Bernstein.checkPolyUpperBound (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) (depth : ℕ) :
      Bool

      ∀ x ∈ I, e x ≤ c by Bernstein coefficients.

      Equations
      Instances For
        source
        def LeanCert.Validity.Bernstein.checkPolyStrictLowerBound (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) (depth : ℕ) :
        Bool

        ∀ x ∈ I, c < e x by Bernstein coefficients.

        Equations
        Instances For
          source
          def LeanCert.Validity.Bernstein.checkPolyStrictUpperBound (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) (depth : ℕ) :
          Bool

          ∀ x ∈ I, e x < c by Bernstein coefficients.

          Equations
          Instances For
            source
            def LeanCert.Validity.Bernstein.isPolynomial (e : Core.Expr) :
            Bool

            Does QPoly.ofExpr recognise e? Used by tactics to decide applicability without spending budget.

            Equations
            Instances For
              source
              theorem LeanCert.Validity.Bernstein.verify_poly_bound (cmp : Engine.QPoly.Cmp) (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) (depth : ℕ) (h : checkPolyBound cmp e I c depth = true) (x : ℝ) :
              x ∈ I → cmp.holds (↑c) (Core.Expr.eval (fun (x_1 : ℕ) => x) e)
              source
              theorem LeanCert.Validity.Bernstein.verify_poly_lower_bound (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) (depth : ℕ) (h : checkPolyLowerBound e I c depth = true) (x : ℝ) :
              x ∈ I → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

              Golden theorem (lower bound).

              source
              theorem LeanCert.Validity.Bernstein.verify_poly_upper_bound (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) (depth : ℕ) (h : checkPolyUpperBound e I c depth = true) (x : ℝ) :
              x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

              Golden theorem (upper bound).

              source
              theorem LeanCert.Validity.Bernstein.verify_poly_strict_lower_bound (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) (depth : ℕ) (h : checkPolyStrictLowerBound e I c depth = true) (x : ℝ) :
              x ∈ I → ↑c < Core.Expr.eval (fun (x_1 : ℕ) => x) e

              Golden theorem (strict lower bound).

              source
              theorem LeanCert.Validity.Bernstein.verify_poly_strict_upper_bound (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) (depth : ℕ) (h : checkPolyStrictUpperBound e I c depth = true) (x : ℝ) :
              x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e < ↑c

              Golden theorem (strict upper bound).

              Set.Icc bridges #

              source
              theorem LeanCert.Validity.Bernstein.verify_poly_lower_bound_Icc (e : Core.Expr) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (depth : ℕ) (h : checkPolyLowerBound e { lo := lo, hi := hi, le := hle } c depth = true) (x : ℝ) :
              x ∈ Set.Icc ↑lo ↑hi → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e
              source
              theorem LeanCert.Validity.Bernstein.verify_poly_upper_bound_Icc (e : Core.Expr) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (depth : ℕ) (h : checkPolyUpperBound e { lo := lo, hi := hi, le := hle } c depth = true) (x : ℝ) :
              x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c
              source
              theorem LeanCert.Validity.Bernstein.verify_poly_strict_lower_bound_Icc (e : Core.Expr) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (depth : ℕ) (h : checkPolyStrictLowerBound e { lo := lo, hi := hi, le := hle } c depth = true) (x : ℝ) :
              x ∈ Set.Icc ↑lo ↑hi → ↑c < Core.Expr.eval (fun (x_1 : ℕ) => x) e
              source
              theorem LeanCert.Validity.Bernstein.verify_poly_strict_upper_bound_Icc (e : Core.Expr) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (depth : ℕ) (h : checkPolyStrictUpperBound e { lo := lo, hi := hi, le := hle } c depth = true) (x : ℝ) :
              x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e < ↑c