Derivative bookkeeping for the L²_x → L¹ analyticity bridge

Identities relating iterated Fréchet derivatives of the coordinate derivative ∂_v f, and of the L²-test functions y ↦ Dⁿf(y)(w), to higher-order iterated derivatives of f. The extra directions are always placed outermost (Fin.cons) or innermost (Fin.snoc), so no symmetry of mixed partials is needed.

theorem AVenhance.Infra.Section5.AnalyticBridge.iteratedFDeriv_fderiv_apply_snoc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (v : E) (w : Fin n → E) (x : E) : (iteratedFDeriv ℝ n (fun (y : E) => (fderiv ℝ f y) v) x) w = (iteratedFDeriv ℝ (n + 1) f x) (Fin.snoc w v)

The n-th derivative of the directional derivative ∂_v f is the (n+1)-st derivative of f with v appended as the innermost direction.

theorem AVenhance.Infra.Section5.AnalyticBridge.fderiv_iteratedFDeriv_apply_cons {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} (hf : ContDiff ℝ (↑⊤) f) (m : ℕ) (v : E) (w : Fin m → E) (x : E) : (fderiv ℝ (fun (y : E) => (iteratedFDeriv ℝ m f y) w) x) v = (iteratedFDeriv ℝ (m + 1) f x) (Fin.cons v w)

The derivative of y ↦ Dᵐf(y)(w) in direction v puts v outermost.

theorem AVenhance.Infra.Section5.AnalyticBridge.contDiff_iteratedFDeriv_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} (hf : ContDiff ℝ (↑⊤) f) (m : ℕ) (w : Fin m → E) : ContDiff ℝ ↑⊤ fun (y : E) => (iteratedFDeriv ℝ m f y) w

The L²-test functions y ↦ Dᵐf(y)(w) are smooth.

theorem AVenhance.Infra.Section5.AnalyticBridge.iteratedFDeriv_two_iteratedFDeriv_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} (hf : ContDiff ℝ (↑⊤) f) (m : ℕ) (w : Fin m → E) (v x : E) : ((iteratedFDeriv ℝ 2 (fun (y : E) => (iteratedFDeriv ℝ m f y) w) x) fun (x : Fin 2) => v) = (iteratedFDeriv ℝ (m + 2) f x) (Fin.cons v (Fin.cons v w))

Two derivatives of y ↦ Dᵐf(y)(w) in the same direction v.

theorem AVenhance.Infra.Section5.AnalyticBridge.isZ2Periodic_iteratedFDeriv_apply {f : Homogenization.Vec 2 → ℝ} (hp : IsZ2Periodic f) (m : ℕ) (w : Fin m → Homogenization.Vec 2) : IsZ2Periodic fun (y : Homogenization.Vec 2) => (iteratedFDeriv ℝ m f y) w

Periodicity passes to the L²-test functions y ↦ Dᵐf(y)(w).

theorem AVenhance.Infra.Section5.AnalyticBridge.orderedPartial_eq_iteratedFDeriv {d : ℕ} {f : Homogenization.Vec d → ℝ} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : Homogenization.Vec d) (I : Fin n → Fin d) : FaaDiBruno.orderedPartial n f x I = (iteratedFDeriv ℝ n f x) fun (j : Fin n) => Homogenization.basisVec (I j)

The coordinate-list partial orderedPartial is the iterated Fréchet derivative evaluated on coordinate basis vectors of Vec d.

theorem AVenhance.Infra.Section5.AnalyticBridge.coordDeriv_ofReal_apply {d : ℕ} {f : Homogenization.Vec d → ℝ} {x : Homogenization.Vec d} (hf : DifferentiableAt ℝ f x) (i : Fin d) : Torus.coordDeriv i (fun (y : Homogenization.Vec d) => ↑(f y)) x = ↑((fderiv ℝ f x) (Homogenization.basisVec i))

The complexified coordinate derivative of a real smooth function.

theorem AVenhance.Infra.Section5.AnalyticBridge.coordDerivIter_ofReal {d : ℕ} {F : Homogenization.Vec d → ℝ} (hF : ContDiff ℝ (↑⊤) F) (i : Fin d) (n : ℕ) : (Ergodic.coordDerivIter i n fun (x : Homogenization.Vec d) => ↑(F x)) = fun (x : Homogenization.Vec d) => ↑((iteratedFDeriv ℝ n F x) fun (x : Fin n) => Homogenization.basisVec i)

∂_i^n of the complexification is the complexification of the iterated derivative on the constant coordinate list.

theorem AVenhance.Infra.Section5.AnalyticBridge.norm_coordDerivIter_ofReal {d : ℕ} {F : Homogenization.Vec d → ℝ} (hF : ContDiff ℝ (↑⊤) F) (i : Fin d) (n : ℕ) (x : Homogenization.Vec d) : ‖Ergodic.coordDerivIter i n (fun (x : Homogenization.Vec d) => ↑(F x)) x‖ = ‖FaaDiBruno.orderedPartial n F x fun (x : Fin n) => i‖

Norm of the complexified iterated coordinate derivative.