# Tagged Questions

**15**

votes

**4**answers

769 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

412 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

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