Pointwise differentiated-drift bounds from the high-order stream-regularity conclusion.
theorem
AVenhance.Infra.Section4.theta_prev_potential_word_abs_le_of_A3
{β : ℝ}
{m : ℕ}
(I : Ingredients β)
(Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ)
(hΦ : IsStreamSeq I Φ)
(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 : ℝ)
(w : List (Fin 2))
:
theorem
AVenhance.Infra.Section4.theta_prev_drift_word_abs_le_of_A3
{β : ℝ}
{m : ℕ}
(I : Ingredients β)
(Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ)
(hΦ : IsStreamSeq I Φ)
(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 : ℝ)
(w : List (Fin 2))
:
1 ≤ w.length →
∀ (j : Fin 2) (x : Homogenization.Vec 2),
|classicalWordDerivative w (fun (y : Homogenization.Vec 2) => streamVel (fun (x : ℝ) => Φ (m - 1) t) 0 y j) x| ≤ 2 ^ 5 * AVenhance.a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ 2 * ↑(w.length + 1).factorial * (2 ^ 8 * (epsilon β I.Λ (m - 1))⁻¹) ^ (w.length + 1)
The drift derivatives entering the transport commutator are controlled by the high-order barNorm clause of the stream-regularity estimates. The hypothesis is copied literally from that clause; its order-two threshold is used because every commutator term differentiates the drift at least once.