Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Section3.CorrectorGradient

Explicit spatial derivatives of the single-mode correctors.

source
theorem AVenhance.Infra.Section3.CorrectorGradient.spaceGrad_cosCoordinate (A ω : ℝ) (i j : Fin 2) (x : Homogenization.Vec 2) :
spaceGrad (fun (y : Homogenization.Vec 2) => A * Real.cos (ω * y i)) x j = if j = i then -A * ω * Real.sin (ω * x i) else 0
source
theorem AVenhance.Infra.Section3.CorrectorGradient.freq_eq (ε x : ℝ) (hε : ε ≠ 0) :
2 * Real.pi / ε * x = 2 * Real.pi * x / ε
source
theorem AVenhance.Infra.Section3.chiMK_spaceGrad_one {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (hk : k % 4 = 1) (hε : epsilon β I.Λ m ≠ 0) :
spaceGrad (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y 1) x 0 = 4 * Real.pi ^ 2 * a β I.Λ m * I.corrTime κ m k t * Real.sin (2 * Real.pi * x 0 / epsilon β I.Λ m)

The nonzero corrector derivative for a horizontal odd shear.

source
theorem AVenhance.Infra.Section3.chiMK_spaceGrad_one_all {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (j : Fin 2) (hk : k % 4 = 1) (hε : epsilon β I.Λ m ≠ 0) :
spaceGrad (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y 1) x j = if j = 0 then 4 * Real.pi ^ 2 * a β I.Λ m * I.corrTime κ m k t * Real.sin (2 * Real.pi * x 0 / epsilon β I.Λ m) else 0

The full coordinate derivative formula for the horizontal component of an active horizontal shear.

source
theorem AVenhance.Infra.Section3.chiMK_spaceGrad_three {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (hk : k % 4 = 3) (hε : epsilon β I.Λ m ≠ 0) :
spaceGrad (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y 0) x 1 = -(4 * Real.pi ^ 2 * a β I.Λ m * I.corrTime κ m k t) * Real.sin (2 * Real.pi * x 1 / epsilon β I.Λ m)

The nonzero corrector derivative for a vertical odd shear.

source
theorem AVenhance.Infra.Section3.chiMK_spaceGrad_three_all {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (j : Fin 2) (hk : k % 4 = 3) (hε : epsilon β I.Λ m ≠ 0) :
spaceGrad (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y 0) x j = if j = 1 then -(4 * Real.pi ^ 2 * a β I.Λ m * I.corrTime κ m k t) * Real.sin (2 * Real.pi * x 1 / epsilon β I.Λ m) else 0

The full coordinate derivative formula for the vertical component of an active vertical shear.