AnalyticTaylor.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Polynomial Taylor expansions and analytic multiplicity

theorem OAI.Nagata.Workers.W28.analytic_order_zero line 21
theorem OAI.Nagata.Workers.W28.analytic_order_add line 27
theorem OAI.Nagata.Workers.W28.analytic_order_const_smul line 37
theorem OAI.Nagata.Workers.W28.monomial_hasAnalyticOrderAtLeast line 47
Source documentation
A bivariate monomial has a convergent power series with every coefficient below its total degree zero.
```
theorem monomial_hasAnalyticOrderAtLeast (a b m : ℕ) (hm : m ≤ a + b) :
    HasAnalyticOrderAtLeast (𝕜 := ℂ)
…
```
Mentions: OAI.Nagata.Workers.W28.HasAnalyticOrderAtLeast
theorem OAI.Nagata.Workers.W28.analytic_order_finset_sum line 73
Source documentation
Finite sums of actual analytic Taylor expansions with the same vanishing range retain that range.
```
theorem analytic_order_finset_sum {ι : Type*} (s : Finset ι)
    (f : ι → ℂ × ℂ → ℂ) (m : ℕ)
    (hf : ∀ i ∈ s, HasAnalyticOrderAtLeast (𝕜 := ℂ) (f i) 0 m) :
…
```
Mentions: OAI.Nagata.Workers.W28.HasAnalyticOrderAtLeast
theorem OAI.Nagata.Workers.W28.eval_hasAnalyticOrderAtLeast_of_coeff line 98
Source documentation
The actual low-degree coefficient criterion for a centered bivariate polynomial yields a genuine convergent Taylor expansion with those terms zero.
```
theorem eval_hasAnalyticOrderAtLeast_of_coeff
    (P : MvPolynomial (Fin 2) ℂ) (m : ℕ)
    (hcoeff : ∀ ell b, ell + b < m → P.coeff (Nagata.Workers.W30.exponentPair ell b) = 0) :
    HasAnalyticOrderAtLeast (𝕜 := ℂ)
…
```
Mentions: OAI.Nagata.Workers.W30.exponentPair, OAI.Nagata.Workers.W28.HasAnalyticOrderAtLeast
theorem OAI.Nagata.Workers.W28.polynomial_order_implies_analytic_order line 134
Source documentation
The actual polynomial evaluated on the affine complex plane has the analytic Taylor vanishing forced by its actual maximal-ideal-power order.
```
theorem polynomial_order_implies_analytic_order
    (P : MvPolynomial (Fin 2) ℂ) (p : ℂ × ℂ) (m : ℕ)
    (hP : Nagata.AffineMultiplicity.orderAtLeast
      (fun i : Fin 2 => if i = 0 then p.1 else p.2) m P) :
    HasAnalyticOrderAtLeast (𝕜 := ℂ)
…
```
Mentions: OAI.Nagata.Workers.W28.HasAnalyticOrderAtLeast