Coordinate derivatives of holomorphic functions

Coordinate differentiation is defined using one-variable slices, and identified with evaluation of the Fréchet derivative on a coordinate vector. Holomorphy of derivatives is inherited from Mathlib's general Fréchet derivative theorem.

noncomputable def CarlsonFunctions.SeveralComplexVariables.partialDerivCarlson {ι : Type u_1} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (i : ι) (f : (ι → ℂ) → F) (z : ι → ℂ) : F

Differentiate in coordinate i, holding all other coordinates fixed.

Equations

• CarlsonFunctions.SeveralComplexVariables.partialDerivCarlson i f z = deriv (fun (w : ℂ) => f (Function.update z i w)) (z i)

theorem CarlsonFunctions.SeveralComplexVariables.hasDerivAt_update_of_differentiableAt {ι : Type u_1} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] [Finite ι] {f : (ι → ℂ) → F} {z : ι → ℂ} (hf : DifferentiableAt ℂ f z) (i : ι) : HasDerivAt (fun (w : ℂ) => f (Function.update z i w)) ((fderiv ℂ f z) (Pi.single i 1)) (z i)

The derivative of a coordinate slice is the corresponding Fréchet derivative value.

theorem CarlsonFunctions.SeveralComplexVariables.partialDeriv_eq_fderiv {ι : Type u_1} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] [Finite ι] {f : (ι → ℂ) → F} {z : ι → ℂ} (hf : DifferentiableAt ℂ f z) (i : ι) : partialDerivCarlson i f z = (fderiv ℂ f z) (Pi.single i 1)

Coordinate derivatives are Fréchet derivatives evaluated on coordinate vectors.

theorem CarlsonFunctions.SeveralComplexVariables.partialDeriv_congr {ι : Type u_1} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] [Finite ι] {f g : (ι → ℂ) → F} {z : ι → ℂ} (hfg : f =ᶠ[nhds z] g) (i : ι) : partialDerivCarlson i f z = partialDerivCarlson i g z

A coordinate derivative only depends on the germ of the function.

theorem CarlsonFunctions.SeveralComplexVariables.fderiv_eq_sum_partialDeriv {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] {f : (ι → ℂ) → F} {z : ι → ℂ} (hf : DifferentiableAt ℂ f z) (v : ι → ℂ) : (fderiv ℂ f z) v = ∑ i : ι, v i • partialDerivCarlson i f z

The Fréchet derivative is recovered from the coordinate derivatives.

theorem CarlsonFunctions.SeveralComplexVariables.partialDeriv_sub {ι : Type u_1} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] [Finite ι] {f g : (ι → ℂ) → F} {z : ι → ℂ} (hf : DifferentiableAt ℂ f z) (hg : DifferentiableAt ℂ g z) (i : ι) : partialDerivCarlson i (f - g) z = partialDerivCarlson i f z - partialDerivCarlson i g z

Coordinate differentiation respects subtraction at differentiability points.

theorem AnalyticOnNhd.analyticAt_updateCarlson {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] {U : Set (ι → ℂ)} {f : (ι → ℂ) → F} (hf : AnalyticOnNhd ℂ f U) {z : ι → ℂ} (hz : z ∈ U) (i : ι) : AnalyticAt ℂ (fun (w : ℂ) => f (Function.update z i w)) (z i)

Holomorphy restricts to each coordinate slice.

theorem CarlsonFunctions.SeveralComplexVariables.partialDeriv_finset_sum {ι : Type u_1} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] [Finite ι] {α : Type u_3} {f : α → (ι → ℂ) → F} (t : Finset α) {z : ι → ℂ} (hf : ∀ a ∈ t, DifferentiableAt ℂ (f a) z) (i : ι) : partialDerivCarlson i (fun (w : ι → ℂ) => ∑ a ∈ t, f a w) z = ∑ a ∈ t, partialDerivCarlson i (f a) z

Coordinate differentiation commutes with a finite sum of differentiable functions.

theorem AnalyticOnNhd.partialDerivCarlson {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set (ι → ℂ)} {f : (ι → ℂ) → F} (hf : AnalyticOnNhd ℂ f U) (hU : IsOpen U) (i : ι) : AnalyticOnNhd ℂ (CarlsonFunctions.SeveralComplexVariables.partialDerivCarlson i f) U

Every coordinate derivative of an analytic function is analytic.

def CarlsonFunctions.SeveralComplexVariables.iteratedPartialDerivCarlson {ι : Type u_1} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] : List ι → ((ι → ℂ) → F) → (ι → ℂ) → F

Repeated coordinate differentiation, with the leftmost coordinate acting last.

Equations

• One or more equations did not get rendered due to their size.
• CarlsonFunctions.SeveralComplexVariables.iteratedPartialDerivCarlson [] x✝ = x✝

theorem CarlsonFunctions.SeveralComplexVariables.hasFDerivAt_partialDeriv {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set (ι → ℂ)} {f : (ι → ℂ) → F} (hf : AnalyticOnNhd ℂ f U) (hU : IsOpen U) {z : ι → ℂ} (hz : z ∈ U) (i : ι) : HasFDerivAt (partialDerivCarlson i f) ((ContinuousLinearMap.apply ℂ F) (Pi.single i 1) ∘SL fderiv ℂ (fderiv ℂ f) z) z

