Source-specific finite telescope for the H_m potential.
theorem
AVenhance.Infra.Section5.frozen_Hm_material_equation
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(κ : ℝ)
(T : ℝ → Homogenization.Vec 2 → ℝ)
(t : ℝ)
(x : Homogenization.Vec 2)
(ht : 0 < t)
(Dt : ℕ → ℝ)
(LH : ℕ → Homogenization.Vec 2 →L[ℝ] ℝ)
(hDt : ∀ r ∈ Finset.range (Jcut β), HasDerivAt (fun (s : ℝ) => I.Hmr hΦ m κ T r s x) (Dt r) t)
(hDx : ∀ r ∈ Finset.range (Jcut β), HasFDerivAt (I.Hmr hΦ m κ T r t) (LH r) x)
(hb : ContDiff ℝ 2 fun (z : ST) => streamVel (Φ (m - 1)) z.1 z.2)
(hdiv : ∀ (z : ST), stDiv (fun (w : ST) => streamVel (Φ (m - 1)) w.1 w.2) z = 0)
(hA :
∀ r ∈ Finset.range (Jcut β),
∀ (n : ℕ) (i j k : Fin 2) (z : ST),
0 < z.1 → DifferentiableAt ℝ (fun (w : ST) => I.Amnr hΦ m κ n T 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 κ T r a) z)
(hFlux : ∀ r ∈ Finset.range (Jcut β), ContDiffAt ℝ 2 (amnrPairFluxSum I hΦ m (Nstar β) κ T r) (t, x))
(hEndNext :
∀ r ∈ Finset.range (Jcut β), DifferentiableAt ℝ (amnrPairEndpointFluxSum I hΦ m (Nstar β) κ T (r + 1)) (t, x))
(hEnd : ∀ r ∈ Finset.range (Jcut β), DifferentiableAt ℝ (amnrPairEndpointFluxSum I hΦ m (Nstar β) κ T r) (t, x))
:
The H_m material equation follows by telescoping the proved
per-index A/q steps. hDt and hDx state the time and spatial
differentiability used for the finite sum; all transport increments are
derived from and the primitive recursion for q.