OAI/Algebra/Determinantal/AmbientPersistence.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PermanentBorder.AmbientPolar.polynomialSystem_differentiable line 11
2. theorem OAI.PermanentBorder.AmbientPolar.exists_affine_polar_approximant line 21

   Source documentation

   A selected finite family of simple polar zeros persists in one determinant approximant.

   theorem exists_affine_polar_approximant {n : ℕ} {P : Poly σ}
       (hb : HasBorderDeterminant n P) (b : σ → ℂ)
       (L : (Option κ → ℂ) →L[ℂ] (σ → ℂ)) (h : κ → σ → ℂ)
       (x : ι → ℂ × (κ → ℂ)) (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) :
       ∃ (A₀ : Matrix (Fin n) (Fin n) ℂ) (A : σ → Matrix (Fin n) (Fin n) ℂ)
         (y : ι → Option κ → ℂ), Function.Injective y ∧
         ∀ i, SimplePolynomialZero (operators b L h)
           (affineMatrixPolynomial n A₀ A) (y i) := by
   …

   Mentions: OAI.PermanentBorder.Poly, OAI.PermanentBorder.HasBorderDeterminant, OAI.PermanentBorder.AmbientPolar.operators, OAI.PermanentBorder.affineMatrixPolynomial

3. theorem OAI.PermanentBorder.AmbientPolar.border_polar_mixed_count line 62

   Source documentation

   The number of selected simple polar zeros is bounded by the mixed coefficient.

   theorem border_polar_mixed_count {n : ℕ} {P : Poly σ}
       (hb : HasBorderDeterminant (n+1) P) (b : σ → ℂ)
       (L : (Option κ → ℂ) →L[ℂ] (σ → ℂ)) (h : κ → σ → ℂ)
       (x : ι → ℂ × (κ → ℂ)) (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) :
       Fintype.card ι ≤
         (Multigraded.mixedPolynomial (firstGroup (κ := κ) (n := n)) secondGroup).coeff
   …

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