Iterates Analytic Weight Order

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterateAnalyticWeight_mono {n i j : ℕ} {L : ℝ} (hL : 0 ≤ L) (hij : i ≤ j) : iterateAnalyticWeight n i L ≤ iterateAnalyticWeight n j L

Increasing the increment index increases its factorial weight.

theorem AVenhance.Infra.Section4.iterateAnalyticWeight_nonneg (n i : ℕ) {L : ℝ} (hL : 0 ≤ L) : 0 ≤ iterateAnalyticWeight n i L