Smoothness and periodicity of the two actual source errors used by tiny.

theorem AVenhance.Infra.Section5.Integration.BigBoundMeanZeroData.meanZeroData_matrixMulVec_contDiff {A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {V : Homogenization.Vec 2 → Homogenization.Vec 2} (hA : ContDiff ℝ (↑⊤) A) (hV : ContDiff ℝ (↑⊤) V) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => (A x).mulVec (V x)

theorem AVenhance.Infra.Section5.Integration.actual_sourceErrors_regular_of_iterates {β : ℝ} (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 → ℝ) (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) : (ContDiff ℝ (↑⊤) (sourceErrorD I hΦ m κm (T (Nstar β)) t) ∧ IsZ2Periodic (sourceErrorD I hΦ m κm (T (Nstar β)) t)) ∧ ContDiff ℝ (↑⊤) (iterateError I hΦ m κm κprev T t) ∧ IsZ2Periodic (iterateError I hΦ m κm κprev T t)

At a positive time, sourceErrorD and iterateError are smooth and periodic under the actual big-bound estimate classical and iterate premises.