Actual endpoint regularity on positive times. No closed-time regularity of the two-sided Amnr recursion is required.
theorem
AVenhance.Infra.Section5.RelativeError.relative_initial_endpoint_contDiffOn_Ioi_top
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
{κm κprev : ℝ}
(hκm : 0 < κm)
{θ₀ : Homogenization.Vec 2 → ℝ}
{θprev : ℝ → Homogenization.Vec 2 → ℝ}
{T : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev)
(hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T)
(r : ℕ)
:
ContDiffOn ℝ (↑⊤) (fun (z : ℝ × Homogenization.Vec 2) => hmEndpoint I hΦ m κm (T (Nstar β)) r z.1 z.2)
(Set.Ioi 0 ×ˢ Set.univ)
Every actual endpoint is jointly smooth on the open positive half-space.
theorem
AVenhance.Infra.Section5.RelativeError.relative_initial_endpoint_periodic_pos
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(κm : ℝ)
{Tm1 : ℝ → Homogenization.Vec 2 → ℝ}
(hTper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (Tm1 t))
(r : ℕ)
{t : ℝ}
(ht : 0 < t)
:
IsZ2Periodic (hmEndpoint I hΦ m κm Tm1 r t)
Every endpoint is spatially periodic at positive times.