The limit field of a stream sequence, packaged

All regularity facts about φ = lim Φ_M needed for tail_sup and the transport limit.

theorem AVenhance.Infra.FullTheorem.Limit.limit_periodic {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {φ : ℝ → Homogenization.Vec 2 → ℝ} (hΦ : ∀ (M : ℕ), IsAdmissibleStream (Φ M)) (htend : ∀ (t : ℝ) (x : Homogenization.Vec 2), Filter.Tendsto (fun (M : ℕ) => Φ M t x) Filter.atTop (nhds (φ t x))) (t : ℝ) : IsZ2Periodic (φ t)

theorem AVenhance.Infra.FullTheorem.Limit.limit_meas {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {φ : ℝ → Homogenization.Vec 2 → ℝ} (hΦ : ∀ (M : ℕ), IsAdmissibleStream (Φ M)) (htend : ∀ (t : ℝ) (x : Homogenization.Vec 2), Filter.Tendsto (fun (M : ℕ) => Φ M t x) Filter.atTop (nhds (φ t x))) (μ : MeasureTheory.Measure (ℝ × Homogenization.Vec 2)) : MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) μ

theorem AVenhance.Infra.FullTheorem.limit_package {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {φ : ℝ → Homogenization.Vec 2 → ℝ} (htend : ∀ (t : ℝ) (x : Homogenization.Vec 2), Filter.Tendsto (fun (M : ℕ) => Φ M t x) Filter.atTop (nhds (φ t x))) : ∃ (Ct : ℝ) (Bφ : ℝ), 0 ≤ Ct ∧ 0 ≤ Bφ ∧ (∀ (M : ℕ) (t : ℝ) (x : Homogenization.Vec 2), |φ t x - Φ M t x| ≤ Ct * epsilon β I.Λ (M + 1) ^ β) ∧ MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ)) ∧ (∀ t ∈ Set.Icc 0 1, IsZ2Periodic (φ t)) ∧ (∀ t ∈ Set.Icc 0 1, Differentiable ℝ (φ t)) ∧ MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => streamVel φ p.1 p.2) (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ)) ∧ (∀ t ∈ Set.Icc 0 1, IsZ2Periodic (streamVel φ t)) ∧ IsDivFree (streamVel φ) ∧ ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖streamVel φ t x‖ ≤ Bφ

Regularity package for the limit field.