OAI/AlgebraicGeometry/PlaneCurves/Collision.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Nagata.W20.order_collision_of_holomorphic_factorization line 20

   Source documentation

   A quantitative holomorphic collision theorem. The total vanishing order is k times the number of centers, with no convergence assumption on quotients.

   theorem order_collision_of_holomorphic_factorization {ι : Type*} [Fintype ι]
       (ξ : ℕ → ι → ℂ) (k : ℕ) (H G : ℕ → ℂ → ℂ) (f : ℂ → ℂ)
       {r M : ℝ} (hr : 0 < r)
       (hξlim : ∀ i, Tendsto (fun n => ξ n i) atTop (𝓝 0))
       (hξbound : ∀ᶠ n in atTop, ∀ i, ‖ξ n i‖ ≤ r / 2)
       (hf : DifferentiableOn ℂ f (ball 0 r))
       (hlim : ∀ z ∈ ball (0 : ℂ) r, Tendsto (fun n => H n z) atTop (𝓝 (f z)))
       (hG : ∀ n, DiffContOnCl ℂ (G n) (ball 0 r))
       (hfactor : ∀ n, ∀ z ∈ closedBall (0 : ℂ) r,
         H n z = (∏ i, (z - ξ n i) ^ k) * G n z)
       (hupper : ∀ᶠ n in atTop, ∀ z ∈ sphere (0 : ℂ) r, ‖H n z‖ ≤ M) :
       (↑(k * Fintype.card ι) : ℕ∞) ≤ analyticOrderAt f 0 := by
   …

2. theorem OAI.Nagata.W20.collision_of_locally_uniform_limit_and_factorizations line 54

   Source documentation

   Collision on an actual open complex domain. Locally uniform convergence supplies holomorphicity of the limit and the required uniform boundary bound; only the genuine holomorphic factorizations remain as explicit inputs.

   theorem collision_of_locally_uniform_limit_and_factorizations
       {ι : Type*} [Fintype ι] {U : Set ℂ} (hU : IsOpen U)
       (ξ : ℕ → ι → ℂ) (k : ℕ) (H G : ℕ → ℂ → ℂ) (f : ℂ → ℂ)
       {r : ℝ} (hr : 0 < r) (hsub : closedBall (0 : ℂ) r ⊆ U)
       (hξlim : ∀ i, Tendsto (fun n => ξ n i) atTop (𝓝 0))
       (hH : ∀ n, DifferentiableOn ℂ (H n) U)
       (hlim : TendstoLocallyUniformlyOn H f atTop U)
       (hG : ∀ n, DifferentiableOn ℂ (G n) U)
       (hfactor : ∀ n, ∀ z ∈ U, H n z = (∏ i, (z - ξ n i) ^ k) * G n z) :
       (↑(k * Fintype.card ι) : ℕ∞) ≤ analyticOrderAt f 0 := by
   …

3. theorem OAI.Nagata.W20.holomorphic_collision_order line 99

   Source documentation

   Colliding q distinct zeros of order at least k produces a zero of order at least q*k in the locally uniform holomorphic limit.

   theorem holomorphic_collision_order {q : ℕ} {U : Set ℂ}
       (hU : IsOpen U) (h0 : (0 : ℂ) ∈ U)
       (ξ : ℕ → Fin q → ℂ) (k : ℕ) (H : ℕ → ℂ → ℂ) (f : ℂ → ℂ)
       (hξlim : ∀ i, Tendsto (fun n => ξ n i) atTop (𝓝 0))
       (hξinj : ∀ n, Function.Injective (ξ n))
       (hξmem : ∀ n i, ξ n i ∈ U)
       (hH : ∀ n, DifferentiableOn ℂ (H n) U)
       (hlim : TendstoLocallyUniformlyOn H f atTop U)
       (horder : ∀ n i, (k : ℕ∞) ≤ analyticOrderAt (H n) (ξ n i)) :
       (↑(q * k) : ℕ∞) ≤ analyticOrderAt f 0 := by
   …

4. theorem OAI.Nagata.W20.holomorphic_collision_jets line 124

   Source documentation

   Derivative form of the collision theorem, matching the row conditions of the manuscript's fixed-surface jet map.

   theorem holomorphic_collision_jets {q : ℕ} {U : Set ℂ}
       (hU : IsOpen U) (h0 : (0 : ℂ) ∈ U)
       (ξ : ℕ → Fin q → ℂ) (k : ℕ) (H : ℕ → ℂ → ℂ) (f : ℂ → ℂ)
       (hξlim : ∀ i, Tendsto (fun n => ξ n i) atTop (𝓝 0))
       (hξinj : ∀ n, Function.Injective (ξ n))
       (hξmem : ∀ n i, ξ n i ∈ U)
       (hH : ∀ n, DifferentiableOn ℂ (H n) U)
       (hlim : TendstoLocallyUniformlyOn H f atTop U)
       (horder : ∀ n i, (k : ℕ∞) ≤ analyticOrderAt (H n) (ξ n i)) :
       ∀ ℓ < q * k, iteratedDeriv ℓ f 0 = 0 := by
   …