The actual classical temperature equation in the ordered mixed calculus.

theorem AVenhance.Infra.Section4.amnr_classical_smooth {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F : ℝ → Homogenization.Vec 2 → ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : IsClassicalSol b κ F θ₀ u) : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ioi 0 ×ˢ Set.univ)

Smoothness on the open positive-time domain follows from the classical-solution definition, including every finite derivative order.

theorem AVenhance.Infra.Section4.amnr_classical_material {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F : ℝ → Homogenization.Vec 2 → ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : IsClassicalSol b κ F θ₀ u) {z : AmnrSpace} (ht : 0 < z.1) : amnrOp (fun (y : AmnrSpace) => b y.1 y.2) none (fun (y : AmnrSpace) => u y.1 y.2) z = κ * spaceLap (u z.1) z.2 + F z.1 z.2

The PDE gives the material derivative itself, without a material regularity assumption on the temperature.

theorem AVenhance.Infra.Section4.amnr_classical_gradient_smooth {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F : ℝ → Homogenization.Vec 2 → ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : IsClassicalSol b κ F θ₀ u) (p : Fin 2) (N : ℕ) : ContDiffOn ℝ (↑N) (fun (z : AmnrSpace) => spaceGrad (u z.1) z.2 p) (Set.Ioi 0 ×ˢ Set.univ)

Actual temperature gradients have every finite order of joint regularity; this is proved from classical smoothness rather than supplied to the AMNR seed.

theorem AVenhance.Infra.Section4.amnr_classical_gradient_evolution {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F : ℝ → Homogenization.Vec 2 → ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : IsClassicalSol b κ F θ₀ u) {z : AmnrSpace} (ht : 0 < z.1) (hb : DifferentiableAt ℝ (fun (y : AmnrSpace) => b y.1 y.2) z) (i : Fin 2) : amnrOp (fun (y : AmnrSpace) => b y.1 y.2) none (amnrOp (fun (y : AmnrSpace) => b y.1 y.2) (some i) fun (y : AmnrSpace) => u y.1 y.2) z = amnrOp (fun (y : AmnrSpace) => b y.1 y.2) (some i) (fun (y : AmnrSpace) => κ * spaceLap (u y.1) y.2 + F y.1 y.2) z - ∑ p : Fin 2, amnrVelocityGradient (fun (y : AmnrSpace) => b y.1 y.2) p i z * amnrOp (fun (y : AmnrSpace) => b y.1 y.2) (some p) (fun (y : AmnrSpace) => u y.1 y.2) z

Differentiating the actual PDE gives the source gradient equation. The velocity contraction has the transpose indices required by e.Tm-1:i:evo.