Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Section4.Amnr.TemperatureGradientMaterialEquation

The actual material gradient equation with all primitive fields identified.

theorem AVenhance.Infra.Section4.amnr_classical_gradient_material_equation {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F u : ℝ → Homogenization.Vec 2 → ℝ} {u₀ : Homogenization.Vec 2 → ℝ} (hu : IsClassicalSol b κ F u₀ u) (hb : ContDiff ℝ ↑⊤ fun (z : AmnrSpace) => b z.1 z.2) (i : Fin 2) {z : AmnrSpace} (hz : 0 < z.1) :
amnrOp (fun (y : AmnrSpace) => b y.1 y.2) none (amnrTGradient u i) z = κ * ∑ q : Fin 2, amnrWord (fun (y : AmnrSpace) => b y.1 y.2) [some q, some q] (amnrTGradient u i) z + spaceGrad (F z.1) z.2 i - ∑ p : Fin 2, amnrVelocityGradient (fun (y : AmnrSpace) => b y.1 y.2) p i z * amnrTGradient u p z

The classical PDE gives the actual gradient material equation. Neither its material derivative nor a differentiated PDE is assumed.