The local derivatives in the corrector diffusion identity follow from the spatial C² regularity of the flows and correctors.
theorem
AVenhance.Infra.Section5.CorrectorDiffusionRegularity.gradMatrix_contDiff_one_of_contDiff_two_local
{X : Homogenization.Vec 2 → Homogenization.Vec 2}
(hX : ContDiff ℝ 2 X)
:
ContDiff ℝ 1 fun (x : Homogenization.Vec 2) => gradMatrix X x
theorem
AVenhance.Infra.Section5.CorrectorDiffusionRegularity.chiMK_vector_contDiff_two
{β : ℝ}
(I : Ingredients β)
(κ : ℝ)
(m : ℕ)
(k : ℤ)
(t : ℝ)
:
ContDiff ℝ 2 fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y
theorem
AVenhance.Infra.Section5.CorrectorDiffusionRegularity.psi_contDiff_two
{β : ℝ}
(I : Ingredients β)
(m : ℕ)
(k : ℤ)
:
theorem
AVenhance.Infra.Section5.CorrectorDiffusionRegularity.matrixMul_contDiff_one_local
{A B : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ}
(hA : ContDiff ℝ 1 A)
(hB : ContDiff ℝ 1 B)
:
ContDiff ℝ 1 fun (y : Homogenization.Vec 2) => A y * B y
theorem
AVenhance.Infra.Section5.CorrectorDiffusionRegularity.corrector_diffusion_columns_contDiff_one
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(k : ℤ)
(t κ : ℝ)
(j : Fin 2)
:
ContDiff ℝ 1 (frozenCorrectorFlux I κ m k j t) ∧ ContDiff ℝ 1 (correctorDefectColumn I hΦ m k t κ j) ∧ ContDiff ℝ 1 (correctorShearCrossColumn I hΦ m k t κ j)
theorem
AVenhance.Infra.Section5.diffusionMatrix_selected_corrector_column_divergence_of_smooth
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(hm : 1 ≤ m)
(k : ℤ)
(t : ℝ)
(x : Homogenization.Vec 2)
(κ : ℝ)
(j : Fin 2)
(hk : Odd k)
(hxi : I.xiMK m k t ≠ 0)
(hdiv : ∀ (r : ℝ) (y : Homogenization.Vec 2), Flow.spatialDivergence (streamVel (Φ (m - 1))) r y = 0)
:
matDiv (fun (y : Homogenization.Vec 2) => diffusionMatrix I hΦ m κ t y * (1 + gradChiTilde I hΦ m κ k t y)) 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
The full selected diffusion-column expansion with its local regularity derived from the flow and corrector definitions.