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

• ratFactorial - Compute n! as a rational
• pow - Compute interval power
• absInterval, maxAbs - Absolute value helpers
• evalTaylorSeries - Evaluate Taylor polynomial on an interval
• expComputable, sinComputable, cosComputable - Computable transcendental functions
• sinhComputable, coshComputable - Computable hyperbolic functions

Main theorems

• mem_pow - FTIA for interval power
• mem_evalTaylorSeries - General FTIA for Taylor series
• mem_expComputable, mem_sinComputable, mem_cosComputable - FTIA for computable functions

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

def LeanCert.Core.IntervalRat.ratFactorial (n : ℕ) : ℚ

Compute n! as a Rational

Equations

• LeanCert.Core.IntervalRat.ratFactorial n = ↑n.factorial

def LeanCert.Core.IntervalRat.pow (I : IntervalRat) : ℕ → IntervalRat

Compute the integer power of an interval using repeated multiplication. This is a simple but correct implementation.

Equations

• I.pow 0 = LeanCert.Core.IntervalRat.singleton 1
• I.pow n.succ = I.mul (I.pow n)

def LeanCert.Core.IntervalRat.absInterval (I : IntervalRat) : IntervalRat

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

Equations

• I.absInterval = if h1 : I.lo ≥ 0 then I else if h2 : I.hi ≤ 0 then I.neg else { lo := 0, hi := max (-I.lo) I.hi, le := ⋯ }

def LeanCert.Core.IntervalRat.maxAbs (I : IntervalRat) : ℚ

Maximum absolute value of an interval

Equations

• I.maxAbs = max |I.lo| |I.hi|

def LeanCert.Core.IntervalRat.evalTaylorSeries (coeffs : List ℚ) (I : IntervalRat) : IntervalRat

Evaluate Taylor series ∑_{i=0}^{n} c_i * x^i at interval I. Uses direct interval arithmetic with incremental powers to avoid recomputing I^i from scratch for each coefficient.

Equations

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

Computable exp via Taylor series

def LeanCert.Core.IntervalRat.expTaylorCoeffs (n : ℕ) : List ℚ

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

Equations

• LeanCert.Core.IntervalRat.expTaylorCoeffs n = LeanCert.Core.IntervalRat.expTaylorCoeffsAux✝ n 0 1

def LeanCert.Core.IntervalRat.expRemainderBoundComputable (I : IntervalRat) (n : ℕ) : IntervalRat

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.

def LeanCert.Core.IntervalRat.expPointComputable (q : ℚ) (n : ℕ := 10) : IntervalRat

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.

def LeanCert.Core.IntervalRat.hull (I J : IntervalRat) : IntervalRat

Hull of two intervals: smallest interval containing both.

Equations

• I.hull J = { lo := min I.lo J.lo, hi := max I.hi J.hi, le := ⋯ }

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

Membership in hull

theorem LeanCert.Core.IntervalRat.mem_hull_right {x : ℝ} {I J : IntervalRat} (hx : x ∈ J) : x ∈ I.hull J

def LeanCert.Core.IntervalRat.expComputable (I : IntervalRat) (n : ℕ := 10) : IntervalRat

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.

Computable sin via Taylor series

def LeanCert.Core.IntervalRat.sinTaylorCoeffs (n : ℕ) : List ℚ

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

Equations

• LeanCert.Core.IntervalRat.sinTaylorCoeffs n = List.map (fun (i : ℕ) => if i % 2 = 1 then (-1) ^ ((i - 1) / 2) / LeanCert.Core.IntervalRat.ratFactorial i else 0) (List.range (n + 1))

def LeanCert.Core.IntervalRat.sinRemainderBoundComputable (I : IntervalRat) (n : ℕ) : IntervalRat

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.

def LeanCert.Core.IntervalRat.sinComputable (I : IntervalRat) (n : ℕ := 10) : IntervalRat

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.

Computable cos via Taylor series

