Fast factor of normie3

normie3 = Σ_k ξ_k frob (F_kᵀ (𝒥 - C⁰_k)) ∇G_k with C⁰_k = cellFluxCell ∘ Y_k. Expanding the Frobenius product, the fast factor in the cell variable is the (p, j) entry of 𝒥 - cellFluxCell, which is continuous, 1/ε_m-periodic, has exact zero cell mean on the support of ξ_{m,k} and is bounded by 4 ψ (1 + ψ/κ), ψ = a_m ε_m². Off the support the fast factor is set to 0 (the slow factor vanishes there).

noncomputable def AVenhance.Infra.Section5.Contracts.n3Fast {β : ℝ} (I : Ingredients β) (κ : ℝ) (m : ℕ) (k : ℤ) (t : ℝ) (p j : Fin 2) (z : Homogenization.Vec 2) : ℝ

The fast factor (𝒥 - C⁰_k)_{pj} of normie3 in the cell variable (zero off supp ξ_{m,k}).

Equations

• AVenhance.Infra.Section5.Contracts.n3Fast I κ m k t p j z = if I.xiMK m k t = 0 then 0 else (I.flux κ m t - AVenhance.Infra.Section5.LeftJacobian.cellFluxCell I m κ k t z) p j

theorem AVenhance.Infra.Section5.Contracts.n3Fast_of_xi_eq_zero {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) (t : ℝ) (p j : Fin 2) (h : I.xiMK m k t = 0) : n3Fast I κ m k t p j = fun (x : Homogenization.Vec 2) => 0

theorem AVenhance.Infra.Section5.Contracts.n3Fast_of_xi_ne_zero {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) (t : ℝ) (p j : Fin 2) (h : I.xiMK m k t ≠ 0) (z : Homogenization.Vec 2) : n3Fast I κ m k t p j z = (I.flux κ m t - LeftJacobian.cellFluxCell I m κ k t z) p j

theorem AVenhance.Infra.Section5.Contracts.cellFluxCell_apply {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) (t : ℝ) (z : Homogenization.Vec 2) (p j : Fin 2) : LeftJacobian.cellFluxCell I m κ k t z p j = ∑ q : Fin 2, (κ * 1 p q + I.zetaProd m k t * psi β I.Λ m k z * sigmaMat p q) * (1 q j + gradMatrix (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y) z q j)

Entry form of the cell flux.

theorem AVenhance.Infra.Section5.Contracts.cellFluxCell_expand {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) (t : ℝ) (z : Homogenization.Vec 2) : LeftJacobian.cellFluxCell I m κ k t z = κ • 1 + κ • gradMatrix (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y) z + (I.zetaProd m k t * psi β I.Λ m k z) • sigmaMat + (I.zetaProd m k t * psi β I.Λ m k z) • (sigmaMat * gradMatrix (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y) z)

theorem AVenhance.Infra.Section5.Contracts.n3Fast_continuous {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) {k : ℤ} (hk : Odd k) (t : ℝ) (p j : Fin 2) : Continuous (n3Fast I κ m k t p j)

theorem AVenhance.Infra.Section5.Contracts.n3Fast_isFastPeriodic {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (k : ℤ) (t : ℝ) (p j : Fin 2) : Ergodic.IsFastPeriodic (ergodicFrequency β I.Λ m) (n3Fast I κ m k t p j)

theorem AVenhance.Infra.Section5.Contracts.n3Fast_cellAverage {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) {k : ℤ} (hk : Odd k) (t : ℝ) (p j : Fin 2) : Ergodic.cellAverage (n3Fast I κ m k t p j) = 0

theorem AVenhance.Infra.Section5.Contracts.cellFluxCell_sub_kappa_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (k : ℤ) (t : ℝ) (z : Homogenization.Vec 2) (p j : Fin 2) : |LeftJacobian.cellFluxCell I m κ k t z p j - κ * 1 p j| ≤ 2 * (a β I.Λ m * epsilon β I.Λ m ^ 2) * (1 + a β I.Λ m * epsilon β I.Λ m ^ 2 / κ)

Entries of cellFluxCell - κ I are bounded by 2ψ(1 + ψ/κ), ψ = a_m ε_m².

theorem AVenhance.Infra.Section5.Contracts.flux_sub_kappa_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (t : ℝ) (p j : Fin 2) : |I.flux κ m t p j - κ * 1 p j| ≤ (a β I.Λ m * epsilon β I.Λ m ^ 2) ^ 2 / (2 * κ)

Entries of 𝒥 - κ I are bounded by ψ²/(2κ).

theorem AVenhance.Infra.Section5.Contracts.n3Fast_abs_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (k : ℤ) (t : ℝ) (p j : Fin 2) (z : Homogenization.Vec 2) : |n3Fast I κ m k t p j z| ≤ 4 * (a β I.Λ m * epsilon β I.Λ m ^ 2) * (1 + a β I.Λ m * epsilon β I.Λ m ^ 2 / κ)

Sup bound of the fast factor: |n3Fast| ≤ 4ψ(1 + ψ/κ).