Mixed Cauchy coefficients

Higher Cauchy kernels on polydiscs with separate radii. Differentiating the evaluation point raises the corresponding kernel exponent; the integration contour remains fixed. This identifies every mixed derivative with the multi-index factorial times its Cauchy coefficient, proves independence from the contour radii, and yields the sharp mixed-derivative Cauchy estimate. PolydiscTaylor uses these coefficients for convergent Taylor expansions.

noncomputable def CarlsonFunctions.SeveralComplexVariables.cauchyKernel {d : ℕ} (m : Fin d → ℕ) (w z : Fin d → ℂ) : ℂ

The higher Cauchy kernel of multi-index m.

Equations

• CarlsonFunctions.SeveralComplexVariables.cauchyKernel m w z = ∏ i : Fin d, (z i - w i)⁻¹ ^ (m i + 1)

noncomputable def CarlsonFunctions.SeveralComplexVariables.cauchyTransform {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : (Fin d → ℂ) → E) (c : Fin d → ℂ) (R : Fin d → ℝ) (m : Fin d → ℕ) (w : Fin d → ℂ) : E

The higher Cauchy transform with a fixed contour and variable evaluation point.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CarlsonFunctions.SeveralComplexVariables.polydiscCauchyCoeffWithRadii {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : (Fin d → ℂ) → E) (c : Fin d → ℂ) (R : Fin d → ℝ) (m : Fin d → ℕ) : E

Multi-index Cauchy coefficients for a polydisc with separate radii.

Equations

• CarlsonFunctions.SeveralComplexVariables.polydiscCauchyCoeffWithRadii f c R m = CarlsonFunctions.SeveralComplexVariables.cauchyTransform f c R m c

def CarlsonFunctions.SeveralComplexVariables.multiIndexList {d : ℕ} (m : Fin d → ℕ) : List (Fin d)

A canonical list containing coordinate i exactly m i times.

Equations

• CarlsonFunctions.SeveralComplexVariables.multiIndexList m = (List.ofFn fun (i : Fin d) => List.replicate (m i) i).flatten

@[simp]

theorem CarlsonFunctions.SeveralComplexVariables.count_multiIndexList {d : ℕ} (m : Fin d → ℕ) (i : Fin d) : List.count i (multiIndexList m) = m i

