Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Section4.Amnr.VelocityFirstSpatialSum

Scale summation for every spatial first-material velocity jet.

theorem AVenhance.Infra.Section4.amnrWord_sub_global {b : AmnrSpace → Homogenization.Vec 2} {f g : AmnrSpace → ℝ} (hb : ContDiff ℝ (↑⊤) b) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (w : List (Option (Fin 2))) :
amnrWord b w (f - g) = amnrWord b w f - amnrWord b w g

A smooth global difference commutes with every actual word.