AnalyticFactorization.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Analytic factorization, punctured identities, and holomorphic divisibility

theorem OAI.Nagata.W19.analyticOnNhd_dslope line 27

Source documentation

The divided slope of an analytic function extends analytically at its center.

theorem analyticOnNhd_dslope {U : Set ℂ} {h : ℂ → ℂ}
    (hh : AnalyticOnNhd ℂ h U) (a : ℂ) (ha : a ∈ U) :
    AnalyticOnNhd ℂ (dslope h a) U := by
…

theorem OAI.Nagata.W19.exists_analytic_centered_factor line 43

Source documentation

Divide out one centered zero while preserving holomorphicity on an open set.

theorem exists_analytic_centered_factor
    {U : Set ℂ} (hU : IsOpen U) (h : ℂ → ℂ)
    (hh : AnalyticOnNhd ℂ h U) (a : ℂ) (ha : a ∈ U)
    (k : ℕ) (ho : (k : ℕ∞) ≤ analyticOrderAt h a) :
    ∃ g : ℂ → ℂ, AnalyticOnNhd ℂ g U ∧
      ∀ z, h z = (z - a) ^ k * g z := by
…

theorem OAI.Nagata.W19.analytic_order_of_nonvanishing_analytic_factor line 78

Source documentation

A factor nonvanishing at a point contributes zero to analytic vanishing order.

theorem analytic_order_of_nonvanishing_analytic_factor
    {U : Set ℂ} (hU : IsOpen U) {h g : ℂ → ℂ}
    (hg : AnalyticOnNhd ℂ g U) {a b : ℂ} (hb : b ∈ U)
    (hab : b ≠ a) (k : ℕ) (heq : ∀ z, h z = (z - a) ^ k * g z) :
    analyticOrderAt h b = analyticOrderAt g b := by
…

theorem OAI.Nagata.W19.exists_analytic_finset_factorization line 91

Source documentation

Simultaneously divide out finitely many distinct centers with prescribed order.

theorem exists_analytic_finset_factorization
    {I : Type*} (s : Finset I) {U : Set ℂ} (hU : IsOpen U)
    (h : ℂ → ℂ) (hh : AnalyticOnNhd ℂ h U)
    (ξ : I → ℂ) (hξ : Function.Injective ξ) (hmem : ∀ i ∈ s, ξ i ∈ U)
    (k : ℕ) (ho : ∀ i ∈ s, (k : ℕ∞) ≤ analyticOrderAt h (ξ i)) :
    ∃ g : ℂ → ℂ, AnalyticOnNhd ℂ g U ∧
      ∀ z, h z = (∏ i ∈ s, (z - ξ i) ^ k) * g z := by
…

theorem OAI.Nagata.W19.exists_analytic_factorization line 116

Source documentation

Interface consumed by the holomorphic collision estimate.

theorem exists_analytic_factorization
    {q : ℕ} {U : Set ℂ} (hU : IsOpen U) (h : ℂ → ℂ)
    (hh : AnalyticOnNhd ℂ h U) (ξ : Fin q → ℂ)
    (hξ : Function.Injective ξ) (hmem : ∀ i, ξ i ∈ U)
    (k : ℕ) (ho : ∀ i, (k : ℕ∞) ≤ analyticOrderAt h (ξ i)) :
    ∃ g : ℂ → ℂ, AnalyticOnNhd ℂ g U ∧
      ∀ z, h z = (∏ i, (z - ξ i) ^ k) * g z := by
…

theorem OAI.Nagata.W19.puncturedPlane_nonempty line 137
theorem OAI.Nagata.W19.puncturedPlane_eq_exp_range line 140
theorem OAI.Nagata.W19.puncturedPlane_isConnected line 148
theorem OAI.Nagata.W19.holomorphic_punctured_mul_zero line 152
theorem OAI.Nagata.W19.exists_holomorphic_centered_factor line 171
theorem OAI.Nagata.W19.analytic_order_of_nonvanishing_factor line 180
theorem OAI.Nagata.W19.exists_holomorphic_finset_factorization line 187

theorem OAI.Nagata.W19.exists_holomorphic_factorization line 199

Source documentation

Interface consumed by the holomorphic collision estimate.

theorem exists_holomorphic_factorization
    {q : ℕ} {U : Set ℂ} (hU : IsOpen U) (h : ℂ → ℂ)
    (hh : DifferentiableOn ℂ h U) (ξ : Fin q → ℂ)
    (hξ : Function.Injective ξ) (hmem : ∀ i, ξ i ∈ U)
    (k : ℕ) (ho : ∀ i, (k : ℕ∞) ≤ analyticOrderAt h (ξ i)) :
    ∃ g : ℂ → ℂ, DifferentiableOn ℂ g U ∧
      ∀ z, h z = (∏ i, (z - ξ i) ^ k) * g z := by
…

theorem OAI.Nagata.W19.differentiableOn_polynomial_eval line 222
theorem OAI.Nagata.W19.polynomial_eval_punctured_mul_zero line 235

theorem OAI.Nagata.W19.cubic_sections_polynomial_mul_zero line 249

Source documentation

The exact three-section specialization used for the degree-three map.

theorem cubic_sections_polynomial_mul_zero {τ γ : ℂ}
    (s : Fin 3 → Nagata.W08.automorphicSections τ 3 γ)
    (P Q : MvPolynomial (Fin 3) ℂ)
    (hPQ : ∀ z, z ≠ 0 → MvPolynomial.eval (fun i => (s i).val z) (P * Q) = 0) :
    (∀ z, z ≠ 0 → MvPolynomial.eval (fun i => (s i).val z) P = 0) ∨
      (∀ z, z ≠ 0 → MvPolynomial.eval (fun i => (s i).val z) Q = 0) := by
…

Mentions: OAI.Nagata.W08.automorphicSections