noncomputable def CarlsonFunctions.SeveralComplexVariables.multiIndexDeriv {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (m : Fin d → ℕ) (f : (Fin d → ℂ) → E) : (Fin d → ℂ) → E

The mixed coordinate derivative of multi-index m, in canonical coordinate order. For holomorphic maps, permutation invariance makes the choice of order immaterial.

Equations

• CarlsonFunctions.SeveralComplexVariables.multiIndexDeriv m f = CarlsonFunctions.SeveralComplexVariables.iteratedPartialDerivCarlson (CarlsonFunctions.SeveralComplexVariables.multiIndexList m) f

theorem CarlsonFunctions.SeveralComplexVariables.polydiscCauchyCoeffWithRadii_const {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : (Fin d → ℂ) → E) (c : Fin d → ℂ) (R : ℝ) (m : Fin d → ℕ) : polydiscCauchyCoeffWithRadii f c (fun (x : Fin d) => R) m = polydiscCauchyCoeff f c R m

Separate-radius coefficients recover the original equal-radius coefficients.

theorem CarlsonFunctions.SeveralComplexVariables.cauchyKernel_update {d : ℕ} (m : Fin d → ℕ) (w z : Fin d → ℂ) (i : Fin d) (v : ℂ) : cauchyKernel m (Function.update w i v) z = (∏ j ∈ Finset.univ.erase i, (z j - w j)⁻¹ ^ (m j + 1)) * (z i - v)⁻¹ ^ (m i + 1)

Isolate one factor of the Cauchy kernel.

theorem CarlsonFunctions.SeveralComplexVariables.hasDerivAt_cauchyKernel_update {d : ℕ} (m : Fin d → ℕ) (w z : Fin d → ℂ) (i : Fin d) (v : ℂ) (hz : z i - v ≠ 0) : HasDerivAt (fun (a : ℂ) => cauchyKernel m (Function.update w i a) z) ((↑(m i) + 1) * cauchyKernel (Function.update m i (m i + 1)) (Function.update w i v) z) v

Differentiating in coordinate i raises that kernel exponent by one.

theorem CarlsonFunctions.SeveralComplexVariables.norm_polydiscCauchyCoeffWithRadii_le {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : (Fin d → ℂ) → E} {c : Fin d → ℂ} {R : Fin d → ℝ} {M : ℝ} (hR : ∀ (i : Fin d), 0 < R i) (hM : ∀ z ∈ closedPolydiscWithRadii c R, ‖f z‖ ≤ M) (m : Fin d → ℕ) : ‖polydiscCauchyCoeffWithRadii f c R m‖ ≤ M * ∏ i : Fin d, (R i)⁻¹ ^ m i

Cauchy's multi-index coefficient estimate with one radius for each coordinate.

theorem CarlsonFunctions.SeveralComplexVariables.continuousOn_cauchyKernel_torus {d : ℕ} {c : Fin d → ℂ} {R : Fin d → ℝ} (hR : ∀ (i : Fin d), 0 < R i) (m : Fin d → ℕ) : ContinuousOn (fun (p : (Fin d → ℂ) × (Fin d → ℝ)) => cauchyKernel m p.1 (torusMap c R p.2)) (polydiscWithRadii c R ×ˢ Set.univ)

Higher Cauchy kernels are jointly continuous in the interior evaluation point and the contour parameter.

theorem CarlsonFunctions.SeveralComplexVariables.hasDerivAt_cauchyTransform_update {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : (Fin d → ℂ) → E} {c w : Fin d → ℂ} {R : Fin d → ℝ} (hR : ∀ (i : Fin d), 0 < R i) (hfc : ContinuousOn f (closedPolydiscWithRadii c R)) (hw : w ∈ polydiscWithRadii c R) (m : Fin d → ℕ) (i : Fin d) : HasDerivAt (fun (a : ℂ) => cauchyTransform f c R m (Function.update w i a)) ((↑(m i) + 1) • cauchyTransform f c R (Function.update m i (m i + 1)) w) (w i)

Coordinate differentiation under the fixed-contour higher Cauchy integral.

theorem CarlsonFunctions.SeveralComplexVariables.cauchyTransform_zero_eq {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : (Fin d → ℂ) → E} {c w : Fin d → ℂ} {R : Fin d → ℝ} (hR : ∀ (i : Fin d), 0 < R i) (hw : w ∈ polydiscWithRadii c R) (hfc : ContinuousOn f (closedPolydiscWithRadii c R)) (hfa : ∀ z ∈ closedPolydiscWithRadii c R, ∀ (i : Fin d), AnalyticAt ℂ (fun (v : ℂ) => f (Function.update z i v)) (z i)) : cauchyTransform f c R 0 w = f w

The zeroth Cauchy transform equals the original function in the open polydisc.

theorem CarlsonFunctions.SeveralComplexVariables.iteratedPartialDeriv_cauchyTransform_zero {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : (Fin d → ℂ) → E} {c w : Fin d → ℂ} {R : Fin d → ℝ} (hR : ∀ (i : Fin d), 0 < R i) (hfc : ContinuousOn f (closedPolydiscWithRadii c R)) (hw : w ∈ polydiscWithRadii c R) (is : List (Fin d)) : iteratedPartialDerivCarlson is (cauchyTransform f c R 0) w = (∏ j : Fin d, ↑(List.count j is).factorial) • cauchyTransform f c R (fun (j : Fin d) => List.count j is) w

Repeated coordinate differentiation of the zeroth Cauchy transform yields factorials times the corresponding higher Cauchy transform.

theorem CarlsonFunctions.SeveralComplexVariables.multiIndexDeriv_eq_factorial_smul_cauchyCoeff {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : (Fin d → ℂ) → E} {c : Fin d → ℂ} {R : Fin d → ℝ} (hR : ∀ (i : Fin d), 0 < R i) (hfc : ContinuousOn f (closedPolydiscWithRadii c R)) (hfa : ∀ z ∈ closedPolydiscWithRadii c R, ∀ (i : Fin d), AnalyticAt ℂ (fun (v : ℂ) => f (Function.update z i v)) (z i)) (m : Fin d → ℕ) : multiIndexDeriv m f c = (∏ i : Fin d, ↑(m i).factorial) • polydiscCauchyCoeffWithRadii f c R m

Mixed derivatives at the center are multi-index factorials times the Cauchy coefficients.

theorem CarlsonFunctions.SeveralComplexVariables.polydiscCauchyCoeffWithRadii_eq_multiIndexDeriv {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : (Fin d → ℂ) → E} {c : Fin d → ℂ} {R : Fin d → ℝ} (hR : ∀ (i : Fin d), 0 < R i) (hfc : ContinuousOn f (closedPolydiscWithRadii c R)) (hfa : ∀ z ∈ closedPolydiscWithRadii c R, ∀ (i : Fin d), AnalyticAt ℂ (fun (v : ℂ) => f (Function.update z i v)) (z i)) (m : Fin d → ℕ) : polydiscCauchyCoeffWithRadii f c R m = (∏ i : Fin d, ↑(m i).factorial)⁻¹ • multiIndexDeriv m f c

Cauchy coefficients are the mixed Taylor coefficients, independent of a contour choice.

theorem CarlsonFunctions.SeveralComplexVariables.iteratedPartialDeriv_eq_multiIndexDeriv {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {U : Set (Fin d → ℂ)} {f : (Fin d → ℂ) → E} (hf : AnalyticOnNhd ℂ f U) (hU : IsOpen U) {z : Fin d → ℂ} (hz : z ∈ U) {is : List (Fin d)} {m : Fin d → ℕ} (hm : ∀ (i : Fin d), List.count i is = m i) : iteratedPartialDerivCarlson is f z = multiIndexDeriv m f z

The mixed derivative can be computed in any order with the prescribed multiplicities.

theorem CarlsonFunctions.SeveralComplexVariables.polydiscCauchyCoeffWithRadii_eq_of_radii {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : (Fin d → ℂ) → E} {c : Fin d → ℂ} {R S : Fin d → ℝ} (hR : ∀ (i : Fin d), 0 < R i) (hS : ∀ (i : Fin d), 0 < S i) (hfcR : ContinuousOn f (closedPolydiscWithRadii c R)) (hfaR : ∀ z ∈ closedPolydiscWithRadii c R, ∀ (i : Fin d), AnalyticAt ℂ (fun (v : ℂ) => f (Function.update z i v)) (z i)) (hfcS : ContinuousOn f (closedPolydiscWithRadii c S)) (hfaS : ∀ z ∈ closedPolydiscWithRadii c S, ∀ (i : Fin d), AnalyticAt ℂ (fun (v : ℂ) => f (Function.update z i v)) (z i)) (m : Fin d → ℕ) : polydiscCauchyCoeffWithRadii f c R m = polydiscCauchyCoeffWithRadii f c S m

Changing the positive contour radii does not change the Cauchy coefficients.

theorem CarlsonFunctions.SeveralComplexVariables.norm_multiIndexDeriv_le {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : (Fin d → ℂ) → E} {c : Fin d → ℂ} {R : Fin d → ℝ} {M : ℝ} (hR : ∀ (i : Fin d), 0 < R i) (hfc : ContinuousOn f (closedPolydiscWithRadii c R)) (hfa : ∀ z ∈ closedPolydiscWithRadii c R, ∀ (i : Fin d), AnalyticAt ℂ (fun (v : ℂ) => f (Function.update z i v)) (z i)) (hM : ∀ z ∈ closedPolydiscWithRadii c R, ‖f z‖ ≤ M) (m : Fin d → ℕ) : ‖multiIndexDeriv m f c‖ ≤ (∏ i : Fin d, ↑(m i).factorial) * (M * ∏ i : Fin d, (R i)⁻¹ ^ m i)

Cauchy's estimate for every mixed derivative, with the usual multi-index factorial and a separate radius in each coordinate.