Exact decomposition of ∇θTilde_m - F ∇T_{m-1} (e.grad.tildetheta.again, 8112–8143)

Source: enhance.tex 8112–8170. At a fixed time t and position x, for T with smooth slice T t and HTilde_m(t) differentiable at x, ∇θTilde_m - F ∇T_{m-1} = ∑_{k odd} ξ_{m,k} (E¹_k + E²_k + E³_k) + ∇HTilde_m, where E¹, E², E³ are leadingErrFlowInv, leadingErrFlowFwd, leadingErrHessian (LeadingErrorAlgebraDefs), the finite sum running over the odd support of ξ_{m,·}(t). The joint continuity of each field on Ici 0 ×ˢ univ is in LeadingErrorAlgebraContinuity (imported here, so this module is the single entry point).

The identity part of F is handled by the partition of unity ∑_{k odd} ξ_{m,k} = 1 (leadingMatrix_eq_finset).

theorem AVenhance.Infra.Section5.RelativeError.mulVec_split_flow (A C Fl : Matrix (Fin 2) (Fin 2) ℝ) (g : Homogenization.Vec 2) : (A * C).mulVec (Fl.mulVec g) - C.mulVec g = ((A - 1) * C).mulVec g + (A * C * (Fl - 1)).mulVec g

Matrix identity behind the second and third terms.

noncomputable def AVenhance.Infra.Section5.RelativeError.ansatzPairing {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (k : ℤ) (t : ℝ) (y : Homogenization.Vec 2) : ℝ

The k-th pairing ΧTilde_{m,k} · G_{l_k} of the ansatz.

Equations

• AVenhance.Infra.Section5.RelativeError.ansatzPairing I hΦ m κm T k t y = Homogenization.vecDot (I.chiTilde hΦ m κm k t y) (AVenhance.Infra.Section5.G I hΦ m T (AVenhance.lIdx β I.Λ m k) t y)

theorem AVenhance.Infra.Section5.RelativeError.contDiff_ansatzPairing {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (k : ℤ) {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) : ContDiff ℝ (↑⊤) (ansatzPairing I hΦ m κm T k t)

theorem AVenhance.Infra.Section5.RelativeError.spaceGrad_ansatzPairing {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (k : ℤ) {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) (x : Homogenization.Vec 2) (i : Fin 2) : spaceGrad (ansatzPairing I hΦ m κm T k t) x i = (gradMatrix (fun (z : Homogenization.Vec 2) => I.xFlowInv hΦ m (lIdx β I.Λ m k) t z) x * gradMatrix (I.chiMK κm m k t) (I.xFlowInv hΦ m (lIdx β I.Λ m k) t x)).mulVec ((I.flowGrad hΦ m (lIdx β I.Λ m k) t x).mulVec (spaceGrad (T t) x)) i + leadingErrHessian I hΦ m κm T k t x i

Gradient of the k-th pairing: the (∇ΧTilde) G part and the Hessian part.

theorem AVenhance.Infra.Section5.RelativeError.ansatz_eq_finset_sum {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) : I.ansatz hΦ m κm T t = fun (y : Homogenization.Vec 2) => T t y + ∑ q ∈ ⋯.toFinset, I.xiMK m (↑q) t * ansatzPairing I hΦ m κm T (↑q) t y + I.Hm hΦ m κm T t y

The ansatz as a finite sum over the odd support of ξ_{m,·}(t).

theorem AVenhance.Infra.Section5.RelativeError.ansatz_spaceGrad_sub_leadingGrad {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κm : ℝ) {T : ℝ → Homogenization.Vec 2 → ℝ} {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) (x : Homogenization.Vec 2) (hHt : DifferentiableAt ℝ (I.Hm hΦ m κm T t) x) : spaceGrad (I.ansatz hΦ m κm T t) x - LeftToShow.leadingGrad I hΦ m κm T t x = ∑ k ∈ ⋯.toFinset, I.xiMK m (↑k) t • (leadingErrFlowInv I hΦ m κm T (↑k) t x + leadingErrFlowFwd I hΦ m κm T (↑k) t x + leadingErrHessian I hΦ m κm T (↑k) t x) + spaceGrad (I.Hm hΦ m κm T t) x

Exact decomposition of ∇θTilde_m - F ∇T_{m-1} (e.grad.tildetheta.again).