Relative energy comparison in the actual gradient carriers. This is a conditional assembly helper, not a proof of the step-down estimate statement.
theorem
AVenhance.Infra.Section5.RelativeError.relative_step_from_errors
(Cans Clead CT Cenergy : ℝ)
(hCans : 0 ≤ Cans)
(hClead : 0 ≤ Clead)
(hCT : 0 ≤ CT)
(hCenergy : 0 ≤ Cenergy)
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m M : ℕ)
(κ : ℝ)
(θm θprev T : ℝ → Homogenization.Vec 2 → ℝ)
(hκm : 0 ≤ I.kappaSeq κ M m)
(hν : 0 ≤ I.kappaSeq κ M (m - 1))
{e : ℝ}
(he : 0 ≤ e)
(he1 : e ≤ 1)
(hθ : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => spaceGrad (θm p.1) p.2) (Set.Ici 0 ×ˢ Set.univ))
(hAns :
∀ (i : Fin 2),
MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => spaceGrad (I.ansatz hΦ m (I.kappaSeq κ M m) T p.1) p.2 i)
2 (MeasureTheory.volume.restrict timeCube))
(hLead :
ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => LeftToShow.leadingGrad I hΦ m (I.kappaSeq κ M m) T p.1 p.2)
(Set.Ici 0 ×ˢ Set.univ))
(hT : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => spaceGrad (T p.1) p.2) (Set.Ici 0 ×ˢ Set.univ))
(hPrev : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => spaceGrad (θprev p.1) p.2) (Set.Ici 0 ×ˢ Set.univ))
(hAnsatzError :
√(I.kappaSeq κ M m) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) =>
spaceGrad (θm s) x - spaceGrad (I.ansatz hΦ m (I.kappaSeq κ M m) T s) x) ≤ Cans * e * (√(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x)))
(hLeadingError :
√(I.kappaSeq κ M m) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) =>
spaceGrad (I.ansatz hΦ m (I.kappaSeq κ M m) T s) x - LeftToShow.leadingGrad I hΦ m (I.kappaSeq κ M m) T s x) ≤ Clead * e ^ 2 * (√(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x)))
(hTemperatureError :
√(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (T s) x - spaceGrad (θprev s) x) ≤ CT * e ^ 2 * (√(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x)))
(hLeadingEnergy :
|I.kappaSeq κ M m * spaceTimeGradNormSq (LeftToShow.leadingGrad I hΦ m (I.kappaSeq κ M m) T) - I.kappaSeq κ M (m - 1) * spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (T s) x| ≤ Cenergy * e ^ 2 * (I.kappaSeq κ M (m - 1) * spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x))
:
|(I.kappaSeq κ M m * spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θm s) x) - I.kappaSeq κ M (m - 1) * spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x| ≤ (Cans + Clead + CT + √Cenergy) * (2 + (Cans + Clead + CT + √Cenergy)) * e * (I.kappaSeq κ M (m - 1) * spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x)