The stream-regularity estimates give the actual high stream-matrix analytic profile.
theorem
AVenhance.Infra.Section4.iterate_stream_matrix_word_abs_le
{φ : Homogenization.Vec 2 → ℝ}
(hφ : ContDiff ℝ (↑⊤) φ)
(w : List (Fin 2))
(x : Homogenization.Vec 2)
(i j : Fin 2)
:
|iterateMatrixWord (fun (y : Homogenization.Vec 2) => φ y • sigmaMat) w x i j| ≤ |iterateSpatialWord w φ x|
The fixed skew matrix introduces no coefficient loss.
theorem
AVenhance.Infra.Section4.iterate_stream_matrix_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)))
(t : ℝ)
(w : List (Fin 2))
(hw : 2 ≤ w.length)
(x : Homogenization.Vec 2)
(i j : Fin 2)
:
High actual stream matrix jets obey the factorial profile under the stream-regularity premise. The additional source denominator is safely discarded.