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:

• Monotonicity analysis
• Lipschitz/contractivity bounds
• Newton method analysis
• Global optimization pruning

Main theorems

Exp (derivative = exp, always positive)

• exp_deriv_pos - exp' x > 0 for all x
• exp_deriv_interval - exp' x ∈ [exp a, exp b] for x ∈ [a, b]

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

• log_deriv_interval - log' x ∈ [1/b, 1/a] for x ∈ [a, b] with 0 < a

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

• arctan_deriv_interval - arctan' x ∈ (0, 1] for all x
• arctan_deriv_mem_Icc - arctan' x ∈ [0, 1] for all x

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

• arsinh_deriv_interval - arsinh' x ∈ (0, 1] for all x
• arsinh_deriv_mem_Icc - arsinh' x ∈ [0, 1] for all x

Sin/Cos (derivatives bounded by 1)

• sin_deriv_interval - |sin' x| = |cos x| ≤ 1
• cos_deriv_interval - |cos' x| = |sin x| ≤ 1

Sinh/Cosh (derivative relationships)

• sinh_deriv_eq_cosh - sinh' = cosh
• cosh_deriv_eq_sinh - cosh' = sinh
• cosh_deriv_interval - cosh' x = sinh x, monotonicity facts

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

theorem LeanCert.Core.DerivativeIntervals.exp_deriv_pos (x : ℝ) : 0 < deriv Real.exp x

The derivative of exp is positive everywhere

theorem LeanCert.Core.DerivativeIntervals.exp_strictMono : StrictMono Real.exp

exp is strictly increasing (follows from positive derivative)

theorem LeanCert.Core.DerivativeIntervals.exp_deriv_interval {a b x : ℝ} (hx : x ∈ Set.Icc a b) : deriv Real.exp x ∈ Set.Icc (Real.exp a) (Real.exp b)

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

Log derivative intervals

theorem LeanCert.Core.DerivativeIntervals.log_deriv_eq_inv {x : ℝ} (_hx : 0 < x) : deriv Real.log x = x⁻¹

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

theorem LeanCert.Core.DerivativeIntervals.log_deriv_interval {a b x : ℝ} (ha : 0 < a) (hx : x ∈ Set.Icc a b) : deriv Real.log x ∈ Set.Icc b⁻¹ a⁻¹

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

theorem LeanCert.Core.DerivativeIntervals.log_strictMonoOn : StrictMonoOn Real.log (Set.Ioi 0)

log is strictly increasing on (0, ∞)

Arctan derivative intervals

theorem LeanCert.Core.DerivativeIntervals.arctan_deriv_eq (x : ℝ) : deriv Real.arctan x = (1 + x ^ 2)⁻¹

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

theorem LeanCert.Core.DerivativeIntervals.arctan_deriv_pos (x : ℝ) : 0 < deriv Real.arctan x

1/(1+x²) is always positive

theorem LeanCert.Core.DerivativeIntervals.arctan_deriv_le_one (x : ℝ) : deriv Real.arctan x ≤ 1

1/(1+x²) ≤ 1 for all x

theorem LeanCert.Core.DerivativeIntervals.arctan_deriv_interval (x : ℝ) : deriv Real.arctan x ∈ Set.Ioc 0 1

arctan' x ∈ (0, 1] for all x

theorem LeanCert.Core.DerivativeIntervals.arctan_deriv_mem_Icc (x : ℝ) : deriv Real.arctan x ∈ Set.Icc 0 1

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

theorem LeanCert.Core.DerivativeIntervals.arctan_strictMono : StrictMono Real.arctan

arctan is strictly increasing (follows from positive derivative)

Arsinh derivative intervals

theorem LeanCert.Core.DerivativeIntervals.arsinh_deriv_eq (x : ℝ) : deriv Real.arsinh x = (√(1 + x ^ 2))⁻¹

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

theorem LeanCert.Core.DerivativeIntervals.sqrt_one_add_sq_ge_one (x : ℝ) : 1 ≤ √(1 + x ^ 2)

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

theorem LeanCert.Core.DerivativeIntervals.sqrt_one_add_sq_pos (x : ℝ) : 0 < √(1 + x ^ 2)

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

theorem LeanCert.Core.DerivativeIntervals.arsinh_deriv_pos (x : ℝ) : 0 < deriv Real.arsinh x

arsinh' x > 0 for all x

