The grouped corrector error mean is the mean of an explicit periodic finite-mode divergence.

LeftJacobian the left-Jacobian form: the slots twistie4, twistie5, normie3 differ from the pre-LeftJacobian bodies twistie4ND, twistie5ND, normie3Old = Σ_k ξ_k (𝒥 - C_k) : ∇G_k by Σ_k ξ_k (F_kᵀ - 1) P : ∇G_k, P = 𝒥 - κ I (LeftJacobian.twistie4Plus_eq, LeftJacobian.normie3_matrix_split), and (F_kᵀ - 1) P has zero column divergence (LeftJacobian.piola_column_hasFDerivAt), so this extra term is again a divergence of a smooth periodic field.

theorem AVenhance.Infra.Section5.Integration.BigBoundMeanZeroGroup.meanZeroGroup_xFlowInv_right_inverse {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (x : Homogenization.Vec 2) : I.xFlow hΦ m l t (I.xFlowInv hΦ m l t x) = x

theorem AVenhance.Infra.Section5.Integration.BigBoundMeanZeroGroup.meanZeroGroup_vecDot_matrixMulVec_transpose (A : Matrix (Fin 2) (Fin 2) ℝ) (u v : Homogenization.Vec 2) : Homogenization.vecDot u (A.mulVec v) = Homogenization.vecDot (A.transpose.mulVec u) v

theorem AVenhance.Infra.Section5.Integration.BigBoundMeanZeroGroup.meanZeroGroup_vecDot_comm (u v : Homogenization.Vec 2) : Homogenization.vecDot u v = Homogenization.vecDot v u

theorem AVenhance.Infra.Section5.Integration.BigBoundMeanZeroGroup.meanZeroGroup_timeDerivative_pairing_pushforward {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (hT : ContDiff ℝ 1 (T t)) : Homogenization.vecDot (chiMKTimeDerivative I m κ k t (I.xFlowInv hΦ m (lIdx β I.Λ m k) t x)) (G I hΦ m T (lIdx β I.Λ m k) t x) = Homogenization.vecDot (chiTimePushforwardFlux I hΦ m κ k t x) (spaceGrad (T t) x)

theorem AVenhance.Infra.Section5.Integration.BigBoundMeanZeroGroup.matrixMulVec_contDiff_infty {A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {V : Homogenization.Vec 2 → Homogenization.Vec 2} (hA : ContDiff ℝ (↑⊤) A) (hV : ContDiff ℝ (↑⊤) V) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => (A x).mulVec (V x)

noncomputable def AVenhance.Infra.Section5.Integration.BigBoundMeanZeroGroup.meanZeroGroupNormie3Old {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : ℝ

The pre-LeftJacobian body of normie3: Σ_k ξ_k (𝒥 - C_k) : ∇G_k with the pulled corrector flux C_k.

Equations

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

theorem AVenhance.Infra.Section5.Integration.group_meanZero_of_slice {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) {t : ℝ} (hTsm : ContDiff ℝ (↑⊤) (T t)) (hTper : IsZ2Periodic (T t)) : Homogenization.MeanZeroOn unitCube fun (x : Homogenization.Vec 2) => twistie4 I hΦ m κ T t x + twistie5 I hΦ m κ T t x + normie3 I hΦ m κ T t x

The sum of the three corrector error terms is a divergence. Its flux is the finite active-mode sum of (J-C_k)G_k + T PDot_k, where PDot_k is the Piola push-forward of the fixed-space time derivative of the shear.