Finite smooth partitions of unity on planar open sets (Jacobian/Dbar/PlanarPoU.lean)

Unit: dbar-solvability (docs/design/dbar-solvability.md §4.4, §7.1). Mathlib-only, planar, project-independent (design D10).

Builds a finite smooth partition of unity on an open V ⊆ ℂ, subordinate to a given finite open cover W : Fin n → Set ℂ, from scratch: shrink the cover in the (normal, being metrizable) subtype ↥V via exists_subset_iUnion_closure_subset, push the shrunk sets back to ℂ (IsOpen.isOpenMap_subtype_val, closure_subtype), build one compactly-conditioned bump per piece via IsOpen.exists_contDiff_support_eq, and normalize by the (pointwise positive on V) sum. This is risk item R5 of the design; the from-scratch route (rather than reusing mathlib's SmoothPartitionOfUnity, which needs a closed base set and bundles into M → ℝ smooth maps, not the plain functions with prescribed exact support needed here) was confirmed as the right call by an upstream investigation of the manifold PartitionOfUnity API.

theorem RS.exists_smooth_partition_of_finite_cover {V : Set ℂ} (hV : IsOpen V) {n : ℕ} {W : Fin n → Set ℂ} (hWo : ∀ (i : Fin n), IsOpen (W i)) (_hWV : ∀ (i : Fin n), W i ⊆ V) (hcov : V ⊆ ⋃ (i : Fin n), W i) : ∃ (ψ : Fin n → ℂ → ℝ), (∀ (i : Fin n), ContDiffOn ℝ (↑⊤) (ψ i) V) ∧ (∀ (i : Fin n) (z : ℂ), 0 ≤ ψ i z) ∧ (∀ z ∈ V, ∑ i : Fin n, ψ i z = 1) ∧ (∀ (i : Fin n), Function.support (ψ i) ⊆ W i) ∧ ∀ (i : Fin n), ∀ z ∈ V, z ∉ W i → ∀ᶠ (w : ℂ) in nhds z, ψ i w = 0

A finite smooth partition of unity on an open planar set V, subordinate to a finite open cover W: each ψ i is smooth on V, nonnegative, supported in W i, summing to 1 on V, and eventually zero near any point of V outside W i.

theorem RS.contDiffOn_indicator_smul_of_eventually_zero {U W V : Set ℂ} (_hU : IsOpen U) (hW : IsOpen W) {ψ : ℂ → ℝ} {f : ℂ → ℂ} (hUV : U ⊆ V) (hψ : ContDiffOn ℝ (↑⊤) ψ V) (hf : ContDiffOn ℝ (↑⊤) f (U ∩ W)) (hvan : ∀ z ∈ U, z ∉ W → ∀ᶠ (w : ℂ) in nhds z, ψ w = 0) : ContDiffOn ℝ (↑⊤) (W.indicator fun (z : ℂ) => ψ z • f z) U

Extending a PoU-weighted term by zero outside its supporting open set stays smooth on U, provided ψ vanishes near any point of U outside W.