Derivatives along coordinate slices of an L^p product

For a function g on the L^p product WithLp p (F × E), freezing one coordinate gives a function of the other coordinate alone. Its derivative is the derivative of g in the corresponding coordinate direction: along the line s ↦ (s, y) in the first factor 𝕜 it is fderiv 𝕜 g (t, y) (1, 0), and on the slice z ↦ (t, z) it is w ↦ fderiv 𝕜 g (t, y) (0, w). These are the chain rules used to compute integrals over a half-space {x | a < x.fst} one normal line or one tangential slice at a time, as in Fubini-type proofs of the divergence theorem. A map w ↦ (f w, g w) into the product is differentiated componentwise. The file also computes the derivative of the normal graph parametrization y ↦ (φ y, y): it is the graph x ↦ (A x, x) of the derivative A of φ, so its geometric Jacobian is the classical surface factor sqrt (1 + ‖A‖²).

Main declarations

• TauCeti.hasDerivAt_comp_toLp_fst: the derivative of g along a line in the first factor is its derivative in the direction (1, 0).
• TauCeti.fderiv_comp_toLp_snd: the derivative of g on a slice of the second factor is its derivative in the direction (0, w).
• TauCeti.fderiv_toLp_prodMk_apply: the derivative of w ↦ (f w, g w) is v ↦ (df v, dg v).
• TauCeti.norm_fderiv_le_norm_fderiv_toLp_prodMk_left, TauCeti.norm_fderiv_le_norm_fderiv_toLp_prodMk_right, TauCeti.norm_fderiv_toLp_prodMk_apply_sq: the derivative of w ↦ (f w, g w) dominates those of f and g, and in the Euclidean product its value on v has squared length ‖df v‖² + ‖dg v‖².
• HasFDerivAt.normalGraphEmbedding: the derivative of a graph parametrization is the graph of the derivative.
• DifferentiableAt.fderiv_normalGraphEmbedding: the Fréchet derivative of a graph parametrization at a differentiability point.
• DifferentiableAt.injective_fderiv_normalGraphEmbedding: that derivative is injective.
• DifferentiableAt.range_fderiv_normalGraphEmbedding: the range of that derivative is the linear tangent graph.
• DifferentiableAt.normDet_fderiv_normalGraphEmbedding: the geometric Jacobian of a graph parametrization is sqrt (1 + ‖Dφ‖²).

theorem TauCeti.hasDerivAt_comp_toLp_fst {𝕜 : Type u_1} {E : Type u_2} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {p : ENNReal} [Fact (1 ≤ p)] {g : WithLp p (𝕜 × E) → G} {t : 𝕜} {y : E} (hg : DifferentiableAt 𝕜 g (WithLp.toLp p (t, y))) : HasDerivAt (fun (s : 𝕜) => g (WithLp.toLp p (s, y))) ((fderiv 𝕜 g (WithLp.toLp p (t, y))) (WithLp.toLp p (1, 0))) t

Along the line s ↦ (s, y) in the first factor of WithLp p (𝕜 × E), the derivative of a function differentiable at (t, y) is its derivative in the direction (1, 0).