def LeanCert.Core.IntervalRat.cosTaylorCoeffs (n : ℕ) : List ℚ

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

Equations

• LeanCert.Core.IntervalRat.cosTaylorCoeffs n = List.map (fun (i : ℕ) => if i % 2 = 0 then (-1) ^ (i / 2) / LeanCert.Core.IntervalRat.ratFactorial i else 0) (List.range (n + 1))

def LeanCert.Core.IntervalRat.cosRemainderBoundComputable (I : IntervalRat) (n : ℕ) : IntervalRat

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.

def LeanCert.Core.IntervalRat.cosComputable (I : IntervalRat) (n : ℕ := 10) : IntervalRat

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.

Computable sinh and cosh via exp

def LeanCert.Core.IntervalRat.sinhPointComputable (q : ℚ) (n : ℕ := 10) : IntervalRat

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.

def LeanCert.Core.IntervalRat.coshPointComputable (q : ℚ) (n : ℕ := 10) : IntervalRat

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.

theorem LeanCert.Core.IntervalRat.coshPointComputable_lo_ge_one (q : ℚ) (n : ℕ) : 1 ≤ (coshPointComputable q n).lo

The lower bound of coshPointComputable is always at least 1.

def LeanCert.Core.IntervalRat.sinhComputable (I : IntervalRat) (n : ℕ := 10) : IntervalRat

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

• I.sinhComputable n = (LeanCert.Core.IntervalRat.sinhPointComputable I.lo n).hull (LeanCert.Core.IntervalRat.sinhPointComputable I.hi n)

def LeanCert.Core.IntervalRat.coshComputable (I : IntervalRat) (n : ℕ := 10) : IntervalRat

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.

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

Helper lemmas for Taylor series membership

theorem LeanCert.Core.IntervalRat.abs_le_maxAbs {x : ℝ} {I : IntervalRat} (hx : x ∈ I) : |x| ≤ ↑I.maxAbs

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) : Real.exp ξ ≤ 3 ^ (⌈r⌉₊ + 1)

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

Coefficient matching lemmas

theorem LeanCert.Core.IntervalRat.iteratedDeriv_exp_zero (i : ℕ) : iteratedDeriv i Real.exp 0 = 1

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: if coeffs has length n+1, then ∑_{i=0}^{n} coeffs[i] * x^i ∈ evalTaylorSeries coeffs I for x ∈ I.

