Finite, ordered correction expansions for actual material powers.

def AVenhance.Infra.Section4.amnrMaterialErrorTerms : ℕ → List AmnrAdvectionTerm

The coarse term is separate; every listed term contains fast advection.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.Infra.Section4.amnrMaterialErrorTerms 0 = []

noncomputable def AVenhance.Infra.Section4.amnrMaterialErrorValue (b c : AmnrSpace → Homogenization.Vec 2) (f : AmnrSpace → ℝ) (n : ℕ) : AmnrSpace → ℝ

Sum of the advection terms representing the iterated material error.

Equations

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

theorem AVenhance.Infra.Section4.amnrMaterialErrorValue_contDiff {b c : AmnrSpace → Homogenization.Vec 2} {f : AmnrSpace → ℝ} (hb : ContDiff ℝ (↑⊤) b) (hc : ContDiff ℝ (↑⊤) c) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) : ContDiff ℝ (↑⊤) (amnrMaterialErrorValue b c f n)

theorem AVenhance.Infra.Section4.amnrMaterialErrorValue_succ {b c : AmnrSpace → Homogenization.Vec 2} {f : AmnrSpace → ℝ} (hb : ContDiff ℝ (↑⊤) b) (hc : ContDiff ℝ (↑⊤) c) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (z : AmnrSpace) : amnrMaterialErrorValue b c f (n + 1) z = amnrOp b none (amnrMaterialErrorValue b c f n) z + ∑ p : Fin 2, amnrAdvectionVelocity b c p z * amnrOp c (some p) (amnrWord c (List.replicate n none) f) z

Exact correction recurrence, with the pure coarse material term absent from the differentiated error list.

theorem AVenhance.Infra.Section4.amnr_material_power_expansion {b c : AmnrSpace → Homogenization.Vec 2} {f : AmnrSpace → ℝ} (hb : ContDiff ℝ (↑⊤) b) (hc : ContDiff ℝ (↑⊤) c) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) : amnrWord b (List.replicate n none) f = amnrWord c (List.replicate n none) f + amnrMaterialErrorValue b c f n

All actual material powers equal one pure coarse power plus the finite ordered correction. No higher derivative estimate is assumed.