Finite actual products in the spatial drift commutator.

structure AVenhance.Infra.Section4.AmnrDriftTerm : Type

Indices and derivative words describing one differentiated drift product.

• row : Fin 2

  Velocity component in the differentiated drift product.

• column : Fin 2

  Spatial direction of the scalar derivative in the drift product.

• coefficientWord : List (Fin 2)

  Spatial derivative word applied to the velocity coefficient.

• scalarWord : List (Fin 2)

  Spatial derivative word applied to the scalar factor.

noncomputable def AVenhance.Infra.Section4.amnrDriftTermValue (b : AmnrSpace → Homogenization.Vec 2) (f : AmnrSpace → ℝ) (q : AmnrDriftTerm) : AmnrSpace → ℝ

The actual product represented by one differentiated drift term.

Equations

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

def AVenhance.Infra.Section4.amnrDriftDerivativeTerms (i : Fin 2) (q : AmnrDriftTerm) : List AmnrDriftTerm

A coordinate derivative can fall on either actual factor.

Equations

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

theorem AVenhance.Infra.Section4.amnrDriftTermValue_contDiff {b : AmnrSpace → Homogenization.Vec 2} {f : AmnrSpace → ℝ} (hb : ContDiff ℝ (↑⊤) b) (hf : ContDiff ℝ (↑⊤) f) (q : AmnrDriftTerm) : ContDiff ℝ (↑⊤) (amnrDriftTermValue b f q)

theorem AVenhance.Infra.Section4.amnrDriftDerivativeTerms_value {b : AmnrSpace → Homogenization.Vec 2} {f : AmnrSpace → ℝ} (hb : ContDiff ℝ (↑⊤) b) (hf : ContDiff ℝ (↑⊤) f) (i : Fin 2) (q : AmnrDriftTerm) : amnrOp b (some i) (amnrDriftTermValue b f q) = (List.map (amnrDriftTermValue b f) (amnrDriftDerivativeTerms i q)).sum

Each step is the product rule for actual derivatives, without an estimate or an assumed commutator expansion.