Generic seed multipliers and AMNR seed infrastructure.

theorem AVenhance.Infra.Section4.amnr_abs_list_sum_le (L : List ℝ) : |L.sum| ≤ (List.map abs L).sum

theorem AVenhance.Infra.Section4.amnrWord_mul_abs_le {U : Set AmnrSpace} (hU : IsOpen U) {b : AmnrSpace → Homogenization.Vec 2} {f g : AmnrSpace → ℝ} {N : ℕ} (hb : ContDiffOn ℝ (↑N) b U) (hf : ContDiffOn ℝ (↑N) f U) (hg : ContDiffOn ℝ (↑N) g U) {S H F G : ℝ} (hS : 0 ≤ S) (hH : 0 ≤ H) (hF : 0 ≤ F) (_hG : 0 ≤ G) (w : List (Option (Fin 2))) (hw : amnrBudget w ≤ N) (hfb : ∀ (v : List (Option (Fin 2))), v.Sublist w → ∀ z ∈ U, |amnrWord b v f z| ≤ F * amnrWeight S H v) (hgb : ∀ (v : List (Option (Fin 2))), v.Sublist w → ∀ z ∈ U, |amnrWord b v g z| ≤ G * amnrWeight S H v) {z : AmnrSpace} (hz : z ∈ U) : |amnrWord b w (f * g) z| ≤ 2 ^ w.length * F * G * amnrWeight S H w

The pointwise counterpart of the mixed L2 multiplier estimate. It is used for the memory coefficient times the pulled-back flow multiplier in the seed.

theorem AVenhance.Infra.Section4.IsAmnrMixedWord.normalForm {w : List (Option (Fin 2))} (hw : IsAmnrMixedWord w) : ∃ (α : List (Fin 2)) (ℓ : ℕ), w = amnrMixedWord α ℓ

Every ordered mixed word has the source's spatial-then-material form.

theorem AVenhance.Infra.Section4.amnr_timeCube_isOpen : IsOpen timeCube

The source cell is open, so the directional calculus and L2 norms apply to the precise paper domain without endpoint extension assumptions.

theorem AVenhance.Infra.Section4.amnr_previous_velocity_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (N : ℕ) : ContDiff ℝ ↑N fun (z : AmnrSpace) => streamVel (Φ (m - 1)) z.1 z.2

Joint smoothness of the actual previous velocity follows from the defining previous-stream witness; it is not an extra induction hypothesis.

theorem AVenhance.Infra.Section4.amnrWord_const_smul (b : AmnrSpace → Homogenization.Vec 2) (c : ℝ) (w : List (Option (Fin 2))) (f : AmnrSpace → ℝ) : amnrWord b w (c • f) = c • amnrWord b w f

Constant scalar multiplication commutes with a differential word even when an intermediate derivative is defined by the total fderiv convention.

noncomputable def AVenhance.Infra.Section4.amnrFlowAverage {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (k p : Fin 2) (z : AmnrSpace) : ℝ

The cutoff-weighted flow factor before multiplication by the memory.

Equations

• AVenhance.Infra.Section4.amnrFlowAverage I hΦ m k p z = ∑' (l : ℤ), I.hatXiML m l z.1 * I.flowGrad hΦ m l z.1 z.2 k p

theorem AVenhance.Infra.Section4.amnrSeedMultiplierA0Plus_eq {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (n : ℕ) (j k i p : Fin 2) : amnrSeedMultiplierA0Plus I hΦ m κ n j k i p = fun (z : ℝ × Homogenization.Vec 2) => -I.LMN κ m n z.1 * amnrFlowAverageA0Plus I hΦ m j k i p z

Unfolded product formula for the left-Jacobian base.

theorem AVenhance.Infra.Section4.amnrLMN_mul_mixed_le {β C₀ : ℝ} (I : Ingredients β) (hcutoff : I.Chat ≤ C₀) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) {n : ℕ} (hn : n ≤ Nstar β) {U : Set AmnrSpace} (hU : IsOpen U) {A : AmnrSpace → ℝ} (hA : ContDiffOn ℝ (↑(Nstar β)) A U) {S X : ℝ} (hS : 0 ≤ S) (hX : 0 ≤ X) (hAbound : ∀ (w : List (Option (Fin 2))), IsAmnrMixedWord w → amnrBudget w ≤ Nstar β → ∀ z ∈ U, |amnrWord (fun (z : AmnrSpace) => streamVel (Φ (m - 1)) z.1 z.2) w A z| ≤ X * amnrWeight S (tauP β I.Λ m)⁻¹ w) (w : List (Option (Fin 2))) (hw : IsAmnrMixedWord w) (hbudget : amnrBudget w ≤ Nstar β) {z : AmnrSpace} (hz : z ∈ U) : |amnrWord (fun (z : AmnrSpace) => streamVel (Φ (m - 1)) z.1 z.2) w (fun (z : AmnrSpace) => -I.LMN κ m n z.1 * A z) z| ≤ 2 ^ Nstar β * amnrMemoryConstant β C₀ * (epsilon β I.Λ m ^ 2 / κ) * X * amnrWeight S (tauP β I.Λ m)⁻¹ w

Generic memory-times-average estimate. The cutoff-flow factor may already contain additional factors inside its summands; only its own smoothness and mixed bound enter this multiplication step.