theorem TauCeti.fderiv_comp_toLp_snd {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {p : ENNReal} [Fact (1 ≤ p)] {g : WithLp p (F × E) → G} {t : F} {y : E} (hg : DifferentiableAt 𝕜 g (WithLp.toLp p (t, y))) (w : E) : (fderiv 𝕜 (fun (z : E) => g (WithLp.toLp p (t, z))) y) w = (fderiv 𝕜 g (WithLp.toLp p (t, y))) (WithLp.toLp p (0, w))

On the slice z ↦ (t, z) of the second factor of WithLp p (F × E), the derivative of a function differentiable at (t, y), applied to a direction w of E, is its derivative in the direction (0, w).

theorem TauCeti.fderiv_toLp_prodMk_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {p : ENNReal} [Fact (1 ≤ p)] {f : G → F} {g : G → E} {y : G} (hf : DifferentiableAt 𝕜 f y) (hg : DifferentiableAt 𝕜 g y) (v : G) : (fderiv 𝕜 (fun (w : G) => WithLp.toLp p (f w, g w)) y) v = WithLp.toLp p ((fderiv 𝕜 f y) v, (fderiv 𝕜 g y) v)

The derivative of a map w ↦ (f w, g w) into WithLp p (F × E), applied to a direction v, is (df v, dg v).

theorem TauCeti.norm_fderiv_le_norm_fderiv_toLp_prodMk_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {p : ENNReal} [Fact (1 ≤ p)] {f : G → F} {g : G → E} {y : G} (hg : DifferentiableAt 𝕜 g y) : ‖fderiv 𝕜 f y‖ ≤ ‖fderiv 𝕜 (fun (w : G) => WithLp.toLp p (f w, g w)) y‖

The derivative of a map w ↦ (f w, g w) into the L^p product dominates the derivative of f.

theorem TauCeti.norm_fderiv_le_norm_fderiv_toLp_prodMk_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {p : ENNReal} [Fact (1 ≤ p)] {f : G → F} {g : G → E} {y : G} (hf : DifferentiableAt 𝕜 f y) : ‖fderiv 𝕜 g y‖ ≤ ‖fderiv 𝕜 (fun (w : G) => WithLp.toLp p (f w, g w)) y‖

The derivative of a map w ↦ (f w, g w) into the L^p product dominates the derivative of g.

theorem TauCeti.norm_fderiv_toLp_prodMk_apply_sq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : G → F} {g : G → E} {y : G} (hf : DifferentiableAt 𝕜 f y) (hg : DifferentiableAt 𝕜 g y) (v : G) : ‖(fderiv 𝕜 (fun (w : G) => WithLp.toLp 2 (f w, g w)) y) v‖ ^ 2 = ‖(fderiv 𝕜 f y) v‖ ^ 2 + ‖(fderiv 𝕜 g y) v‖ ^ 2

In the Euclidean product, the derivative of a map w ↦ (f w, g w) in the direction v has squared length ‖df v‖² + ‖dg v‖².

theorem HasFDerivAt.normalGraphEmbedding {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] {φ : V → ℝ} {φ' : V →L[ℝ] ℝ} {x : V} (hφ : HasFDerivAt φ φ' x) : HasFDerivAt (TauCeti.normalGraphEmbedding φ) φ'.normalGraphL x

The derivative of a graph parametrization is the graph of the derivative.

theorem DifferentiableAt.fderiv_normalGraphEmbedding {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] {φ : V → ℝ} {x : V} (hφ : DifferentiableAt ℝ φ x) : fderiv ℝ (TauCeti.normalGraphEmbedding φ) x = (fderiv ℝ φ x).normalGraphL

At a differentiability point, the Fréchet derivative of a graph parametrization is the continuous linear graph of the derivative.

theorem DifferentiableAt.injective_fderiv_normalGraphEmbedding {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] {φ : V → ℝ} {x : V} (hφ : DifferentiableAt ℝ φ x) : Function.Injective ⇑(fderiv ℝ (TauCeti.normalGraphEmbedding φ) x)

At a differentiability point, the Fréchet derivative of a graph parametrization is injective.

theorem DifferentiableAt.range_fderiv_normalGraphEmbedding {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] {φ : V → ℝ} {x : V} (hφ : DifferentiableAt ℝ φ x) : ↑(↑(fderiv ℝ (TauCeti.normalGraphEmbedding φ) x)).range = {z : WithLp 2 (ℝ × V) | z.fst = (fderiv ℝ φ x) z.snd}

At a differentiability point of φ, the range of the derivative of the normal graph parametrization is the linear graph of fderiv ℝ φ x. This is the tangent plane to a C¹ normal graph at the corresponding point.

theorem DifferentiableAt.normDet_fderiv_normalGraphEmbedding {U : Type u_6} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] {φ : U → ℝ} {x : U} (hφ : DifferentiableAt ℝ φ x) : (↑(fderiv ℝ (TauCeti.normalGraphEmbedding φ) x)).normDet = √(1 + ‖fderiv ℝ φ x‖ ^ 2)

At a differentiability point, the geometric Jacobian of a normal graph parametrization is the classical surface factor sqrt (1 + ‖Dφ‖²).