theorem LeanCert.Core.IntervalRat.mem_evalTaylorSeries_exp {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (n : ℕ) : ∑ i ∈ Finset.range (n + 1), 1 / ↑i.factorial * x ^ i ∈ evalTaylorSeries (expTaylorCoeffs n) 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.

theorem LeanCert.Core.IntervalRat.mem_evalTaylorSeries_sin {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (n : ℕ) : ∑ i ∈ Finset.range (n + 1), iteratedDeriv i Real.sin 0 / ↑i.factorial * x ^ i ∈ evalTaylorSeries (sinTaylorCoeffs n) I

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

theorem LeanCert.Core.IntervalRat.mem_evalTaylorSeries_cos {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (n : ℕ) : ∑ i ∈ Finset.range (n + 1), iteratedDeriv i Real.cos 0 / ↑i.factorial * x ^ i ∈ evalTaylorSeries (cosTaylorCoeffs n) I

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

theorem LeanCert.Core.IntervalRat.exp_taylor_remainder_in_interval {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (n : ℕ) : Real.exp x - ∑ i ∈ Finset.range (n + 1), iteratedDeriv i Real.exp 0 / ↑i.factorial * x ^ i ∈ I.expRemainderBoundComputable n

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.

theorem LeanCert.Core.IntervalRat.sin_taylor_remainder_in_interval {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (n : ℕ) : Real.sin x - ∑ i ∈ Finset.range (n + 1), iteratedDeriv i Real.sin 0 / ↑i.factorial * x ^ i ∈ I.sinRemainderBoundComputable n

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.

theorem LeanCert.Core.IntervalRat.cos_taylor_remainder_in_interval {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (n : ℕ) : Real.cos x - ∑ i ∈ Finset.range (n + 1), iteratedDeriv i Real.cos 0 / ↑i.factorial * x ^ i ∈ I.cosRemainderBoundComputable n

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

theorem LeanCert.Core.IntervalRat.mem_expPointComputable (q : ℚ) (n : ℕ) : Real.exp ↑q ∈ expPointComputable q n

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

theorem LeanCert.Core.IntervalRat.mem_expComputable {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (n : ℕ) : Real.exp x ∈ I.expComputable n

theorem LeanCert.Core.IntervalRat.mem_sinComputable {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (n : ℕ) : Real.sin x ∈ I.sinComputable 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].

theorem LeanCert.Core.IntervalRat.mem_cosComputable {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (n : ℕ) : Real.cos x ∈ I.cosComputable n

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].

theorem LeanCert.Core.IntervalRat.mem_sinhPointComputable (q : ℚ) (n : ℕ) : Real.sinh ↑q ∈ sinhPointComputable q n

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

theorem LeanCert.Core.IntervalRat.mem_coshPointComputable (q : ℚ) (n : ℕ) : Real.cosh ↑q ∈ coshPointComputable q n

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

theorem LeanCert.Core.IntervalRat.mem_sinhComputable {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (n : ℕ) : Real.sinh x ∈ I.sinhComputable n

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

Uses endpoint evaluation and monotonicity of sinh.

theorem LeanCert.Core.IntervalRat.mem_coshComputable {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (n : ℕ) : Real.cosh x ∈ I.coshComputable n

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.

def LeanCert.Core.IntervalRat.atanhTaylorCoeffs (n : ℕ) : List ℚ

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

• LeanCert.Core.IntervalRat.atanhTaylorCoeffs n = List.map (fun (i : ℕ) => if i % 2 = 1 then 1 / ↑i else 0) (List.range (n + 1))

def LeanCert.Core.IntervalRat.atanhRemainderBoundComputable (r : ℚ) (n : ℕ) : IntervalRat

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.

def LeanCert.Core.IntervalRat.atanhPointComputable (q : ℚ) (n : ℕ := 15) : IntervalRat

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.

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.

theorem LeanCert.Core.IntervalRat.mem_evalTaylorSeries_atanh {q : ℚ} (n : ℕ) : (List.map (fun (x : ℚ × ℕ) => match x with | (c, i) => ↑c * ↑q ^ i) (atanhTaylorCoeffs n).zipIdx).sum ∈ evalTaylorSeries (atanhTaylorCoeffs n) (singleton q)

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

The atanh Taylor remainder bound: for |q| < 1, the remainder after n terms is bounded. The remainder is |Σ_{k: 2k+1 > n} q^(2k+1)/(2k+1)| ≤ |q|^(n+1)/(1-|q|).

theorem LeanCert.Core.IntervalRat.mem_atanhPointComputable (q : ℚ) (n : ℕ) (hq : |↑q| < 1) : Real.atanh ↑q ∈ atanhPointComputable 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)

def LeanCert.Core.IntervalRat.ln2Computable (n : ℕ := 20) : IntervalRat

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

• LeanCert.Core.IntervalRat.ln2Computable n = LeanCert.Core.IntervalRat.scale 2 (LeanCert.Core.IntervalRat.atanhPointComputable (1 / 3) n)

theorem LeanCert.Core.IntervalRat.mem_ln2Computable (n : ℕ) : Real.log 2 ∈ ln2Computable n

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)

def LeanCert.Core.IntervalRat.logReductionExponent (q : ℚ) : ℤ

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

Equations

• LeanCert.Core.IntervalRat.logReductionExponent q = if q ≤ 0 then 0 else have n_log := q.num.natAbs.log2; have d_log := q.den.log2; ↑n_log - ↑d_log

def LeanCert.Core.IntervalRat.logReduceMantissa (q : ℚ) : ℚ

Reduced mantissa m = q * 2^(-k)

Equations

• LeanCert.Core.IntervalRat.logReduceMantissa q = if q ≤ 0 then 1 else q * 2 ^ (-LeanCert.Core.IntervalRat.logReductionExponent q)

def LeanCert.Core.IntervalRat.logPointComputable (q : ℚ) (n : ℕ := 20) : IntervalRat

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.

def LeanCert.Core.IntervalRat.logComputable (I : IntervalRat) (n : ℕ := 20) : IntervalRat

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.

theorem LeanCert.Core.IntervalRat.mem_logPointComputable {q : ℚ} (hq : 0 < q) (n : ℕ) : Real.log ↑q ∈ logPointComputable q n

FTIA for logPointComputable

theorem LeanCert.Core.IntervalRat.mem_logComputable {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (hpos : 0 < I.lo) (n : ℕ) : Real.log x ∈ I.logComputable 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 : ℕ) : Real.log x ∈ I.logComputable 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

def LeanCert.Core.IntervalRat.two_div_sqrt_pi : IntervalRat

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

Equations

• LeanCert.Core.IntervalRat.two_div_sqrt_pi = { lo := 1128 / 1000, hi := 1129 / 1000, le := LeanCert.Core.IntervalRat.two_div_sqrt_pi._proof_1 }

def LeanCert.Core.IntervalRat.erfTaylorCoeffs (n : ℕ) : List ℚ

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.

def LeanCert.Core.IntervalRat.erfRemainderBoundComputable (I : IntervalRat) (n : ℕ) : IntervalRat

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.

def LeanCert.Core.IntervalRat.erfPointComputable (q : ℚ) (n : ℕ := 15) : IntervalRat

Computable interval enclosure for erf at a single rational point. Uses sign-aware global bounds:

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

Equations

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

def LeanCert.Core.IntervalRat.erfComputable (I : IntervalRat) (n : ℕ := 15) : IntervalRat

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.

theorem LeanCert.Core.IntervalRat.two_div_sqrt_pi_mem : 2 / √Real.pi ∈ two_div_sqrt_pi

2/√π is in the interval two_div_sqrt_pi. 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

• LeanCert.Core.IntervalRat.erfInner x = ∫ (t : ℝ) in 0..x, Real.exp (-t ^ 2)

theorem LeanCert.Core.IntervalRat.erf_eq_factor_mul_inner (x : ℝ) : Real.erf x = 2 / √Real.pi * erfInner x

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

theorem LeanCert.Core.IntervalRat.erfInner_deriv : deriv erfInner = fun (x : ℝ) => Real.exp (-x ^ 2)

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

theorem LeanCert.Core.IntervalRat.contDiff_exp_neg_sq : ContDiff ℝ ⊤ fun (x : ℝ) => Real.exp (-x ^ 2)

exp(-x²) is smooth.

theorem LeanCert.Core.IntervalRat.analyticAt_exp_neg_sq (x : ℝ) : AnalyticAt ℝ (fun (t : ℝ) => Real.exp (-t ^ 2)) x

exp(-x²) is analytic everywhere.

theorem LeanCert.Core.IntervalRat.analyticOnNhd_exp_neg_sq : AnalyticOnNhd ℝ (fun (t : ℝ) => Real.exp (-t ^ 2)) Set.univ

exp(-x²) is analytic on ℝ.

Computable atanh interval via endpoint evaluation

def LeanCert.Core.IntervalRat.atanhComputable (I : IntervalRat) (n : ℕ := 15) : IntervalRat

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.

theorem LeanCert.Core.IntervalRat.mem_atanhComputable {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (hlo : -1 < I.lo) (hhi : I.hi < 1) (n : ℕ) : Real.atanh x ∈ I.atanhComputable n

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