Documentation

LeanPool.MovingSofa.Development.IntervalArithmetic.Foundations.Development001

Moving sofa: related mathematical developments #

Differentiability of sinc and dslope #

This file proves that the sinc function is differentiable everywhere, including at 0.

Main results #

Mathematical background #

The sinc function is defined as:

Equivalently, sinc = dslope sin 0.

The derivative of sinc at 0 can be computed using Taylor expansion:

theorem Real.abs_sin_sub_self_le (x : ℝ) (_hx : |x| ≤ 1) :
|sin x - x| ≤ |x| ^ 3 / 4

Bound on |sin x - x| in terms of |x|³. For x > 0: sin x < x and x - x³/4 < sin x, so 0 < x - sin x < x³/4. By symmetry (sin(-x) = -sin(x)), |sin x - x| ≤ |x|³/4 for all x with |x| ≤ 1.

The derivative of sinc at 0 is 0.

The proof uses the squeeze theorem with the bound |sinc x - 1| ≤ |x|² / 4, which follows from sin bounds in Mathlib.

sinc is differentiable everywhere.

sinc is a differentiable function.

theorem Real.sinc_eq_integral_cos (x : ℝ) :
sinc x = ∫ (t : ℝ) in 0..1, cos (x * t)

Integral representation of sinc: sinc x = ∫ t in 0..1, cos (x * t). This is the standard average-cosine form used for derivative bounds.

theorem Real.hasDerivAt_sinc_of_ne_zero {x : ℝ} (hx : x ≠ 0) :
HasDerivAt sinc ((x * cos x - sin x) / x ^ 2) x

The derivative of sinc at a nonzero point.

theorem Real.deriv_sinc {x : ℝ} :
deriv sinc x = if x = 0 then 0 else (x * cos x - sin x) / x ^ 2

The derivative of sinc. For x = 0, deriv sinc 0 = 0. For x ≠ 0, deriv sinc x = (x cos x - sin x) / x².

@[simp]

Bound: |x cos x - sin x| ≤ x² for all x. Proof uses monotonicity of auxiliary functions on [0, ∞).

deriv sinc x is in [-1, 1] for all x

Integral representation and smoothness of sinc #

The sinc function is smooth (C^∞). The key insight is the integral representation: sinc(x) = ∫ t in 0..1, cos(t * x) dt

This works because:

Smoothness follows from differentiation under the integral sign (Leibniz rule): since cos(t*x) is C^∞ in x and the domain [0,1] is compact, the integral is C^∞.

theorem Real.sinc_eq_integral (x : ℝ) :
sinc x = ∫ (t : ℝ) in 0..1, cos (t * x)

The integral representation of sinc: sinc(x) = ∫ t in 0..1, cos(t * x)

The derivative of sinc equals dslope (cos - sinc) at 0.

For x ≠ 0: dslope (cos - sinc) 0 x = (cos x - sinc x) / x = (x cos x - sin x) / x² = deriv sinc x

For x = 0: dslope (cos - sinc) 0 0 = deriv (cos - sinc) 0 = -sin 0 - deriv sinc 0 = 0 = deriv sinc 0

sinc is smooth at every nonzero point.

sinc is analytic at 0.

The proof uses the order theory of analytic functions. Since sin is analytic at 0 with order ≥ 1 (because sin(0) = 0), there exists an analytic function g such that sin(z) = z • g(z) near 0. This g must equal sinc away from 0, and by continuity of both functions at 0, g = sinc everywhere near 0. Therefore sinc is analytic at 0.

sinc is analytic at every point.

sinc is smooth (infinitely differentiable).

The proof uses that sinc is analytic everywhere (analyticAt_sinc), and analytic functions are smooth.

sinc is an analytic function.

Derivative Interval Library #

This file provides a systematic collection of derivative interval facts for basic functions. These lemmas establish that derivatives of common functions lie within specified intervals, which feeds into:

Main theorems #

Exp (derivative = exp, always positive) #

Log (derivative = 1/x on (0, ∞)) #

Arctan (derivative = 1/(1+x²) ∈ (0, 1]) #

Arsinh (derivative = 1/√(1+x²) ∈ (0, 1]) #

Sin/Cos (derivatives bounded by 1) #

Sinh/Cosh (derivative relationships) #

Design notes #

These lemmas are independent of any specific algorithm; they're just facts about functions. They're designed to be composable with the chain rule for AD correctness proofs.

Exp derivative intervals #

The derivative of exp is positive everywhere

exp is strictly increasing (follows from positive derivative)

For x ∈ [a, b], we have exp' x = exp x ∈ [exp a, exp b]

Log derivative intervals #

The derivative of log at x > 0 is x⁻¹

For x ∈ [a, b] with 0 < a ≤ b, we have log' x = 1/x ∈ [1/b, 1/a]

Arctan derivative intervals #

The derivative of arctan at x is 1/(1+x²)

1/(1+x²) is always positive

arctan' x ∈ [0, 1] for all x (closed interval version for interval arithmetic)

arctan is strictly increasing (follows from positive derivative)

Arsinh derivative intervals #

The derivative of arsinh at x is (√(1+x²))⁻¹

√(1+x²) ≥ 1 for all x

√(1+x²) > 0 for all x

arsinh' x ∈ [0, 1] for all x (closed interval version)

Sin derivative intervals #

The derivative of sin is cos

sin' x ∈ [-1, 1] for all x

Cos derivative intervals #

The derivative of cos is -sin

cos' x ∈ [-1, 1] for all x

Sinh derivative intervals #

The derivative of sinh is cosh

sinh' x = cosh x ≥ 1 for all x

Cosh derivative intervals #

The derivative of cosh is sinh

For x > 0, cosh' x = sinh x > 0

For x < 0, cosh' x = sinh x < 0

One-Sided Taylor Bounds #

For convex functions, the Taylor polynomial provides a one-sided bound. For exp on [0, ∞), the n-th Taylor polynomial is a lower bound. For concave functions, similar upper bounds hold.

These bounds are tighter than symmetric remainder bounds at endpoints, which is important for verified numerics.

Exp lower bounds (convexity gives Taylor poly ≤ function) #

1 ≤ exp x for x ≥ 0 (Taylor degree 0)

1 + x ≤ exp x for all x (Taylor degree 1)

x + 1 ≤ exp x for all x (alternate form)

Monotonicity from derivative bounds #

These wrap the Mathlib lemmas for convenience with our naming.

