Source-form hypotheses for the Section 2 material estimates.

The quantitative bounds here are stated as hypotheses; they are discharged for all material orders in MaterialGoalAllOrders.

noncomputable def AVenhance.Infra.Construction.materialIterateVector (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (ell : ℕ) (F : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2

Coordinatewise material iterates of a vector field, using the scalar material derivative already used for Jacobian entries.

Equations

• AVenhance.Infra.Construction.materialIterateVector b ell F t x i = AVenhance.constructionMaterialIterate b ell (fun (r : ℝ) (y : Homogenization.Vec 2) => F r y i) t x

noncomputable def AVenhance.Infra.Construction.materialIterateGradientEntry (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (ell : ℕ) (F : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (i j : Fin 2) : ℝ → Homogenization.Vec 2 → ℝ

One coordinate of the material derivative of the spatial gradient of a vector field.

Equations

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

structure AVenhance.Infra.Construction.PMaterialGoalSourceData {β : ℝ} (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (Cmat : ℝ) (m : ℕ) : Prop

p.material.goal in coordinate Fréchet-derivative form at one scale. The second line is stated on its defined range n ≥ 1, since the paper's display ∇^(n-1) is undefined at n = 0.

• constant_ge_one : 1 ≤ Cmat
• velocity_material_bound (n ell : ℕ) : 1 ≤ n + ell → n + ell ≤ Nstar β → ∀ (t : ℝ) (x : Homogenization.Vec 2) (J : Fin n → Fin 2), ‖(iteratedFDeriv ℝ n (materialIterateVector (streamVel (Φ m)) ell (streamVel (Φ m)) t) x) fun (k : Fin n) => Homogenization.basisVec (J k)‖ ≤ Cmat * epsilon β I.Λ m ^ (β - 1) * (epsilon β I.Λ m ^ (β - 2)) ^ ell * (epsilon β I.Λ m)⁻¹ ^ n
• gradient_material_bound (n ell : ℕ) : 1 ≤ n → n + ell ≤ Nstar β → ∀ (t : ℝ) (x : Homogenization.Vec 2) (i j : Fin 2) (J : Fin (n - 1) → Fin 2), ‖(iteratedFDeriv ℝ (n - 1) (materialIterateGradientEntry (streamVel (Φ m)) ell (streamVel (Φ m)) i j t) x) fun (k : Fin (n - 1)) => Homogenization.basisVec (J k)‖ ≤ Cmat * epsilon β I.Λ m ^ (β - 2) * (epsilon β I.Λ m ^ (β - 2)) ^ ell * (epsilon β I.Λ m)⁻¹ ^ (n - 1)

def AVenhance.Infra.Construction.iteratedTimeDerivative {α : Type} [NormedAddCommGroup α] [NormedSpace ℝ α] : ℕ → (ℝ → α) → ℝ → α

Iteration of an ordinary time derivative, for the displayed ∂ₜ^ell in c.material.goal.

Equations

• AVenhance.Infra.Construction.iteratedTimeDerivative 0 x✝ = x✝
• AVenhance.Infra.Construction.iteratedTimeDerivative ell.succ x✝ = fun (t : ℝ) => deriv (AVenhance.Infra.Construction.iteratedTimeDerivative ell x✝) t

noncomputable def AVenhance.Infra.Construction.inverseJacobianPulledBack {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (m : ℕ) (s r : ℝ) (x : Homogenization.Vec 2) : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2

The inverse Jacobian pulled back along the forward flow, as in the left-hand side of c.material.goal.

Equations

• AVenhance.Infra.Construction.inverseJacobianPulledBack hseq m s r x = AVenhance.constructionFlowInvJacobian hseq m r s (AVenhance.constructionFlow hseq m (s + r) x s)

structure AVenhance.Infra.Construction.CMaterialGoalSourceData {β : ℝ} (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hseq : IsStreamSeq I Φ) (Cmat : ℝ) (m : ℕ) : Prop

c.material.goal in componentwise form at one scale. Its quantitative input is recorded separately from PMaterialGoalSourceData until the space-time chain-rule argument from p.material.goal is formalized.

• pulled_inverse_jacobian_bound (s r : ℝ) : |r| ≤ 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) => iteratedTimeDerivative ell (fun (q : ℝ) => (inverseJacobianPulledBack hseq m s q y) (Homogenization.basisVec j) i) r) x) fun (k : Fin n) => Homogenization.basisVec (J k)‖ ≤ Cmat * (epsilon β I.Λ m)⁻¹ ^ n * (epsilon β I.Λ m ^ (β - 2)) ^ ell