TaylorMultiplicity.lean`

29 declarations, 0 contain sorry, 0 declared as axioms

Translation, Taylor coefficients, and ordinary multiplicity

theorem OAI.Nagata.AffineMultiplicity.cancel_nonmember_maximal_power line 21
theorem OAI.Nagata.AffineMultiplicity.orderAtLeast_cancel_nonvanishing line 40
def OAI.Nagata.AffineMultiplicity.translateHom line 60
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:49 (different declaration text). Qualify references as OAI.Nagata.AffineMultiplicity.translateHom@path.
theorem OAI.Nagata.AffineMultiplicity.translateHom_C line 63
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:53 (different declaration text). Qualify references as OAI.Nagata.AffineMultiplicity.translateHom_C@path.
theorem OAI.Nagata.AffineMultiplicity.translateHom_X line 67
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:57 (different declaration text). Qualify references as OAI.Nagata.AffineMultiplicity.translateHom_X@path.
theorem OAI.Nagata.AffineMultiplicity.translateHom_neg_comp line 71
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:61 (different declaration text). Qualify references as OAI.Nagata.AffineMultiplicity.translateHom_neg_comp@path.
theorem OAI.Nagata.AffineMultiplicity.translateHom_comp_neg line 77
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:67 (different declaration text). Qualify references as OAI.Nagata.AffineMultiplicity.translateHom_comp_neg@path.
def OAI.Nagata.AffineMultiplicity.translateEquiv line 81
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:71 (different declaration text). Qualify references as OAI.Nagata.AffineMultiplicity.translateEquiv@path.
theorem OAI.Nagata.AffineMultiplicity.translateEquiv_apply line 87
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:77 (different declaration text). Qualify references as OAI.Nagata.AffineMultiplicity.translateEquiv_apply@path.
theorem OAI.Nagata.AffineMultiplicity.eval_zero_translate line 90
theorem OAI.Nagata.AffineMultiplicity.eval_translate line 111
Source documentation
Actual polynomial evaluation intertwines coordinate translation with translation of the input point, at every point, not only at the origin.
```
theorem eval_translate (p x : σ → R) (f : MvPolynomial σ R) :
    MvPolynomial.eval x (translateHom p f) = MvPolynomial.eval (x + p) f := by
…
```
theorem OAI.Nagata.AffineMultiplicity.pointIdeal_zero_eq_idealOfVars line 134
theorem OAI.Nagata.AffineMultiplicity.orderAtLeast_iff_taylor_coeff line 145
Source documentation
Vanishing order at p is exactly vanishing of every coefficient below total degree m after the explicit translation X ↦ X+p.
```
theorem orderAtLeast_iff_taylor_coeff (p : σ → R) (m : ℕ) (f : MvPolynomial σ R) :
    orderAtLeast p m f ↔
      ∀ a : σ →₀ ℕ, Finsupp.degree a < m → (translateHom p f).coeff a = 0 := by
…
```
theorem OAI.Nagata.AffineMultiplicity.translate_ne_zero line 173
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:80 (different declaration text). Qualify references as OAI.Nagata.AffineMultiplicity.translate_ne_zero@path.
theorem OAI.Nagata.AffineMultiplicity.translated_support_nonempty line 180
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:87 (different declaration text). Qualify references as OAI.Nagata.AffineMultiplicity.translated_support_nonempty@path.
theorem OAI.Nagata.AffineMultiplicity.translated_support_finite line 184
def OAI.Nagata.AffineMultiplicity.ordinaryMultiplicity line 189
Source documentation
The ordinary multiplicity is a finite minimum of genuine Taylor degrees.
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:92 (different declaration text). Qualify references as OAI.Nagata.AffineMultiplicity.ordinaryMultiplicity@path.
```
noncomputable def ordinaryMultiplicity (p : σ → R) (f : MvPolynomial σ R)
    (hf : f ≠ 0) : ℕ :=
