Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Section3.FluxSymmetry

The time shift by two large cells exchanges the active flux direction.

theorem AVenhance.Infra.Section3.zetaMK_add_twoCellCount {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (k : ℤ) (t : ℝ) :
I.zetaMK m (k + 2 * ↑(Ingredients.tauCellCount β I.Λ m)) (t + 2 * tauPP β I.Λ m) = I.zetaMK m k t

The small shear cutoff is invariant under shifting time by two large cells and its integer mode by twice the number of small cells in a large cell.

theorem AVenhance.Infra.Section3.flux_add_twoCellCount_swap {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ t : ℝ) (i j : Fin 2) :
I.flux κ m (t + 2 * tauPP β I.Λ m) i j = I.flux κ m t (if i = 0 then 1 else 0) (if j = 0 then 1 else 0)

Entrywise covariance of the fixed-time flux under the large-cell time shift and coordinate swap.

theorem AVenhance.Infra.Section3.flux_fourCell_periodic {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ t : ℝ) (i j : Fin 2) :
I.flux κ m (t + 2 * tauPP β I.Λ m + 2 * tauPP β I.Λ m) i j = I.flux κ m t i j

A second simultaneous time shift restores each flux entry, so the fixed-time flux has period 4 τ''_m.