Spatial derivatives of a classical solution remain smooth and continuous down to the initial time. The derivatives are taken within the closed nonnegative-time half-space, so their boundary values are the derivatives of the initial trace.

def AVenhance.Infra.Section4.ThetaTimeSpatialTrace.thetaNonnegativeJointDomain : Set (ℝ × Homogenization.Vec 2)

Joint time-space domain with nonnegative time, including the initial trace.

Equations

• AVenhance.Infra.Section4.ThetaTimeSpatialTrace.thetaNonnegativeJointDomain = Set.Ici 0 ×ˢ Set.univ

theorem AVenhance.Infra.Section4.ThetaTimeSpatialTrace.thetaNonnegativeJointDomain_uniqueDiff : UniqueDiffOn ℝ thetaNonnegativeJointDomain

def AVenhance.Infra.Section4.ThetaTimeSpatialTrace.thetaSpatialDirection (i : Fin 2) : ℝ × Homogenization.Vec 2

Spatial coordinate direction embedded in the joint temperature domain.

Equations

• AVenhance.Infra.Section4.ThetaTimeSpatialTrace.thetaSpatialDirection i = (0, Homogenization.basisVec i)

def AVenhance.Infra.Section4.ThetaTimeSpatialTrace.thetaJointWordDerivativeWithin : List (Fin 2) → (ℝ × Homogenization.Vec 2 → ℝ) → ℝ × Homogenization.Vec 2 → ℝ

Iterate spatial directional derivatives within the nonnegative-time domain.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.Infra.Section4.ThetaTimeSpatialTrace.thetaJointWordDerivativeWithin [] x✝ = x✝

theorem AVenhance.Infra.Section4.ThetaTimeSpatialTrace.thetaJointWordDerivativeWithin_contDiffOn {f : ℝ × Homogenization.Vec 2 → ℝ} (hf : ContDiffOn ℝ (↑⊤) f thetaNonnegativeJointDomain) (w : List (Fin 2)) : ContDiffOn ℝ (↑⊤) (thetaJointWordDerivativeWithin w f) thetaNonnegativeJointDomain

theorem AVenhance.Infra.Section4.ThetaTimeSpatialTrace.thetaJointWordDerivativeWithin_eq_slice {f : ℝ × Homogenization.Vec 2 → ℝ} (hf : ContDiffOn ℝ (↑⊤) f thetaNonnegativeJointDomain) (w : List (Fin 2)) (t : ℝ) : 0 ≤ t → ∀ (x : Homogenization.Vec 2), thetaJointWordDerivativeWithin w f (t, x) = classicalWordDerivative w (fun (y : Homogenization.Vec 2) => f (t, y)) x

theorem AVenhance.Infra.Section4.theta_classical_word_joint_contDiffOn_nonneg {θ : ℝ → Homogenization.Vec 2 → ℝ} (hθ : ContDiffOn ℝ (↑⊤) (Function.uncurry θ) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => classicalWordDerivative w (θ p.1) p.2) (Set.Ici 0 ×ˢ Set.univ)

theorem AVenhance.Infra.Section4.theta_classical_word_slice_contDiff_nonneg {θ : ℝ → Homogenization.Vec 2 → ℝ} (hθ : ContDiffOn ℝ (↑⊤) (Function.uncurry θ) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) (t : ℝ) : 0 ≤ t → ContDiff ℝ (↑⊤) (classicalWordDerivative w (θ t))