Word Linear Calculus #
Support for the Armstrong–Vicol anomalous-diffusion formalization.
theorem
AVenhance.Infra.Section4.amnrWord_add
{U : Set AmnrSpace}
(hU : IsOpen U)
{b : AmnrSpace → Homogenization.Vec 2}
{f g : AmnrSpace → ℝ}
{N : ℕ}
(hb : ContDiffOn ℝ (↑N) b U)
(hf : ContDiffOn ℝ (↑N) f U)
(hg : ContDiffOn ℝ (↑N) g U)
(w : List (Option (Fin 2)))
(hw : w.length ≤ N)
: