OAI/Algebra/Determinantal/AmbientMain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PermanentBorder.ambient_polar_bound line 14

   Source documentation

   Selected distinct simple ambient polar zeros of an affine determinant limit are bounded by its mixed coefficient, the corresponding binomial count, and a numerical matrix-size bound. The affine map and the ambient directions are arbitrary.

   theorem ambient_polar_bound
       (N n K D : ℕ) (_hN : 0 < N) (_hD : 0 < D)
       (P : Poly (Fin N)) (hb : HasBorderDeterminant n P)
       (b : Fin N → ℂ)
       (L : (Option (Fin K) → ℂ) →L[ℂ] (Fin N → ℂ))
       (h : Fin K → Fin N → ℂ)
       (x : Fin D → ℂ × (Fin K → ℂ)) (hx : Function.Injective x)
       (hz : ∀ j, polarPair (fun y => eval y P)
         (fun z => b + L (optionProduct.symm z)) h (x j) = 0)
       (hs : ∀ j, (fderiv ℂ (polarPair (fun y => eval y P)
         (fun z => b + L (optionProduct.symm z)) h) (x j)).IsInvertible) :
       D ≤ ((X (0 : Fin 3) + X 1)^n * (X 0 + X 2)^(n-1) *
   …

   Mentions: OAI.PermanentBorder.Poly, OAI.PermanentBorder.HasBorderDeterminant