Globally continuous extensions of a classical solution and its derivatives

Composing with t ↦ max t 0 gives continuous functions on all of ℝ × ℝ² that agree with the classical solution, its gradient and its time derivative on t ≥ 0. They give the regularity clauses of the weak-solution predicate.

def AVenhance.Infra.Section5.RelativeError.clExt (θ : ℝ → Homogenization.Vec 2 → ℝ) (p : ℝ × Homogenization.Vec 2) : ℝ

Extension of a classical solution by t ↦ max t 0.

Equations

• AVenhance.Infra.Section5.RelativeError.clExt θ p = θ (max p.1 0) p.2

noncomputable def AVenhance.Infra.Section5.RelativeError.clGradExt (θ : ℝ → Homogenization.Vec 2 → ℝ) (i : Fin 2) (p : ℝ × Homogenization.Vec 2) : ℝ

Extension of the spatial gradient components.

Equations

• AVenhance.Infra.Section5.RelativeError.clGradExt θ i p = (AVenhance.Infra.Section5.RelativeError.classicalJointFDeriv θ (max p.1 0, p.2)) (0, Homogenization.basisVec i)

noncomputable def AVenhance.Infra.Section5.RelativeError.clTimeExt (θ : ℝ → Homogenization.Vec 2 → ℝ) (p : ℝ × Homogenization.Vec 2) : ℝ

Extension of the time derivative.

Equations

• AVenhance.Infra.Section5.RelativeError.clTimeExt θ p = (AVenhance.Infra.Section5.RelativeError.classicalJointFDeriv θ (max p.1 0, p.2)) (1, 0)

theorem AVenhance.Infra.Section5.RelativeError.clMap_continuous : Continuous fun (p : ℝ × Homogenization.Vec 2) => (max p.1 0, p.2)

theorem AVenhance.Infra.Section5.RelativeError.clMap_mem (p : ℝ × Homogenization.Vec 2) : (max p.1 0, p.2) ∈ classicalHalfSpace

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

theorem AVenhance.Infra.Section5.RelativeError.clJoint_continuous {θ : ℝ → Homogenization.Vec 2 → ℝ} (hθ : ContDiffOn ℝ (↑⊤) (Function.uncurry θ) classicalHalfSpace) : Continuous fun (p : ℝ × Homogenization.Vec 2) => classicalJointFDeriv θ (max p.1 0, p.2)

theorem AVenhance.Infra.Section5.RelativeError.clGradExt_continuous {θ : ℝ → Homogenization.Vec 2 → ℝ} (hθ : ContDiffOn ℝ (↑⊤) (Function.uncurry θ) classicalHalfSpace) (i : Fin 2) : Continuous (clGradExt θ i)

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

theorem AVenhance.Infra.Section5.RelativeError.clExt_eq {θ : ℝ → Homogenization.Vec 2 → ℝ} {p : ℝ × Homogenization.Vec 2} (hp : 0 ≤ p.1) : clExt θ p = θ p.1 p.2

theorem AVenhance.Infra.Section5.RelativeError.clGradExt_eq {θ : ℝ → Homogenization.Vec 2 → ℝ} (hθ : ContDiffOn ℝ (↑⊤) (Function.uncurry θ) classicalHalfSpace) {p : ℝ × Homogenization.Vec 2} (hp : 0 ≤ p.1) (i : Fin 2) : clGradExt θ i p = spaceGrad (θ p.1) p.2 i

theorem AVenhance.Infra.Section5.RelativeError.clTimeExt_eq {θ : ℝ → Homogenization.Vec 2 → ℝ} (hθ : ContDiffOn ℝ (↑⊤) (Function.uncurry θ) classicalHalfSpace) {p : ℝ × Homogenization.Vec 2} (hp : 0 < p.1) : clTimeExt θ p = deriv (fun (s : ℝ) => θ s p.2) p.1