Actual Hm bound from its endpoint-difference L2 source on positive time. The source estimate uses the terminal one-letter budget from EndpointPhysical.
theorem
AVenhance.Infra.Section5.RelativeError.relative_initial_Hm_backward_of_source_L2
{β : ℝ}
(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)
{B : ℝ}
(hB : 0 ≤ B)
(hcell : tauPP β I.Λ m / 2 < 1)
(hsource :
MeasureTheory.eLpNorm
(fun (z : ℝ × Homogenization.Vec 2) =>
hmEndpoint I hΦ m κm (T (Nstar β)) (Jcut β) z.1 z.2 - hmEndpoint I hΦ m κm (T (Nstar β)) 0 z.1 z.2)
2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal B)
(t : ℝ)
:
A genuine spacetime L2 source bound gives uniform Hm control on the first positive half-cell. No source norm at any particular time is assumed.