MixedDerivatives.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Mixed partial derivatives and ordinary polynomial jets

def OAI.Nagata.Workers.W30.planePoint line 21
Source documentation
The ordinary affine point (x,y).
```
def planePoint (x y : ℂ) : Fin 2 → ℂ := Fin.cases x (fun _ => y)
```
lemma OAI.Nagata.Workers.W30.planePoint_zero line 23
lemma OAI.Nagata.Workers.W30.planePoint_one line 24
def OAI.Nagata.Workers.W30.planeValue line 27
Source documentation
Evaluate a genuine bivariate polynomial on its two complex coordinates.
```
noncomputable def planeValue (p : Bivariate ℂ) (x y : ℂ) : ℂ :=
…
```
Mentions: OAI.Nagata.Workers.W30.Bivariate
lemma OAI.Nagata.Workers.W30.planeValue_monomial line 30
lemma OAI.Nagata.Workers.W30.planeValue_sum line 37

lemma OAI.Nagata.Workers.W30.innerDerivative_zero line 46

Source documentation

Ordinary Y-derivatives at Y=0, retaining the X-variable.

lemma innerDerivative_zero (p : Bivariate ℂ) (b : ℕ) (x : ℂ) :
    iteratedDeriv b (fun y => planeValue p x y) 0 =
      ∑ a ∈ p.support, p.coeff a * x ^ (a 0) *
        (if b = a 1 then ((a 1).factorial : ℂ) else 0) := by
…

Mentions: OAI.Nagata.Workers.W30.Bivariate, OAI.Nagata.Workers.W30.planeValue

def OAI.Nagata.Workers.W30.mixedDerivative line 59
Source documentation
Take Y-derivatives first, and then X-derivatives, at an ordinary affine point.
```
noncomputable def mixedDerivative (ell b : ℕ) (p : Bivariate ℂ) (x y : ℂ) : ℂ :=
…
```
Mentions: OAI.Nagata.Workers.W30.Bivariate
theorem OAI.Nagata.Workers.W30.mixedDerivative_zero line 63
Source documentation
At the origin the actual mixed analytic derivative is factorial times coefficient.
```
theorem mixedDerivative_zero (ell b : ℕ) (p : Bivariate ℂ) :
    mixedDerivative ell b p 0 0 =
      (ell.factorial : ℂ) * (b.factorial : ℂ) * p.coeff (exponentPair ell b) := by
…
```
Mentions: OAI.Nagata.Workers.W30.Bivariate, OAI.Nagata.Workers.W30.mixedDerivative, OAI.Nagata.Workers.W30.exponentPair
lemma OAI.Nagata.Workers.W30.planePoint_add line 88
lemma OAI.Nagata.Workers.W30.planePoint_eta line 93
lemma OAI.Nagata.Workers.W30.planeValue_translate line 100
lemma OAI.Nagata.Workers.W30.mixedDerivative_translate_zero line 107
Source documentation
Translation commutes with actual ordinary mixed derivatives.
```
lemma mixedDerivative_translate_zero (ell b : ℕ) (p : Bivariate ℂ) (x y : ℂ) :
    mixedDerivative ell b
      (Nagata.AffineMultiplicity.translateHom (planePoint x y) p) 0 0 =
      mixedDerivative ell b p x y := by
…
```
Mentions: OAI.Nagata.Workers.W30.Bivariate, OAI.Nagata.Workers.W30.mixedDerivative, OAI.Nagata.Workers.W30.planePoint
theorem OAI.Nagata.Workers.W30.mixedDerivative_eq_translated_coefficient line 119
Source documentation
Exact factorial bridge between ordinary analytic derivatives and translated polynomial coefficients at every affine point. All orders, including zero, are retained.
```
theorem mixedDerivative_eq_translated_coefficient (ell b : ℕ) (p : Bivariate ℂ)
    (v : Fin 2 → ℂ) :
    mixedDerivative ell b p (v 0) (v 1) =
      (ell.factorial : ℂ) * (b.factorial : ℂ) *
        (Nagata.AffineMultiplicity.translateHom v p).coeff (exponentPair ell b) := by
…
```
Mentions: OAI.Nagata.Workers.W30.Bivariate, OAI.Nagata.Workers.W30.mixedDerivative, OAI.Nagata.Workers.W30.exponentPair