Joint continuity of the three remainder fields of e.grad.tildetheta.again #
For T jointly C^∞ on [0,∞) × ℝ², the fields leadingErrFlowInv, leadingErrFlowFwd,
leadingErrHessian (LeadingErrorAlgebraDefs) are jointly continuous on Ici 0 ×ˢ univ. Every
ingredient (entries of ∇X^{±1}, ∇X∘X⁻¹, ∂²X∘X⁻¹, Χ∘X⁻¹, ∇Χ∘X⁻¹) is continuous on all
of ℝ × ℝ²; only the derivatives of T need the set Ici 0 ×ˢ univ.
Flow ingredients (continuous on all of ℝ × ℝ²) #
theorem
AVenhance.Infra.Section5.RelativeError.contDiffOn_spaceGrad_joint
{T : ℝ → Homogenization.Vec 2 → ℝ}
(hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ))
(p : Fin 2)
:
ContDiffOn ℝ (↑⊤) (fun (r : ℝ × Homogenization.Vec 2) => spaceGrad (T r.1) r.2 p) (Set.Ici 0 ×ˢ Set.univ)
The spatial derivative ∂_p T is C^∞ on Ici 0 ×ˢ univ.
theorem
AVenhance.Infra.Section5.RelativeError.continuousOn_spaceGrad_joint
{T : ℝ → Homogenization.Vec 2 → ℝ}
(hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ))
(p : Fin 2)
:
ContinuousOn (fun (r : ℝ × Homogenization.Vec 2) => spaceGrad (T r.1) r.2 p) (Set.Ici 0 ×ˢ Set.univ)
theorem
AVenhance.Infra.Section5.RelativeError.continuousOn_spaceHess_joint
{T : ℝ → Homogenization.Vec 2 → ℝ}
(hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ))
(i p : Fin 2)
:
ContinuousOn (fun (r : ℝ × Homogenization.Vec 2) => spaceHess (T r.1) r.2 i p) (Set.Ici 0 ×ˢ Set.univ)