Step 4: analytic snorm bounds for the flow slice

FlowForErgodicBound A e X (the derivative bounds |∇ⁿX| ≤ A n! (A/e)^{n-1}) gives ⟦X⟧_{j,2A/e} ≤ K e for every j ≥ 1, with K the absolute constant of exists_poly_le_two_pow.

theorem AVenhance.Infra.Section5.AnalyticBridge.sq_succ_le_of_poly {K : ℝ} (hK : ∀ (n : ℕ), (↑n + 3) ^ 5 ≤ K * 2 ^ n) (j : ℕ) : (↑j + 1) ^ 2 ≤ K * 2 ^ j

(j+1)² ≤ K 2^j.

theorem AVenhance.Infra.Section5.AnalyticBridge.flow_bound_real {K : ℝ} (hK : ∀ (n : ℕ), (↑n + 3) ^ 5 ≤ K * 2 ^ n) {A e : ℝ} (hA : 0 < A) (he : 0 < e) (k : ℕ) : A * ↑(k + 1).factorial * (A / e) ^ k ≤ K * e * (2 * A / e) ^ (k + 1) * ↑(k + 1).factorial / (↑(k + 1) + 1) ^ 2

Abstract-real core of step 4.

theorem AVenhance.Infra.Section5.AnalyticBridge.snorm_flow_le {K : ℝ} (hK : ∀ (n : ℕ), (↑n + 3) ^ 5 ≤ K * 2 ^ n) {A e : ℝ} (hA : 0 < A) (he : 0 < e) {X : Homogenization.Vec 2 → Homogenization.Vec 2} (hX : FlowForErgodicBound A e X) (j : ℕ) (hj : 1 ≤ j) : FaaDiBruno.snorm X j (2 * A / e) ≤ ENNReal.ofReal (K * e)

Step 4: ⟦X⟧_{j,2A/e} ≤ K e for j ≥ 1.