TUpgrade Consumers Trace Frequency

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.TUpgradeConsumersTraceFrequency.iterateSpatialWord_eq_classicalWordDerivative (w : List (Fin 2)) (f : Homogenization.Vec 2 → ℝ) : iterateSpatialWord w f = classicalWordDerivative w f