Imports
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Physlib.Units.WithDim.Basic
public import Mathlib.Analysis.Calculus.FDeriv.EquivDimensional invariance 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 carries dimensions d1 and M2 carries
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.
@[expose] public sectionM1:TypeM2:Typeinst✝⁸:NormedAddCommGroup M1inst✝⁷:NormedSpace ℝ M1inst✝⁶:ContinuousConstSMul ℝ M1inst✝⁵:HasDim M1inst✝⁴:NormedAddCommGroup M2inst✝³:NormedSpace ℝ M2inst✝²:SMulCommClass ℝ ℝ M2inst✝¹:ContinuousConstSMul ℝ M2inst✝:HasDim M2u1:UnitChoicesu2:UnitChoicesx:M1dm:M1f:M1 → M2hf:IsDimensionallyCorrect ff_diff:Differentiable ℝ f⊢ (↑((u2.dimScale u1) (dim M2)) •
↑((u1.dimScale u2) (dim M1)) • fderiv ℝ f (↑((u1.dimScale u2) (dim M1)) • ↑((u2.dimScale u1) (dim M1)) • x))
dm =
(u2.dimScale u1) (dim M2) • (u1.dimScale u2) (dim M1) • (fderiv ℝ f x) dm
M1:TypeM2:Typeinst✝⁸:NormedAddCommGroup M1inst✝⁷:NormedSpace ℝ M1inst✝⁶:ContinuousConstSMul ℝ M1inst✝⁵:HasDim M1inst✝⁴:NormedAddCommGroup M2inst✝³:NormedSpace ℝ M2inst✝²:SMulCommClass ℝ ℝ M2inst✝¹:ContinuousConstSMul ℝ M2inst✝:HasDim M2u1:UnitChoicesu2:UnitChoicesx:M1dm:M1f:M1 → M2hf:IsDimensionallyCorrect ff_diff:Differentiable ℝ f⊢ (↑((u2.dimScale u1) (dim M2)) * ↑((u1.dimScale u2) (dim M1))) • (fderiv ℝ f x) dm =
((u2.dimScale u1) (dim M2) * (u1.dimScale u2) (dim M1)) • (fderiv ℝ f x) dm
All goals completed! 🐙
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 considered dimensionful.
lemma fderiv_dimension_const_direction (dm : M1) (f : M1 → M2) (hf : IsDimensionallyCorrect f)
(f_diff : Differentiable ℝ f) :
IsDimensionallyCorrect (fun x (v : WithDim (dim M2 * (dim M1)⁻¹) M2) =>
fderiv ℝ f x dm = v.1) := M1:TypeM2:Typeinst✝⁸:NormedAddCommGroup M1inst✝⁷:NormedSpace ℝ M1inst✝⁶:ContinuousConstSMul ℝ M1inst✝⁵:HasDim M1inst✝⁴:NormedAddCommGroup M2inst✝³:NormedSpace ℝ M2inst✝²:SMulCommClass ℝ ℝ M2inst✝¹:ContinuousConstSMul ℝ M2inst✝:HasDim M2dm:M1f:M1 → M2hf:IsDimensionallyCorrect ff_diff:Differentiable ℝ f⊢ IsDimensionallyCorrect fun x v => (fderiv ℝ f x) dm = v.val
All goals completed! 🐙