Reindexing finite complex coordinate spaces

Coordinate derivatives commute with renaming coordinates. The polydisc Cauchy formula is transported along any enumeration of a finite index type; its value is independent of that enumeration whenever the Cauchy hypotheses hold.

theorem CarlsonFunctions.SeveralComplexVariables.partialDeriv_reindex {ι : Type u_1} {κ : Type u_2} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℂ F] (e : κ ≃ ι) (f : (κ → ℂ) → F) (z : ι → ℂ) (i : ι) : partialDerivCarlson i (fun (w : ι → ℂ) => f (w ∘ ⇑e)) z = partialDerivCarlson (e.symm i) f (z ∘ ⇑e)

Renaming coordinates renames a coordinate derivative by the inverse equivalence.

theorem CarlsonFunctions.SeveralComplexVariables.iteratedPartialDeriv_reindex {ι : Type u_1} {κ : Type u_2} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℂ F] (e : κ ≃ ι) (f : (κ → ℂ) → F) (is : List ι) (z : ι → ℂ) : iteratedPartialDerivCarlson is (fun (w : ι → ℂ) => f (w ∘ ⇑e)) z = iteratedPartialDerivCarlson (List.map (⇑e.symm) is) f (z ∘ ⇑e)

All iterated coordinate derivatives are natural under coordinate reindexing.

theorem CarlsonFunctions.SeveralComplexVariables.polydisc_cauchy_reindex {ι : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {n : ℕ} (e : Fin n ≃ ι) {f : (ι → ℂ) → F} {c w : ι → ℂ} {R : ι → ℝ} (hR : ∀ (i : ι), 0 < R i) (hw : ∀ (i : ι), ‖w i - c i‖ < R i) (hfc : ContinuousOn f (closedPolydiscWithRadii c R)) (hfa : ∀ z ∈ closedPolydiscWithRadii c R, ∀ (i : ι), AnalyticAt ℂ (fun (x : ℂ) => f (Function.update z i x)) (z i)) : (((2 * ↑Real.pi * Complex.I) ^ n)⁻¹ • ∯ (z : Fin n → ℂ) in T(c ∘ ⇑e, R ∘ ⇑e), (∏ i : Fin n, (z i - w (e i))⁻¹) • f (z ∘ ⇑e.symm)) = f w

Cauchy's polydisc formula for an arbitrary finite index type, integrated using any enumeration by Fin n. No nonemptiness or positive-dimension hypothesis is needed.