The three remainder fields of e.grad.tildetheta.again: definitions and calculus

Source: enhance.tex 8112–8143 (and 8146–8170, the estimates). Writing Y = X⁻¹_{m-1,l_k}(t,·), A = ∇Y (x), C = ∇Χ_{m,k}(Y x) (gradMatrix convention: entry (i,j) = ∂_i χ_j), Fl = ∇X_{m-1,l_k}∘X⁻¹_{m-1,l_k} (x) (flowGrad) and g = ∇T_{m-1}(t,x), the three remainder vector fields are

• leadingErrFlowInv = ((A - 1) C) g — the second term of e.grad.tildetheta.again;
• leadingErrFlowFwd = (A C (Fl - 1)) g — the third term (∇ΧTilde = A C by the chain rule);
• leadingErrHessian — the fourth term ΧTilde · ∇(∇(T∘X)∘X⁻¹), expanded by the product and chain rules into ∑_j χ_j(Yx) ∑_p ( Fl_{jp} ∂_i∂_p T + (∑_q A_{iq} ∂_q∂_j X^p(Yx)) ∂_p T ).

This file contains the definitions, the smoothness of the objects, and the calculus lemmas (chain rule for ∇ΧTilde, entries of ∇G_{l_k}) used by the identity file.

noncomputable def AVenhance.Infra.Section5.RelativeError.xFlowHess {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (z : Homogenization.Vec 2) (p j q : Fin 2) : ℝ

The second spatial derivative ∂_q ∂_j X^p_{m-1,l}(t,·)(z) of the flow.

Equations

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

noncomputable def AVenhance.Infra.Section5.RelativeError.spaceHess (f : Homogenization.Vec 2 → ℝ) (x : Homogenization.Vec 2) (i p : Fin 2) : ℝ

The second spatial derivative ∂_i ∂_p f (x) of a scalar function.

Equations

• AVenhance.Infra.Section5.RelativeError.spaceHess f x i p = AVenhance.spaceGrad (fun (y : Homogenization.Vec 2) => AVenhance.spaceGrad f y p) x i

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

Second term of e.grad.tildetheta.again (before the factor ξ_{m,k} and the sum): (∇X⁻¹_{m-1,l_k} - I) (∇Χ_{m,k})∘X⁻¹_{m-1,l_k} ∇T_{m-1}.

Equations

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

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

Third term of e.grad.tildetheta.again (before the factor ξ_{m,k} and the sum): ∇ΧTilde_{m,k} ((∇X_{m-1,l_k})∘X⁻¹_{m-1,l_k} - I) ∇T_{m-1}, with the chain rule ∇ΧTilde_{m,k} = ∇X⁻¹_{m-1,l_k} · (∇Χ_{m,k})∘X⁻¹_{m-1,l_k} already expanded (see gradMatrix_chiTilde_eq).

Equations

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

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

Fourth term of e.grad.tildetheta.again (before the factor ξ_{m,k} and the sum), ΧTilde_{m,k} · ∇(∇(T_{m-1}∘X_{m-1,l_k})∘X⁻¹_{m-1,l_k}), expanded: component i is ∑_j χ_{m,k,j}(Yx) ∑_p ( Fl_{jp} ∂_i∂_p T + (∑_q (∇Y)_{iq} ∂_q∂_j X^p (Yx)) ∂_p T ).

Equations

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

Smoothness of the objects

theorem AVenhance.Infra.Section5.RelativeError.contDiff_chiMK {β : ℝ} (I : Ingredients β) (κm : ℝ) (m : ℕ) (k : ℤ) (t : ℝ) : ContDiff ℝ (↑⊤) (I.chiMK κm m k t)

theorem AVenhance.Infra.Section5.RelativeError.contDiff_xFlowInv_slice {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) : ContDiff ℝ (↑⊤) (I.xFlowInv hΦ m l t)

theorem AVenhance.Infra.Section5.RelativeError.contDiff_xFlow_slice {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) : ContDiff ℝ (↑⊤) (I.xFlow hΦ m l t)

theorem AVenhance.Infra.Section5.RelativeError.xFlow_xFlowInv {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (x : Homogenization.Vec 2) : I.xFlow hΦ m l t (I.xFlowInv hΦ m l t x) = x

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

theorem AVenhance.Infra.Section5.RelativeError.contDiff_G {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) (l : ℤ) {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) : ContDiff ℝ ↑⊤ fun (y : Homogenization.Vec 2) => G I hΦ m T l t y

theorem AVenhance.Infra.Section5.RelativeError.chiMK_eq_zero_of_not_odd {β : ℝ} (I : Ingredients β) (κ : ℝ) (m : ℕ) {k : ℤ} (hk : ¬Odd k) (t : ℝ) : I.chiMK κ m k t = 0

The corrector Χ_{m,k} vanishes for even k (uShear = 0).

Elementary spaceGrad calculus

theorem AVenhance.Infra.Section5.RelativeError.spaceGrad_mul_of_differentiableAt {f g : Homogenization.Vec 2 → ℝ} {x : Homogenization.Vec 2} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) (i : Fin 2) : spaceGrad (fun (y : Homogenization.Vec 2) => f y * g y) x i = f x * spaceGrad g x i + g x * spaceGrad f x i

theorem AVenhance.Infra.Section5.RelativeError.spaceGrad_sum_univ_of_differentiableAt {f : Fin 2 → Homogenization.Vec 2 → ℝ} {x : Homogenization.Vec 2} (h : ∀ (p : Fin 2), DifferentiableAt ℝ (f p) x) (i : Fin 2) : spaceGrad (fun (y : Homogenization.Vec 2) => ∑ p : Fin 2, f p y) x i = ∑ p : Fin 2, spaceGrad (f p) x i

theorem AVenhance.Infra.Section5.RelativeError.gradMatrix_chiTilde_eq {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) : gradMatrix (I.chiTilde hΦ m κm k t) x = 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)

Chain rule ∇ΧTilde_{m,k} = ∇X⁻¹_{m-1,l_k} · (∇Χ_{m,k})∘X⁻¹_{m-1,l_k}.

theorem AVenhance.Infra.Section5.RelativeError.spaceGrad_G_component {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) (l : ℤ) {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) (x : Homogenization.Vec 2) (i j : Fin 2) : spaceGrad (fun (y : Homogenization.Vec 2) => G I hΦ m T l t y j) x i = ∑ p : Fin 2, (I.flowGrad hΦ m l t x j p * spaceHess (T t) x i p + (∑ q : Fin 2, gradMatrix (fun (z : Homogenization.Vec 2) => I.xFlowInv hΦ m l t z) x i q * xFlowHess I hΦ m l t (I.xFlowInv hΦ m l t x) p j q) * spaceGrad (T t) x p)

The product/chain-rule expansion of the entries of ∇G_{l}.