Iterates Diffusivity Comparison

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_kappaAt_abs_le_previous {β : ℝ} (I : Ingredients β) {κ : ℝ} (hκ : 0 < κ) {m M : ℕ} (hm : 1 ≤ m) (hmM : m ≤ M) : |I.kappaAt κ m (M - m)| ≤ I.kappaAt κ (m - 1) (M - (m - 1))

The actual diffusivity chain supplies the new coefficient's molecular scale bound; this is proved from its recursion, not an assumed input.

theorem AVenhance.Infra.Section4.iterate_kappaSeq_abs_le_previous {β : ℝ} (I : Ingredients β) {κ : ℝ} (hκ : 0 < κ) {m M : ℕ} (hm : 1 ≤ m) (hmM : m ≤ M) : |I.kappaSeq κ M m| ≤ I.kappaSeq κ M (m - 1)