Iterates Diffusive Material Scale

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_diffusive_material_normalization {κ N : ℝ} (hκ : 0 < κ) : κ ^ 2 * (N / √κ) ^ 2 = κ * N ^ 2

Diffusive normalization cancels the square-root diffusivity exactly.

theorem AVenhance.Infra.Section4.iterate_diffusive_material_product {κ N R : ℝ} (hκ : 0 < κ) : R * √κ * N * (N / √κ) = R * N ^ 2

The two material factors have reciprocal diffusive scales.

theorem AVenhance.Infra.Section4.iterate_diffusive_gradient_normalization {κ N : ℝ} (hκ : 0 < κ) : κ * (N / √κ) ^ 2 = N ^ 2

The preceding scalar gradient has the reciprocal diffusive normalization.