Joint regularity of a classical solution up to time zero

A classical solution is smooth on the closed half-space t ≥ 0. Its space-time derivative (taken inside the half-space) is continuous up to t = 0, and its spatial gradient and time derivative are the corresponding components of that joint derivative.

def AVenhance.Infra.Section5.RelativeError.classicalHalfSpace : Set (ℝ × Homogenization.Vec 2)

The closed half-space t ≥ 0.

Equations

• AVenhance.Infra.Section5.RelativeError.classicalHalfSpace = Set.Ici 0 ×ˢ Set.univ

theorem AVenhance.Infra.Section5.RelativeError.classicalHalfSpace_uniqueDiffOn : UniqueDiffOn ℝ classicalHalfSpace

noncomputable def AVenhance.Infra.Section5.RelativeError.classicalJointFDeriv (θ : ℝ → Homogenization.Vec 2 → ℝ) : ℝ × Homogenization.Vec 2 → ℝ × Homogenization.Vec 2 →L[ℝ] ℝ

The joint derivative of a classical solution inside the closed half-space.

Equations

• AVenhance.Infra.Section5.RelativeError.classicalJointFDeriv θ = fderivWithin ℝ (Function.uncurry θ) AVenhance.Infra.Section5.RelativeError.classicalHalfSpace

theorem AVenhance.Infra.Section5.RelativeError.classicalJointFDeriv_continuousOn {θ : ℝ → Homogenization.Vec 2 → ℝ} (hθ : ContDiffOn ℝ (↑⊤) (Function.uncurry θ) classicalHalfSpace) : ContinuousOn (classicalJointFDeriv θ) classicalHalfSpace

theorem AVenhance.Infra.Section5.RelativeError.classicalHasFDerivWithinAt {θ : ℝ → Homogenization.Vec 2 → ℝ} (hθ : ContDiffOn ℝ (↑⊤) (Function.uncurry θ) classicalHalfSpace) {t : ℝ} (ht : 0 ≤ t) (x : Homogenization.Vec 2) : HasFDerivWithinAt (Function.uncurry θ) (classicalJointFDeriv θ (t, x)) classicalHalfSpace (t, x)

theorem AVenhance.Infra.Section5.RelativeError.classical_spaceGrad_eq_joint {θ : ℝ → Homogenization.Vec 2 → ℝ} (hθ : ContDiffOn ℝ (↑⊤) (Function.uncurry θ) classicalHalfSpace) {t : ℝ} (ht : 0 ≤ t) (x : Homogenization.Vec 2) (i : Fin 2) : spaceGrad (θ t) x i = (classicalJointFDeriv θ (t, x)) (0, Homogenization.basisVec i)

The spatial gradient of a classical solution is a component of the joint derivative.

theorem AVenhance.Infra.Section5.RelativeError.classical_deriv_eq_joint {θ : ℝ → Homogenization.Vec 2 → ℝ} (hθ : ContDiffOn ℝ (↑⊤) (Function.uncurry θ) classicalHalfSpace) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) : HasDerivAt (fun (s : ℝ) => θ s x) ((classicalJointFDeriv θ (t, x)) (1, 0)) t

The time derivative of a classical solution is a component of the joint derivative.