Full actual mixed seed-multiplier bounds from source ingredients.

theorem AVenhance.Infra.Section4.amnr_seedMultiplierA0Plus_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (n N : ℕ) (hN : N ≤ Nstar β) (j k i p : Fin 2) : ContDiff ℝ (↑N) (amnrSeedMultiplierA0Plus I hΦ m κ n j k i p)

Smoothness of the candidate seed through the full source order.

theorem AVenhance.Infra.Section4.amnr_seedMultiplier_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (n N : ℕ) (hN : N ≤ Nstar β) (j k i p : Fin 2) : ContDiff ℝ (↑N) (amnrSeedMultiplier I hΦ m κ n j k i p)

Smoothness of the actual seed through the source order.