Abstract-real arithmetic of the centered ergodic estimates

Proved real-variable estimates for the centered ergodic argument

theorem AVenhance.Infra.Section5.Contracts.sd_arith_final {x y κ ν ψ B A K Cd c₀ c₁ c₂ cfl M ρ e d D₀ D₁ D₂ E : ℝ} (hK : 1 ≤ K) (hκ : 0 < κ) (hν : 0 < ν) (hνK : ν ≤ K) (hψ : 0 ≤ ψ) (hψκ : ψ ^ 2 ≤ K * κ * ν) (hx : 0 < x) (hy : 0 < y) (hρ : 0 < ρ) (hyx : y ≤ K * x) (hyρ : y ≤ K * ρ) (he : 0 ≤ e) (hed : e ≤ d) (hB : 0 ≤ B) (hA : 0 ≤ A) (hCd : 0 ≤ Cd) (hc₀ : 0 ≤ c₀) (hc₁ : 0 ≤ c₁) (hc₂ : 0 ≤ c₂) (hcfl : 0 ≤ cfl) (hM : 0 ≤ M) (hD₀ : 0 ≤ D₀) (hD₁ : 0 ≤ D₁) (hD₂ : 0 ≤ D₂) (hD₀b : √ν * D₀ ≤ A * B) (hD₁b : √ν * D₁ ≤ A * (A / ρ) * B) (hD₂b : √ν * D₂ ≤ A * (A / ρ) * B) (hE : 0 ≤ E) (hEb : (ρ ^ 2)⁻¹ * E ≤ M * d) : 2 * ((144 * Cd * y * (c₀ * ψ * e / x) + cfl * e * ψ) * D₀ + 144 * Cd * y * (c₁ * ψ * e) * D₁ + 144 * Cd * y * (c₁ * ψ * e) * D₂ + 144 * Cd * c₂ * B * ψ * ((ρ ^ 2)⁻¹ * E)) ≤ (2 * (144 * Cd * c₀ * K + cfl) * √K * A + 576 * Cd * c₁ * A ^ 2 * K * √K + 288 * Cd * c₂ * M * K) * d * √κ * B