AnalyticOrder.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Analytic coefficient order, nested order, and ideal-power multiplicity

theorem OAI.Nagata.W18.scalarExpression_iteratedDeriv_zero line 21
Source documentation
Exact transverse derivative of an actual polynomial of function coefficients. No analyticity assumption on the coefficient functions is needed for this identity.
```
theorem scalarExpression_iteratedDeriv_zero
    (F : Polynomial (ℂ → ℂ)) (j : ℕ) (z : ℂ) :
    iteratedDeriv j (fun w => scalarExpression F z w) 0 =
      (j.factorial : ℂ) * F.coeff j z := by
…
```

theorem OAI.Nagata.W18.analyticOrderAt_nonzero_const_mul line 40

Source documentation

Nonzero constant multiplication preserves analytic order of an analytic germ.

theorem analyticOrderAt_nonzero_const_mul
    (f : ℂ → ℂ) (a c : ℂ) (hc : c ≠ 0) (hf : AnalyticAt ℂ f a) :
    analyticOrderAt (fun z => c * f z) a = analyticOrderAt f a := by
…

theorem OAI.Nagata.W18.scalar_coefficient_analyticAt line 49

Source documentation

Joint analyticity forces analyticity of every actual function coefficient, including indices above the polynomial degree.

theorem scalar_coefficient_analyticAt
    (F : Polynomial (ℂ → ℂ)) (a : ℂ) (j : ℕ)
    (hF : AnalyticAt ℂ (fun p : ℂ × ℂ => scalarExpression F p.1 p.2) (a, 0)) :
    AnalyticAt ℂ (F.coeff j) a := by
…

theorem OAI.Nagata.W18.scalar_coefficient_order line 67
Source documentation
Ordinary analytic order at a zero-displacement point gives order m-j of every genuine scalar coefficient, with natural truncated subtraction.
```
theorem scalar_coefficient_order
    (F : Polynomial (ℂ → ℂ)) (a : ℂ) (m j : ℕ)
    (hF : Nagata.Workers.W28.HasAnalyticOrderAtLeast (𝕜 := ℂ)
…
```
Mentions: OAI.Nagata.Workers.W28.HasAnalyticOrderAtLeast

theorem OAI.Nagata.W18.polynomial_coeff_zero_of_centered_powerSeries line 104

Source documentation

Centered convergent-series vanishing forces every low polynomial coefficient zero. The nonzero factorials are cancelled in the actual field ℂ.

theorem polynomial_coeff_zero_of_centered_powerSeries
    (P : MvPolynomial (Fin 2) ℂ)
    (S : FormalMultilinearSeries ℂ (ℂ × ℂ) ℂ)
    (hS : HasFPowerSeriesAt (fun z : ℂ × ℂ => planeValue P z.1 z.2) S 0)
    (m : ℕ) (hzero : ∀ n < m, S n = 0) :
    ∀ ell b : ℕ, ell + b < m → P.coeff (exponentPair ell b) = 0 := by
…

theorem OAI.Nagata.W18.polynomial_ideal_order_of_powerSeries line 121

Source documentation

A convergent series at any actual affine point with low terms zero forces membership in the corresponding point-ideal power.

theorem polynomial_ideal_order_of_powerSeries
    (P : MvPolynomial (Fin 2) ℂ) (p : ℂ × ℂ)
    (S : FormalMultilinearSeries ℂ (ℂ × ℂ) ℂ)
    (hS : HasFPowerSeriesAt (fun z : ℂ × ℂ => planeValue P z.1 z.2) S p)
    (m : ℕ) (hzero : ∀ n < m, S n = 0) :
    orderAtLeast (planePoint p.1 p.2) m P := by
…

