Corrected inverse-flow push-forward decomposition for divergence, followed by its corrector specialization.
theorem
AVenhance.Infra.Section5.FlowPushforward.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)
:
theorem
AVenhance.Infra.Section5.vecDiv_matrix_identity_split
{V : Homogenization.Vec 2 → Homogenization.Vec 2}
{Q : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ}
{x : Homogenization.Vec 2}
{LV : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2}
{LQ : Fin 2 → Fin 2 → Homogenization.Vec 2 →L[ℝ] ℝ}
(hV : HasFDerivAt V LV x)
(hQ : ∀ (i j : Fin 2), HasFDerivAt (fun (y : Homogenization.Vec 2) => Q y i j) (LQ i j) x)
:
vecDiv V x = vecDiv (fun (y : Homogenization.Vec 2) => (Q y).mulVec (V y)) x + vecDiv (fun (y : Homogenization.Vec 2) => (1 - Q y).mulVec (V y)) x
Adding complementary matrix coefficients splits the divergence exactly.
This is the algebraic step behind the corrected e.pushforward formula.
theorem
AVenhance.Infra.Section5.vecDiv_comp_eq_pulledDiv_add_correction
{M g : Homogenization.Vec 2 → Homogenization.Vec 2}
{Q : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ}
{x : Homogenization.Vec 2}
{LM Lg : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2}
{LQ : Fin 2 → Fin 2 → Homogenization.Vec 2 →L[ℝ] ℝ}
(hM : HasFDerivAt M LM x)
(hg : HasFDerivAt g Lg (M x))
(hQ : ∀ (i j : Fin 2), HasFDerivAt (fun (y : Homogenization.Vec 2) => Q y i j) (LQ i j) x)
(hPiola : vecDiv (fun (y : Homogenization.Vec 2) => (Q y).mulVec (g (M y))) x = vecDiv g (M x))
:
vecDiv (fun (y : Homogenization.Vec 2) => g (M y)) x = vecDiv g (M x) + vecDiv (fun (y : Homogenization.Vec 2) => (1 - Q y).mulVec (g (M y))) x
Corrected push-forward decomposition: the Piola term is the pulled-back source divergence, and the complementary Jacobian coefficient remains as a separate divergence.
theorem
AVenhance.Infra.Section5.xFlowInv_cofactor_pushforward_split
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(l : ℤ)
(t : ℝ)
(x : Homogenization.Vec 2)
{g : Homogenization.Vec 2 → Homogenization.Vec 2}
{LM Lg : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2}
{LQ : Fin 2 → Fin 2 → Homogenization.Vec 2 →L[ℝ] ℝ}
(hM : HasFDerivAt (I.xFlowInv hΦ m l t) LM x)
(hg : HasFDerivAt g Lg (I.xFlowInv hΦ m l t x))
(hQ :
∀ (i j : Fin 2),
HasFDerivAt (fun (y : Homogenization.Vec 2) => rowCofactor (gradMatrix (I.xFlowInv hΦ m l t) y) i j) (LQ i j) x)
(hPiolaDiv : ∀ (j : Fin 2), ∑ i : Fin 2, (LQ i j) (Homogenization.basisVec i) = 0)
(hdiv : ∀ (r : ℝ) (y : Homogenization.Vec 2), Flow.spatialDivergence (streamVel (Φ (m - 1))) r y = 0)
:
vecDiv (fun (y : Homogenization.Vec 2) => g (I.xFlowInv hΦ m l t y)) x = vecDiv g (I.xFlowInv hΦ m l t x) + vecDiv
(fun (y : Homogenization.Vec 2) =>
(1 - rowCofactor (gradMatrix (I.xFlowInv hΦ m l t) y)).mulVec (g (I.xFlowInv hΦ m l t y)))
x
inverse-flow version with the coordinate Piola premise stated explicitly. The Jacobian correction has the transposed row-Jacobian orientation required by the matrix convention.
theorem
AVenhance.Infra.Section5.xFlowInv_corrector_pushforward
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(k : ℤ)
(t : ℝ)
(x : Homogenization.Vec 2)
(κ : ℝ)
(j : Fin 2)
{LM Lg : 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)
(hg : HasFDerivAt (frozenCorrectorFlux I κ m k j t) Lg (I.xFlowInv hΦ m (lIdx β I.Λ m k) t 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)
:
vecDiv (fun (y : Homogenization.Vec 2) => frozenCorrectorFlux I κ m k j t (I.xFlowInv hΦ m (lIdx β I.Λ m k) t y)) x = deriv (fun (s : ℝ) => I.chiMK κ m k s (I.xFlowInv hΦ m (lIdx β I.Λ m k) t x) j) t + vecDiv
(fun (y : Homogenization.Vec 2) =>
(1 - rowCofactor (gradMatrix (I.xFlowInv hΦ m (lIdx β I.Λ m k) t) y)).mulVec
(frozenCorrectorFlux I κ m k j t (I.xFlowInv hΦ m (lIdx β I.Λ m k) t y)))
x
Source corrector push-forward identity with its local corrector equation substituted. The remaining Piola divergence is explicit as in the flow bridge.
theorem
AVenhance.Infra.Section5.xFlowInv_corrector_pushforward_flowGrad
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(k : ℤ)
(t : ℝ)
(x : Homogenization.Vec 2)
(κ : ℝ)
(j : Fin 2)
{LM Lg : 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)
(hg : HasFDerivAt (frozenCorrectorFlux I κ m k j t) Lg (I.xFlowInv hΦ m (lIdx β I.Λ m k) t 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)
:
vecDiv (fun (y : Homogenization.Vec 2) => frozenCorrectorFlux I κ m k j t (I.xFlowInv hΦ m (lIdx β I.Λ m k) t y)) x = deriv (fun (s : ℝ) => I.chiMK κ m k s (I.xFlowInv hΦ m (lIdx β I.Λ m k) t x) j) t + vecDiv
(fun (y : Homogenization.Vec 2) =>
(1 - (I.flowGrad hΦ m (lIdx β I.Λ m k) t y).transpose).mulVec
(frozenCorrectorFlux I κ m k j t (I.xFlowInv hΦ m (lIdx β I.Λ m k) t y)))
x
Rewrite the cofactor correction in xFlowInv_corrector_pushforward using
the corrected transpose of the forward row-Jacobian.