Planar atoms for paths-and-integrals (CC6)

Unit: paths-and-integrals (docs/design/paths-and-integrals.md §2.3). Pure-ℂ content, no manifold imports: this file is meant to be reused by dbar-solvability, residue-calculus, monodromy, and abel-weak-solutions for disk primitives and convex-minus-countable path-connectivity — do not re-prove these atoms elsewhere.

Main declarations:

• RS.exists_hasDerivAt_ball — a holomorphic function on a disk has a primitive with a prescribed value at any interior point (Morera, via mathlib's HasPrimitives.lean).
• RS.eventuallyEq_of_hasDerivAt_eq — two local primitives of the same function that agree at a point agree on a neighborhood of it.
• RS.Convex.isPathConnected_diff_countable — an open convex planar set minus a countable set is path-connected.
• RS.exists_homotopy_range_subset_of_convex — any two paths with the same endpoints inside a convex planar set are homotopic rel endpoints through the set (affine homotopy).

theorem RS.exists_hasDerivAt_ball {f : ℂ → ℂ} {U : Set ℂ} (hf : AnalyticOnNhd ℂ f U) {c z₀ w : ℂ} {r : ℝ} (hb : Metric.ball c r ⊆ U) (_hz₀ : z₀ ∈ Metric.ball c r) : ∃ (g : ℂ → ℂ), g z₀ = w ∧ ∀ z ∈ Metric.ball c r, HasDerivAt g (f z) z

Primitive with prescribed value on a ball inside a domain of analyticity.

theorem RS.eventuallyEq_of_hasDerivAt_eq {f g d : ℂ → ℂ} {z₀ : ℂ} (hf : ∀ᶠ (z : ℂ) in nhds z₀, HasDerivAt f (d z) z) (hg : ∀ᶠ (z : ℂ) in nhds z₀, HasDerivAt g (d z) z) (h : f z₀ = g z₀) : f =ᶠ[nhds z₀] g

Two local primitives of the same function with equal value agree nearby.

An open convex planar set minus a countable set is path-connected

Adaptation of Set.Countable.isPathConnected_compl_of_one_lt_rank (Analysis/Normed/Module/Connected.lean), relativized to a convex open subset s instead of the whole space: the auxiliary point z t := c + t • y is kept inside a ball around the midpoint c that lies in s (openness), instead of ranging over all of t : ℝ.

theorem RS.Convex.isPathConnected_diff_countable {s : Set ℂ} (hs : Convex ℝ s) (ho : IsOpen s) (hne : s.Nonempty) {T : Set ℂ} (hT : T.Countable) : IsPathConnected (s \ T)

theorem RS.exists_homotopy_range_subset_of_convex {a b : ℂ} {s : Set ℂ} (hs : Convex ℝ s) {p q : Path a b} (hp : Set.range ⇑p ⊆ s) (hq : Set.range ⇑q ⊆ s) : ∃ (H : p.Homotopy q), ∀ (z : ↑unitInterval × ↑unitInterval), H z ∈ s

Any two paths with the same endpoints inside a convex planar set are homotopic rel endpoints, through the set.