Column divergence of the per-corrector diffusion flux and its inverse-flow expansion.

theorem AVenhance.Infra.Section5.CorrectorDiffusionDivergence.vecDiv_eq_fderiv {V : Homogenization.Vec 2 → Homogenization.Vec 2} {x : Homogenization.Vec 2} {LV : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} (hV : HasFDerivAt V LV x) : vecDiv V x = ∑ i : Fin 2, LV (Homogenization.basisVec i) i

theorem AVenhance.Infra.Section5.CorrectorDiffusionDivergence.vecDiv_add_hasFDerivAt {V W : Homogenization.Vec 2 → Homogenization.Vec 2} {x : Homogenization.Vec 2} {LV LW : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} (hV : HasFDerivAt V LV x) (hW : HasFDerivAt W LW x) : vecDiv (fun (y : Homogenization.Vec 2) => V y + W y) x = vecDiv V x + vecDiv W x

theorem AVenhance.Infra.Section5.CorrectorDiffusionDivergence.vecDiv_const_eq_zero (v x : Homogenization.Vec 2) : vecDiv (fun (x : Homogenization.Vec 2) => v) x = 0

noncomputable def AVenhance.Infra.Section5.correctorBaseMatrix {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (k : ℤ) (t κ : ℝ) (y : Homogenization.Vec 2) : Matrix (Fin 2) (Fin 2) ℝ

Shear matrix plus the diffusive corrector gradient, evaluated along the inverse flow.

Equations

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

noncomputable def AVenhance.Infra.Section5.correctorDefectMatrix {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (k : ℤ) (t κ : ℝ) (y : Homogenization.Vec 2) : Matrix (Fin 2) (Fin 2) ℝ

Corrector defect caused by the inverse-flow Jacobian's deviation from the identity.

Equations

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

noncomputable def AVenhance.Infra.Section5.correctorPushforwardMatrix {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (k : ℤ) (t κ : ℝ) (y : Homogenization.Vec 2) : Matrix (Fin 2) (Fin 2) ℝ

Corrector matrix contribution caused by the transposed flow Jacobian's deviation from identity.

Equations

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

noncomputable def AVenhance.Infra.Section5.correctorShearCrossColumn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (k : ℤ) (t κ : ℝ) (j : Fin 2) (y : Homogenization.Vec 2) : Homogenization.Vec 2

Shear amplitude multiplied by the rotated gradient of one transported corrector component.

Equations

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

noncomputable def AVenhance.Infra.Section5.correctorDefectColumn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (k : ℤ) (t κ : ℝ) (j : Fin 2) (y : Homogenization.Vec 2) : Homogenization.Vec 2

Specified column of the inverse-flow corrector defect matrix.

Equations

• AVenhance.Infra.Section5.correctorDefectColumn I hΦ m k t κ j y i = AVenhance.Infra.Section5.correctorDefectMatrix I hΦ m k t κ y i j

noncomputable def AVenhance.Infra.Section5.correctorPushforwardColumn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (k : ℤ) (t κ : ℝ) (j : Fin 2) (y : Homogenization.Vec 2) : Homogenization.Vec 2

Specified column of the corrector pushforward matrix.

Equations

• AVenhance.Infra.Section5.correctorPushforwardColumn I hΦ m k t κ j y i = AVenhance.Infra.Section5.correctorPushforwardMatrix I hΦ m k t κ y i j

theorem AVenhance.Infra.Section5.CorrectorDiffusionDivergence.correctorFlux_column_decomposition {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (k : ℤ) (t κ : ℝ) (j : Fin 2) : (fun (y : Homogenization.Vec 2) (i : Fin 2) => correctorFlux I hΦ m κ k t y i j) = fun (y : Homogenization.Vec 2) => κ • Homogenization.basisVec j + frozenCorrectorFlux I κ m k j t (I.xFlowInv hΦ m (lIdx β I.Λ m k) t y) + correctorDefectColumn I hΦ m k t κ j y + correctorShearCrossColumn I hΦ m k t κ j y

theorem AVenhance.Infra.Section5.frozen_corrector_diffusion_column_divergence {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (κ : ℝ) (j : Fin 2) {LM LB LD LE : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} {LQ : Fin 2 → Fin 2 → Homogenization.Vec 2 →L[ℝ] ℝ} (hM : HasFDerivAt (I.xFlowInv hΦ m (lIdx β I.Λ m k) t) LM x) (hB : HasFDerivAt (frozenCorrectorFlux I κ m k j t) LB (I.xFlowInv hΦ m (lIdx β I.Λ m k) t x)) (hD : HasFDerivAt (correctorDefectColumn I hΦ m k t κ j) LD x) (hE : HasFDerivAt (correctorShearCrossColumn I hΦ m k t κ j) LE x) (hQ : ∀ (i q : Fin 2), HasFDerivAt (fun (y : Homogenization.Vec 2) => rowCofactor (gradMatrix (I.xFlowInv hΦ m (lIdx β I.Λ m k) t) y) i q) (LQ i q) x) (hPiolaDiv : ∀ (q : Fin 2), ∑ i : Fin 2, (LQ i q) (Homogenization.basisVec i) = 0) (hdiv : ∀ (r : ℝ) (y : Homogenization.Vec 2), Flow.spatialDivergence (streamVel (Φ (m - 1))) r y = 0) : matDiv (correctorFlux I hΦ m κ k t) x j = deriv (fun (s : ℝ) => I.chiMK κ m k s (I.xFlowInv hΦ m (lIdx β I.Λ m k) t x) j) t + matDiv (correctorDefectMatrix I hΦ m k t κ) x j + matDiv (correctorPushforwardMatrix I hΦ m k t κ) x j

Column divergence of the twisted-corrector diffusion matrix. The displayed derivative inputs are only local regularity: one derivative of the pulled base flux and of the two error columns, one derivative of the inverse-flow cofactor, and the explicit Piola divergence identity.