A modewise flux-energy identity from the exact memory ODE.

theorem AVenhance.Infra.Section3.FluxEnergy.corrTime_mul_deriv_interval {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) (s t : ℝ) : ∫ (r : ℝ) in s..t, I.corrTime κ m k r * deriv (I.corrTime κ m k) r = (I.corrTime κ m k t ^ 2 - I.corrTime κ m k s ^ 2) / 2

theorem AVenhance.Infra.Section3.activeFluxEnergyBalance_one {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (k : ℤ) (t : ℝ) (hk : k % 4 = 1) : ((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) - κ * spaceAvg fun (x : Homogenization.Vec 2) => spaceGrad (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y 1) x 0 ^ 2) = 2 * Real.pi ^ 2 * a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 2 * I.corrTime κ m k t * deriv (I.corrTime κ m k) t

For a horizontal active shear, the instantaneous flux correction minus the corrector energy is exactly the memory derivative term.

theorem AVenhance.Infra.Section3.activeFluxEnergyBalance_three {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (k : ℤ) (t : ℝ) (hk : k % 4 = 3) : ((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) - κ * spaceAvg fun (x : Homogenization.Vec 2) => spaceGrad (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y 0) x 1 ^ 2) = 2 * Real.pi ^ 2 * a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 2 * I.corrTime κ m k t * deriv (I.corrTime κ m k) t

The same instantaneous flux-energy identity holds for a vertical active shear, with the matching first coordinate.

theorem AVenhance.Infra.Section3.activeFluxEnergyBalance_one_small {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ τ L : ℝ) (hκ : 0 < κ) (hτ : 0 < τ) (k : ℤ) (t : ℝ) (hk : k % 4 = 1) (hderiv : |deriv (I.corrTime κ m k) t| ≤ L * epsilon β I.Λ m ^ 2 / (κ * τ)) : |(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) - κ * spaceAvg fun (x : Homogenization.Vec 2) => spaceGrad (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y 1) x 0 ^ 2| ≤ L * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / (2 * κ)) * (epsilon β I.Λ m ^ 2 / (κ * τ))

The horizontal single-mode flux-energy defect has the small scale of the full source lemma whenever the memory derivative has the corresponding slow forcing bound. The derivative estimate is kept as an explicit hypothesis here; the full moving-cutoff aggregate still needs that estimate proved and summed.

theorem AVenhance.Infra.Section3.activeFluxEnergyBalance_three_small {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ τ L : ℝ) (hκ : 0 < κ) (hτ : 0 < τ) (k : ℤ) (t : ℝ) (hk : k % 4 = 3) (hderiv : |deriv (I.corrTime κ m k) t| ≤ L * epsilon β I.Λ m ^ 2 / (κ * τ)) : |(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) - κ * spaceAvg fun (x : Homogenization.Vec 2) => spaceGrad (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y 0) x 1 ^ 2| ≤ L * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / (2 * κ)) * (epsilon β I.Λ m ^ 2 / (κ * τ))

The vertical active-mode flux-energy defect has the same conditional small-scale estimate.

theorem AVenhance.Infra.Section3.activeFluxEnergyBalance_one_cutoff_error {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (hκ : 0 < κ) (k : ℤ) (t : ℝ) (hk : k % 4 = 1) : |(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) - κ * spaceAvg fun (x : Homogenization.Vec 2) => spaceGrad (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y 1) x 0 ^ 2| ≤ (I.Czeta + I.Chat) / (4 * Real.pi ^ 2) * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / (2 * κ)) * (epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m))

The horizontal active-mode defect estimate with its derivative hypothesis discharged from the cutoff bounds.

theorem AVenhance.Infra.Section3.activeFluxEnergyBalance_three_cutoff_error {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (hκ : 0 < κ) (k : ℤ) (t : ℝ) (hk : k % 4 = 3) : |(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) - κ * spaceAvg fun (x : Homogenization.Vec 2) => spaceGrad (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y 0) x 1 ^ 2| ≤ (I.Czeta + I.Chat) / (4 * Real.pi ^ 2) * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / (2 * κ)) * (epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m))

The vertical active-mode defect estimate with its derivative hypothesis discharged from the cutoff bounds.