FrechetMultiplicity.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Frechet derivatives, transverse jets, and analytic multiplicity

theorem OAI.Nagata.W19.directional_derivative_taylor_vanishing line 30

Source documentation

One constant directional derivative lowers total Taylor vanishing order by at most one.

theorem directional_derivative_taylor_vanishing
    {H : E → ℂ} {p : E} (hH : AnalyticAt ℂ H p) (v : E) (m : ℕ)
    (hvan : ∀ n < m, iteratedFDeriv ℂ n H p = 0) :
    ∀ n, n + 1 < m →
      iteratedFDeriv ℂ n (fun z => fderiv ℂ H z v) p = 0 := by
…

def OAI.Nagata.W19.directionalIterate line 46

Source documentation

Repeated constant directional differentiation as a genuine derivative operator.

noncomputable def directionalIterate (v : E) : ℕ → (E → ℂ) → E → ℂ
  | 0, H => H
  | b + 1, H => directionalIterate v b (fun z => fderiv ℂ H z v)

theorem OAI.Nagata.W19.directionalIterate_analyticAt line 50

theorem OAI.Nagata.W19.directionalIterate_taylor_vanishing line 60

Source documentation

Any number of directional derivatives reduces the total Taylor order by at most that number.

theorem directionalIterate_taylor_vanishing {H : E → ℂ} {p : E}
    (hH : AnalyticAt ℂ H p) (v : E) (m b : ℕ)
    (hvan : ∀ n < m, iteratedFDeriv ℂ n H p = 0) :
    ∀ n, n + b < m → iteratedFDeriv ℂ n (directionalIterate v b H) p = 0 := by
…

Mentions: OAI.Nagata.W19.directionalIterate

theorem OAI.Nagata.W19.analytic_pullback_taylor_vanishing line 76

Source documentation

Analytic pullback preserves vanishing of total Taylor derivatives.

theorem analytic_pullback_taylor_vanishing
    [CompleteSpace E]
    {H : E → ℂ} {p : ℂ} {γ : ℂ → E}
    (hH : AnalyticAt ℂ H (γ p)) (hγ : AnalyticAt ℂ γ p)
    (m : ℕ) (hvan : ∀ n < m, iteratedFDeriv ℂ n H (γ p) = 0) :
    ∀ n < m, iteratedFDeriv ℂ n (H ∘ γ) p = 0 := by
…

theorem OAI.Nagata.W19.transverse_restriction_order_of_total_taylor_vanishing line 95

Source documentation

The Taylor-derivative form of ordinary bivariate multiplicity yields the required univariate analytic order after transverse differentiation.

theorem transverse_restriction_order_of_total_taylor_vanishing
    {H : (ℂ × ℂ) → ℂ} (ξ : ℂ)
    (hH : AnalyticAt ℂ H (ξ, 0)) (m b : ℕ)
    (hvan : ∀ n < m, iteratedFDeriv ℂ n H (ξ, 0) = 0) :
    (m - b : ℕ) ≤ analyticOrderAt
      (fun x => directionalIterate (0, 1) b H (x, 0)) ξ := by
…

Mentions: OAI.Nagata.W19.directionalIterate

theorem OAI.Nagata.W19.directionalIterate_vertical_eq_iteratedDeriv line 115
Source documentation
Repeated transverse Fréchet differentiation is the ordinary repeated one-variable derivative in the second coordinate.
```
theorem directionalIterate_vertical_eq_iteratedDeriv
    {H : (ℂ × ℂ) → ℂ} {x y : ℂ} (hH : AnalyticAt ℂ H (x, y)) (b : ℕ) :
    directionalIterate (0, 1) b H (x, y) =
      iteratedDeriv b (fun t => H (x, t)) y := by
…
```
Mentions: OAI.Nagata.W19.directionalIterate

theorem OAI.Nagata.W19.transverse_iteratedDeriv_order_of_total_taylor_vanishing line 143

Source documentation

Actual transverse iterated derivatives satisfy the collision order bound from total Fréchet Taylor vanishing, including identically zero functions.

theorem transverse_iteratedDeriv_order_of_total_taylor_vanishing
    {H : (ℂ × ℂ) → ℂ} (ξ : ℂ)
    (hH : AnalyticAt ℂ H (ξ, 0)) (m b : ℕ)
    (hvan : ∀ n < m, iteratedFDeriv ℂ n H (ξ, 0) = 0) :
    (m - b : ℕ) ≤ analyticOrderAt
      (fun x => iteratedDeriv b (fun y => H (x, y)) 0) ξ := by
…

theorem OAI.Nagata.W19.derivSeries_coeff_zero line 169
theorem OAI.Nagata.W19.iteratedFDeriv_zero_of_series_coeff line 184

theorem OAI.Nagata.W19.total_taylor_vanishing_of_powerSeries line 203

Source documentation

Vanishing actual convergent power-series coefficients implies vanishing of total derivatives below that order.

theorem total_taylor_vanishing_of_powerSeries
    {H : E → ℂ} {p : E} {P : FormalMultilinearSeries ℂ E ℂ}
    (hP : HasFPowerSeriesAt H P p) (m : ℕ) (hzero : ∀ n < m, P n = 0) :
    ∀ n < m, iteratedFDeriv ℂ n H p = 0 := by
…

theorem OAI.Nagata.W19.transverse_iteratedDeriv_order_of_powerSeries line 212

Source documentation

Ordinary analytic power-series multiplicity gives the transverse order needed by the moving-center collision theorem.

theorem transverse_iteratedDeriv_order_of_powerSeries
    {H : (ℂ × ℂ) → ℂ} {P : FormalMultilinearSeries ℂ (ℂ × ℂ) ℂ}
    (ξ : ℂ) (hP : HasFPowerSeriesAt H P (ξ, 0))
    (m b : ℕ) (hzero : ∀ n < m, P n = 0) :
    (m - b : ℕ) ≤ analyticOrderAt
      (fun x => iteratedDeriv b (fun y => H (x, y)) 0) ξ := by
…

theorem OAI.Nagata.W19.analyticAt_transverse_iteratedDeriv line 232

Source documentation

Transverse derivatives restricted to the horizontal line are analytic.

theorem analyticAt_transverse_iteratedDeriv
    {H : (ℂ × ℂ) → ℂ} (ξ : ℂ) (hH : AnalyticAt ℂ H (ξ, 0)) (b : ℕ) :
    AnalyticAt ℂ (fun x => iteratedDeriv b (fun y => H (x, y)) 0) ξ := by
…

theorem OAI.Nagata.W19.mixed_iteratedDeriv_zero_of_powerSeries line 245

Source documentation

Explicit mixed derivative vanishing from actual convergent Taylor coefficients.

theorem mixed_iteratedDeriv_zero_of_powerSeries
    {H : (ℂ × ℂ) → ℂ} {P : FormalMultilinearSeries ℂ (ℂ × ℂ) ℂ}
    (ξ : ℂ) (hP : HasFPowerSeriesAt H P (ξ, 0)) (m : ℕ)
    (hzero : ∀ n < m, P n = 0) (ell b : ℕ) (hlt : ell + b < m) :
    iteratedDeriv ell (fun x => iteratedDeriv b (fun y => H (x, y)) 0) ξ = 0 := by
…