Iterates Forcing Profiles From Flow

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_TForcing_profiles_from_flow {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev K Cflow Cmean r₀ ρ : ℝ} (hκ : 0 ≤ κprev) (hK : 0 ≤ K) (hCf : 0 ≤ Cflow) (hCm : 0 ≤ Cmean) (hr : 0 ≤ r₀) (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hflow : ∀ (t : ℝ) (l : ℤ), ContDiff ℝ (↑⊤) (I.flowGrad hΦ m l t)) (hKm : ∀ (t : ℝ) (j k : Fin 2), |I.Kmat κm m t j k| ≤ K * κprev) (hmean : ∀ (j k : Fin 2), |(timeAvgMat (I.Kmat κm m) - κprev • 1) j k| ≤ κprev * Cmean * ρ) (hzero : ∀ (t : ℝ) (x : Homogenization.Vec 2) (l : ℤ), I.hatXiML m l t ≠ 0 → ∀ (j k : Fin 2), |(I.flowGrad hΦ m l t x - 1) j k| ≤ Cflow * ρ) (hpositive : ∀ (t : ℝ) (x : Homogenization.Vec 2) (l : ℤ), I.hatXiML m l t ≠ 0 → ∀ (p : List (Fin 2)), 1 ≤ p.length → ∀ (j k : Fin 2), |iterateSpatialWord p (fun (y : Homogenization.Vec 2) => (I.flowGrad hΦ m l t y - 1) j k) x| ≤ Cflow * ↑p.length.factorial * r₀ ^ p.length) (hκscale : |κm| ≤ κprev) (hrad1 : 1 ≤ r₀ / ρ) : (∀ (t : ℝ) (x : Homogenization.Vec 2) (p : List (Fin 2)) (j k : Fin 2), |iterateMatrixWord (fun (y : Homogenization.Vec 2) => I.Kmat κm m t - κprev • 1 + I.sMat hΦ m κm t y) p x j k| ≤ κprev * (K + 1 + Cmean + (2 * K * Cflow + 4 * (K + 1) * Cflow * (Cflow + 1))) * ↑p.length.factorial * (2 * (r₀ / ρ)) ^ p.length) ∧ ∀ (t : ℝ) (x : Homogenization.Vec 2) (p : List (Fin 2)) (j k : Fin 2), |iterateMatrixWord (fun (y : Homogenization.Vec 2) => timeAvgMat (I.Kmat κm m) - κprev • 1 + I.sMat hΦ m κm t y) p x j k| ≤ κprev * (K + 1 + Cmean + (2 * K * Cflow + 4 * (K + 1) * Cflow * (Cflow + 1))) * ρ * ↑p.length.factorial * (2 * (r₀ / ρ)) ^ p.length

The two actual forcing coefficient profiles are derived from active flow jets, the K bound, and the mean comparison. Positive flow jets need not carry the small distortion prefactor before radius inflation.