OAI/NumberTheory/Ostmann/Arithmetic/WeightedPolynomialRoots.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Weighted polynomial root bounds for the arithmetic priors

  1. theorem OAI.Ostmann.weighted_univariate_roots_le line 14
  2. theorem OAI.Ostmann.weighted_polynomial_roots_le line 34

    Source documentation

    The arithmetic polynomial estimate for independent, possibly unequal finite priors.

    theorem weighted_polynomial_roots_le {A : Type*} [Fintype A]
    (value : A → ℚ) (hinj : Function.Injective value) (α : ℝ) (hα : 0 ≤ α) :
    ∀ {n : ℕ} (P : MvPolynomial (Fin n) ℚ), P ≠ 0 →
      ∀ μ : Fin n → A → ℝ,
      (∀ i a, 0 ≤ μ i a) → (∀ i, ∑ a, μ i a = 1) → (∀ i a, μ i a ≤ α) →
      (∑ x : Fin n → A, productPrior μ x *
        (if MvPolynomial.eval (fun i => value (x i)) P = 0 then 1 else 0)) ≤
          (P.totalDegree : ℝ) * α := by
…

    Mentions: OAI.Ostmann.productPrior