Iterates Actual First Energy Recurrence #
Support for the Armstrong–Vicol anomalous-diffusion formalization.
theorem
AVenhance.Infra.Section4.iterate_actual_first_increment_energy_recurrence
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(hNstar : 1 ≤ Nstar β)
{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)
(hκ : 0 < κprev)
(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)))
(w : List (Fin 2))
{C Ccoef Gcur N B r L D Bflow ρ q : ℝ}
(hL : 0 < L)
(hg : 2 * (r / L) ^ 2 ≤ 1 / 2)
(hvel : 2 * (256 * (epsilon β I.Λ (m - 1))⁻¹ / L) ^ 2 ≤ 1 / 4)
(hD : 0 ≤ D)
(hC : 0 ≤ C)
(hGc : 0 ≤ Gcur)
(hN : 0 ≤ N)
(hB : 0 ≤ B)
(hr : 0 ≤ r)
(hρ : 0 ≤ ρ)
(hq : 0 < q)
(hρq : ρ ≤ q)
(hQ : ∀ (t : ℝ) (j k : Fin 2), |iterateKmatPrimitive I κm m t j k| ≤ D)
(hscale : D * L ^ 2 ≤ C * q)
(hvelocity : B * r ≤ C * κprev * L ^ 2)
(hjet :
∀ (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| ≤ B * ↑p.length.factorial * r ^ p.length)
(hFlowBound : ∀ (t : ℝ) (x : Homogenization.Vec 2) (j k : Fin 2), |gradMatrix (streamVel (Φ (m - 1)) t) x j k| ≤ Bflow)
(hFlowScale : D * Bflow ≤ C * κprev * ρ)
(hrem :
∀ (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 * Ccoef * ρ * ↑p.length.factorial * r ^ p.length)
(hbase :
∀ (p : List (Fin 2)),
p.length ≤ w.length + 3 →
(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord p (θprev t))) ≤ (N / √κprev) ^ 2 * (↑p.length.factorial * L ^ p.length) ^ 2)
(hterminal :
∀ (p : List (Fin 2)),
1 ≤ p.length →
p.length ≤ w.length + 2 →
∀ (t : ℝ),
0 ≤ t → t ≤ 1 → l2NormSq (iterateSpatialWord p (θprev t)) ≤ N ^ 2 * (↑p.length.factorial * L ^ p.length) ^ 2)
(d : ℕ → ℝ)
(hd : ∀ (n : ℕ), 0 ≤ d n)
(hlower :
∀ (p : List (Fin 2)),
p.length < w.length →
(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord p (iterateIncrement T 1 t))) ≤ Gcur ^ 2 * (↑(p.length + 2).factorial * L ^ p.length) ^ 2 * d p.length ^ 2)
{s : ℝ}
(hs : 0 ≤ s)
(hs1 : s ≤ 1)
:
l2NormSq (iterateSpatialWord w (iterateIncrement T 1 s)) / 2 + κprev * ∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecNormSq (spaceGrad (iterateSpatialWord w (iterateIncrement T 1 z.1)) z.2) ≤ (l2NormSq (iterateSpatialWord w (iterateIncrement T 1 s)) / 4 + 3 * κprev / 8 * spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (iterateIncrement T 1 t))) + iterateFirstEnergyBudget w.length κprev D (a β I.Λ (m - 1)) (epsilon β I.Λ (m - 1)) r L C Ccoef B Gcur N ρ q d
Complete exceptional first-increment energy recurrence. The first material forcing cancellation is derived from the actual homogeneous base equation.