Extending primitives from a convex part of a disc

Mathlib's DifferentiableOn.isExactOn_ball gives every holomorphic function on a disc a primitive there. This file records the gluing consequence: a primitive of the same integrand on a convex part of the disc extends to a primitive on the whole disc, because two primitives of one function differ by a constant on a convex set.

Main results

• DifferentiableOn.exists_hasDerivAt_eqOn_ball_inter -- a primitive of a holomorphic integrand on ball c r ∩ U, for convex U, is the restriction of a primitive on ball c r.

theorem DifferentiableOn.exists_hasDerivAt_eqOn_ball_inter {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f g : ℂ → E} {c : ℂ} {r : ℝ} {U : Set ℂ} (hg : DifferentiableOn ℂ g (Metric.ball c r)) (hU : Convex ℝ U) (hf : ∀ z ∈ Metric.ball c r ∩ U, HasDerivWithinAt f (g z) (Metric.ball c r ∩ U) z) : ∃ (G : ℂ → E), (∀ z ∈ Metric.ball c r, HasDerivAt G (g z) z) ∧ Set.EqOn G f (Metric.ball c r ∩ U)

A holomorphic integrand g on a disc has a primitive on the disc agreeing with any given primitive f of g on the intersection of the disc with a convex set U.