PolynomialRootCells.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The root cells used to split the long-variable weights

A cell records the side of each real root, retaining the roots themselves as separate cells. Polynomial inequalities are constant on a cell; polynomial arguments are monotone when the derivative roots are included among the cuts.

def OAI.Ostmann.rootCellCode line 21
theorem OAI.Ostmann.rootCellCode_convex line 24
theorem OAI.Ostmann.rootCellCode_no_root_between line 40

theorem OAI.Ostmann.continuous_sign_on_interval line 53

Source documentation

A continuous real function with no zeros on an interval has one sign.

theorem continuous_sign_on_interval (f : ℝ → ℝ) (a b : ℝ)
    (hf : ContinuousOn f (Set.Ioo a b)) (hn : ∀ x ∈ Set.Ioo a b, f x ≠ 0) :
    (∀ x ∈ Set.Ioo a b, 0 ≤ f x) ∨ (∀ x ∈ Set.Ioo a b, f x ≤ 0) := by
…

theorem OAI.Ostmann.polynomial_monotoneOn_of_root_cell line 68
theorem OAI.Ostmann.rootCellCode_card line 103
Source documentation
Even the crude count of all codes is exponential only in the total degree, as required by the eventual exp(poly(m)) weight bound. Empty cells cost nothing.
```
theorem rootCellCode_card (S : Finset ℝ) :
    Fintype.card (S → Ordering) = 3 ^ S.card := by
…
```
def OAI.Ostmann.polynomialRootCuts line 108
theorem OAI.Ostmann.polynomialRootCuts_card line 112