Explicit finite monomials for noncommuting material-power corrections.

@[reducible, inline]

abbrev AVenhance.Infra.Section4.AmnrAdvectionFactor : Type

One actual velocity-component jet, including its precise operator word.

Equations

• AVenhance.Infra.Section4.AmnrAdvectionFactor = (Fin 2 × List (Option (Fin 2)))

structure AVenhance.Infra.Section4.AmnrAdvectionTerm : Type

A monomial in fast-velocity jets, ending in one actual scalar jet.

• factors : List AmnrAdvectionFactor

  Velocity factors, each carrying its component and derivative word.

• scalarWord : List (Option (Fin 2))

  Derivative word applied to the scalar factor of the advection term.

def AVenhance.Infra.Section4.amnrAdvectionProduct (c : AmnrSpace → Homogenization.Vec 2) (v : Fin 2 → AmnrSpace → ℝ) : List AmnrAdvectionFactor → AmnrSpace → ℝ

The actual product of the prescribed velocity jets.

Equations

• AVenhance.Infra.Section4.amnrAdvectionProduct c v [] = 1
• AVenhance.Infra.Section4.amnrAdvectionProduct c v (a :: A) = AVenhance.Infra.Section4.amnrWord c a.2 (v a.1) * AVenhance.Infra.Section4.amnrAdvectionProduct c v A

noncomputable def AVenhance.Infra.Section4.amnrAdvectionTermValue (c : AmnrSpace → Homogenization.Vec 2) (v : Fin 2 → AmnrSpace → ℝ) (f : AmnrSpace → ℝ) (t : AmnrAdvectionTerm) : AmnrSpace → ℝ

Actual evaluation of the finite correction monomial.

Equations

• AVenhance.Infra.Section4.amnrAdvectionTermValue c v f t = AVenhance.Infra.Section4.amnrAdvectionProduct c v t.factors * AVenhance.Infra.Section4.amnrWord c t.scalarWord f

def AVenhance.Infra.Section4.amnrAdvectionTermPrepend (a : AmnrAdvectionFactor) (t : AmnrAdvectionTerm) : AmnrAdvectionTerm

Prepending a genuine velocity factor.

Equations

• AVenhance.Infra.Section4.amnrAdvectionTermPrepend a t = { factors := a :: t.factors, scalarWord := t.scalarWord }

def AVenhance.Infra.Section4.amnrAdvectionDerivativeTerms (d : Option (Fin 2)) : List AmnrAdvectionFactor → List (Option (Fin 2)) → List AmnrAdvectionTerm

Exact Leibniz terms for one spatial or coarse-material differentiation. The operator order is retained in every factor and in the final scalar jet.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.Infra.Section4.amnrAdvectionDerivativeTerms d [] x✝ = [{ factors := [], scalarWord := d :: x✝ }]

theorem AVenhance.Infra.Section4.amnrAdvectionProduct_contDiff {c : AmnrSpace → Homogenization.Vec 2} {v : Fin 2 → AmnrSpace → ℝ} (hc : ContDiff ℝ (↑⊤) c) (hv : ∀ (p : Fin 2), ContDiff ℝ (↑⊤) (v p)) (A : List AmnrAdvectionFactor) : ContDiff ℝ (↑⊤) (amnrAdvectionProduct c v A)

Every actual factor product is smooth from its primitive fields.

theorem AVenhance.Infra.Section4.amnrAdvectionTermValue_contDiff {c : AmnrSpace → Homogenization.Vec 2} {v : Fin 2 → AmnrSpace → ℝ} {f : AmnrSpace → ℝ} (hc : ContDiff ℝ (↑⊤) c) (hv : ∀ (p : Fin 2), ContDiff ℝ (↑⊤) (v p)) (hf : ContDiff ℝ (↑⊤) f) (t : AmnrAdvectionTerm) : ContDiff ℝ (↑⊤) (amnrAdvectionTermValue c v f t)

theorem AVenhance.Infra.Section4.amnrAdvectionTermValue_prepend (c : AmnrSpace → Homogenization.Vec 2) (v : Fin 2 → AmnrSpace → ℝ) (f : AmnrSpace → ℝ) (a : AmnrAdvectionFactor) (t : AmnrAdvectionTerm) (z : AmnrSpace) : amnrAdvectionTermValue c v f (amnrAdvectionTermPrepend a t) z = amnrWord c a.2 (v a.1) z * amnrAdvectionTermValue c v f t z

Prepending a factor is ordinary multiplication of actual monomial values.

theorem AVenhance.Infra.Section4.amnrAdvectionTermValue_sum_prepend (c : AmnrSpace → Homogenization.Vec 2) (v : Fin 2 → AmnrSpace → ℝ) (f : AmnrSpace → ℝ) (a : AmnrAdvectionFactor) (T : List AmnrAdvectionTerm) (z : AmnrSpace) : (List.map (fun (t : AmnrAdvectionTerm) => amnrAdvectionTermValue c v f t z) (List.map (amnrAdvectionTermPrepend a) T)).sum = amnrWord c a.2 (v a.1) z * (List.map (fun (t : AmnrAdvectionTerm) => amnrAdvectionTermValue c v f t z) T).sum

A factor distributes over the exact finite sum of correction monomials.

theorem AVenhance.Infra.Section4.amnrAdvectionDerivativeTerms_value {c : AmnrSpace → Homogenization.Vec 2} {v : Fin 2 → AmnrSpace → ℝ} {f : AmnrSpace → ℝ} (hc : ContDiff ℝ (↑⊤) c) (hv : ∀ (p : Fin 2), ContDiff ℝ (↑⊤) (v p)) (hf : ContDiff ℝ (↑⊤) f) (d : Option (Fin 2)) (A : List AmnrAdvectionFactor) (w : List (Option (Fin 2))) (z : AmnrSpace) : amnrOp c d (amnrAdvectionTermValue c v f { factors := A, scalarWord := w }) z = (List.map (fun (t : AmnrAdvectionTerm) => amnrAdvectionTermValue c v f t z) (amnrAdvectionDerivativeTerms d A w)).sum

The explicit finite derivative list evaluates to the actual derivative. Every intermediate derivative is admitted by proved smoothness.