The relative energy comparison with an open-time ansatz gradient

relative_step_from_errors asks for joint continuity of ∇θTilde_m on [0,∞) × ℝ². The ansatz is extension-dependent at t = 0 (two-sided time derivative in Amnr), so relative_step_from_errors_Ioi only asks that ∇θTilde_m agree on (0,∞) × ℝ² with some field continuous on [0,∞) × ℝ² (OpenTimeExtends). Since spaceTimeGradNormSq integrates over timeCube ⊆ (0,∞) × ℝ², every norm is unchanged by passing to the extension, which supplies the square integrability the L² triangle inequalities need.

def AVenhance.Infra.Section5.RelativeError.OpenTimeExtends (f : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : Prop

f agrees on the open half space with a field continuous on the closed half space.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Section5.RelativeError.OpenTimeExtends.of_continuousOn {f : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hf : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => f p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) : OpenTimeExtends f

theorem AVenhance.Infra.Section5.RelativeError.spaceTimeGradNormSq_congr_Ioi {f g : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (h : ∀ p ∈ Set.Ioi 0 ×ˢ Set.univ, f p.1 p.2 = g p.1 p.2) : spaceTimeGradNormSq f = spaceTimeGradNormSq g

spaceTimeGradNormSq only sees timeCube ⊆ (0,∞) × ℝ².

theorem AVenhance.Infra.Section5.RelativeError.relative_gradient_norm_sub_le_of_extends {f g : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hf : OpenTimeExtends f) (hg : OpenTimeExtends g) : |√(spaceTimeGradNormSq f) - √(spaceTimeGradNormSq g)| ≤ √(spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => f t x - g t x)

theorem AVenhance.Infra.Section5.RelativeError.relative_step_from_errors_Ioi (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 : OpenTimeExtends fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (I.ansatz hΦ m (I.kappaSeq κ M m) T s) x) (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)