Actual differentiated correction monomials for changing material velocity.

def AVenhance.Infra.Section4.amnrAdvectionVelocity (b c : AmnrSpace → Homogenization.Vec 2) (p : Fin 2) : AmnrSpace → ℝ

The actual difference of the two advecting velocities.

Equations

• AVenhance.Infra.Section4.amnrAdvectionVelocity b c p z = b z p - c z p

theorem AVenhance.Infra.Section4.amnrAdvectionVelocity_contDiff {b c : AmnrSpace → Homogenization.Vec 2} (hb : ContDiff ℝ (↑⊤) b) (hc : ContDiff ℝ (↑⊤) c) (p : Fin 2) : ContDiff ℝ (↑⊤) (amnrAdvectionVelocity b c p)

def AVenhance.Infra.Section4.amnrChangedAdvectionDerivativeTerms (t : AmnrAdvectionTerm) : List AmnrAdvectionTerm

Every new-velocity material derivative is its coarse material part plus two actual fast-advection derivatives. Each new factor records its coordinate.

Equations

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

theorem AVenhance.Infra.Section4.amnrChangedAdvectionDerivativeTerms_value {b c : AmnrSpace → Homogenization.Vec 2} {f : AmnrSpace → ℝ} (hb : ContDiff ℝ (↑⊤) b) (hc : ContDiff ℝ (↑⊤) c) (hf : ContDiff ℝ (↑⊤) f) (t : AmnrAdvectionTerm) (z : AmnrSpace) : amnrOp b none (amnrAdvectionTermValue c (amnrAdvectionVelocity b c) f t) z = (List.map (fun (a : AmnrAdvectionTerm) => amnrAdvectionTermValue c (amnrAdvectionVelocity b c) f a z) (amnrChangedAdvectionDerivativeTerms t)).sum

The full differentiated list evaluates to the actual new material operator. Its two advection terms are retained, without commuting operators.

theorem AVenhance.Infra.Section4.amnrChangedAdvectionDerivativeTerms_list_value {b c : AmnrSpace → Homogenization.Vec 2} {f : AmnrSpace → ℝ} (hb : ContDiff ℝ (↑⊤) b) (hc : ContDiff ℝ (↑⊤) c) (hf : ContDiff ℝ (↑⊤) f) (T : List AmnrAdvectionTerm) (z : AmnrSpace) : amnrOp b none (List.map (amnrAdvectionTermValue c (amnrAdvectionVelocity b c) f) T).sum z = (List.map (fun (a : AmnrAdvectionTerm) => amnrAdvectionTermValue c (amnrAdvectionVelocity b c) f a z) (List.flatMap amnrChangedAdvectionDerivativeTerms T)).sum

The actual changed material operator differentiates a finite correction sum into the concatenated derivative lists.