Iterates Velocity Physical Bounds

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_velocity_gradMatrix_bound_of_A3 {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) (hA3 : ∀ (j : ℕ), 1 ≤ j → ∀ (t : ℝ) (n : ℕ), 2 ≤ n → barNorm n (2 ^ 8 * (epsilon β I.Λ j)⁻¹) (Φ j t) ≤ ENNReal.ofReal (2 ^ 5 * AVenhance.a β I.Λ j * epsilon β I.Λ j ^ 2 * ((↑n + 2) ^ 2 / (↑n + 1) ^ 3))) (t : ℝ) (x : Homogenization.Vec 2) (j k : Fin 2) : |gradMatrix (streamVel (Φ (m - 1)) t) x j k| ≤ 2 ^ 21 * a β I.Λ (m - 1)

The stream-regularity estimates supply the actual velocity-gradient scale.

theorem AVenhance.Infra.Section4.iterate_velocity_extended_profile_of_A3 {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) (hA3 : ∀ (j : ℕ), 1 ≤ j → ∀ (t : ℝ) (n : ℕ), 2 ≤ n → barNorm n (2 ^ 8 * (epsilon β I.Λ j)⁻¹) (Φ j t) ≤ ENNReal.ofReal (2 ^ 5 * AVenhance.a β I.Λ j * epsilon β I.Λ j ^ 2 * ((↑n + 2) ^ 2 / (↑n + 1) ^ 3))) {r : ℝ} (hr : 0 < r) (hle : 256 * (epsilon β I.Λ (m - 1))⁻¹ ≤ r) (t : ℝ) (x : Homogenization.Vec 2) (p : List (Fin 2)) : 1 ≤ p.length → ∀ (j : Fin 2), |iterateSpatialWord p (fun (y : Homogenization.Vec 2) => streamVel (Φ (m - 1)) t y j) x| ≤ 2 ^ 21 * AVenhance.a β I.Λ (m - 1) / r * ↑p.length.factorial * r ^ p.length

Positive-order stream-regularity jets extend to the common inflated flow radius while keeping the physical first-jet product fixed.