: the source material equation for the names.
This is frozen_source_material_equation with the two corrected-form inputs switched in:
the coarse coefficient (I.sMat = sMatPlus) and the base tensor
(I.Amnr · 0 = amnrBasePlus); both are rfl (sMat_eq_sMatPlus,
Amnr_zero_eq_amnrBasePlus). The conclusion is the transport equation with the Piola flux V_tr
(transportFluxPlus) and the corrected-form forcing error d⁺ (sourceErrorDPlus).
theorem
AVenhance.Infra.Section5.LeftJacobian.variantA_source_material_equation
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(hm : 1 ≤ m)
(κm κprev : ℝ)
(θ₀ : Homogenization.Vec 2 → ℝ)
(θprev : ℝ → Homogenization.Vec 2 → ℝ)
(T : ℕ → ℝ → Homogenization.Vec 2 → ℝ)
(hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T)
(t : ℝ)
(ht : 0 < t)
(x : Homogenization.Vec 2)
(Dt : ℕ → ℝ)
(LH : ℕ → Homogenization.Vec 2 →L[ℝ] ℝ)
(hDt : ∀ r ∈ Finset.range (Jcut β), HasDerivAt (fun (s : ℝ) => I.Hmr hΦ m κm (T (Nstar β)) r s x) (Dt r) t)
(hDx : ∀ r ∈ Finset.range (Jcut β), HasFDerivAt (I.Hmr hΦ m κm (T (Nstar β)) r t) (LH r) x)
(hA :
∀ r ∈ Finset.range (Jcut β),
∀ (n : ℕ) (i j k : Fin 2) (z : ST),
0 < z.1 → DifferentiableAt ℝ (fun (w : ST) => I.Amnr hΦ m κm n (T (Nstar β)) r w.1 w.2 i j k) z)
(hPair :
∀ r ∈ Finset.range (Jcut β),
∀ (a : AmnrPairIndex) (z : ST), 0 < z.1 → DifferentiableAt ℝ (amnrPairFlux I hΦ m κm (T (Nstar β)) r a) z)
(hFlux : ∀ r ∈ Finset.range (Jcut β), ContDiffAt ℝ 2 (amnrPairFluxSum I hΦ m (Nstar β) κm (T (Nstar β)) r) (t, x))
(hEndNext :
∀ r ∈ Finset.range (Jcut β),
DifferentiableAt ℝ (amnrPairEndpointFluxSum I hΦ m (Nstar β) κm (T (Nstar β)) (r + 1)) (t, x))
(hEnd :
∀ r ∈ Finset.range (Jcut β), DifferentiableAt ℝ (amnrPairEndpointFluxSum I hΦ m (Nstar β) κm (T (Nstar β)) r) (t, x))
(hAvg :
DifferentiableAt ℝ
(fun (y : Homogenization.Vec 2) =>
(I.Kmat κm m t + sMatPlus I hΦ m κm t y).mulVec (spaceGrad (T (Nstar β) t) y) + iterateError I hΦ m κm κprev T t y)
x)
(hTail : DifferentiableAt ℝ (terminalTail I hΦ m κm (T (Nstar β)) t) x)
(hBase :
DifferentiableAt ℝ
(fun (y : Homogenization.Vec 2) =>
∑' (l : ℤ), I.hatXiML m l t • (I.flowGrad hΦ m l t y).transpose.mulVec
((I.Jhat κm m t - I.Kmat κm m t).mulVec ((I.flowGrad hΦ m l t y).mulVec (spaceGrad (T (Nstar β) t) y))))
x)
:
deriv (fun (s : ℝ) => T (Nstar β) s x) t + Homogenization.vecDot (streamVel (Φ (m - 1)) t x) (spaceGrad (T (Nstar β) t) x) + deriv (fun (s : ℝ) => I.Hm hΦ m κm (T (Nstar β)) s x) t + (fderiv ℝ (I.Hm hΦ m κm (T (Nstar β)) t) x) (streamVel (Φ (m - 1)) t x) = vecDiv
(fun (y : Homogenization.Vec 2) =>
transportFluxPlus I hΦ m κm (T (Nstar β)) t y + sourceErrorDPlus I hΦ m κm (T (Nstar β)) t y + iterateError I hΦ m κm κprev T t y)
x
corrected-form source material equation for the T, H_m.
Regularity hypotheses (the analogues of hAvg, hTail, hGap of
frozen_source_material_equation; each is the differentiability at x of one of the three
vector fields whose divergence is split):