…
```

theorem OAI.Nagata.AffineMultiplicity.ordinaryMultiplicity_attained line 194

Source documentation

The minimum is attained by an actual nonzero coefficient.

theorem ordinaryMultiplicity_attained (p : σ → R) (f : MvPolynomial σ R)
    (hf : f ≠ 0) :
    ∃ a : σ →₀ ℕ, (translateHom p f).coeff a ≠ 0 ∧
      ordinaryMultiplicity p f hf = Finsupp.degree a := by
…

theorem OAI.Nagata.AffineMultiplicity.orderAtLeast_iff_le_ordinaryMultiplicity line 203

Source documentation

The baseline lower-bound predicate agrees with the actual numeric order.

theorem orderAtLeast_iff_le_ordinaryMultiplicity
    (p : σ → R) (m : ℕ) (f : MvPolynomial σ R) (hf : f ≠ 0) :
    orderAtLeast p m f ↔ m ≤ ordinaryMultiplicity p f hf := by
…

theorem OAI.Nagata.AffineMultiplicity.orderAtLeast_ordinaryMultiplicity line 214
theorem OAI.Nagata.AffineMultiplicity.not_orderAtLeast_succ_ordinaryMultiplicity line 218

theorem OAI.Nagata.AffineMultiplicity.ordinaryMultiplicity_equiv line 225

Source documentation

Any actual evaluation-compatible polynomial-ring isomorphism preserves the finite minimum; its nonzero and coordinate hypotheses are explicit.

theorem ordinaryMultiplicity_equiv {τ : Type*}
    (p : σ → R) (q : τ → R)
    (e : MvPolynomial σ R ≃+* MvPolynomial τ R)
    (he : ∀ f, MvPolynomial.eval q (e f) = MvPolynomial.eval p f)
    (f : MvPolynomial σ R) (hf : f ≠ 0) (hef : e f ≠ 0) :
    ordinaryMultiplicity q (e f) hef = ordinaryMultiplicity p f hf := by
…

theorem OAI.Nagata.AffineMultiplicity.ordinaryMultiplicity_translate line 241
Source documentation
Actual translation preserves numerical multiplicity when its center is moved to the origin. The coordinate isomorphism is explicitly constructed.
```
theorem ordinaryMultiplicity_translate (p : σ → R) (f : MvPolynomial σ R)
    (hf : f ≠ 0) :
    ordinaryMultiplicity (0 : σ → R) (translateHom p f) (translate_ne_zero p f hf) =
      ordinaryMultiplicity p f hf :=
…
```
theorem OAI.Nagata.AffineMultiplicity.ordinaryMultiplicity_unit_mul line 248
theorem OAI.Nagata.AffineMultiplicity.ordinaryMultiplicity_mul_lower_bound line 260
theorem OAI.Nagata.AffineMultiplicity.ordinaryMultiplicity_pow_lower_bound line 268
theorem OAI.Nagata.AffineMultiplicity.ordinaryMultiplicity_nonvanishing_mul line 280
Source documentation
Nonvanishing multipliers are units in the local ring and leave the actual minimum unchanged, even when they are not units in the polynomial ring.
```
theorem ordinaryMultiplicity_nonvanishing_mul (p : σ → F) (f g : MvPolynomial σ F)
    (hf : f ≠ 0) (hgf : g * f ≠ 0) (hg : MvPolynomial.eval p g ≠ 0) :
    ordinaryMultiplicity p (g * f) hgf = ordinaryMultiplicity p f hf := by
…
```
theorem OAI.Nagata.AffineMultiplicity.pointIdeal_finTwo_zero line 303
theorem OAI.Nagata.AffineMultiplicity.orderAtLeast_finTwo_iff_taylor_coeff line 324
Source documentation
Exact ordinary multiplicity criterion for a plane polynomial, including mixed Taylor coefficients and order zero.
```
theorem orderAtLeast_finTwo_iff_taylor_coeff
    (p : Fin 2 → R) (m : ℕ) (f : MvPolynomial (Fin 2) R) :
    orderAtLeast p m f ↔ ∀ ell b : ℕ, ell + b < m →
      (translateHom p f).coeff (Nagata.Workers.W30.exponentPair ell b) = 0 := by
…
```
Mentions: OAI.Nagata.Workers.W30.exponentPair