theorem LeanCert.Core.DerivativeIntervals.arsinh_deriv_le_one (x : ℝ) : deriv Real.arsinh x ≤ 1

arsinh' x ≤ 1 for all x

theorem LeanCert.Core.DerivativeIntervals.arsinh_deriv_interval (x : ℝ) : deriv Real.arsinh x ∈ Set.Ioc 0 1

arsinh' x ∈ (0, 1] for all x

theorem LeanCert.Core.DerivativeIntervals.arsinh_deriv_mem_Icc (x : ℝ) : deriv Real.arsinh x ∈ Set.Icc 0 1

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

theorem LeanCert.Core.DerivativeIntervals.arsinh_strictMono : StrictMono Real.arsinh

arsinh is strictly increasing

Sin derivative intervals

theorem LeanCert.Core.DerivativeIntervals.sin_deriv_eq (x : ℝ) : deriv Real.sin x = Real.cos x

The derivative of sin is cos

theorem LeanCert.Core.DerivativeIntervals.sin_deriv_abs_le_one (x : ℝ) : |deriv Real.sin x| ≤ 1

|sin' x| = |cos x| ≤ 1

theorem LeanCert.Core.DerivativeIntervals.sin_deriv_mem_Icc (x : ℝ) : deriv Real.sin x ∈ Set.Icc (-1) 1

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

Cos derivative intervals

theorem LeanCert.Core.DerivativeIntervals.cos_deriv_eq (x : ℝ) : deriv Real.cos x = -Real.sin x

The derivative of cos is -sin

theorem LeanCert.Core.DerivativeIntervals.cos_deriv_abs_le_one (x : ℝ) : |deriv Real.cos x| ≤ 1

|cos' x| = |sin x| ≤ 1

theorem LeanCert.Core.DerivativeIntervals.cos_deriv_mem_Icc (x : ℝ) : deriv Real.cos x ∈ Set.Icc (-1) 1

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

Sinh derivative intervals

theorem LeanCert.Core.DerivativeIntervals.sinh_deriv_eq (x : ℝ) : deriv Real.sinh x = Real.cosh x

The derivative of sinh is cosh

theorem LeanCert.Core.DerivativeIntervals.sinh_deriv_ge_one (x : ℝ) : 1 ≤ deriv Real.sinh x

sinh' x = cosh x ≥ 1 for all x

theorem LeanCert.Core.DerivativeIntervals.sinh_deriv_pos (x : ℝ) : 0 < deriv Real.sinh x

sinh' x > 0 for all x

theorem LeanCert.Core.DerivativeIntervals.sinh_strictMono : StrictMono Real.sinh

sinh is strictly increasing

Cosh derivative intervals

theorem LeanCert.Core.DerivativeIntervals.cosh_deriv_eq (x : ℝ) : deriv Real.cosh x = Real.sinh x

The derivative of cosh is sinh

theorem LeanCert.Core.DerivativeIntervals.cosh_deriv_zero : deriv Real.cosh 0 = 0

cosh' 0 = sinh 0 = 0

theorem LeanCert.Core.DerivativeIntervals.cosh_deriv_pos_of_pos {x : ℝ} (hx : 0 < x) : 0 < deriv Real.cosh x

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

theorem LeanCert.Core.DerivativeIntervals.cosh_deriv_neg_of_neg {x : ℝ} (hx : x < 0) : deriv Real.cosh x < 0

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

theorem LeanCert.Core.DerivativeIntervals.cosh_strictAntiOn_nonpos : StrictAntiOn Real.cosh (Set.Iic 0)

cosh is strictly decreasing on (-∞, 0]

theorem LeanCert.Core.DerivativeIntervals.cosh_strictMonoOn_nonneg : StrictMonoOn Real.cosh (Set.Ici 0)

cosh is strictly increasing on [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)

theorem LeanCert.Core.OneSidedTaylor.one_le_exp_of_nonneg (x : ℝ) (hx : 0 ≤ x) : 1 ≤ Real.exp x

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

theorem LeanCert.Core.OneSidedTaylor.one_add_le_exp (x : ℝ) : 1 + x ≤ Real.exp x

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

theorem LeanCert.Core.OneSidedTaylor.add_one_le_exp' (x : ℝ) : x + 1 ≤ Real.exp x

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) : MonotoneOn f (Set.Icc a b)

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) : StrictMonoOn f (Set.Icc a b)

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) : AntitoneOn f (Set.Icc a b)

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) : StrictAntiOn f (Set.Icc a b)

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