Pulling material derivatives back along a flow turns them into ordinary time derivatives. This is the all-order chain-rule interface for material estimates.

def AVenhance.Infra.Construction.constructionJointScalar (F : ℝ → Homogenization.Vec 2 → ℝ) : ℝ × Homogenization.Vec 2 → ℝ

View a curried scalar field as a function on joint time-space.

Equations

• AVenhance.Infra.Construction.constructionJointScalar F p = F p.1 p.2

def AVenhance.Infra.Construction.constructionJointVector (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2

View a curried vector field as a function on joint time-space.

Equations

• AVenhance.Infra.Construction.constructionJointVector b p = b p.1 p.2

def AVenhance.Infra.Construction.MaterialPullback.constructionSpatialInputCLM : Homogenization.Vec 2 →L[ℝ] ℝ × Homogenization.Vec 2 × ℝ

Embed a spatial direction into the time-space-start-time domain, fixing both times.

Equations

• AVenhance.Infra.Construction.MaterialPullback.constructionSpatialInputCLM = ContinuousLinearMap.prod 0 ((ContinuousLinearMap.id ℝ (Homogenization.Vec 2)).prod 0)

theorem AVenhance.Infra.Construction.constructionMaterialDerivative_eq_joint_fderiv {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {F : ℝ → Homogenization.Vec 2 → ℝ} (hF : ContDiff ℝ (↑⊤) (constructionJointScalar F)) (t : ℝ) (x : Homogenization.Vec 2) : constructionMaterialDerivative b F t x = (fderiv ℝ (constructionJointScalar F) (t, x)) (1, b t x)

The material derivative is the joint derivative in the space-time direction (1,b).

theorem AVenhance.Infra.Construction.constructionMaterialDerivative_joint_contDiff {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {F : ℝ → Homogenization.Vec 2 → ℝ} (hb : ContDiff ℝ (↑⊤) (constructionJointVector b)) (hF : ContDiff ℝ (↑⊤) (constructionJointScalar F)) : ContDiff ℝ (↑⊤) (constructionJointScalar (constructionMaterialDerivative b F))

Smooth space-time data give a smooth material derivative.

theorem AVenhance.Infra.Construction.constructionMaterialIterate_joint_contDiff {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {F : ℝ → Homogenization.Vec 2 → ℝ} (hb : ContDiff ℝ (↑⊤) (constructionJointVector b)) (hF : ContDiff ℝ (↑⊤) (constructionJointScalar F)) (ell : ℕ) : ContDiff ℝ (↑⊤) (constructionJointScalar (constructionMaterialIterate b ell F))

Every material iterate stays smooth when the velocity and the original space-time profile are smooth.

theorem AVenhance.Infra.Construction.constructionComposedFlowJacobian_joint_contDiff {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} (m : ℕ) (s : ℝ) : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => constructionComposedFlowJacobian hseq m s p.1 p.2

The composed forward Jacobian is jointly smooth in the target time and spatial point. This is obtained by differentiating the joint smooth flow in its spatial variable and composing with the jointly smooth inverse flow.

theorem AVenhance.Infra.Construction.constructionMaterialDerivative_eq_deriv_pullback {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {F : ℝ → Homogenization.Vec 2 → ℝ} {X : ℝ → Homogenization.Vec 2} (hF : ContDiff ℝ (↑⊤) (constructionJointScalar F)) (t : ℝ) (hX : HasDerivAt X (b t (X t)) t) : constructionMaterialDerivative b F t (X t) = deriv (fun (r : ℝ) => F r (X r)) t

Along any differentiable characteristic of b, one material derivative is the ordinary derivative of the pulled-back profile.

theorem AVenhance.Infra.Construction.constructionMaterialIterate_eq_iteratedTimeDerivative_pullback {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {F : ℝ → Homogenization.Vec 2 → ℝ} {X : ℝ → Homogenization.Vec 2} (hb : ContDiff ℝ (↑⊤) (constructionJointVector b)) (hF : ContDiff ℝ (↑⊤) (constructionJointScalar F)) (hX : ∀ (t : ℝ), HasDerivAt X (b t (X t)) t) (ell : ℕ) (t : ℝ) : constructionMaterialIterate b ell F t (X t) = iteratedTimeDerivative ell (fun (r : ℝ) => F r (X r)) t

All iterated material derivatives pull back to ordinary time derivatives along the characteristic.

theorem AVenhance.Infra.Construction.constructionComposedFlowJacobian_materialIterate_eq_timeDerivative {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} (m : ℕ) (s : ℝ) (x : Homogenization.Vec 2) (i j : Fin 2) (ell : ℕ) (t : ℝ) (hF : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => (constructionComposedFlowJacobian hseq m s p.1 p.2) (Homogenization.basisVec j) i) : constructionMaterialIterate (fun (r : ℝ) (y : Homogenization.Vec 2) => streamVel (Φ m) (s + r) y) ell (fun (r : ℝ) (y : Homogenization.Vec 2) => (constructionComposedFlowJacobian hseq m s r y) (Homogenization.basisVec j) i) t (constructionFlow hseq m (s + t) x s) = iteratedTimeDerivative ell (fun (r : ℝ) => (constructionFlowJacobian hseq m r s x) (Homogenization.basisVec j) i) t

For the Section 2 flow, material iteration of the composed forward Jacobian becomes ordinary differentiation of the forward Jacobian along its starting point. The smoothness premise is qualitative joint smoothness of the composed Jacobian entry.

theorem AVenhance.Infra.Construction.constructionComposedFlowJacobian_materialIterate_eq_timeDerivative_of_flow {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} (m : ℕ) (s : ℝ) (x : Homogenization.Vec 2) (i j : Fin 2) (ell : ℕ) (t : ℝ) : constructionMaterialIterate (fun (r : ℝ) (y : Homogenization.Vec 2) => streamVel (Φ m) (s + r) y) ell (fun (r : ℝ) (y : Homogenization.Vec 2) => (constructionComposedFlowJacobian hseq m s r y) (Homogenization.basisVec j) i) t (constructionFlow hseq m (s + t) x s) = iteratedTimeDerivative ell (fun (r : ℝ) => (constructionFlowJacobian hseq m r s x) (Homogenization.basisVec j) i) t

The composed-flow Jacobian pullback identity with its qualitative smoothness premise supplied by joint smoothness of the construction flow.