# Tagged Questions

**15**

votes

**4**answers

763 views

### Proving univariate polynomials (defined by sums, binomial coeffs, etc.) are nonnegative: is it 'routine'?

My colleagues and I are working on a project related to an old paper of C. Borell and we have boiled it down to the following problem:
Show, for all integers $1 \leq i \leq k$, that the univariate ...

**4**

votes

**1**answer

539 views

### “Less than” formula for complete theory of the rationals

Does anyone know the name/author of the model theory paper where it's proven that you can define the $ < $ relation on $ (\mathbb{Q}, +, \cdot, 1, 0) $?

**5**

votes

**2**answers

407 views

### Sturm chain analogue for exponential polynomials?

I'm going to define an exponential polynomial of degree $k$ as a function $f$ of the form
$f(x) = \sum_{i=1}^k c_ie^{\alpha_ix}$ ($\alpha_i$s real).
My first question is: is there an algorithm for ...

**3**

votes

**1**answer

884 views

### Proving inequalities over algebraic structures

I've been looking at proof techniques in formal systems like Coq and Agda recently, and encountered the newring tactic described here for proving equalities over ...