Faà di Bruno transfer of material-Jacobian bounds through the flow map.

theorem AVenhance.Infra.Construction.MaterialFlowComposition.orderedPartial_eq_iteratedFDeriv_local {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} {f : Homogenization.Vec 2 → F} (hf : ContDiff ℝ (↑n) f) (x : Homogenization.Vec 2) (J : Fin n → Fin 2) : FaaDiBruno.orderedPartial n f x J = (iteratedFDeriv ℝ n f x) fun (k : Fin n) => Homogenization.basisVec (J k)

theorem AVenhance.Infra.Construction.MaterialFlowComposition.derivativeSup_le_of_uniform_coordinate_bound {n : ℕ} {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : Homogenization.Vec 2 → F) (hf : ContDiff ℝ (↑n) f) {B : ℝ} (hcoord : ∀ (x : Homogenization.Vec 2) (J : Fin n → Fin 2), ‖(iteratedFDeriv ℝ n f x) fun (k : Fin n) => Homogenization.basisVec (J k)‖ ≤ B) : FaaDiBruno.derivativeSup n f ≤ ENNReal.ofReal B

Uniform coordinate derivative bounds imply the corresponding Appendix B derivative seminorm bound.

theorem AVenhance.Infra.Construction.MaterialFlowComposition.snorm_le_of_uniform_coordinate_bound {n : ℕ} {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : Homogenization.Vec 2 → F) (hf : ContDiff ℝ (↑n) f) {R : ℝ} (hR : 0 < R) {B : ℝ} (hcoord : ∀ (x : Homogenization.Vec 2) (J : Fin n → Fin 2), ‖(iteratedFDeriv ℝ n f x) fun (k : Fin n) => Homogenization.basisVec (J k)‖ ≤ B) : FaaDiBruno.snorm f n R ≤ ENNReal.ofReal ((↑n + 1) ^ 2 / ↑n.factorial * R⁻¹ ^ n * B)

Coordinate derivatives bounded at the natural inverse-regularity radius give a uniform source seminorm, with the finite order loss exposed.

theorem AVenhance.Infra.Construction.MaterialFlowComposition.materialJacobianField_joint_smooth {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} (m : ℕ) (s : ℝ) (ell : ℕ) (i j : Fin 2) : ContDiff ℝ (↑⊤) (constructionJointScalar (constructionMaterialIterate (fun (q : ℝ) (y : Homogenization.Vec 2) => streamVel (Φ m) (s + q) y) ell fun (q : ℝ) (y : Homogenization.Vec 2) => (constructionComposedFlowJacobian hseq m s q y) (Homogenization.basisVec j) i))

theorem AVenhance.Infra.Construction.MaterialFlowComposition.materialJacobianField_snorm {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} {Cmat : ℝ} {m : ℕ} (hflow : FlowBoundsData I Φ hseq Cmat) (hm : 1 ≤ m) (s r : ℝ) (hr : |r| ≤ 2 ^ (-25) * (a β I.Λ m)⁻¹) (ell n : ℕ) (hnell : n + ell ≤ Nstar β) (i j : Fin 2) : FaaDiBruno.snorm (fun (y : Homogenization.Vec 2) => constructionMaterialIterate (fun (q : ℝ) (z : Homogenization.Vec 2) => streamVel (Φ m) (s + q) z) ell (fun (q : ℝ) (z : Homogenization.Vec 2) => (constructionComposedFlowJacobian hseq m s q z) (Homogenization.basisVec j) i) r y) n (epsilon β I.Λ m)⁻¹ ≤ ENNReal.ofReal (Cmat * (↑(Nstar β) + 1) ^ 2 * (epsilon β I.Λ m ^ (β - 2)) ^ ell)

A material Jacobian field has a uniform Appendix B seminorm after normalizing its source derivative scale.

theorem AVenhance.Infra.Construction.MaterialFlowComposition.constructionFlowSlice_smooth_local {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} (m : ℕ) (s r : ℝ) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => constructionFlow hseq m (s + r) x s

theorem AVenhance.Infra.Construction.MaterialFlowComposition.constructionFlowSlice_snorm {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} {Cmat : ℝ} {m : ℕ} (hflow : FlowBoundsData I Φ hseq Cmat) (hm : 1 ≤ m) (s r : ℝ) (hr : |r| ≤ 2 ^ (-25) * (a β I.Λ m)⁻¹) (n : ℕ) (hn : 1 ≤ n) (hnN : n ≤ Nstar β) : FaaDiBruno.snorm (fun (x : Homogenization.Vec 2) => constructionFlow hseq m (s + r) x s) n (2 ^ 14 * (epsilon β I.Λ m)⁻¹) ≤ ENNReal.ofReal (2 * (↑(Nstar β) + 1) ^ 2 * (2 ^ 14 * (epsilon β I.Λ m)⁻¹)⁻¹)

The forward flow map has the scale-normalized composition seminorm required by App. B.3, using the corrected c.flowreg derivative display.

noncomputable def AVenhance.Infra.Construction.materialFlowCompositionConstant (β Cmat : ℝ) : ℝ

Uniform constant for composing material derivatives with the flow.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Construction.materialJacobianPullback_spatial_bound {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} {Cmat : ℝ} {m : ℕ} (hflow : FlowBoundsData I Φ hseq Cmat) (hm : 1 ≤ m) (s r : ℝ) (hr : |r| ≤ 2 ^ (-25) * (a β I.Λ m)⁻¹) (ell n : ℕ) (hnell : 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 (q : ℝ) (z : Homogenization.Vec 2) => streamVel (Φ m) (s + q) z) ell (fun (q : ℝ) (z : Homogenization.Vec 2) => (constructionComposedFlowJacobian hseq m s q z) (Homogenization.basisVec j) i) r (constructionFlow hseq m (s + r) y s)) x) fun (k : Fin n) => Homogenization.basisVec (J k)‖ ≤ materialFlowCompositionConstant β Cmat * (epsilon β I.Λ m)⁻¹ ^ n * (epsilon β I.Λ m ^ (β - 2)) ^ ell

Spatial differentiation of the pulled back material Jacobian is controlled by App. B.3, the pointwise source material display, and the flow derivative display.

theorem AVenhance.Infra.Construction.MaterialFlowComposition.iteratedTimeDerivative_neg_local (ell : ℕ) (f : ℝ → ℝ) : (iteratedTimeDerivative ell fun (t : ℝ) => -f t) = fun (t : ℝ) => -iteratedTimeDerivative ell f t

theorem AVenhance.Infra.Construction.MaterialFlowComposition.norm_iteratedFDeriv_neg_local {g : Homogenization.Vec 2 → ℝ} (n : ℕ) (x : Homogenization.Vec 2) (J : Fin n → Homogenization.Vec 2) : ‖(iteratedFDeriv ℝ n (fun (y : Homogenization.Vec 2) => -g y) x) J‖ = ‖(iteratedFDeriv ℝ n g x) J‖

theorem AVenhance.Infra.Construction.c_material_goal_source_of_flow_bounds {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} {Cmat : ℝ} {m : ℕ} (hflow : FlowBoundsData I Φ hseq Cmat) (hm : 1 ≤ m) : CMaterialGoalSourceData I Φ hseq (materialFlowCompositionConstant β Cmat) m

c.material.goal, with the source c.material.DX.Xinv field read from FlowBoundsData. The two dimensional cofactor converts the inverse Jacobian to entries of the composed forward Jacobian, the material pullback identity turns those entries into time derivatives, and App. B.3 transfers their spatial estimates through the flow.