The material Jacobian field follows from the all-order velocity-gradient jets and the spatial flow displays.
def
AVenhance.Infra.Construction.MaterialJacobianFromP.materialTimeShift
(s : ℝ)
(z : Section4.AmnrSpace)
:
Translate the time coordinate while fixing the spatial coordinate.
Instances For
theorem
AVenhance.Infra.Construction.MaterialJacobianFromP.amnrOp_timeShift
{b : Section4.AmnrSpace → Homogenization.Vec 2}
{f : Section4.AmnrSpace → ℝ}
(s : ℝ)
(hf : ContDiff ℝ (↑⊤) f)
(d : Option (Fin 2))
(z : Section4.AmnrSpace)
:
Section4.amnrOp (fun (y : Section4.AmnrSpace) => b (materialTimeShift s y)) d
(fun (y : Section4.AmnrSpace) => f (materialTimeShift s y)) z = Section4.amnrOp b d f (materialTimeShift s z)
theorem
AVenhance.Infra.Construction.MaterialJacobianFromP.amnrWord_timeShift
{b : Section4.AmnrSpace → Homogenization.Vec 2}
{f : Section4.AmnrSpace → ℝ}
(s : ℝ)
(hb : ContDiff ℝ (↑⊤) b)
(hf : ContDiff ℝ (↑⊤) f)
(w : List (Option (Fin 2)))
:
(Section4.amnrWord (fun (y : Section4.AmnrSpace) => b (materialTimeShift s y)) w fun (y : Section4.AmnrSpace) =>
f (materialTimeShift s y)) = fun (z : Section4.AmnrSpace) => Section4.amnrWord b w f (materialTimeShift s z)
theorem
AVenhance.Infra.Construction.MaterialJacobianFromP.materialJacobianEntry_transport
{β : ℝ}
{I : Ingredients β}
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
{hseq : IsStreamSeq I Φ}
(m : ℕ)
(s : ℝ)
(i j : Fin 2)
(z : Section4.AmnrSpace)
:
Section4.amnrOp (fun (y : Section4.AmnrSpace) => streamVel (Φ m) (s + y.1) y.2) none
(fun (y : Section4.AmnrSpace) => (constructionComposedFlowJacobian hseq m s y.1 y.2) (Homogenization.basisVec j) i)
z = ∑ q : Fin 2,
(constructionComposedFlowJacobian hseq m s z.1 z.2) (Homogenization.basisVec j) q * Section4.amnrVelocityGradient (fun (y : Section4.AmnrSpace) => streamVel (Φ m) (s + y.1) y.2) i q z
theorem
AVenhance.Infra.Construction.MaterialJacobianFromP.materialPureWord_eq_iterate
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{F : ℝ → Homogenization.Vec 2 → ℝ}
(hb : ContDiff ℝ (↑⊤) (constructionJointVector b))
(hF : ContDiff ℝ (↑⊤) (constructionJointScalar F))
(ell : ℕ)
:
theorem
AVenhance.Infra.Construction.MaterialJacobianFromP.amnrVelocityGradient_timeShift
{b : Section4.AmnrSpace → Homogenization.Vec 2}
(hb : ContDiff ℝ (↑⊤) b)
(s : ℝ)
(i p : Fin 2)
(z : Section4.AmnrSpace)
:
Section4.amnrVelocityGradient (fun (y : Section4.AmnrSpace) => b (materialTimeShift s y)) i p z = Section4.amnrVelocityGradient b i p (materialTimeShift s z)
Constant controlling the material derivatives of the Section 2 Jacobian.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AVenhance.Infra.Construction.section2MaterialJacobianConstant_ge_one
{β K : ℝ}
(hK : 1 ≤ K)
:
theorem
AVenhance.Infra.Construction.section2_material_jacobian_of_material_levels
{β : ℝ}
{I : Ingredients β}
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
{hseq : IsStreamSeq I Φ}
{K : ℝ}
(hK : 1 ≤ K)
(hlevels : MaterialAuxJetLevels I Φ (2 * Nstar β + 1) K (Nstar β))
{m : ℕ}
(hflow : Section2SpatialFlowData I Φ hseq m)
(s t : ℝ)
:
|t| ≤ 2 ^ (-25) * (a β I.Λ m)⁻¹ →
∀ (n ell : ℕ),
n + ell ≤ Nstar β →
∀ (i j : Fin 2) (x : Homogenization.Vec 2) (J : Fin n → Fin 2),
‖(iteratedFDeriv ℝ n
(fun (y : Homogenization.Vec 2) =>
constructionMaterialIterate (fun (r : ℝ) (z : Homogenization.Vec 2) => streamVel (Φ m) (s + r) z) ell
(fun (r : ℝ) (z : Homogenization.Vec 2) =>
(constructionComposedFlowJacobian hseq m s r z) (Homogenization.basisVec j) i)
t y)
x)
fun (k : Fin n) => Homogenization.basisVec (J k)‖ ≤ section2MaterialJacobianConstant β K * (epsilon β I.Λ m)⁻¹ ^ n * (epsilon β I.Λ m ^ (β - 2)) ^ ell
The material-Jacobian display follows from the all-order weighted material gradient jets and the source spatial flow displays.