A0CoreContract: the main theorem at ingredient level

The content of the main theorem, for the given stream sequence and limit field (the limit field from the regularity estimates agrees with the given one by uniqueness of limits).

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.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)

The pointwise limit of periodic streams is periodic.

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.limit_aestronglyMeasurable {Φ : ℕ → ℝ → 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) μ

The pointwise limit of admissible streams is jointly measurable.

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.a0Core (β C₀ : ℝ) (hβ : 6 / 5 ≤ β) : A0CoreContract β C₀