The exact averaged diagonal contribution of a single active shear mode.

theorem AVenhance.Infra.Section3.zetaProd_nonneg {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (k : ℤ) (t : ℝ) : 0 ≤ I.zetaProd m k t

The shear forcing coefficient is nonnegative.

theorem AVenhance.Infra.Section3.corrTime_nonneg {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (k : ℤ) (t : ℝ) : 0 ≤ I.corrTime κ m k t

The exponential memory of a nonnegative shear forcing is nonnegative.

theorem AVenhance.Infra.Section3.spaceAvg_cross_one {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (k : ℤ) (t : ℝ) (hk : k % 4 = 1) (hε : epsilon β I.Λ m ≠ 0) : (spaceAvg fun (x : Homogenization.Vec 2) => I.zetaProd m k t * psi β I.Λ m k x * spaceGrad (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y 1) x 0) = 2 * Real.pi ^ 2 * a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 2 * I.zetaProd m k t * I.corrTime κ m k t

Spatially averaging the horizontal active-mode interaction gives the positive diagonal coefficient in e.Jm.explicit.mofo.

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

Spatially averaging the vertical active-mode interaction gives the same positive diagonal coefficient in the other coordinate.

theorem AVenhance.Infra.Section3.spaceAvg_chiMK_gradient_sq_one {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (k : ℤ) (t : ℝ) (hk : k % 4 = 1) : (spaceAvg fun (x : Homogenization.Vec 2) => spaceGrad (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y 1) x 0 ^ 2) = 8 * Real.pi ^ 4 * a β I.Λ m ^ 2 * I.corrTime κ m k t ^ 2

The mean square of the sole nonzero corrector gradient in a horizontal active shear. This is the energy term paired with the explicit flux formula.

theorem AVenhance.Infra.Section3.spaceAvg_chiMK_gradient_sq_three {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (k : ℤ) (t : ℝ) (hk : k % 4 = 3) : (spaceAvg fun (x : Homogenization.Vec 2) => spaceGrad (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y 0) x 1 ^ 2) = 8 * Real.pi ^ 4 * a β I.Λ m ^ 2 * I.corrTime κ m k t ^ 2

The mean square of the sole nonzero corrector gradient in a vertical active shear.