Matrix entry calculations for the explicit active-mode flux.

def AVenhance.Infra.Section3.FluxMatrix.closedUnitSquare : Set (Homogenization.Vec 2)

Closed spatial unit cell used for compactness and periodic integration.

Equations

• AVenhance.Infra.Section3.FluxMatrix.closedUnitSquare = Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

theorem AVenhance.Infra.Section3.FluxMatrix.continuous_integrableOn_unitCell {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) : MeasureTheory.IntegrableOn f (Torus.unitCell 2) MeasureTheory.volume

theorem AVenhance.Infra.Section3.FluxMatrix.spaceAvg_add_of_continuous {f g : Homogenization.Vec 2 → ℝ} (hf : Continuous f) (hg : Continuous g) : (spaceAvg fun (x : Homogenization.Vec 2) => f x + g x) = spaceAvg f + spaceAvg g

theorem AVenhance.Infra.Section3.FluxMatrix.spaceAvg_sub_of_continuous {f g : Homogenization.Vec 2 → ℝ} (hf : Continuous f) (hg : Continuous g) : (spaceAvg fun (x : Homogenization.Vec 2) => f x - g x) = spaceAvg f - spaceAvg g

theorem AVenhance.Infra.Section3.FluxMatrix.spaceAvg_const_eq (c : ℝ) : (spaceAvg fun (x : Homogenization.Vec 2) => c) = c

theorem AVenhance.Infra.Section3.FluxMatrix.spaceAvg_const_mul (c : ℝ) (f : Homogenization.Vec 2 → ℝ) : (spaceAvg fun (x : Homogenization.Vec 2) => c * f x) = c * spaceAvg f

theorem AVenhance.Infra.Section3.FluxMatrix.chiMK_horizontal_zero_component {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) (t : ℝ) (hk : k % 4 = 1) : (fun (x : Homogenization.Vec 2) => I.chiMK κ m k t x 0) = fun (x : Homogenization.Vec 2) => 0

theorem AVenhance.Infra.Section3.FluxMatrix.chiMK_vertical_zero_component {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) (t : ℝ) (hk : k % 4 = 3) : (fun (x : Homogenization.Vec 2) => I.chiMK κ m k t x 1) = fun (x : Homogenization.Vec 2) => 0

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

Entries of the gradient matrix for a horizontal active corrector mode.

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

Entries of the gradient matrix for a vertical active corrector mode.

theorem AVenhance.Infra.Section3.spaceAvg_psi_eq_zero {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (k : ℤ) (hk : k % 4 = 1 ∨ k % 4 = 3) : spaceAvg (psi β I.Λ m k) = 0

A single shear mode has zero spatial mean.

theorem AVenhance.Infra.Section3.FluxMatrix.psiM_eq_active_mode {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (k : ℤ) (t : ℝ) (hk : Odd k) (hzk : I.zetaMK m k t ≠ 0) : (fun (x : Homogenization.Vec 2) => I.psiM m t x) = fun (x : Homogenization.Vec 2) => I.zetaProd m k t * psi β I.Λ m k x

theorem AVenhance.Infra.Section3.FluxMatrix.chiM_eq_active_mode {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (k : ℤ) (t : ℝ) (hk : Odd k) (hzk : I.zetaMK m k t ≠ 0) : I.chiM κ m t = fun (x : Homogenization.Vec 2) => I.chiMK κ m k t x

theorem AVenhance.Infra.Section3.FluxMatrix.fluxIntegrand_active_one_matrix {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (k : ℤ) (t : ℝ) (hk : k % 4 = 1) (hzk : I.zetaMK m k t ≠ 0) (x : Homogenization.Vec 2) : I.fluxIntegrand κ m t x = Matrix.of fun (i j : Fin 2) => if i = 0 then if j = 0 then κ else κ * spaceGrad (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y 1) x 0 - I.zetaProd m k t * psi β I.Λ m k x else if j = 0 then I.zetaProd m k t * psi β I.Λ m k x else κ + 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

The full flux integrand on an active horizontal mode, entry by entry.

theorem AVenhance.Infra.Section3.FluxMatrix.fluxIntegrand_active_three_matrix {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (k : ℤ) (t : ℝ) (hk : k % 4 = 3) (hzk : I.zetaMK m k t ≠ 0) (x : Homogenization.Vec 2) : I.fluxIntegrand κ m t x = Matrix.of fun (i j : Fin 2) => if i = 0 then if j = 0 then κ + 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 else -(I.zetaProd m k t * psi β I.Λ m k x) else if j = 0 then 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 else κ

theorem AVenhance.Infra.Section3.flux_active_one {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (k : ℤ) (t : ℝ) (hk : k % 4 = 1) (hzk : I.zetaMK m k t ≠ 0) : I.flux κ m t = κ • 1 + (2 * Real.pi ^ 2 * a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 2 * I.zetaProd m k t * I.corrTime κ m k t) • Matrix.single 1 1 1

The full spatially averaged flux matrix on an active horizontal mode.

theorem AVenhance.Infra.Section3.flux_active_three {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (k : ℤ) (t : ℝ) (hk : k % 4 = 3) (hzk : I.zetaMK m k t ≠ 0) : I.flux κ m t = κ • 1 + (2 * Real.pi ^ 2 * a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 2 * I.zetaProd m k t * I.corrTime κ m k t) • Matrix.single 0 0 1

The full spatially averaged flux matrix on an active vertical mode.

theorem AVenhance.Infra.Section3.FluxMatrix.gradMatrix_entry_continuous {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ t : ℝ) (i j : Fin 2) : Continuous fun (x : Homogenization.Vec 2) => gradMatrix (I.chiM κ m t) x i j

theorem AVenhance.Infra.Section3.flux_eq_kappa_of_no_odd_active {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ t : ℝ) (hzero : ∀ (k : ℤ), Odd k → I.zetaMK m k t = 0) : I.flux κ m t = κ • 1

If every odd stream mode is inactive, its spatially averaged flux is just κ I; the remaining corrector-gradient term has zero mean by periodicity.

theorem AVenhance.Infra.Section3.flux_offdiag_eq_zero {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ t : ℝ) {i j : Fin 2} (hij : i ≠ j) : I.flux κ m t i j = 0

The complete fixed-time flux has no off-diagonal entries.

theorem AVenhance.Infra.Section3.flux_diag_ge_kappa {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ t : ℝ) (i : Fin 2) : κ ≤ I.flux κ m t i i

Every diagonal flux entry is at least the molecular diffusivity κ.

theorem AVenhance.Infra.Section3.FluxMatrix.activeFluxCoeff_le_amplitude {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (hκ : 0 < κ) (k : ℤ) (t : ℝ) : 2 * Real.pi ^ 2 * a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 2 * I.zetaProd m k t * I.corrTime κ m k t ≤ a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / (2 * κ)

theorem AVenhance.Infra.Section3.flux_diag_le_kappa_add_amplitude {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (hκ : 0 < κ) (t : ℝ) (i : Fin 2) : I.flux κ m t i i ≤ κ + a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / (2 * κ)

The fixed-time diagonal flux has a uniform upper bound from the memory relaxation estimate.