The comparison's initial defect is measured from the right against the actual datum. No value or regularity of the comparison at zero is consumed.

theorem AVenhance.Infra.Section5.RelativeError.relative_classical_initial_L2_tendsto {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {g : Homogenization.Vec 2 → ℝ} {u f : ℝ → Homogenization.Vec 2 → ℝ} (hu : IsClassicalSol b κ f g u) : Filter.Tendsto (fun (s : ℝ) => √(l2NormSq fun (x : Homogenization.Vec 2) => u s x - g x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

A classical solution approaches its actual datum in L2 from the right.