Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Section4.IteratesVelocityLower

Every material commutator contains a positive-order velocity jet.

theorem AVenhance.Infra.Section4.iterateWordMaterialError_lower_velocity {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {u : ℝ → Homogenization.Vec 2 → ℝ} (hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ioi 0 ×ˢ Set.univ)) (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ioi 0 ×ˢ Set.univ)) {t : ℝ} (ht : 0 < t) (w : List (Fin 2)) (x : Homogenization.Vec 2) :
iterateWordMaterialError (fun (z : AmnrSpace) => b z.1 z.2) w (fun (z : AmnrSpace) => u z.1 z.2) (t, x) = ∑ j : Fin 2, (List.map (fun (p : List (Fin 2) × List (Fin 2)) => iterateSpatialWord p.1 (fun (y : Homogenization.Vec 2) => b t y j) x * spaceGrad (iterateSpatialWord p.2 (u t)) x j) (List.filter (fun (p : List (Fin 2) × List (Fin 2)) => !p.1.isEmpty) (iterateSpatialSplits w))).sum

The velocity commutator has exactly the nonprincipal ordered splits.