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

• LeanCert.Core.Expr - The expression AST supporting algebraic and transcendental operations
• LeanCert.Core.Expr.eval - Evaluation of expressions given a variable assignment

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

• LeanCert.Core.Real.atanh x = 1 / 2 * Real.log ((1 + x) / (1 - x))

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]

theorem LeanCert.Core.Real.atanh_zero : atanh 0 = 0

atanh(0) = 0

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

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

theorem LeanCert.Core.Real.atanh_strictMonoOn : StrictMonoOn atanh (Set.Ioo (-1) 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 x ≤ atanh 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

• LeanCert.Core.Real.erf x = 2 / √Real.pi * ∫ (t : ℝ) in 0..x, Real.exp (-t ^ 2)

theorem LeanCert.Core.Real.erf_le_one (x : ℝ) : erf x ≤ 1

The error function is bounded above by 1.

theorem LeanCert.Core.Real.neg_one_le_erf (x : ℝ) : -1 ≤ erf x

The error function is bounded below by -1.

inductive LeanCert.Core.MathConst : Type

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.

• pi : MathConst
• eulerMascheroni : MathConst

@[implicit_reducible]

instance LeanCert.Core.instReprMathConst : Repr MathConst

Equations

• LeanCert.Core.instReprMathConst = { reprPrec := LeanCert.Core.instReprMathConst.repr }

def LeanCert.Core.instReprMathConst.repr : MathConst → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance LeanCert.Core.instDecidableEqMathConst : DecidableEq MathConst

Equations

• LeanCert.Core.instDecidableEqMathConst x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance LeanCert.Core.instInhabitedMathConst : Inhabited MathConst

Equations

• LeanCert.Core.instInhabitedMathConst = { default := LeanCert.Core.instInhabitedMathConst.default }

def LeanCert.Core.instInhabitedMathConst.default : MathConst

Equations

• LeanCert.Core.instInhabitedMathConst.default = LeanCert.Core.MathConst.pi

noncomputable def LeanCert.Core.MathConst.toReal : MathConst → ℝ

The real value of a named mathematical constant.

Equations

• LeanCert.Core.MathConst.pi.toReal = Real.pi
• LeanCert.Core.MathConst.eulerMascheroni.toReal = Real.eulerMascheroniConstant

def LeanCert.Core.MathConst.toFloat : MathConst → Float

Float approximation for heuristic evaluation (unverified).

Equations

• LeanCert.Core.MathConst.pi.toFloat = 3.141592653589793
• LeanCert.Core.MathConst.eulerMascheroni.toFloat = 0.5772156649015329

def LeanCert.Core.MathConst.toRatApprox : MathConst → ℚ

Rational approximation for display/debugging (unverified).

Equations

• LeanCert.Core.MathConst.pi.toRatApprox = 157 / 50
• LeanCert.Core.MathConst.eulerMascheroni.toRatApprox = 577 / 1000

inductive LeanCert.Core.Expr : Type

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.

def LeanCert.Core.instReprExpr.repr : Expr → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance LeanCert.Core.instReprExpr : Repr Expr

Equations

• LeanCert.Core.instReprExpr = { reprPrec := LeanCert.Core.instReprExpr.repr }

def LeanCert.Core.instDecidableEqExpr.decEq (x✝ x✝¹ : Expr) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance LeanCert.Core.instDecidableEqExpr : DecidableEq Expr

Equations

• LeanCert.Core.instDecidableEqExpr = LeanCert.Core.instDecidableEqExpr.decEq

@[implicit_reducible]

instance LeanCert.Core.instInhabitedExpr : Inhabited Expr

Equations

• LeanCert.Core.instInhabitedExpr = { default := LeanCert.Core.instInhabitedExpr.default }

def LeanCert.Core.instInhabitedExpr.default : Expr

Equations

• LeanCert.Core.instInhabitedExpr.default = LeanCert.Core.Expr.const default

def LeanCert.Core.Expr.sub (e₁ e₂ : Expr) : Expr

Subtraction as a derived operation

Equations

• e₁.sub e₂ = e₁.add e₂.neg

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

Division as a derived operation

Equations

• e₁.div e₂ = e₁.mul e₂.inv

def LeanCert.Core.Expr.pow (e : Expr) : ℕ → Expr

Integer power (non-negative exponent)

Equations

• e.pow 0 = LeanCert.Core.Expr.const 1
• e.pow n.succ = e.mul (e.pow n)

def LeanCert.Core.Expr.abs (e : Expr) : Expr

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

Equations

• e.abs = (e.mul e).sqrt

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

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

Equations

• LeanCert.Core.Expr.eval ρ (LeanCert.Core.Expr.const a) = ↑a
• LeanCert.Core.Expr.eval ρ (LeanCert.Core.Expr.var a) = ρ a
• LeanCert.Core.Expr.eval ρ (a.add a_1) = LeanCert.Core.Expr.eval ρ a + LeanCert.Core.Expr.eval ρ a_1
• LeanCert.Core.Expr.eval ρ (a.mul a_1) = LeanCert.Core.Expr.eval ρ a * LeanCert.Core.Expr.eval ρ a_1
• LeanCert.Core.Expr.eval ρ a.neg = -LeanCert.Core.Expr.eval ρ a
• LeanCert.Core.Expr.eval ρ a.inv = (LeanCert.Core.Expr.eval ρ a)⁻¹
• LeanCert.Core.Expr.eval ρ a.exp = Real.exp (LeanCert.Core.Expr.eval ρ a)
• LeanCert.Core.Expr.eval ρ a.sin = Real.sin (LeanCert.Core.Expr.eval ρ a)
• LeanCert.Core.Expr.eval ρ a.cos = Real.cos (LeanCert.Core.Expr.eval ρ a)
• LeanCert.Core.Expr.eval ρ a.log = Real.log (LeanCert.Core.Expr.eval ρ a)
• LeanCert.Core.Expr.eval ρ a.atan = Real.arctan (LeanCert.Core.Expr.eval ρ a)
• LeanCert.Core.Expr.eval ρ a.arsinh = Real.arsinh (LeanCert.Core.Expr.eval ρ a)
• LeanCert.Core.Expr.eval ρ a.atanh = LeanCert.Core.Real.atanh (LeanCert.Core.Expr.eval ρ a)
• LeanCert.Core.Expr.eval ρ a.sinc = Real.sinc (LeanCert.Core.Expr.eval ρ a)
• LeanCert.Core.Expr.eval ρ a.erf = LeanCert.Core.Real.erf (LeanCert.Core.Expr.eval ρ a)
• LeanCert.Core.Expr.eval ρ a.sinh = Real.sinh (LeanCert.Core.Expr.eval ρ a)
• LeanCert.Core.Expr.eval ρ a.cosh = Real.cosh (LeanCert.Core.Expr.eval ρ a)
• LeanCert.Core.Expr.eval ρ a.tanh = Real.tanh (LeanCert.Core.Expr.eval ρ a)
• LeanCert.Core.Expr.eval ρ a.sqrt = √(LeanCert.Core.Expr.eval ρ a)
• LeanCert.Core.Expr.eval ρ (LeanCert.Core.Expr.namedConst a) = a.toReal

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

Update variable assignment at a specific index

Equations

• (ρ[idx ↦ x]) i = if i = idx then x else ρ i

def LeanCert.Core.Expr.«term_[_↦_]» : Lean.TrailingParserDescr

Equations

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

@[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

• e.evalAlong ρ idx t = LeanCert.Core.Expr.eval (ρ[idx ↦ t]) e

def LeanCert.Core.Expr.freeVars : Expr → Finset ℕ

The set of free variable indices in an expression

Equations

• (LeanCert.Core.Expr.const a).freeVars = ∅
• (LeanCert.Core.Expr.var a).freeVars = {a}
• (a.add a_1).freeVars = a.freeVars ∪ a_1.freeVars
• (a.mul a_1).freeVars = a.freeVars ∪ a_1.freeVars
• a.neg.freeVars = a.freeVars
• a.inv.freeVars = a.freeVars
• a.exp.freeVars = a.freeVars
• a.sin.freeVars = a.freeVars
• a.cos.freeVars = a.freeVars
• a.log.freeVars = a.freeVars
• a.atan.freeVars = a.freeVars
• a.arsinh.freeVars = a.freeVars
• a.atanh.freeVars = a.freeVars
• a.sinc.freeVars = a.freeVars
• a.erf.freeVars = a.freeVars
• a.sinh.freeVars = a.freeVars
• a.cosh.freeVars = a.freeVars
• a.tanh.freeVars = a.freeVars
• a.sqrt.freeVars = a.freeVars
• (LeanCert.Core.Expr.namedConst a).freeVars = ∅

def LeanCert.Core.Expr.isClosed (e : Expr) : Prop

An expression is closed if it has no free variables

Equations

• e.isClosed = (e.freeVars = ∅)

@[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) : eval ρ e.arsinh = Real.arsinh (eval ρ e)

@[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_namedConst (ρ : ℕ → ℝ) (c : MathConst) : eval ρ (namedConst c) = c.toReal

theorem LeanCert.Core.Expr.eval_pi (ρ : ℕ → ℝ) : eval ρ (namedConst MathConst.pi) = Real.pi

Backward-compat alias for simp lists referencing eval_pi.

theorem LeanCert.Core.Expr.eval_eulerMascheroni (ρ : ℕ → ℝ) : eval ρ (namedConst MathConst.eulerMascheroni) = Real.eulerMascheroniConstant

@[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_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.

def LeanCert.Core.Expr.usesOnlyVar0 : Expr → Bool

Check if an expression only uses variable 0 (computable)

Equations

• (LeanCert.Core.Expr.const a).usesOnlyVar0 = true
• (LeanCert.Core.Expr.var a).usesOnlyVar0 = (a == 0)
• (a.add a_1).usesOnlyVar0 = (a.usesOnlyVar0 && a_1.usesOnlyVar0)
• (a.mul a_1).usesOnlyVar0 = (a.usesOnlyVar0 && a_1.usesOnlyVar0)
• a.neg.usesOnlyVar0 = a.usesOnlyVar0
• a.inv.usesOnlyVar0 = a.usesOnlyVar0
• a.exp.usesOnlyVar0 = a.usesOnlyVar0
• a.sin.usesOnlyVar0 = a.usesOnlyVar0
• a.cos.usesOnlyVar0 = a.usesOnlyVar0
• a.log.usesOnlyVar0 = a.usesOnlyVar0
• a.atan.usesOnlyVar0 = a.usesOnlyVar0
• a.arsinh.usesOnlyVar0 = a.usesOnlyVar0
• a.atanh.usesOnlyVar0 = a.usesOnlyVar0
• a.sinc.usesOnlyVar0 = a.usesOnlyVar0
• a.erf.usesOnlyVar0 = a.usesOnlyVar0
• a.sinh.usesOnlyVar0 = a.usesOnlyVar0
• a.cosh.usesOnlyVar0 = a.usesOnlyVar0
• a.tanh.usesOnlyVar0 = a.usesOnlyVar0
• a.sqrt.usesOnlyVar0 = a.usesOnlyVar0
• (LeanCert.Core.Expr.namedConst a).usesOnlyVar0 = true

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