SymbolicLimits.jl

compare_variance_rapidity(expr1, expr2, x, assumptions)

Compare the rapidity of growth between two expressions as x approaches infinity.

Returns:

• -1 if expr1 grows slower than expr2 (i.e., expr1 ≺ expr2)
• 0 if expr1 and expr2 grow at the same rate (i.e., expr1 ≍ expr2)
• 1 if expr1 grows faster than expr2 (i.e., expr1 ≻ expr2)

The comparison is based on the limit of log(expr1)/log(expr2) as x approaches infinity:

• f ≺ g iff log(f)/log(g) → 0
• f ≍ g iff log(f)/log(g) → c for some finite nonzero constant c
• f ≻ g iff log(f)/log(g) → ∞

Arguments

• expr1, expr2: Expressions to compare (must be of the form x or exp(...)).
• x: The variable approaching infinity
• assumptions: A set to track assumptions made during computation

Returns

An integer (-1, 0, or 1) indicating the relative growth rates.

get_leading_exponent(expr, ω, h, assumptions)

Find the leading (smallest) exponent in the series expansion of expr in powers of ω.

This function determines the power of the leading term in the series expansion: expr = c_{e}⋅ω^e + c_{e+1}⋅ω^{e+1} + ... where e is the leading exponent (the smallest exponent with a non-zero coefficient).

Returns Inf if expr is equivalent to zero.

Arguments

• expr: The expression to analyze
• ω: A symbol representing the distinguished exponential exp(h)
• h: The argument of the distinguished exponential
• assumptions: A set to track assumptions made during computation

Returns

The leading exponent e, or Inf if expr is equivalent to zero.

get_series_term(expr, ω, h, i, assumptions)

Get the coefficient of ω^i in the series expansion of expr around the most rapidly varying term.

This function computes the i-th coefficient in the series expansion of expr in powers of ω, where ω represents the expression exp(h). The expansion takes the form: expr = c₀ + c₁⋅ω + c₂⋅ω² + ...

This is a core component of the Gruntz algorithm for computing limits.

Arguments

• expr: The expression to expand
• ω: A symbol representing the distinguished exponential exp(h)
• h: The argument of the distinguished exponential
• i: The power of ω for which to compute the coefficient
• assumptions: A set to track assumptions made during computation

Returns

The coefficient of ω^i in the series expansion of expr.

is_exp(expr)

Check if an expression is of the form exp(...).

Returns true if expr is a symbolic expression with the exponential function as its operation, false otherwise.

limit(expr, var, h[, side::Symbol])

Compute the limit of expr as var approaches h and return (limit, assumptions). If all the assumptions are true, then the returned limit is correct.

side indicates the direction from which var approaches h. It may be one of :left, :right, or :both. If side is :both and the two sides do not align, an error is thrown. Side defaults to :both for finite h, :left for h = Inf, and :right for h = -Inf.

limit_inf(expr, x)

Compute the limit of expr as x approaches infinity and return (limit, assumptions).

This is the internal API boundary between the internal limits.jl file and the public SymbolicLimits.jl file

log_exp_simplify(expr)

Simplify expressions by canceling log(exp(x)) → x transformations.

This function performs basic log-exp simplifications that are always valid, specifically canceling log(exp(x)) to x. This is a conservative simplification that doesn't extend domains.

Arguments

• expr: The expression to simplify

Returns

The simplified expression with log-exp cancellations applied.

most_rapidly_varying_subexpressions(expr, x, assumptions)

Find the most rapidly varying subexpressions (MRV set) in expr with respect to x.

The MRV set consists of subexpressions that grow most rapidly as x approaches infinity. This is a key component of the Gruntz algorithm for computing symbolic limits.

For scalar expressions, returns an empty list.

Arguments

• expr: The expression to analyze
• x: The variable with respect to which we find rapidly varying subexpressions
• assumptions: A set to track assumptions made during computation

Returns

A list of the most rapidly varying subexpressions in expr.

recursive(f, args...)

Apply function f recursively to its arguments, where f takes the recursive function as its first argument.

This utility function enables recursive operations on nested expressions by passing the recursive function itself as the first argument to f.

Example

recursive(expr) do f, ex
    # f is the recursive function, ex is the current expression
    # Apply f to subexpressions and build the result
end

rewrite(expr, ω, h, x, assumptions)

Rewrite expr in the form A⋅ω^c where A is less rapidly varying than ω and c is a real number.

This function takes an exponential expression and rewrites it in terms of a distinguished exponential subexpression ω. The symbol ω represents exp(h) where h is the argument of the most rapidly varying exponential.

The rewriting follows the formula: if expr = exp(s) and ω = exp(h), then we compute c = lim(s/h, x, ∞) and rewrite as exp(s-c⋅h) ⋅ ω^c.

Arguments

• expr: An exponential expression to rewrite (must be of the form exp(...))
• ω: A symbol representing the distinguished exponential exp(h)
• h: The argument of the distinguished exponential
• x: The variable approaching infinity
• assumptions: A set to track assumptions made during computation

Returns

An expression of the form A⋅ω^c where A is less rapidly varying than ω.

signed_limit_inf(expr, x, assumptions)

Compute the limit of expr as x approaches infinity and return (limit, sign). This function handles both symbolic expressions and scalar values, tracking assumptions made during the computation.

For scalar expressions, returns (expr, sign(expr)). For symbolic expressions, applies the Gruntz algorithm to compute the limit.

Arguments

• expr: The expression to take the limit of
• x: The variable approaching infinity
• assumptions: A set to track assumptions made during computation

Returns

A tuple (limit, sign) where:

• limit: The computed limit value
• sign: The sign of the limit

cancels log(exp(x)) and exp(log(x)), the latter may extend the domain

zero_equivalence(expr, assumptions)

Determine if expr is equivalent to zero on its domain using heuristic methods.

This function uses symbolic simplification to determine if an expression is zero. Since zero equivalence of general expressions is undecidable, this function uses heuristics and records the result as an assumption that must hold for the computed limit to be correct.

The function applies strong log-exp simplification and algebraic expansion before testing for zero equivalence.

Arguments

• expr: The expression to test for zero equivalence
• assumptions: A set to record assumptions made (updated in-place)

Returns

true if the expression is determined to be zero, false otherwise.

Side Effects

Adds an assumption about the zero-equivalence of expr to the assumptions set.