Theorems · Theorem · complex analysis

hasDerivAt_circleAverage_herglotzRieszKernel_smul

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {R : ℝ} {w : ℂ},
  CircleIntegrable f 0 R →
    w ∈ Metric.ball 0 R →
      HasDerivAt (fun w => Real.circleAverage (fun ζ => herglotzRieszKernel 0 w ζ • f ζ) 0 R)
        (Real.circleAverage (fun ζ => (2 * ζ / (ζ - w) ^ 2) • f ζ) 0 R) w

Derivative of the Herglotz–Riesz kernel integral: if f is circle integrable and w lies inside the circle, then w ↦ circleAverage (fun ζ ↦ herglotzRieszKernel 0 w ζ • f ζ) 0 R has derivative circleAverage (fun ζ ↦ (2 * ζ / (ζ - w) ^ 2) • f ζ) 0 R at w.

Defined in

Mathlib.Analysis.Complex.Poisson

Cited by

1 results in Mathlib

Foundations

Depth 266 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace