Iterates Flow Support

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_hatXi_time_window {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {l : ℤ} {t : ℝ} (hne : I.hatXiML m l t ≠ 0) : |t - ↑l * tauPP β I.Λ m| ≤ tauPP β I.Λ m

The enlarged hat cutoff stays within one refresh cell.

theorem AVenhance.Infra.Section4.iterate_refresh_amplitude_bound {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) : tauPP β I.Λ m * a β I.Λ (m - 1) ≤ 2 ^ (-25) * epsilon β I.Λ (m - 1) ^ (2 * delta β)

Refresh time times the preceding shear amplitude retains the rho gain.

theorem AVenhance.Infra.Section4.iterate_hatXi_section2_window {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {l : ℤ} {t : ℝ} (hne : I.hatXiML m l t ≠ 0) : |t - ↑l * tauPP β I.Λ m| ≤ 2 ^ (-25) * (a β I.Λ (m - 1))⁻¹

The hat support fits the signed-time Section 2 flow window.