Kmat jets from the actual one-step diffusivity size comparison.

noncomputable def AVenhance.Infra.Section4.amnrKmatStepConstant (β C₀ : ℝ) : ℝ

Step constant for mixed derivatives of the effective diffusivity matrix.

Equations

• AVenhance.Infra.Section4.amnrKmatStepConstant β C₀ = (1 + ↑(AVenhance.Nstar β) * 2 ^ AVenhance.Nstar β * C₀ ^ 3) * (160 / 9)

theorem AVenhance.Infra.Section4.amnr_Kmat_mixed_bound_of_step_size {β C₀ κm κprev : ℝ} (I : Ingredients β) (hz : I.Czeta ≤ C₀) (hh : I.Chat ≤ C₀) {m : ℕ} (hm : 1 ≤ m) (hκm : 0 < κm) (hκprev : 0 ≤ κprev) (hratio : epsilon β I.Λ m ^ 2 ≤ κm * tau β I.Λ m) (hsize : κm + a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κm ≤ 160 / 9 * κprev) (b : AmnrSpace → Homogenization.Vec 2) {S : ℝ} (hS : 0 ≤ S) (α : List (Fin 2)) (r : ℕ) (hbudget : α.length + 2 * r ≤ Nstar β) (i j : Fin 2) (z : AmnrSpace) : |amnrWord b (amnrMixedWord α r) (fun (y : AmnrSpace) => I.Kmat κm m y.1 i j) z| ≤ amnrKmatStepConstant β C₀ * κprev * amnrWeight S (tauP β I.Λ m)⁻¹ (amnrMixedWord α r)