The oscillatory corrector has a legitimate right trace. Combining this trace with a positive-time Hm bound supplies the relative initial leaf.
theorem
AVenhance.Infra.Section5.RelativeError.relative_initial_defect_from_right_Hm_bound
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
{κ ν : ℝ}
(hκ : 0 < κ)
{g : Homogenization.Vec 2 → ℝ}
{θprev : ℝ → Homogenization.Vec 2 → ℝ}
{T : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hp : IsClassicalSol (streamVel (Φ (m - 1))) ν (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θprev)
(hT : I.IsTIterates hΦ m κ ν g θprev T)
{B D : ℝ}
(hCorrector :
√(l2NormSq fun (x : Homogenization.Vec 2) => ∑' (k : ℤ), Integration.ansatzSummand I hΦ m κ (T (Nstar β)) k 0 x) ≤ B)
(hHm : ∀ᶠ (s : ℝ) in nhdsWithin 0 (Set.Ioi 0), √(l2NormSq (I.Hm hΦ m κ (T (Nstar β)) s)) ≤ D)
(η : ℝ)
:
Conditional assembly of the right-limit defect. The Hm hypothesis is an eventual positive-time bound, and no Hm value at zero appears.