OAI/Algebra/Determinantal/InitialForm.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PermanentBorder.InitialHomogeneous.dilation line 13
2. lemma OAI.PermanentBorder.InitialHomogeneous.dilation_eq_aeval line 17
3. lemma OAI.PermanentBorder.InitialHomogeneous.dilation_monomial line 25
4. lemma OAI.PermanentBorder.InitialHomogeneous.coeff_dilation line 32
5. def OAI.PermanentBorder.InitialHomogeneous.normalizedDilation line 44
6. lemma OAI.PermanentBorder.InitialHomogeneous.coeff_eq_zero_of_lower_components line 48
7. lemma OAI.PermanentBorder.InitialHomogeneous.coeff_normalizedDilation line 54
8. theorem OAI.PermanentBorder.InitialHomogeneous.normalizedDilation_tendsto line 69

   Source documentation

   Cancellation of the pole gives coefficientwise convergence along any filter approaching zero through nonzero complex values.

   theorem normalizedDilation_tendsto {α : Type*} {l : Filter α}
       {q : Poly σ} {r : ℕ}
       (hlow : ∀ j < r, homogeneousComponent j q = 0)
       {t : α → ℂ} (ht : Tendsto t l (𝓝 0))
       (hne : ∀ᶠ j in l, t j ≠ 0) (e : σ →₀ ℕ) :
       Tendsto (fun j => (normalizedDilation r q (t j)).coeff e)
         l (𝓝 ((homogeneousComponent r q).coeff e)) := by
   …

   Mentions: OAI.PermanentBorder.Poly, OAI.PermanentBorder.InitialHomogeneous.normalizedDilation

9. theorem OAI.PermanentBorder.InitialHomogeneous.normalizedDilation_tendsto_positive line 93

   Source documentation

   Normalized dilation converges coefficientwise as the positive real scale tends to zero.

   theorem normalizedDilation_tendsto_positive {q : Poly σ} {r : ℕ}
       (hlow : ∀ j < r, homogeneousComponent j q = 0) (e : σ →₀ ℕ) :
       Tendsto (fun t : ℝ => (normalizedDilation r q (t : ℂ)).coeff e)
         (𝓝[Set.Ioi 0] 0) (𝓝 ((homogeneousComponent r q).coeff e)) := by
   …

   Mentions: OAI.PermanentBorder.Poly, OAI.PermanentBorder.InitialHomogeneous.normalizedDilation

10. theorem OAI.PermanentBorder.HasBorderDeterminant.lowest_homogeneousComponent line 106

    Source documentation

    The lowest homogeneous component inherits the fixed border determinant size by degeneration along a geometric sequence of nonzero scales.

    theorem HasBorderDeterminant.lowest_homogeneousComponent
        {σ : Type*} [Fintype σ] {n r : ℕ} {q : Poly σ}
        (hb : HasBorderDeterminant n q)
        (hlow : ∀ j < r, homogeneousComponent j q = 0) :
        HasBorderDeterminant n (homogeneousComponent r q) := by
    …

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

11. theorem OAI.PermanentBorder.smooth_initial_form_lower_bound line 128

    Source documentation

    A smooth lowest homogeneous term after translation bounds both border and exact determinant sizes by the product of its degree minus one and dimension minus one, divided by 4 * Real.exp 1.

    Distinct definitions of this name: ComparatorChallenges/SmoothInitialForm.lean:35 (different declaration text). Qualify references as OAI.PermanentBorder.smooth_initial_form_lower_bound@path.

    theorem smooth_initial_form_lower_bound (d r : ℕ) (g : Poly (Fin d))
        (a : Fin d → ℂ) (hd : 2 ≤ d) (hr : 2 ≤ r)
        (_hG : homogeneousComponent r
          (affineSubstitution a (fun i j : Fin d => if i = j then 1 else 0) g) ≠ 0)
        (hlow : ∀ j < r, homogeneousComponent j
          (affineSubstitution a (fun i j : Fin d => if i = j then 1 else 0) g) = 0)
        (hs : ∀ y : Fin d → ℂ,
          eval y (homogeneousComponent r
            (affineSubstitution a (fun i j : Fin d => if i = j then 1 else 0) g)) = 0 →
          (∀ i, eval y (pderiv i (homogeneousComponent r
            (affineSubstitution a (fun i j : Fin d => if i = j then 1 else 0) g))) = 0) →
          y = 0) :
    …

    Mentions: OAI.PermanentBorder.Poly