Time continuity of the homogenized flux from the active shear formula.

noncomputable def AVenhance.Infra.Section3.FluxTimeRegularity.fluxModeCoefficient {β : ℝ} (I : Ingredients β) (κ : ℝ) (m : ℕ) (k : ℤ) (t : ℝ) : ℝ

Scalar coefficient of a flux mode, including its cutoff and time corrector.

Equations

• AVenhance.Infra.Section3.FluxTimeRegularity.fluxModeCoefficient I κ m k t = 2 * Real.pi ^ 2 * AVenhance.a β I.Λ m ^ 2 * AVenhance.epsilon β I.Λ m ^ 2 * I.zetaProd m k t * I.corrTime κ m k t

def AVenhance.Infra.Section3.FluxTimeRegularity.fluxModeDirection (k : ℤ) : Matrix (Fin 2) (Fin 2) ℝ

Diagonal matrix direction selected by the flux mode index.

Equations

• AVenhance.Infra.Section3.FluxTimeRegularity.fluxModeDirection k = if k % 4 = 1 then Matrix.single 1 1 1 else if k % 4 = 3 then Matrix.single 0 0 1 else 0

noncomputable def AVenhance.Infra.Section3.FluxTimeRegularity.fluxModeTerm {β : ℝ} (I : Ingredients β) (κ : ℝ) (m : ℕ) (k : ℤ) (t : ℝ) : Matrix (Fin 2) (Fin 2) ℝ

Matrix-valued flux term obtained from one mode coefficient and direction.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Section3.FluxTimeRegularity.fluxModeTerm_continuous {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) : Continuous fun (t : ℝ) => fluxModeTerm I κ m k t

theorem AVenhance.Infra.Section3.FluxTimeRegularity.flux_eq_active_mode_series {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ t : ℝ) : I.flux κ m t = κ • 1 + ∑' (k : ℤ), fluxModeTerm I κ m k t

theorem AVenhance.Infra.Section3.FluxTimeRegularity.fluxModeTerm_eq_zero_of_xi_zero {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (k : ℤ) (t : ℝ) (hxi : I.xiMK m k t = 0) : fluxModeTerm I κ m k t = 0

theorem AVenhance.Infra.Section3.FluxTimeRegularity.fluxModeTerm_eq_bounded_sum {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ t₀ t : ℝ) (N : ℕ) (hN : (|t₀| + 1) / tau β I.Λ m + 2 < ↑N) (ht : t ∈ Set.Icc (t₀ - 1) (t₀ + 1)) : ∑' (k : ℤ), fluxModeTerm I κ m k t = ∑ k ∈ Finset.Icc (-↑N) ↑N, fluxModeTerm I κ m k t

theorem AVenhance.Infra.Section3.flux_entry_time_continuous {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (i j : Fin 2) : Continuous fun (t : ℝ) => I.flux κ m t i j

Every fixed flux entry is continuous in time. The active-mode formula reduces the spatial average to a locally finite sum of scalar memory terms.