The analytic case of r.LeBron.2, proved

analyticUniform_contract: assembly of the two cases M ≤ m₀ − 1 (case_small) and M ≥ m₀ (case_big), with the scale ε_{m₀-1} converted to a power of the analytic radius R (epsilon_mTheta0_lower, inv_rpow_le).

noncomputable def AVenhance.Infra.FullTheorem.Contracts.unifP (β : ℝ) : ℝ

The exponent of R^{-p}: p = q/(1+γ/2) · e.

Equations

• AVenhance.Infra.FullTheorem.Contracts.unifP β = AVenhance.q β / (1 + AVenhance.gamma β / 2) * AVenhance.Infra.FullTheorem.unifE β

theorem AVenhance.Infra.FullTheorem.Contracts.AnalyticUniform.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.Contracts.AnalyticUniform.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.Contracts.analyticUniform_contract (β C₀ : ℝ) : AnalyticUniformContract β C₀