theorem LeanCert.Core.OneSidedTaylor.monotoneOn_of_deriv_nonneg {f : ℝ → ℝ} {a b : ℝ} (hf : ContinuousOn f (Set.Icc a b)) (hf' : DifferentiableOn ℝ f (Set.Ioo a b)) (hderiv : ∀ x ∈ Set.Ioo a b, 0 ≤ deriv f x) :

If f' ≥ 0 on [a, b], then f is monotone increasing on [a, b]

theorem LeanCert.Core.OneSidedTaylor.strictMonoOn_of_deriv_pos {f : ℝ → ℝ} {a b : ℝ} (_hab : a < b) (hf : ContinuousOn f (Set.Icc a b)) (_hf' : DifferentiableOn ℝ f (Set.Ioo a b)) (hderiv : ∀ x ∈ Set.Ioo a b, 0 < deriv f x) :

If f' > 0 on (a, b), then f is strictly monotone on [a, b]

theorem LeanCert.Core.OneSidedTaylor.antitoneOn_of_deriv_nonpos {f : ℝ → ℝ} {a b : ℝ} (hf : ContinuousOn f (Set.Icc a b)) (hf' : DifferentiableOn ℝ f (Set.Ioo a b)) (hderiv : ∀ x ∈ Set.Ioo a b, deriv f x ≤ 0) :

If f' ≤ 0 on [a, b], then f is antitone (monotone decreasing) on [a, b]

theorem LeanCert.Core.OneSidedTaylor.strictAntiOn_of_deriv_neg {f : ℝ → ℝ} {a b : ℝ} (_hab : a < b) (hf : ContinuousOn f (Set.Icc a b)) (_hf' : DifferentiableOn ℝ f (Set.Ioo a b)) (hderiv : ∀ x ∈ Set.Ioo a b, deriv f x < 0) :

If f' < 0 on (a, b), then f is strictly antitone on [a, b]

Dyadic Rationals (n * 2^e) #

This file defines Dyadic rationals, which are the backbone of high-performance verified numerics. Unlike arbitrary Rat, Dyadics do not require GCD normalization, making them significantly faster for kernel evaluation.

Main definitions #

Design notes #

Dyadics use power-of-2 multiplications instead of GCD-based normalization. This makes them orders of magnitude faster for kernel evaluation via native_decide, since 2^n can be computed by simple bit operations.

For interval arithmetic, we use directed rounding:

This ensures mathematical soundness even when truncating precision.

A Dyadic rational number: mantissa * 2^exponent

This representation allows fast arithmetic without GCD normalization.

  • mantissa : ℤ

    The significand/mantissa

  • exponent : ℤ

    The exponent (power of 2)

Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def LeanCert.Core.instDecidableEqDyadic.decEq (x✝ x✝¹ : Dyadic) :
      Decidable (x✝ = x✝¹)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Helper: Power of 2 #

        Compute 2^n for natural n

        Equations
        Instances For

          Shift an integer left by n bits (multiply by 2^n)

          Equations
          Instances For

            Shift an integer right by n bits (divide by 2^n, floor toward -∞)

            Equations
            Instances For

              Check if any of the low n bits are set

              Equations
              Instances For

                Conversion to Rat #

                Convert Dyadic to standard Rat.

                For non-negative exponents: mantissa * 2^exponent For negative exponents: mantissa / 2^(-exponent)

                Equations
                Instances For

                  Equality of represented values, ignoring noncanonical mantissa/exponent pairs.

                  Equations
                  Instances For
                    @[instance_reducible]
                    Equations
                    @[simp]
                    theorem LeanCert.Core.Dyadic.valueEq_iff (d₁ d₂ : Dyadic) :
                    d₁.ValueEq d₂ ↔ d₁.toRat = d₂.toRat

                    A lawful identity key for caches, sets, serialization, and deduplication.

                    Arithmetic keeps the fast, noncanonical Dyadic representation. Converting at an identity boundary collapses all representations of the same rational value.

                    • value : ℚ

                      The exact rational value used to compare normalized dyadic numbers.

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

                          Convert a dyadic value to its canonical identity key.

                          Equations
                          Instances For

                            Canonical keys agree exactly when represented dyadic values agree.

                            Cast a Dyadic to ℝ by going through ℚ

                            Equations
                            Instances For
                              theorem LeanCert.Core.Dyadic.valueEq_of_toRat_eq {d₁ d₂ : Dyadic} (h : d₁.toRat = d₂.toRat) :
                              d₁.ValueEq d₂

                              Equality of rational denotations gives semantic dyadic equality.

                              Construction #

                              Create a dyadic from an integer (exponent = 0)

                              Equations
                              Instances For

                                Create a dyadic for 2^n

                                Equations
                                Instances For

                                  Zero as a Dyadic

                                  Equations
                                  Instances For

                                    One as a Dyadic

                                    Equations
                                    Instances For

                                      Arithmetic Operations #

                                      Negation of a Dyadic

                                      Equations
                                      Instances For

                                        Addition of Dyadics. Aligns exponents by shifting the mantissa with larger exponent to match the smaller one.

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

                                          Subtraction of Dyadics

                                          Equations
                                          Instances For

                                            Multiplication of Dyadics. Simply multiplies mantissas and adds exponents.

                                            Equations
                                            Instances For

                                              Absolute value of a Dyadic

                                              Equations
                                              Instances For

                                                Scale by a power of 2 (efficient: just adjusts exponent)

                                                Equations
                                                Instances For

                                                  Directed Rounding for Interval Arithmetic #

                                                  Shift a dyadic to a new (larger) exponent with "Down" rounding (for lower bounds).

                                                  If newExp > d.exponent, we lose precision by right-shifting the mantissa. Bits are discarded (floor division toward -∞).

                                                  Equations
                                                  Instances For

                                                    Shift a dyadic to a new (larger) exponent with "Up" rounding (for upper bounds).

                                                    If newExp > d.exponent, we lose precision by right-shifting the mantissa. If any bits are lost, we add 1 to ensure upward rounding (ceiling toward +∞).

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

                                                      Normalization (Mantissa Control) #

                                                      Get the bit length of a natural number

                                                      Equations
                                                      Instances For

                                                        Get the bit length of the absolute value of an integer

                                                        Equations
                                                        Instances For
                                                          def LeanCert.Core.Dyadic.normalize (d : Dyadic) (maxBits : ℕ := 256) (roundUp : Bool := false) :

                                                          Normalize a Dyadic to keep the mantissa within a reasonable bit-limit.

                                                          This prevents mantissas from growing without bound during repeated multiplications. Similar to how hardware floats work, but with directed rounding.

                                                          • maxBits: Maximum allowed bits for mantissa (default 256)
                                                          • roundUp: If true, round toward +∞; if false, round toward -∞
                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            def LeanCert.Core.Dyadic.normalizeDown (d : Dyadic) (maxBits : ℕ := 256) :

                                                            Normalize for lower bounds (round down)

                                                            Equations
                                                            Instances For
                                                              def LeanCert.Core.Dyadic.normalizeUp (d : Dyadic) (maxBits : ℕ := 256) :

                                                              Normalize for upper bounds (round up)

                                                              Equations
                                                              Instances For

                                                                Comparison #

                                                                Compare two Dyadics (decidable)

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

                                                                  Less-than-or-equal for Dyadics

                                                                  Equations
                                                                  Instances For

                                                                    Less-than for Dyadics

                                                                    Equations
                                                                    Instances For
                                                                      @[instance_reducible]
                                                                      Equations
                                                                      @[instance_reducible]
                                                                      Equations
                                                                      @[instance_reducible]
                                                                      Equations
                                                                      @[instance_reducible]
                                                                      Equations

                                                                      Minimum of two Dyadics

                                                                      Equations
                                                                      Instances For

                                                                        Maximum of two Dyadics

                                                                        Equations
                                                                        Instances For

                                                                          Minimum of four Dyadics

                                                                          Equations
                                                                          Instances For

                                                                            Maximum of four Dyadics

                                                                            Equations
                                                                            Instances For

                                                                              Correctness Theorems #

                                                                              Helper lemmas for shift proofs #

                                                                              Arithmetic Homomorphisms #

                                                                              Unification lemma: toRat d = d.mantissa * 2^d.exponent

                                                                              theorem LeanCert.Core.Dyadic.toRat_add (d₁ d₂ : Dyadic) :
                                                                              (d₁.add d₂).toRat = d₁.toRat + d₂.toRat
                                                                              theorem LeanCert.Core.Dyadic.toRat_mul (d₁ d₂ : Dyadic) :
                                                                              (d₁.mul d₂).toRat = d₁.toRat * d₂.toRat

                                                                              Rounding Properties #

                                                                              shiftDown produces a value ≤ the original

                                                                              theorem LeanCert.Core.Dyadic.toRat_shiftUp_ge (d : Dyadic) (newExp : ℤ) :
                                                                              d.toRat ≤ (d.shiftUp newExp).toRat

                                                                              shiftUp produces a value ≥ the original

                                                                              Comparison Helper Lemmas #

                                                                              Comparison Theorems #

                                                                              theorem LeanCert.Core.Dyadic.le_iff_toRat_le (d₁ d₂ : Dyadic) :
                                                                              d₁.le d₂ = true ↔ d₁.toRat ≤ d₂.toRat

                                                                              le is correct with respect to toRat ordering

                                                                              theorem LeanCert.Core.Dyadic.compare_lt_iff (d₁ d₂ : Dyadic) :
                                                                              d₁.compare d₂ = Ordering.lt ↔ d₁.toRat < d₂.toRat

                                                                              compare reflects toRat ordering: lt case

                                                                              theorem LeanCert.Core.Dyadic.compare_gt_iff (d₁ d₂ : Dyadic) :
                                                                              d₁.compare d₂ = Ordering.gt ↔ d₁.toRat > d₂.toRat

                                                                              compare reflects toRat ordering: gt case

                                                                              theorem LeanCert.Core.Dyadic.compare_eq_iff (d₁ d₂ : Dyadic) :
                                                                              d₁.compare d₂ = Ordering.eq ↔ d₁.toRat = d₂.toRat

                                                                              compare reflects toRat ordering: eq case

                                                                              Min/Max Lemmas #

                                                                              theorem LeanCert.Core.Dyadic.min_toRat_le_left (d₁ d₂ : Dyadic) :
                                                                              (d₁.min d₂).toRat ≤ d₁.toRat

                                                                              min produces value ≤ first argument

                                                                              theorem LeanCert.Core.Dyadic.min_toRat_le_right (d₁ d₂ : Dyadic) :
                                                                              (d₁.min d₂).toRat ≤ d₂.toRat

                                                                              min produces value ≤ second argument

                                                                              theorem LeanCert.Core.Dyadic.le_max_toRat_left (d₁ d₂ : Dyadic) :
                                                                              d₁.toRat ≤ (d₁.max d₂).toRat

                                                                              first argument ≤ max

                                                                              theorem LeanCert.Core.Dyadic.le_max_toRat_right (d₁ d₂ : Dyadic) :
                                                                              d₂.toRat ≤ (d₁.max d₂).toRat

                                                                              second argument ≤ max

                                                                              theorem LeanCert.Core.Dyadic.min_toRat (d₁ d₂ : Dyadic) :
                                                                              (d₁.min d₂).toRat = Min.min d₁.toRat d₂.toRat

                                                                              Dyadic.min commutes with toRat

                                                                              theorem LeanCert.Core.Dyadic.max_toRat (d₁ d₂ : Dyadic) :
                                                                              (d₁.max d₂).toRat = Max.max d₁.toRat d₂.toRat

                                                                              Dyadic.max commutes with toRat

                                                                              theorem LeanCert.Core.Dyadic.min4_le_max4 (a b c d : Dyadic) :
                                                                              (a.min4 b c d).toRat ≤ (a.max4 b c d).toRat

                                                                              min4 ≤ max4

                                                                              Normalize Lemmas #

                                                                              normalizeDown produces value ≤ original

                                                                              normalizeUp produces value ≥ original

                                                                              Scale2 Lemmas #

                                                                              theorem LeanCert.Core.Dyadic.toRat_scale2 (d : Dyadic) (n : ℤ) :
                                                                              (d.scale2 n).toRat = d.toRat * 2 ^ n

                                                                              scale2 multiplies by 2^n

                                                                              theorem LeanCert.Core.Dyadic.toRat_scale2_le_scale2 (d₁ d₂ : Dyadic) (n : ℤ) (h : d₁.toRat ≤ d₂.toRat) :
                                                                              (d₁.scale2 n).toRat ≤ (d₂.scale2 n).toRat

                                                                              scale2 preserves order

                                                                              Square Root Operations #

                                                                              Integer square root of a natural number. Satisfies: (intSqrtNat n)^2 ≤ n < (intSqrtNat n + 1)^2

                                                                              Equations
                                                                              Instances For

                                                                                Integer square root of a non-negative integer. Returns 0 for negative inputs.

                                                                                Equations
                                                                                Instances For
                                                                                  theorem LeanCert.Core.Dyadic.intSqrt_sq_le {n : ℤ} (hn : 0 ≤ n) :
                                                                                  intSqrt n ^ 2 ≤ n

                                                                                  intSqrt n ^ 2 ≤ n for n ≥ 0

                                                                                  theorem LeanCert.Core.Dyadic.int_lt_succ_sqrt_sq {n : ℤ} (hn : 0 ≤ n) :
                                                                                  n < (intSqrt n + 1) ^ 2

                                                                                  n < (intSqrt n + 1) ^ 2 for n ≥ 0

                                                                                  theorem LeanCert.Core.Dyadic.intSqrt_nonneg {n : ℤ} (hn : 0 ≤ n) :

                                                                                  intSqrt is nonnegative for nonnegative inputs

                                                                                  Compute sqrt(d) with a target exponent prec. Returns a Dyadic with exponent prec such that result ≤ sqrt(d).

                                                                                  For d = m * 2^e, we compute:

                                                                                  • shift = e - 2*prec (to align for sqrt)
                                                                                  • m' = m * 2^shift (or m / 2^(-shift) if shift < 0)
                                                                                  • result = floor(sqrt(m')) * 2^prec

                                                                                  This ensures: result.toRat ≤ sqrt(d.toRat)

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

                                                                                    Compute sqrt(d) rounded up with target exponent prec. Returns a Dyadic with exponent prec such that result ≥ sqrt(d).

                                                                                    Uses the same computation as sqrtDown, but if the result is not a perfect square, adds 1 to round up.

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

                                                                                      Sqrt Correctness Theorems #

                                                                                      theorem LeanCert.Core.Dyadic.sqrtDown_nonneg (d : Dyadic) (prec : ℤ) (hd : 0 ≤ d.mantissa) :
                                                                                      0 ≤ (d.sqrtDown prec).mantissa

                                                                                      sqrtDown is non-negative for non-negative inputs

                                                                                      theorem LeanCert.Core.Dyadic.sqrtUp_nonneg (d : Dyadic) (prec : ℤ) (hd : 0 ≤ d.mantissa) :
                                                                                      0 ≤ (d.sqrtUp prec).mantissa

                                                                                      sqrtUp is non-negative for non-negative inputs

                                                                                      theorem LeanCert.Core.Dyadic.sqrtDown_le_sqrtUp (d : Dyadic) (prec : ℤ) (hd : 0 ≤ d.mantissa) :
                                                                                      (d.sqrtDown prec).toRat ≤ (d.sqrtUp prec).toRat

                                                                                      sqrtDown.toRat ≤ sqrtUp.toRat for non-negative inputs

                                                                                      Unified Expression AST #

                                                                                      This file defines the unified AST for real expressions (Expr) and its evaluation semantics. All numerical algorithms in LeanCert operate on this single expression type.

                                                                                      Main definitions #

                                                                                      Design notes #

                                                                                      The expression type uses natural number indices for variables. This simplifies the interval evaluation and automatic differentiation implementations.

                                                                                      Auxiliary definition for atanh #

                                                                                      Since Mathlib doesn't provide Real.atanh, we define it here using the standard formula: atanh x = (1/2) * log((1+x)/(1-x)) for |x| < 1.

                                                                                      noncomputable def LeanCert.Core.Real.atanh (x : ℝ) :

                                                                                      The inverse hyperbolic tangent function. Defined as atanh x = (1/2) * log((1+x)/(1-x)) for |x| < 1.

                                                                                      Equations
                                                                                      Instances For
                                                                                        theorem LeanCert.Core.Real.atanh_arg_pos {x : ℝ} (hx : |x| < 1) :
                                                                                        0 < (1 + x) / (1 - x)

                                                                                        For |x| < 1, the argument (1+x)/(1-x) is positive.

                                                                                        @[simp]

                                                                                        atanh(0) = 0

                                                                                        theorem LeanCert.Core.Real.atanh_neg {x : ℝ} (hx : |x| < 1) :

                                                                                        atanh(-x) = -atanh(x) for |x| < 1

                                                                                        atanh is strictly monotone on (-1, 1)

                                                                                        theorem LeanCert.Core.Real.atanh_mono {x y : ℝ} (hx : |x| < 1) (hy : |y| < 1) (hxy : x ≤ y) :

                                                                                        atanh is monotone on (-1, 1): if x ≤ y then atanh x ≤ atanh y

                                                                                        noncomputable def LeanCert.Core.Real.erf (x : ℝ) :

                                                                                        The error function: erf(x) = (2/√π) ∫₀ˣ exp(-t²) dt. Essential for statistical and financial modeling (normal distribution CDF). Uses interval integral notation (∫ t in 0..x) which handles negative x correctly.

                                                                                        Equations
                                                                                        Instances For

                                                                                          The error function is bounded above by 1.

                                                                                          The error function is bounded below by -1.

                                                                                          The error function always lies in [-1, 1].

                                                                                          The normalized sinc function always lies in [-1, 1].

                                                                                          Named mathematical constants with known interval bounds. Adding a new constant (e.g., Catalan's) only requires extending this enum and its lookup tables — zero evaluator files need updating.

                                                                                          Instances For
                                                                                            Equations
                                                                                            • One or more equations did not get rendered due to their size.
                                                                                            Instances For
                                                                                              @[instance_reducible]
                                                                                              Equations

                                                                                              Float approximation for heuristic evaluation (unverified).

                                                                                              Equations
                                                                                              Instances For

                                                                                                Rational approximation for display/debugging (unverified).

                                                                                                Equations
                                                                                                Instances For

                                                                                                  Unified AST for real-valued expressions.

                                                                                                  • const (q : ℚ) : Expr

                                                                                                    Rational constant

                                                                                                  • var (idx : ℕ) : Expr

                                                                                                    Variable with de Bruijn-style index

                                                                                                  • add (e₁ e₂ : Expr) : Expr

                                                                                                    Addition

                                                                                                  • mul (e₁ e₂ : Expr) : Expr

                                                                                                    Multiplication

                                                                                                  • neg (e : Expr) : Expr

                                                                                                    Negation

                                                                                                  • inv (e : Expr) : Expr

                                                                                                    Multiplicative inverse (partial: undefined at 0)

                                                                                                  • exp (e : Expr) : Expr

                                                                                                    Exponential function

                                                                                                  • sin (e : Expr) : Expr

                                                                                                    Sine function

                                                                                                  • cos (e : Expr) : Expr

                                                                                                    Cosine function

                                                                                                  • log (e : Expr) : Expr

                                                                                                    Natural logarithm (partial: undefined for x ≤ 0)

                                                                                                  • atan (e : Expr) : Expr

                                                                                                    Arctangent function

                                                                                                  • arsinh (e : Expr) : Expr

                                                                                                    Inverse hyperbolic sine (arsinh)

                                                                                                  • atanh (e : Expr) : Expr

                                                                                                    Inverse hyperbolic tangent (partial: undefined for |x| ≥ 1)

                                                                                                  • sinc (e : Expr) : Expr

                                                                                                    Sinc function: sinc(x) = sin(x)/x for x ≠ 0, sinc(0) = 1

                                                                                                  • erf (e : Expr) : Expr

                                                                                                    Error function: erf(x) = (2/√π) ∫₀ˣ exp(-t²) dt

                                                                                                  • sinh (e : Expr) : Expr

                                                                                                    Hyperbolic sine: sinh(x) = (exp(x) - exp(-x)) / 2

                                                                                                  • cosh (e : Expr) : Expr

                                                                                                    Hyperbolic cosine: cosh(x) = (exp(x) + exp(-x)) / 2

                                                                                                  • tanh (e : Expr) : Expr

                                                                                                    Hyperbolic tangent: tanh(x) = sinh(x) / cosh(x) ∈ (-1, 1)

                                                                                                  • sqrt (e : Expr) : Expr

                                                                                                    Square root (partial: undefined for x < 0)

                                                                                                  • namedConst (c : MathConst) : Expr

                                                                                                    A named mathematical constant (π, γ, …) looked up from a table.

                                                                                                  Instances For
                                                                                                    Equations
                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                    Instances For
                                                                                                      def LeanCert.Core.instDecidableEqExpr.decEq (x✝ x✝¹ : Expr) :
                                                                                                      Decidable (x✝ = x✝¹)
                                                                                                      Equations
                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                      Instances For
                                                                                                        def LeanCert.Core.Expr.sub (e₁ e₂ : Expr) :

                                                                                                        Subtraction as a derived operation

                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          def LeanCert.Core.Expr.div (e₁ e₂ : Expr) :

                                                                                                          Division as a derived operation

                                                                                                          Equations
                                                                                                          Instances For

                                                                                                            Integer power (non-negative exponent)

                                                                                                            Equations
                                                                                                            Instances For

                                                                                                              Absolute value as a derived operation: |x| = sqrt(x²) This gives correct results for all real x (except at 0 for interval purposes)

                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                noncomputable def LeanCert.Core.Expr.eval (ρ : ℕ → ℝ) :
                                                                                                                Expr → ℝ

                                                                                                                Evaluate an expression given a variable assignment ρ : Nat → ℝ

                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  def LeanCert.Core.Expr.updateVar (ρ : ℕ → ℝ) (idx : ℕ) (x : ℝ) :
                                                                                                                  ℕ → ℝ

                                                                                                                  Update variable assignment at a specific index

                                                                                                                  Equations
                                                                                                                  Instances For

                                                                                                                    Notation for replacing one coordinate of a variable environment.

                                                                                                                    Equations
                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                    Instances For
                                                                                                                      @[simp]
                                                                                                                      theorem LeanCert.Core.Expr.updateVar_same (ρ : ℕ → ℝ) (idx : ℕ) (x : ℝ) :
                                                                                                                      (ρ[idx ↦ x]) idx = x
                                                                                                                      @[simp]
                                                                                                                      theorem LeanCert.Core.Expr.updateVar_other (ρ : ℕ → ℝ) (idx i : ℕ) (x : ℝ) (h : i ≠ idx) :
                                                                                                                      (ρ[idx ↦ x]) i = ρ i
                                                                                                                      theorem LeanCert.Core.Expr.updateVar_self (ρ : ℕ → ℝ) (idx : ℕ) :
                                                                                                                      ρ[idx ↦ ρ idx] = ρ
                                                                                                                      @[reducible, inline]
                                                                                                                      noncomputable abbrev LeanCert.Core.Expr.evalAlong (e : Expr) (ρ : ℕ → ℝ) (idx : ℕ) :
                                                                                                                      ℝ → ℝ

                                                                                                                      Evaluate e as a scalar function of variable idx, with all other variables fixed by ρ. This represents the map t ↦ eval ρ[idx ↦ t] e.

                                                                                                                      Equations
                                                                                                                      Instances For

                                                                                                                        An expression is closed if it has no free variables

                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          @[simp]
                                                                                                                          theorem LeanCert.Core.Expr.eval_const (ρ : ℕ → ℝ) (q : ℚ) :
                                                                                                                          eval ρ (const q) = ↑q
                                                                                                                          @[simp]
                                                                                                                          theorem LeanCert.Core.Expr.eval_var (ρ : ℕ → ℝ) (idx : ℕ) :
                                                                                                                          eval ρ (var idx) = ρ idx
                                                                                                                          @[simp]
                                                                                                                          theorem LeanCert.Core.Expr.eval_add (ρ : ℕ → ℝ) (e₁ e₂ : Expr) :
                                                                                                                          eval ρ (e₁.add e₂) = eval ρ e₁ + eval ρ e₂
                                                                                                                          @[simp]
                                                                                                                          theorem LeanCert.Core.Expr.eval_mul (ρ : ℕ → ℝ) (e₁ e₂ : Expr) :
                                                                                                                          eval ρ (e₁.mul e₂) = eval ρ e₁ * eval ρ e₂
                                                                                                                          @[simp]
                                                                                                                          theorem LeanCert.Core.Expr.eval_neg (ρ : ℕ → ℝ) (e : Expr) :
                                                                                                                          eval ρ e.neg = -eval ρ e
                                                                                                                          @[simp]
                                                                                                                          theorem LeanCert.Core.Expr.eval_inv (ρ : ℕ → ℝ) (e : Expr) :
                                                                                                                          eval ρ e.inv = (eval ρ e)⁻¹
                                                                                                                          @[simp]
                                                                                                                          theorem LeanCert.Core.Expr.eval_exp (ρ : ℕ → ℝ) (e : Expr) :
                                                                                                                          eval ρ e.exp = Real.exp (eval ρ e)
                                                                                                                          @[simp]
                                                                                                                          theorem LeanCert.Core.Expr.eval_sin (ρ : ℕ → ℝ) (e : Expr) :
                                                                                                                          eval ρ e.sin = Real.sin (eval ρ e)
                                                                                                                          @[simp]
                                                                                                                          theorem LeanCert.Core.Expr.eval_cos (ρ : ℕ → ℝ) (e : Expr) :
                                                                                                                          eval ρ e.cos = Real.cos (eval ρ e)
                                                                                                                          @[simp]
                                                                                                                          theorem LeanCert.Core.Expr.eval_log (ρ : ℕ → ℝ) (e : Expr) :
                                                                                                                          eval ρ e.log = Real.log (eval ρ e)
                                                                                                                          @[simp]
                                                                                                                          theorem LeanCert.Core.Expr.eval_atan (ρ : ℕ → ℝ) (e : Expr) :
                                                                                                                          eval ρ e.atan = Real.arctan (eval ρ e)
                                                                                                                          @[simp]
                                                                                                                          theorem LeanCert.Core.Expr.eval_arsinh (ρ : ℕ → ℝ) (e : Expr) :
                                                                                                                          @[simp]
                                                                                                                          theorem LeanCert.Core.Expr.eval_atanh (ρ : ℕ → ℝ) (e : Expr) :
                                                                                                                          eval ρ e.atanh = Real.atanh (eval ρ e)
                                                                                                                          @[simp]
                                                                                                                          theorem LeanCert.Core.Expr.eval_sinc (ρ : ℕ → ℝ) (e : Expr) :
                                                                                                                          eval ρ e.sinc = Real.sinc (eval ρ e)
                                                                                                                          @[simp]
                                                                                                                          theorem LeanCert.Core.Expr.eval_erf (ρ : ℕ → ℝ) (e : Expr) :
                                                                                                                          eval ρ e.erf = Real.erf (eval ρ e)
                                                                                                                          @[simp]
                                                                                                                          theorem LeanCert.Core.Expr.eval_sinh (ρ : ℕ → ℝ) (e : Expr) :
                                                                                                                          eval ρ e.sinh = Real.sinh (eval ρ e)
                                                                                                                          @[simp]
                                                                                                                          theorem LeanCert.Core.Expr.eval_cosh (ρ : ℕ → ℝ) (e : Expr) :
                                                                                                                          eval ρ e.cosh = Real.cosh (eval ρ e)
                                                                                                                          @[simp]
                                                                                                                          theorem LeanCert.Core.Expr.eval_tanh (ρ : ℕ → ℝ) (e : Expr) :
                                                                                                                          eval ρ e.tanh = Real.tanh (eval ρ e)
                                                                                                                          @[simp]
                                                                                                                          theorem LeanCert.Core.Expr.eval_sqrt (ρ : ℕ → ℝ) (e : Expr) :
                                                                                                                          eval ρ e.sqrt = √(eval ρ e)
                                                                                                                          @[simp]
                                                                                                                          theorem LeanCert.Core.Expr.eval_sub (ρ : ℕ → ℝ) (e₁ e₂ : Expr) :
                                                                                                                          eval ρ (e₁.sub e₂) = eval ρ e₁ - eval ρ e₂
                                                                                                                          @[simp]
                                                                                                                          theorem LeanCert.Core.Expr.eval_div (ρ : ℕ → ℝ) (e₁ e₂ : Expr) :
                                                                                                                          eval ρ (e₁.div e₂) = eval ρ e₁ / eval ρ e₂
                                                                                                                          @[simp]
                                                                                                                          theorem LeanCert.Core.Expr.eval_pow (ρ : ℕ → ℝ) (e : Expr) (n : ℕ) :
                                                                                                                          eval ρ (e.pow n) = eval ρ e ^ n
                                                                                                                          theorem LeanCert.Core.Expr.eval_abs (ρ : ℕ → ℝ) (e : Expr) :
                                                                                                                          eval ρ e.abs = |eval ρ e|

                                                                                                                          Evaluation of abs for any argument: |x| = sqrt(x²)

                                                                                                                          theorem LeanCert.Core.Expr.eval_sqrt_mul_self_eq_abs (ρ : ℕ → ℝ) (e : Expr) :
                                                                                                                          eval ρ (e.mul e).sqrt = |eval ρ e|

                                                                                                                          Evaluation of sqrt(x * x) = |x| (unfolded form of abs).

                                                                                                                          √(x * x) = |x| — LeanCert-namespaced alias of Real.sqrt_mul_self_eq_abs.

                                                                                                                          theorem LeanCert.Core.Expr.eval_sqrt_sq_of_pos (ρ : ℕ → ℝ) (e : Expr) (hpos : 0 < eval ρ e) :
                                                                                                                          eval ρ (e.mul e).sqrt = eval ρ e

                                                                                                                          For positive x, sqrt(x²) = x

                                                                                                                          theorem LeanCert.Core.Expr.eval_abs_of_pos (ρ : ℕ → ℝ) (e : Expr) (hpos : 0 < eval ρ e) :
                                                                                                                          eval ρ e.abs = eval ρ e

                                                                                                                          Abs correctly computes absolute value for positive inputs

                                                                                                                          theorem LeanCert.Core.Expr.eval_abs_of_neg (ρ : ℕ → ℝ) (e : Expr) (hneg : eval ρ e < 0) :
                                                                                                                          eval ρ e.abs = -eval ρ e

                                                                                                                          Abs correctly computes absolute value for negative inputs

                                                                                                                          theorem LeanCert.Core.Expr.evalAlong_eq (e : Expr) (ρ : ℕ → ℝ) (idx : ℕ) (t : ℝ) :
                                                                                                                          e.evalAlong ρ idx t = eval (ρ[idx ↦ t]) e
                                                                                                                          theorem LeanCert.Core.Expr.evalAlong_at_ρ (e : Expr) (ρ : ℕ → ℝ) (idx : ℕ) :
                                                                                                                          e.evalAlong ρ idx (ρ idx) = eval ρ e
                                                                                                                          theorem LeanCert.Core.Expr.evalAlong_const' (ρ : ℕ → ℝ) (idx : ℕ) (q : ℚ) :
                                                                                                                          (const q).evalAlong ρ idx = fun (x : ℝ) => ↑q

                                                                                                                          evalAlong for a constant is constant

                                                                                                                          theorem LeanCert.Core.Expr.evalAlong_var_active (ρ : ℕ → ℝ) (idx : ℕ) :
                                                                                                                          (var idx).evalAlong ρ idx = id

                                                                                                                          evalAlong for the active variable is the identity

                                                                                                                          theorem LeanCert.Core.Expr.evalAlong_var_passive (ρ : ℕ → ℝ) (idx i : ℕ) (h : i ≠ idx) :
                                                                                                                          (var i).evalAlong ρ idx = fun (x : ℝ) => ρ i

                                                                                                                          evalAlong for a passive variable is constant

                                                                                                                          theorem LeanCert.Core.Expr.evalAlong_add (e₁ e₂ : Expr) (ρ : ℕ → ℝ) (idx : ℕ) :
                                                                                                                          (e₁.add e₂).evalAlong ρ idx = fun (t : ℝ) => e₁.evalAlong ρ idx t + e₂.evalAlong ρ idx t

                                                                                                                          evalAlong for addition

                                                                                                                          theorem LeanCert.Core.Expr.evalAlong_add_pi (e₁ e₂ : Expr) (ρ : ℕ → ℝ) (idx : ℕ) :
                                                                                                                          (e₁.add e₂).evalAlong ρ idx = e₁.evalAlong ρ idx + e₂.evalAlong ρ idx

                                                                                                                          evalAlong for addition (Pi form for compatibility with deriv_add)

                                                                                                                          theorem LeanCert.Core.Expr.evalAlong_mul (e₁ e₂ : Expr) (ρ : ℕ → ℝ) (idx : ℕ) :
                                                                                                                          (e₁.mul e₂).evalAlong ρ idx = fun (t : ℝ) => e₁.evalAlong ρ idx t * e₂.evalAlong ρ idx t

                                                                                                                          evalAlong for multiplication

                                                                                                                          theorem LeanCert.Core.Expr.evalAlong_mul_pi (e₁ e₂ : Expr) (ρ : ℕ → ℝ) (idx : ℕ) :
                                                                                                                          (e₁.mul e₂).evalAlong ρ idx = e₁.evalAlong ρ idx * e₂.evalAlong ρ idx

                                                                                                                          evalAlong for multiplication (Pi form for compatibility with deriv_mul)

                                                                                                                          theorem LeanCert.Core.Expr.evalAlong_neg (e : Expr) (ρ : ℕ → ℝ) (idx : ℕ) :
                                                                                                                          e.neg.evalAlong ρ idx = fun (t : ℝ) => -e.evalAlong ρ idx t

                                                                                                                          evalAlong for negation

                                                                                                                          theorem LeanCert.Core.Expr.evalAlong_neg_pi (e : Expr) (ρ : ℕ → ℝ) (idx : ℕ) :
                                                                                                                          e.neg.evalAlong ρ idx = -e.evalAlong ρ idx

                                                                                                                          evalAlong for negation (Pi form for compatibility with deriv.neg)

                                                                                                                          theorem LeanCert.Core.Expr.evalAlong_sin (e : Expr) (ρ : ℕ → ℝ) (idx : ℕ) :
                                                                                                                          e.sin.evalAlong ρ idx = fun (t : ℝ) => Real.sin (e.evalAlong ρ idx t)

                                                                                                                          evalAlong for sin

                                                                                                                          theorem LeanCert.Core.Expr.evalAlong_cos (e : Expr) (ρ : ℕ → ℝ) (idx : ℕ) :
                                                                                                                          e.cos.evalAlong ρ idx = fun (t : ℝ) => Real.cos (e.evalAlong ρ idx t)

                                                                                                                          evalAlong for cos

                                                                                                                          theorem LeanCert.Core.Expr.evalAlong_exp (e : Expr) (ρ : ℕ → ℝ) (idx : ℕ) :
                                                                                                                          e.exp.evalAlong ρ idx = fun (t : ℝ) => Real.exp (e.evalAlong ρ idx t)

                                                                                                                          evalAlong for exp

                                                                                                                          theorem LeanCert.Core.Expr.evalAlong_inv (e : Expr) (ρ : ℕ → ℝ) (idx : ℕ) :
                                                                                                                          e.inv.evalAlong ρ idx = fun (t : ℝ) => (e.evalAlong ρ idx t)⁻¹

                                                                                                                          evalAlong for inv

                                                                                                                          theorem LeanCert.Core.Expr.evalAlong_log (e : Expr) (ρ : ℕ → ℝ) (idx : ℕ) :
                                                                                                                          e.log.evalAlong ρ idx = fun (t : ℝ) => Real.log (e.evalAlong ρ idx t)

                                                                                                                          evalAlong for log

                                                                                                                          theorem LeanCert.Core.Expr.evalAlong_atan (e : Expr) (ρ : ℕ → ℝ) (idx : ℕ) :
                                                                                                                          e.atan.evalAlong ρ idx = fun (t : ℝ) => Real.arctan (e.evalAlong ρ idx t)

                                                                                                                          evalAlong for atan

                                                                                                                          theorem LeanCert.Core.Expr.evalAlong_arsinh (e : Expr) (ρ : ℕ → ℝ) (idx : ℕ) :
                                                                                                                          e.arsinh.evalAlong ρ idx = fun (t : ℝ) => Real.arsinh (e.evalAlong ρ idx t)

                                                                                                                          evalAlong for arsinh

                                                                                                                          theorem LeanCert.Core.Expr.evalAlong_atanh (e : Expr) (ρ : ℕ → ℝ) (idx : ℕ) :
                                                                                                                          e.atanh.evalAlong ρ idx = fun (t : ℝ) => Real.atanh (e.evalAlong ρ idx t)

                                                                                                                          evalAlong for atanh

                                                                                                                          Single-variable expressions #

                                                                                                                          For 1D optimization and root finding, we often work with expressions that only use variable 0. These lemmas establish that such expressions can be evaluated equivalently with different environment representations.

                                                                                                                          theorem LeanCert.Core.Expr.eval_usesOnlyVar0_eq (e : Expr) (he : e.usesOnlyVar0 = true) (ρ₁ ρ₂ : ℕ → ℝ) (h0 : ρ₁ 0 = ρ₂ 0) :
                                                                                                                          eval ρ₁ e = eval ρ₂ e

                                                                                                                          If two environments agree on variable 0, then a usesOnlyVar0 expression evaluates the same

                                                                                                                          theorem LeanCert.Core.Expr.eval_1d_equiv (e : Expr) (he : e.usesOnlyVar0 = true) (x : ℝ) :
                                                                                                                          eval (fun (n : ℕ) => if n = 0 then x else 0) e = eval (fun (x_1 : ℕ) => x) e

                                                                                                                          For single-variable expressions, fun n => if n = 0 then x else 0 and fun _ => x give the same evaluation result.

                                                                                                                          theorem LeanCert.Core.Expr.eval_box1d_eq_eval1d (e : Expr) (he : e.usesOnlyVar0 = true) (x : ℝ) :
                                                                                                                          eval (fun (n : ℕ) => if n = 0 then x else 0) e = eval (fun (x_1 : ℕ) => x) e

                                                                                                                          Alternative: evaluation with Box-style environment equals 1D evaluation

                                                                                                                          Abstract Interval Interface #

                                                                                                                          This file defines the abstract notion of intervals as subsets of ℝ, with semantic properties. This provides the mathematical foundation that IntervalReal will implement computationally.

                                                                                                                          Main definitions #

                                                                                                                          Design notes #

                                                                                                                          We primarily use Set.Icc a b from Mathlib as our semantic interval type. This file collects lemmas and abstractions useful for verified numerics.

                                                                                                                          Interval membership and operations #

                                                                                                                          @[reducible, inline]
                                                                                                                          abbrev LeanCert.Core.memIcc (x a b : ℝ) :

                                                                                                                          A real number is in the interval [a, b]

                                                                                                                          Equations
                                                                                                                          Instances For
                                                                                                                            theorem LeanCert.Core.mem_Icc_iff (x a b : ℝ) :
                                                                                                                            memIcc x a b ↔ x ∈ Set.Icc a b

                                                                                                                            Interval arithmetic semantics #

                                                                                                                            These lemmas establish the semantic foundation for interval arithmetic: if x ∈ [a, b] and y ∈ [c, d], then x ⊕ y ∈ [a ⊕ c, b ⊕ d] (for appropriate ⊕).

                                                                                                                            theorem LeanCert.Core.add_mem_Icc {x y a b c d : ℝ} (hx : x ∈ Set.Icc a b) (hy : y ∈ Set.Icc c d) :
                                                                                                                            x + y ∈ Set.Icc (a + c) (b + d)

                                                                                                                            Addition preserves interval membership

                                                                                                                            theorem LeanCert.Core.neg_mem_Icc {x a b : ℝ} (hx : x ∈ Set.Icc a b) :
                                                                                                                            -x ∈ Set.Icc (-b) (-a)

                                                                                                                            Negation reverses interval bounds

                                                                                                                            theorem LeanCert.Core.sub_mem_Icc {x y a b c d : ℝ} (hx : x ∈ Set.Icc a b) (hy : y ∈ Set.Icc c d) :
                                                                                                                            x - y ∈ Set.Icc (a - d) (b - c)

                                                                                                                            Subtraction on intervals

                                                                                                                            Convexity #

                                                                                                                            Closed intervals are convex

                                                                                                                            Compactness #

                                                                                                                            Nonempty closed bounded intervals are compact

                                                                                                                            Continuous functions on intervals #

                                                                                                                            theorem LeanCert.Core.continuous_Icc_bounds {f : ℝ → ℝ} {a b : ℝ} (hab : a ≤ b) (hf : Continuous f) :
                                                                                                                            ∃ (lo : ℝ) (hi : ℝ), (∀ x ∈ Set.Icc a b, lo ≤ f x ∧ f x ≤ hi) ∧ (∃ x ∈ Set.Icc a b, f x = lo) ∧ ∃ x ∈ Set.Icc a b, f x = hi

                                                                                                                            A continuous function on a compact interval attains its bounds

                                                                                                                            Rational Endpoint Intervals - Core Definitions #

                                                                                                                            This file defines IntervalRat, a concrete interval type with rational endpoints suitable for computation. We prove the Fundamental Theorem of Interval Arithmetic (FTIA) for each operation.

                                                                                                                            Main definitions #

                                                                                                                            Main theorems #

                                                                                                                            Design notes #

                                                                                                                            All operations maintain the invariant lo ≤ hi. Domain restrictions for partial operations (like inv) are encoded via separate types or explicit hypotheses.

                                                                                                                            An interval with rational endpoints

                                                                                                                            • lo : ℚ

                                                                                                                              Lower endpoint of the interval.

                                                                                                                            • hi : ℚ

                                                                                                                              Upper endpoint of the interval.

                                                                                                                            • le : self.lo ≤ self.hi
                                                                                                                            Instances For
                                                                                                                              Equations
                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                              Instances For
                                                                                                                                Equations
                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                Instances For
                                                                                                                                  @[instance_reducible]

                                                                                                                                  Default interval [0, 0] for unsupported expression branches

                                                                                                                                  Equations

                                                                                                                                  The set of reals contained in this interval

                                                                                                                                  Equations
                                                                                                                                  Instances For
                                                                                                                                    @[instance_reducible]

                                                                                                                                    Membership in an interval

                                                                                                                                    Equations
                                                                                                                                    @[simp]
                                                                                                                                    theorem LeanCert.Core.IntervalRat.mem_def (x : ℝ) (I : IntervalRat) :
                                                                                                                                    x ∈ I ↔ ↑I.lo ≤ x ∧ x ≤ ↑I.hi

                                                                                                                                    Membership in IntervalRat is the same as membership in Set.Icc

                                                                                                                                    theorem LeanCert.Core.IntervalRat.forall_mem_iff_forall_Icc {P : ℝ → Prop} (I : IntervalRat) :
                                                                                                                                    (∀ x ∈ I, P x) ↔ ∀ x ∈ Set.Icc ↑I.lo ↑I.hi, P x

                                                                                                                                    Universal quantifier over IntervalRat equals universal over Set.Icc

                                                                                                                                    theorem LeanCert.Core.IntervalRat.exists_mem_iff_exists_Icc {P : ℝ → Prop} (I : IntervalRat) :
                                                                                                                                    (∃ x ∈ I, P x) ↔ ∃ x ∈ Set.Icc ↑I.lo ↑I.hi, P x

                                                                                                                                    Existence in IntervalRat equals existence in Set.Icc

                                                                                                                                    Create an interval from a single rational

                                                                                                                                    Equations
                                                                                                                                    Instances For

                                                                                                                                      The width of an interval

                                                                                                                                      Equations
                                                                                                                                      Instances For

                                                                                                                                        Midpoint of an interval

                                                                                                                                        Equations
                                                                                                                                        Instances For

                                                                                                                                          The midpoint of an interval is contained in the interval

                                                                                                                                          Interval addition #

                                                                                                                                          Add two intervals

                                                                                                                                          Equations
                                                                                                                                          Instances For
                                                                                                                                            theorem LeanCert.Core.IntervalRat.mem_add {x y : ℝ} {I J : IntervalRat} (hx : x ∈ I) (hy : y ∈ J) :
                                                                                                                                            x + y ∈ I.add J

                                                                                                                                            FTIA for addition

                                                                                                                                            Interval negation #

                                                                                                                                            Negate an interval

                                                                                                                                            Equations
                                                                                                                                            Instances For
                                                                                                                                              theorem LeanCert.Core.IntervalRat.mem_neg {x : ℝ} {I : IntervalRat} (hx : x ∈ I) :
                                                                                                                                              -x ∈ I.neg

                                                                                                                                              FTIA for negation

                                                                                                                                              Interval subtraction #

                                                                                                                                              Subtract two intervals

                                                                                                                                              Equations
                                                                                                                                              Instances For
                                                                                                                                                theorem LeanCert.Core.IntervalRat.mem_sub {x y : ℝ} {I J : IntervalRat} (hx : x ∈ I) (hy : y ∈ J) :
                                                                                                                                                x - y ∈ I.sub J

                                                                                                                                                FTIA for subtraction

                                                                                                                                                Interval multiplication #

                                                                                                                                                Helper: minimum of four rationals

                                                                                                                                                Equations
                                                                                                                                                Instances For

                                                                                                                                                  Helper: maximum of four rationals

                                                                                                                                                  Equations
                                                                                                                                                  Instances For
                                                                                                                                                    theorem LeanCert.Core.IntervalRat.min4_le_all (a b c d : ℚ) :
                                                                                                                                                    min4 a b c d ≤ a ∧ min4 a b c d ≤ b ∧ min4 a b c d ≤ c ∧ min4 a b c d ≤ d
                                                                                                                                                    theorem LeanCert.Core.IntervalRat.all_le_max4 (a b c d : ℚ) :
                                                                                                                                                    a ≤ max4 a b c d ∧ b ≤ max4 a b c d ∧ c ≤ max4 a b c d ∧ d ≤ max4 a b c d
                                                                                                                                                    theorem LeanCert.Core.IntervalRat.le_min4_iff (x a b c d : ℚ) :
                                                                                                                                                    x ≤ min4 a b c d ↔ x ≤ a ∧ x ≤ b ∧ x ≤ c ∧ x ≤ d
                                                                                                                                                    theorem LeanCert.Core.IntervalRat.max4_le_iff (x a b c d : ℚ) :
                                                                                                                                                    max4 a b c d ≤ x ↔ a ≤ x ∧ b ≤ x ∧ c ≤ x ∧ d ≤ x

                                                                                                                                                    Multiply two intervals

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

                                                                                                                                                      Fast interval multiplication using sign-based case splitting. Reduces from 4 multiplications + 12 comparisons to 2 multiplications in the common case (both intervals positive or both negative). Falls back to the full 4-way product for mixed-sign intervals.

                                                                                                                                                      Equations
                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                      Instances For
                                                                                                                                                        theorem LeanCert.Core.IntervalRat.mem_mul {x y : ℝ} {I J : IntervalRat} (hx : x ∈ I) (hy : y ∈ J) :
                                                                                                                                                        x * y ∈ I.mul J

                                                                                                                                                        FTIA for multiplication

                                                                                                                                                        theorem LeanCert.Core.IntervalRat.eq_min4_of_le {a b c d : ℚ} (h1 : a ≤ b) (h2 : a ≤ c) (h3 : a ≤ d) :
                                                                                                                                                        a = min4 a b c d

                                                                                                                                                        Helper: show a = min4 a b c d when a ≤ b, a ≤ c, a ≤ d

                                                                                                                                                        theorem LeanCert.Core.IntervalRat.eq_min4_of_le2 {a b c d : ℚ} (h1 : b ≤ a) (h2 : b ≤ c) (h3 : b ≤ d) :
                                                                                                                                                        b = min4 a b c d
                                                                                                                                                        theorem LeanCert.Core.IntervalRat.eq_min4_of_le3 {a b c d : ℚ} (h1 : c ≤ a) (h2 : c ≤ b) (h3 : c ≤ d) :
                                                                                                                                                        c = min4 a b c d
                                                                                                                                                        theorem LeanCert.Core.IntervalRat.eq_min4_of_le4 {a b c d : ℚ} (h1 : d ≤ a) (h2 : d ≤ b) (h3 : d ≤ c) :
                                                                                                                                                        d = min4 a b c d
                                                                                                                                                        theorem LeanCert.Core.IntervalRat.eq_max4_of_ge {a b c d : ℚ} (h1 : b ≤ a) (h2 : c ≤ a) (h3 : d ≤ a) :
                                                                                                                                                        a = max4 a b c d
                                                                                                                                                        theorem LeanCert.Core.IntervalRat.eq_max4_of_ge2 {a b c d : ℚ} (h1 : a ≤ b) (h2 : c ≤ b) (h3 : d ≤ b) :
                                                                                                                                                        b = max4 a b c d
                                                                                                                                                        theorem LeanCert.Core.IntervalRat.eq_max4_of_ge3 {a b c d : ℚ} (h1 : a ≤ c) (h2 : b ≤ c) (h3 : d ≤ c) :
                                                                                                                                                        c = max4 a b c d
                                                                                                                                                        theorem LeanCert.Core.IntervalRat.eq_max4_of_ge4 {a b c d : ℚ} (h1 : a ≤ d) (h2 : b ≤ d) (h3 : c ≤ d) :
                                                                                                                                                        d = max4 a b c d
                                                                                                                                                        theorem LeanCert.Core.IntervalRat.mem_mulFast {x y : ℝ} {I J : IntervalRat} (hx : x ∈ I) (hy : y ∈ J) :
                                                                                                                                                        x * y ∈ I.mulFast J

                                                                                                                                                        mulFast preserves the containment property of mul. This is retained as documentation and a future audited optimization hook; production certificate checking currently uses mul directly.

                                                                                                                                                        Interval containing zero check #

                                                                                                                                                        Check if an interval contains zero

                                                                                                                                                        Equations
                                                                                                                                                        Instances For
                                                                                                                                                          @[instance_reducible]

                                                                                                                                                          Decidable containsZero

                                                                                                                                                          Equations

                                                                                                                                                          An interval that is guaranteed not to contain zero

                                                                                                                                                          Instances For

                                                                                                                                                            Interval inversion (for nonzero intervals) #

                                                                                                                                                            Invert an interval that doesn't contain zero

                                                                                                                                                            Equations
                                                                                                                                                            Instances For

                                                                                                                                                              FTIA for inversion #

                                                                                                                                                              Scalar operations #

                                                                                                                                                              Scale an interval by a rational

                                                                                                                                                              Equations
                                                                                                                                                              Instances For
                                                                                                                                                                theorem LeanCert.Core.IntervalRat.mem_scale {x : ℝ} {I : IntervalRat} (q : ℚ) (hx : x ∈ I) :
                                                                                                                                                                ↑q * x ∈ scale q I

                                                                                                                                                                FTIA for scaling

                                                                                                                                                                Interval splitting #

                                                                                                                                                                Split an interval at its midpoint

                                                                                                                                                                Equations
                                                                                                                                                                Instances For
                                                                                                                                                                  theorem LeanCert.Core.IntervalRat.mem_bisect_left {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (hm : x ≤ ↑I.midpoint) :
                                                                                                                                                                  x ∈ I.bisect.1
                                                                                                                                                                  theorem LeanCert.Core.IntervalRat.mem_bisect_right {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (hm : ↑I.midpoint ≤ x) :
                                                                                                                                                                  x ∈ I.bisect.2
                                                                                                                                                                  theorem LeanCert.Core.IntervalRat.midpoint_sub_lo (I : IntervalRat) :
                                                                                                                                                                  ↑I.midpoint - ↑I.lo = (↑I.hi - ↑I.lo) / 2

                                                                                                                                                                  Distance from midpoint to lo is half the width

                                                                                                                                                                  theorem LeanCert.Core.IntervalRat.hi_sub_midpoint (I : IntervalRat) :
                                                                                                                                                                  ↑I.hi - ↑I.midpoint = (↑I.hi - ↑I.lo) / 2

                                                                                                                                                                  Distance from hi to midpoint is half the width

                                                                                                                                                                  Midpoint is at least lo (real version)

                                                                                                                                                                  Midpoint is at most hi (real version)

                                                                                                                                                                  Left bisection is a subset of the original interval

                                                                                                                                                                  Right bisection is a subset of the original interval

                                                                                                                                                                  theorem LeanCert.Core.IntervalRat.mem_bisect_or {x : ℝ} {I : IntervalRat} (hx : x ∈ I) :
                                                                                                                                                                  x ∈ I.bisect.1 ∨ x ∈ I.bisect.2

                                                                                                                                                                  Any point in an interval is in one of its bisected halves

                                                                                                                                                                  The default interval [0,0] contains only 0

                                                                                                                                                                  Interval intersection #

                                                                                                                                                                  Intersect two intervals. Returns none if they don't intersect.

                                                                                                                                                                  Equations
                                                                                                                                                                  Instances For
                                                                                                                                                                    theorem LeanCert.Core.IntervalRat.mem_intersect {x : ℝ} {I J : IntervalRat} (hI : x ∈ I) (hJ : x ∈ J) :
                                                                                                                                                                    ∃ (K : IntervalRat), I.intersect J = some K ∧ x ∈ K

                                                                                                                                                                    If intersection succeeds, the result contains any point in both intervals

                                                                                                                                                                    If intersection returns some K, then K ⊆ I

                                                                                                                                                                    If intersection returns some K, then K ⊆ J

                                                                                                                                                                    Verified Argument Reduction for Logarithm #

                                                                                                                                                                    This file provides argument reduction for computing log(q) using the identity: log(q) = log(m) + k * log(2) where m = q * 2^(-k) is in a "good" range [1/2, 2] for Taylor series convergence.

                                                                                                                                                                    Main definitions #

                                                                                                                                                                    Main theorems #

                                                                                                                                                                    Design notes #

                                                                                                                                                                    This reduction allows us to use the rapidly converging atanh-based series: log(m) = 2 * atanh((m-1)/(m+1)) For m ∈ [1/2, 2], we have (m-1)/(m+1) ∈ [-1/3, 1/3], where atanh converges very fast.

                                                                                                                                                                    Argument Reduction #

                                                                                                                                                                    Find k such that q * 2^(-k) is approximately in [1/2, 2]. Implementation: k = log2(num) - log2(den) approximately.

                                                                                                                                                                    Equations
                                                                                                                                                                    Instances For

                                                                                                                                                                      The reduced mantissa m = q * 2^(-k).

                                                                                                                                                                      Equations
                                                                                                                                                                      Instances For
                                                                                                                                                                        theorem LeanCert.Core.LogReduction.reconstruction_eq {q : ℚ} (hq : 0 < q) :
                                                                                                                                                                        have k := reductionExponent q; have m := reduceMantissa q; q = m * 2 ^ k

                                                                                                                                                                        The main algebraic theorem: q = m * 2^k for positive q

                                                                                                                                                                        theorem LeanCert.Core.LogReduction.reduced_bounds_weak {q : ℚ} (hq : 0 < q) :
                                                                                                                                                                        have m := reduceMantissa q; 1 / 4 ≤ m ∧ m ≤ 4

                                                                                                                                                                        The reduced mantissa is bounded: 1/4 ≤ m ≤ 4 for q > 0. (We use slightly weaker bounds than [1/2, 2] for simpler proofs, but the series still converges rapidly.)

                                                                                                                                                                        theorem LeanCert.Core.LogReduction.reduced_bounds {q : ℚ} (hq : 0 < q) :
                                                                                                                                                                        have m := reduceMantissa q; 1 / 2 ≤ m ∧ m ≤ 2

                                                                                                                                                                        Tighter bounds: 1 / 2 ≤ m ≤ 2 for most q > 0

                                                                                                                                                                        The reduced mantissa is positive for positive input

                                                                                                                                                                        Connection to Real.log #

                                                                                                                                                                        theorem LeanCert.Core.LogReduction.log_reduction {q : ℚ} (hq : 0 < q) :
                                                                                                                                                                        have k := reductionExponent q; have m := reduceMantissa q; Real.log ↑q = Real.log ↑m + ↑k * Real.log 2

                                                                                                                                                                        Key algebraic identity for Real.log: log(q) = log(m) + k * log(2)

                                                                                                                                                                        theorem LeanCert.Core.LogReduction.atanh_arg_bounds {m : ℚ} (hlo : 1 / 2 ≤ m) (hhi : m ≤ 2) :
                                                                                                                                                                        have y := (m - 1) / (m + 1); -1 / 3 ≤ y ∧ y ≤ 1 / 3

                                                                                                                                                                        The transformation y = (m-1)/(m+1) maps m ∈ [1/2, 2] to y ∈ [-1/3, 1/3]

                                                                                                                                                                        theorem LeanCert.Core.LogReduction.log_via_atanh {m : ℚ} (hm_pos : 0 < m) :
                                                                                                                                                                        Real.log ↑m = 2 * Real.atanh ((↑m - 1) / (↑m + 1))

                                                                                                                                                                        log(m) = 2 * atanh((m-1)/(m+1)) for m > 0 with m ≠ 1

                                                                                                                                                                        Rational Endpoint Intervals - Transcendental Functions #

                                                                                                                                                                        This file provides noncomputable interval bounds for transcendental functions using floor/ceiling to obtain rational endpoints.

                                                                                                                                                                        Main definitions #

                                                                                                                                                                        Main theorems #

                                                                                                                                                                        Design notes #

                                                                                                                                                                        All definitions in this file are noncomputable as they use Real.exp, Real.log, etc. For computable versions, see IntervalRat.Taylor.

                                                                                                                                                                        Rational enclosure of real intervals #

                                                                                                                                                                        noncomputable def LeanCert.Core.IntervalRat.ofRealEndpoints (lo hi : ℝ) (hle : lo ≤ hi) :

                                                                                                                                                                        Coarse rational enclosure of a real interval using floor/ceil. Given a real interval [lo, hi], returns a rational interval [⌊lo⌋, ⌈hi⌉] that is guaranteed to contain all points in the original interval.

                                                                                                                                                                        Equations
                                                                                                                                                                        Instances For
                                                                                                                                                                          theorem LeanCert.Core.IntervalRat.mem_ofRealEndpoints {x lo hi : ℝ} (hle : lo ≤ hi) (hx : lo ≤ x ∧ x ≤ hi) :
                                                                                                                                                                          x ∈ ofRealEndpoints lo hi hle

                                                                                                                                                                          Any point in [lo, hi] is in the rational enclosure [⌊lo⌋, ⌈hi⌉]

                                                                                                                                                                          Exponential interval #

                                                                                                                                                                          Interval bound for exp on rational intervals. Since exp is strictly increasing, exp([a,b]) ⊆ [⌊exp(a)⌋, ⌈exp(b)⌉]. This uses Real.exp and floor/ceil to get rational bounds.

                                                                                                                                                                          Equations
                                                                                                                                                                          Instances For

                                                                                                                                                                            FTIA for exp: if x ∈ I, then exp(x) ∈ expInterval(I)

                                                                                                                                                                            Positive interval check #

                                                                                                                                                                            Check if an interval is strictly positive (lo > 0)

                                                                                                                                                                            Equations
                                                                                                                                                                            Instances For

                                                                                                                                                                              An interval that is guaranteed to be strictly positive

                                                                                                                                                                              Instances For

                                                                                                                                                                                Logarithm interval (for positive intervals) #

                                                                                                                                                                                Interval bound for log on positive rational intervals. Since log is strictly increasing on (0, ∞), log([a,b]) ⊆ [⌊log(a)⌋, ⌈log(b)⌉] for a > 0. This uses Real.log and floor/ceil to get rational bounds.

                                                                                                                                                                                Equations
                                                                                                                                                                                Instances For

                                                                                                                                                                                  FTIA for log: if x ∈ I with lo > 0, then log(x) ∈ logInterval(I)

                                                                                                                                                                                  Atanh interval (for intervals in (-1, 1)) #

                                                                                                                                                                                  An interval strictly contained in (-1, 1), suitable for atanh

                                                                                                                                                                                  • lo : ℚ

                                                                                                                                                                                    Lower endpoint of the interval.

                                                                                                                                                                                  • hi : ℚ

                                                                                                                                                                                    Upper endpoint of the interval.

                                                                                                                                                                                  • le : self.lo ≤ self.hi
                                                                                                                                                                                  • lo_gt : -1 < self.lo
                                                                                                                                                                                  • hi_lt : self.hi < 1
                                                                                                                                                                                  Instances For

                                                                                                                                                                                    Convert to standard interval

                                                                                                                                                                                    Equations
                                                                                                                                                                                    Instances For

                                                                                                                                                                                      Interval bound for atanh on intervals strictly inside (-1, 1). Since atanh is strictly increasing on (-1, 1), atanh([a,b]) ⊆ [⌊atanh(a)⌋, ⌈atanh(b)⌉].

                                                                                                                                                                                      Equations
                                                                                                                                                                                      Instances For

                                                                                                                                                                                        FTIA for atanh: if x ∈ I and I ⊂ (-1, 1), then atanh(x) ∈ atanhIntervalComputed(I)

                                                                                                                                                                                        Square Root Interval #

                                                                                                                                                                                        Integer square root (floor of sqrt). Satisfies: (intSqrtNat n)^2 ≤ n < (intSqrtNat n + 1)^2

                                                                                                                                                                                        Equations
                                                                                                                                                                                        Instances For

                                                                                                                                                                                          Rational lower bound for sqrt. For q ≥ 0 with q = num/den, we compute floor(sqrt(num * den)) / den. This gives: sqrtRatLower q ≤ sqrt(q).

                                                                                                                                                                                          The idea: sqrt(num/den) = sqrt(num*den)/den when properly scaled.

                                                                                                                                                                                          Equations
                                                                                                                                                                                          Instances For

                                                                                                                                                                                            Rational upper bound for sqrt. For q ≥ 0, we compute ceil(sqrt(num * den)) / den. This gives: sqrt(q) ≤ sqrtRatUpper q.

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

                                                                                                                                                                                              Scaling exponent for precise sqrt bounds (2^scaleBits = scaling factor for denominator)

                                                                                                                                                                                              Equations
                                                                                                                                                                                              Instances For

                                                                                                                                                                                                Rational lower bound for sqrt with high precision. For q ≥ 0, we scale by 4^k, compute integer sqrt, and scale back by 2^k. This gives: sqrtRatLowerPrec q ≤ sqrt(q) with precision ~2^(-k).

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

                                                                                                                                                                                                  Rational upper bound for sqrt with high precision. For q ≥ 0, we scale by 4^k, compute ceil of integer sqrt, and scale back by 2^k. This gives: sqrt(q) ≤ sqrtRatUpperPrec q with precision ~2^(-k).

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

                                                                                                                                                                                                    Soundness of sqrtRatLower: sqrtRatLower q ≤ Real.sqrt q for q ≥ 0

                                                                                                                                                                                                    Soundness of sqrtRatUpper: Real.sqrt q ≤ sqrtRatUpper q for q ≥ 0

                                                                                                                                                                                                    Square root interval with conservative bounds. For a non-negative interval [lo, hi], sqrt is monotone so: sqrt([lo, hi]) ⊆ [0, max(hi, 1)]

                                                                                                                                                                                                    The lower bound is 0 (always sound for sqrt). The upper bound uses max(hi, 1) which satisfies sqrt(x) ≤ max(x, 1) for x ≥ 0.

                                                                                                                                                                                                    Equations
                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                      Improved square root interval with tight lower bounds. For a non-negative interval [lo, hi] with lo ≥ 0:

                                                                                                                                                                                                      • Lower bound: sqrtRatLower(lo)
                                                                                                                                                                                                      • Upper bound: sqrtRatUpper(hi)

                                                                                                                                                                                                      For intervals crossing zero, we use 0 as lower bound.

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

                                                                                                                                                                                                        Soundness of sqrtRatLowerPrec: sqrtRatLowerPrec q k ≤ Real.sqrt q for q ≥ 0

                                                                                                                                                                                                        Soundness of sqrtRatUpperPrec: Real.sqrt q ≤ sqrtRatUpperPrec q k for q ≥ 0

                                                                                                                                                                                                        High-precision square root interval. For a non-negative interval [lo, hi] with lo ≥ 0:

                                                                                                                                                                                                        • Lower bound: sqrtRatLowerPrec(lo)
                                                                                                                                                                                                        • Upper bound: sqrtRatUpperPrec(hi)

                                                                                                                                                                                                        Uses scaling to achieve ~6 decimal digits of precision.

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

                                                                                                                                                                                                          Membership theorem for sqrtIntervalTightPrec

                                                                                                                                                                                                          theorem LeanCert.Core.IntervalRat.mem_sqrtInterval {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (hx_nn : 0 ≤ x) :

                                                                                                                                                                                                          Soundness of sqrt interval: if x ∈ I and x ≥ 0, then sqrt(x) ∈ sqrtInterval I

                                                                                                                                                                                                          General soundness of sqrt interval: works for any x ∈ I (including negative). When x < 0, Real.sqrt x = 0, which is always in [0, max(hi, 1)].

                                                                                                                                                                                                          Soundness of tight sqrt interval: if x ∈ I and x ≥ 0, then sqrt(x) ∈ sqrtIntervalTight I

                                                                                                                                                                                                          General soundness of tight sqrt interval: works for any x ∈ I (including negative). When x < 0, Real.sqrt x = 0, which is always in the result interval.

                                                                                                                                                                                                          Expression Support Predicates #

                                                                                                                                                                                                          This file defines predicates indicating which expressions are supported by different interval evaluation strategies.

                                                                                                                                                                                                          Main definitions #

                                                                                                                                                                                                          Design notes #

                                                                                                                                                                                                          ADSupported is the differentiable fragment used by automatic differentiation. It is contained in ExprSupportedCore via ADSupported.toCore. Checked evaluators accept arbitrary expressions and encode domain failure in their result type, so they need no syntactic support predicate.

                                                                                                                                                                                                          The core subset is kept computable so that tactics can use native_decide for interval bound checking. The extended subset uses Real.exp with floor/ceil bounds, which requires noncomputability.

                                                                                                                                                                                                          Core supported expression subset (computable) #

                                                                                                                                                                                                          Predicate indicating an expression is in the computable core subset. Supports: const, var, add, mul, neg, sin, cos, exp, log, sqrt, sinh, cosh, tanh, erf, pi

                                                                                                                                                                                                          Note: log requires positive domain for correctness. The correctness theorem evalIntervalCore_correct has an additional hypothesis evalDomainValid that ensures log arguments evaluate to positive intervals.

                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                            Extended supported expression subset (with exp) #

                                                                                                                                                                                                            Predicate indicating an expression is in the fully-verified subset for AD. Supports: const, var, add, mul, neg, sin, cos, exp Does NOT support:

                                                                                                                                                                                                            • sqrt (not differentiable at 0 - use ExprSupportedCore for interval evaluation only)
                                                                                                                                                                                                            • inv (requires nonzero interval checks)
                                                                                                                                                                                                            • log (requires positive interval checks)
                                                                                                                                                                                                            • atan/arsinh/atanh (derivative proofs incomplete in the total AD evaluator)
                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                              ADSupported expressions are also in ExprSupportedCore

                                                                                                                                                                                                              The executable support check recognizes exactly the differentiable ADSupported fragment used by the checked AD/monotonicity backend.

                                                                                                                                                                                                              A successful computable core-support check produces the corresponding proof object required by the tight Rational evaluator theorem.

                                                                                                                                                                                                              Generic Taylor Series Abstractions #

                                                                                                                                                                                                              This file provides generic Taylor series machinery for verified numerics. We wrap Mathlib's Taylor expansion theorems in forms convenient for our interval arithmetic framework.

                                                                                                                                                                                                              Phase Status #

                                                                                                                                                                                                              This module is now Phase 3 complete. The main Taylor remainder bound theorem taylor_remainder_bound is fully proved with no sorry markers.

                                                                                                                                                                                                              The theorem provides rigorous bounds on Taylor polynomial approximation errors using Lagrange's form of the remainder.

                                                                                                                                                                                                              Main definitions #

                                                                                                                                                                                                              Design notes #

                                                                                                                                                                                                              This file provides the abstract theory. Specific Taylor expansions for exp, sin, cos, etc. are built using this machinery in conjunction with Mathlib's calculus lemmas.

                                                                                                                                                                                                              Taylor approximation structure #

                                                                                                                                                                                                              A Taylor approximation of a function on an interval.

                                                                                                                                                                                                              Given a function f, center c, and radius r, this represents:

                                                                                                                                                                                                              • A polynomial approximation poly of degree n
                                                                                                                                                                                                              • A remainder bound R such that for all x with |x - c| ≤ r: |f(x) - poly(x - c)| ≤ R
                                                                                                                                                                                                              • degree : ℕ

                                                                                                                                                                                                                Degree of the polynomial

                                                                                                                                                                                                              • coeffs : Fin (self.degree + 1) → ℚ

                                                                                                                                                                                                                Polynomial coefficients (Taylor coefficients at center)

                                                                                                                                                                                                              • remainder : ℚ

                                                                                                                                                                                                                Remainder bound

                                                                                                                                                                                                              • remainder_nonneg : 0 ≤ self.remainder

                                                                                                                                                                                                                The remainder is non-negative

                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                Evaluate the polynomial part at a point

                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                  Derivative bounds #

                                                                                                                                                                                                                  A bound on the n-th derivative of a function on an interval

                                                                                                                                                                                                                  • order : ℕ

                                                                                                                                                                                                                    The derivative order

                                                                                                                                                                                                                  • bound : ℚ

                                                                                                                                                                                                                    Upper bound on |f^(n)(x)| for x in the interval

                                                                                                                                                                                                                  • bound_nonneg : 0 ≤ self.bound

                                                                                                                                                                                                                    The bound is non-negative

                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                    Taylor remainder bounds #

                                                                                                                                                                                                                    Helper lemmas for iteratedDerivWithin conversion #

                                                                                                                                                                                                                    Unique differentiability at the left endpoint of a closed interval.

                                                                                                                                                                                                                    Unique differentiability at the right endpoint of a closed interval.

                                                                                                                                                                                                                    theorem LeanCert.Core.derivWithin_Icc_left_eq_deriv {f : ℝ → ℝ} {c x : ℝ} (hcx : c < x) (hf : DifferentiableAt ℝ f c) :
                                                                                                                                                                                                                    derivWithin f (Set.Icc c x) c = deriv f c

                                                                                                                                                                                                                    At the left endpoint of [c, x], derivWithin equals deriv for differentiable functions.

                                                                                                                                                                                                                    theorem LeanCert.Core.derivWithin_Icc_right_eq_deriv {f : ℝ → ℝ} {c x : ℝ} (hcx : c < x) (hf : DifferentiableAt ℝ f x) :
                                                                                                                                                                                                                    derivWithin f (Set.Icc c x) x = deriv f x

                                                                                                                                                                                                                    At the right endpoint of [c, x], derivWithin equals deriv for differentiable functions.

                                                                                                                                                                                                                    theorem LeanCert.Core.iteratedDerivWithin_Icc_interior_eq {f : ℝ → ℝ} {a b x : ℝ} {n : ℕ} (_hab : a < b) (hx : x ∈ Set.Ioo a b) :

                                                                                                                                                                                                                    Helper lemma: iteratedDerivWithin on Icc a b equals iteratedDeriv at interior points.

                                                                                                                                                                                                                    This bridges Mathlib's iteratedDerivWithin-based Taylor theorems with global iteratedDeriv.

                                                                                                                                                                                                                    theorem LeanCert.Core.iteratedDerivWithin_Icc_left_eq_iteratedDeriv {f : ℝ → ℝ} {c x : ℝ} {n : ℕ} (hcx : c < x) (hf : ContDiff ℝ (↑n) f) :

                                                                                                                                                                                                                    At the left endpoint of [c, x], iteratedDerivWithin equals iteratedDeriv for ContDiff functions.

                                                                                                                                                                                                                    theorem LeanCert.Core.iteratedDerivWithin_Icc_left_eq_iteratedDeriv_of_isOpen {f : ℝ → ℝ} {c x : ℝ} {n : ℕ} {U : Set ℝ} (hU_open : IsOpen U) (hcU : c ∈ U) (hcx : c < x) (hI_sub : Set.Icc c x ⊆ U) (hf : ContDiffOn ℝ (↑n) f U) :

                                                                                                                                                                                                                    At the left endpoint of [c, x], iteratedDerivWithin equals iteratedDeriv for functions that are ContDiffOn on an open set containing c.

                                                                                                                                                                                                                    This is useful for functions like log that are only smooth on (0, ∞).

                                                                                                                                                                                                                    theorem LeanCert.Core.taylor_remainder_bound_on_c_lt_x {f : ℝ → ℝ} {a b c : ℝ} {m : ℕ} {M : ℝ} {U : Set ℝ} (hU_open : IsOpen U) (hI_sub : Set.Icc a b ⊆ U) (hca : a ≤ c) (hf : ContDiffOn ℝ (↑m + 1) f U) (hM : ∀ y ∈ Set.Icc a b, ‖iteratedDeriv (m + 1) f y‖ ≤ M) (x : ℝ) (hx : x ∈ Set.Icc a b) (hcx : c < x) :
                                                                                                                                                                                                                    ‖f x - ∑ i ∈ Finset.range (m + 1), iteratedDeriv i f c / ↑i.factorial * (x - c) ^ i‖ ≤ M * |x - c| ^ (m + 1) / ↑(m + 1).factorial

                                                                                                                                                                                                                    Taylor remainder bound for c < x case with ContDiffOn hypothesis.

                                                                                                                                                                                                                    For functions that are ContDiffOn on an open set containing [a, b], this provides the same Lagrange remainder bound as the global ContDiff version.

                                                                                                                                                                                                                    theorem LeanCert.Core.iteratedDeriv_reflect_of_contDiffOn {f : ℝ → ℝ} {c : ℝ} {n : ℕ} {U : Set ℝ} (hU_open : IsOpen U) (hf : ContDiffOn ℝ (↑n) f U) (t : ℝ) (ht : 2 * c - t ∈ U) :
                                                                                                                                                                                                                    iteratedDeriv n (fun (s : ℝ) => f (2 * c - s)) t = (-1) ^ n * iteratedDeriv n f (2 * c - t)

                                                                                                                                                                                                                    Key lemma for reflection: derivatives of g(t) = f(2c - t) when f is smooth on an open set.

                                                                                                                                                                                                                    This is a local version of iteratedDeriv_reflect that works with ContDiffOn on an open set rather than global ContDiff.

                                                                                                                                                                                                                    theorem LeanCert.Core.taylor_remainder_bound_on_x_lt_c {f : ℝ → ℝ} {a b c : ℝ} {m : ℕ} {M : ℝ} {U : Set ℝ} (hU_open : IsOpen U) (hI_sub : Set.Icc a b ⊆ U) (hcb : c ≤ b) (hf : ContDiffOn ℝ (↑m + 1) f U) (hM : ∀ y ∈ Set.Icc a b, ‖iteratedDeriv (m + 1) f y‖ ≤ M) (x : ℝ) (hx : x ∈ Set.Icc a b) (hxc : x < c) :
                                                                                                                                                                                                                    ‖f x - ∑ i ∈ Finset.range (m + 1), iteratedDeriv i f c / ↑i.factorial * (x - c) ^ i‖ ≤ M * |x - c| ^ (m + 1) / ↑(m + 1).factorial

                                                                                                                                                                                                                    Taylor remainder bound for x < c case with ContDiffOn hypothesis.

                                                                                                                                                                                                                    For functions that are ContDiffOn on an open set containing [a, b], this provides the same Lagrange remainder bound as the global ContDiff version.

                                                                                                                                                                                                                    The proof uses reflection: define g(t) = f(2c - t), apply Lagrange to g on [c, 2c-x], then convert back.

                                                                                                                                                                                                                    theorem LeanCert.Core.taylor_remainder_bound_on {f : ℝ → ℝ} {a b c : ℝ} {n : ℕ} {M : ℝ} {U : Set ℝ} (hU_open : IsOpen U) (hI_sub : Set.Icc a b ⊆ U) (hca : a ≤ c) (hcb : c ≤ b) (hf : ContDiffOn ℝ (↑n) f U) (hM : ∀ x ∈ Set.Icc a b, ‖iteratedDeriv n f x‖ ≤ M) (_hMnonneg : 0 ≤ M) (x : ℝ) :
                                                                                                                                                                                                                    x ∈ Set.Icc a b → ‖f x - ∑ i ∈ Finset.range n, iteratedDeriv i f c / ↑i.factorial * (x - c) ^ i‖ ≤ M * |x - c| ^ n / ↑n.factorial

                                                                                                                                                                                                                    Combined Taylor remainder bound with ContDiffOn hypothesis.

                                                                                                                                                                                                                    For functions that are ContDiffOn on an open set containing [a, b], this provides the Lagrange remainder bound for any x ∈ [a, b] and center c ∈ [a, b].

                                                                                                                                                                                                                    theorem LeanCert.Core.iteratedDeriv_reflect {f : ℝ → ℝ} {c : ℝ} {n : ℕ} (hf : ContDiff ℝ (↑n) f) (t : ℝ) :
                                                                                                                                                                                                                    iteratedDeriv n (fun (s : ℝ) => f (2 * c - s)) t = (-1) ^ n * iteratedDeriv n f (2 * c - t)

                                                                                                                                                                                                                    Key lemma: derivatives of reflected function g(t) = f(2c - t).

                                                                                                                                                                                                                    For the x < c case, we use reflection: define g(t) = f(2c - t), apply Lagrange to g on [c, 2c-x], then convert back. This lemma shows how g's derivatives relate to f's derivatives.

                                                                                                                                                                                                                    theorem LeanCert.Core.neg_one_pow_mul_self (n : ℕ) :
                                                                                                                                                                                                                    (-1) ^ n * (-1) ^ n = 1

                                                                                                                                                                                                                    Auxiliary lemma: (-1)^n * (-1)^n = 1 for any natural n.

                                                                                                                                                                                                                    theorem LeanCert.Core.taylor_remainder_bound_c_lt_x {f : ℝ → ℝ} {a b c : ℝ} {m : ℕ} {M : ℝ} (hca : a ≤ c) (hf : ContDiff ℝ (↑m + 1) f) (hM : ∀ y ∈ Set.Icc a b, ‖iteratedDeriv (m + 1) f y‖ ≤ M) (x : ℝ) (hx : x ∈ Set.Icc a b) (hcx : c < x) :
                                                                                                                                                                                                                    ‖f x - ∑ i ∈ Finset.range (m + 1), iteratedDeriv i f c / ↑i.factorial * (x - c) ^ i‖ ≤ M * |x - c| ^ (m + 1) / ↑(m + 1).factorial

                                                                                                                                                                                                                    Taylor remainder bound for c < x case (Lagrange form).

                                                                                                                                                                                                                    For c < x, we apply taylor_mean_remainder_lagrange on [c, x] and convert iteratedDerivWithin to iteratedDeriv using the helper lemmas above.

                                                                                                                                                                                                                    theorem LeanCert.Core.taylor_remainder_bound_x_lt_c {f : ℝ → ℝ} {a b c : ℝ} {m : ℕ} {M : ℝ} (hcb : c ≤ b) (hf : ContDiff ℝ (↑m + 1) f) (hM : ∀ y ∈ Set.Icc a b, ‖iteratedDeriv (m + 1) f y‖ ≤ M) (x : ℝ) (hx : x ∈ Set.Icc a b) (hxc : x < c) :
                                                                                                                                                                                                                    ‖f x - ∑ i ∈ Finset.range (m + 1), iteratedDeriv i f c / ↑i.factorial * (x - c) ^ i‖ ≤ M * |x - c| ^ (m + 1) / ↑(m + 1).factorial

                                                                                                                                                                                                                    Taylor remainder bound for x < c case (Lagrange form via reflection).

                                                                                                                                                                                                                    For x < c, we define g(t) = f(2c - t), apply taylor_mean_remainder_lagrange on [c, 2c-x], then use iteratedDeriv_reflect to convert back to f's derivatives. The key insight is that g's Taylor expansion at c, evaluated at 2c-x, equals f's Taylor expansion at c, evaluated at x, because the (-1)^i factors from the derivatives cancel with the (-1)^i factors from the powers.

                                                                                                                                                                                                                    theorem LeanCert.Core.taylor_remainder_bound {f : ℝ → ℝ} {a b c : ℝ} {n : ℕ} {M : ℝ} (_hab : a ≤ b) (hca : a ≤ c) (hcb : c ≤ b) (hf : ContDiff ℝ (↑n) f) (hM : ∀ x ∈ Set.Icc a b, ‖iteratedDeriv n f x‖ ≤ M) (_hMnonneg : 0 ≤ M) (x : ℝ) :
                                                                                                                                                                                                                    x ∈ Set.Icc a b → ‖f x - ∑ i ∈ Finset.range n, iteratedDeriv i f c / ↑i.factorial * (x - c) ^ i‖ ≤ M * |x - c| ^ n / ↑n.factorial

                                                                                                                                                                                                                    Lagrange form remainder bound for Taylor approximation.

                                                                                                                                                                                                                    If |f^(n)(x)| ≤ M for all x in [a, b], and c ∈ [a, b], then the Taylor polynomial of degree n-1 (sum over range n) satisfies: for any x ∈ [a, b]: |f(x) - T_{n-1}(x; c)| ≤ M * |x - c|^n / n!

                                                                                                                                                                                                                    Note: The sum ∑ i ∈ Finset.range n gives terms 0..n-1 (degree n-1 polynomial). The remainder involves the n-th derivative, matching our bound on iteratedDeriv n f.

                                                                                                                                                                                                                    All cases are fully proved:

                                                                                                                                                                                                                    Common Taylor expansions #

                                                                                                                                                                                                                    Taylor coefficients for exp at 0: 1/n!

                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                      Taylor coefficients for sin at 0

                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                        Taylor coefficients for cos at 0

                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                          Derivative bounds for common functions #

                                                                                                                                                                                                                          theorem LeanCert.Core.exp_deriv_bound {a b : ℝ} (_hab : a ≤ b) (n : ℕ) (x : ℝ) :

                                                                                                                                                                                                                          All derivatives of exp are bounded by exp on any bounded interval

                                                                                                                                                                                                                          All derivatives of sin and cos are bounded by 1. The derivatives cycle: sin → cos → -sin → -cos → sin → ...

                                                                                                                                                                                                                          cosh x ≤ exp |x| for all x

                                                                                                                                                                                                                          |sinh x| ≤ cosh x for all x

                                                                                                                                                                                                                          All derivatives of sinh and cosh are bounded by exp(max(|a|, |b|)) on [a, b]. The derivatives cycle: sinh → cosh → sinh → cosh → ...

                                                                                                                                                                                                                          theorem LeanCert.Core.iteratedDeriv_log {n : ℕ} (hn : n ≠ 0) {x : ℝ} (hx : 0 < x) :
                                                                                                                                                                                                                          iteratedDeriv n Real.log x = (-1) ^ (n - 1) * ↑(n - 1).factorial * x ^ (-↑n)

                                                                                                                                                                                                                          Rational Endpoint Intervals - Computable Taylor Series #

                                                                                                                                                                                                                          This file provides computable interval enclosures for transcendental functions using Taylor series with rational coefficients and rigorous remainder bounds.

                                                                                                                                                                                                                          Main definitions #

                                                                                                                                                                                                                          Main theorems #

                                                                                                                                                                                                                          Design notes #

                                                                                                                                                                                                                          All definitions in this file use only rational arithmetic and are fully computable. The proofs connect these to the real-valued functions via Taylor's theorem.

                                                                                                                                                                                                                          Computable Taylor series helpers #

                                                                                                                                                                                                                          Compute n! as a Rational

                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                            @[irreducible]

                                                                                                                                                                                                                            Compute the integer power of an interval using exponentiation by squaring. O(log n) interval multiplications instead of O(n).

                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                              Compute the absolute value interval: |I| = [0, max(|lo|, |hi|)] if 0 ∈ I, or [min(|lo|,|hi|), max(|lo|,|hi|)] otherwise

                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                Maximum absolute value of an interval

                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                  Evaluate Taylor series ∑_{i=0}^{n} c_i * x^i at interval I using Horner's method. Computes c₀ + I * (c₁ + I * (c₂ + ... + I * cₙ)), which is mathematically equivalent to the direct sum but uses fewer operations and often gives tighter bounds by reducing the dependency problem in interval arithmetic.

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

                                                                                                                                                                                                                                    Computable exp via Taylor series #

                                                                                                                                                                                                                                    Tail-recursive exp coefficient generator. expTaylorCoeffsAux n k c produces n+1 coefficients starting at index k, assuming c = 1 / k!.

                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                      Taylor coefficients for exp: 1/i! for i = 0, 1, ..., n. Implemented iteratively to avoid repeated factorial recomputation.

                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                        Computable exp remainder bound using rational arithmetic. The Lagrange remainder is exp(ξ) * x^{n+1} / (n+1)! where ξ is between 0 and x. We use e < 3, so e^r ≤ 3^(⌈r⌉+1) as a conservative bound.

                                                                                                                                                                                                                                        Returns an interval [-R, R] where R bounds the remainder.

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

                                                                                                                                                                                                                                          The raw rational Taylor enclosure of the exponential at a point.

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

                                                                                                                                                                                                                                            Heuristic reduction factor for exp evaluation. We choose k = log2(ceil(|q|) + 1), so 2^k grows roughly with |q|. No correctness depends on the specific choice; it only affects performance.

                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                              Computable interval enclosure for exp at a single rational point. Uses argument reduction: exp(q) = exp(q/2^k)^(2^k).

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

                                                                                                                                                                                                                                                Point exponential using Taylor coefficients prepared for depth n.

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

                                                                                                                                                                                                                                                  Hull of two intervals: smallest interval containing both.

                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                    theorem LeanCert.Core.IntervalRat.mem_hull_left {x : ℝ} {I J : IntervalRat} (hx : x ∈ I) :
                                                                                                                                                                                                                                                    x ∈ I.hull J

                                                                                                                                                                                                                                                    Membership in hull

                                                                                                                                                                                                                                                    Computable interval enclosure for exp using Taylor series with monotonicity optimization.

                                                                                                                                                                                                                                                    exp(x) = ∑_{i=0}^{n} x^i/i! + R where |R| ≤ exp(|x|) * |x|^{n+1} / (n+1)!

                                                                                                                                                                                                                                                    For intervals not crossing 0, we use endpoint evaluation and take the hull, which is tighter than direct Taylor evaluation due to interval widening.

                                                                                                                                                                                                                                                    This is fully computable using only rational arithmetic.

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

                                                                                                                                                                                                                                                      Interval exponential using Taylor coefficients prepared for depth n.

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

                                                                                                                                                                                                                                                        Computable sin via Taylor series #

                                                                                                                                                                                                                                                        Taylor coefficients for sin: 0, 1, 0, -1/6, 0, 1/120, ...

                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                          Computable sin remainder bound. Since |sin^{(k)}(x)| ≤ 1 for all k, x, the remainder is bounded by |x|^{n+1}/(n+1)!

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

                                                                                                                                                                                                                                                            Computable interval enclosure for sin using Taylor series.

                                                                                                                                                                                                                                                            sin(x) = ∑_{k=0}^{n/2} (-1)^k x^{2k+1}/(2k+1)! + R where |R| ≤ |x|^{n+1}/(n+1)! since all derivatives of sin are bounded by 1.

                                                                                                                                                                                                                                                            We intersect with [-1, 1] for tighter bounds on small intervals.

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

                                                                                                                                                                                                                                                              Interval sine using Taylor coefficients prepared for depth n.

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

                                                                                                                                                                                                                                                                Computable cos via Taylor series #

                                                                                                                                                                                                                                                                Taylor coefficients for cos: 1, 0, -1/2, 0, 1/24, 0, ...

                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                  Computable cos remainder bound. Since |cos^{(k)}(x)| ≤ 1 for all k, x, the remainder is bounded by |x|^{n+1}/(n+1)!

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

                                                                                                                                                                                                                                                                    Computable interval enclosure for cos using Taylor series.

                                                                                                                                                                                                                                                                    cos(x) = ∑_{k=0}^{n/2} (-1)^k x^{2k}/(2k)! + R where |R| ≤ |x|^{n+1}/(n+1)! since all derivatives of cos are bounded by 1.

                                                                                                                                                                                                                                                                    We intersect with [-1, 1] for tighter bounds on small intervals.

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

                                                                                                                                                                                                                                                                      Interval cosine using Taylor coefficients prepared for depth n.

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

                                                                                                                                                                                                                                                                        Computable sinh and cosh via exp #

                                                                                                                                                                                                                                                                        Computable interval enclosure for sinh at a single rational point. Uses the definition sinh(q) = (exp(q) - exp(-q)) / 2.

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

                                                                                                                                                                                                                                                                          Computable interval enclosure for cosh at a single rational point. Uses the definition cosh(q) = (exp(q) + exp(-q)) / 2.

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

                                                                                                                                                                                                                                                                            The lower bound of coshPointComputable is always at least 1.

                                                                                                                                                                                                                                                                            Computable interval enclosure for sinh using exp with endpoint evaluation.

                                                                                                                                                                                                                                                                            sinh(x) = (exp(x) - exp(-x)) / 2 Since sinh is strictly monotone increasing, sinh([a,b]) = [sinh(a), sinh(b)]. We use endpoint evaluation for tight bounds.

                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                              Computable interval enclosure for cosh using exp with endpoint evaluation.

                                                                                                                                                                                                                                                                              cosh(x) = (exp(x) + exp(-x)) / 2 cosh has minimum 1 at x = 0, and is symmetric: cosh(-x) = cosh(x).

                                                                                                                                                                                                                                                                              • cosh is decreasing on (-∞, 0]
                                                                                                                                                                                                                                                                              • cosh is increasing on [0, ∞)

                                                                                                                                                                                                                                                                              We use endpoint evaluation with monotonicity for tight bounds.

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

                                                                                                                                                                                                                                                                                FTIA for pow #

                                                                                                                                                                                                                                                                                theorem LeanCert.Core.IntervalRat.mem_pow {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (n : ℕ) :
                                                                                                                                                                                                                                                                                x ^ n ∈ I.pow n

                                                                                                                                                                                                                                                                                FTIA for interval power (binary exponentiation version)

                                                                                                                                                                                                                                                                                Helper lemmas for Taylor series membership #

                                                                                                                                                                                                                                                                                Any x in I has |x| ≤ maxAbs I

                                                                                                                                                                                                                                                                                theorem LeanCert.Core.IntervalRat.abs_le_mem_symmetric_interval {x : ℝ} {R : ℚ} (hR : 0 ≤ R) (h : |x| ≤ ↑R) :
                                                                                                                                                                                                                                                                                x ∈ { lo := -R, hi := R, le := ⋯ }

                                                                                                                                                                                                                                                                                If |x| ≤ R for nonnegative R, then x ∈ [-R, R]. This is the key micro-lemma for embedding Lagrange remainder bounds into intervals.

                                                                                                                                                                                                                                                                                theorem LeanCert.Core.IntervalRat.domain_from_abs_bound {x : ℝ} {r : ℚ} (_hr : 0 ≤ r) (habs : |x| ≤ ↑r) :
                                                                                                                                                                                                                                                                                x ∈ Set.Icc ↑(-r) ↑r

                                                                                                                                                                                                                                                                                Domain setup for Taylor theorem: if |x| ≤ r for nonnegative r, then x ∈ [-r, r] as an Icc with the required inequalities.

                                                                                                                                                                                                                                                                                theorem LeanCert.Core.IntervalRat.domain_from_mem {x : ℝ} {I : IntervalRat} (hx : x ∈ I) :
                                                                                                                                                                                                                                                                                have r := I.maxAbs; 0 ≤ ↑r ∧ |x| ≤ ↑r ∧ x ∈ Set.Icc ↑(-r) ↑r ∧ ↑(-r) ≤ 0 ∧ 0 ≤ ↑r ∧ ↑(-r) ≤ ↑r

                                                                                                                                                                                                                                                                                Combined domain setup from interval membership.

                                                                                                                                                                                                                                                                                theorem LeanCert.Core.IntervalRat.remainder_to_interval {v : ℝ} {R : ℚ} (hbound : |v| ≤ ↑R) :
                                                                                                                                                                                                                                                                                v ∈ { lo := -R, hi := R, le := ⋯ }

                                                                                                                                                                                                                                                                                Convert an absolute value bound |v| ≤ R to interval membership v ∈ [-R, R]. This is the key micro-lemma for the final step of Taylor remainder bounds.

                                                                                                                                                                                                                                                                                theorem LeanCert.Core.IntervalRat.exp_bound_by_pow3 {r : ℚ} (_hr : 0 ≤ r) {ξ : ℝ} (hξ : |ξ| ≤ ↑r) :

                                                                                                                                                                                                                                                                                Key lemma: exp(ξ) ≤ 3^(⌈r⌉+1) for |ξ| ≤ r

                                                                                                                                                                                                                                                                                Coefficient matching lemmas #

                                                                                                                                                                                                                                                                                For exp, all iterated derivatives at 0 equal 1.

                                                                                                                                                                                                                                                                                Helper lemmas for Taylor series membership #

                                                                                                                                                                                                                                                                                theorem LeanCert.Core.IntervalRat.mem_evalTaylorSeries {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (coeffs : List ℚ) :
                                                                                                                                                                                                                                                                                (List.map (fun (x_1 : ℚ × ℕ) => match x_1 with | (c, i) => ↑c * x ^ i) coeffs.zipIdx).sum ∈ evalTaylorSeries coeffs I

                                                                                                                                                                                                                                                                                General FTIA for evalTaylorSeries (Horner version): if coeffs has length n+1, then ∑_{i=0}^{n} coeffs[i] * x^i ∈ evalTaylorSeries coeffs I for x ∈ I.

                                                                                                                                                                                                                                                                                The exp Taylor polynomial value matches our evalTaylorSeries. The proof shows that our list-based polynomial evaluation produces the same sum as the Finset.sum form used in Mathlib's Taylor theorem.

                                                                                                                                                                                                                                                                                The sin Taylor polynomial value matches our evalTaylorSeries. Key: iteratedDeriv i sin 0 = 0, 1, 0, -1, 0, 1, ... matches sinTaylorCoeffs.

                                                                                                                                                                                                                                                                                The cos Taylor polynomial value matches our evalTaylorSeries. Key: iteratedDeriv i cos 0 = 1, 0, -1, 0, 1, 0, ... matches cosTaylorCoeffs.

                                                                                                                                                                                                                                                                                Taylor remainder micro-lemmas #

                                                                                                                                                                                                                                                                                Unified Taylor remainder bound for exp: given x ∈ I with r = maxAbs I, the Taylor remainder |exp x - poly(x)| ≤ 3^(⌈r⌉+1) * r^(n+1) / (n+1)!. This encapsulates the domain setup and remainder calculation.

                                                                                                                                                                                                                                                                                Unified Taylor remainder bound for sin: given x ∈ I with r = maxAbs I, the Taylor remainder |sin x - poly(x)| ≤ r^(n+1) / (n+1)!. Uses the fact that |sin^(k)(x)| ≤ 1 for all k, x.

                                                                                                                                                                                                                                                                                Unified Taylor remainder bound for cos: given x ∈ I with r = maxAbs I, the Taylor remainder |cos x - poly(x)| ≤ r^(n+1) / (n+1)!. Uses the fact that |cos^(k)(x)| ≤ 1 for all k, x.

                                                                                                                                                                                                                                                                                FTIA for computable functions #

                                                                                                                                                                                                                                                                                FTIA for single-point exp: Real.exp q ∈ expPointComputable q n

                                                                                                                                                                                                                                                                                FTIA for sinComputable: Real.sin x ∈ sinComputable I n for any x ∈ I.

                                                                                                                                                                                                                                                                                The proof uses the Taylor remainder micro-lemma and the global bound sin ∈ [-1, 1].

                                                                                                                                                                                                                                                                                FTIA for cosComputable: Real.cos x ∈ cosComputable I n for any x ∈ I.

                                                                                                                                                                                                                                                                                The proof uses the Taylor remainder micro-lemma and the global bound cos ∈ [-1, 1].

                                                                                                                                                                                                                                                                                FTIA for sinhPointComputable: Real.sinh q ∈ sinhPointComputable q n

                                                                                                                                                                                                                                                                                FTIA for coshPointComputable: Real.cosh q ∈ coshPointComputable q n

                                                                                                                                                                                                                                                                                FTIA for sinhComputable: Real.sinh x ∈ sinhComputable I n for any x ∈ I.

                                                                                                                                                                                                                                                                                Uses endpoint evaluation and monotonicity of sinh.

                                                                                                                                                                                                                                                                                FTIA for coshComputable: Real.cosh x ∈ coshComputable I n for any x ∈ I.

                                                                                                                                                                                                                                                                                Uses endpoint evaluation and monotonicity properties of cosh.

                                                                                                                                                                                                                                                                                Computable atanh via Taylor series #

                                                                                                                                                                                                                                                                                For |y| < 1, atanh(y) = y + y³/3 + y⁵/5 + ... We compute this series for y ∈ [-1/3, 1/3] where it converges rapidly.

                                                                                                                                                                                                                                                                                Taylor coefficients for atanh: 0, 1, 0, 1/3, 0, 1/5, ... atanh(y) = Σ y^(2k+1)/(2k+1) = y + y³/3 + y⁵/5 + ...

                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                  Computable atanh remainder bound. For |y| ≤ r < 1, the remainder after n terms is bounded by r^(n+1)/(1 - r²). We use a conservative bound: r^(n+1) / ((n+1) * (1 - r)) for simplicity.

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

                                                                                                                                                                                                                                                                                    Computable interval enclosure for atanh at a single rational point. Requires |q| < 1 for convergence. For |q| ≤ 1/3, this is very accurate.

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

                                                                                                                                                                                                                                                                                      Point atanh using Taylor coefficients prepared for depth n.

                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                        theorem LeanCert.Core.IntervalRat.Real.atanh_hasSum' {x : ℝ} (hx : |x| < 1) :
                                                                                                                                                                                                                                                                                        HasSum (fun (k : ℕ) => x ^ (2 * k + 1) / (2 * ↑k + 1)) (Real.atanh x)

                                                                                                                                                                                                                                                                                        The atanh series: atanh(x) = Σ_{k=0}^∞ x^(2k+1)/(2k+1) for |x| < 1. Derived from Mathlib's hasSum_log_sub_log_of_abs_lt_one.

                                                                                                                                                                                                                                                                                        The atanh Taylor polynomial membership: the partial sum of atanh coefficients at q is in evalTaylorSeries (atanhTaylorCoeffs n) (singleton q).

                                                                                                                                                                                                                                                                                        theorem LeanCert.Core.IntervalRat.atanh_taylor_remainder_in_interval {q : ℚ} (hq : |↑q| < 1) (n : ℕ) :
                                                                                                                                                                                                                                                                                        Real.atanh ↑q - (List.map (fun (x : ℚ × ℕ) => match x with | (c, i) => ↑c * ↑q ^ i) (atanhTaylorCoeffs n).zipIdx).sum ∈ atanhRemainderBoundComputable |q| n

                                                                                                                                                                                                                                                                                        FTIA for atanhPointComputable: Real.atanh q ∈ atanhPointComputable q n for |q| < 1.

                                                                                                                                                                                                                                                                                        Computable ln(2) via atanh #

                                                                                                                                                                                                                                                                                        ln(2) = 2 * atanh(1/3), since: 2 = (1 + 1/3) / (1 - 1/3) = (4/3) / (2/3) So atanh(1/3) = (1/2) * ln(2), giving ln(2) = 2 * atanh(1/3)

                                                                                                                                                                                                                                                                                        Compute ln(2) as an interval using 2 * atanh(1/3). This converges rapidly since atanh series at 1/3 has |y| = 1/3.

                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                          FTIA for ln2Computable: Real.log 2 ∈ ln2Computable n. Uses the identity log(2) = 2 * atanh(1/3) from log_via_atanh.

                                                                                                                                                                                                                                                                                          Computable log via argument reduction #

                                                                                                                                                                                                                                                                                          For q > 0, we compute:

                                                                                                                                                                                                                                                                                          1. Reduce q to m * 2^k where m ∈ [1/2, 2]
                                                                                                                                                                                                                                                                                          2. Compute log(m) = 2 * atanh((m-1)/(m+1)), which has |arg| ≤ 1/3
                                                                                                                                                                                                                                                                                          3. Result = log(m) + k * ln(2)

                                                                                                                                                                                                                                                                                          Reduction exponent k such that q * 2^(-k) ≈ 1

                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                            Computable log at a single rational point q > 0. Returns log(q) = log(m) + k * ln(2) where m = q * 2^(-k).

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

                                                                                                                                                                                                                                                                                              Logarithm evaluation using all configuration-dependent data prepared for depth n.

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

                                                                                                                                                                                                                                                                                                Computable interval enclosure for log using endpoint evaluation. Since log is strictly increasing on (0, ∞), we evaluate at endpoints.

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

                                                                                                                                                                                                                                                                                                  Interval logarithm using all data prepared for depth n.

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

                                                                                                                                                                                                                                                                                                    FTIA for logPointComputable

                                                                                                                                                                                                                                                                                                    theorem LeanCert.Core.IntervalRat.mem_logComputable {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (hpos : 0 < I.lo) (n : ℕ) :

                                                                                                                                                                                                                                                                                                    FTIA for logComputable: if x ∈ I and I.lo > 0, then log(x) ∈ logComputable I n

                                                                                                                                                                                                                                                                                                    theorem LeanCert.Core.IntervalRat.mem_logComputable' {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (hpos : 0 < I.lo) (n : ℕ) :

                                                                                                                                                                                                                                                                                                    Conditional version of mem_logComputable for use in correctness proofs. Requires I.lo > 0 so the log interval is well-defined and monotone.

                                                                                                                                                                                                                                                                                                    Computable erf via Taylor series #

                                                                                                                                                                                                                                                                                                    Interval containing 2/√π ≈ 1.128379... Used for erf calculations. 2/√π is in (1.128, 1.129).

                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                      Taylor coefficients for erf (without the 2/√π factor): erf(x) = (2/√π) * Σ_{n=0}^∞ (-1)^n * x^(2n+1) / (n! * (2n+1))

                                                                                                                                                                                                                                                                                                      So the coefficient of x^k is:

                                                                                                                                                                                                                                                                                                      • 0 if k is even
                                                                                                                                                                                                                                                                                                      • (-1)^((k-1)/2) / (((k-1)/2)! * k) if k is odd
                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                        Computable erf remainder bound. Since |erf^{(k)}(x)| ≤ (2/√π) * 2^k for all x (rough bound), and erf is bounded by 1, we use a combination.

                                                                                                                                                                                                                                                                                                        For the Taylor remainder centered at 0, we use: |R_n(x)| ≤ sup|f^{(n+1)}(ξ)| * |x|^{n+1} / (n+1)!

                                                                                                                                                                                                                                                                                                        A conservative bound: |erf^{(k)}(x)| ≤ (2/√π) * k! / (k/2)! ≤ 2 * k^{k/2} But since |erf| ≤ 1, we can intersect with [-1, 1].

                                                                                                                                                                                                                                                                                                        We use: remainder ≤ 2 * |x|^{n+1} / (n+1)! (very conservative).

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

                                                                                                                                                                                                                                                                                                          Computable interval enclosure for erf at a single rational point. Uses sign-aware clipped linear bounds: |erf(q)| ≤ min(1, (2257/2000)*|q|).

                                                                                                                                                                                                                                                                                                          Cases:

                                                                                                                                                                                                                                                                                                          • q < 0 => erf(q) ∈ [-1, 0]
                                                                                                                                                                                                                                                                                                          • q = 0 => erf(q) = 0
                                                                                                                                                                                                                                                                                                          • q > 0 => erf(q) ∈ [0, 1]

                                                                                                                                                                                                                                                                                                          with tighter near-zero magnitude via (2257/2000)*|q|.

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

                                                                                                                                                                                                                                                                                                            Computable interval enclosure for erf using Taylor series with monotonicity.

                                                                                                                                                                                                                                                                                                            erf(x) = (2/√π) * Σ_{n=0}^∞ (-1)^n * x^(2n+1) / (n! * (2n+1))

                                                                                                                                                                                                                                                                                                            Since erf is strictly monotone increasing (erf'(x) = (2/√π)e^{-x²} > 0), we use endpoint evaluation: erf([a,b]) ⊆ [erf(a), erf(b)].

                                                                                                                                                                                                                                                                                                            We intersect with [-1, 1] for safety.

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

                                                                                                                                                                                                                                                                                                              2/√π is in the interval twoDivSqrtPi. 2/√π ≈ 1.1283791670955126, which is in (1.128, 1.129).

                                                                                                                                                                                                                                                                                                              This is a helper theorem for correctness proofs. The computation of erfComputable is independent of this theorem.

                                                                                                                                                                                                                                                                                                              noncomputable def LeanCert.Core.IntervalRat.erfInner (x : ℝ) :

                                                                                                                                                                                                                                                                                                              The "inner" erf function without the 2/√π factor: erfInner(x) = ∫₀ˣ exp(-t²) dt = (√π/2) * erf(x)

                                                                                                                                                                                                                                                                                                              This is the function whose Taylor series coefficients are erfTaylorCoeffs.

                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                erf(x) = (2/√π) * erfInner(x)

                                                                                                                                                                                                                                                                                                                The derivatives of erfInner(x) = ∫₀ˣ exp(-t²) dt. erfInner'(x) = exp(-x²) erfInner''(x) = -2x * exp(-x²) etc.

                                                                                                                                                                                                                                                                                                                exp(-x²) is smooth.

                                                                                                                                                                                                                                                                                                                exp(-x²) is analytic everywhere.

                                                                                                                                                                                                                                                                                                                exp(-x²) is analytic on ℝ.

                                                                                                                                                                                                                                                                                                                Computable atanh interval via endpoint evaluation #

                                                                                                                                                                                                                                                                                                                Computable interval enclosure for atanh using endpoint evaluation. Since atanh is strictly increasing on (-1, 1), we evaluate at endpoints. Requires the interval to be strictly inside (-1, 1); returns a wide fallback otherwise.

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

                                                                                                                                                                                                                                                                                                                  Interval atanh using Taylor coefficients prepared for depth n.

                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                    theorem LeanCert.Core.IntervalRat.mem_atanhComputable {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (hlo : -1 < I.lo) (hhi : I.hi < 1) (n : ℕ) :

                                                                                                                                                                                                                                                                                                                    FTIA for atanhComputable: if x ∈ I and I ⊂ (-1, 1), then atanh(x) ∈ atanhComputable I n.

                                                                                                                                                                                                                                                                                                                    Rational Endpoint Intervals #

                                                                                                                                                                                                                                                                                                                    This file defines IntervalRat, a concrete interval type with rational endpoints suitable for computation. We prove the Fundamental Theorem of Interval Arithmetic (FTIA) for each operation.

                                                                                                                                                                                                                                                                                                                    Module Structure #

                                                                                                                                                                                                                                                                                                                    Main definitions #

                                                                                                                                                                                                                                                                                                                    Main theorems #

                                                                                                                                                                                                                                                                                                                    Design notes #

                                                                                                                                                                                                                                                                                                                    All operations maintain the invariant lo ≤ hi. Domain restrictions for partial operations (like inv) are encoded via separate types or explicit hypotheses.

                                                                                                                                                                                                                                                                                                                    Dyadic Intervals #

                                                                                                                                                                                                                                                                                                                    Intervals with Dyadic endpoints. These support "Outward Rounding", ensuring mathematical soundness even when we limit numerical precision.

                                                                                                                                                                                                                                                                                                                    Main definitions #

                                                                                                                                                                                                                                                                                                                    Design notes #

                                                                                                                                                                                                                                                                                                                    The key feature is roundOut: after each operation, we can enforce a minimum exponent to prevent precision explosion. When rounding:

                                                                                                                                                                                                                                                                                                                    This maintains the containment invariant: the rounded interval always contains the original interval, which contains the true mathematical value.

                                                                                                                                                                                                                                                                                                                    Performance #

                                                                                                                                                                                                                                                                                                                    In v1.0, Rat multiplication of 1/3 * 1/3 * ... * 1/3 (10 times) creates a denominator of 3^10 = 59049. Each operation requires GCD computation.

                                                                                                                                                                                                                                                                                                                    In v1.1, with precision = -10, the denominator stays fixed at 2^10 = 1024. The result is slightly less tight but computed significantly faster.

                                                                                                                                                                                                                                                                                                                    An interval with Dyadic endpoints.

                                                                                                                                                                                                                                                                                                                    Maintains invariant: lo.toRat ≤ hi.toRat

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

                                                                                                                                                                                                                                                                                                                        Membership and Sets #

                                                                                                                                                                                                                                                                                                                        The set of reals contained in this interval

                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                          @[instance_reducible]

                                                                                                                                                                                                                                                                                                                          Membership in a Dyadic interval

                                                                                                                                                                                                                                                                                                                          Equations

                                                                                                                                                                                                                                                                                                                          Conversion to IntervalRat #

                                                                                                                                                                                                                                                                                                                          Convert to IntervalRat for verification with existing theorems

                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                            Membership is preserved by conversion to IntervalRat

                                                                                                                                                                                                                                                                                                                            Construction #

                                                                                                                                                                                                                                                                                                                            Create a singleton interval from a Dyadic

                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                              A Dyadic value is in its singleton interval

                                                                                                                                                                                                                                                                                                                              Create an interval, checking the invariant

                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                The width of an interval

                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                  @[simp]

                                                                                                                                                                                                                                                                                                                                  The dyadic width denotes endpoint subtraction exactly.

                                                                                                                                                                                                                                                                                                                                  Exact midpoint of a dyadic interval.

                                                                                                                                                                                                                                                                                                                                  Dyadics are closed under division by two, so midpoint construction must lower the exponent rather than shift (and potentially round) the mantissa.

                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                    @[simp]

                                                                                                                                                                                                                                                                                                                                    The dyadic midpoint denotes the ordinary rational midpoint exactly.

                                                                                                                                                                                                                                                                                                                                    The lower endpoint is at most the exact midpoint.

                                                                                                                                                                                                                                                                                                                                    The exact midpoint is at most the upper endpoint.

                                                                                                                                                                                                                                                                                                                                    Split a dyadic interval into two exact closed halves.

                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                      theorem LeanCert.Core.IntervalDyadic.mem_bisect_left {x : ℝ} {I : IntervalDyadic} (hx : x ∈ I) (hm : x ≤ ↑I.midpoint.toRat) :
                                                                                                                                                                                                                                                                                                                                      x ∈ I.bisect.1

                                                                                                                                                                                                                                                                                                                                      A point in the original interval and left of the midpoint is in the left half.

                                                                                                                                                                                                                                                                                                                                      theorem LeanCert.Core.IntervalDyadic.mem_bisect_right {x : ℝ} {I : IntervalDyadic} (hx : x ∈ I) (hm : ↑I.midpoint.toRat ≤ x) :
                                                                                                                                                                                                                                                                                                                                      x ∈ I.bisect.2

                                                                                                                                                                                                                                                                                                                                      A point in the original interval and right of the midpoint is in the right half.

                                                                                                                                                                                                                                                                                                                                      Membership in the left half implies membership in the original interval.

                                                                                                                                                                                                                                                                                                                                      Membership in the right half implies membership in the original interval.

                                                                                                                                                                                                                                                                                                                                      The two closed halves cover the original interval, including their shared seam.

                                                                                                                                                                                                                                                                                                                                      Both closed halves contain the midpoint seam.

                                                                                                                                                                                                                                                                                                                                      The overlap of the two closed children is exactly their midpoint seam.

                                                                                                                                                                                                                                                                                                                                      The left child has exactly half the semantic width of its parent.

                                                                                                                                                                                                                                                                                                                                      The right child has exactly half the semantic width of its parent.

                                                                                                                                                                                                                                                                                                                                      Outward Rounding #

                                                                                                                                                                                                                                                                                                                                      Outward rounding: enforces a maximum precision (minimum exponent).

                                                                                                                                                                                                                                                                                                                                      This is the key operation for preventing precision explosion. minExp is the minimum allowed exponent (higher = coarser precision).

                                                                                                                                                                                                                                                                                                                                      For example, minExp = -10 ensures all values are multiples of 2^(-10) ≈ 0.001.

                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                                        theorem LeanCert.Core.IntervalDyadic.roundOut_contains {x : ℝ} {I : IntervalDyadic} (hx : x ∈ I) (minExp : ℤ) :
                                                                                                                                                                                                                                                                                                                                        x ∈ I.roundOut minExp

                                                                                                                                                                                                                                                                                                                                        roundOut produces an interval containing the original

                                                                                                                                                                                                                                                                                                                                        Interval Negation #

                                                                                                                                                                                                                                                                                                                                        Negate an interval

                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                          FTIA for negation

                                                                                                                                                                                                                                                                                                                                          Interval Addition #

                                                                                                                                                                                                                                                                                                                                          Add two intervals

                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                            theorem LeanCert.Core.IntervalDyadic.mem_add {x y : ℝ} {I J : IntervalDyadic} (hx : x ∈ I) (hy : y ∈ J) :
                                                                                                                                                                                                                                                                                                                                            x + y ∈ I.add J

                                                                                                                                                                                                                                                                                                                                            FTIA for addition

                                                                                                                                                                                                                                                                                                                                            Add with precision control

                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                              Interval Subtraction #

                                                                                                                                                                                                                                                                                                                                              Subtract two intervals

                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                                theorem LeanCert.Core.IntervalDyadic.mem_sub {x y : ℝ} {I J : IntervalDyadic} (hx : x ∈ I) (hy : y ∈ J) :
                                                                                                                                                                                                                                                                                                                                                x - y ∈ I.sub J

                                                                                                                                                                                                                                                                                                                                                FTIA for subtraction

                                                                                                                                                                                                                                                                                                                                                Interval Multiplication #

                                                                                                                                                                                                                                                                                                                                                Multiply two intervals.

                                                                                                                                                                                                                                                                                                                                                Uses min/max of all four endpoint products to handle signs correctly. This is the exact multiplication - mantissas may grow. Use mulRounded or mulNormalized for controlled precision.

                                                                                                                                                                                                                                                                                                                                                Correctness: For x ∈ [a,b] and y ∈ [c,d], the product x*y lies in the interval [min(ac,ad,bc,bd), max(ac,ad,bc,bd)].

                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                  Fast interval multiplication using sign-based case splitting. Reduces from 4 multiplications + 12 comparisons to 2 multiplications in the common case (both intervals positive or both negative). Falls back to the full 4-way product for mixed-sign intervals.

                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                    theorem LeanCert.Core.IntervalDyadic.mem_mul {x y : ℝ} {I J : IntervalDyadic} (hx : x ∈ I) (hy : y ∈ J) :
                                                                                                                                                                                                                                                                                                                                                    x * y ∈ I.mul J

                                                                                                                                                                                                                                                                                                                                                    FTIA for multiplication

                                                                                                                                                                                                                                                                                                                                                    theorem LeanCert.Core.IntervalDyadic.mem_mulFast {x y : ℝ} {I J : IntervalDyadic} (hx : x ∈ I) (hy : y ∈ J) :
                                                                                                                                                                                                                                                                                                                                                    x * y ∈ I.mulFast J

                                                                                                                                                                                                                                                                                                                                                    mulFast preserves the containment property of mul. This is retained as documentation and a future audited optimization hook; production certificate checking currently uses mul directly.

                                                                                                                                                                                                                                                                                                                                                    Multiply with precision control (outward rounding)

                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                      Multiply with mantissa normalization (prevents bit explosion)

                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                        Interval Scaling #

                                                                                                                                                                                                                                                                                                                                                        Scale an interval by a constant Dyadic

                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                          Scale by a power of 2 (very efficient: just adjusts exponents)

                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                            Square Root #

                                                                                                                                                                                                                                                                                                                                                            Square root of an interval. Returns a conservative bound [0, max(hi, 1)]. This is sound because:

                                                                                                                                                                                                                                                                                                                                                            • sqrt(x) = 0 for x < 0 (by definition in Mathlib)
                                                                                                                                                                                                                                                                                                                                                            • sqrt(x) ≥ 0 for all x
                                                                                                                                                                                                                                                                                                                                                            • sqrt(x) ≤ max(x, 1) for x ≥ 0 Therefore for any x ∈ [lo, hi], sqrt(x) ∈ [0, max(hi, 1)].
                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                              theorem LeanCert.Core.IntervalDyadic.mem_sqrt {x : ℝ} {I : IntervalDyadic} (hx : x ∈ I) (hx_nn : 0 ≤ x) (prec : ℤ) :
                                                                                                                                                                                                                                                                                                                                                              √x ∈ I.sqrt prec

                                                                                                                                                                                                                                                                                                                                                              Soundness of interval sqrt: if x ∈ I, x ≥ 0, then Real.sqrt x ∈ sqrt I

                                                                                                                                                                                                                                                                                                                                                              theorem LeanCert.Core.IntervalDyadic.mem_sqrt' {x : ℝ} {I : IntervalDyadic} (hx : x ∈ I) (prec : ℤ) :
                                                                                                                                                                                                                                                                                                                                                              √x ∈ I.sqrt prec

                                                                                                                                                                                                                                                                                                                                                              General soundness of interval sqrt for any real input. Handles both non-negative inputs and negative inputs (where Real.sqrt returns 0).

                                                                                                                                                                                                                                                                                                                                                              Comparison and Containment #

                                                                                                                                                                                                                                                                                                                                                              Check if entire interval is positive

                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                Check if entire interval is negative

                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                  Check if I ⊆ J

                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                    Check if the upper bound is ≤ a rational

                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                      Check if a rational is ≤ the lower bound

                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                        Upper bound extraction from membership

                                                                                                                                                                                                                                                                                                                                                                        Lower bound extraction from membership

                                                                                                                                                                                                                                                                                                                                                                        What upperBoundedBy means: the interval's hi endpoint is ≤ q

                                                                                                                                                                                                                                                                                                                                                                        What lowerBoundedBy means: q is ≤ the interval's lo endpoint

                                                                                                                                                                                                                                                                                                                                                                        Helper for Transcendentals #

                                                                                                                                                                                                                                                                                                                                                                        Convert from IntervalRat (for transcendental results)

                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                                          theorem LeanCert.Core.IntervalDyadic.mem_ofIntervalRat {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (prec : ℤ) (hprec : prec ≤ 0 := by norm_num) :

                                                                                                                                                                                                                                                                                                                                                                          If x ∈ IntervalRat I, then x ∈ ofIntervalRat I prec (outward rounding preserves membership). Requires precision ≤ 0 (e.g. -53).

                                                                                                                                                                                                                                                                                                                                                                          Intervals with Real Endpoints #

                                                                                                                                                                                                                                                                                                                                                                          This file defines IntervalReal, an interval type with real (ℝ) endpoints. Unlike IntervalRat (which has rational endpoints and is suitable for computation), IntervalReal allows us to represent intervals involving transcendental values like [1, Real.exp 1] or [Real.log 2, π].

                                                                                                                                                                                                                                                                                                                                                                          Main definitions #

                                                                                                                                                                                                                                                                                                                                                                          Main theorems #

                                                                                                                                                                                                                                                                                                                                                                          Design notes #

                                                                                                                                                                                                                                                                                                                                                                          This type complements IntervalRat for proving facts about transcendental functions. While IntervalRat is used for numerical computation (since rationals are computable), IntervalReal is used for correctness proofs involving exp, log, etc.

                                                                                                                                                                                                                                                                                                                                                                          Typical workflow:

                                                                                                                                                                                                                                                                                                                                                                          1. Use IntervalRat for actual interval arithmetic computations
                                                                                                                                                                                                                                                                                                                                                                          2. Convert to IntervalReal when proving facts about transcendental functions
                                                                                                                                                                                                                                                                                                                                                                          3. Use mathlib's analysis lemmas directly on real intervals

                                                                                                                                                                                                                                                                                                                                                                          An interval with real endpoints

                                                                                                                                                                                                                                                                                                                                                                          • lo : ℝ

                                                                                                                                                                                                                                                                                                                                                                            Lower endpoint of the interval.

                                                                                                                                                                                                                                                                                                                                                                          • hi : ℝ

                                                                                                                                                                                                                                                                                                                                                                            Upper endpoint of the interval.

                                                                                                                                                                                                                                                                                                                                                                          • le : self.lo ≤ self.hi
                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                            The set of reals contained in this interval

                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                                              @[instance_reducible]

                                                                                                                                                                                                                                                                                                                                                                              Membership in an interval

                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                              @[simp]

                                                                                                                                                                                                                                                                                                                                                                              Create an interval from a single real

                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                Convert from IntervalRat to IntervalReal

                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                  Interval addition #

                                                                                                                                                                                                                                                                                                                                                                                  Add two intervals

                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                                                    theorem LeanCert.Core.IntervalReal.mem_add {x y : ℝ} {I J : IntervalReal} (hx : x ∈ I) (hy : y ∈ J) :
                                                                                                                                                                                                                                                                                                                                                                                    x + y ∈ I.add J

                                                                                                                                                                                                                                                                                                                                                                                    FTIA for addition

                                                                                                                                                                                                                                                                                                                                                                                    Interval negation #

                                                                                                                                                                                                                                                                                                                                                                                    Negate an interval

                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                                                      theorem LeanCert.Core.IntervalReal.mem_neg {x : ℝ} {I : IntervalReal} (hx : x ∈ I) :
                                                                                                                                                                                                                                                                                                                                                                                      -x ∈ I.neg

                                                                                                                                                                                                                                                                                                                                                                                      FTIA for negation

                                                                                                                                                                                                                                                                                                                                                                                      Interval multiplication #

                                                                                                                                                                                                                                                                                                                                                                                      The minimum of four real endpoints, used for interval multiplication.

                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                        The maximum of four real endpoints, used for interval multiplication.

                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                          Multiply two intervals

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

                                                                                                                                                                                                                                                                                                                                                                                            Exponential interval #

                                                                                                                                                                                                                                                                                                                                                                                            Interval bound for exp. Since exp is strictly increasing, exp([a,b]) = [exp(a), exp(b)].

                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                              FTIA for exp: if x ∈ [a,b], then exp(x) ∈ [exp(a), exp(b)]. This is FULLY PROVED - no sorry, no axioms.

                                                                                                                                                                                                                                                                                                                                                                                              Logarithm interval (for positive intervals) #

                                                                                                                                                                                                                                                                                                                                                                                              An interval that is strictly positive

                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                Interval bound for log on positive intervals. Since log is strictly increasing on (0, ∞), log([a,b]) = [log(a), log(b)] for a > 0.

                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                  FTIA for log: if x ∈ [a,b] with a > 0, then log(x) ∈ [log(a), log(b)]. This is FULLY PROVED - no sorry, no axioms.

                                                                                                                                                                                                                                                                                                                                                                                                  Trigonometric intervals (global bounds) #

                                                                                                                                                                                                                                                                                                                                                                                                  Interval bound for sin. Since |sin x| ≤ 1 for all x, we use [-1, 1].

                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                                                    Interval bound for cos. Since |cos x| ≤ 1 for all x, we use [-1, 1].

                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                      Interval bound for atan. Since arctan x ∈ (-π/2, π/2) ⊂ [-2, 2] for all x.

                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                                        |arsinh x| ≤ |x| for all x. This follows from MVT and |arsinh'| ≤ 1.

                                                                                                                                                                                                                                                                                                                                                                                                        Interval bound for arsinh. Uses a conservative bound based on input interval.

                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                                          Hyperbolic function intervals #

                                                                                                                                                                                                                                                                                                                                                                                                          Interval bound for sinh. Since sinh is strictly monotonic increasing, sinh([a,b]) = [sinh(a), sinh(b)].

                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                                            FTIA for sinh: if x ∈ [a,b], then sinh(x) ∈ [sinh(a), sinh(b)]. This is FULLY PROVED - no sorry, no axioms.

                                                                                                                                                                                                                                                                                                                                                                                                            Interval bound for cosh. cosh is convex with minimum at 0:

                                                                                                                                                                                                                                                                                                                                                                                                            • If interval is all non-negative: cosh is increasing
                                                                                                                                                                                                                                                                                                                                                                                                            • If interval is all non-positive: cosh is decreasing
                                                                                                                                                                                                                                                                                                                                                                                                            • If interval contains 0: minimum is cosh(0) = 1, max is at endpoints
                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                              FTIA for cosh: if x ∈ [a,b], then cosh(x) ∈ coshInterval([a,b]). This is FULLY PROVED - no sorry, no axioms.

                                                                                                                                                                                                                                                                                                                                                                                                              Square root interval #

                                                                                                                                                                                                                                                                                                                                                                                                              Interval bound for sqrt. For any interval I, sqrt(x) ∈ [0, max(hi, 1)] for x ∈ I. This is always sound because:

                                                                                                                                                                                                                                                                                                                                                                                                              • sqrt(x) ≥ 0 for all x (Mathlib convention: sqrt(negative) = 0)
                                                                                                                                                                                                                                                                                                                                                                                                              • sqrt(x) ≤ max(x, 1) for x ≥ 0, so sqrt(x) ≤ max(hi, 1)
                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                FTIA for sqrt: if x ∈ I, then sqrt(x) ∈ sqrtInterval(I). Works for all x including negative (where sqrt returns 0 by Mathlib convention).

                                                                                                                                                                                                                                                                                                                                                                                                                Shared Trigonometric Range Reduction #

                                                                                                                                                                                                                                                                                                                                                                                                                Common rational π bounds and interval-shifting proofs used by IntervalRat and Taylor-model trigonometric evaluators.

                                                                                                                                                                                                                                                                                                                                                                                                                Rational approximations of π and 2π #

                                                                                                                                                                                                                                                                                                                                                                                                                Lower bound for π: 314159265/100000000 < π

                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                  Upper bound for π: π < 355/113

                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                    piRatLo < π, proved from Mathlib's decimal π bounds.

                                                                                                                                                                                                                                                                                                                                                                                                                    π < piRatHi, proved from Mathlib's decimal π bounds.

                                                                                                                                                                                                                                                                                                                                                                                                                    Range reduction #

                                                                                                                                                                                                                                                                                                                                                                                                                    Compute the shift amount k such that I.midpoint - k * 2π is approximately in [-π, π].

                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                      Shift an interval by subtracting k * 2π using rational bounds.

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

                                                                                                                                                                                                                                                                                                                                                                                                                        Correctness of range reduction #

                                                                                                                                                                                                                                                                                                                                                                                                                        If x ∈ I, then x - 2πk ∈ shiftInterval I k.

                                                                                                                                                                                                                                                                                                                                                                                                                        Convenience form: if x ∈ I, then x - 2πk ∈ (reduceToMainPeriod I).1.

                                                                                                                                                                                                                                                                                                                                                                                                                        Computable Range Reduction for Trigonometric Functions #

                                                                                                                                                                                                                                                                                                                                                                                                                        This file implements range reduction for sin and cos to improve Taylor series convergence for intervals far from 0.

                                                                                                                                                                                                                                                                                                                                                                                                                        Problem #

                                                                                                                                                                                                                                                                                                                                                                                                                        Standard Taylor series for sin/cos centered at 0 have remainder bounds of |x|^{n+1} / (n+1)!. For intervals far from 0 (e.g., [10, 11]), this remainder is huge even for moderate n.

                                                                                                                                                                                                                                                                                                                                                                                                                        Solution: Range Reduction #

                                                                                                                                                                                                                                                                                                                                                                                                                        Use the periodicity of sin/cos:

                                                                                                                                                                                                                                                                                                                                                                                                                        By choosing k to bring x - 2πk into [-π, π], the Taylor series converges much faster since |x - 2πk| ≤ π ≈ 3.14.

                                                                                                                                                                                                                                                                                                                                                                                                                        Main definitions #

                                                                                                                                                                                                                                                                                                                                                                                                                        Shared range-reduction API #

                                                                                                                                                                                                                                                                                                                                                                                                                        The rational lower π bound from the trigonometric reduction implementation.

                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                          The rational upper π bound from the trigonometric reduction implementation.

                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                            The rational lower bound for twice π used in argument reduction.

                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                              The rational upper bound for twice π used in argument reduction.

                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                Choose the integer number of periods used to reduce an input interval.

                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                  Shift an interval by the selected integer multiple of the period enclosure.

                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                    Computable reduced evaluation #

                                                                                                                                                                                                                                                                                                                                                                                                                                    Computable sin evaluation with range reduction.

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

                                                                                                                                                                                                                                                                                                                                                                                                                                      Computable cos evaluation with range reduction.

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

                                                                                                                                                                                                                                                                                                                                                                                                                                        sin x ∈ sinComputableReduced I for all x ∈ I

                                                                                                                                                                                                                                                                                                                                                                                                                                        cos x ∈ cosComputableReduced I for all x ∈ I

                                                                                                                                                                                                                                                                                                                                                                                                                                        Computable Interval Evaluation #

                                                                                                                                                                                                                                                                                                                                                                                                                                        This file implements the computable interval evaluator for LeanCert.Core.Expr. Given an expression and intervals for its variables, we compute an interval guaranteed to contain all possible values.

                                                                                                                                                                                                                                                                                                                                                                                                                                        Main definitions #

                                                                                                                                                                                                                                                                                                                                                                                                                                        Design notes #

                                                                                                                                                                                                                                                                                                                                                                                                                                        This evaluator is COMPUTABLE, allowing use of native_decide for bound checking in tactics. The transcendental functions (exp, sin, cos) use Taylor series with configurable depth for precision control.

                                                                                                                                                                                                                                                                                                                                                                                                                                        For inv: computes bounds using invInterval, but correctness is not covered by evalIntervalCore_correct. Use evalIntervalOption for inv.

                                                                                                                                                                                                                                                                                                                                                                                                                                        Interval bounds for transcendental functions #

                                                                                                                                                                                                                                                                                                                                                                                                                                        Simple interval bound for sin. Since |sin x| ≤ 1 for all x, we use the global bound [-1, 1]. This is sound but not tight.

                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                          Correctness of sin interval: sin x ∈ [-1, 1] for all x

                                                                                                                                                                                                                                                                                                                                                                                                                                          Simple interval bound for cos. Since |cos x| ≤ 1 for all x, we use the global bound [-1, 1]. This is sound but not tight.

                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                            Correctness of cos interval: cos x ∈ [-1, 1] for all x

                                                                                                                                                                                                                                                                                                                                                                                                                                            Simple interval bound for atan. Since atan x ∈ (-π/2, π/2) for all x, we use the global bound [-2, 2]. This is sound but not tight (π/2 ≈ 1.57).

                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                              Correctness of atan interval: arctan x ∈ [-2, 2] for all x

                                                                                                                                                                                                                                                                                                                                                                                                                                              Interval bound for erf using computable Taylor series. erf(x) = (2/√π) * ∫₀ˣ exp(-t²) dt, strictly monotone increasing. This computes tight bounds using verified Taylor series.

                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                erf is strictly monotone increasing. Proof: erf'(x) = (2/√π) * exp(-x²) > 0 for all x.

                                                                                                                                                                                                                                                                                                                                                                                                                                                We use that for a < b, the integral ∫_{a}^{b} exp(-t²) dt > 0 since the integrand is strictly positive.

                                                                                                                                                                                                                                                                                                                                                                                                                                                Correctness of erfPointComputable. The enclosure is sign-aware and uses monotonicity of erf with erf(0)=0.

                                                                                                                                                                                                                                                                                                                                                                                                                                                theorem LeanCert.Engine.mem_erfInterval {x : ℝ} {I : Core.IntervalRat} (hx : x ∈ I) (n : ℕ := 15) :

                                                                                                                                                                                                                                                                                                                                                                                                                                                Correctness of erf interval using monotonicity and endpoint evaluation.

                                                                                                                                                                                                                                                                                                                                                                                                                                                Since erf is strictly monotone increasing:

                                                                                                                                                                                                                                                                                                                                                                                                                                                • For x ∈ [I.lo, I.hi], we have erf(I.lo) ≤ erf(x) ≤ erf(I.hi)
                                                                                                                                                                                                                                                                                                                                                                                                                                                • erfPointComputable(I.lo) contains erf(I.lo)
                                                                                                                                                                                                                                                                                                                                                                                                                                                • erfPointComputable(I.hi) contains erf(I.hi)
                                                                                                                                                                                                                                                                                                                                                                                                                                                • hull of these intervals contains [erf(I.lo), erf(I.hi)]
                                                                                                                                                                                                                                                                                                                                                                                                                                                • Therefore erf(x) ∈ hull(...) ∩ [-1, 1]

                                                                                                                                                                                                                                                                                                                                                                                                                                                Simple interval bound for arsinh. arsinh is unbounded, so we use a very rough linear bound. We use max(|lo|, |hi|) + 1 as a safe bound that always works.

                                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                  Correctness of arsinh interval. Uses the bound |arsinh x| ≤ |x| for all x (from IntervalRealEndpoints).

                                                                                                                                                                                                                                                                                                                                                                                                                                                  Interval bound for atanh. atanh is defined for (-1, 1). If interval is within this range, we compute tight bounds using monotonicity. Otherwise returns default.

                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                    theorem LeanCert.Engine.mem_atanhInterval {x : ℝ} {I : Core.IntervalRat} (hx : x ∈ I) (hlo : -1 < I.lo) (hhi : I.hi < 1) :

                                                                                                                                                                                                                                                                                                                                                                                                                                                    Correctness of atanh interval: when x ∈ I and I ⊂ (-1, 1), atanh(x) ∈ atanhInterval I.

                                                                                                                                                                                                                                                                                                                                                                                                                                                    Tight interval bound for tanh. Since tanh(x) ∈ (-1, 1) for all x ∈ ℝ, we use the global bound [-1, 1]. This avoids the interval explosion that occurs when desugaring to exp.

                                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                      Correctness of tanh interval: tanh x ∈ [-1, 1] for all x

                                                                                                                                                                                                                                                                                                                                                                                                                                                      Interval enclosure for π. Uses tight bounds from Mathlib's pi_gt_d20 and pi_lt_d20 which give 20 decimal digits. 3.14159265358979323846 < π < 3.14159265358979323847

                                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                        Correctness of pi interval: Real.pi ∈ piInterval

                                                                                                                                                                                                                                                                                                                                                                                                                                                        Interval enclosure for the Euler–Mascheroni constant γ. Tight bounds derived from eulerMascheroniSeq 100 < γ < eulerMascheroniSeq' 100 combined with explicit Taylor partial sums for log. The proofs below are axiom-free (no native_decide): all rational arithmetic is certified by norm_num, and the only analytic inputs are Mathlib's abs_log_sub_add_sum_range_le and the d9 bounds on log 2.

                                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                          Correctness of Euler–Mascheroni interval: γ ∈ eulerMascheroniInterval

                                                                                                                                                                                                                                                                                                                                                                                                                                                          Centralized interval lookup for named mathematical constants. Extending this table is the ONLY change needed to add a new constant.

                                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                            Correctness: the real value of every named constant is in its interval.

                                                                                                                                                                                                                                                                                                                                                                                                                                                            Interval bound for sinh using computable Taylor series for exp. sinh(x) = (exp(x) - exp(-x)) / 2, and sinh is strictly monotonic. This computes tight bounds using the verified exp implementation.

                                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                              Interval bound for cosh using computable Taylor series for exp. cosh(x) = (exp(x) + exp(-x)) / 2, with minimum 1 at x = 0. This computes tight bounds using the verified exp implementation.

                                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                Interval inverse #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                Wide bound constant for when inverse is undefined (denominator contains 0)

                                                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Computable interval inverse. For [a,b] with a > 0: returns [1/b, 1/a] (1/x is decreasing on positive reals) For [a,b] with b < 0: returns [1/b, 1/a] (1/x is decreasing on negative reals) For intervals containing 0: returns wide bounds [-M, M]. NOTE: this branch is NOT a sound enclosure of x⁻¹ in general (1/x is unbounded near 0); the correctness theorem mem_invInterval therefore requires the extra hypothesis |x⁻¹| ≤ invWideBound in that case.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                    theorem LeanCert.Engine.mem_invInterval_pos {x : ℝ} {I : Core.IntervalRat} (hx : x ∈ I) (hpos : I.lo > 0) :

                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Correctness of invInterval when denominator interval is positive. For x ∈ [a,b] with a > 0, we have 1/x ∈ [1/b, 1/a]

                                                                                                                                                                                                                                                                                                                                                                                                                                                                    theorem LeanCert.Engine.mem_invInterval_neg {x : ℝ} {I : Core.IntervalRat} (hx : x ∈ I) (hneg : I.hi < 0) :

                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Correctness of invInterval when denominator interval is negative. For x ∈ [a,b] with b < 0, we have 1/x ∈ [1/b, 1/a]

                                                                                                                                                                                                                                                                                                                                                                                                                                                                    theorem LeanCert.Engine.mem_invInterval_wide {x : ℝ} {I : Core.IntervalRat} (_hx : x ∈ I) (hlo : ¬I.lo > 0) (hhi : ¬I.hi < 0) (hbnd : |x⁻¹| ≤ ↑invWideBound) :

                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Correctness of invInterval when denominator interval contains zero. Requires a bound on |x⁻¹| to be provable, since x can be arbitrarily close to 0.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Main correctness theorem for invInterval. Fully proved for intervals bounded away from zero. For intervals containing zero, requires a bound on |x⁻¹|.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                    theorem LeanCert.Engine.mem_invInterval_nonzero {x : ℝ} {I : Core.IntervalRat} (hx : x ∈ I) (hnonzero : I.lo > 0 ∨ I.hi < 0) :

                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Correctness of invInterval for intervals bounded away from zero (no extra hypothesis needed)

                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Core interval evaluation (computable) #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                    @[reducible, inline]

                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Variable assignment as intervals

                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Configuration for interval evaluation parameters. This allows certificates to specify the required precision.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                      • taylorDepth : ℕ

                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Number of Taylor series terms for transcendental functions

                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                            @[instance_reducible]

                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Default evaluation configuration with 10 Taylor terms

                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations

                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Internal total evaluator for the theorem-restricted core expression fragment.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                            For expressions in ExprSupportedCore, this computes correct interval bounds with a fully-verified proof (given domain validity conditions).

                                                                                                                                                                                                                                                                                                                                                                                                                                                                            For inv: computes bounds using invInterval, but correctness is not covered by evalIntervalCore_correct. Use evalIntervalOption for inv.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                            For log: uses logComputable with Taylor series. Correctness requires that the argument interval is positive (see evalDomainValid).

                                                                                                                                                                                                                                                                                                                                                                                                                                                                            This evaluator is COMPUTABLE, allowing use of native_decide for bound checking in tactics. The transcendental functions (exp, sin, cos, log) use Taylor series with configurable depth for precision control.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                              def LeanCert.Engine.envMem (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) :

                                                                                                                                                                                                                                                                                                                                                                                                                                                                              A real environment is contained in an interval environment

                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Domain validity predicate for expressions with domain restrictions.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                For log: requires the argument interval to be strictly positive. This ensures that logComputable returns correct bounds.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                For other expressions: always true (no domain restrictions).

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Single-variable domain validity

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Computable (decidable) check for domain validity

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Single-variable domain check

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        checkDomainValid = true implies evalDomainValid

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        checkDomainValid1 = true implies evalDomainValid1

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        evalDomainValid is equivalent to checkDomainValid = true

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        @[instance_reducible]

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Decidability instance for domain validity

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        @[instance_reducible]

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Decidability instance for single-variable domain validity

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        ADSupported expressions (which don't include log) always have valid domains. This is because only log has domain restrictions (positive argument).

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Single-variable version of domainValid for ADSupported

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        theorem LeanCert.Engine.evalIntervalCore_correct (e : Core.Expr) (hsupp : ExprSupportedCore e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (hρ : envMem ρ_real ρ_int) (cfg : EvalConfig := { }) (hdom : evalDomainValid e ρ_int cfg) :

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Fundamental correctness theorem for core evaluation.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        This theorem is FULLY PROVED for core expressions (no sorry, no axioms). The hsupp hypothesis ensures we only consider expressions in the computable verified subset. The hdom hypothesis ensures domain validity (e.g., log arguments are positive). Works for any Taylor depth.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Convenience functions #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Computable single-variable evaluation for core expressions

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          theorem LeanCert.Engine.evalIntervalCore1_correct (e : Core.Expr) (hsupp : ExprSupportedCore e) (x : ℝ) (I : Core.IntervalRat) (hx : x ∈ I) (cfg : EvalConfig := { }) (hdom : evalDomainValid1 e I cfg) :

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Correctness for single-variable core evaluation

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Smart constructors for supported expressions #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Build a constant expression (always supported)

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Build a variable expression (always supported)

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Build an addition (supported if both operands are supported)

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Build a multiplication (supported if both operands are supported)

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Build a negation (supported if operand is supported)

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Build a sin (supported if operand is supported)

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Build a cos (supported if operand is supported)

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Build an exp (supported if operand is supported)

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Checked evaluation results #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Certified evaluators return a finite enclosure only after all partial-domain conditions have been checked. Failures are data: callers must propagate them instead of substituting a finite sentinel that could be mistaken for an enclosure.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Why a checked evaluator could not produce a finite certified enclosure.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                @[reducible, inline]

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Result type used by checked evaluators and public computation APIs.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Extended (Noncomputable) Interval Evaluation #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  This file implements the noncomputable interval evaluator for LeanCert.Core.Expr, supporting exp with floor/ceil bounds and partial evaluation for inv/log.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Main definitions #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Design notes #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  The extended evaluator uses Real.exp with floor/ceil bounds, which requires noncomputability. For computability, use LeanCert.Internal.Rational.evalTotalCore instead.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  The partial evaluator evalIntervalOption returns none when:

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  When it returns some I, correctness is guaranteed.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Extended interval evaluation (noncomputable, supports exp) #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Noncomputable interval evaluator supporting exp.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  For supported expressions (const, var, add, mul, neg, sin, cos, exp), this computes correct interval bounds with a fully-verified proof.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  For unsupported expressions (inv, log), returns a default interval. Do not rely on results for expressions containing inv or log. Use evalIntervalOption for partial functions like inv and log.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  This evaluator is NONCOMPUTABLE due to exp using Real.exp with floor/ceil.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    theorem LeanCert.Engine.evalInterval_correct (e : Core.Expr) (hsupp : ADSupported e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (hρ : envMem ρ_real ρ_int) :

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Fundamental correctness theorem for extended evaluation.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    This theorem is FULLY PROVED (no sorry, no axioms) for supported expressions. The hsupp hypothesis ensures we only consider expressions in the verified subset.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Convenience functions #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Note: LeanCert.Internal.Rational.evalTotalCore now uses Taylor series for exp/sin/cos, which gives different (often tighter) intervals than evalInterval's floor/ceil bounds. Both are correct, but they are not necessarily equal.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    For purely algebraic expressions (const, var, add, mul, neg), both evaluators give identical results.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Correctness for single-variable extended evaluation

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Partial interval evaluation with inv support #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Partial (Option-returning) interval evaluator supporting inv.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    For expressions with inv, this evaluator returns none if the denominator interval contains zero, and some I with a correct enclosure otherwise.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    This allows safe interval evaluation of expressions like 1/x when we can verify the denominator is bounded away from zero.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    For expressions without inv, this always returns some with the same result as evalInterval.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      The Taylor truncation depth used by the checked exponential evaluator.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Taylor depth used by the strict atanh evaluator.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Evaluate an expression by rational intervals, failing when a domain check fails.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            theorem LeanCert.Engine.evalIntervalOption_correct (e : Core.Expr) (ρ_int : IntervalEnv) (I : Core.IntervalRat) (hsome : evalIntervalOption e ρ_int = some I) (ρ_real : ℕ → ℝ) (hρ : envMem ρ_real ρ_int) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Core.Expr.eval ρ_real e ∈ I

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Main correctness theorem for evalIntervalOption (approach 1 from plan).

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            When evalIntervalOption returns some I:

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            1. The expression evaluates to a value in I for all ρ_real ∈ ρ_int
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            2. All inv denominators along the evaluation are guaranteed nonzero (because their intervals don't contain zero)

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            This follows your suggestion to keep ADSupported syntactic and add separate semantic hypotheses. The key insight is that if evalIntervalOption succeeds (returns Some), the interval arithmetic has already verified that no denominator interval contains zero.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Checked API with diagnostics #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            @[irreducible]

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Diagnose the first partial-domain failure after evalIntervalOption returned none. This function is deliberately separate from the trusted computation: soundness depends only on successful evalIntervalOption, while diagnostics may be refined without changing the correctness theorem.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Checked rational evaluator. Every successful result is a certified finite enclosure; domain-invalid expressions return a structured error.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                theorem LeanCert.Engine.evalIntervalChecked_correct (e : Core.Expr) (ρ_int : IntervalEnv) (I : Core.IntervalRat) (hsuccess : evalIntervalChecked e ρ_int = Except.ok I) (ρ_real : ℕ → ℝ) (hρ : envMem ρ_real ρ_int) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Core.Expr.eval ρ_real e ∈ I

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Success of evalIntervalChecked is sufficient for enclosure correctness for every expression constructor.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Checked Rational evaluation with a tight path for the verified computable core. Unsupported syntax or a failed core-domain check falls back to the general checked evaluator, preserving its structured domain errors.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem LeanCert.Engine.evalIntervalTightChecked_correct (e : Core.Expr) (ρ_int : IntervalEnv) (cfg : EvalConfig) (I : Core.IntervalRat) (hsuccess : evalIntervalTightChecked e ρ_int cfg = Except.ok I) (ρ_real : ℕ → ℝ) (hρ : envMem ρ_real ρ_int) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Core.Expr.eval ρ_real e ∈ I

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Every successful tight checked Rational evaluation encloses the expression value. The core branch uses the core correctness theorem; the fallback uses the general checked evaluator theorem.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Single-variable version of evalIntervalOption

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    theorem LeanCert.Engine.evalIntervalOption1_correct (e : Core.Expr) (I J : Core.IntervalRat) (hsome : evalIntervalOption1 e I = some J) (x : ℝ) (hx : x ∈ I) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ J

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Correctness for single-variable partial evaluation

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    theorem LeanCert.Engine.evalIntervalOption_le_of_hi (e : Core.Expr) (I J : Core.IntervalRat) (c : ℚ) (hsome : evalIntervalOption1 e I = some J) (hhi : J.hi ≤ c) (x : ℝ) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    When evalIntervalOption succeeds, we get bounds

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    theorem LeanCert.Engine.evalIntervalOption_ge_of_lo (e : Core.Expr) (I J : Core.IntervalRat) (c : ℚ) (hsome : evalIntervalOption1 e I = some J) (hlo : c ≤ J.lo) (x : ℝ) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    x ∈ I → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    When evalIntervalOption succeeds, we get lower bounds

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Semantic Lemmas for Interval Bounds #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    This file provides semantic lemmas for deriving real bounds from certified interval enclosures. Tactics consume these lemmas, but the definitions belong to the engine layer so checked programmatic APIs do not depend on tactic modules.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Main theorems #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Core (computable) lemmas #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Extended (noncomputable) lemmas #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Usage #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    These lemmas are intended to be used by tactics like certify_bound and interval_decide to close goals of the form ∀ x ∈ I, f(x) ≤ c or similar.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    The core lemmas use the computable evaluator and can work with native_decide. The extended lemmas use the noncomputable evaluator with floor/ceil bounds.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Tactic-facing lemmas for interval bounds (core, computable) #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    theorem LeanCert.Engine.exprCore_le_of_interval_hi (e : Core.Expr) (hsupp : ExprSupportedCore e) (I : Core.IntervalRat) (c : ℚ) (cfg : EvalConfig := { }) (hdom : evalDomainValid1 e I cfg) (hhi : (Internal.Rational.evalTotalCore1 e I cfg).hi ≤ c) (x : ℝ) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Upper bound lemma for core expressions (computable). FULLY PROVED - no sorry, no axioms. Accepts configurable Taylor depth. Requires domain validity (e.g., log arguments must be positive).

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    theorem LeanCert.Engine.exprCore_ge_of_interval_lo (e : Core.Expr) (hsupp : ExprSupportedCore e) (I : Core.IntervalRat) (c : ℚ) (cfg : EvalConfig := { }) (hdom : evalDomainValid1 e I cfg) (hlo : c ≤ (Internal.Rational.evalTotalCore1 e I cfg).lo) (x : ℝ) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    x ∈ I → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Lower bound lemma for core expressions (computable). FULLY PROVED - no sorry, no axioms. Accepts configurable Taylor depth. Requires domain validity (e.g., log arguments must be positive).

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    theorem LeanCert.Engine.exprCore_lt_of_interval_hi_lt (e : Core.Expr) (hsupp : ExprSupportedCore e) (I : Core.IntervalRat) (c : ℚ) (cfg : EvalConfig := { }) (hdom : evalDomainValid1 e I cfg) (hhi : (Internal.Rational.evalTotalCore1 e I cfg).hi < c) (x : ℝ) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e < ↑c

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Strict upper bound for core expressions (computable). FULLY PROVED - no sorry, no axioms. Accepts configurable Taylor depth. Requires domain validity (e.g., log arguments must be positive).

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    theorem LeanCert.Engine.exprCore_gt_of_interval_lo_gt (e : Core.Expr) (hsupp : ExprSupportedCore e) (I : Core.IntervalRat) (c : ℚ) (cfg : EvalConfig := { }) (hdom : evalDomainValid1 e I cfg) (hlo : c < (Internal.Rational.evalTotalCore1 e I cfg).lo) (x : ℝ) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    x ∈ I → ↑c < Core.Expr.eval (fun (x_1 : ℕ) => x) e

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Strict lower bound for core expressions (computable). FULLY PROVED - no sorry, no axioms. Accepts configurable Taylor depth. Requires domain validity (e.g., log arguments must be positive).

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Tactic-facing lemmas for interval bounds (extended, noncomputable) #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    theorem LeanCert.Engine.expr_le_of_interval_hi (e : Core.Expr) (hsupp : ADSupported e) (I : Core.IntervalRat) (c : ℚ) (hhi : (Internal.Rational.evalUnchecked1 e I).hi ≤ c) (x : ℝ) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Upper bound lemma for extended expressions. FULLY PROVED - no sorry, no axioms.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    theorem LeanCert.Engine.expr_ge_of_interval_lo (e : Core.Expr) (hsupp : ADSupported e) (I : Core.IntervalRat) (c : ℚ) (hlo : c ≤ (Internal.Rational.evalUnchecked1 e I).lo) (x : ℝ) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    x ∈ I → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Lower bound lemma for extended expressions. FULLY PROVED - no sorry, no axioms.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    theorem LeanCert.Engine.expr_lt_of_interval_hi_lt (e : Core.Expr) (hsupp : ADSupported e) (I : Core.IntervalRat) (c : ℚ) (hhi : (Internal.Rational.evalUnchecked1 e I).hi < c) (x : ℝ) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e < ↑c

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Strict upper bound for extended expressions. FULLY PROVED - no sorry, no axioms.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    theorem LeanCert.Engine.expr_gt_of_interval_lo_gt (e : Core.Expr) (hsupp : ADSupported e) (I : Core.IntervalRat) (c : ℚ) (hlo : c < (Internal.Rational.evalUnchecked1 e I).lo) (x : ℝ) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    x ∈ I → ↑c < Core.Expr.eval (fun (x_1 : ℕ) => x) e

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Strict lower bound for extended expressions. FULLY PROVED - no sorry, no axioms.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    theorem LeanCert.Engine.expr_le_of_mem_interval (e : Core.Expr) (hsupp : ADSupported e) (I : Core.IntervalRat) (c : ℚ) (x : ℝ) (hx : x ∈ I) (hhi : (Internal.Rational.evalUnchecked1 e I).hi ≤ c) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Variant for single point (extended).

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    theorem LeanCert.Engine.expr_ge_of_mem_interval (e : Core.Expr) (hsupp : ADSupported e) (I : Core.IntervalRat) (c : ℚ) (x : ℝ) (hx : x ∈ I) (hlo : c ≤ (Internal.Rational.evalUnchecked1 e I).lo) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Variant for single point (extended).

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Interval Evaluation of Expressions #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    This file re-exports the interval evaluation infrastructure for LeanCert.Core.Expr.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Module structure #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    The implementation is split across several files:

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Main definitions (re-exported) #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Expression support predicates #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Evaluators #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Correctness theorems #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Tactic lemmas #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Design notes #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    The evaluators are split by computability:

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Automatic Differentiation - Basic Definitions #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    This file provides the core types and algebraic operations for forward-mode automatic differentiation using interval arithmetic.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Main definitions #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Dual number with interval components: represents (value, derivative)

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        @[instance_reducible]

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Default DualInterval for unsupported expression branches

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Dual interval for a constant (derivative is zero)

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Dual interval for the constant π (derivative is zero)

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Dual interval for a named mathematical constant (derivative is zero)

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Dual interval for the variable we're differentiating with respect to

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Add two dual intervals

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Multiply two dual intervals (product rule)

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Negate a dual interval

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Inverse of a dual interval (quotient rule: d(1/f) = -f'/f²) Uses invInterval for the value component. For intervals containing zero, returns wide bounds.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Automatic Differentiation - Transcendental Functions #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        This file provides dual interval implementations for transcendental functions, implementing the chain rule for each.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Main definitions #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Total functions (always succeed) #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Partial functions (return Option) #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Dual for sin (chain rule: d(sin f) = cos(f) * f')

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Dual for cos (chain rule: d(cos f) = -sin(f) * f')

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Dual for exp (chain rule: d(exp f) = exp(f) * f')

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              The interval [0, 1] used to bound derivative factors in (0, 1]

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                The derivative factor for arctan: 1/(1+x²) is in [0, 1]

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                The derivative factor for arsinh: 1/√(1+x²) is in [0, 1]

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Dual for atan (chain rule: d(atan f) = f' / (1 + f²))

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Dual for arsinh (chain rule: d(arsinh f) = f' / √(1 + f²))

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Dual for sinh (chain rule: d(sinh f) = cosh(f) * f')

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Dual for cosh (chain rule: d(cosh f) = sinh(f) * f')

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Dual for tanh (chain rule: d(tanh f) = sech²(f) * f' = (1 - tanh²(f)) * f') Since sech²(x) = 1 - tanh²(x) ∈ (0, 1] for all x, we use [0, 1] as bound.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Interval containing 2/√π ≈ 1.128379...

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Dual for erf (chain rule: d(erf f) = (2/√π) * exp(-f²) * f') erf'(x) = (2/√π) * exp(-x²), which is always positive and bounded by 2/√π ≈ 1.13

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

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Computable dual for erf using expComputable

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

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Dual for sqrt (chain rule: d(sqrt f) = f' / (2 * sqrt(f))) sqrt'(x) = 1/(2*sqrt(x)) for x > 0, undefined at x = 0. We use sqrtInterval for the value and a conservative bound for the derivative. Note: The derivative blows up as x → 0+, so this uses a wide conservative bound.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Conservative derivative bound [-1, 1] for sinc derivative

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Dual for sinc (chain rule: d(sinc f) = sinc'(f) * f') sinc'(x) = (x cos x - sin x) / x² for x ≠ 0, limit 0 at x = 0. We use conservative bound: |sinc'(x)| ≤ 1 for all x.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Partial functions (domain-restricted) #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Partial dual for atanh (chain rule: d(atanh f) = f' / (1 - f²)) Returns None if the value interval is not contained in (-1, 1).

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

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Partial dual for inv (chain rule: d(1/f) = -f'/f²) Returns None if the value interval contains zero.

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

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Partial dual for log (chain rule: d(log f) = f'/f) Returns None if the value interval is not strictly positive.

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

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Compute a conservative upper bound on 1/(2*sqrt(lo)) for lo > 0. Uses the fact that:

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            • For 0 < lo ≤ 1: sqrt(lo) ≥ lo, so 1/(2sqrt(lo)) ≤ 1/(2lo)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            • For lo > 1: sqrt(lo) > 1, so 1/(2*sqrt(lo)) < 1/2
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              theorem LeanCert.Engine.DualInterval.sqrtDerivCoef_bound {x lo : ℝ} (hlo_pos : 0 < lo) (hx_ge : lo ≤ x) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              1 / (2 * √x) ≤ max (1 / (2 * lo)) (1 / 2)

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              For lo > 0, the derivative coefficient 1/(2*sqrt(x)) is bounded above for x ≥ lo.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Partial dual for sqrt (chain rule: d(sqrt f) = f' / (2 * sqrt(f))) Returns None if the value interval is not strictly positive.

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

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Automatic Differentiation - Evaluators #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                This file provides the evaluation functions for automatic differentiation, mapping expressions to dual intervals.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Main definitions #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Dual evaluation #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                @[reducible, inline]

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Environment for dual evaluation

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Evaluate expression in dual interval mode.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  For supported expressions (const, var, add, mul, neg, sin, cos, exp), this computes correct dual interval bounds with a fully-verified proof.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  For unsupported expressions (inv, log), returns a default interval. Do not rely on results for expressions containing inv or log. Use evalDualOption for partial functions like inv and log.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Partial dual evaluation #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Partial dual evaluator that supports domain-checked functions. Returns none if any domain error would occur:

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    • inv of an interval containing zero
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    • log of an interval not strictly positive When it returns some, the result is guaranteed to be correct.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    The total and computable dual evaluators support tanh, but this Option-returning evaluator deliberately keeps tanh disabled until the evalDualOption-specific value/differentiability/derivative correctness path is wired for that constructor.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Single-variable version of evalDualOption

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Single variable differentiation #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Create dual environment for differentiating with respect to variable idx

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          noncomputable def LeanCert.Engine.evalWithDeriv (e : Core.Expr) (ρ : IntervalEnv) (idx : ℕ) :

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Evaluate and differentiate with respect to variable idx

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Get just the derivative interval

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Evaluate and differentiate a single-variable expression

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Automatic Differentiation - Correctness Theorems #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                This file proves the correctness of forward-mode automatic differentiation for supported expressions (ADSupported).

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Main theorems #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Design notes #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                All theorems in this file are FULLY PROVED with no sorry or axioms. The correctness relies on the chain rule for each supported operation.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Correctness #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                theorem LeanCert.Engine.evalDualUnchecked_val_correct (e : Core.Expr) (hsupp : ADSupported e) (ρ_real : ℕ → ℝ) (ρ_dual : DualEnv) (hρ : ∀ (i : ℕ), ρ_real i ∈ (ρ_dual i).val) :

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                The value component is correct for supported expressions.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                This theorem is FULLY PROVED (no sorry, no axioms) for supported expressions. The hsupp hypothesis ensures we only consider expressions in the verified subset.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Single-variable evaluation for derivative proofs #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                @[reducible, inline]
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                noncomputable abbrev LeanCert.Engine.evalFunc1 (e : Core.Expr) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                ℝ → ℝ

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                The function t ↦ Expr.eval (fun _ => t) e for single-variable expressions

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Differentiability of supported expressions #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Supported expressions are differentiable as single-variable functions. This theorem shows that for any supported expression, the function evalFunc1 e is differentiable.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  FULLY PROVED - no sorry, no axioms.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Core derivative correctness micro-lemmas #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Real.cos y is always in cosInterval I (which is [-1, 1]). This micro-lemma encapsulates the fact that cosInterval uses the global bound.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Real.sin y is always in sinInterval I (which is [-1, 1]). This micro-lemma encapsulates the fact that sinInterval uses the global bound.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  -Real.sin y is always in IntervalRat.neg (sinInterval I). This combines the sin global bound with negation for the cos derivative rule.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem LeanCert.Engine.updateVar_mem_mkDualEnv_val (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (idx : ℕ) (x : ℝ) (hx : x ∈ ρ_int idx) (hρ : ∀ (i : ℕ), ρ_real i ∈ ρ_int i) (i : ℕ) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  (ρ_real[idx ↦ x]) i ∈ (mkDualEnv ρ_int idx i).val

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  The key lemma for n-variable AD: updateVar ρ_real idx x respects mkDualEnv ρ_int idx. This encapsulates the repeated proof that appears in mul/exp cases.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  evalFunc1 unfolding lemmas #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem LeanCert.Engine.evalFunc1_add (e₁ e₂ : Core.Expr) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  evalFunc1 (e₁.add e₂) = fun (t : ℝ) => evalFunc1 e₁ t + evalFunc1 e₂ t

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Helper lemma: evalFunc1 for addition unfolds correctly

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem LeanCert.Engine.evalFunc1_add_pi (e₁ e₂ : Core.Expr) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  evalFunc1 (e₁.add e₂) = evalFunc1 e₁ + evalFunc1 e₂

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Helper lemma: evalFunc1 for addition in Pi form

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem LeanCert.Engine.evalFunc1_mul (e₁ e₂ : Core.Expr) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  evalFunc1 (e₁.mul e₂) = fun (t : ℝ) => evalFunc1 e₁ t * evalFunc1 e₂ t

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Helper lemma: evalFunc1 for multiplication unfolds correctly

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem LeanCert.Engine.evalFunc1_mul_pi (e₁ e₂ : Core.Expr) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  evalFunc1 (e₁.mul e₂) = evalFunc1 e₁ * evalFunc1 e₂

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Helper lemma: evalFunc1 for multiplication in Pi form

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Helper lemma: evalFunc1 for negation unfolds correctly

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Helper lemma: evalFunc1 for negation in Pi form

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Helper lemma: evalFunc1 for sin unfolds correctly

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Helper lemma: evalFunc1 for cos unfolds correctly

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Helper lemma: evalFunc1 for exp unfolds correctly

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Helper lemma: evalFunc1 for log unfolds correctly

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Helper lemma: evalFunc1 for atan unfolds correctly

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Helper lemma: evalFunc1 for arsinh unfolds correctly

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Helper lemma: evalFunc1 for atanh unfolds correctly

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Helper lemma: evalFunc1 for sinc unfolds correctly

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Helper lemma: evalFunc1 for erf unfolds correctly

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Helper lemma: evalFunc1 for sqrt unfolds correctly

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  @[simp]
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem LeanCert.Engine.evalFunc1_const (q : ℚ) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  evalFunc1 (Core.Expr.const q) = fun (x : ℝ) => ↑q

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Helper lemma: evalFunc1 for const

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  @[simp]

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Helper lemma: evalFunc1 for var

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  @[simp]

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Helper lemma: evalFunc1 for namedConst (constant function)

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Helper lemma: evalFunc1 for pi (constant function)

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Helper lemma: evalFunc1 for eulerMascheroni (constant function)

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Helper: the dual environment evaluation gives correct derivative. This connects the interval-based AD to actual calculus derivatives.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  FULLY PROVED - no sorry, no axioms.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem LeanCert.Engine.evalDualUnchecked_der_correct (e : Core.Expr) (hsupp : ADSupported e) (I : Core.IntervalRat) (x : ℝ) (hx : x ∈ I) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  deriv (fun (t : ℝ) => Core.Expr.eval (fun (x : ℕ) => t) e) x ∈ (Internal.AD.evalUnchecked e fun (x : ℕ) => DualInterval.varActive I).der

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  The derivative component of dual interval evaluation is correct. For a supported expression evaluated at a point x in the interval I, the derivative of the expression (as a function of x) lies in the computed derivative interval.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  This is the fundamental correctness theorem for forward-mode AD: the derivative bounds computed by interval arithmetic contain the true derivative at every point in the domain.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  FULLY PROVED - no sorry, no axioms.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Generalized n-variable derivative correctness #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem LeanCert.Engine.evalAlong_differentiable (e : Core.Expr) (hsupp : ADSupported e) (ρ : ℕ → ℝ) (idx : ℕ) :

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Helper: evalAlong is differentiable for supported expressions

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem LeanCert.Engine.evalDualUnchecked_der_correct_idx (e : Core.Expr) (hsupp : ADSupported e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (idx : ℕ) (hρ : ∀ (i : ℕ), ρ_real i ∈ ρ_int i) (x : ℝ) (hx : x ∈ ρ_int idx) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  deriv (e.evalAlong ρ_real idx) x ∈ (Internal.AD.evalUnchecked e (mkDualEnv ρ_int idx)).der

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  The derivative of evalAlong with respect to coordinate idx lies in the computed derivative interval from mkDualEnv.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  This is the fundamental n-variable derivative correctness theorem. It shows that for any expression, if we differentiate along coordinate idx while holding all other coordinates fixed according to ρ, the derivative at any point x in the interval ρ_int idx lies in the computed interval.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  FULLY PROVED - no sorry, no axioms.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem LeanCert.Engine.derivInterval_correct_idx (e : Core.Expr) (hsupp : ADSupported e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (idx : ℕ) (hρ : ∀ (i : ℕ), ρ_real i ∈ ρ_int i) (x : ℝ) (hx : x ∈ ρ_int idx) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  deriv (e.evalAlong ρ_real idx) x ∈ derivInterval e ρ_int idx

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Convenience theorem: derivInterval correctness for n-variable expressions. The derivative of evalAlong e ρ idx at any point x in the interval lies in derivInterval e ρ_int idx.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Single-variable expressions #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Predicate: expression only uses variable index 0. This is useful for proving that different environments give the same result when they agree at index 0.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Bridge between the canonical boolean predicate and the proof-carrying UsesOnlyVar0 predicate used by AD correctness lemmas.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    theorem LeanCert.Engine.evalDualUnchecked_congr_at_0 (e : Core.Expr) (h : UsesOnlyVar0 e) (ρ₁ ρ₂ : DualEnv) (heq : ρ₁ 0 = ρ₂ 0) :

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    For expressions using only var 0, LeanCert.Internal.AD.evalUnchecked agrees for environments that match at 0

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    mkDualEnv at index 0 equals varActive at 0

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    For expressions using only var 0, derivInterval equals evalWithDeriv1

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    theorem LeanCert.Engine.evalWithDeriv1_correct (e : Core.Expr) (hsupp : ADSupported e) (I : Core.IntervalRat) (x : ℝ) (hx : x ∈ I) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ (evalWithDeriv1 e I).val ∧ deriv (fun (t : ℝ) => Core.Expr.eval (fun (x : ℕ) => t) e) x ∈ (evalWithDeriv1 e I).der

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Correctness of single-variable derivative bounds

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Automatic Differentiation - Computable Evaluators #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    This file provides computable dual evaluators using Taylor-based approximations for transcendental functions. This enables native_decide for derivative-based bound checking.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Main definitions #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Main theorems #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Computable Dual Evaluation for ExprSupportedCore #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    This section provides a fully computable dual evaluator that uses Taylor-based approximations for transcendental functions. This enables native_decide for derivative-based bound checking.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Computable dual for exp using Taylor series (chain rule: d(exp f) = exp(f) * f')

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Computable dual for sin using Taylor series

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Computable dual for cos using Taylor series

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Computable dual for log using Taylor series via atanh reduction. Chain rule: d(log f) = f' / f

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Computable dual for sinh using Taylor series (chain rule: d(sinh f) = cosh(f) * f')

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Computable dual for cosh using Taylor series (chain rule: d(cosh f) = sinh(f) * f')

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Computable dual for tanh (chain rule: d(tanh f) = sech²(f) * f') Since sech²(x) ∈ (0, 1], we use [0, 1] as a conservative bound.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Computable dual interval evaluator for ExprSupportedCore expressions.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  This uses Taylor series approximations for transcendental functions, making it fully computable and usable with native_decide.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  For inv and log, use evalDualChecked or the bounded-denominator evalDualDyadicChecked; they validate the actual input box before exposing this total kernel's result. Correctness is not claimed for unchecked partial-operation branches here.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Computable single-variable derivative interval

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Domain validity for dual evaluation. This is defined directly in terms of LeanCert.Internal.AD.evalTotalCore to ensure compatibility. For log, we require the argument interval to have positive lower bound.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        theorem LeanCert.Engine.evalDualTotalCore_val_correct (e : Core.Expr) (hsupp : ExprSupportedCore e) (ρ_real : ℕ → ℝ) (ρ_dual : DualEnv) (cfg : EvalConfig) (hρ : ∀ (i : ℕ), ρ_real i ∈ (ρ_dual i).val) (hdom : evalDomainValidDual e ρ_dual cfg) :

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Correctness theorem for computable dual value component.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Note: Requires domain validity for log (positive argument interval).

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        For ADSupported expressions (which exclude log), domain validity is trivially true. This is because ADSupported has no log constructor.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Correctness theorem for computable dual derivative component. Uses ADSupported since derivative correctness requires differentiability.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Convenience theorem: derivIntervalCore correctness

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        If derivIntervalCore doesn't contain zero, the derivative is nonzero everywhere on I. This is a key theorem for Newton contraction analysis.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        If derivIntervalCore.lo > 0, then the derivative is positive everywhere on I.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        If derivIntervalCore.hi < 0, then the derivative is negative everywhere on I.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Strictly positive derivative (via Core bounds) implies strict monotonicity

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Strictly negative derivative (via Core bounds) implies strict antitonicity

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Computable domain-aware automatic differentiation #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        This module extends LeanCert's computable forward-mode AD path with checked reciprocal and logarithm nodes. The existing ADSupported fragment remains the domain-free fast path. Here, successful evaluation itself certifies both syntactic support and every partial-domain side condition.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Computable checked dual evaluation. No finite derivative enclosure is returned unless every reciprocal denominator excludes zero and every logarithm argument is strictly positive on the input box.

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

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Checked value-and-derivative evaluation along coordinate idx.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Checked derivative enclosure along coordinate idx.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Checked derivative enclosure for a single-variable expression.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                theorem LeanCert.Engine.evalDualChecked_val_correct (e : Core.Expr) (ρReal : ℕ → ℝ) (ρDual : DualEnv) (cfg : EvalConfig) (D : DualInterval) (hρ : ∀ (i : ℕ), ρReal i ∈ (ρDual i).val) (hok : evalDualChecked e ρDual cfg = Except.ok D) :

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Successful checked dual evaluation encloses the expression value for every real environment represented by the dual environment.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                theorem LeanCert.Engine.evalWithDerivChecked_differentiableAt (e : Core.Expr) (ρReal : ℕ → ℝ) (ρInt : IntervalEnv) (idx : ℕ) (cfg : EvalConfig) (D : DualInterval) (x : ℝ) (hx : x ∈ ρInt idx) (hρ : ∀ (i : ℕ), ρReal i ∈ ρInt i) (hok : evalWithDerivChecked e ρInt idx cfg = Except.ok D) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                DifferentiableAt ℝ (e.evalAlong ρReal idx) x

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                A successful checked evaluation proves differentiability at every point in the input box along the selected coordinate.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                theorem LeanCert.Engine.evalWithDerivChecked_der_correct (e : Core.Expr) (ρReal : ℕ → ℝ) (ρInt : IntervalEnv) (idx : ℕ) (cfg : EvalConfig) (D : DualInterval) (x : ℝ) (hx : x ∈ ρInt idx) (hρ : ∀ (i : ℕ), ρReal i ∈ ρInt i) (hok : evalWithDerivChecked e ρInt idx cfg = Except.ok D) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                deriv (e.evalAlong ρReal idx) x ∈ D.der

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Successful checked indexed AD encloses the true partial derivative.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                theorem LeanCert.Engine.derivIntervalChecked_correct (e : Core.Expr) (ρReal : ℕ → ℝ) (ρInt : IntervalEnv) (idx : ℕ) (cfg : EvalConfig) (dI : Core.IntervalRat) (x : ℝ) (hx : x ∈ ρInt idx) (hρ : ∀ (i : ℕ), ρReal i ∈ ρInt i) (hok : derivIntervalChecked e ρInt idx cfg = Except.ok dI) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                deriv (e.evalAlong ρReal idx) x ∈ dI

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Golden soundness theorem for the checked derivative-only API.