Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Section4.Amnr.TemperatureDiffusionRates

Abstract scalar rate algebra used by the temperature energy cascade.

theorem AVenhance.Infra.Section4.amnr_diffusivity_radius_identity {E : ℝ} (hE : 0 < E) (A γ : ℝ) :
A * E ^ (2 + γ) * (E ^ (-(1 + γ / 2))) ^ 2 = A

The source spatial radius cancels the extra diffusivity power exactly.

theorem AVenhance.Infra.Section4.amnr_diffusion_rate_le {E A κ C H γ : ℝ} (hE : 0 < E) (hκ : κ ≤ C * (A * E ^ (2 + γ))) (hA : A ≤ H) (hC : 0 ≤ C) :
κ * (E ^ (-(1 + γ / 2))) ^ 2 ≤ C * H

The upper diffusivity-recursion estimate supplies the material diffusion rate.