The diffusion and forcing terms of the actual temperature equation.
Spatial diffusion in ordered coordinates, with its actual finite sum.
Equations
- AVenhance.Infra.Section4.amnrSpatialLap f z = ∑ p : Fin 2, AVenhance.Infra.Section4.amnrWord (fun (x : AVenhance.Infra.Section4.AmnrSpace) => 0) [some p, some p] f z
Instances For
theorem
AVenhance.Infra.Section4.amnr_classical_spatialLap
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{κ : ℝ}
{F : ℝ → Homogenization.Vec 2 → ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
{u : ℝ → Homogenization.Vec 2 → ℝ}
(hu : IsClassicalSol b κ F θ₀ u)
:
The ordered spatial Laplacian equals the slice Laplacian for the actual classical temperature, on the entire positive-time domain.
theorem
AVenhance.Infra.Section4.amnr_classical_spatialLap_contDiffOn
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{κ : ℝ}
{F : ℝ → Homogenization.Vec 2 → ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
{u : ℝ → Homogenization.Vec 2 → ℝ}
(hu : IsClassicalSol b κ F θ₀ u)
(N : ℕ)
:
Classical smoothness supplies every finite joint derivative of diffusion, with exactly the two additional spatial derivatives required by the cascade.
theorem
AVenhance.Infra.Section4.amnr_classical_forcing_contDiffOn
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{κ : ℝ}
{F : ℝ → Homogenization.Vec 2 → ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
{u : ℝ → Homogenization.Vec 2 → ℝ}
(hu : IsClassicalSol b κ F θ₀ u)
(N : ℕ)
(hb : ContDiffOn ℝ (↑N + 1) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ioi 0 ×ˢ Set.univ))
:
The forcing of a classical solution has every finite joint derivative allowed by the velocity's smoothness. No regularity of the forcing coefficient or the solution's material derivatives is assumed.