theorem OAI.Nagata.W18.planePoint_eq_coordinate_function line 140
theorem OAI.Nagata.W18.polynomial_analytic_order_implies_ideal_order line 145
theorem OAI.Nagata.W18.polynomial_analytic_order_iff_ideal_order line 159
Source documentation
Ordinary ideal-power multiplicity and existence of a genuine convergent Taylor expansion with low terms zero are equivalent for actual plane polynomials.
```
theorem polynomial_analytic_order_iff_ideal_order
    (P : MvPolynomial (Fin 2) ℂ) (p : ℂ × ℂ) (m : ℕ) :
    HasAnalyticOrderAtLeast (𝕜 := ℂ)
…
```
theorem OAI.Nagata.W18.nested_ideal_order_of_analytic_order line 170
Source documentation
The analytic normal-limit order can now be passed to the actual nested polynomial point ideal used by the coefficient and fiber-order package.
```
theorem nested_ideal_order_of_analytic_order
    (P : MvPolynomial (Fin 2) ℂ) (a c : ℂ) (m : ℕ)
    (hP : HasAnalyticOrderAtLeast (𝕜 := ℂ)
…
```
theorem OAI.Nagata.W18.analytic_top_coefficient_base_divisibility line 184
Source documentation
Analytic order directly forces base order of the highest possible fiber coefficient of the actual local polynomial.
```
theorem analytic_top_coefficient_base_divisibility
    (P : MvPolynomial (Fin 2) ℂ) (a c : ℂ) (m J : ℕ)
    (hP : HasAnalyticOrderAtLeast (𝕜 := ℂ)
…
```
theorem OAI.Nagata.W18.analytic_fiber_power_divides line 195
Source documentation
Analytic order directly gives the actual marked fiber root divisibility.
```
theorem analytic_fiber_power_divides
    (P : MvPolynomial (Fin 2) ℂ) (a c : ℂ) (m : ℕ)
    (hP : HasAnalyticOrderAtLeast (𝕜 := ℂ)
…
```

theorem OAI.Nagata.W18.nestedEvaluation_eq_polynomialEvaluation line 219

Source documentation

Explicit inverse-coordinate evaluation identity.

theorem nestedEvaluation_eq_polynomialEvaluation
    (H : Polynomial (Polynomial ℂ)) (z : ℂ × ℂ) :
    (H.eval (Polynomial.C z.2)).eval z.1 =
      MvPolynomial.eval (fun i : Fin 2 => if i = 0 then z.1 else z.2)
        (nestedToBivariate H) := by
…

Mentions: OAI.Nagata.W18.nestedToBivariate

theorem OAI.Nagata.W18.nested_polynomial_ideal_order_of_analytic_order line 235
Source documentation
A genuine convergent analytic-order statement for H(U,W) implies its actual nested point-ideal-power membership.
```
theorem nested_polynomial_ideal_order_of_analytic_order
    (H : Polynomial (Polynomial ℂ)) (a c : ℂ) (m : ℕ)
    (hH : HasAnalyticOrderAtLeast (𝕜 := ℂ)
…
```

theorem OAI.Nagata.W18.nested_polynomial_ideal_order_of_powerSeries line 250

Source documentation

Direct genuine-series version of the nested polynomial order bridge.

theorem nested_polynomial_ideal_order_of_powerSeries
    (H : Polynomial (Polynomial ℂ)) (a c : ℂ)
    (S : FormalMultilinearSeries ℂ (ℂ × ℂ) ℂ)
    (hS : HasFPowerSeriesAt
      (fun z : ℂ × ℂ => (H.eval (Polynomial.C z.2)).eval z.1) S (a, c))
    (m : ℕ) (hzero : ∀ n < m, S n = 0) :
    H ∈ (nestedPointIdeal a c) ^ m :=
…

Mentions: OAI.Nagata.W18.nestedPointIdeal

theorem OAI.Nagata.W18.nested_analytic_top_coefficient_divisibility line 261
Source documentation
The analytic limit's actual local polynomial top coefficient has the required base vanishing divisibility.
```
theorem nested_analytic_top_coefficient_divisibility
    (H : Polynomial (Polynomial ℂ)) (a c : ℂ) (m J : ℕ)
    (hH : HasAnalyticOrderAtLeast (𝕜 := ℂ)
…
```
theorem OAI.Nagata.W18.nested_analytic_fiber_divisibility line 271
Source documentation
The analytic limit's actual local polynomial has the required fiber root.
```
theorem nested_analytic_fiber_divisibility
    (H : Polynomial (Polynomial ℂ)) (a c : ℂ) (m : ℕ)
    (hH : HasAnalyticOrderAtLeast (𝕜 := ℂ)
…
```