OAI/NumberTheory/Ostmann/Characters/PolynomialCellSupports.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Sharp polynomial support conditions are functions of the root cell

  1. def OAI.Ostmann.polynomialSupportCode line 11
  2. theorem OAI.Ostmann.polynomialSupportCode_of_rootCell line 14
  3. def OAI.Ostmann.polynomialRootCellFlag line 24

    Source documentation

    This is the actual support flag, defined from the inequalities, rather than an assumption that the supports are regular on the cells.

    noncomputable def polynomialRootCellFlag {I : Type*} (P : I → Polynomial ℝ)
    (S : Finset ℝ) (keep : (I → Bool) → Bool) (c : S → Ordering) : ℂ :=
…
  4. theorem OAI.Ostmann.polynomialRootCellFlag_norm line 28
  5. theorem OAI.Ostmann.polynomialRootCellFlag_value line 34