Regularity of the R46 flux when its temperature is an actual T iterate.
At each fixed time the cutoff sums are finite. The flow-pulled gradients are smooth and periodic because the actual flow and inverse are jointly smooth and lattice equivariant.
theorem
AVenhance.Infra.Section5.R46IteratesRegularity.r46_G_contDiff
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(T : ℝ → Homogenization.Vec 2 → ℝ)
(t : ℝ)
(l : ℤ)
(hT : ContDiff ℝ (↑⊤) (T t))
:
theorem
AVenhance.Infra.Section5.R46IteratesRegularity.r46_G_periodic
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(T : ℝ → Homogenization.Vec 2 → ℝ)
(t : ℝ)
(l : ℤ)
(hT : IsZ2Periodic (T t))
(hTsmooth : ContDiff ℝ 1 (T t))
:
IsZ2Periodic (G I hΦ m T l t)
theorem
AVenhance.Infra.Section5.R46IteratesRegularity.r46_flux_contDiff_of_slice
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(hm : 1 ≤ m)
(κm : ℝ)
(T : ℝ → Homogenization.Vec 2 → ℝ)
(t : ℝ)
(hT : ContDiff ℝ (↑⊤) (T t))
:
theorem
AVenhance.Infra.Section5.R46IteratesRegularity.r46_flux_periodic_of_slice
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(hm : 1 ≤ m)
(κm : ℝ)
(T : ℝ → Homogenization.Vec 2 → ℝ)
(t : ℝ)
(hT : IsZ2Periodic (T t))
(hTsmooth : ContDiff ℝ 1 (T t))
:
IsZ2Periodic (r46Flux I hΦ m κm T t)
theorem
AVenhance.Infra.Section5.tIterate_r46Flux_regular
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
(κm : ℝ)
{κprev : ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
{θprev : ℝ → Homogenization.Vec 2 → ℝ}
{T : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T)
(hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev)
{i : ℕ}
(hi : i ≤ Nstar β)
{t : ℝ}
(ht : 0 < t)
:
The R46 flux of any actual iterate is smooth and periodic at positive
times. The only iterate bound used is the finite cutoff index constraint.