SmoothFiniteRegularization.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Removing finitely many actual character poles simultaneously

theorem OAI.Ostmann.smoothContour_finite_regularization line 14

Source documentation

Fill in the removable values after subtracting the principal parts of all zeros in a prescribed region. The pole set is the actual zero set in that region.

theorem smoothContour_finite_regularization (χ : PrimitiveComplexCharacter)
    (X : ℝ) (hX : 0 < X) (K : Set ℂ) (S : Finset ℂ)
    (hzeros : ∀ z ∈ K, χ.L z = 0 → z ∈ S) :
    ∃ F : ℂ → ℂ, AnalyticOnNhd ℂ F K ∧
      ∀ z ∉ S, F z = (-deriv χ.L z / χ.L z) * smoothContourWeight X z +
        ∑ w ∈ S, (analyticOrderNatAt χ.L w : ℂ) * smoothContourWeight X w / (z - w) := by
…

Mentions: OAI.Ostmann.PrimitiveComplexCharacter, OAI.Ostmann.smoothContourWeight