Regularity data of the limit field

limit_data β: a constant C_t ≥ 1 such that for every stream sequence and every pointwise limit φ of it, φ satisfies the tail estimate and the measurability/periodicity/boundedness hypotheses of tail_sup.

theorem AVenhance.Infra.FullTheorem.NoSel.limit_data (β : ℝ) : ∃ (Ct : ℝ), 1 ≤ Ct ∧ ∀ (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ), IsStreamSeq I Φ → ∀ (φ : ℝ → Homogenization.Vec 2 → ℝ), (∀ (t : ℝ) (x : Homogenization.Vec 2), Filter.Tendsto (fun (M : ℕ) => Φ M t x) Filter.atTop (nhds (φ t x))) → ∃ (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φ