Forced classical energy with relative initial defect and residual, on open time.
The comparison field v (the ansatz) is only required to be regular for t > 0, and the
initial defect is taken from the right (s → 0⁺, Integration.InitialLayerContract): the
ansatz at t = 0 reads the negative-time extension of T through the two-sided time derivative of
Amnr, so v 0 is not a meaningful datum. The energy estimate is
Integration.forced_energy_estimate_Ioi.
theorem
AVenhance.Infra.Section5.RelativeError.relative_forced_energy_estimate
{φ : ℝ → Homogenization.Vec 2 → ℝ}
(hφ : IsAdmissibleStream φ)
{κ : ℝ}
(hκ : 0 < κ)
{g : Homogenization.Vec 2 → ℝ}
{u v : ℝ → Homogenization.Vec 2 → ℝ}
(hu : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g u)
(hv : ContDiffOn ℝ 2 (fun (p : ℝ × Homogenization.Vec 2) => v p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ))
(hvs : ∀ (t : ℝ), 0 < t → ContDiff ℝ (↑⊤) (v t))
(hvp : ∀ (t : ℝ), 0 < t → IsZ2Periodic (v t))
{Ci Cr ε δ S : ℝ}
(hCr : 0 ≤ Cr)
(hε : 0 < ε)
(hS : 0 ≤ S)
(hInitial :
∀ᶠ (s : ℝ) in nhdsWithin 0 (Set.Ioi 0), √(l2NormSq fun (x : Homogenization.Vec 2) => u s x - v s x) ≤ Ci * ε ^ δ * S)
(hResidual :
(timeHMinusOneNorm fun (s : ℝ) (x : Homogenization.Vec 2) => advDiffOp (streamVel φ) κ v s x) ≤ ENNReal.ofReal (Cr * √κ * ε ^ δ * S))
(t : ℝ)
:
theorem
AVenhance.Infra.Section5.RelativeError.relative_ansatz_error
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
{κ : ℝ}
(hκ : 0 < κ)
{g : Homogenization.Vec 2 → ℝ}
{u T : ℝ → Homogenization.Vec 2 → ℝ}
(hu : IsClassicalSol (streamVel (Φ m)) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g u)
(hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ))
(hTs : ∀ (t : ℝ), 0 ≤ t → ContDiff ℝ (↑⊤) (T t))
(hTp : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (T t))
(hH : ContDiffOn ℝ 2 (fun (p : ℝ × Homogenization.Vec 2) => I.Hm hΦ m κ T p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ))
(hHs : ∀ (t : ℝ), 0 < t → ContDiff ℝ (↑⊤) (I.Hm hΦ m κ T t))
(hHp : ∀ (t : ℝ), 0 < t → IsZ2Periodic (I.Hm hΦ m κ T t))
{Ci Cr ε δ S : ℝ}
(hCr : 0 ≤ Cr)
(hε : 0 < ε)
(hS : 0 ≤ S)
(hInitial :
∀ᶠ (s : ℝ) in nhdsWithin 0 (Set.Ioi 0), √(l2NormSq fun (x : Homogenization.Vec 2) => u s x - I.ansatz hΦ m κ T s x) ≤ Ci * ε ^ δ * S)
(hResidual :
(timeHMinusOneNorm fun (s : ℝ) (x : Homogenization.Vec 2) => advDiffOp (streamVel (Φ m)) κ (I.ansatz hΦ m κ T) s x) ≤ ENNReal.ofReal (Cr * √κ * ε ^ δ * S))
(t : ℝ)
:
Actual ansatz specialization, with joint and slice regularity of the ansatz discharged on
(0,∞) × ℝ² by the existing ansatz lemmas from regularity of T (up to t = 0) and of HTilde_m
(for t > 0 only).