Material differentiation of the spatial gradient of a smooth scalar field.

noncomputable def AVenhance.Infra.Section5.materialDerivative (T : ℝ → Homogenization.Vec 2 → ℝ) (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : ℝ → Homogenization.Vec 2 → ℝ

The material derivative represented by the spacetime Fréchet derivative.

Equations

• AVenhance.Infra.Section5.materialDerivative T b t x = (fderiv ℝ (Function.uncurry T) (t, x)) (1, b t x)

theorem AVenhance.Infra.Section5.fderiv_uncurry_scalar_spatial {T : ℝ → Homogenization.Vec 2 → ℝ} {t : ℝ} {x v : Homogenization.Vec 2} (hT : DifferentiableAt ℝ (Function.uncurry T) (t, x)) : (fderiv ℝ (Function.uncurry T) (t, x)) (0, v) = (fderiv ℝ (T t) x) v

Restricting a spacetime Fréchet derivative to a spatial direction agrees with differentiating the fixed-time slice.

theorem AVenhance.Infra.Section5.fderiv_uncurry_vector_spatial {B : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {t : ℝ} {x v : Homogenization.Vec 2} (hB : DifferentiableAt ℝ (Function.uncurry B) (t, x)) : (fderiv ℝ (Function.uncurry B) (t, x)) (0, v) = (fderiv ℝ (B t) x) v

Vector-valued version of fderiv_uncurry_scalar_spatial.

theorem AVenhance.Infra.Section5.materialDerivative_eq_advective_of_hasFDerivAt {T : ℝ → Homogenization.Vec 2 → ℝ} {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {t : ℝ} {x : Homogenization.Vec 2} {L : ℝ × Homogenization.Vec 2 →L[ℝ] ℝ} (hF : HasFDerivAt (Function.uncurry T) L (t, x)) : materialDerivative T b t x = deriv (fun (r : ℝ) => T r x) t + Homogenization.vecDot (b t x) (spaceGrad (T t) x)

The spacetime Fréchet representation is the ordinary material derivative when the scalar field is differentiable.

theorem AVenhance.Infra.Section5.deriv_comp_flow_eq_materialDerivative {T : ℝ → Homogenization.Vec 2 → ℝ} {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} {t s : ℝ} {y : Homogenization.Vec 2} (hX : IsFlow b X) (hF : HasFDerivAt (Function.uncurry T) (fderiv ℝ (Function.uncurry T) (t, X t y s)) (t, X t y s)) : deriv (fun (r : ℝ) => T r (X r y s)) t = materialDerivative T b t (X t y s)

The forward-flow form of transport calculus: differentiating a scalar field along a characteristic gives its material derivative.

theorem AVenhance.Infra.Section5.gradient_material_deriv_along_flow {T : ℝ → Homogenization.Vec 2 → ℝ} {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {t s : ℝ} {y : Homogenization.Vec 2} (i : Fin 2) (hT : ContDiffAt ℝ 2 (Function.uncurry T) (t, X t y s)) (hb : ContDiffAt ℝ 1 (Function.uncurry b) (t, X t y s)) (hgrad : (fun (r : ℝ) => spaceGrad (T r) (X r y s) i) =ᶠ[nhds t] fun (r : ℝ) => (fderiv ℝ (Function.uncurry T) (r, X r y s)) (0, Homogenization.basisVec i)) : HasDerivAt (fun (r : ℝ) => spaceGrad (T r) (X r y s) i) (spaceGrad (materialDerivative T b t) (X t y s) i - (fderiv ℝ (Function.uncurry T) (t, X t y s)) (0, (fderiv ℝ (Function.uncurry b) (t, X t y s)) (0, Homogenization.basisVec i))) t

Along a flow characteristic, the spatial gradient differentiates by the gradient of the material derivative and the usual velocity-gradient correction. The eventual equality hgrad is the local identification of a spatial slice derivative with the corresponding spacetime derivative.