Dimensional invarance of fderiv

In this module we prove that the derivative is dimensionally correct. That is to say for a function f : M1 → M2 where M1 carrys dimensions d1 and M2 carrys dimension d2 such that f has the correct dimension, then fderiv ℝ f : M1 → M1 →L[ℝ] M2 has the correct dimensions.

To give an explicit example let us say M1 has dimension L𝓭 and M2 has dimension L𝓭 * L𝓭 and f : M1 → M2 : x ↦ x ^ 2, this is dimensionally correct. The fderiv of this fderiv ℝ f : M1 → M1 →L[ℝ] M2 takes x dx ↦ dx • (2 * x) which is still dimensionally correct. Here dx is the direction in which the derivative is taken.

theorem fderiv_apply_scaleUnit {M1 M2 : Type} [NormedAddCommGroup M1] [NormedSpace ℝ M1] [ContinuousConstSMul ℝ M1] [ModuleCarriesDimension M1] [NormedAddCommGroup M2] [NormedSpace ℝ M2] [SMulCommClass ℝ ℝ M2] [ContinuousConstSMul ℝ M2] [ModuleCarriesDimension M2] (u1 u2 : UnitChoices) (x dm : M1) (f : M1 → M2) (hf : IsDimensionallyCorrect f) (f_diff : Differentiable ℝ f) : (fderiv ℝ f (UnitDependent.scaleUnit u2 u1 x)) dm = (u2.dimScale u1) (CarriesDimension.d M2) • (u1.dimScale u2) (CarriesDimension.d M1) • (fderiv ℝ f x) dm

theorem fderiv_isDimensionallyCorrect {M1 M2 : Type} [NormedAddCommGroup M1] [NormedSpace ℝ M1] [ContinuousConstSMul ℝ M1] [ModuleCarriesDimension M1] [NormedAddCommGroup M2] [NormedSpace ℝ M2] [SMulCommClass ℝ ℝ M2] [ContinuousConstSMul ℝ M2] [ModuleCarriesDimension M2] (f : M1 → M2) (hf : IsDimensionallyCorrect f) (f_diff : Differentiable ℝ f) : IsDimensionallyCorrect (fderiv ℝ f)

If a function is dimensionally valid then so is it's derivative.

theorem fderiv_dimension_const_direction {M1 M2 : Type} [NormedAddCommGroup M1] [NormedSpace ℝ M1] [ContinuousConstSMul ℝ M1] [ModuleCarriesDimension M1] [NormedAddCommGroup M2] [NormedSpace ℝ M2] [SMulCommClass ℝ ℝ M2] [ContinuousConstSMul ℝ M2] [ModuleCarriesDimension M2] (dm : M1) (f : M1 → M2) (hf : IsDimensionallyCorrect f) (f_diff : Differentiable ℝ f) : IsDimensionallyCorrect fun (x : M1) (v : WithDim (CarriesDimension.d M2 * (CarriesDimension.d M1)⁻¹) M2) => (fderiv ℝ f x) dm = v.val

The expression fderiv ℝ f x dm = v.1 for a fixed dm and for v with dimension d M2 * (d M1)⁻¹ is dimensionally correct. This is the ordinary manifestation of dimensions of a derivative, usually dm is taken as e.g. 1.

This result also shows that dimensional correctness does depend on what quantities are condsidered dimensionful.