Part I: the one-sided recursion amnrWithin and its C^∞ extension to t ≥ 0

The Amnr recursion differentiates in time with the two-sided deriv, so at t = 0 it depends on the arbitrary negative-time values of T. amnrWithin is the same recursion with derivWithin (·) (Set.Ici 0). It agrees with Amnr at every positive time and is jointly C^∞ on the closed half space [0,∞) × ℝ². Nothing is assumed about Amnr at t ≤ 0.

def AVenhance.Infra.Section5.Integration.amnrWithin {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (n : ℕ) (Tm1 : ℝ → Homogenization.Vec 2 → ℝ) : ℕ → ℝ → Homogenization.Vec 2 → Fin 2 → Fin 2 → Fin 2 → ℝ

The recursion of the Amnr, with the time derivative taken within [0,∞).

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.Infra.Section5.Integration.amnrWithin I hΦ m κm n Tm1 0 = I.Amnr hΦ m κm n Tm1 0

theorem AVenhance.Infra.Section5.Integration.amnrWithin_eq_Amnr {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (n : ℕ) (Tm1 : ℝ → Homogenization.Vec 2 → ℝ) (r : ℕ) (t : ℝ) : 0 < t → ∀ (x : Homogenization.Vec 2) (i j k : Fin 2), amnrWithin I hΦ m κm n Tm1 r t x i j k = I.Amnr hΦ m κm n Tm1 r t x i j k

At positive times the one-sided recursion is the Amnr.

theorem AVenhance.Infra.Section5.Integration.derivWithin_slice_eq_fderivWithin {F : ℝ × Homogenization.Vec 2 → ℝ} (t : ℝ) (x : Homogenization.Vec 2) (ht : 0 ≤ t) (hF : DifferentiableWithinAt ℝ F (Set.Ici 0 ×ˢ Set.univ) (t, x)) : derivWithin (fun (s : ℝ) => F (s, x)) (Set.Ici 0) t = (fderivWithin ℝ F (Set.Ici 0 ×ˢ Set.univ) (t, x)) (1, 0)

The time slice derivative within [0,∞) of a function differentiable within the closed half space is the corresponding directional fderivWithin.

theorem AVenhance.Infra.Section5.Integration.amnrWithin_contDiffOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κm : ℝ) (n : ℕ) (Tm1 : ℝ → Homogenization.Vec 2 → ℝ) (j k : Fin 2) (hb : ContDiff ℝ ↑⊤ fun (z : Section4.AmnrSpace) => streamVel (Φ (m - 1)) z.1 z.2) (hf : ∀ (i p : Fin 2), ContDiff ℝ (↑⊤) (Section4.amnrSeedMultiplier I hΦ m κm n j k i p)) (hg : ∀ (p : Fin 2), ContDiffOn ℝ (↑⊤) (Section4.amnrTGradient Tm1 p) (Set.Ici 0 ×ˢ Set.univ)) (r : ℕ) (i : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (z : ℝ × Homogenization.Vec 2) => amnrWithin I hΦ m κm n Tm1 r z.1 z.2 i j k) (Set.Ici 0 ×ˢ Set.univ)

amnrWithin is jointly C^∞ on [0,∞) × ℝ², given C^∞ coefficient factors.