Theorems · Theorem · complex analysis

Complex.IsConservativeOn.eventually_nhds_wedgeIntegral_sub_wedgeIntegral

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {c : ℂ} {r : ℝ} {f : ℂ → E},
  ContinuousOn f (Metric.ball c r) →
    ∀ {z : ℂ},
      z ∈ Metric.ball c r →
        Complex.IsConservativeOn f (Metric.ball c r) →
          ∀ᶠ (w : ℂ) in nhds z, c.wedgeIntegral w f - c.wedgeIntegral z f = z.wedgeIntegral w f

If a function f IsConservativeOn on a disk of center c, then for points z in this disk, the wedge integral from c to z is additive under a detour through a nearby point w.

Defined in

Mathlib.Analysis.Complex.HasPrimitives

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace