Iterates VAbstract Amplitude

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_V_abstract_amplitude_of_diffusivity_and_flow {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hm : 2 ≤ m) (hκm : 0 < κm) (hflow : ∀ (l : ℤ), ContDiff ℝ ↑⊤ fun (z : AmnrSpace) => I.flowGrad hΦ m l z.1 z.2) (hflowp : ∀ (t : ℝ), 0 < t → ∀ (l : ℤ), IsZ2Periodic (I.flowGrad hΦ m l t)) (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))) {c Ck K Cflow Cmean Rflow Cθ Rθ C₀ N : ℝ} (hN : 0 < N) (hc : 0 < c) (hCk : 0 ≤ Ck) (hK : 0 ≤ K) (hCf : 0 ≤ Cflow) (hCm : 0 ≤ Cmean) (hRf : 256 ≤ Rflow) (hRθ : 0 < Rθ) (hlower : c * (a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ (2 + gamma β)) ≤ κprev) (hupper : κprev ≤ Ck * (a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ (2 + gamma β))) (hC₀ : iterateSourceConstant (iterateBudgetUniversalConstant K Ck c (2 ^ (-25)) Cflow Cmean) Rflow Cθ ≤ C₀) (hsmall : C₀ ^ 3 * epsilon β I.Λ (m - 1) ^ (2 * delta β) * max 1 (epsilon β I.Λ (m - 1) ^ (2 + gamma β) * Rθ ^ (-2)) ≤ 1) (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 * epsilon β I.Λ (m - 1) ^ (2 * delta β)) (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 * epsilon β I.Λ (m - 1) ^ (2 * delta β)) (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 * (Rflow / epsilon β I.Λ (m - 1)) ^ p.length) (hκscale : |κm| ≤ κprev) (hbase : iterateCoordinateEnergyProfile θprev κprev N (max (C₀ * epsilon β I.Λ (m - 1) ^ (-1 - gamma β / 2)) (C₀ / Rθ)) 0) (i : ℕ) : 1 ≤ i → i ≤ Nstar β → ∀ (v w : List (Fin 2)), v.length = w.length → ∀ (s : ℝ), 0 ≤ s → s ≤ 1 → √(l2NormSq (iterateSpatialWord v (iterateIncrement T i s))) + √κprev * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (iterateIncrement T i t))) ≤ N * iterateAmplitude (C₀ ^ 3 * epsilon β I.Λ (m - 1) ^ (2 * delta β) * max 1 (epsilon β I.Λ (m - 1) ^ (2 + gamma β) * Rθ ^ (-2))) i * iterateAnalyticWeight v.length i (max (C₀ * epsilon β I.Λ (m - 1) ^ (-1 - gamma β / 2)) (C₀ / Rθ))

Abstract-amplitude corrected l.V for positive increments. The theta base profile excludes its undifferentiated scalar energy, so both the initial-data and RelativeError relative-dissipation normalizations use this same theorem.