: the zero cell mean of the fast factor of normie3⁺.

For an odd k with ξ_{m,k}(t) ≠ 0, the unpulled cell flux z ↦ (κ I + p₀(z) σ)(I + ∇χ_k(z)), p₀ = ζ̂_{l_k} ζ_k ψ_k, has cell average exactly the flux 𝒥 = I.flux κ m t. Hence 𝒥 - C⁰_k has exact zero cell mean. Two cases: if ζ_k(t) ≠ 0 the unpulled integrand is the flux integrand pointwise; if ζ_k(t) = 0 then (by transition separation) every odd ζ vanishes, so 𝒥 = κ I, and ⟨κ (I + ∇χ_k)⟩ = κ I because ∇χ_k has mean zero.

noncomputable def AVenhance.Infra.Section5.LeftJacobian.cellFluxCell {β : ℝ} (I : Ingredients β) (m : ℕ) (κ : ℝ) (k : ℤ) (t : ℝ) (z : Homogenization.Vec 2) : Matrix (Fin 2) (Fin 2) ℝ

The unpulled cell flux in the cell variable: (κ I + p₀ σ)(I + ∇χ_k), p₀ = ζ̂ ζ_k ψ_k.

Equations

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

theorem AVenhance.Infra.Section5.LeftJacobian.CellMean.spaceAvg_const_eq' (c : ℝ) : (spaceAvg fun (x : Homogenization.Vec 2) => c) = c

theorem AVenhance.Infra.Section5.LeftJacobian.CellMean.spaceAvg_add' {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.Section5.LeftJacobian.CellMean.spaceAvg_sub' {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.Section5.LeftJacobian.CellMean.spaceAvg_const_mul' (c : ℝ) (f : Homogenization.Vec 2 → ℝ) : (spaceAvg fun (x : Homogenization.Vec 2) => c * f x) = c * spaceAvg f

theorem AVenhance.Infra.Section5.LeftJacobian.CellMean.continuous_psi {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) : Continuous (psi β I.Λ m k)

theorem AVenhance.Infra.Section5.LeftJacobian.CellMean.continuous_cellFluxCell {β : ℝ} (I : Ingredients β) (m : ℕ) (κ : ℝ) {k : ℤ} (hk : Odd k) (t : ℝ) : Continuous (cellFluxCell I m κ k t)

theorem AVenhance.Infra.Section5.LeftJacobian.cellFluxCell_mean {β : ℝ} (I : Ingredients β) (m : ℕ) (hm : 1 ≤ m) (κ : ℝ) {k : ℤ} (hk : Odd k) (t : ℝ) (hξ : I.xiMK m k t ≠ 0) : spaceAvgMat (cellFluxCell I m κ k t) = I.flux κ m t

The cell average of the unpulled cell flux is the flux.

theorem AVenhance.Infra.Section5.LeftJacobian.cellFluxCell_fastFactor_mean_zero {β : ℝ} (I : Ingredients β) (m : ℕ) (hm : 1 ≤ m) (κ : ℝ) {k : ℤ} (hk : Odd k) (t : ℝ) (hξ : I.xiMK m k t ≠ 0) : (spaceAvgMat fun (z : Homogenization.Vec 2) => I.flux κ m t - cellFluxCell I m κ k t z) = 0

The fast factor 𝒥 - C⁰_k of normie3⁺ has exact zero cell mean.