Pointwise regularity consequences of the classical-solution definition on the open positive-time region.

theorem AVenhance.Infra.Section5.classicalSol_contDiffAt_of_pos {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F : ℝ → Homogenization.Vec 2 → ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol b κ F θ₀ θ) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) : ContDiffAt ℝ (↑⊤) (Function.uncurry θ) (t, x)

A classical solution is jointly smooth at every positive-time space-time point. The boundary value at time zero is not used.

theorem AVenhance.Infra.Section5.classicalSol_hasFDerivAt_of_pos {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F : ℝ → Homogenization.Vec 2 → ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol b κ F θ₀ θ) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) : HasFDerivAt (Function.uncurry θ) (fderiv ℝ (Function.uncurry θ) (t, x)) (t, x)

The spacetime Fréchet derivative of a classical solution exists at each point with positive time.

theorem AVenhance.Infra.Section5.classicalSol_space_contDiff_of_nonneg {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F : ℝ → Homogenization.Vec 2 → ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol b κ F θ₀ θ) {t : ℝ} (ht : 0 ≤ t) : ContDiff ℝ (↑⊤) (θ t)

At each nonnegative time, the spatial slice of a classical solution is globally smooth.

theorem AVenhance.Infra.Section5.classicalSol_spaceGrad_contDiff_of_nonneg {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F : ℝ → Homogenization.Vec 2 → ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol b κ F θ₀ θ) {t : ℝ} (ht : 0 ≤ t) : ContDiff ℝ (↑⊤) (spaceGrad (θ t))

The spatial gradient of a classical solution is itself smooth on every nonnegative time slice.

theorem AVenhance.Infra.Section5.classicalSol_space_hasFDerivAt_of_pos {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F : ℝ → Homogenization.Vec 2 → ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol b κ F θ₀ θ) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) : HasFDerivAt (θ t) (fderiv ℝ (Function.uncurry θ) (t, x) ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Homogenization.Vec 2))) x

The spatial slice of a classical solution is Fréchet differentiable at every positive-time point.

theorem AVenhance.Infra.Section5.classicalSol_spaceGrad_eq_jointFDeriv_eventually {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F : ℝ → Homogenization.Vec 2 → ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol b κ F θ₀ θ) {t : ℝ} (ht : 0 < t) (γ : ℝ → Homogenization.Vec 2) (i : Fin 2) : (fun (r : ℝ) => spaceGrad (θ r) (γ r) i) =ᶠ[nhds t] fun (r : ℝ) => (fderiv ℝ (Function.uncurry θ) (r, γ r)) (0, Homogenization.basisVec i)

Along any spatial curve, a positive-time slice gradient agrees locally with the spatial restriction of the spacetime derivative.