Backward transport for the actual Hm on the first positive half-cell. The quantitative source primitive is separate from the proved calculus.
theorem
AVenhance.Infra.Section5.RelativeError.relative_initial_Hm_backward_of_source_integral
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
{κm κprev : ℝ}
(hκm : 0 < κm)
{g : Homogenization.Vec 2 → ℝ}
{θprev : ℝ → Homogenization.Vec 2 → ℝ}
{T : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θprev)
(hT : I.IsTIterates hΦ m κm κprev g θprev T)
{D : ℝ}
(hD : 0 ≤ D)
(hsource :
∀ t ∈ Set.Ioc 0 (tauPP β I.Λ m / 2),
∫ (s : ℝ) in t..tauPP β I.Λ m / 2, √(l2NormSq fun (x : Homogenization.Vec 2) =>
hmEndpoint I hΦ m κm (T (Nstar β)) (Jcut β) s x - hmEndpoint I hΦ m κm (T (Nstar β)) 0 s x) ≤ D)
(t : ℝ)
:
Actual positive-time Hm is controlled by the integrated endpoint source. All flow, periodicity, continuity and material-equation premises are discharged.