Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Section5.LeftJacobian.CellMeanPull

: the pulled cell flux C⁰_k of normie3⁺ is the cell flux cellFluxCell (whose fast mean is the flux, cellFluxCell_mean) composed with the inverse flow Y_{l_k}.

theorem AVenhance.Infra.Section5.LeftJacobian.cellFlux_eq_cellFluxCell_comp {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) :
cellFlux I hΦ m κm k t x = cellFluxCell I m κm k t (I.xFlowInv hΦ m (lIdx β I.Λ m k) t x)

C⁰_k(x) = cellFluxCell (Y_{l_k} x).