Differentiate a coordinate derivative by composing the second Fréchet derivative with evaluation on its coordinate vector.

theorem CarlsonFunctions.SeveralComplexVariables.partialDeriv_partialDeriv_comm {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set (ι → ℂ)} {f : (ι → ℂ) → F} (hf : AnalyticOnNhd ℂ f U) (hU : IsOpen U) {z : ι → ℂ} (hz : z ∈ U) (i j : ι) : partialDerivCarlson i (partialDerivCarlson j f) z = partialDerivCarlson j (partialDerivCarlson i f) z

Mixed coordinate derivatives commute for a holomorphic function.

theorem AnalyticOnNhd.iteratedPartialDerivCarlson {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set (ι → ℂ)} {f : (ι → ℂ) → F} (hf : AnalyticOnNhd ℂ f U) (hU : IsOpen U) (is : List ι) : AnalyticOnNhd ℂ (CarlsonFunctions.SeveralComplexVariables.iteratedPartialDerivCarlson is f) U

All iterated coordinate derivatives are holomorphic on the original open domain.

theorem CarlsonFunctions.SeveralComplexVariables.iteratedPartialDeriv_perm {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set (ι → ℂ)} {f : (ι → ℂ) → F} (hf : AnalyticOnNhd ℂ f U) (hU : IsOpen U) {is js : List ι} (h : is.Perm js) : Set.EqOn (iteratedPartialDerivCarlson is f) (iteratedPartialDerivCarlson js f) U

Iterated coordinate derivatives depend only on the multiplicity of each coordinate, not on their order in the differentiation list.

theorem CarlsonFunctions.SeveralComplexVariables.iteratedPartialDeriv_congrOn {ι : Type u_1} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] [Finite ι] {U : Set (ι → ℂ)} {f g : (ι → ℂ) → F} (hU : IsOpen U) (hfg : Set.EqOn f g U) (is : List ι) : Set.EqOn (iteratedPartialDerivCarlson is f) (iteratedPartialDerivCarlson is g) U

Iterated coordinate derivatives agree on an open set where the original functions agree.

theorem CarlsonFunctions.SeveralComplexVariables.iteratedPartialDeriv_finset_sum {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {α : Type u_3} {U : Set (ι → ℂ)} {f : α → (ι → ℂ) → F} (t : Finset α) (hf : ∀ a ∈ t, AnalyticOnNhd ℂ (f a) U) (hU : IsOpen U) (is : List ι) : Set.EqOn (iteratedPartialDerivCarlson is fun (z : ι → ℂ) => ∑ a ∈ t, f a z) (fun (z : ι → ℂ) => ∑ a ∈ t, iteratedPartialDerivCarlson is (f a) z) U

Mixed coordinate differentiation commutes with finite sums of holomorphic functions.

noncomputable def CarlsonFunctions.SeveralComplexVariables.complexJacobian {ι : Type u_1} {κ : Type u_3} (f : (ι → ℂ) → κ → ℂ) (z : ι → ℂ) : Matrix κ ι ℂ

The complex Jacobian in the standard coordinate bases.

Equations

• CarlsonFunctions.SeveralComplexVariables.complexJacobian f z j i = CarlsonFunctions.SeveralComplexVariables.partialDerivCarlson i (fun (w : ι → ℂ) => f w j) z

theorem CarlsonFunctions.SeveralComplexVariables.complexJacobian_apply {ι : Type u_1} [Finite ι] {κ : Type u_3} {f : (ι → ℂ) → κ → ℂ} {z : ι → ℂ} (hf : DifferentiableAt ℂ f z) (j : κ) (i : ι) : complexJacobian f z j i = (fderiv ℂ f z) (Pi.single i 1) j

Entries of the complex Jacobian are the coordinate entries of the Fréchet derivative.

theorem CarlsonFunctions.SeveralComplexVariables.partialDeriv_comp {ι : Type u_1} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] [Finite ι] {κ : Type u_3} [Fintype κ] {f : (ι → ℂ) → κ → ℂ} {g : (κ → ℂ) → F} {z : ι → ℂ} (hg : DifferentiableAt ℂ g (f z)) (hf : DifferentiableAt ℂ f z) (i : ι) : partialDerivCarlson i (g ∘ f) z = ∑ j : κ, complexJacobian f z j i • partialDerivCarlson j g (f z)

The coordinate chain rule, with an arbitrary complex normed outer target.

theorem CarlsonFunctions.SeveralComplexVariables.complexJacobian_comp {ι : Type u_1} [Finite ι] {κ : Type u_3} {ν : Type u_4} [Fintype κ] {f : (ι → ℂ) → κ → ℂ} {g : (κ → ℂ) → ν → ℂ} {z : ι → ℂ} (hg : DifferentiableAt ℂ g (f z)) (hf : DifferentiableAt ℂ f z) : complexJacobian (g ∘ f) z = complexJacobian g (f z) * complexJacobian f z

Jacobians compose by matrix multiplication.