SmoothRectangleResidues.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The finite rectangle identity for the actual smooth character integrand

theorem OAI.Ostmann.smoothContour_rectangle_residues line 16

Source documentation

The finite contour-shift identity, with the genuine analytic zero orders. The hypotheses specify only which finite set contains the rectangle's zeros and that its points are interior; no residue or integral identity is assumed.

theorem smoothContour_rectangle_residues (χ : PrimitiveComplexCharacter)
    (X : ℝ) (hX : 0 < X) (a b c d : ℝ) (S : Finset ℂ)
    (hinside : ∀ z ∈ S, a < z.re ∧ z.re < b ∧ c < z.im ∧ z.im < d)
    (hzeros : ∀ z ∈ uIcc a b ×ℂ uIcc c d, χ.L z = 0 → z ∈ S) :
    rectangleBoundaryIntegral
      (fun z => (-deriv χ.L z / χ.L z) * smoothContourWeight X z) a b c d =
      -(2 * (Real.pi : ℂ) * I) *
        ∑ z ∈ S, (analyticOrderNatAt χ.L z : ℂ) * smoothContourWeight X z := by
…

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