Provider proofs for the §2 construction recursion.

theorem AVenhance.Proofs.IsAdmissibleStream.NextStreamAdmissible.epsilon_inv_eq_nat {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) : (epsilon β I.Λ m)⁻¹ = ↑⌈↑I.Λ ^ (q β ^ m / (q β - 1))⌉₊

theorem AVenhance.Proofs.IsAdmissibleStream.NextStreamAdmissible.psi_lattice_periodic {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (k : ℤ) (x : Homogenization.Vec 2) (j : Fin 2 → ℤ) : psi β I.Λ m k (x + latticeShift j) = psi β I.Λ m k x

theorem AVenhance.Proofs.IsAdmissibleStream.NextStreamAdmissible.psi_index_periodic {β : ℝ} (I : Ingredients β) (m : ℕ) {K : ℤ} (hK : K % 4 = 0) (k : ℤ) (x : Homogenization.Vec 2) : psi β I.Λ m (k + K) x = psi β I.Λ m k x

theorem AVenhance.Proofs.IsAdmissibleStream.NextStreamAdmissible.nextStreamTerm_contDiff {β : ℝ} (I : Ingredients β) (m : ℕ) (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (k : ℤ) : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => I.nextStreamTerm m φ hφ p.1 p.2 k

theorem AVenhance.Proofs.IsAdmissibleStream.NextStreamAdmissible.nextStreamTerm_ne_zero_distance {β : ℝ} (I : Ingredients β) (m : ℕ) (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (t : ℝ) (x : Homogenization.Vec 2) (k : ℤ) (hne : I.nextStreamTerm m φ hφ t x k ≠ 0) : |t - ↑k * tau β I.Λ m| ≤ 2 / 3 * tau β I.Λ m

theorem AVenhance.Proofs.IsAdmissibleStream.NextStreamAdmissible.nextStreamTerm_locally_finite_sum {β : ℝ} (I : Ingredients β) (m : ℕ) (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (p : ℝ × Homogenization.Vec 2) : ∃ (S : Finset ℤ), ∀ᶠ (q : ℝ × Homogenization.Vec 2) in nhds p, ∑' (k : ℤ), I.nextStreamTerm m φ hφ q.1 q.2 k = ∑ k ∈ S, I.nextStreamTerm m φ hφ q.1 q.2 k

theorem AVenhance.Proofs.IsAdmissibleStream.NextStreamAdmissible.nextStream_smooth {β : ℝ} (I : Ingredients β) (m : ℕ) (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) : ContDiff ℝ (↑⊤) (Function.uncurry (I.nextStream m φ hφ))

theorem AVenhance.Proofs.IsAdmissibleStream.NextStreamAdmissible.flow_integer_time_shift {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Infra.Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (hL : ∃ (L : ℝ), ∀ (t : ℝ) (x y : Homogenization.Vec 2), ‖b t x - b t y‖ ≤ L * ‖x - y‖) (N : ℤ) (x : Homogenization.Vec 2) (s t : ℝ) : X (t + ↑N) x (s + ↑N) = X t x s

theorem AVenhance.Proofs.IsAdmissibleStream.NextStreamAdmissible.lIdx_add_time_shift {β : ℝ} (I : Ingredients β) (m : ℕ) (k K L : ℤ) (hKτ : ↑K * tau β I.Λ m = ↑L * tauPP β I.Λ m) : lIdx β I.Λ m (k + K) = lIdx β I.Λ m k + L

theorem AVenhance.Proofs.IsAdmissibleStream.NextStreamAdmissible.zetaMK_add_time_shift {β : ℝ} (I : Ingredients β) (m : ℕ) (k K N : ℤ) (t : ℝ) (hKτ : ↑K * tau β I.Λ m = ↑N) : I.zetaMK m (k + K) (t + ↑N) = I.zetaMK m k t

theorem AVenhance.Proofs.IsAdmissibleStream.NextStreamAdmissible.hatZetaML_add_time_shift {β : ℝ} (I : Ingredients β) (m : ℕ) (l L N : ℤ) (t : ℝ) (hLPP : ↑L * tauPP β I.Λ m = ↑N) : I.hatZetaML m (l + L) (t + ↑N) = I.hatZetaML m l t

theorem AVenhance.Proofs.IsAdmissibleStream.nextStream_isAdmissible {β : ℝ} (I : Ingredients β) (m : ℕ) (hm : 1 ≤ m) (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) : IsAdmissibleStream (I.nextStream m φ hφ)

The §2 recursion preserves the smooth joint space-time profile and its integer space-time periodicity.