Part I: spatial periodicity of Amnr and HTilde_m for positive times #
Amnr is built from ℤ²-periodic pieces (∇T, the pulled-back flow gradient, the previous
velocity and its gradient). Time derivatives only see a neighbourhood of t, so periodicity at
t > 0 follows from periodicity at all nearby (positive) times.
theorem
AVenhance.Infra.Section5.Integration.streamVel_prev_isZ2Periodic
{β : ℝ}
{I : Ingredients β}
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(t : ℝ)
:
IsZ2Periodic (streamVel (Φ (m - 1)) t)
The previous velocity is ℤ²-periodic in space at every time.
theorem
AVenhance.Infra.Section5.Integration.Amnr_isZ2Periodic_pos
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(κm : ℝ)
(n : ℕ)
{Tm1 : ℝ → Homogenization.Vec 2 → ℝ}
(hTper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (Tm1 t))
(r : ℕ)
(t : ℝ)
:
0 < t → ∀ (i j k : Fin 2), IsZ2Periodic fun (x : Homogenization.Vec 2) => I.Amnr hΦ m κm n Tm1 r t x i j k
Amnr is ℤ²-periodic in space at positive times, given a spatially periodic T
at nonnegative times.
theorem
AVenhance.Infra.Section5.Integration.Hmr_isZ2Periodic_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 (I.Hmr hΦ m κm Tm1 r t)
Each HTilde_{m,r} is ℤ²-periodic at positive times.
theorem
AVenhance.Infra.Section5.Integration.Hm_periodic_pos
{β : ℝ}
(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)
{t : ℝ}
(ht : 0 < t)
:
IsZ2Periodic (I.Hm hΦ m κm (T (Nstar β)) t)
HTilde_m is ℤ²-periodic in space at every positive time.