Actual mixed stream rates on the current material-amplitude scale.

noncomputable def AVenhance.Infra.Section4.amnrStreamMixedCurrentConstant {β : ℝ} (I : Ingredients β) : ℝ

One source constant absorbs every fine cutoff time derivative.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Section4.amnrStreamMixedCurrentConstant_pos {β : ℝ} (I : Ingredients β) : 0 < amnrStreamMixedCurrentConstant I

theorem AVenhance.Infra.Section4.amnr_fine_time_power_le_current {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {r N : ℕ} (hr : r ≤ N) : 2 ^ r * (tau β I.Λ m)⁻¹ ^ r ≤ (2 * max 1 (amnrFineMaterialConstant β)) ^ N * a β I.Λ m ^ r

Every fine-time power is controlled by the actual current amplitude.

theorem AVenhance.Infra.Section4.amnr_streamIncrement_mixed_current_abs_le_of_A3 {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (α : List (Fin 2)) (r : ℕ) (hbudget : α.length + 2 * r ≤ Nstar β) (z : AmnrSpace) : |amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (amnrMixedWord α r) (fun (y : AmnrSpace) => Φ m y.1 y.2 - Φ (m - 1) y.1 y.2) z| ≤ amnrStreamMixedCurrentConstant I * a β I.Λ m * epsilon β I.Λ m ^ 2 * (epsilon β I.Λ m)⁻¹ ^ α.length * a β I.Λ m ^ r

Actual canonical mixed stream jets use only the construction and the stream-regularity estimates. The fine cutoff rate is absorbed into the current material amplitude.